aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLinus Torvalds <torvalds@linux-foundation.org>2025-07-30 16:23:12 -0700
committerLinus Torvalds <torvalds@linux-foundation.org>2025-07-30 16:23:12 -0700
commit4ff261e725d7376c12e745fdbe8a33cd6dbd5a83 (patch)
tree20ea818ed1425630b9fc7c0de0adac7497fb9de5
parentd50b07d05ca53fdb6c6d1581b9084c09d4e98f54 (diff)
parent614384533dfe99293a7ff1bce3d4389adadbb759 (diff)
Merge tag 'trace-rv-6.17' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace
Pull runtime verification updates from Steven Rostedt: - Added Linear temporal logic monitors for RT application Real-time applications may have design flaws causing them to have unexpected latency. For example, the applications may raise page faults, or may be blocked trying to take a mutex without priority inheritance. However, while attempting to implement DA monitors for these real-time rules, deterministic automaton is found to be inappropriate as the specification language. The automaton is complicated, hard to understand, and error-prone. For these cases, linear temporal logic is found to be more suitable. The LTL is more concise and intuitive. - Make printk_deferred() public The new monitors needed access to printk_deferred(). Make them visible for the entire kernel. - Add a vpanic() to allow for va_list to be passed to panic. - Add rtapp container monitor. A collection of monitors that check for common problems with real-time applications that cause unexpected latency. - Add page fault tracepoints to risc-v These tracepoints are necessary to for the RV monitor to run on risc-v. - Fix the behaviour of the rv tool with -s and idle tasks. - Allow the rv tool to gracefully terminate with SIGTERM - Adjusts dot2c not to create lines over 100 columns - Properly order nested monitors in the RV Kconfig file - Return the registration error in all DA monitor instead of 0 - Update and add new sched collection monitors Replace tss and sncid monitors with more complete sts: Not only prove that switches occur in scheduling context and scheduling needs interrupt disabled but also that each call to the scheduler disables interrupts to (optionally) switch. New monitor: nrp Preemption requires need resched which is cleared by any switch (includes a non optimal workaround for /nested/ preemptions) New monitor: sssw suspension requires setting the task to sleepable and, after the switch occurs, the task requires a wakeup to come back to runnable New monitor: opid waking and need-resched operations occur with interrupts and preemption disabled or in IRQ without explicitly disabling preemption" * tag 'trace-rv-6.17' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: (48 commits) rv: Add opid per-cpu monitor rv: Add nrp and sssw per-task monitors rv: Replace tss and sncid monitors with more complete sts sched: Adapt sched tracepoints for RV task model rv: Retry when da monitor detects race conditions rv: Adjust monitor dependencies rv: Use strings in da monitors tracepoints rv: Remove trailing whitespace from tracepoint string rv: Add da_handle_start_run_event_ to per-task monitors rv: Fix wrong type cast in reactors_show() and monitor_reactor_show() rv: Fix wrong type cast in monitors_show() rv: Remove struct rv_monitor::reacting rv: Remove rv_reactor's reference counter rv: Merge struct rv_reactor_def into struct rv_reactor rv: Merge struct rv_monitor_def into struct rv_monitor rv: Remove unused field in struct rv_monitor_def rv: Return init error when registering monitors verification/rvgen: Organise Kconfig entries for nested monitors tools/dot2c: Fix generated files going over 100 column limit tools/rv: Stop gracefully also on SIGTERM ...
-rw-r--r--Documentation/trace/rv/da_monitor_synthesis.rst147
-rw-r--r--Documentation/trace/rv/index.rst4
-rw-r--r--Documentation/trace/rv/linear_temporal_logic.rst134
-rw-r--r--Documentation/trace/rv/monitor_rtapp.rst133
-rw-r--r--Documentation/trace/rv/monitor_sched.rst307
-rw-r--r--Documentation/trace/rv/monitor_synthesis.rst271
-rw-r--r--arch/riscv/mm/fault.c8
-rw-r--r--include/linux/panic.h3
-rw-r--r--include/linux/printk.h7
-rw-r--r--include/linux/rv.h86
-rw-r--r--include/linux/sched.h15
-rw-r--r--include/rv/da_monitor.h172
-rw-r--r--include/rv/ltl_monitor.h186
-rw-r--r--include/trace/events/sched.h12
-rw-r--r--kernel/fork.c5
-rw-r--r--kernel/panic.c18
-rw-r--r--kernel/printk/internal.h1
-rw-r--r--kernel/sched/core.c13
-rw-r--r--kernel/trace/rv/Kconfig43
-rw-r--r--kernel/trace/rv/Makefile9
-rw-r--r--kernel/trace/rv/monitors/nrp/Kconfig (renamed from kernel/trace/rv/monitors/tss/Kconfig)12
-rw-r--r--kernel/trace/rv/monitors/nrp/nrp.c138
-rw-r--r--kernel/trace/rv/monitors/nrp/nrp.h75
-rw-r--r--kernel/trace/rv/monitors/nrp/nrp_trace.h15
-rw-r--r--kernel/trace/rv/monitors/opid/Kconfig19
-rw-r--r--kernel/trace/rv/monitors/opid/opid.c168
-rw-r--r--kernel/trace/rv/monitors/opid/opid.h104
-rw-r--r--kernel/trace/rv/monitors/opid/opid_trace.h (renamed from kernel/trace/rv/monitors/sncid/sncid_trace.h)8
-rw-r--r--kernel/trace/rv/monitors/pagefault/Kconfig20
-rw-r--r--kernel/trace/rv/monitors/pagefault/pagefault.c88
-rw-r--r--kernel/trace/rv/monitors/pagefault/pagefault.h64
-rw-r--r--kernel/trace/rv/monitors/pagefault/pagefault_trace.h14
-rw-r--r--kernel/trace/rv/monitors/rtapp/Kconfig11
-rw-r--r--kernel/trace/rv/monitors/rtapp/rtapp.c33
-rw-r--r--kernel/trace/rv/monitors/rtapp/rtapp.h3
-rw-r--r--kernel/trace/rv/monitors/sched/Kconfig1
-rw-r--r--kernel/trace/rv/monitors/sched/sched.c3
-rw-r--r--kernel/trace/rv/monitors/sco/sco.c7
-rw-r--r--kernel/trace/rv/monitors/scpd/Kconfig2
-rw-r--r--kernel/trace/rv/monitors/scpd/scpd.c7
-rw-r--r--kernel/trace/rv/monitors/sleep/Kconfig22
-rw-r--r--kernel/trace/rv/monitors/sleep/sleep.c237
-rw-r--r--kernel/trace/rv/monitors/sleep/sleep.h257
-rw-r--r--kernel/trace/rv/monitors/sleep/sleep_trace.h14
-rw-r--r--kernel/trace/rv/monitors/sncid/sncid.c96
-rw-r--r--kernel/trace/rv/monitors/sncid/sncid.h49
-rw-r--r--kernel/trace/rv/monitors/snep/Kconfig2
-rw-r--r--kernel/trace/rv/monitors/snep/snep.c7
-rw-r--r--kernel/trace/rv/monitors/snep/snep.h14
-rw-r--r--kernel/trace/rv/monitors/snroc/snroc.c3
-rw-r--r--kernel/trace/rv/monitors/sssw/Kconfig (renamed from kernel/trace/rv/monitors/sncid/Kconfig)10
-rw-r--r--kernel/trace/rv/monitors/sssw/sssw.c116
-rw-r--r--kernel/trace/rv/monitors/sssw/sssw.h105
-rw-r--r--kernel/trace/rv/monitors/sssw/sssw_trace.h15
-rw-r--r--kernel/trace/rv/monitors/sts/Kconfig19
-rw-r--r--kernel/trace/rv/monitors/sts/sts.c156
-rw-r--r--kernel/trace/rv/monitors/sts/sts.h117
-rw-r--r--kernel/trace/rv/monitors/sts/sts_trace.h (renamed from kernel/trace/rv/monitors/tss/tss_trace.h)8
-rw-r--r--kernel/trace/rv/monitors/tss/tss.c91
-rw-r--r--kernel/trace/rv/monitors/tss/tss.h47
-rw-r--r--kernel/trace/rv/monitors/wip/Kconfig2
-rw-r--r--kernel/trace/rv/monitors/wip/wip.c3
-rw-r--r--kernel/trace/rv/monitors/wwnr/wwnr.c3
-rw-r--r--kernel/trace/rv/reactor_panic.c8
-rw-r--r--kernel/trace/rv/reactor_printk.c8
-rw-r--r--kernel/trace/rv/rv.c220
-rw-r--r--kernel/trace/rv/rv.h39
-rw-r--r--kernel/trace/rv/rv_reactors.c138
-rw-r--r--kernel/trace/rv/rv_trace.h166
-rw-r--r--tools/objtool/noreturns.h1
-rw-r--r--tools/verification/dot2/Makefile26
-rw-r--r--tools/verification/dot2/dot2k53
-rw-r--r--tools/verification/models/rtapp/pagefault.ltl1
-rw-r--r--tools/verification/models/rtapp/sleep.ltl22
-rw-r--r--tools/verification/models/sched/nrp.dot29
-rw-r--r--tools/verification/models/sched/opid.dot35
-rw-r--r--tools/verification/models/sched/sncid.dot18
-rw-r--r--tools/verification/models/sched/sssw.dot30
-rw-r--r--tools/verification/models/sched/sts.dot38
-rw-r--r--tools/verification/models/sched/tss.dot18
-rw-r--r--tools/verification/rv/src/in_kernel.c4
-rw-r--r--tools/verification/rv/src/rv.c1
-rw-r--r--tools/verification/rvgen/.gitignore3
-rw-r--r--tools/verification/rvgen/Makefile27
-rw-r--r--tools/verification/rvgen/__main__.py67
-rw-r--r--tools/verification/rvgen/dot2c (renamed from tools/verification/dot2/dot2c)2
-rw-r--r--tools/verification/rvgen/rvgen/automata.py (renamed from tools/verification/dot2/automata.py)0
-rw-r--r--tools/verification/rvgen/rvgen/container.py32
-rw-r--r--tools/verification/rvgen/rvgen/dot2c.py (renamed from tools/verification/dot2/dot2c.py)22
-rw-r--r--tools/verification/rvgen/rvgen/dot2k.py129
-rw-r--r--tools/verification/rvgen/rvgen/generator.py (renamed from tools/verification/dot2/dot2k.py)265
-rw-r--r--tools/verification/rvgen/rvgen/ltl2ba.py566
-rw-r--r--tools/verification/rvgen/rvgen/ltl2k.py271
-rw-r--r--tools/verification/rvgen/rvgen/templates/Kconfig (renamed from tools/verification/dot2/dot2k_templates/Kconfig)0
-rw-r--r--tools/verification/rvgen/rvgen/templates/container/Kconfig5
-rw-r--r--tools/verification/rvgen/rvgen/templates/container/main.c (renamed from tools/verification/dot2/dot2k_templates/main_container.c)3
-rw-r--r--tools/verification/rvgen/rvgen/templates/container/main.h (renamed from tools/verification/dot2/dot2k_templates/main_container.h)0
-rw-r--r--tools/verification/rvgen/rvgen/templates/dot2k/main.c (renamed from tools/verification/dot2/dot2k_templates/main.c)3
-rw-r--r--tools/verification/rvgen/rvgen/templates/dot2k/trace.h (renamed from tools/verification/dot2/dot2k_templates/trace.h)0
-rw-r--r--tools/verification/rvgen/rvgen/templates/ltl2k/main.c102
-rw-r--r--tools/verification/rvgen/rvgen/templates/ltl2k/trace.h14
101 files changed, 4860 insertions, 1265 deletions
diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/da_monitor_synthesis.rst
deleted file mode 100644
index 0a92729c8a9b..000000000000
--- a/Documentation/trace/rv/da_monitor_synthesis.rst
+++ /dev/null
@@ -1,147 +0,0 @@
-Deterministic Automata Monitor Synthesis
-========================================
-
-The starting point for the application of runtime verification (RV) techniques
-is the *specification* or *modeling* of the desired (or undesired) behavior
-of the system under scrutiny.
-
-The formal representation needs to be then *synthesized* into a *monitor*
-that can then be used in the analysis of the trace of the system. The
-*monitor* connects to the system via an *instrumentation* that converts
-the events from the *system* to the events of the *specification*.
-
-
-In Linux terms, the runtime verification monitors are encapsulated inside
-the *RV monitor* abstraction. The RV monitor includes a set of instances
-of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
-functions that glue the monitor to the system reference model, and the
-trace output as a reaction to event parsing and exceptions, as depicted
-below::
-
- Linux +----- RV Monitor ----------------------------------+ Formal
- Realm | | Realm
- +-------------------+ +----------------+ +-----------------+
- | Linux kernel | | Monitor | | Reference |
- | Tracing | -> | Instance(s) | <- | Model |
- | (instrumentation) | | (verification) | | (specification) |
- +-------------------+ +----------------+ +-----------------+
- | | |
- | V |
- | +----------+ |
- | | Reaction | |
- | +--+--+--+-+ |
- | | | | |
- | | | +-> trace output ? |
- +------------------------|--|----------------------+
- | +----> panic ?
- +-------> <user-specified>
-
-DA monitor synthesis
---------------------
-
-The synthesis of automata-based models into the Linux *RV monitor* abstraction
-is automated by the dot2k tool and the rv/da_monitor.h header file that
-contains a set of macros that automatically generate the monitor's code.
-
-dot2k
------
-
-The dot2k utility leverages dot2c by converting an automaton model in
-the DOT format into the C representation [1] and creating the skeleton of
-a kernel monitor in C.
-
-For example, it is possible to transform the wip.dot model present in
-[1] into a per-cpu monitor with the following command::
-
- $ dot2k -d wip.dot -t per_cpu
-
-This will create a directory named wip/ with the following files:
-
-- wip.h: the wip model in C
-- wip.c: the RV monitor
-
-The wip.c file contains the monitor declaration and the starting point for
-the system instrumentation.
-
-Monitor macros
---------------
-
-The rv/da_monitor.h enables automatic code generation for the *Monitor
-Instance(s)* using C macros.
-
-The benefits of the usage of macro for monitor synthesis are 3-fold as it:
-
-- Reduces the code duplication;
-- Facilitates the bug fix/improvement;
-- Avoids the case of developers changing the core of the monitor code
- to manipulate the model in a (let's say) non-standard way.
-
-This initial implementation presents three different types of monitor instances:
-
-- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
-- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
-- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
-
-The first declares the functions for a global deterministic automata monitor,
-the second for monitors with per-cpu instances, and the third with per-task
-instances.
-
-In all cases, the 'name' argument is a string that identifies the monitor, and
-the 'type' argument is the data type used by dot2k on the representation of
-the model in C.
-
-For example, the wip model with two states and three events can be
-stored in an 'unsigned char' type. Considering that the preemption control
-is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
-
- DECLARE_DA_MON_PER_CPU(wip, unsigned char);
-
-The monitor is executed by sending events to be processed via the functions
-presented below::
-
- da_handle_event_$(MONITOR_NAME)($(event from event enum));
- da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
- da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
-
-The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
-the event will be processed if the monitor is processing events.
-
-When a monitor is enabled, it is placed in the initial state of the automata.
-However, the monitor does not know if the system is in the *initial state*.
-
-The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
-monitor that the system is returning to the initial state, so the monitor can
-start monitoring the next event.
-
-The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
-the monitor that the system is known to be in the initial state, so the
-monitor can start monitoring and monitor the current event.
-
-Using the wip model as example, the events "preempt_disable" and
-"sched_waking" should be sent to monitor, respectively, via [2]::
-
- da_handle_event_wip(preempt_disable_wip);
- da_handle_event_wip(sched_waking_wip);
-
-While the event "preempt_enabled" will use::
-
- da_handle_start_event_wip(preempt_enable_wip);
-
-To notify the monitor that the system will be returning to the initial state,
-so the system and the monitor should be in sync.
-
-Final remarks
--------------
-
-With the monitor synthesis in place using the rv/da_monitor.h and
-dot2k, the developer's work should be limited to the instrumentation
-of the system, increasing the confidence in the overall approach.
-
-[1] For details about deterministic automata format and the translation
-from one representation to another, see::
-
- Documentation/trace/rv/deterministic_automata.rst
-
-[2] dot2k appends the monitor's name suffix to the events enums to
-avoid conflicting variables when exporting the global vmlinux.h
-use by BPF programs.
diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst
index e80e0057feb4..a2812ac5cfeb 100644
--- a/Documentation/trace/rv/index.rst
+++ b/Documentation/trace/rv/index.rst
@@ -8,8 +8,10 @@ Runtime Verific