From nobody Sun Oct 5 01:45:13 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 588D22DAFDE; Mon, 11 Aug 2025 08:41:01 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; cv=none; b=hhoHJgzdaM3ugm+F2ClhnmMy4vOvQJ8zZjGmjrZ72/cTRcCvlO87bK9yzOE3tjIbb7ma29kIpdZdqixSadLnw+GsI5E5CqXiF4p7Ixkt0Lm8XMZOp9xvNO/lr+VQu3ueEh5lkFISunJ9kH2O8e2j2CDIR0cXKPkHrvqeKWmEdU0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; c=relaxed/simple; bh=Uesn38aob0MqcbKV3gio0rTGdqwKMtOR7nm2jvHxr4I=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=g58AFnt+81UpxnLbBoiKhkftvKDHf1hZbjs+ZqnCjF604DcvYzxNWPpH6tjcVO6ZRE+5AREK+iIP1K05cOyEMRy7+xlGs8oR1CMU5C/O5d37VJBL5w2Kvo2C+xRtkMQHWqLfeoMwH3J5klf4/y6KIk+eGwCbeZ1o0k0R1i4am8U= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=UKHHsrum; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=vdlbuMkq; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="UKHHsrum"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="vdlbuMkq" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1754901659; 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=sTX3RTvCUX/Mm46SCDPZbioQpsq3KjD49jPHt93BLXs=; b=UKHHsrumNOkON6Z0VDIVBY+AFXuS7Ritneuk9PnnLWG122N/Stdpck6ankwJbUu7A+E6Y/ LCQ5wO40aeLqWQnQGzvCe54KoD9iQzf0jKPeegq1egFRMEHCZrAITDG/ttzONf2LG/c0K8 gncBW4RfFs/KVmZbOZX1Y+P0U1s3Ovs/JkcQE1WduP1NOL9r6sr+bUIJPRhbBIRhwPCzxq r7o7xpnaReyulL2GS6xwm0WNN29xViEEkzl7N2ptplS/pJfiMvOnXU1Igr7fGURU9BMMLe nuI+Eh8ua8bQntZ5sHLHnEuCiGbXDdygibqnCve58Fr5krCtBOEhmEMDZX/F6g== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1754901659; 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=sTX3RTvCUX/Mm46SCDPZbioQpsq3KjD49jPHt93BLXs=; b=vdlbuMkqajmufI+zeF08puQzt3as4TXA1ChjyomdwhINlxsUd/ipwJ4LeVOkka0c+pvVIG Vn1V/oEeTVSyKsCA== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 1/5] rv/ltl: Prepare for other monitor types Date: Mon, 11 Aug 2025 10:40:49 +0200 Message-Id: In-Reply-To: References: 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 Content-Type: text/plain; charset="utf-8" rv/ltl_monitor.h is the template file used by all LTL monitors. But only per-task monitor is supported. Prepare to support for other monitor types: - Change the monitored target type into an opaque type which will be defined differently depending on the monitor type. This type is only defined as struct task_struct * for now. - Separate out the per-task-specific printf format and arguments, so that rv_cond_react() can be shared with other monitor types. No functional change intended. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v2: define the macros for DA usage as well --- include/linux/rv.h | 4 + include/rv/ltl_monitor.h | 85 +++++++++++-------- .../trace/rv/monitors/pagefault/pagefault.h | 2 + kernel/trace/rv/monitors/sleep/sleep.h | 2 + 4 files changed, 58 insertions(+), 35 deletions(-) diff --git a/include/linux/rv.h b/include/linux/rv.h index 14410a42faef..10a8be730d89 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -13,6 +13,10 @@ #define MAX_DA_NAME_LEN 32 #define MAX_DA_RETRY_RACING_EVENTS 3 =20 +#define RV_MON_GLOBAL 0 +#define RV_MON_PER_CPU 1 +#define RV_MON_PER_TASK 2 + #ifdef CONFIG_RV #include #include diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index 67031a774e3d..9dabc5b133a3 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -16,49 +16,63 @@ #error "Please include $(MODEL_NAME).h generated by rvgen" #endif =20 +#if LTL_MONITOR_TYPE =3D=3D RV_MON_PER_TASK + +#define TARGET_PRINT_FORMAT "%s[%d]" +#define TARGET_PRINT_ARGS(task) task->comm, task->pid + +typedef struct task_struct *monitor_target; + +#endif + #ifdef CONFIG_RV_REACTORS #define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) static struct rv_monitor RV_MONITOR_NAME; =20 -static void rv_cond_react(struct task_struct *task) +static void rv_cond_react(monitor_target target) { if (!rv_reacting_on() || !RV_MONITOR_NAME.react) return; - RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)": %s[%d]: violation= detected\n", - task->comm, task->pid); + + RV_MONITOR_NAME.react( + "rv: "__stringify(MONITOR_NAME)": "TARGET_PRINT_FORMAT": violation detec= ted\n", + TARGET_PRINT_ARGS(target)); } #else -static void rv_cond_react(struct task_struct *task) +static void rv_cond_react(monitor_target target) { } #endif =20 -static int ltl_monitor_slot =3D RV_PER_TASK_MONITOR_INIT; +static void ltl_atoms_fetch(monitor_target target, struct ltl_monitor *mon= ); +static void ltl_atoms_init(monitor_target target, struct ltl_monitor *mon,= bool target_creation); =20 -static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *= mon); -static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *m= on, bool task_creation); +#if LTL_MONITOR_TYPE =3D=3D RV_MON_PER_TASK +static int ltl_monitor_slot =3D RV_PER_TASK_MONITOR_INIT; =20 -static struct ltl_monitor *ltl_get_monitor(struct task_struct *task) +static struct ltl_monitor *ltl_get_monitor(monitor_target target) { - return &task->rv[ltl_monitor_slot].ltl_mon; + return &target->rv[ltl_monitor_slot].ltl_mon; } +#endif =20 -static void ltl_task_init(struct task_struct *task, bool task_creation) +static void ltl_target_init(monitor_target target, bool target_creation) { - struct ltl_monitor *mon =3D ltl_get_monitor(task); + struct ltl_monitor *mon =3D ltl_get_monitor(target); =20 memset(&mon->states, 0, sizeof(mon->states)); =20 for (int i =3D 0; i < LTL_NUM_ATOM; ++i) __set_bit(i, mon->unknown_atoms); =20 - ltl_atoms_init(task, mon, task_creation); - ltl_atoms_fetch(task, mon); + ltl_atoms_init(target, mon, target_creation); + ltl_atoms_fetch(target, mon); } =20 +#if LTL_MONITOR_TYPE =3D=3D RV_MON_PER_TASK static void handle_task_newtask(void *data, struct task_struct *task, unsi= gned long flags) { - ltl_task_init(task, true); + ltl_target_init(task, true); } =20 static int ltl_monitor_init(void) @@ -77,10 +91,10 @@ static int ltl_monitor_init(void) read_lock(&tasklist_lock); =20 for_each_process_thread(g, p) - ltl_task_init(p, false); + ltl_target_init(p, false); =20 for_each_present_cpu(cpu) - ltl_task_init(idle_task(cpu), false); + ltl_target_init(idle_task(cpu), false); =20 read_unlock(&tasklist_lock); =20 @@ -94,17 +108,18 @@ static void ltl_monitor_destroy(void) rv_put_task_monitor_slot(ltl_monitor_slot); ltl_monitor_slot =3D RV_PER_TASK_MONITOR_INIT; } +#endif =20 -static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor= *mon) +static void ltl_illegal_state(monitor_target target, struct ltl_monitor *m= on) { - CONCATENATE(trace_error_, MONITOR_NAME)(task); - rv_cond_react(task); + CONCATENATE(trace_error_, MONITOR_NAME)(target); + rv_cond_react(target); } =20 -static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor= *mon) +static void ltl_attempt_start(monitor_target target, struct ltl_monitor *m= on) { if (rv_ltl_all_atoms_known(mon)) - ltl_start(task, mon); + ltl_start(target, mon); } =20 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom ato= m, bool value) @@ -117,7 +132,7 @@ static inline void ltl_atom_set(struct ltl_monitor *mon= , enum ltl_atom atom, boo } =20 static void -ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigne= d long *next_state) +ltl_trace_event(monitor_target target, struct ltl_monitor *mon, unsigned l= ong *next_state) { const char *format_str =3D "%s"; DECLARE_SEQ_BUF(atoms, 64); @@ -137,10 +152,10 @@ ltl_trace_event(struct task_struct *task, struct ltl_= monitor *mon, unsigned long } } =20 - CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next); + CONCATENATE(trace_event_, MONITOR_NAME)(target, states, atoms.buffer, nex= t); } =20 -static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon) +static void ltl_validate(monitor_target target, struct ltl_monitor *mon) { DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) =3D {0}; =20 @@ -152,35 +167,35 @@ static void ltl_validate(struct task_struct *task, st= ruct ltl_monitor *mon) ltl_possible_next_states(mon, i, next_states); } =20 - ltl_trace_event(task, mon, next_states); + ltl_trace_event(target, mon, next_states); =20 memcpy(mon->states, next_states, sizeof(next_states)); =20 if (!rv_ltl_valid_state(mon)) - ltl_illegal_state(task, mon); + ltl_illegal_state(target, mon); } =20 -static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, = bool value) +static void ltl_atom_update(monitor_target target, enum ltl_atom atom, boo= l value) { - struct ltl_monitor *mon =3D ltl_get_monitor(task); + struct ltl_monitor *mon =3D ltl_get_monitor(target); =20 ltl_atom_set(mon, atom, value); - ltl_atoms_fetch(task, mon); + ltl_atoms_fetch(target, mon); =20 if (!rv_ltl_valid_state(mon)) { - ltl_attempt_start(task, mon); + ltl_attempt_start(target, mon); return; } =20 - ltl_validate(task, mon); + ltl_validate(target, mon); } =20 -static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum l= tl_atom atom, bool value) +static void __maybe_unused ltl_atom_pulse(monitor_target target, enum ltl_= atom atom, bool value) { - struct ltl_monitor *mon =3D ltl_get_monitor(task); + struct ltl_monitor *mon =3D ltl_get_monitor(target); =20 - ltl_atom_update(task, atom, value); + ltl_atom_update(target, atom, value); =20 ltl_atom_set(mon, atom, !value); - ltl_validate(task, mon); + ltl_validate(target, mon); } diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h b/kernel/trace/= rv/monitors/pagefault/pagefault.h index c580ec194009..d449af84c24c 100644 --- a/kernel/trace/rv/monitors/pagefault/pagefault.h +++ b/kernel/trace/rv/monitors/pagefault/pagefault.h @@ -11,6 +11,8 @@ =20 #define MONITOR_NAME pagefault =20 +#define LTL_MONITOR_TYPE RV_MON_PER_TASK + enum ltl_atom { LTL_PAGEFAULT, LTL_RT, diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monit= ors/sleep/sleep.h index 2ab46fd218d2..0c87875d9040 100644 --- a/kernel/trace/rv/monitors/sleep/sleep.h +++ b/kernel/trace/rv/monitors/sleep/sleep.h @@ -11,6 +11,8 @@ =20 #define MONITOR_NAME sleep =20 +#define LTL_MONITOR_TYPE RV_MON_PER_TASK + enum ltl_atom { LTL_ABORT_SLEEP, LTL_BLOCK_ON_RT_MUTEX, --=20 2.39.5 From nobody Sun Oct 5 01:45:13 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 A23E22DBF73; Mon, 11 Aug 2025 08:41:01 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; cv=none; b=aubzK6ke4KCL1agSiX9kvsEux7HH5ROP91UtrK7oWHGagnpNsIuTyAPP43ZVNONrXiMyZ8LFo920cuPspqgVZ1TWefgcWGpGU6XNFVuPSNr+Rf8pidKS4ZHci/HD+E2r7L3OAlcJRfIdvCGPfwS6/MYi1lXpcnZyE3fvzo3HZ6c= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; c=relaxed/simple; bh=3cgHXkt2+wvn9nm5uflyN+Y5IXr5ILwA4NGjMAsfYak=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=QvuPEbZfVR0J4AGRk+5vgmcbdORK4TUAClmzjoJaVfSVcJOso8pvu87kkaBcnRWKw3ZVA5lrchVrsLVzDuKBzkwlf2Lob7WeAe1uHWkOftgs1HQ0Fjdaz02CFeO3WZ3Q8H5mbK09qKy+j7+uMuz/yQ3KIPNUzO1xAyxJmDX7ZdM= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=qWMgEACz; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=Y4z2pMfb; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="qWMgEACz"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="Y4z2pMfb" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1754901660; 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=RpoGBjZAqSKvw2d7xmGbPfOry9HApa42BH6CDkVJSNk=; b=qWMgEACztBujkFsgCezh3kJYdDcYZqmiGgyUa37CB5T6Ras1xe1amLExddsvkA+dwt4ZkE DucZIm3OhNHft1KxR6/eQaqQf+7uLGDpiEiLlbiyBt3m2jx9wSyxjYKn3DFtt6ao0ObaTM XOfNPl1v6Hp3nurySkd5kPwzzqZytsOFqJnUE9KEZMqYl6g9+7Vm7Xs0m8bBUBZ99BD4/G ROGXa1jD6maTQnPG3ylCi663Ya61U3SfCYDRRc388JhPksFlE7NxkNaqgqlOKEWjzR+9VE cK3QJmcHw/DzDPRgcpASXfNMFyY2zJBXETY8OC8OallKLzClg7aKuQJe4Nt+KA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1754901660; 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=RpoGBjZAqSKvw2d7xmGbPfOry9HApa42BH6CDkVJSNk=; b=Y4z2pMfbMpqI/vL8rBiBR0ZOZSkvSGZ+q3OPUTICCwZuMvFT+tvir77x3AWaNqBAPY9Lcy dqVIYUPVCEwNQmDw== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 2/5] rv/ltl: Support per-cpu monitors Date: Mon, 11 Aug 2025 10:40:50 +0200 Message-Id: <9a1b5a8c449fcb4f1a671016389c1e4fca49a351.1754900299.git.namcao@linutronix.de> In-Reply-To: References: 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 Content-Type: text/plain; charset="utf-8" Add support for per-cpu run-time verification linear temporal logic monitors. This is analogous to deterministic automaton per-cpu monitors. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v3: fixup build issue on sh4 v2: Rename "implicit" to "cpu" --- include/rv/ltl_monitor.h | 32 ++++++++++++++++++++++++++ kernel/trace/rv/Kconfig | 4 ++++ kernel/trace/rv/rv_trace.h | 46 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 82 insertions(+) diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index 9dabc5b133a3..5c0197a59db0 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -23,12 +23,21 @@ =20 typedef struct task_struct *monitor_target; =20 +#elif LTL_MONITOR_TYPE =3D=3D RV_MON_PER_CPU + +#define TARGET_PRINT_FORMAT "%u" +#define TARGET_PRINT_ARGS(cpu) cpu + +typedef unsigned int monitor_target; + #endif =20 #ifdef CONFIG_RV_REACTORS #define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) static struct rv_monitor RV_MONITOR_NAME; =20 +static struct ltl_monitor *ltl_get_monitor(monitor_target target); + static void rv_cond_react(monitor_target target) { if (!rv_reacting_on() || !RV_MONITOR_NAME.react) @@ -54,6 +63,13 @@ static struct ltl_monitor *ltl_get_monitor(monitor_targe= t target) { return &target->rv[ltl_monitor_slot].ltl_mon; } +#elif LTL_MONITOR_TYPE =3D=3D RV_MON_PER_CPU +static DEFINE_PER_CPU(struct ltl_monitor, ltl_monitor); + +static struct ltl_monitor *ltl_get_monitor(unsigned int cpu) +{ + return per_cpu_ptr(<l_monitor, cpu); +} #endif =20 static void ltl_target_init(monitor_target target, bool target_creation) @@ -108,6 +124,22 @@ static void ltl_monitor_destroy(void) rv_put_task_monitor_slot(ltl_monitor_slot); ltl_monitor_slot =3D RV_PER_TASK_MONITOR_INIT; } + +#elif LTL_MONITOR_TYPE =3D=3D RV_MON_PER_CPU + +static int ltl_monitor_init(void) +{ + unsigned int cpu; + + for_each_possible_cpu(cpu) + ltl_target_init(cpu, false); + return 0; +} + +static void ltl_monitor_destroy(void) +{ +} + #endif =20 static void ltl_illegal_state(monitor_target target, struct ltl_monitor *m= on) diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 5b4be87ba59d..7ef89006ed50 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -16,6 +16,10 @@ config DA_MON_EVENTS_ID select RV_MON_MAINTENANCE_EVENTS bool =20 +config LTL_MON_EVENTS_CPU + select RV_MON_EVENTS + bool + config LTL_MON_EVENTS_ID select RV_MON_EVENTS bool diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index 4a6faddac614..bf7cca6579ec 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -177,8 +177,54 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_id, #include #include // Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here + #endif /* CONFIG_LTL_MON_EVENTS_ID */ =20 +#ifdef CONFIG_LTL_MON_EVENTS_CPU +DECLARE_EVENT_CLASS(event_ltl_monitor_cpu, + + TP_PROTO(unsigned int cpu, char *states, char *atoms, char *next), + + TP_ARGS(cpu, states, atoms, next), + + TP_STRUCT__entry( + __field(unsigned int, cpu) + __string(states, states) + __string(atoms, atoms) + __string(next, next) + ), + + TP_fast_assign( + __entry->cpu =3D cpu; + __assign_str(states); + __assign_str(atoms); + __assign_str(next); + ), + + TP_printk("cpu%u: (%s) x (%s) -> (%s)", __entry->cpu, + __get_str(states), __get_str(atoms), __get_str(next)) +); + +DECLARE_EVENT_CLASS(error_ltl_monitor_cpu, + + TP_PROTO(unsigned int cpu), + + TP_ARGS(cpu), + + TP_STRUCT__entry( + __field(unsigned int, cpu) + ), + + TP_fast_assign( + __entry->cpu =3D cpu; + ), + + TP_printk("cpu%u: violation detected", __entry->cpu) +); +// Add new monitors based on CONFIG_LTL_MON_EVENTS_CPU here + +#endif /* CONFIG_LTL_MON_EVENTS_CPU */ + #ifdef CONFIG_RV_MON_MAINTENANCE_EVENTS /* Tracepoint useful for monitors development, currenly only used in DA */ TRACE_EVENT(rv_retries_error, --=20 2.39.5 From nobody Sun Oct 5 01:45:13 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 E8AB02DC327; Mon, 11 Aug 2025 08:41:01 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; cv=none; b=ON26cPHmgkMrU9rOww+f5Yf/3NQacwoqMnQzYUG6NVrqPG5TiMqjau5/HxmHrraWLzG9xzF53JOjU/iXVmo9k6IYMDHYmI4uZrTxODRFeYgHGsB3OGlLYjCI0Y3koz0qgrlccyMdJlZRLl+Jn26RXvbe3s7mTNQdQf8qcYan+w8= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901663; c=relaxed/simple; bh=Pkh60LQE6oQM6hJ6LKjGr8fgjy8bvBfKlnosy6SE+X4=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=YDSnwPFEroSetW7OnMDr7Ab5uKc9OMhm9SWzARxeKvw2lyBNd1GaSbimrIx4Aajxj9V2UvWhV6e5P3vFT25d6Al1uT1c39w+O+Fx5rARrGAoCXFGqKPmK4M7Yciim1YBRktgvriVgWgbxbCuy9aOrKilXVS1OQU2sMXA5xHQDuc= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=2mJ7MpNF; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=InUNx2If; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="2mJ7MpNF"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="InUNx2If" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1754901660; 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=c9JdoIob0IoJYUL+k+Xeng5nvnqhWJYDYOUC/vZBBeQ=; b=2mJ7MpNF3cNzLViG+c6tQyB75EJe9ieMFbmeamzaGsVKHHSFyiG6WV1s9pjx4v9JxHw2lW 7qri/xnt+NcFZ3Je3t+gjyMPC66apFvAOhBJ27UHIuP9w8yR9CeLrsCKbWZ4hFrzT62o3/ x89vHb+3FJEJxAd3yhwwof2ChyvdaBB2VU94h5paRnGyO0YWLJNFMdcT4mPNxwPL9jD3ba 8OXuHldz0T+AqeJeEv2//tmAp3gky4jp3eNlogddmfIgcFL9BMFDjxRtiXgS/1UUGFroq2 Rfh+vcUORd4pHZk55HofbMFHqri+rtTKdRg2K7HLgIG1HfKgqeqrrojKA4kNpA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1754901660; 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=c9JdoIob0IoJYUL+k+Xeng5nvnqhWJYDYOUC/vZBBeQ=; b=InUNx2IfXIg/90xO+3/pDTf0rrzwCY+UL0uwLE9IDXxGdOtuOdrNHRu5tVjT1eEBdqblEM 9+G4dX62jJ+vnXDw== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 3/5] verification/rvgen/ltl: Support per-cpu monitor generation Date: Mon, 11 Aug 2025 10:40:51 +0200 Message-Id: In-Reply-To: References: 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 Content-Type: text/plain; charset="utf-8" Add support to generate per-cpu LTL monitors. Similar to generating per-cpu monitors from .dot files, the "-t per_cpu" parameter can be used to generate per-cpu monitors from .ltl files. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v3: re-write the description in ltl_atoms_init() to be more precise v2: Rename "implicit" to "cpu" --- tools/verification/rvgen/rvgen/ltl2k.py | 48 ++++++++++++++++--- .../rvgen/rvgen/templates/ltl2k/main.c | 9 ++-- .../rvgen/rvgen/templates/ltl2k/trace.h | 7 ++- 3 files changed, 50 insertions(+), 14 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index b075f98d50c4..f291d1f03d05 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -57,9 +57,16 @@ class ltl2k(generator.Monitor): template_dir =3D "ltl2k" =20 def __init__(self, file_path, MonitorType, extra_params=3D{}): - if MonitorType !=3D "per_task": - raise NotImplementedError("Only per_task monitor is supported = for LTL") + if MonitorType =3D=3D "per_task": + self._target_arg =3D "struct task_struct *task" + self._target =3D "task" + elif MonitorType =3D=3D "per_cpu": + self._target_arg =3D "unsigned int cpu" + self._target =3D "cpu" + else: + raise NotImplementedError(f"LTL does not support monitor type = {MonitorType}") super().__init__(extra_params) + self.monitor_type =3D MonitorType with open(file_path) as f: self.atoms, self.ba, self.ltl =3D ltl2ba.create_graph(f.read()) self.atoms_abbr =3D abbreviate_atoms(self.atoms) @@ -67,6 +74,13 @@ class ltl2k(generator.Monitor): if not self.name: self.name =3D Path(file_path).stem =20 + def _fill_monitor_type(self) -> str: + if self.monitor_type =3D=3D "per_task": + return "#define LTL_MONITOR_TYPE RV_MON_PER_TASK" + if self.monitor_type =3D=3D "per_cpu": + return "#define LTL_MONITOR_TYPE RV_MON_PER_CPU" + assert False + def _fill_states(self) -> str: buf =3D [ "enum ltl_buchi_state {", @@ -174,7 +188,7 @@ class ltl2k(generator.Monitor): =20 def _fill_start(self): buf =3D [ - "static void ltl_start(struct task_struct *task, struct ltl_mo= nitor *mon)", + "static void ltl_start(%s, struct ltl_monitor *mon)" % self._t= arget_arg, "{" ] =20 @@ -205,7 +219,7 @@ class ltl2k(generator.Monitor): buff =3D [] buff.append("static void handle_example_event(void *data, /* XXX: = fill header */)") buff.append("{") - buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.= atoms[0]) + buff.append("\tltl_atom_update(%s, LTL_%s, true/false);" % (self._= target, self.atoms[0])) buff.append("}") buff.append("") return '\n'.join(buff) @@ -241,6 +255,9 @@ class ltl2k(generator.Monitor): "" ] =20 + buf.append(self._fill_monitor_type()) + buf.append('') + buf.extend(self._fill_atoms()) buf.append('') =20 @@ -259,13 +276,32 @@ class ltl2k(generator.Monitor): return '\n'.join(buf) =20 def fill_monitor_class_type(self): - return "LTL_MON_EVENTS_ID" + if self.monitor_type =3D=3D "per_task": + return "LTL_MON_EVENTS_ID" + if self.monitor_type =3D=3D "per_cpu": + return "LTL_MON_EVENTS_CPU" + assert False =20 def fill_monitor_class(self): - return "ltl_monitor_id" + if self.monitor_type =3D=3D "per_task": + return "ltl_monitor_id" + if self.monitor_type =3D=3D "per_cpu": + return "ltl_monitor_cpu" + assert False + + def fill_tracepoint_args_skel(self, tp_type): + if tp_type =3D=3D "event": + return \ + ("\tTP_PROTO(%s, char *states, char *atoms, char *next),\n= " % self._target_arg) + \ + ("\tTP_ARGS(%s, states, atoms, next)" % self._target) + if tp_type =3D=3D "error": + return \ + ("\tTP_PROTO(%s),\n" % self._target_arg) + \ + ("\tTP_ARGS(%s)" % self._target) =20 def fill_main_c(self): main_c =3D super().fill_main_c() main_c =3D main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + main_c =3D main_c.replace("%%TARGET_ARG%%", self._target_arg) =20 return main_c diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/= verification/rvgen/rvgen/templates/ltl2k/main.c index f85d076fbf78..c6b51a04c360 100644 --- a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -23,7 +23,7 @@ #include "%%MODEL_NAME%%.h" #include =20 -static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *= mon) +static void ltl_atoms_fetch(%%TARGET_ARG%%, struct ltl_monitor *mon) { /* * This is called everytime the Buchi automaton is triggered. @@ -36,13 +36,14 @@ static void ltl_atoms_fetch(struct task_struct *task, s= truct ltl_monitor *mon) */ } =20 -static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *m= on, bool task_creation) +static void ltl_atoms_init(%%TARGET_ARG%%, struct ltl_monitor *mon, bool t= arget_creation) { /* * This should initialize as many atomic propositions as possible. * - * @task_creation indicates whether the task is being created. This is - * false if the task is already running before the monitor is enabled. + * @target_creation indicates whether the monitored target is being + * created. This is false if the monitor target exists already before + * the monitor is enabled. */ %%ATOMS_INIT%% } diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools= /verification/rvgen/rvgen/templates/ltl2k/trace.h index 49394c4b0f1c..87d3a1308926 100644 --- a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -6,9 +6,8 @@ =20 #ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, - TP_PROTO(struct task_struct *task, char *states, char *atoms, char *= next), - TP_ARGS(task, states, atoms, next)); +%%TRACEPOINT_ARGS_SKEL_EVENT%%); + DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, - TP_PROTO(struct task_struct *task), - TP_ARGS(task)); +%%TRACEPOINT_ARGS_SKEL_ERROR%%); #endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ --=20 2.39.5 From nobody Sun Oct 5 01:45:13 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 D01FF2DC33D; Mon, 11 Aug 2025 08:41:02 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901664; cv=none; b=Hk+t/Z6BwoS91MbJ6c5emoKfZTJp2/w2kVyO/qVCZcQNiGGNYPZslFQO7cGBfXTgx4N5Rca1Cf2qch4yuDT+ZVTgSGOkbrC1dS309ABlIseZ40U2JftzbiYaPBUOYdhb7X6UrBiXhJoMxETPSc/tbJBniBz8yKxe410S4xq5Cls= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901664; c=relaxed/simple; bh=9YsG06WtB9/zUOgaTgppqAwdfXZoFjPNkZ6vFpzOkHs=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=uOu/ACjsM3C7rOPLvqUdg9oSTTEf4SofJAdCkBoq4Lqx5GarWY4vV8asXo+ACzkVPEa5EgPs5ugg1TkvUVlP3cZ6vZeUxqE5l6THYtOXElF1SwplS7NXpfxFz7r+DrTihoilxgUMTWCQO5EzNFxkmO8+9iB5uv9fpW8yozAVitk= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=OukrhY09; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=hnyGRGTk; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="OukrhY09"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="hnyGRGTk" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1754901661; 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=Miprh6lutDZczVUr8OdDe4LY5knk2xmnfHBwc1ZmSzQ=; b=OukrhY09UYSeVdjYlnkQK4tMEcuxsTjqCe4eGSGEm6aZLcFulwJuydpmcaX7n0HjrLoiDp 84JesybPgouSeitUVFqHpd7b/33hEts1Mm5xTrFZsDuHHGx+6VHs0VKZPhTEIeitHNBk9N LbIYBJNS41awBgx7JbLjHaUnfkAq/q+j2sVkegFKbCWmrpXSa43gaJoDukgw/iricv+34i 0FP3W+t/9WxPadng54VdgXTiraFjpUOVBC3UmT3kD+ZDwDmaIFvxAIazw+Vf48l4tDrAG4 oGaVc1FYBFRPhPwQPcis/WE68zLwhNPI0ujOuJOMj9hygFRkKQGuJcUkyVI1nw== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1754901661; 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=Miprh6lutDZczVUr8OdDe4LY5knk2xmnfHBwc1ZmSzQ=; b=hnyGRGTkvGJBfAbmtGNTsmCR6rhkiB0ptn4XyoH+DKZDpWTrK7v5eTM88lhJvW8zhbPl8W QyDaxLZdFiJL2lDA== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao , Ingo Molnar , Peter Zijlstra , Juri Lelli , Vincent Guittot , Dietmar Eggemann , Ben Segall , Mel Gorman , Valentin Schneider , K Prateek Nayak Subject: [PATCH v3 4/5] sched: Add task enqueue/dequeue trace points Date: Mon, 11 Aug 2025 10:40:52 +0200 Message-Id: <918fe0f29a94e49db05c4f63a8a210dda9b90925.1754900299.git.namcao@linutronix.de> In-Reply-To: References: 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 Content-Type: text/plain; charset="utf-8" Add trace points into enqueue_task() and dequeue_task(). They are useful to implement RV monitor which validates RT scheduling. Signed-off-by: Nam Cao --- Cc: Ingo Molnar Cc: Peter Zijlstra Cc: Juri Lelli Cc: Vincent Guittot Cc: Dietmar Eggemann Cc: Ben Segall Cc: Mel Gorman Cc: Valentin Schneider Cc: K Prateek Nayak --- v3: fix up build issue on !SMP v2: Move the tracepoints to cover all task enqueue/dequeue, not just RT --- include/trace/events/sched.h | 13 +++++++++++++ kernel/sched/core.c | 8 +++++++- 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/include/trace/events/sched.h b/include/trace/events/sched.h index 7b2645b50e78..696d22af5a98 100644 --- a/include/trace/events/sched.h +++ b/include/trace/events/sched.h @@ -896,6 +896,19 @@ DECLARE_TRACE(sched_set_need_resched, TP_PROTO(struct task_struct *tsk, int cpu, int tif), TP_ARGS(tsk, cpu, tif)); =20 +/* + * The two trace points below may not work as expected for fair tasks due + * to delayed dequeue. See: + * https://lore.kernel.org/lkml/179674c6-f82a-4718-ace2-67b5e672fdee@amd.c= om/ + */ +DECLARE_TRACE(enqueue_task, + TP_PROTO(int cpu, struct task_struct *task), + TP_ARGS(cpu, task)); + +DECLARE_TRACE(dequeue_task, + TP_PROTO(int cpu, struct task_struct *task), + TP_ARGS(cpu, task)); + #endif /* _TRACE_SCHED_H */ =20 /* This part must be outside protection */ diff --git a/kernel/sched/core.c b/kernel/sched/core.c index be00629f0ba4..6367799aa023 100644 --- a/kernel/sched/core.c +++ b/kernel/sched/core.c @@ -2077,6 +2077,8 @@ unsigned long get_wchan(struct task_struct *p) =20 void enqueue_task(struct rq *rq, struct task_struct *p, int flags) { + trace_enqueue_task_tp(cpu_of(rq), p); + if (!(flags & ENQUEUE_NOCLOCK)) update_rq_clock(rq); =20 @@ -2119,7 +2121,11 @@ inline bool dequeue_task(struct rq *rq, struct task_= struct *p, int flags) * and mark the task ->sched_delayed. */ uclamp_rq_dec(rq, p); - return p->sched_class->dequeue_task(rq, p, flags); + if (p->sched_class->dequeue_task(rq, p, flags)) { + trace_dequeue_task_tp(cpu_of(rq), p); + return true; + } + return false; } =20 void activate_task(struct rq *rq, struct task_struct *p, int flags) --=20 2.39.5 From nobody Sun Oct 5 01:45:13 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 2CFB02DCBFA; Mon, 11 Aug 2025 08:41:03 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901666; cv=none; b=RLv5UcnRaM67Z6eCDtk+KjoO2UweE02lQHnIQjJkGBVe22jcs0SUtj47tcadd2eKw5caY4/insWXdEHEFSgqqqlQ22as/5y5MSvQh1gIiSZocR6aGdD+rPnnRdqhO2c23swuPHXX0GXIvfxMYceunwPdU+e5ZNqxMxmWd53eExI= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1754901666; c=relaxed/simple; bh=nbt/8wyO0vG/AvEor5nPA9ct0xfAm/ABn85Xmu2wJAM=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=dHQouNrUN8kfnzFA2mHJarj88SMFiBV101Xu5EYmW3pynU7h8sqkDZSEgfoYCvD4iTP87vfcjKV5CogwtDGN8KpnBQACmvrxCeR5Eh0Q/YQjexHItULb208cnxgCIv8a77DjxUUEKJWlaDTEZ5sKho5VcLFrv7fcdR6l63KW1Dc= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=I0veobmp; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=tJaeCiwx; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="I0veobmp"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="tJaeCiwx" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1754901661; 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=A2QvfG22MoYtv/ETBw1+NVVwCDmQ4At5ovreIQwBYAM=; b=I0veobmpKyyUYDImXmQ9VfE4DFyWo4lrnpK9MMl45yFpH9bnaV71YcEnwEgHwuYqQs2/6z QudAJNtPbbE5HWHmM3thFfAkPZbICEQb8ucQvvhOsW9npAqYrUt7ZHb6L1QJgeTzXpqTPf eATNudvjNNYztiWJj2Vc7CQ+0fL6gRFNpByWp9EjN9Kfgja7wAX3b5bzLDgnR3JxrUKYq5 vZQyLFcexj+HyXHgTibPImBqgS7MZhN+chAVJSM/QuOrDXJbIY6hOwXM2+M7fwGhk1VPAr 3ed1mw0YOzXNLmCu2hkHMBuzQXI2lelPx+dfAvJg6lL0YKM384s/n/u6+5iZVQ== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1754901661; 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=A2QvfG22MoYtv/ETBw1+NVVwCDmQ4At5ovreIQwBYAM=; b=tJaeCiwx/Tq9Bm6Kzy5qsGHVd6TQzkxpvjuOv1JFKmHMv4pLCGhAG60EE0OWt1WDEifjpZ 8CjfVpsSS9l0tDCQ== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao , Ingo Molnar , Peter Zijlstra , Juri Lelli , Vincent Guittot , Dietmar Eggemann , Ben Segall , Mel Gorman , Valentin Schneider , K Prateek Nayak Subject: [PATCH v3 5/5] rv: Add rts monitor Date: Mon, 11 Aug 2025 10:40:53 +0200 Message-Id: In-Reply-To: References: 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 Content-Type: text/plain; charset="utf-8" Add "real-time scheduling" monitor, which validates that SCHED_RR and SCHED_FIFO tasks are scheduled before tasks with normal and extensible scheduling policies Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- Cc: Ingo Molnar Cc: Peter Zijlstra Cc: Juri Lelli Cc: Vincent Guittot Cc: Dietmar Eggemann Cc: Ben Segall Cc: Mel Gorman Cc: Valentin Schneider Cc: K Prateek Nayak --- v3: - move document file and specification file to be under rtapp v2: - use the new tracepoints - move to be under the rtapp container monitor - re-generate with the modified scripts - fixup incorrect enqueued status --- Documentation/trace/rv/monitor_rtapp.rst | 19 +++ kernel/trace/rv/Kconfig | 1 + kernel/trace/rv/Makefile | 1 + kernel/trace/rv/monitors/rts/Kconfig | 17 +++ kernel/trace/rv/monitors/rts/rts.c | 144 +++++++++++++++++++++++ kernel/trace/rv/monitors/rts/rts.h | 126 ++++++++++++++++++++ kernel/trace/rv/monitors/rts/rts_trace.h | 15 +++ kernel/trace/rv/rv_trace.h | 1 + tools/verification/models/rtapp/rts.ltl | 5 + 9 files changed, 329 insertions(+) create mode 100644 kernel/trace/rv/monitors/rts/Kconfig create mode 100644 kernel/trace/rv/monitors/rts/rts.c create mode 100644 kernel/trace/rv/monitors/rts/rts.h create mode 100644 kernel/trace/rv/monitors/rts/rts_trace.h create mode 100644 tools/verification/models/rtapp/rts.ltl diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace= /rv/monitor_rtapp.rst index c8104eda924a..40001ace5612 100644 --- a/Documentation/trace/rv/monitor_rtapp.rst +++ b/Documentation/trace/rv/monitor_rtapp.rst @@ -131,3 +131,22 @@ special cases: real-time-safe because preemption is disabled for the duration. - `FUTEX_LOCK_PI` is included in the allowlist for the same reason as `BLOCK_ON_RT_MUTEX`. + +Monitor rts ++++++++++++ + +The real-time scheduling monitor validates that tasks with real-time sched= uling +policies (`SCHED_FIFO` and `SCHED_RR`) are always scheduled before tasks w= ith +normal and extensible scheduling policies (`SCHED_OTHER`, `SCHED_BATCH`, +`SCHED_IDLE`, `SCHED_EXT`): + +.. literalinclude:: ../../../tools/verification/models/rtapp/rts.ltl + +Note that this monitor may report errors if real-time throttling or fair +deadline server is enabled. These mechanisms prevent real-time tasks from +monopolying the CPU by giving tasks with normal and extensible scheduling +policies a chance to run. They give system administrators a chance to kill= a +misbehaved real-time task. However, they violate the scheduling priorities= and +may cause latency to well-behaved real-time tasks. Thus, if you see errors= from +this monitor, consider disabling real-time throttling and the fair deadline +server. diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 7ef89006ed50..e9007ed32aea 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -67,6 +67,7 @@ source "kernel/trace/rv/monitors/opid/Kconfig" source "kernel/trace/rv/monitors/rtapp/Kconfig" source "kernel/trace/rv/monitors/pagefault/Kconfig" source "kernel/trace/rv/monitors/sleep/Kconfig" +source "kernel/trace/rv/monitors/rts/Kconfig" # Add new rtapp monitors here =20 # Add new monitors here diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 750e4ad6fa0f..d7bfc7ae6677 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -17,6 +17,7 @@ obj-$(CONFIG_RV_MON_STS) +=3D monitors/sts/sts.o obj-$(CONFIG_RV_MON_NRP) +=3D monitors/nrp/nrp.o obj-$(CONFIG_RV_MON_SSSW) +=3D monitors/sssw/sssw.o obj-$(CONFIG_RV_MON_OPID) +=3D monitors/opid/opid.o +obj-$(CONFIG_RV_MON_RTS) +=3D monitors/rts/rts.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/rts/Kconfig b/kernel/trace/rv/monitor= s/rts/Kconfig new file mode 100644 index 000000000000..5481b371bce1 --- /dev/null +++ b/kernel/trace/rv/monitors/rts/Kconfig @@ -0,0 +1,17 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_RTS + depends on RV + select RV_LTL_MONITOR + depends on RV_MON_RTAPP + default y + select LTL_MON_EVENTS_CPU + bool "rts monitor" + help + Add support for RTS (real-time scheduling) monitor which validates + that real-time-priority tasks are scheduled before SCHED_OTHER tasks. + + This monitor may report an error if RT throttling or deadline server + is enabled. + + Say Y if you are debugging or testing a real-time system. diff --git a/kernel/trace/rv/monitors/rts/rts.c b/kernel/trace/rv/monitors/= rts/rts.c new file mode 100644 index 000000000000..b4c3d3a4671d --- /dev/null +++ b/kernel/trace/rv/monitors/rts/rts.c @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "rts" + +#include +#include +#include + +#include "rts.h" +#include + +static DEFINE_PER_CPU(unsigned int, nr_queued); + +static void ltl_atoms_fetch(unsigned int cpu, struct ltl_monitor *mon) +{ +} + +static void ltl_atoms_init(unsigned int cpu, struct ltl_monitor *mon, + bool target_creation) +{ + ltl_atom_set(mon, LTL_SCHED_SWITCH, false); + ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false); + ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false); + + /* + * This may not be accurate, there may be enqueued RT tasks. But that's + * okay, the worst we get is a false negative. It will be accurate as + * soon as the CPU no longer has any queued RT task. + */ + ltl_atom_set(mon, LTL_RT_TASK_ENQUEUED, false); +} + +static void handle_enqueue_task(void *data, int cpu, struct task_struct *t= ask) +{ + unsigned int *queued =3D per_cpu_ptr(&nr_queued, cpu); + + if (!rt_task(task)) + return; + + (*queued)++; + ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, true); +} + +static void handle_dequeue_task(void *data, int cpu, struct task_struct *t= ask) +{ + unsigned int *queued =3D per_cpu_ptr(&nr_queued, cpu); + + if (!rt_task(task)) + return; + + /* + * This may not be accurate for a short time after the monitor is + * enabled, because there may be enqueued RT tasks which are not counted + * torward nr_queued. But that's okay, the worst we get is a false + * negative. nr_queued will be accurate as soon as the CPU no longer has + * any queued RT task. + */ + if (*queued) + (*queued)--; + if (!*queued) + ltl_atom_update(cpu, LTL_RT_TASK_ENQUEUED, false); +} + +static void handle_sched_switch(void *data, bool preempt, struct task_stru= ct *prev, + struct task_struct *next, unsigned int prev_state) +{ + unsigned int cpu =3D smp_processor_id(); + struct ltl_monitor *mon =3D ltl_get_monitor(cpu); + + ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, rt_task(next)); + ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, dl_task(next)); + ltl_atom_update(cpu, LTL_SCHED_SWITCH, true); + + ltl_atom_set(mon, LTL_SCHED_SWITCH_RT, false); + ltl_atom_set(mon, LTL_SCHED_SWITCH_DL, false); + ltl_atom_update(cpu, LTL_SCHED_SWITCH, false); +} + +static int enable_rts(void) +{ + unsigned int cpu; + int retval; + + retval =3D ltl_monitor_init(); + if (retval) + return retval; + + for_each_possible_cpu(cpu) { + unsigned int *queued =3D per_cpu_ptr(&nr_queued, cpu); + + *queued =3D 0; + } + + rv_attach_trace_probe("rts", dequeue_task_tp, handle_dequeue_task); + rv_attach_trace_probe("rts", enqueue_task_tp, handle_enqueue_task); + rv_attach_trace_probe("rts", sched_switch, handle_sched_switch); + + return 0; +} + +static void disable_rts(void) +{ + rv_detach_trace_probe("rts", sched_switch, handle_sched_switch); + rv_detach_trace_probe("rts", enqueue_task_tp, handle_enqueue_task); + rv_detach_trace_probe("rts", dequeue_task_tp, handle_dequeue_task); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_rts =3D { + .name =3D "rts", + .description =3D "Validate that real-time tasks are scheduled before lowe= r-priority tasks", + .enable =3D enable_rts, + .disable =3D disable_rts, +}; + +static int __init register_rts(void) +{ + return rv_register_monitor(&rv_rts, &rv_rtapp); +} + +static void __exit unregister_rts(void) +{ + rv_unregister_monitor(&rv_rts); +} + +module_init(register_rts); +module_exit(unregister_rts); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Nam Cao "); +MODULE_DESCRIPTION("rts: Validate that real-time tasks are scheduled befor= e lower-priority tasks"); diff --git a/kernel/trace/rv/monitors/rts/rts.h b/kernel/trace/rv/monitors/= rts/rts.h new file mode 100644 index 000000000000..5881f30a38ce --- /dev/null +++ b/kernel/trace/rv/monitors/rts/rts.h @@ -0,0 +1,126 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * C implementation of Buchi automaton, automatically generated by + * tools/verification/rvgen from the linear temporal logic specification. + * For further information, see kernel documentation: + * Documentation/trace/rv/linear_temporal_logic.rst + */ + +#include + +#define MONITOR_NAME rts + +#define LTL_MONITOR_TYPE RV_MON_PER_CPU + +enum ltl_atom { + LTL_RT_TASK_ENQUEUED, + LTL_SCHED_SWITCH, + LTL_SCHED_SWITCH_DL, + LTL_SCHED_SWITCH_RT, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <=3D RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] =3D { + "rt_ta_en", + "sc_sw", + "sc_sw_dl", + "sc_sw_rt", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <=3D RV_MAX_BA_STATES); + +static void ltl_start(unsigned int cpu, struct ltl_monitor *mon) +{ + bool sched_switch_rt =3D test_bit(LTL_SCHED_SWITCH_RT, mon->atoms); + bool sched_switch_dl =3D test_bit(LTL_SCHED_SWITCH_DL, mon->atoms); + bool sched_switch =3D test_bit(LTL_SCHED_SWITCH, mon->atoms); + bool rt_task_enqueued =3D test_bit(LTL_RT_TASK_ENQUEUED, mon->atoms); + bool val13 =3D !rt_task_enqueued; + bool val8 =3D sched_switch_dl || val13; + bool val9 =3D sched_switch_rt || val8; + bool val6 =3D !sched_switch; + bool val1 =3D !rt_task_enqueued; + + if (val1) + __set_bit(S0, mon->states); + if (val6) + __set_bit(S1, mon->states); + if (val9) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsi= gned long *next) +{ + bool sched_switch_rt =3D test_bit(LTL_SCHED_SWITCH_RT, mon->atoms); + bool sched_switch_dl =3D test_bit(LTL_SCHED_SWITCH_DL, mon->atoms); + bool sched_switch =3D test_bit(LTL_SCHED_SWITCH, mon->atoms); + bool rt_task_enqueued =3D test_bit(LTL_RT_TASK_ENQUEUED, mon->atoms); + bool val13 =3D !rt_task_enqueued; + bool val8 =3D sched_switch_dl || val13; + bool val9 =3D sched_switch_rt || val8; + bool val6 =3D !sched_switch; + bool val1 =3D !rt_task_enqueued; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (val6) + __set_bit(S1, next); + if (val9) + __set_bit(S4, next); + break; + case S1: + if (val6) + __set_bit(S1, next); + if (val1 && val6) + __set_bit(S2, next); + if (val1 && val9) + __set_bit(S3, next); + if (val9) + __set_bit(S4, next); + break; + case S2: + if (val6) + __set_bit(S1, next); + if (val1 && val6) + __set_bit(S2, next); + if (val1 && val9) + __set_bit(S3, next); + if (val9) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (val6) + __set_bit(S1, next); + if (val9) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (val6) + __set_bit(S1, next); + if (val9) + __set_bit(S4, next); + break; + } +} diff --git a/kernel/trace/rv/monitors/rts/rts_trace.h b/kernel/trace/rv/mon= itors/rts/rts_trace.h new file mode 100644 index 000000000000..ac4ea84162f7 --- /dev/null +++ b/kernel/trace/rv/monitors/rts/rts_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_RTS +DEFINE_EVENT(event_ltl_monitor_cpu, event_rts, + TP_PROTO(unsigned int cpu, char *states, char *atoms, char *next), + TP_ARGS(cpu, states, atoms, next)); + +DEFINE_EVENT(error_ltl_monitor_cpu, error_rts, + TP_PROTO(unsigned int cpu), + TP_ARGS(cpu)); +#endif /* CONFIG_RV_MON_RTS */ diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index bf7cca6579ec..7b3a6fb8ca6f 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -221,6 +221,7 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_cpu, =20 TP_printk("cpu%u: violation detected", __entry->cpu) ); +#include // Add new monitors based on CONFIG_LTL_MON_EVENTS_CPU here =20 #endif /* CONFIG_LTL_MON_EVENTS_CPU */ diff --git a/tools/verification/models/rtapp/rts.ltl b/tools/verification/m= odels/rtapp/rts.ltl new file mode 100644 index 000000000000..90872bca46b1 --- /dev/null +++ b/tools/verification/models/rtapp/rts.ltl @@ -0,0 +1,5 @@ +RULE =3D always (RT_TASK_ENQUEUED imply SCHEDULE_RT_NEXT) + +SCHEDULE_RT_NEXT =3D (not SCHED_SWITCH) until (SCHED_SWITCH_RT or EXCEPTIO= NS) + +EXCEPTIONS =3D SCHED_SWITCH_DL or not RT_TASK_ENQUEUED --=20 2.39.5