From nobody Mon Oct 6 15:14:23 2025 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 40ECA28A407 for ; Mon, 21 Jul 2025 08:24:58 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753086301; cv=none; b=bsOY0O7FM8C5BWeFZOmAaicOAyFon/ZcVy3rITE116AGi/FqPIKbJwo+JlHZe54SwPM5QjSNDrcusheyWNJT/LF2BXL7Gx432f4QINg4/Hxbvi/2tYbxxPa4Xk0e0TYh6E8it1G51tDuws/9DPXjTe9o5/KNEUFZuhCQij4m8NU= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753086301; c=relaxed/simple; bh=YF3Zs+lTFKQuTNQ8XT13bw9XUnyalmK79oYC57L6+Yw=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=ItgkkymuYfz8/M+idNJeYHnb/IS78Cv9UhoTjFA5F1L9iK/APUXgAEH4H4mcVEcoLc28mycYjGtshbMBPtrVdxRBgqn2zA0WHZb73mqIduQHD5KLUSPoJwz/xfDHcRBCKNbkRRPLm+0+KviGrcxcYYKU7ym4S8Ulx6OrnH/obJ0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=OWIwSHUA; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="OWIwSHUA" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1753086298; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=6k/FmSevEF5yFErWOF/sff5A8U3b2lGj0tKTgrYZvJo=; b=OWIwSHUAOxHsFVOYlME/anfcH0z6bHCtpJ1Hmdj1XO6U1fzIZ02tvY/XJCW81fMUqp8iT4 qzp+C9pwNC9Pl592SSk5J0mE7zhKmPSKCfPAsvYr4+Mz7+1KyfW5VM9xU0O6eww8gRDUJJ NnQe/P/n96NKc5rRaJ8sC9HeR9xWJWU= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-632-qK0cpccEOkesV5OtM1BvIg-1; Mon, 21 Jul 2025 04:24:56 -0400 X-MC-Unique: qK0cpccEOkesV5OtM1BvIg-1 X-Mimecast-MFC-AGG-ID: qK0cpccEOkesV5OtM1BvIg_1753086295 Received: from mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.17]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id C794219560B5; Mon, 21 Jul 2025 08:24:54 +0000 (UTC) Received: from gmonaco-thinkpadt14gen3.rmtit.com (unknown [10.44.32.136]) by mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 714A2195608D; Mon, 21 Jul 2025 08:24:49 +0000 (UTC) From: Gabriele Monaco To: linux-kernel@vger.kernel.org, Steven Rostedt , Jonathan Corbet , Masami Hiramatsu , linux-trace-kernel@vger.kernel.org, linux-doc@vger.kernel.org Cc: Gabriele Monaco , Ingo Molnar , Peter Zijlstra , Nam Cao , Tomas Glozar , Juri Lelli , Clark Williams , John Kacur Subject: [PATCH v4 12/14] rv: Replace tss and sncid monitors with more complete sts Date: Mon, 21 Jul 2025 10:23:22 +0200 Message-ID: <20250721082325.71554-13-gmonaco@redhat.com> In-Reply-To: <20250721082325.71554-1-gmonaco@redhat.com> References: <20250721082325.71554-1-gmonaco@redhat.com> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-Scanned-By: MIMEDefang 3.0 on 10.30.177.17 Content-Type: text/plain; charset="utf-8" The tss monitor currently guarantees task switches can happen only while scheduling, whereas the sncid monitor enforces scheduling occurs with interrupt disabled. Replace the monitors with a more comprehensive specification which implies both but also ensures that: * each scheduler call disable interrupts to switch * each task switch happens with interrupts disabled Cc: Ingo Molnar Cc: Peter Zijlstra fixup sts remove sncid Signed-off-by: Gabriele Monaco Acked-by: Nam Cao --- Documentation/trace/rv/monitor_sched.rst | 87 +++++----- kernel/trace/rv/Kconfig | 3 +- kernel/trace/rv/Makefile | 3 +- kernel/trace/rv/monitors/sncid/Kconfig | 15 -- kernel/trace/rv/monitors/sncid/sncid.c | 95 ----------- kernel/trace/rv/monitors/sncid/sncid.h | 49 ------ kernel/trace/rv/monitors/sncid/sncid_trace.h | 15 -- kernel/trace/rv/monitors/sts/Kconfig | 19 +++ kernel/trace/rv/monitors/sts/sts.c | 156 ++++++++++++++++++ kernel/trace/rv/monitors/sts/sts.h | 117 +++++++++++++ .../{tss/tss_trace.h =3D> sts/sts_trace.h} | 8 +- kernel/trace/rv/monitors/tss/Kconfig | 14 -- kernel/trace/rv/monitors/tss/tss.c | 90 ---------- kernel/trace/rv/monitors/tss/tss.h | 47 ------ kernel/trace/rv/rv_trace.h | 3 +- tools/verification/models/sched/sncid.dot | 18 -- tools/verification/models/sched/sts.dot | 38 +++++ tools/verification/models/sched/tss.dot | 18 -- 18 files changed, 385 insertions(+), 410 deletions(-) delete mode 100644 kernel/trace/rv/monitors/sncid/Kconfig delete mode 100644 kernel/trace/rv/monitors/sncid/sncid.c delete mode 100644 kernel/trace/rv/monitors/sncid/sncid.h delete mode 100644 kernel/trace/rv/monitors/sncid/sncid_trace.h create mode 100644 kernel/trace/rv/monitors/sts/Kconfig create mode 100644 kernel/trace/rv/monitors/sts/sts.c create mode 100644 kernel/trace/rv/monitors/sts/sts.h rename kernel/trace/rv/monitors/{tss/tss_trace.h =3D> sts/sts_trace.h} (67= %) delete mode 100644 kernel/trace/rv/monitors/tss/Kconfig delete mode 100644 kernel/trace/rv/monitors/tss/tss.c delete mode 100644 kernel/trace/rv/monitors/tss/tss.h delete mode 100644 tools/verification/models/sched/sncid.dot create mode 100644 tools/verification/models/sched/sts.dot delete mode 100644 tools/verification/models/sched/tss.dot diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace= /rv/monitor_sched.rst index 24b2c62a3bc26..6c4c00216c07a 100644 --- a/Documentation/trace/rv/monitor_sched.rst +++ b/Documentation/trace/rv/monitor_sched.rst @@ -40,26 +40,6 @@ defined in by Daniel Bristot in [1]. =20 Currently we included the following: =20 -Monitor tss -~~~~~~~~~~~ - -The task switch while scheduling (tss) monitor ensures a task switch happe= ns -only in scheduling context, that is inside a call to `__schedule`:: - - | - | - v - +-----------------+ - | thread | <+ - +-----------------+ | - | | - | schedule_entry | schedule_exit - v | - sched_switch | - +--------------- | - | sched | - +--------------> -+ - Monitor sco ~~~~~~~~~~~ =20 @@ -144,26 +124,55 @@ does not enable preemption:: | scheduling_contex -+ =20 -Monitor sncid -~~~~~~~~~~~~~ - -The schedule not called with interrupt disabled (sncid) monitor ensures -schedule is not called with interrupt disabled:: +Monitor sts +~~~~~~~~~~~ =20 - | - | - v - schedule_entry +--------------+ - schedule_exit | | - +----------------- | can_sched | - | | | - +----------------> | | <+ - +--------------+ | - | | - | irq_disable | irq_enable - v | - | - cant_sched -+ +The schedule implies task switch (sts) monitor ensures a task switch happe= ns +only in scheduling context and up to once, as well as scheduling occurs wi= th +interrupts enabled but no task switch can happen before interrupts are +disabled. When the next task picked for execution is the same as the previ= ously +running one, no real task switch occurs but interrupts are disabled noneth= eless:: + + irq_entry | + +----+ | + v | v + +------------+ irq_enable #=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D# irq_disable + | | ------------> H H irq_entry + | cant_sched | <------------ H H irq_enable + | | irq_disable H can_sched H --------------+ + +------------+ H H | + H H | + +---------------> H H <-------------+ + | #=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D# + | | + schedule_exit | schedule_entry + | v + | +-------------------+ irq_enable + | | scheduling | <---------------+ + | +-------------------+ | + | | | + | | irq_disable +--------+ irq_entry + | v | | --------+ + | +-------------------+ irq_entry | in_irq | | + | | | -----------> | | <-------+ + | | disable_to_switch | +--------+ + | | | --+ + | +-------------------+ | + | | | + | | sched_switch | + | v | + | +-------------------+ | + | | switching | | irq_enable + | +-------------------+ | + | | | + | | irq_enable | + | v | + | +-------------------+ | + +-- | enable_to_exit | <-+ + +-------------------+ + ^ | irq_disable + | | irq_entry + +---------------+ irq_enable =20 References ---------- diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 34164eb4ec913..b688b24081c8e 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -50,12 +50,11 @@ source "kernel/trace/rv/monitors/wip/Kconfig" source "kernel/trace/rv/monitors/wwnr/Kconfig" =20 source "kernel/trace/rv/monitors/sched/Kconfig" -source "kernel/trace/rv/monitors/tss/Kconfig" source "kernel/trace/rv/monitors/sco/Kconfig" source "kernel/trace/rv/monitors/snroc/Kconfig" source "kernel/trace/rv/monitors/scpd/Kconfig" source "kernel/trace/rv/monitors/snep/Kconfig" -source "kernel/trace/rv/monitors/sncid/Kconfig" +source "kernel/trace/rv/monitors/sts/Kconfig" # Add new sched monitors here =20 source "kernel/trace/rv/monitors/rtapp/Kconfig" diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 13ec2944c6650..1939d3d7621c6 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -6,15 +6,14 @@ obj-$(CONFIG_RV) +=3D rv.o obj-$(CONFIG_RV_MON_WIP) +=3D monitors/wip/wip.o obj-$(CONFIG_RV_MON_WWNR) +=3D monitors/wwnr/wwnr.o obj-$(CONFIG_RV_MON_SCHED) +=3D monitors/sched/sched.o -obj-$(CONFIG_RV_MON_TSS) +=3D monitors/tss/tss.o obj-$(CONFIG_RV_MON_SCO) +=3D monitors/sco/sco.o obj-$(CONFIG_RV_MON_SNROC) +=3D monitors/snroc/snroc.o obj-$(CONFIG_RV_MON_SCPD) +=3D monitors/scpd/scpd.o obj-$(CONFIG_RV_MON_SNEP) +=3D monitors/snep/snep.o -obj-$(CONFIG_RV_MON_SNCID) +=3D monitors/sncid/sncid.o obj-$(CONFIG_RV_MON_RTAPP) +=3D monitors/rtapp/rtapp.o obj-$(CONFIG_RV_MON_PAGEFAULT) +=3D monitors/pagefault/pagefault.o obj-$(CONFIG_RV_MON_SLEEP) +=3D monitors/sleep/sleep.o +obj-$(CONFIG_RV_MON_STS) +=3D monitors/sts/sts.o # Add new monitors here obj-$(CONFIG_RV_REACTORS) +=3D rv_reactors.o obj-$(CONFIG_RV_REACT_PRINTK) +=3D reactor_printk.o diff --git a/kernel/trace/rv/monitors/sncid/Kconfig b/kernel/trace/rv/monit= ors/sncid/Kconfig deleted file mode 100644 index 3a5639feaaaf6..0000000000000 --- a/kernel/trace/rv/monitors/sncid/Kconfig +++ /dev/null @@ -1,15 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-only -# -config RV_MON_SNCID - depends on RV - depends on TRACE_IRQFLAGS - depends on RV_MON_SCHED - default y - select DA_MON_EVENTS_IMPLICIT - bool "sncid monitor" - help - Monitor to ensure schedule is not called with interrupt disabled. - This monitor is part of the sched monitors collection. - - For further information, see: - Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/sncid/sncid.c b/kernel/trace/rv/monit= ors/sncid/sncid.c deleted file mode 100644 index c8491f4263650..0000000000000 --- a/kernel/trace/rv/monitors/sncid/sncid.c +++ /dev/null @@ -1,95 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include -#include -#include -#include -#include -#include -#include -#include - -#define MODULE_NAME "sncid" - -#include -#include -#include -#include - -#include "sncid.h" - -static struct rv_monitor rv_sncid; -DECLARE_DA_MON_PER_CPU(sncid, unsigned char); - -static void handle_irq_disable(void *data, unsigned long ip, unsigned long= parent_ip) -{ - da_handle_event_sncid(irq_disable_sncid); -} - -static void handle_irq_enable(void *data, unsigned long ip, unsigned long = parent_ip) -{ - da_handle_start_event_sncid(irq_enable_sncid); -} - -static void handle_schedule_entry(void *data, bool preempt) -{ - da_handle_start_event_sncid(schedule_entry_sncid); -} - -static void handle_schedule_exit(void *data, bool is_switch) -{ - da_handle_start_event_sncid(schedule_exit_sncid); -} - -static int enable_sncid(void) -{ - int retval; - - retval =3D da_monitor_init_sncid(); - if (retval) - return retval; - - rv_attach_trace_probe("sncid", irq_disable, handle_irq_disable); - rv_attach_trace_probe("sncid", irq_enable, handle_irq_enable); - rv_attach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry); - rv_attach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit); - - return 0; -} - -static void disable_sncid(void) -{ - rv_sncid.enabled =3D 0; - - rv_detach_trace_probe("sncid", irq_disable, handle_irq_disable); - rv_detach_trace_probe("sncid", irq_enable, handle_irq_enable); - rv_detach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry); - rv_detach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit); - - da_monitor_destroy_sncid(); -} - -static struct rv_monitor rv_sncid =3D { - .name =3D "sncid", - .description =3D "schedule not called with interrupt disabled.", - .enable =3D enable_sncid, - .disable =3D disable_sncid, - .reset =3D da_monitor_reset_all_sncid, - .enabled =3D 0, -}; - -static int __init register_sncid(void) -{ - return rv_register_monitor(&rv_sncid, &rv_sched); -} - -static void __exit unregister_sncid(void) -{ - rv_unregister_monitor(&rv_sncid); -} - -module_init(register_sncid); -module_exit(unregister_sncid); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("Gabriele Monaco "); -MODULE_DESCRIPTION("sncid: schedule not called with interrupt disabled."); diff --git a/kernel/trace/rv/monitors/sncid/sncid.h b/kernel/trace/rv/monit= ors/sncid/sncid.h deleted file mode 100644 index 21304725142bc..0000000000000 --- a/kernel/trace/rv/monitors/sncid/sncid.h +++ /dev/null @@ -1,49 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ -/* - * Automatically generated C representation of sncid automaton - * For further information about this format, see kernel documentation: - * Documentation/trace/rv/deterministic_automata.rst - */ - -enum states_sncid { - can_sched_sncid =3D 0, - cant_sched_sncid, - state_max_sncid -}; - -#define INVALID_STATE state_max_sncid - -enum events_sncid { - irq_disable_sncid =3D 0, - irq_enable_sncid, - schedule_entry_sncid, - schedule_exit_sncid, - event_max_sncid -}; - -struct automaton_sncid { - char *state_names[state_max_sncid]; - char *event_names[event_max_sncid]; - unsigned char function[state_max_sncid][event_max_sncid]; - unsigned char initial_state; - bool final_states[state_max_sncid]; -}; - -static const struct automaton_sncid automaton_sncid =3D { - .state_names =3D { - "can_sched", - "cant_sched" - }, - .event_names =3D { - "irq_disable", - "irq_enable", - "schedule_entry", - "schedule_exit" - }, - .function =3D { - { cant_sched_sncid, INVALID_STATE, can_sched_sncid, can_sched_sncid }, - { INVALID_STATE, can_sched_sncid, INVALID_STATE, INVALID_STATE }, - }, - .initial_state =3D can_sched_sncid, - .final_states =3D { 1, 0 }, -}; diff --git a/kernel/trace/rv/monitors/sncid/sncid_trace.h b/kernel/trace/rv= /monitors/sncid/sncid_trace.h deleted file mode 100644 index 3ce42a57671d4..0000000000000 --- a/kernel/trace/rv/monitors/sncid/sncid_trace.h +++ /dev/null @@ -1,15 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ - -/* - * Snippet to be included in rv_trace.h - */ - -#ifdef CONFIG_RV_MON_SNCID -DEFINE_EVENT(event_da_monitor, event_sncid, - TP_PROTO(char *state, char *event, char *next_state, bool final_stat= e), - TP_ARGS(state, event, next_state, final_state)); - -DEFINE_EVENT(error_da_monitor, error_sncid, - TP_PROTO(char *state, char *event), - TP_ARGS(state, event)); -#endif /* CONFIG_RV_MON_SNCID */ diff --git a/kernel/trace/rv/monitors/sts/Kconfig b/kernel/trace/rv/monitor= s/sts/Kconfig new file mode 100644 index 0000000000000..7d1ff0f6fc91e --- /dev/null +++ b/kernel/trace/rv/monitors/sts/Kconfig @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_STS + depends on RV + depends on TRACE_IRQFLAGS + depends on RV_MON_SCHED + default y + select DA_MON_EVENTS_IMPLICIT + bool "sts monitor" + help + Monitor to ensure relationships between scheduler and task switches + * the scheduler is called and returns with interrupts disabled + * each call to the scheduler has up to one switch + * switches only happen inside the scheduler + * each call to the scheduler disables interrupts to switch + This monitor is part of the sched monitors collection. + + For further information, see: + Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/sts/sts.c b/kernel/trace/rv/monitors/= sts/sts.c new file mode 100644 index 0000000000000..c4a9cd67c1d21 --- /dev/null +++ b/kernel/trace/rv/monitors/sts/sts.c @@ -0,0 +1,156 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "sts" + +#include +#include +#include +#include +#include + +#include "sts.h" + +static struct rv_monitor rv_sts; +DECLARE_DA_MON_PER_CPU(sts, unsigned char); + +#ifdef CONFIG_X86_LOCAL_APIC +#include + +static void handle_vector_irq_entry(void *data, int vector) +{ + da_handle_event_sts(irq_entry_sts); +} + +static void attach_vector_irq(void) +{ + rv_attach_trace_probe("sts", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_attach_trace_probe("sts", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_attach_trace_probe("sts", reschedule_entry, handle_vector_irq_entry); + rv_attach_trace_probe("sts", call_function_entry, handle_vector_irq_entr= y); + rv_attach_trace_probe("sts", call_function_single_entry, handle_vector_i= rq_entry); + } +} + +static void detach_vector_irq(void) +{ + rv_detach_trace_probe("sts", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_detach_trace_probe("sts", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_detach_trace_probe("sts", reschedule_entry, handle_vector_irq_entry); + rv_detach_trace_probe("sts", call_function_entry, handle_vector_irq_entr= y); + rv_detach_trace_probe("sts", call_function_single_entry, handle_vector_i= rq_entry); + } +} + +#else +/* We assume irq_entry tracepoints are sufficient on other architectures */ +static void attach_vector_irq(void) { } +static void detach_vector_irq(void) { } +#endif + +static void handle_irq_disable(void *data, unsigned long ip, unsigned long= parent_ip) +{ + da_handle_event_sts(irq_disable_sts); +} + +static void handle_irq_enable(void *data, unsigned long ip, unsigned long = parent_ip) +{ + da_handle_event_sts(irq_enable_sts); +} + +static void handle_irq_entry(void *data, int irq, struct irqaction *action) +{ + da_handle_event_sts(irq_entry_sts); +} + +static void handle_sched_switch(void *data, bool preempt, + struct task_struct *prev, + struct task_struct *next, + unsigned int prev_state) +{ + da_handle_event_sts(sched_switch_sts); +} + +static void handle_schedule_entry(void *data, bool preempt) +{ + da_handle_event_sts(schedule_entry_sts); +} + +static void handle_schedule_exit(void *data, bool is_switch) +{ + da_handle_start_event_sts(schedule_exit_sts); +} + +static int enable_sts(void) +{ + int retval; + + retval =3D da_monitor_init_sts(); + if (retval) + return retval; + + rv_attach_trace_probe("sts", irq_disable, handle_irq_disable); + rv_attach_trace_probe("sts", irq_enable, handle_irq_enable); + rv_attach_trace_probe("sts", irq_handler_entry, handle_irq_entry); + rv_attach_trace_probe("sts", sched_switch, handle_sched_switch); + rv_attach_trace_probe("sts", sched_entry_tp, handle_schedule_entry); + rv_attach_trace_probe("sts", sched_exit_tp, handle_schedule_exit); + attach_vector_irq(); + + return 0; +} + +static void disable_sts(void) +{ + rv_sts.enabled =3D 0; + + rv_detach_trace_probe("sts", irq_disable, handle_irq_disable); + rv_detach_trace_probe("sts", irq_enable, handle_irq_enable); + rv_detach_trace_probe("sts", irq_handler_entry, handle_irq_entry); + rv_detach_trace_probe("sts", sched_switch, handle_sched_switch); + rv_detach_trace_probe("sts", sched_entry_tp, handle_schedule_entry); + rv_detach_trace_probe("sts", sched_exit_tp, handle_schedule_exit); + detach_vector_irq(); + + da_monitor_destroy_sts(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_sts =3D { + .name =3D "sts", + .description =3D "schedule implies task switch.", + .enable =3D enable_sts, + .disable =3D disable_sts, + .reset =3D da_monitor_reset_all_sts, + .enabled =3D 0, +}; + +static int __init register_sts(void) +{ + return rv_register_monitor(&rv_sts, &rv_sched); +} + +static void __exit unregister_sts(void) +{ + rv_unregister_monitor(&rv_sts); +} + +module_init(register_sts); +module_exit(unregister_sts); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco "); +MODULE_DESCRIPTION("sts: schedule implies task switch."); diff --git a/kernel/trace/rv/monitors/sts/sts.h b/kernel/trace/rv/monitors/= sts/sts.h new file mode 100644 index 0000000000000..3368b6599a005 --- /dev/null +++ b/kernel/trace/rv/monitors/sts/sts.h @@ -0,0 +1,117 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of sts automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +enum states_sts { + can_sched_sts =3D 0, + cant_sched_sts, + disable_to_switch_sts, + enable_to_exit_sts, + in_irq_sts, + scheduling_sts, + switching_sts, + state_max_sts +}; + +#define INVALID_STATE state_max_sts + +enum events_sts { + irq_disable_sts =3D 0, + irq_enable_sts, + irq_entry_sts, + sched_switch_sts, + schedule_entry_sts, + schedule_exit_sts, + event_max_sts +}; + +struct automaton_sts { + char *state_names[state_max_sts]; + char *event_names[event_max_sts]; + unsigned char function[state_max_sts][event_max_sts]; + unsigned char initial_state; + bool final_states[state_max_sts]; +}; + +static const struct automaton_sts automaton_sts =3D { + .state_names =3D { + "can_sched", + "cant_sched", + "disable_to_switch", + "enable_to_exit", + "in_irq", + "scheduling", + "switching" + }, + .event_names =3D { + "irq_disable", + "irq_enable", + "irq_entry", + "sched_switch", + "schedule_entry", + "schedule_exit" + }, + .function =3D { + { + cant_sched_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + scheduling_sts, + INVALID_STATE + }, + { + INVALID_STATE, + can_sched_sts, + cant_sched_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + INVALID_STATE, + enable_to_exit_sts, + in_irq_sts, + switching_sts, + INVALID_STATE, + INVALID_STATE + }, + { + enable_to_exit_sts, + enable_to_exit_sts, + enable_to_exit_sts, + INVALID_STATE, + INVALID_STATE, + can_sched_sts + }, + { + INVALID_STATE, + scheduling_sts, + in_irq_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + disable_to_switch_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + INVALID_STATE, + enable_to_exit_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + }, + .initial_state =3D can_sched_sts, + .final_states =3D { 1, 0, 0, 0, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/tss/tss_trace.h b/kernel/trace/rv/mon= itors/sts/sts_trace.h similarity index 67% rename from kernel/trace/rv/monitors/tss/tss_trace.h rename to kernel/trace/rv/monitors/sts/sts_trace.h index 4619dbb50cc06..d78beb58d5b3d 100644 --- a/kernel/trace/rv/monitors/tss/tss_trace.h +++ b/kernel/trace/rv/monitors/sts/sts_trace.h @@ -4,12 +4,12 @@ * Snippet to be included in rv_trace.h */ =20 -#ifdef CONFIG_RV_MON_TSS -DEFINE_EVENT(event_da_monitor, event_tss, +#ifdef CONFIG_RV_MON_STS +DEFINE_EVENT(event_da_monitor, event_sts, TP_PROTO(char *state, char *event, char *next_state, bool final_stat= e), TP_ARGS(state, event, next_state, final_state)); =20 -DEFINE_EVENT(error_da_monitor, error_tss, +DEFINE_EVENT(error_da_monitor, error_sts, TP_PROTO(char *state, char *event), TP_ARGS(state, event)); -#endif /* CONFIG_RV_MON_TSS */ +#endif /* CONFIG_RV_MON_STS */ diff --git a/kernel/trace/rv/monitors/tss/Kconfig b/kernel/trace/rv/monitor= s/tss/Kconfig deleted file mode 100644 index 479f86f52e60d..0000000000000 --- a/kernel/trace/rv/monitors/tss/Kconfig +++ /dev/null @@ -1,14 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-only -# -config RV_MON_TSS - depends on RV - depends on RV_MON_SCHED - default y - select DA_MON_EVENTS_IMPLICIT - bool "tss monitor" - help - Monitor to ensure sched_switch happens only in scheduling context. - This monitor is part of the sched monitors collection. - - For further information, see: - Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/tss/tss.c b/kernel/trace/rv/monitors/= tss/tss.c deleted file mode 100644 index 95ebd15131f52..0000000000000 --- a/kernel/trace/rv/monitors/tss/tss.c +++ /dev/null @@ -1,90 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include -#include -#include -#include -#include -#include -#include -#include - -#define MODULE_NAME "tss" - -#include -#include -#include - -#include "tss.h" - -static struct rv_monitor rv_tss; -DECLARE_DA_MON_PER_CPU(tss, unsigned char); - -static void handle_sched_switch(void *data, bool preempt, - struct task_struct *prev, - struct task_struct *next, - unsigned int prev_state) -{ - da_handle_event_tss(sched_switch_tss); -} - -static void handle_schedule_entry(void *data, bool preempt) -{ - da_handle_event_tss(schedule_entry_tss); -} - -static void handle_schedule_exit(void *data, bool is_switch) -{ - da_handle_start_event_tss(schedule_exit_tss); -} - -static int enable_tss(void) -{ - int retval; - - retval =3D da_monitor_init_tss(); - if (retval) - return retval; - - rv_attach_trace_probe("tss", sched_switch, handle_sched_switch); - rv_attach_trace_probe("tss", sched_entry_tp, handle_schedule_entry); - rv_attach_trace_probe("tss", sched_exit_tp, handle_schedule_exit); - - return 0; -} - -static void disable_tss(void) -{ - rv_tss.enabled =3D 0; - - rv_detach_trace_probe("tss", sched_switch, handle_sched_switch); - rv_detach_trace_probe("tss", sched_entry_tp, handle_schedule_entry); - rv_detach_trace_probe("tss", sched_exit_tp, handle_schedule_exit); - - da_monitor_destroy_tss(); -} - -static struct rv_monitor rv_tss =3D { - .name =3D "tss", - .description =3D "task switch while scheduling.", - .enable =3D enable_tss, - .disable =3D disable_tss, - .reset =3D da_monitor_reset_all_tss, - .enabled =3D 0, -}; - -static int __init register_tss(void) -{ - return rv_register_monitor(&rv_tss, &rv_sched); -} - -static void __exit unregister_tss(void) -{ - rv_unregister_monitor(&rv_tss); -} - -module_init(register_tss); -module_exit(unregister_tss); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("Gabriele Monaco "); -MODULE_DESCRIPTION("tss: task switch while scheduling."); diff --git a/kernel/trace/rv/monitors/tss/tss.h b/kernel/trace/rv/monitors/= tss/tss.h deleted file mode 100644 index f0a36fda1b873..0000000000000 --- a/kernel/trace/rv/monitors/tss/tss.h +++ /dev/null @@ -1,47 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ -/* - * Automatically generated C representation of tss automaton - * For further information about this format, see kernel documentation: - * Documentation/trace/rv/deterministic_automata.rst - */ - -enum states_tss { - thread_tss =3D 0, - sched_tss, - state_max_tss -}; - -#define INVALID_STATE state_max_tss - -enum events_tss { - sched_switch_tss =3D 0, - schedule_entry_tss, - schedule_exit_tss, - event_max_tss -}; - -struct automaton_tss { - char *state_names[state_max_tss]; - char *event_names[event_max_tss]; - unsigned char function[state_max_tss][event_max_tss]; - unsigned char initial_state; - bool final_states[state_max_tss]; -}; - -static const struct automaton_tss automaton_tss =3D { - .state_names =3D { - "thread", - "sched" - }, - .event_names =3D { - "sched_switch", - "schedule_entry", - "schedule_exit" - }, - .function =3D { - { INVALID_STATE, sched_tss, INVALID_STATE }, - { sched_tss, INVALID_STATE, thread_tss }, - }, - .initial_state =3D thread_tss, - .final_states =3D { 1, 0 }, -}; diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index 044772515256a..fa9613cb94699 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -58,11 +58,10 @@ DECLARE_EVENT_CLASS(error_da_monitor, ); =20 #include -#include #include #include #include -#include +#include // Add new monitors based on CONFIG_DA_MON_EVENTS_IMPLICIT here =20 #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */ diff --git a/tools/verification/models/sched/sncid.dot b/tools/verification= /models/sched/sncid.dot deleted file mode 100644 index 072851721b50a..0000000000000 --- a/tools/verification/models/sched/sncid.dot +++ /dev/null @@ -1,18 +0,0 @@ -digraph state_automaton { - center =3D true; - size =3D "7,11"; - {node [shape =3D plaintext, style=3Dinvis, label=3D""] "__init_can_sched"= }; - {node [shape =3D ellipse] "can_sched"}; - {node [shape =3D plaintext] "can_sched"}; - {node [shape =3D plaintext] "cant_sched"}; - "__init_can_sched" -> "can_sched"; - "can_sched" [label =3D "can_sched", color =3D green3]; - "can_sched" -> "can_sched" [ label =3D "schedule_entry\nschedule_exit" ]; - "can_sched" -> "cant_sched" [ label =3D "irq_disable" ]; - "cant_sched" [label =3D "cant_sched"]; - "cant_sched" -> "can_sched" [ label =3D "irq_enable" ]; - { rank =3D min ; - "__init_can_sched"; - "can_sched"; - } -} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/m= odels/sched/sts.dot new file mode 100644 index 0000000000000..8f5f38be04d54 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center =3D true; + size =3D "7,11"; + {node [shape =3D plaintext, style=3Dinvis, label=3D""] "__init_can_sched"= }; + {node [shape =3D doublecircle] "can_sched"}; + {node [shape =3D circle] "can_sched"}; + {node [shape =3D circle] "cant_sched"}; + {node [shape =3D circle] "disable_to_switch"}; + {node [shape =3D circle] "enable_to_exit"}; + {node [shape =3D circle] "in_irq"}; + {node [shape =3D circle] "scheduling"}; + {node [shape =3D circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label =3D "can_sched", color =3D green3]; + "can_sched" -> "cant_sched" [ label =3D "irq_disable" ]; + "can_sched" -> "scheduling" [ label =3D "schedule_entry" ]; + "cant_sched" [label =3D "cant_sched"]; + "cant_sched" -> "can_sched" [ label =3D "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label =3D "irq_entry" ]; + "disable_to_switch" [label =3D "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label =3D "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label =3D "irq_entry" ]; + "disable_to_switch" -> "switching" [ label =3D "sched_switch" ]; + "enable_to_exit" [label =3D "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label =3D "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label =3D "irq_disable\nirq_entry\= nirq_enable" ]; + "in_irq" [label =3D "in_irq"]; + "in_irq" -> "in_irq" [ label =3D "irq_entry" ]; + "in_irq" -> "scheduling" [ label =3D "irq_enable" ]; + "scheduling" [label =3D "scheduling"]; + "scheduling" -> "disable_to_switch" [ label =3D "irq_disable" ]; + "switching" [label =3D "switching"]; + "switching" -> "enable_to_exit" [ label =3D "irq_enable" ]; + { rank =3D min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/models/sched/tss.dot b/tools/verification/m= odels/sched/tss.dot deleted file mode 100644 index 7dfa1d9121bbd..0000000000000 --- a/tools/verification/models/sched/tss.dot +++ /dev/null @@ -1,18 +0,0 @@ -digraph state_automaton { - center =3D true; - size =3D "7,11"; - {node [shape =3D plaintext] "sched"}; - {node [shape =3D plaintext, style=3Dinvis, label=3D""] "__init_thread"}; - {node [shape =3D ellipse] "thread"}; - {node [shape =3D plaintext] "thread"}; - "__init_thread" -> "thread"; - "sched" [label =3D "sched"]; - "sched" -> "sched" [ label =3D "sched_switch" ]; - "sched" -> "thread" [ label =3D "schedule_exit" ]; - "thread" [label =3D "thread", color =3D green3]; - "thread" -> "sched" [ label =3D "schedule_entry" ]; - { rank =3D min ; - "__init_thread"; - "thread"; - } -} --=20 2.50.1