Over the last years, I've been exploring the possibility of
verifying the Linux kernel behavior using Runtime Verification.
Runtime Verification (RV) is a lightweight (yet rigorous) method that
complements classical exhaustive verification techniques (such as model
checking and theorem proving) with a more practical approach for complex
systems.
Instead of relying on a fine-grained model of a system (e.g., a
re-implementation a instruction level), RV works by analyzing the trace of the
system's actual execution, comparing it against a formal specification of
the system behavior.
The usage of deterministic automaton for RV is a well-established
approach. In the specific case of the Linux kernel, you can check how
to model complex behavior of the Linux kernel with this paper:
DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo Silva.
*Efficient formal verification for the Linux kernel.* In: International
Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
p. 315-332.
And how efficient is this approach here:
DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread
synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
Architecture, 2020, 107: 101729.
tlrd: it is possible to model complex behaviors in a modular way, with
an acceptable overhead (even for production systems). See this
presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg
Here I am proposing a more practical approach for the usage of deterministic
automata for runtime verification, and it includes:
- An interface for controlling the verification;
- A tool and set of headers that enables the automatic code
generation of the RV monitor (Monitor Synthesis);
- Sample monitors to evaluate the interface;
- A sample monitor developed in the context of the Elisa Project
demonstrating how to use RV in the context of safety-critical
systems.
Given that RV is a tracing consumer, the code is being placed inside the
tracing subsystem (Steven and I have been talking about it for a while).
The changes since V1 includes:
- rebased to the latest kernel;
- code cleanup;
- the watchdog dev monitor;
- safety app;
The TODO list still includes:
- Make per-task monitor use the task struct to store the
per monitor state (Suggested by peterz)
- Add a reactor tha enables the visualization of the visited
states via KCOV (Marco Elver & Dmitry Vyukov)
- Add a CRC method to check from user-space if the values
exported by the monitor were not corrupted by any other
kernel task (Gabriele Paoloni)
I am sending the V2 with some TODOs because I need
some feedback on the interface/files placement inside the kernel,
so I can adjust all the patches accordingly. Also, to make it possible
for people in the Elisa Project to evaluate the safety_app approach.
Daniel Bristot de Oliveira (21):
rv: Add Runtime Verification (RV) interface
rv: Add runtime reactors interface
rv/include: Add helper functions for deterministic automata
rv/include: Add deterministic automata monitor definition via C macros
rv/include: Add tracing helper functions
tools/rv: Add dot2c
tools/rv: Add dot2k
rv/monitor: Add the wip monitor skeleton created by dot2k
rv/monitor: wip instrumentation and Makefile/Kconfig entries
rv/monitor: Add the wwnr monitor skeleton created by dot2k
rv/monitor: wwnr instrumentation and Makefile/Kconfig entries
rv/reactor: Add the printk reactor
rv/reactor: Add the panic reactor
Documentation/rv: Add a basic documentation
Documentation/rv: Add deterministic automata monitor synthesis
documentation
Documentation/rv: Add deterministic automata instrumentation
documentation
watchdog/dev: Add tracepoints
rv/monitor: Add safe watchdog monitor
rv/monitor: Add safe watchdog nowayout monitor
rv/safety_app: Add an safety_app sample
Documentation/rv: Add watchdog-monitor documentation
Documentation/trace/index.rst | 1 +
.../trace/rv/da_monitor_instrumentation.rst | 230 ++++++
.../trace/rv/da_monitor_synthesis.rst | 286 +++++++
Documentation/trace/rv/index.rst | 9 +
.../trace/rv/runtime-verification.rst | 233 ++++++
Documentation/trace/rv/watchdog-monitor.rst | 307 ++++++++
drivers/watchdog/watchdog_dev.c | 41 +-
include/linux/rv.h | 31 +
include/linux/watchdog.h | 7 +-
include/rv/automata.h | 52 ++
include/rv/da_monitor.h | 398 ++++++++++
include/rv/trace_helpers.h | 69 ++
include/trace/events/watchdog.h | 103 +++
kernel/trace/Kconfig | 2 +
kernel/trace/Makefile | 2 +
kernel/trace/rv/Kconfig | 78 ++
kernel/trace/rv/Makefile | 10 +
kernel/trace/rv/monitor_safe_wtd/model.h | 84 +++
kernel/trace/rv/monitor_safe_wtd/safe_wtd.c | 322 ++++++++
kernel/trace/rv/monitor_safe_wtd/safe_wtd.h | 64 ++
kernel/trace/rv/monitor_safe_wtd_nwo/model.h | 61 ++
.../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c | 309 ++++++++
.../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h | 64 ++
kernel/trace/rv/monitor_wip/model.h | 38 +
kernel/trace/rv/monitor_wip/wip.c | 124 +++
kernel/trace/rv/monitor_wip/wip.h | 64 ++
kernel/trace/rv/monitor_wwnr/model.h | 38 +
kernel/trace/rv/monitor_wwnr/wwnr.c | 122 +++
kernel/trace/rv/monitor_wwnr/wwnr.h | 70 ++
kernel/trace/rv/reactor_panic.c | 44 ++
kernel/trace/rv/reactor_printk.c | 43 ++
kernel/trace/rv/rv.c | 700 +++++++++++++++++
kernel/trace/rv/rv.h | 50 ++
kernel/trace/rv/rv_reactors.c | 478 ++++++++++++
kernel/trace/trace.c | 4 +
kernel/trace/trace.h | 2 +
tools/tracing/rv/dot2/Makefile | 26 +
tools/tracing/rv/dot2/automata.py | 179 +++++
tools/tracing/rv/dot2/dot2c | 30 +
tools/tracing/rv/dot2/dot2c.py | 240 ++++++
tools/tracing/rv/dot2/dot2k | 46 ++
tools/tracing/rv/dot2/dot2k.py | 184 +++++
.../rv/dot2/dot2k_templates/main_global.c | 96 +++
.../rv/dot2/dot2k_templates/main_global.h | 64 ++
.../rv/dot2/dot2k_templates/main_per_cpu.c | 96 +++
.../rv/dot2/dot2k_templates/main_per_cpu.h | 64 ++
.../rv/dot2/dot2k_templates/main_per_task.c | 96 +++
.../rv/dot2/dot2k_templates/main_per_task.h | 70 ++
tools/tracing/rv/safety_app/Makefile | 51 ++
tools/tracing/rv/safety_app/safety_app.c | 713 ++++++++++++++++++
50 files changed, 6486 insertions(+), 9 deletions(-)
create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
create mode 100644 Documentation/trace/rv/index.rst
create mode 100644 Documentation/trace/rv/runtime-verification.rst
create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
create mode 100644 include/linux/rv.h
create mode 100644 include/rv/automata.h
create mode 100644 include/rv/da_monitor.h
create mode 100644 include/rv/trace_helpers.h
create mode 100644 include/trace/events/watchdog.h
create mode 100644 kernel/trace/rv/Kconfig
create mode 100644 kernel/trace/rv/Makefile
create mode 100644 kernel/trace/rv/monitor_safe_wtd/model.h
create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.c
create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.h
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/model.h
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h
create mode 100644 kernel/trace/rv/monitor_wip/model.h
create mode 100644 kernel/trace/rv/monitor_wip/wip.c
create mode 100644 kernel/trace/rv/monitor_wip/wip.h
create mode 100644 kernel/trace/rv/monitor_wwnr/model.h
create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.c
create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.h
create mode 100644 kernel/trace/rv/reactor_panic.c
create mode 100644 kernel/trace/rv/reactor_printk.c
create mode 100644 kernel/trace/rv/rv.c
create mode 100644 kernel/trace/rv/rv.h
create mode 100644 kernel/trace/rv/rv_reactors.c
create mode 100644 tools/tracing/rv/dot2/Makefile
create mode 100644 tools/tracing/rv/dot2/automata.py
create mode 100644 tools/tracing/rv/dot2/dot2c
create mode 100644 tools/tracing/rv/dot2/dot2c.py
create mode 100644 tools/tracing/rv/dot2/dot2k
create mode 100644 tools/tracing/rv/dot2/dot2k.py
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h
create mode 100644 tools/tracing/rv/safety_app/Makefile
create mode 100644 tools/tracing/rv/safety_app/safety_app.c
--
2.33.1
Adds documentation about the safe_wtd and safe_wtd_nwo RV monitors,
and their usage via a safety application.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
Documentation/trace/rv/watchdog-monitor.rst | 307 ++++++++++++++++++++
1 file changed, 307 insertions(+)
create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
diff --git a/Documentation/trace/rv/watchdog-monitor.rst b/Documentation/trace/rv/watchdog-monitor.rst
new file mode 100644
index 000000000000..98d5bdd0ed85
--- /dev/null
+++ b/Documentation/trace/rv/watchdog-monitor.rst
@@ -0,0 +1,307 @@
+Watchdog monitor
+----------------
+
+The watchdog is an essential building block for the usage of Linux in
+safety-critical systems because it allows the system to be monitored from
+an external element - the watchdog hardware, acting as a safety-monitor.
+
+A user-space application controls the watchdog device via the watchdog
+interface. This application, hereafter safety_app, enables the watchdog
+and periodically pets the watchdog upon correct completion of the safety
+related processing.
+
+If the safety_app, for any reason, stops pinging the watchdog,
+the watchdog hardware can set the system in a fail-safe state. For
+example, shutting the system down.
+
+Given the importance of the safety_app / watchdog hardware couple,
+the interaction between these software pieces also needs some
+sort of monitoring. In other words, "who monitors the monitor?"
+
+The safe watchdog (safe_wtd) RV monitor monitors the interaction between
+the safety_app and the watchdog device, enforcing the correct sequence of
+events that leads the system to a safe state.
+
+Furthermore, the safety_app can monitor the RV monitor by collecting the
+events generated by the RV monitor itself via tracing interface. In this way,
+closing the monitoring loop with the safety_app.
+
+A diagram of the components and their interactions is::
+
+ user-space:
+ +--------------------------------+
+ | safety_app |-----------+
+ +--------------------------------+ |
+ | ^ |
+ | Configure | Enable and |
+ | | check data |
+ ===================+====================+=============== |
+ kernel-space: | | |
+ v v |
+ +----------+ instr. +-------------+ |
+ | watchdog | ----------->| RV Monitor |----+ |
+ | device | +-------------+ | |
+ +----------+ | |
+ | | |
+ | | |
+ ================+====================================== | |
+ hardware: | | |
+ v | +-> Bring the system
+ +--------------------+ +----> to a safe state,
+ | watchdog hardware |---------------------------> e.g., halt.
+ +--------------------+
+
+Sample safety_app
+-----------------
+
+The user-space safety_app sample code in ``tools/tracing/rv/safety_app/``
+serves to illustrate the usage of the RV monitors for this use-case, as
+well as the starting point to the development of a user-specific safety_app.
+
+Watchdog events
+---------------
+
+The RV monitor observes the watchdog by using instrumentation to
+process the events generated by the interaction between the
+safety_app and the watchdog device layer in kernel.
+
+The monitored events are:
+
+ - watchdog:watchdog_open: open the watchdog device;
+ - watchdog:watchdog_close: close the watchdog device;
+ - watchdog:watchdog_start: start the watchdog;
+ - watchdog:watchdog_stop: stop the watchdog;
+ - watchdog:watchdog_set_timeout: set the watchdog timeout;
+ - watchdog:watchdog_ping: reprogram the watchdog with the previously set
+ timeout;
+ - watchdog:watchdog_nowayout: prevents the watchdog from stopping;
+ - watchdog:watchdog_set_keep_alive: set an intermediary ping to overcome
+ the limitation of a hardware watchdog maximum timeout being shorter than
+ the timeout set by the user-space tool;
+ - watchdog:watchdog_keep_alive: the execution of the function that runs the
+ intermediary keep alive ping;
+
+RV monitor events
+-----------------
+
+The RV monitor monitors the relevant events as an outside observer,
+interpreting all the components (the hardware; the watchdog device
+interface; and the safety monitor) as an integrated component.
+
+The events selected for the monitor are:
+
+ - other_threads: an event generated by any thread other than the
+ one that set nowayout or open the watchdog the last time.
+ - open: a thread opens the watchdog to manipulate it;
+ - close: a thread closes the watchdog;
+ - start: starts the watchdog countdown;
+ - stop: stops the watchdog;
+ - set_safe_timeout: configures the watchdog with a given timeout;
+ - ping: resets the watchdog countdown with the previously configured timeout;
+ - nowayout: prevents the watchdog to be stopped until the system's shutdown;
+ - sched_keep_alive: schedules a kernel worker to ping the watchdog if the
+ timeout is longer than the watchdog hardware can handle.
+ - keep_alive: executes the previously scheduled watchdog ping;
+
+Noting that the events that does not appear in the automata models are
+considered blocked events, and their execution will always cause the
+RV monitor to react to an unexpected event.
+
+RV monitor specification
+------------------------
+
+The monitor's goal is to assess a set of specifications that conducts the
+system to a safe state.
+
+These specifications are:
+
+ - 1: Once open, only one process manipulates the watchdog;
+ - 2: Following 1, the keep-alive mechanisms will not be used;
+ - 3: If required, nowayout will be set before opening the watchdog;
+ - 4: A safe timeout must be set;
+ - 5: At least one ping must be made before entering the safe/safe_nwo states
+ - 6: The The RV monitor does not react if the watchdog is closed without stopping.
+ But the hardware watchdog is expected to react.
+
+Deterministic automata monitors
+-------------------------------
+
+Following the specifications, two deterministic automata monitors
+were developed. The are the safe_wtd and the safe_wtd_nwo monitors.
+The monitors are modeled as Deterministic Automata models.
+
+The difference between the safe_wtd and the safe_wtd_nwo is that
+the latter enforces the usage of the watchdog's nowayout option
+to reach the safe state.
+
+The deterministic automata model for safe_wtd is::
+
+ #==================================# other_threads
+ H H ----------------+
+ -----------> H init H |
+ H H <---------------+
+ #==================================#
+ | | ^
+ | | | close
+ | | +----------------------------------------------------+
+ | | |
+ | | open |
+ | +------------------------------------------------------+ |
+ | | |
+ | nowayout | |
+ v | |
+ nowayout +-------------------+ | |
+ other_threads | | nowayout | |
+ +---------------- | nwo |<-------------------------------------+ | |
+ | | | | | |
+ +---------------> | | <+ | | |
+ +-------------------+ | | | |
+ | | | | |
+ | open | close | | |
+ v | | | |
+ +-------------------+ | | | |
+ | opened_nwo | -+ | | |
+ +-------------------+ | | |
+ | | | |
+ | start | | |
+ v | | |
+ +-------------------+ | | |
+ +---------------> | started_nwo | -+ | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | open | set_safe_timeout | | | |
+ | v | | | |
+ | +-------------------+ | | | |
+ | | set_nwo | | | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | +-------------+ | ping | | | |
+ | | | | | | | |
+ | | ping v v | | | |
+ | | +-------------------+ | | | |
+ | +-----------| safe_nwo | | | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | | close | close | | |
+ | v v | | |
+ | +----------------------------------+ nowayout | | |
+ | | | other_threads | | |
+ | | closed_running_nwo | ----------------+ | | |
+ | | | | | | |
+ +---------------- | | <---------------+ | | |
+ +----------------------------------+ | | |
+ | nowayout ^ | | |
+ +-----------------------------+ | | |
+ | | |
+ | | |
+ +-------------------+ +--------+ | | |
+ | | | |------+---+ |
+ | started | start | opened | | |
+ +---------------- | | <-------- | |>-----+-------+
+ | +-------------------+ +--------+ | ^
+ | | | |
+ | | set_safe_timeout +-------------+-------+
+ | v | |
+ | +-------------------+ | |
+ | | | | |
+ | | set | | |
+ +----------+---------------> | | | |
+ | | +-------------------+ | |
+ | | | | |
+ | | | ping | |
+ | | v | |
+ | | +-------------------+ ping | |
+ | | | | -------+ | |
+ | | +---- | safe | | | |
+ | | | | | <------+ | |
+ | | | +-------------------+ | |
+ | | | | | |
+ | | stop | | stop | |
+ | | | v | |
+ | | | +-------------------+ close | |
+ | +-----------+---> | stopped |-------------+ |
+ | | +-------------------+ |
+ | +---+ |
+ | | close |
+ | v |
+ | other_threads +----------------------------------------+ |
+ | +--------------> | | |
+ | | | closed_running | |
+ | +--------------- | |--------------+
+ | +----------------------------------------+
+ | | ^
+ | open | | close
+ | v |
+ | set_safe_timeout +-------------------+
+ +-------------------------> | reopened |
+ +-------------------+
+
+The deterministic automata model for safe_wtd_nwo is::
+
+ |
+ |
+ v
+ #===================#
+ H init H
+ #===================#
+ |
+ | nowayout
+ v
+ nowayout +-------------------+
+ other_threads | |
+ +---------------- | nwo |
+ | | |
+ +---------------> | | <---+
+ +-------------------+ |
+ | |
+ | open | close
+ v |
+ +-------------------+ |
+ | opened | ----+
+ +-------------------+
+ |
+ | start
+ v
+ +-------------------+
+ +---------------> | started | ---+
+ | +-------------------+ |
+ | | |
+ | open | set_safe_timeout |
+ | v |
+ | +-------------------+ |
+ | | set | |
+ | +-------------------+ |
+ | | |
+ | +------------+ | ping |
+ | | v v |
+ | | ping +-------------------+ |
+ | +---------| safe | |
+ | +-------------------+ |
+ | | |
+ | | close | close
+ | v |
+ | +-------------------+ |
+ +---------------- | closed_running | <--+
+ +-------------------+
+ ^ |
+ | nowayout |
+ | other_threads |
+ +---------------+
+
+It is important to note that the events sched_keep_alive and keep_alive
+are not allowed on any of the present monitors (they are said to be blocked
+events). The execution of any blocked events leads the RV monitor to react.
+
+Additional options
+------------------
+
+The RV monitor also has a set of options enabled via kernel command
+line/module options. They are:
+
+ - watchdog_id: the device id to monitor (default 0);
+ - dont_stop: once enabled, do not allow the RV monitor to be stopped (default off);
+ - safe_timeout: define a maximum safe value that a user-space application can
+ set as the watchdog timeout (default unlimited);
+ - check_timeout: After every ping, check if the time left in the watchdog is less
+ than or equal to the last timeout set for the watchdog. It only works for watchdog
+ devices that provide the get_timeleft() function (default off);
--
2.33.1
Add the da_monitor_instrumentation.rst. It describes the basics
of RV monitor instrumentation.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
.../trace/rv/da_monitor_instrumentation.rst | 230 ++++++++++++++++++
1 file changed, 230 insertions(+)
create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst
new file mode 100644
index 000000000000..6c5188f76cba
--- /dev/null
+++ b/Documentation/trace/rv/da_monitor_instrumentation.rst
@@ -0,0 +1,230 @@
+Deterministic Automata Instrumentation
+========================================
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor instrumentation.
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automatized by a tool named dot2k, and the "rv/da_monitor.h" provided
+by the RV interface.
+
+For example, given a file "wip.dot", representing a per-cpu monitor, with
+this content::
+
+ digraph state_automaton {
+ center = true;
+ size = "7,11";
+ rankdir = LR;
+ {node [shape = circle] "non_preemptive"};
+ {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+ {node [shape = doublecircle] "preemptive"};
+ {node [shape = circle] "preemptive"};
+ "__init_preemptive" -> "preemptive";
+ "non_preemptive" [label = "non_preemptive"];
+ "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+ "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+ "preemptive" [label = "preemptive"];
+ "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+ { rank = min ;
+ "__init_preemptive";
+ "preemptive";
+ }
+ }
+
+That is the "DOT" representation of this automata model::
+
+ preempt_enable
+ +---------------------------------+
+ v |
+ #============# preempt_disable +------------------+
+ --> H preemptive H -----------------> | non_preemptive |
+ #============# +------------------+
+ ^ sched_waking |
+ +--------------+
+
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+ $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+ monitor
+- wip.c: the RV monitor
+
+The monitor instrumentation should be done entirely in the RV monitor,
+in the example above, in the wip.c file.
+
+The RV monitor instrumentation section
+--------------------------------------
+
+The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
+will include a section dedicated to instrumentation.
+
+In the example of the wip.dot above, it will look like::
+
+ /*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(preempt_disable);
+ }
+
+ void handle_preempt_enable(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(preempt_enable);
+ }
+
+ void handle_sched_waking(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(sched_waking);
+ }
+
+ #define NR_TP 3
+ struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_preempt_disable,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_preempt_enable,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_sched_waking,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ };
+
+The comment at the top of the section explains the general idea: the
+instrumentation section translates *kernel events* into the *events
+accepted by the model*.
+
+Tracing callback functions
+-----------------------------
+
+The first three functions are skeletons for callback *handler functions* for
+each of the three events from the wip model. The developer does not
+necessarily need to use them: they are just starting points.
+
+Using the example of::
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(preempt_disable);
+ }
+
+The "preempt_disable" event from the model conects directly to the
+"preemptirq:preempt_disable". The "preemptirq:preempt_disable" event
+has the following signature, from "include/trace/events/preemptirq.h"::
+
+ TP_PROTO(unsigned long ip, unsigned long parent_ip)
+
+Hence, the "handle_preempt_disable()" function will look like::
+
+ void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
+
+In this case, the kernel even translates one to one with the automata event,
+and indeed, no other change is needed for this function.
+
+The next handler function, "handle_preempt_enable()" has the same argument
+list from the "handle_preempt_disable()". The difference is that the
+"preempt_enable" event will be used to synchronize the system to the model.
+
+Initially, the *model* is placed in the initial state. However, the *system*
+might, or might not be in the initial state. The monitor cannot start
+processing events until it knows that the system reached the initial state. Otherwise the monitor and the system could be out-of-sync.
+
+Looking at the automata definition, it is possible to see that the system
+and the model are expected to return to the initial state after the
+"preempt_enable" execution. Hence, it can be used to synchronize the
+system and the model at the initialization of the monitoring section.
+
+The initialization is informed via an special handle function, the
+"da_handle_init_event_$(MONITOR)(event)", in this case::
+
+ da_handle_event_wip(preempt_disable);
+
+So, the callback function will look like::
+
+ void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
+ {
+ da_handle_init_event_wip(preempt_enable);
+ }
+
+Finally, the "handle_sched_waking()" will look like::
+
+ void handle_sched_waking(void *data, struct task_struct *task)
+ {
+ da_handle_event_wip(sched_waking);
+ }
+
+And the explanation is left for the reader as an exercise.
+
+Tracepoint hook helpers
+--------------------------
+
+Still in the previous example, the next code section is the
+"tracepoint_to_hook" definition, which is a structure that aims to help to
+connect a monitor *handler function* with a given "tracepoint". Note that
+this is just a suggestion. Indeed, the *handler functions* can hook to anything
+that is possible to hook in the kernel, not even limited to the
+tracing interface.
+
+For the specific case of wip, the "tracepoints_to_hook" structure was
+defined as::
+
+ #define NR_TP 3
+ struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_preempt_disable,
+ .name = "preempt_disable",
+ .registered = 0
+ },
+ {
+ .probe = handle_preempt_enable,
+ .name = "preempt_enable",
+ .registered = 0
+ },
+ {
+ .probe = handle_sched_waking,
+ .name = "sched_wakeup",
+ .registered = 0
+ },
+ };
+
+And that is the instrumentation required for the wip sample model.
+
+Start and Stop functions
+------------------------
+
+Finally, dot2k automatically creates two special functions::
+
+ start_$MODELNAME()
+ stop_$MODELNAME()
+
+These functions are called when the monitor is enabled and disabled,
+respectivelly.
+They should be used to *hook* and *unhook* the instrumentation to the running
+system. The developer must add to the relative function all that is needed to
+*hook* and *unhook* its monitor to the system.
+
+For the wip case, these functions were named::
+
+ start_wip()
+ stop_wip()
+
+But no change was required because: by default, these functions *hook* and
+*unhook* the tracepoints_to_hook, which was enough for this case.
--
2.33.1
Per task wakeup while not running (wwnr) monitor, generated by dot2k
with this command line:
$ dot2k -d wwnr.dot -t per_task
The model is:
----- %< -----
digraph state_automaton {
center = true;
size = "7,11";
{node [shape = plaintext, style=invis, label=""] "__init_not_running"};
{node [shape = ellipse] "not_running"};
{node [shape = plaintext] "not_running"};
{node [shape = plaintext] "running"};
"__init_not_running" -> "not_running";
"not_running" [label = "not_running", color = green3];
"not_running" -> "not_running" [ label = "wakeup" ];
"not_running" -> "running" [ label = "switch_in" ];
"running" [label = "running"];
"running" -> "not_running" [ label = "switch_out" ];
{ rank = min ;
"__init_not_running";
"not_running";
}
}
----- >% -----
This model is broken, the reason is that a task can be running in the
processor without being set as RUNNABLE. Think about a task about to
sleep:
1: set_current_state(TASK_UNINTERRUPTIBLE);
2: schedule();
And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.
Q: Why do we need this model, so?
A: To test the reactors.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/monitor_wwnr/model.h | 38 ++++++++
kernel/trace/rv/monitor_wwnr/wwnr.c | 127 +++++++++++++++++++++++++++
kernel/trace/rv/monitor_wwnr/wwnr.h | 70 +++++++++++++++
3 files changed, 235 insertions(+)
create mode 100644 kernel/trace/rv/monitor_wwnr/model.h
create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.c
create mode 100644 kernel/trace/rv/monitor_wwnr/wwnr.h
diff --git a/kernel/trace/rv/monitor_wwnr/model.h b/kernel/trace/rv/monitor_wwnr/model.h
new file mode 100644
index 000000000000..7840ffbda98d
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/model.h
@@ -0,0 +1,38 @@
+enum states_wwnr {
+ not_running = 0,
+ running,
+ state_max
+};
+
+enum events_wwnr {
+ switch_in = 0,
+ switch_out,
+ wakeup,
+ event_max
+};
+
+struct automaton_wwnr {
+ char *state_names[state_max];
+ char *event_names[event_max];
+ char function[state_max][event_max];
+ char initial_state;
+ char final_states[state_max];
+};
+
+struct automaton_wwnr automaton_wwnr = {
+ .state_names = {
+ "not_running",
+ "running"
+ },
+ .event_names = {
+ "switch_in",
+ "switch_out",
+ "wakeup"
+ },
+ .function = {
+ { running, -1, not_running },
+ { -1, not_running, -1 },
+ },
+ .initial_state = not_running,
+ .final_states = { 1, 0 },
+};
\ No newline at end of file
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.c b/kernel/trace/rv/monitor_wwnr/wwnr.c
new file mode 100644
index 000000000000..91cb3b70a6a7
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.c
@@ -0,0 +1,127 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "wwnr"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_wwnr;
+DECLARE_DA_MON_PER_TASK(wwnr, char);
+
+#define CREATE_TRACE_POINTS
+#include "wwnr.h"
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+void handle_switch_in(void *data, /* XXX: fill header */)
+{
+ pid_t pid = /* XXX how do I get the pid? */;
+ da_handle_event_wwnr(pid, switch_in);
+}
+
+void handle_switch_out(void *data, /* XXX: fill header */)
+{
+ pid_t pid = /* XXX how do I get the pid? */;
+ da_handle_event_wwnr(pid, switch_out);
+}
+
+void handle_wakeup(void *data, /* XXX: fill header */)
+{
+ pid_t pid = /* XXX how do I get the pid? */;
+ da_handle_event_wwnr(pid, wakeup);
+}
+
+#define NR_TP 3
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_switch_in,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_switch_out,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_wakeup,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+};
+
+static int start_wwnr(void)
+{
+ int retval;
+
+ da_monitor_init_wwnr();
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_wwnr(void)
+{
+ rv_wwnr.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_wwnr = {
+ .name = "wwnr",
+ .description = "auto-generated wwnr",
+ .start = start_wwnr,
+ .stop = stop_wwnr,
+ .reset = da_monitor_reset_all_wwnr,
+ .enabled = 0,
+};
+
+int register_wwnr(void)
+{
+ rv_register_monitor(&rv_wwnr);
+ return 0;
+}
+
+void unregister_wwnr(void)
+{
+ if (rv_wwnr.enabled)
+ stop_wwnr();
+
+ rv_unregister_monitor(&rv_wwnr);
+}
+
+module_init(register_wwnr);
+module_exit(unregister_wwnr);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("wwnr");
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.h b/kernel/trace/rv/monitor_wwnr/wwnr.h
new file mode 100644
index 000000000000..4af1827d2f16
--- /dev/null
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.h
@@ -0,0 +1,70 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_WWNR_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _WWNR_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_wwnr,
+
+ TP_PROTO(pid_t pid, char state, char event, char next_state, bool safe),
+
+ TP_ARGS(pid, state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( pid_t, pid )
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->pid = pid;
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%d: %s x %s -> %s %s",
+ __entry->pid,
+ model_get_state_name_wwnr(__entry->state),
+ model_get_event_name_wwnr(__entry->event),
+ model_get_state_name_wwnr(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_wwnr,
+
+ TP_PROTO(pid_t pid, char state, char event),
+
+ TP_ARGS(pid, state, event),
+
+ TP_STRUCT__entry(
+ __field( pid_t, pid )
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->pid = pid;
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("%d event %s not expected in the state %s",
+ __entry->pid,
+ model_get_event_name_wwnr(__entry->event),
+ model_get_state_name_wwnr(__entry->state))
+);
+
+#endif /* _WWNR_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE wwnr
+#include <trace/define_trace.h>
--
2.33.1
RV is a lightweight (yet rigorous) method that complements classical
exhaustive verification techniques (such as model checking and
theorem proving) with a more practical approach to complex systems.
RV works by analyzing the trace of the system's actual execution,
comparing it against a formal specification of the system behavior.
RV can give precise information on the runtime behavior of the
monitored system while enabling the reaction for unexpected
events, avoiding, for example, the propagation of a failure on
safety-critical systems.
The development of this interface roots in the development of the
paper:
DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo
Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods.
Springer, Cham, 2019. p. 315-332.
And:
DE OLIVEIRA, Daniel Bristot, et al. Automata-based formal analysis
and verification of the real-time Linux kernel. PhD Thesis, 2020.
The RV interface resembles the tracing/ interface on purpose. The current
path for the RV interface is /sys/kernel/tracing/rv/.
It presents these files:
"available_monitors"
- List the available monitors, one per line.
For example:
[root@f32 rv]# cat available_monitors
wip
wwnr
"enabled_monitors"
- Lists the enabled monitors, one per line;
- Writing to it enables a given monitor;
- Writing a monitor name with a '-' prefix disables it;
- Truncating the file disables all enabled monitors.
For example:
[root@f32 rv]# cat enabled_monitors
[root@f32 rv]# echo wip > enabled_monitors
[root@f32 rv]# echo wwnr >> enabled_monitors
[root@f32 rv]# cat enabled_monitors
wip
wwnr
[root@f32 rv]# echo -wip >> enabled_monitors
[root@f32 rv]# cat enabled_monitors
wwnr
[root@f32 rv]# echo > enabled_monitors
[root@f32 rv]# cat enabled_monitors
[root@f32 rv]#
Note that more than one monitor can be enabled concurrently.
"monitoring_on"
- It is an on/off general switcher for monitoring. Note
that it does not disable enabled monitors, but stop the per-entity
monitors of monitoring the events received from the system.
It resambles the "tracing_on" switcher.
"monitors/"
Each monitor will have its one directory inside "monitors/". There
the monitor specific files will be presented.
The "monitors/" directory resambles the "events" directory on
tracefs.
For example:
[root@f32 rv]# cd monitors/wip/
[root@f32 wip]# ls
desc enable
[root@f32 wip]# cat desc
auto-generated wakeup in preemptive monitor.
[root@f32 wip]# cat enable
0
For further information, see the comments in the header of
kernel/trace/rv/rv.c from this patch.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/linux/rv.h | 21 ++
kernel/trace/Kconfig | 2 +
kernel/trace/Makefile | 2 +
kernel/trace/rv/Kconfig | 12 +
kernel/trace/rv/Makefile | 3 +
kernel/trace/rv/rv.c | 687 +++++++++++++++++++++++++++++++++++++++
kernel/trace/rv/rv.h | 31 ++
kernel/trace/trace.c | 4 +
kernel/trace/trace.h | 2 +
9 files changed, 764 insertions(+)
create mode 100644 include/linux/rv.h
create mode 100644 kernel/trace/rv/Kconfig
create mode 100644 kernel/trace/rv/Makefile
create mode 100644 kernel/trace/rv/rv.c
create mode 100644 kernel/trace/rv/rv.h
diff --git a/include/linux/rv.h b/include/linux/rv.h
new file mode 100644
index 000000000000..6034eac8c01b
--- /dev/null
+++ b/include/linux/rv.h
@@ -0,0 +1,21 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Runtime Verification.
+ *
+ * For futher information, see: kernel/trace/rv/rv.c.
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+struct rv_monitor {
+ const char *name;
+ const char *description;
+ bool enabled;
+ int (*start)(void);
+ void (*stop)(void);
+ void (*reset)(void);
+};
+
+extern bool monitoring_on;
+int rv_unregister_monitor(struct rv_monitor *monitor);
+int rv_register_monitor(struct rv_monitor *monitor);
diff --git a/kernel/trace/Kconfig b/kernel/trace/Kconfig
index a5eb5e7fd624..a9bccb108eaa 100644
--- a/kernel/trace/Kconfig
+++ b/kernel/trace/Kconfig
@@ -1062,4 +1062,6 @@ config HIST_TRIGGERS_DEBUG
If unsure, say N.
+source "kernel/trace/rv/Kconfig"
+
endif # FTRACE
diff --git a/kernel/trace/Makefile b/kernel/trace/Makefile
index bedc5caceec7..1a3a12c5f334 100644
--- a/kernel/trace/Makefile
+++ b/kernel/trace/Makefile
@@ -101,3 +101,5 @@ obj-$(CONFIG_FTRACE_RECORD_RECURSION) += trace_recursion_record.o
obj-$(CONFIG_TRACEPOINT_BENCHMARK) += trace_benchmark.o
libftrace-y := ftrace.o
+
+obj-$(CONFIG_RV) += rv/
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
new file mode 100644
index 000000000000..6d127cdb00dd
--- /dev/null
+++ b/kernel/trace/rv/Kconfig
@@ -0,0 +1,12 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+menuconfig RV
+ bool "Runtime Verification"
+ depends on TRACING
+ help
+ Enable the kernel runtime verification infrastructure. RV is a
+ lightweight (yet rigorous) method that complements classical
+ exhaustive verification techniques (such as model checking and
+ theorem proving). RV works by analyzing the trace of the system's
+ actual execution, comparing it against a formal specification of
+ the system behavior.
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
new file mode 100644
index 000000000000..fd995379df67
--- /dev/null
+++ b/kernel/trace/rv/Makefile
@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: GPL-2.0
+
+obj-$(CONFIG_RV) += rv.o
diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
new file mode 100644
index 000000000000..7ec033f4bcda
--- /dev/null
+++ b/kernel/trace/rv/rv.c
@@ -0,0 +1,687 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This is the online Runtime Verification (RV) interface.
+ *
+ * RV is a lightweight (yet rigorous) method that complements classical
+ * exhaustive verification techniques (such as model checking and
+ * theorem proving) with a more practical approach to complex systems.
+ *
+ * RV works by analyzing the trace of the system's actual execution,
+ * comparing it against a formal specification of the system behavior.
+ * RV can give precise information on the runtime behavior of the
+ * monitored system while enabling the reaction for unexpected
+ * events, avoiding, for example, the propagation of a failure on
+ * safety-critical systems.
+ *
+ * The development of this interface roots in the development of the
+ * paper:
+ *
+ * DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo
+ * Silva. Efficient formal verification for the Linux kernel. In:
+ * International Conference on Software Engineering and Formal Methods.
+ * Springer, Cham, 2019. p. 315-332.
+ *
+ * And:
+ *
+ * DE OLIVEIRA, Daniel Bristot, et al. Automata-based formal analysis
+ * and verification of the real-time Linux kernel. PhD Thesis, 2020.
+ *
+ * == Runtime monitor interface ==
+ *
+ * A monitor is the central part of the runtime verification of a system.
+ *
+ * The monitor stands in between the formal specification of the desired
+ * (or undesired) behavior, and the trace of the actual system system.
+ *
+ * In Linux terms, the runtime verification monitors are encapsulated
+ * inside the "RV monitor" abstraction. A RV monitor includes a reference
+ * model of the system, a set of instances of the monitor (per-cpu monitor,
+ * per-task monitor, and so on), and the helper functions that glue the
+ * monitor to the system via trace. Generally, a monitor includes some form
+ * of trace output as a reaction for event parsing and exceptions,
+ * as depicted bellow:
+ *
+ * Linux +----- RV Monitor ----------------------------------+ Formal
+ * Realm | | Realm
+ * +-------------------+ +----------------+ +-----------------+
+ * | Linux kernel | | Monitor | | Reference |
+ * | Tracing | -> | Instance(s) | <- | Model |
+ * | (instrumentation) | | (verification) | | (specification) |
+ * +-------------------+ +----------------+ +-----------------+
+ * | | |
+ * | V |
+ * | +----------+ |
+ * | | Reaction | |
+ * | +--+--+--+-+ |
+ * | | | | |
+ * | | | +-> trace output ? |
+ * +------------------------|--|----------------------+
+ * | +----> panic ?
+ * +-------> <user-specified>
+ *
+ * This file implements the interface for loading RV monitors, and
+ * to control the verification session.
+ *
+ * == Registering monitors ==
+ *
+ * The struct rv_monitor defines a set of callback functions to control
+ * a verification session. For instance, when a given monitor is enabled,
+ * the "start" callback function is called to hook the instrumentation
+ * functions to the kernel trace events. The "stop" function is called
+ * when disabling the verification session.
+ *
+ * A RV monitor is registered via:
+ * int rv_register_monitor(struct rv_monitor *monitor);
+ * And unregistered via:
+ * int rv_unregister_monitor(struct rv_monitor *monitor);
+ *
+ * These functions are exported to modules, enabling verification monitors
+ * to be dynamically loaded.
+ *
+ * == User interface ==
+ *
+ * The user interface resembles kernel tracing interface. It presents
+ * these files:
+ *
+ * "available_monitors"
+ * - List the available monitors, one per line.
+ *
+ * For example:
+ * [root@f32 rv]# cat available_monitors
+ * wip
+ * wwnr
+ *
+ * "enabled_monitors"
+ * - Lists the enabled monitors, one per line;
+ * - Writing to it enables a given monitor;
+ * - Writing a monitor name with a '-' prefix disables it;
+ * - Truncating the file disables all enabled monitors.
+ *
+ * For example:
+ * [root@f32 rv]# cat enabled_monitors
+ * [root@f32 rv]# echo wip > enabled_monitors
+ * [root@f32 rv]# echo wwnr >> enabled_monitors
+ * [root@f32 rv]# cat enabled_monitors
+ * wip
+ * wwnr
+ * [root@f32 rv]# echo -wip >> enabled_monitors
+ * [root@f32 rv]# cat enabled_monitors
+ * wwnr
+ * [root@f32 rv]# echo > enabled_monitors
+ * [root@f32 rv]# cat enabled_monitors
+ * [root@f32 rv]#
+ *
+ * Note that more than one monitor can be enabled concurrently.
+ *
+ * "monitoring_on"
+ * - It is an on/off general switcher for monitoring. Note
+ * that it does not disable enabled monitors, but stop the per-entity
+ * monitors of monitoring the events received from the system.
+ * It resambles the "tracing_on" switcher.
+ *
+ * "monitors/"
+ * Each monitor will have its one directory inside "monitors/". There
+ * the monitor specific files will be presented.
+ * The "monitors/" directory resambles the "events" directory on
+ * tracefs.
+ *
+ * For example:
+ * [root@f32 rv]# cd monitors/wip/
+ * [root@f32 wip]# ls
+ * desc enable
+ * [root@f32 wip]# cat desc
+ * auto-generated wakeup in preemptive monitor.
+ * [root@f32 wip]# cat enable
+ * 0
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/slab.h>
+
+#include "rv.h"
+
+DEFINE_MUTEX(rv_interface_lock);
+struct rv_interface rv_root;
+
+struct dentry *get_monitors_root(void)
+{
+ return rv_root.monitors_dir;
+}
+
+/*
+ * Monitoring on global switcher!
+ */
+bool __read_mostly monitoring_on = false;
+EXPORT_SYMBOL_GPL(monitoring_on);
+
+/*
+ * Interface for the monitor register.
+ */
+LIST_HEAD(rv_monitors_list);
+
+/*
+ * This section collects the monitor/ files and folders.
+ */
+static ssize_t monitor_enable_read_data(struct file *filp,
+ char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ struct rv_monitor_def *mdef = filp->private_data;
+ char buff[4];
+
+ memset(buff, 0, sizeof(buff));
+
+ mutex_lock(&rv_interface_lock);
+ sprintf(buff, "%x\n", mdef->monitor->enabled);
+ mutex_unlock(&rv_interface_lock);
+
+ return simple_read_from_buffer(user_buf, count, ppos,
+ buff, strlen(buff)+1);
+}
+
+/*
+ * Disable a given runtime monitor.
+ */
+void disable_monitor(struct rv_monitor_def *mdef)
+{
+ if (mdef->monitor->enabled) {
+ mdef->monitor->enabled = 0;
+ mdef->monitor->stop();
+ }
+
+ mdef->enabled = 0;
+}
+
+/*
+ * Enable a given monitor.
+ */
+void enable_monitor(struct rv_monitor_def *mdef)
+{
+ /*
+ * Reset all internal monitors before starting.
+ */
+ mdef->monitor->reset();
+ if (!mdef->monitor->enabled)
+ mdef->monitor->start();
+
+ mdef->monitor->enabled = 1;
+ mdef->enabled = 1;
+}
+
+/*
+ * interface for enabling/disabling a monitor.
+ */
+static ssize_t monitor_enable_write_data(struct file *filp,
+ const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ struct rv_monitor_def *mdef = filp->private_data;
+ int retval;
+ u64 val;
+
+ retval = kstrtoull_from_user(user_buf, count, 10, &val);
+ if (retval)
+ return retval;
+
+ retval = count;
+
+ mutex_lock(&rv_interface_lock);
+
+ switch (val) {
+ case 0:
+ disable_monitor(mdef);
+ break;
+ case 1:
+ enable_monitor(mdef);
+ break;
+ default:
+ retval = -EINVAL;
+ }
+
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+static const struct file_operations interface_enable_fops = {
+ .open = simple_open,
+ .llseek = no_llseek,
+ .write = monitor_enable_write_data,
+ .read = monitor_enable_read_data,
+};
+
+/*
+ * Interface to read the enable/disable status of a monitor.
+ */
+static ssize_t
+monitor_desc_read_data(struct file *filp, char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ struct rv_monitor_def *mdef = filp->private_data;
+ char buf[MAX_RV_MONITOR_NAME_SIZE];
+
+ memset(buf, 0, sizeof(buf));
+
+ mutex_lock(&rv_interface_lock);
+ sprintf(buf, "%s\n", mdef->monitor->description);
+ mutex_unlock(&rv_interface_lock);
+
+ return simple_read_from_buffer(user_buf, count, ppos,
+ buf, strlen(buf)+1);
+}
+
+static const struct file_operations interface_desc_fops = {
+ .open = simple_open,
+ .llseek = no_llseek,
+ .read = monitor_desc_read_data,
+};
+
+/*
+ * During the registration of a monitor, this function creates
+ * the monitor dir, where the specific options of the monitor
+ * is exposed.
+ */
+static int create_monitor_dir(struct rv_monitor_def *mdef)
+{
+ struct dentry *root = get_monitors_root();
+ struct dentry *tmp;
+ const char *name = mdef->monitor->name;
+ int retval = 0;
+
+ mdef->root_d = rv_create_dir(name, root);
+
+ if (!mdef->root_d)
+ return -ENOMEM;
+
+ tmp = rv_create_file("enable", 0600,
+ mdef->root_d, mdef,
+ &interface_enable_fops);
+ if (!tmp) {
+ retval = -ENOMEM;
+ goto out_remove_root;
+ }
+
+ tmp = rv_create_file("desc", 0400,
+ mdef->root_d, mdef,
+ &interface_desc_fops);
+ if (!tmp) {
+ retval = -ENOMEM;
+ goto out_remove_root;
+ }
+
+ return retval;
+
+out_remove_root:
+ rv_remove(mdef->root_d);
+ return retval;
+}
+
+/*
+ * Available/Enable monitor shared seq functions.
+ */
+static int monitors_show(struct seq_file *m, void *p)
+{
+ struct rv_monitor_def *mon_def = p;
+ seq_printf(m, "%s\n", mon_def->monitor->name);
+ return 0;
+}
+
+/*
+ * Used by the seq file operations at the end of a read
+ * operation.
+ */
+static void monitors_stop(struct seq_file *m, void *p)
+{
+ mutex_unlock(&rv_interface_lock);
+}
+
+/*
+ * Available monitor seq functions:
+ */
+static void *available_monitors_start(struct seq_file *m, loff_t *pos)
+{
+ mutex_lock(&rv_interface_lock);
+ return seq_list_start(&rv_monitors_list, *pos);
+}
+
+static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos)
+{
+ return seq_list_next(p, &rv_monitors_list, pos);
+}
+
+/*
+ * Enable monitor seq functions:
+ */
+
+static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos)
+{
+ struct rv_monitor_def *m_def = p;
+
+ (*pos)++;
+
+ list_for_each_entry_continue(m_def, &rv_monitors_list, list) {
+ if (m_def->monitor->enabled)
+ return m_def;
+ }
+
+ return NULL;
+}
+
+static void *enabled_monitors_start(struct seq_file *m, loff_t *pos)
+{
+ struct rv_monitor_def *m_def;
+ loff_t l;
+
+ mutex_lock(&rv_interface_lock);
+ m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list);
+
+ for (l = 0; l <= *pos; ) {
+ m_def = enabled_monitors_next(m, m_def, &l);
+ if (!m_def)
+ break;
+ }
+
+ return m_def;
+}
+
+/*
+ * available/enabled monitors seq definition.
+ */
+static const struct seq_operations available_monitors_seq_ops = {
+ .start = available_monitors_start,
+ .next = available_monitors_next,
+ .stop = monitors_stop,
+ .show = monitors_show
+};
+
+static const struct seq_operations enabled_monitors_seq_ops = {
+ .start = enabled_monitors_start,
+ .next = enabled_monitors_next,
+ .stop = monitors_stop,
+ .show = monitors_show
+};
+
+/*
+ * available_monitors interface.
+ */
+static int available_monitors_open(struct inode *inode, struct file *file)
+{
+ return seq_open(file, &available_monitors_seq_ops);
+};
+
+static struct file_operations available_monitors_ops = {
+ .open = available_monitors_open,
+ .read = seq_read,
+ .llseek = seq_lseek,
+ .release = seq_release
+};
+
+/*
+ * enabled_monitors interface
+ */
+static void disable_all_monitors(void)
+{
+ struct rv_monitor_def *mdef;
+
+ list_for_each_entry(mdef, &rv_monitors_list, list)
+ disable_monitor(mdef);
+
+ return;
+}
+
+static int enabled_monitors_open(struct inode *inode, struct file *file)
+{
+ if ((file->f_mode & FMODE_WRITE) && (file->f_flags & O_TRUNC))
+ disable_all_monitors();
+
+ return seq_open(file, &enabled_monitors_seq_ops);
+};
+
+static ssize_t
+enabled_monitors_write(struct file *filp, const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[MAX_RV_MONITOR_NAME_SIZE+1];
+ struct rv_monitor_def *mdef;
+ int retval = -EINVAL;
+ bool enable = true;
+ char *ptr = buff;
+ int len;
+
+ if (count < 1 || count > MAX_RV_MONITOR_NAME_SIZE+1)
+ return -EINVAL;
+
+ memset(buff, 0, sizeof(buff));
+
+ retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf,
+ count);
+ if (!retval)
+ return -EFAULT;
+
+ if (buff[0] == '-') {
+ enable=false;
+ ptr++;
+ }
+
+ len = strlen(ptr);
+ if (!len)
+ return count;
+ /*
+ * remove the \n
+ */
+ ptr[len-1]='\0';
+
+ mutex_lock(&rv_interface_lock);
+
+ retval = -EINVAL;
+
+ list_for_each_entry(mdef, &rv_monitors_list, list) {
+ if (strcmp(ptr, mdef->monitor->name) == 0) {
+ /*
+ * Monitor found!
+ */
+ if (enable)
+ enable_monitor(mdef);
+ else
+ disable_monitor(mdef);
+
+ retval=count;
+ break;
+ }
+ }
+
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+static struct file_operations enabled_monitors_ops = {
+ .open = enabled_monitors_open,
+ .read = seq_read,
+ .write = enabled_monitors_write,
+ .llseek = seq_lseek,
+ .release = seq_release,
+};
+
+/*
+ * monitoring_on general switcher
+ */
+static ssize_t monitoring_on_read_data(struct file *filp,
+ char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[4];
+
+ memset(buff, 0, sizeof(buff));
+
+ mutex_lock(&rv_interface_lock);
+ sprintf(buff, "%d\n", monitoring_on);
+ mutex_unlock(&rv_interface_lock);
+
+ return simple_read_from_buffer(user_buf, count, ppos,
+ buff, strlen(buff)+1);
+}
+
+static void turn_monitoring_off(void)
+{
+ monitoring_on=false;
+}
+
+static void turn_monitoring_on(void)
+{
+ reset_all_monitors();
+ monitoring_on=true;
+
+ return;
+}
+
+static ssize_t monitoring_on_write_data(struct file *filp,
+ const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ int retval;
+ u64 val;
+
+ retval = kstrtoull_from_user(user_buf, count, 10, &val);
+ if (retval)
+ return retval;
+
+ retval = count;
+
+ mutex_lock(&rv_interface_lock);
+
+ switch (val) {
+ case 0:
+ turn_monitoring_off();
+ break;
+ case 1:
+ turn_monitoring_on();
+ break;
+ default:
+ retval = -EINVAL;
+ }
+
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+static const struct file_operations monitoring_on_fops = {
+ .open = simple_open,
+ .llseek = no_llseek,
+ .write = monitoring_on_write_data,
+ .read = monitoring_on_read_data,
+};
+
+/*
+ * Monitor API.
+ */
+static void destroy_monitor_dir(struct rv_monitor_def *mdef)
+{
+ rv_remove(mdef->root_d);
+}
+
+/**
+ * rv_register_monitor - register a rv monitor.
+ * @monitor: The rv_monitor to be registered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_register_monitor(struct rv_monitor *monitor)
+{
+ struct rv_monitor_def *r;
+ int retval = 0;
+
+ if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) {
+ pr_info("Monitor %s has a name longer than %d\n",
+ monitor->name, MAX_RV_MONITOR_NAME_SIZE);
+ return -1;
+ }
+
+ mutex_lock(&rv_interface_lock);
+
+ list_for_each_entry(r, &rv_monitors_list, list) {
+ if (strcmp(monitor->name, r->monitor->name) == 0) {
+ pr_info("Monitor %s is already registered\n",
+ monitor->name);
+ retval = -1;
+ goto out_unlock;
+ }
+ }
+
+ r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL);
+ if (!r) {
+ retval = -ENOMEM;
+ goto out_unlock;
+ }
+
+ r->monitor = monitor;
+
+ create_monitor_dir(r);
+
+ list_add_tail(&r->list, &rv_monitors_list);
+
+out_unlock:
+ mutex_unlock(&rv_interface_lock);
+ return retval;
+}
+EXPORT_SYMBOL_GPL(rv_register_monitor);
+
+/**
+ * rv_unregister_monitor - unregister a rv monitor.
+ * @monitor: The rv_monitor to be unregistered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_unregister_monitor(struct rv_monitor *monitor)
+{
+ struct rv_monitor_def *ptr, *next;
+
+ mutex_lock(&rv_interface_lock);
+
+ list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) {
+ if (strcmp(monitor->name, ptr->monitor->name) == 0) {
+ list_del(&ptr->list);
+ destroy_monitor_dir(ptr);
+ }
+ }
+
+ mutex_unlock(&rv_interface_lock);
+ return 0;
+}
+EXPORT_SYMBOL_GPL(rv_unregister_monitor);
+
+void reset_all_monitors(void)
+{
+ struct rv_monitor_def *mdef;
+
+ /*
+ * Reset all monitors before re-enabling monitoring.
+ */
+ list_for_each_entry(mdef, &rv_monitors_list, list) {
+ if (mdef->monitor->enabled)
+ mdef->monitor->reset();
+ }
+
+}
+
+int __init rv_init_interface(void)
+{
+ rv_root.root_dir = rv_create_dir("rv", NULL);
+ rv_root.monitors_dir = rv_create_dir("monitors", rv_root.root_dir);
+
+ rv_create_file("available_monitors", 0400, rv_root.root_dir, NULL,
+ &available_monitors_ops);
+ rv_create_file("enabled_monitors", 0600, rv_root.root_dir, NULL,
+ &enabled_monitors_ops);
+ rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL,
+ &monitoring_on_fops);
+
+ monitoring_on=true;
+
+ return 0;
+}
diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h
new file mode 100644
index 000000000000..908a5e0357d4
--- /dev/null
+++ b/kernel/trace/rv/rv.h
@@ -0,0 +1,31 @@
+#include <linux/mutex.h>
+
+struct rv_interface {
+ struct dentry *root_dir;
+ struct dentry *monitors_dir;
+};
+
+#include "../trace.h"
+#include <linux/tracefs.h>
+#include <linux/rv.h>
+
+#define rv_create_dir tracefs_create_dir
+#define rv_create_file tracefs_create_file
+#define rv_remove tracefs_remove
+
+#define MAX_RV_MONITOR_NAME_SIZE 100
+
+extern struct mutex rv_interface_lock;
+
+struct rv_monitor_def {
+ struct list_head list;
+ struct rv_monitor *monitor;
+ struct dentry *root_d;
+ bool enabled;
+ bool reacting;
+};
+
+extern bool monitoring_on;
+struct dentry *get_monitors_root(void);
+void reset_all_monitors(void);
+int init_rv_monitors(struct dentry *root_dir);
diff --git a/kernel/trace/trace.c b/kernel/trace/trace.c
index c860f582b078..6a5b858cd1a4 100644
--- a/kernel/trace/trace.c
+++ b/kernel/trace/trace.c
@@ -9712,6 +9712,10 @@ static __init int tracer_init_tracefs(void)
update_tracer_options(&global_trace);
+#ifdef CONFIG_RV
+ rv_init_interface();
+#endif
+
return 0;
}
diff --git a/kernel/trace/trace.h b/kernel/trace/trace.h
index d038ddbf1bea..730e5d646df7 100644
--- a/kernel/trace/trace.h
+++ b/kernel/trace/trace.h
@@ -2010,4 +2010,6 @@ struct trace_min_max_param {
extern const struct file_operations trace_min_max_fops;
+extern int rv_init_interface(void);
+
#endif /* _LINUX_KERNEL_TRACE_H */
--
2.33.1
Adds the instrumentation to the previously created wwnr monitor, as an
example of the developer work. It also adds a Makefile and Kconfig
entries.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 7 ++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitor_wwnr/wwnr.c | 35 +++++++++++++----------------
kernel/trace/rv/monitor_wwnr/wwnr.h | 2 +-
4 files changed, 24 insertions(+), 21 deletions(-)
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 7338e661d78f..f2d0bed05a55 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -20,6 +20,13 @@ config RV_MON_WIP
Enable WIP sample monitor, this is a sample monitor that
illustrates the usage of per-cpu monitors.
+config RV_MON_WWNR
+ tristate "WWNR monitor"
+ help
+ Enable WWNR sample monitor, this is a sample monitor that
+ illustrates the usage of per-task monitor. The model is
+ broken on purpose: it serves to test reactors.
+
config RV_REACTORS
bool "Runtime verification reactors"
default y if RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 20f30741b933..edad01bb2b5d 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -3,3 +3,4 @@
obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_MON_WIP) += monitor_wip/wip.o
+obj-$(CONFIG_RV_MON_WWNR) += monitor_wwnr/wwnr.o
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.c b/kernel/trace/rv/monitor_wwnr/wwnr.c
index 91cb3b70a6a7..cb364a02639b 100644
--- a/kernel/trace/rv/monitor_wwnr/wwnr.c
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.c
@@ -33,39 +33,34 @@ DECLARE_DA_MON_PER_TASK(wwnr, char);
*
*/
-void handle_switch_in(void *data, /* XXX: fill header */)
+static void handle_switch(void *data, bool preempt, struct task_struct *p, struct task_struct *n)
{
- pid_t pid = /* XXX how do I get the pid? */;
- da_handle_event_wwnr(pid, switch_in);
-}
+ int ppid = p->pid;
+ int npid = n->pid;
-void handle_switch_out(void *data, /* XXX: fill header */)
-{
- pid_t pid = /* XXX how do I get the pid? */;
- da_handle_event_wwnr(pid, switch_out);
+ if (ppid && ppid < MAX_PID)
+ da_handle_init_event_wwnr(ppid, switch_out);
+
+ if (npid && npid < MAX_PID)
+ da_handle_event_wwnr(npid, switch_in);
}
-void handle_wakeup(void *data, /* XXX: fill header */)
+static void handle_wakeup(void *data, struct task_struct *p)
{
- pid_t pid = /* XXX how do I get the pid? */;
- da_handle_event_wwnr(pid, wakeup);
+ if (p->pid && p->pid < MAX_PID)
+ da_handle_event_wwnr(p->pid, wakeup);
}
-#define NR_TP 3
+#define NR_TP 2
static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
{
- .probe = handle_switch_in,
- .name = /* XXX: tracepoint name here */,
- .registered = 0
- },
- {
- .probe = handle_switch_out,
- .name = /* XXX: tracepoint name here */,
+ .probe = handle_switch,
+ .name = "sched_switch",
.registered = 0
},
{
.probe = handle_wakeup,
- .name = /* XXX: tracepoint name here */,
+ .name = "sched_wakeup",
.registered = 0
},
};
diff --git a/kernel/trace/rv/monitor_wwnr/wwnr.h b/kernel/trace/rv/monitor_wwnr/wwnr.h
index 4af1827d2f16..387f5a83ee7c 100644
--- a/kernel/trace/rv/monitor_wwnr/wwnr.h
+++ b/kernel/trace/rv/monitor_wwnr/wwnr.h
@@ -65,6 +65,6 @@ TRACE_EVENT(error_wwnr,
/* This part ust be outside protection */
#undef TRACE_INCLUDE_PATH
-#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitor_wwnr/
#define TRACE_INCLUDE_FILE wwnr
#include <trace/define_trace.h>
--
2.33.1
Formally, a deterministic automaton, denoted by G, is defined as a
quintuple:
G = { X, E, f, x_0, X_m }
where:
- X is the set of states;
- E is the finite set of events;
- x_0 is the initial state;
- X_m (subset of X) is the set of marked states.
- f : X x E -> X $ is the transition function. It defines the
state transition in the occurrence of a event from E in
the state X. In the special case of deterministic automata,
the occurence of the event in E in a state in X has a
deterministic next state from X.
An automaton can also be represented using a graphical format of
vertices (nodes) and edges. The open-source tool Graphviz can produce
this graphic format using the (textual) DOT language as the source code.
The dot2c tool presented in this paper:
DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo
Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods.
Springer, Cham, 2019. p. 315-332.
Translates a deterministic automaton in the DOT format into a C
source code representation that to be used for monitoring.
This header file implements helper functions to facilitate the usage
of the C output from dot2c for monitoring.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/rv/automata.h | 52 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 52 insertions(+)
create mode 100644 include/rv/automata.h
diff --git a/include/rv/automata.h b/include/rv/automata.h
new file mode 100644
index 000000000000..dfd0bbf0dc5c
--- /dev/null
+++ b/include/rv/automata.h
@@ -0,0 +1,52 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Deterministic automata helper functions, to be used with the automata
+ * models in C generated by the dot2k tool.
+ *
+ * The dot2k tool is available at https://gitlab.com/linux-rv-tools/dot2/.
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#define DECLARE_AUTOMATA_HELPERS(name, type) \
+ \
+static inline void *model_get_model_##name(void) \
+{ \
+ return (void *) &automaton_##name; \
+} \
+ \
+char *model_get_state_name_##name(enum states_##name state) \
+{ \
+ return automaton_##name.state_names[state]; \
+} \
+ \
+char *model_get_event_name_##name(enum events_##name event) \
+{ \
+ return automaton_##name.event_names[event]; \
+} \
+ \
+static inline type model_get_init_state_##name(void) \
+{ \
+ return automaton_##name.initial_state; \
+} \
+ \
+static inline type \
+model_get_next_state_##name(enum states_##name curr_state, \
+ enum events_##name event) \
+{ \
+ if ((curr_state < 0) || (curr_state > state_max)) \
+ return -1; \
+ \
+ if ((event < 0) || (event > event_max)) \
+ return -1; \
+ \
+ return automaton_##name.function[curr_state][event]; \
+} \
+ \
+static inline bool model_is_final_state_##name(enum states_##name state) \
+{ \
+ if ((state < 0) || (state > state_max)) \
+ return 0; \
+ \
+ return !!automaton_##name.final_states[state]; \
+}
--
2.33.1
Add the da_monitor_synthesis.rst introduces some concepts behind the
Deterministic Automata (DA) monitor synthesis and interface.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
.../trace/rv/da_monitor_synthesis.rst | 286 ++++++++++++++++++
1 file changed, 286 insertions(+)
create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/da_monitor_synthesis.rst
new file mode 100644
index 000000000000..697eb5a45910
--- /dev/null
+++ b/Documentation/trace/rv/da_monitor_synthesis.rst
@@ -0,0 +1,286 @@
+Deterministic Automata Monitor Synthesis
+========================================
+
+The starting point for the application of runtime verification (RV) technics 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*
+conects to the system via an *instrumentation* layer, that converts the events
+from the *system* to the events of the *specification*.
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor synthesis.
+
+DA monitor synthesis in a nutshell
+------------------------------------------------------
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automatized by a tool named "dot2k", and the "rv/da_monitor.h" provided
+by the RV interface.
+
+Given a file "wip.dot", representing a per-cpu monitor, with this content::
+
+ digraph state_automaton {
+ center = true;
+ size = "7,11";
+ rankdir = LR;
+ {node [shape = circle] "non_preemptive"};
+ {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+ {node [shape = doublecircle] "preemptive"};
+ {node [shape = circle] "preemptive"};
+ "__init_preemptive" -> "preemptive";
+ "non_preemptive" [label = "non_preemptive"];
+ "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+ "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+ "preemptive" [label = "preemptive"];
+ "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+ { rank = min ;
+ "__init_preemptive";
+ "preemptive";
+ }
+ }
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+ $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+ monitor
+- wip.c: the RV monitor
+
+The following line in the "wip.c" file is responsible for the monitor
+synthesis::
+
+ DECLARE_DA_MON_PER_CPU(wip, char);
+
+With that in place, the work left to be done is the *instrumentation* of
+the monitor, which is already initialized by dot2k.
+
+DA: Introduction and representation formats
+---------------------------------------------------------------
+
+Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
+
+ *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
+
+where:
+
+- *X* is the set of states;
+- *E* is the finite set of events;
+- x\ :subscript:`0` is the initial state;
+- X\ :subscript:`m` (subset of *X*) is the set of marked states.
+- *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
+ transition in the occurrence of an event from *E* in the state *X*. In the
+ special case of deterministic automata, the occurrence of the event in *E*
+ in a state in *X* has a deterministic next state from *X*.
+
+One of the most evident benefits for the practical application of the automata
+formalism is its *graphic representation*, represented using vertices (nodes)
+and edges, which is very intuitive for *operating system* practitioners.
+
+For example, given an automata wip, with a regular representation of:
+
+- *X* = { ``preemptive``, ``non_preemptive``}
+- *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
+- x\ :subscript:`0` = ``preemptive``
+- X\ :subscript:`m` = {``preemptive``}
+- *f* =
+ - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
+ - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
+ - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
+
+
+It can also be represented in a graphic format, without any loss, using this
+format::
+
+ preempt_enable
+ +---------------------------------+
+ v |
+ #============# preempt_disable +------------------+
+ --> H preemptive H -----------------> | non_preemptive |
+ #============# +------------------+
+ ^ sched_waking |
+ +--------------+
+
+The Graphviz open-source tool can produce this graphic format using the
+(textual) DOT language as the source code. The DOT format is widely
+used and can be converted to many other formats, including the ASCII art above.
+
+The dot2c tool presented in:
+
+ DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Romulo
+ Silva. Efficient formal verification for the Linux kernel. In:
+ International Conference on Software Engineering and Formal Methods.
+ Springer, Cham, 2019. p. 315-332.
+
+Translates a deterministic automaton in the DOT format into a C source
+code. For instance, using the wip model as input for dot2c results in
+the following C representation::
+
+ enum states {
+ preemptive = 0,
+ non_preemptive,
+ state_max
+ };
+
+ enum events {
+ preempt_disable = 0,
+ preempt_enable,
+ sched_waking,
+ event_max
+ };
+
+ struct automaton {
+ char *state_names[state_max];
+ char *event_names[event_max];
+ char function[state_max][event_max];
+ char initial_state;
+ char final_states[state_max];
+ };
+
+ struct automaton aut = {
+ .state_names = {
+ "preemptive",
+ "non_preemptive"
+ },
+ .event_names = {
+ "preempt_disable",
+ "preempt_enable",
+ "sched_waking"
+ },
+ .function = {
+ { non_preemptive, -1, -1 },
+ { -1, preemptive, non_preemptive },
+ },
+ .initial_state = preemptive,
+ .final_states = { 1, 0 },
+ };
+
+DA monitor synthesis for Linux
+------------------------------
+
+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 for 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>
+
+
+The dot2c tool works connecting the *Reference Model* to the *RV Monitor*
+abstraction by translating the *formal notation* into *code*.
+
+The "rv/da_monitor.h" header goes beyond dot2c, extending the code
+generation to the verification stage, generating the code to the *Monitor
+Instance(s)* level using C macros. The trace event code inspires this
+approach.
+
+The benefits of the usage of macro for monitor synthesis is 3-fold:
+
+- 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 two different types of monitor instances:
+
+- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
+- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
+
+The first declares the functions for deterministic automata monitor with
+per-cpu instances, and the second with per-task instances.
+
+In both cases, the name is a string that identifies the monitor, and the type
+is the data type used by dot2c/k on the representation of the model.
+
+For example, the "wip" model with two states and three events can be
+stored in a "char" type. Considering that the preemption control is a
+per-cpu behavior, the monitor declaration will be::
+
+ DECLARE_DA_MON_PER_CPU(wip, 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_init_event_$(MONITOR_NAME)($(event from event enum));
+
+The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case,
+while the function ``da_handle_init_event_$(MONITOR_NAME)()`` is a special
+case used to synchronize the system with the model.
+
+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*.
+Hence, the monitor ignores events sent by sent by
+``da_handle_event_$(MONITOR_NAME)()`` until the function
+``da_handle_init_event_$(MONITOR_NAME)()`` is called.
+
+The function ``da_handle_init_event_$(MONITOR_NAME)()`` should be used for
+the case in which the system generates the event is the one that returns
+the automata to the initial state.
+
+After receiving a ``da_handle_init_event_$(MONITOR_NAME)()`` event, the
+monitor will know that it is in sync with the system and hence will
+start processing the next events.
+
+Using the wip model as example, the events "preempt_disable" and
+"sched_waking" should be sent to to monitor, respectively, via::
+
+ da_handle_event_wip(preempt_disable);
+ da_handle_event_wip(sched_waking);
+
+While the event "preempt_enabled" will use::
+
+ da_handle_init_event_wip(preempt_enable);
+
+To notify the monitor that the system will be returning to the initial state,
+so the system and the monitor should be in sync.
+
+rv/da_monitor.h
+-------------------------------------------
+
+The "rv/da_monitor.h" is, mostly, a set of C macros that create function
+definitions based on the paremeters passed via ``DECLARE_DA_MON_*``.
+
+In fewer words, the declaration of a monitor generates:
+
+- Helper functions for getting information from the automata model generated
+ by dot2k.
+- Helper functions for the analysis of a deterministic automata model
+- Functions for the initialization of the monitor instances
+- The definition of the structure to store the monitor instances' data
+
+One important aspect is that the monitor does not call external functions
+for the handling of the events sent by the instrumentation, except for
+generating *tracing events* or *reactions*.
+
+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.
--
2.33.1
The watchdog is an essential building block for the usage of Linux in
safety-critical systems because it allows the system to be monitored from
an external element - the watchdog hardware, acting as a safety-monitor.
A user-space application controls the watchdog device via the watchdog
interface. This application, hereafter safety_app, enables the watchdog
and periodically pets the watchdog upon correct completion of the safety
related processing.
If the safety_app, for any reason, stops pinging the watchdog,
the watchdog hardware can set the system in a fail-safe state. For
example, shutting the system down.
Given the importance of the safety_app / watchdog hardware couple,
the interaction between these software pieces also needs some
sort of monitoring. In other words, "who monitors the monitor?"
The safe watchdog (safe_wtd) RV monitor monitors the interaction between
the safety_app and the watchdog device, enforcing the correct sequence of
events that leads the system to a safe state.
Furthermore, the safety_app can monitor the RV monitor by collecting the
events generated by the RV monitor itself via tracing interface. In this way,
closing the monitoring loop with the safety_app.
To reach a safe state, the safe_wtd RV monitor requires the
safety_app to:
- Open the watchdog device
- Start the watchdog
- Set a timeout
- ping at least once
The RV monitor also avoids some undesired actions. For example, to have
other threads to touch the watchdog.
The monitor also has a set of options, enabled via kernel command
line/module options. They are:
- watchdog_id: the device id to monitor (default 0).
- dont_stop: once enabled, do not allow the RV monitor to be stopped
(default off);
- safe_timeout: define a maximum safe value that an user-space
application can set as the watchdog timeout
(default unlimited).
- check_timeout: After every ping, check if the time left in the
watchdog is less than or equal to the last timeout set
for the watchdog. It only works for watchdog devices that
provide the get_timeleft() function (default off).
For further information, please refer to:
Documentation/trace/rv/watchdog-monitor.rst
The monitor specification was developed together with Gabriele Paoloni,
in the context of the Linux Foundation Elisa Project.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 9 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitor_safe_wtd/model.h | 84 +++++
kernel/trace/rv/monitor_safe_wtd/safe_wtd.c | 322 ++++++++++++++++++++
kernel/trace/rv/monitor_safe_wtd/safe_wtd.h | 64 ++++
5 files changed, 480 insertions(+)
create mode 100644 kernel/trace/rv/monitor_safe_wtd/model.h
create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.c
create mode 100644 kernel/trace/rv/monitor_safe_wtd/safe_wtd.h
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index a6545a84df13..93b36f215b2b 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -30,6 +30,15 @@ config RV_MON_WWNR
illustrates the usage of per-task monitor. The model is
broken on purpose: it serves to test reactors.
+config RV_MON_SAFE_WTD
+ tristate "Safety watchdog"
+ help
+ Enable safe_wtd, this monitor observes the interaction
+ between a user-space safety monitor and a watchdog device.
+
+ For futher information see:
+ Documentation/trace/rv/safety-monitor.rst
+
config RV_REACTORS
bool "Runtime verification reactors"
default y if RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 1f5747f065ce..854d0f6e453b 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -3,6 +3,7 @@
obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_MON_WIP) += monitor_wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitor_wwnr/wwnr.o
+obj-$(CONFIG_RV_MON_SAFE_WTD) += monitor_safe_wtd/safe_wtd.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o
diff --git a/kernel/trace/rv/monitor_safe_wtd/model.h b/kernel/trace/rv/monitor_safe_wtd/model.h
new file mode 100644
index 000000000000..04377b165c96
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd/model.h
@@ -0,0 +1,84 @@
+enum states_safe_wtd {
+ init = 0,
+ closed_running,
+ closed_running_nwo,
+ nwo,
+ opened,
+ opened_nwo,
+ reopened,
+ safe,
+ safe_nwo,
+ set,
+ set_nwo,
+ started,
+ started_nwo,
+ stopped,
+ state_max
+};
+
+enum events_safe_wtd {
+ close = 0,
+ nowayout,
+ open,
+ other_threads,
+ ping,
+ set_safe_timeout,
+ start,
+ stop,
+ event_max
+};
+
+struct automaton_safe_wtd {
+ char *state_names[state_max];
+ char *event_names[event_max];
+ char function[state_max][event_max];
+ char initial_state;
+ char final_states[state_max];
+};
+
+struct automaton_safe_wtd automaton_safe_wtd = {
+ .state_names = {
+ "init",
+ "closed_running",
+ "closed_running_nwo",
+ "nwo",
+ "opened",
+ "opened_nwo",
+ "reopened",
+ "safe",
+ "safe_nwo",
+ "set",
+ "set_nwo",
+ "started",
+ "started_nwo",
+ "stopped"
+ },
+ .event_names = {
+ "close",
+ "nowayout",
+ "open",
+ "other_threads",
+ "ping",
+ "set_safe_timeout",
+ "start",
+ "stop"
+ },
+ .function = {
+ { -1, nwo, opened, init, -1, -1, -1, -1 },
+ { -1, closed_running_nwo, reopened, closed_running, -1, -1, -1, -1 },
+ { -1, closed_running_nwo, started_nwo, closed_running_nwo, -1, -1, -1, -1 },
+ { -1, nwo, opened_nwo, nwo, -1, -1, -1, -1 },
+ { init, -1, -1, -1, -1, -1, started, -1 },
+ { nwo, -1, -1, -1, -1, -1, started_nwo, -1 },
+ { closed_running, -1, -1, -1, -1, set, -1, opened },
+ { closed_running, -1, -1, -1, safe, -1, -1, stopped },
+ { closed_running_nwo, -1, -1, -1, safe_nwo, -1, -1, -1 },
+ { -1, -1, -1, -1, safe, -1, -1, -1 },
+ { -1, -1, -1, -1, safe_nwo, -1, -1, -1 },
+ { closed_running, -1, -1, -1, -1, set, -1, stopped },
+ { closed_running_nwo, -1, -1, -1, -1, set_nwo, -1, -1 },
+ { init, -1, -1, -1, -1, -1, -1, -1 },
+ },
+ .initial_state = init,
+ .final_states = { 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 },
+};
\ No newline at end of file
diff --git a/kernel/trace/rv/monitor_safe_wtd/safe_wtd.c b/kernel/trace/rv/monitor_safe_wtd/safe_wtd.c
new file mode 100644
index 000000000000..2916d17f8de9
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd/safe_wtd.c
@@ -0,0 +1,322 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#include <linux/watchdog.h>
+#include <linux/moduleparam.h>
+
+#define MODULE_NAME "safe_wtd"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_safe_wtd;
+DECLARE_DA_MON_GLOBAL(safe_wtd, char);
+
+#define CREATE_TRACE_POINTS
+#include "safe_wtd.h"
+
+/*
+ * custom: safe_timeout is the maximum value a watchdog monitor
+ * can set. This value is registered here to duplicate the information.
+ * In this way, a miss-behaving monitor can be detected.
+ */
+static int safe_timeout = ~0;
+module_param(safe_timeout, int, 0444);
+
+/*
+ * custom: if check_timeout is set, the monitor will check if the time left
+ * in the watchdog is less than or equals to the last safe timeout set by
+ * user-space. This check is done after each ping. In this way, if any
+ * code by-passed the watchdog dev interface setting a higher (so unsafe)
+ * timeout, this monitor will catch the side effect and react.
+ */
+static int last_timeout_set = 0;
+static int check_timeout = 0;
+module_param(check_timeout, int, 0444);
+
+/*
+ * custom: if dont_stop is set the monitor will react if stopped.
+ */
+static int dont_stop = 0;
+module_param(dont_stop, int, 0444);
+
+/*
+ * custom: there are some states that are kept after the watchdog is closed.
+ * For example, the nowayout state.
+ *
+ * Thus, the RV monitor needs to keep track of these states after a start/stop
+ * of the RV monitor itself, and should not reset after each restart - keeping the
+ * know state until the system shutdown.
+ *
+ * If for an unknown reason an RV monitor would like to reset the RV monitor at each
+ * RV monitor start, set it to one.
+ */
+static int reset_on_restart = 0;
+module_param(reset_on_restart, int, 0444);
+
+/*
+ * open_pid takes note of the first thread that opened the watchdog.
+ *
+ * Any other thread that generates an event will cause an "other_threads"
+ * event in the monitor.
+ */
+static int open_pid = 0;
+
+/*
+ * watchdog_id: the watchdog to monitor
+ */
+static int watchdog_id = 0;
+module_param(watchdog_id, int, 0444);
+
+static void handle_nowayout(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ da_handle_init_run_event_safe_wtd(nowayout);
+}
+
+static void handle_close(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ } else {
+ da_handle_event_safe_wtd(close);
+ open_pid = 0;
+ }
+}
+
+static void handle_open(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ } else {
+ da_handle_init_run_event_safe_wtd(open);
+ open_pid = current->pid;
+ }
+}
+
+static void blocked_events(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ return;
+ }
+ da_handle_event_safe_wtd(other_threads);
+}
+
+static void handle_ping(void *data, struct watchdog_device *wdd)
+{
+ char msg[128];
+ unsigned int timeout;
+
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd(ping);
+
+ if (!check_timeout)
+ return;
+
+ if (wdd->ops->get_timeleft) {
+ timeout = wdd->ops->get_timeleft(wdd);
+ if (timeout > last_timeout_set) {
+ snprintf(msg, 128,
+ "watchdog timeout is %u > than previously set (%d)\n",
+ timeout, last_timeout_set);
+ cond_react(msg);
+ }
+ } else {
+ snprintf(msg, 128, "error getting timeout: option not supported\n");
+ cond_react(msg);
+ }
+}
+
+static void handle_set_safe_timeout(void *data, struct watchdog_device *wdd, unsigned long timeout)
+{
+ char msg[128];
+
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd(set_safe_timeout);
+
+ if (timeout > safe_timeout) {
+ snprintf(msg, 128, "set safety timeout is too high: %d", (int) timeout);
+ cond_react(msg);
+ }
+
+ if (check_timeout)
+ last_timeout_set = timeout;
+}
+
+static void handle_start(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd(start);
+}
+
+static void handle_stop(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd(stop);
+}
+
+#define NR_TP 9
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_close,
+ .name = "watchdog_close",
+ .registered = 0
+ },
+ {
+ .probe = handle_nowayout,
+ .name = "watchdog_nowayout",
+ .registered = 0
+ },
+ {
+ .probe = handle_open,
+ .name = "watchdog_open",
+ .registered = 0
+ },
+ {
+ .probe = handle_ping,
+ .name = "watchdog_ping",
+ .registered = 0
+ },
+ {
+ .probe = handle_set_safe_timeout,
+ .name = "watchdog_set_timeout",
+ .registered = 0
+ },
+ {
+ .probe = handle_start,
+ .name = "watchdog_start",
+ .registered = 0
+ },
+ {
+ .probe = handle_stop,
+ .name = "watchdog_stop",
+ .registered = 0
+ },
+ {
+ .probe = blocked_events,
+ .name = "watchdog_set_keep_alive",
+ .registered = 0
+ },
+ {
+ .probe = blocked_events,
+ .name = "watchdog_keep_alive",
+ .registered = 0
+ },
+};
+
+static int mon_started = 0;
+
+static int start_safe_wtd(void)
+{
+ int retval;
+
+ if (!mon_started || reset_on_restart) {
+ da_monitor_init_safe_wtd();
+ mon_started = 1;
+ }
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_safe_wtd(void)
+{
+ if (dont_stop)
+ cond_react("dont_stop safe_wtd is set.");
+
+ rv_safe_wtd.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_safe_wtd = {
+ .name = "safe_wtd",
+ .description = "A watchdog monitor guarding a safety monitor actions",
+ .start = start_safe_wtd,
+ .stop = stop_safe_wtd,
+ .reset = da_monitor_reset_all_safe_wtd,
+ .enabled = 0,
+};
+
+int register_safe_wtd(void)
+{
+ rv_register_monitor(&rv_safe_wtd);
+ return 0;
+}
+
+void unregister_safe_wtd(void)
+{
+ if (rv_safe_wtd.enabled)
+ stop_safe_wtd();
+
+ rv_unregister_monitor(&rv_safe_wtd);
+}
+
+module_init(register_safe_wtd);
+module_exit(unregister_safe_wtd);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("Daniel Bristot de Oliveira <[email protected]>");
+MODULE_DESCRIPTION("Safe watchdog RV monitor");
diff --git a/kernel/trace/rv/monitor_safe_wtd/safe_wtd.h b/kernel/trace/rv/monitor_safe_wtd/safe_wtd.h
new file mode 100644
index 000000000000..8d758b9ab445
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd/safe_wtd.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_SAFETY_MONITOR_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _SAFETY_MONITOR_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_safe_wtd,
+
+ TP_PROTO(char state, char event, char next_state, bool safe),
+
+ TP_ARGS(state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%s x %s -> %s %s",
+ model_get_state_name_safe_wtd(__entry->state),
+ model_get_event_name_safe_wtd(__entry->event),
+ model_get_state_name_safe_wtd(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_safe_wtd,
+
+ TP_PROTO(char state, char event),
+
+ TP_ARGS(state, event),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("event %s not expected in the state %s",
+ model_get_event_name_safe_wtd(__entry->event),
+ model_get_state_name_safe_wtd(__entry->state))
+);
+
+#endif /* _SAFETY_MONITOR_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitor_safe_wtd/
+#define TRACE_INCLUDE_FILE safe_wtd
+#include <trace/define_trace.h>
--
2.33.1
transform .dot file into kernel rv monitor
usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION]
optional arguments:
-h, --help show this help message and exit
-d DOT_FILE, --dot DOT_FILE
-t MONITOR_TYPE, --monitor_type MONITOR_TYPE
-n MODEL_NAME, --model_name MODEL_NAME
-D DESCRIPTION, --description DESCRIPTION
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
tools/tracing/rv/dot2/Makefile | 5 +
tools/tracing/rv/dot2/dot2k | 46 +++++
tools/tracing/rv/dot2/dot2k.py | 184 ++++++++++++++++++
.../rv/dot2/dot2k_templates/main_global.c | 96 +++++++++
.../rv/dot2/dot2k_templates/main_global.h | 64 ++++++
.../rv/dot2/dot2k_templates/main_per_cpu.c | 96 +++++++++
.../rv/dot2/dot2k_templates/main_per_cpu.h | 64 ++++++
.../rv/dot2/dot2k_templates/main_per_task.c | 96 +++++++++
.../rv/dot2/dot2k_templates/main_per_task.h | 70 +++++++
9 files changed, 721 insertions(+)
create mode 100644 tools/tracing/rv/dot2/dot2k
create mode 100644 tools/tracing/rv/dot2/dot2k.py
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h
diff --git a/tools/tracing/rv/dot2/Makefile b/tools/tracing/rv/dot2/Makefile
index 9dd59ec8a733..fcec4bf2bb11 100644
--- a/tools/tracing/rv/dot2/Makefile
+++ b/tools/tracing/rv/dot2/Makefile
@@ -19,3 +19,8 @@ install:
$(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
$(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
$(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
+ $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
+ $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
+
+ mkdir -p ${miscdir}/
+ cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
diff --git a/tools/tracing/rv/dot2/dot2k b/tools/tracing/rv/dot2/dot2k
new file mode 100644
index 000000000000..84c069164949
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k
@@ -0,0 +1,46 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+if __name__ == '__main__':
+ from dot2.dot2k import dot2k
+ import argparse
+ import ntpath
+ import os
+ import platform
+ import sys
+ import sys
+ import argparse
+
+ parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
+ parser.add_argument('-d', "--dot", dest="dot_file", required=True)
+ parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True)
+ parser.add_argument('-n', "--model_name", dest="model_name", required=False)
+ parser.add_argument("-D", "--description", dest="description", required=False)
+ params = parser.parse_args()
+
+ print("Opening and parsing the dot file %s" % params.dot_file)
+ try:
+ monitor=dot2k(params.dot_file, params.monitor_type)
+ except Exception as e:
+ print('Error: '+ str(e))
+ print("Sorry : :-(")
+ sys.exit(1)
+
+ # easier than using argparse action.
+ if params.model_name != None:
+ print(params.model_name)
+
+ print("Writing the monitor into the directory %s" % monitor.name)
+ monitor.print_files()
+ print("Done, now edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name))
+ print("Add a Makefile to compile it as a module, or follow the WWNR example in kernel source")
diff --git a/tools/tracing/rv/dot2/dot2k.py b/tools/tracing/rv/dot2/dot2k.py
new file mode 100644
index 000000000000..ad682b1283f0
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k.py
@@ -0,0 +1,184 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2k: transform dot files into a monitor for the Linux kernel.
+#
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+from dot2.dot2c import Dot2c
+import platform
+import os
+
+class dot2k(Dot2c):
+ monitor_types={ "global" : 1, "per_cpu" : 2, "per_task" : 3 }
+ monitor_templates_dir="dot2k/rv_templates/"
+ monitor_type="per_cpu"
+
+ def __init__(self, file_path, MonitorType):
+ super().__init__(file_path)
+
+ self.monitor_type=self.monitor_types.get(MonitorType)
+ if self.monitor_type == None:
+ raise Exception("Unknown monitor type: %s" % MonitorType)
+
+ self.monitor_type=MonitorType
+ self.__fill_rv_templates_dir()
+ self.main_h = self.__open_file(self.monitor_templates_dir + "main_" + MonitorType + ".h")
+ self.main_c = self.__open_file(self.monitor_templates_dir + "main_" + MonitorType + ".c")
+
+ def __fill_rv_templates_dir(self):
+
+ if os.path.exists(self.monitor_templates_dir) == True:
+ return
+
+ if platform.system() != "Linux":
+ raise Exception("I can only run on Linux.")
+
+ kernel_path="/lib/modules/%s/build/tools/rv/%s" % (platform.release(), self.monitor_templates_dir)
+
+ if os.path.exists(kernel_path) == True:
+ self.monitor_templates_dir=kernel_path
+ return
+
+ if os.path.exists("/usr/share/dot2/dot2k_templates/") == True:
+ self.monitor_templates_dir="/usr/share/dot2/dot2k_templates/"
+ return
+
+ raise Exception("Could not find the template directory, do you have the kernel source installed?")
+
+
+ def __open_file(self, path):
+ try:
+ fd = open(path)
+ except OSError:
+ raise Exception("Cannot open the file: %s" % path)
+
+ content = fd.read()
+
+ return content
+
+ def __buff_to_string(self, buff):
+ string=""
+
+ for line in buff:
+ string=string + line + "\n"
+
+ # cut off the last \n
+ return string[:-1]
+
+ def fill_monitor_h(self):
+ monitor_h = self.monitor_h
+
+ min_type=self.get_minimun_type()
+
+ monitor_h = monitor_h.replace("MIN_TYPE", min_type)
+
+ return monitor_h
+
+ def fill_tracepoint_handlers_skel(self):
+ buff=[]
+ for event in self.events:
+ buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event)
+ buff.append("{")
+ if self.monitor_type == "per_task":
+ buff.append("\tpid_t pid = /* XXX how do I get the pid? */;");
+ buff.append("\tda_handle_event_%s(pid, %s);" % (self.name, event));
+ else:
+ buff.append("\tda_handle_event_%s(%s);" % (self.name, event));
+ buff.append("}")
+ buff.append("")
+ return self.__buff_to_string(buff)
+
+ def fill_tracepoint_hook_helper(self):
+ buff=[]
+ for event in self.events:
+ buff.append("\t{")
+ buff.append("\t\t.probe = handle_%s," % event)
+ buff.append("\t\t.name = /* XXX: tracepoint name here */,")
+ buff.append("\t\t.registered = 0")
+ buff.append("\t},")
+ return self.__buff_to_string(buff)
+
+ def fill_main_c(self):
+ main_c = self.main_c
+ min_type=self.get_minimun_type()
+ nr_events=self.events.__len__()
+ tracepoint_handlers=self.fill_tracepoint_handlers_skel()
+ tracepoint_hook_helpers=self.fill_tracepoint_hook_helper()
+
+ main_c = main_c.replace("MIN_TYPE", min_type)
+ main_c = main_c.replace("MODEL_NAME", self.name)
+ main_c = main_c.replace("NR_EVENTS", str(nr_events))
+ main_c = main_c.replace("TRACEPOINT_HANDLERS_SKEL", tracepoint_handlers)
+ main_c = main_c.replace("TRACEPOINT_HOOK_HELPERS", tracepoint_hook_helpers)
+
+ return main_c
+
+ def fill_main_h(self):
+ main_h = self.main_h
+ main_h = main_h.replace("MIN_TYPE", self.get_minimun_type())
+ main_h = main_h.replace("MODEL_NAME_BIG", self.name.upper())
+ main_h = main_h.replace("MODEL_NAME", self.name)
+
+ return main_h
+
+ def fill_model_h(self):
+ #
+ # Adjust the definition names
+ #
+ self.enum_states_def="states_%s" % self.name
+ self.enum_events_def="events_%s" % self.name
+ self.struct_automaton_def="automaton_%s" % self.name
+ self.var_automaton_def="automaton_%s" % self.name
+
+ buff=self.format_model()
+
+ return self.__buff_to_string(buff)
+
+ def __create_directory(self):
+ try:
+ os.mkdir(self.name)
+ except FileExistsError:
+ return
+ except:
+ print("Fail creating the output dir: %s" % self.name)
+
+ def __create_file(self, file_name, content):
+ path="%s/%s" % (self.name, file_name)
+ try:
+ file = open(path, 'w')
+ except FileExistsError:
+ return
+ except:
+ print("Fail creating file: %s" % path)
+
+ file.write(content)
+
+ file.close()
+
+ def __get_main_name(self):
+ path="%s/%s" % (self.name, "main.c")
+ if os.path.exists(path) == False:
+ return "main.c"
+ return "__main.c"
+
+ def print_files(self):
+ main_h=self.fill_main_h()
+ main_c=self.fill_main_c()
+ model_h=self.fill_model_h()
+
+ self.__create_directory()
+
+ path="%s.h" % self.name
+ self.__create_file(path, main_h)
+
+ path="%s.c" % self.name
+ self.__create_file(path, main_c)
+
+ self.__create_file("model.h", model_h)
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_global.c b/tools/tracing/rv/dot2/dot2k_templates/main_global.c
new file mode 100644
index 000000000000..4dc0785ab190
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_global.c
@@ -0,0 +1,96 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_GLOBAL(MODEL_NAME, MIN_TYPE);
+
+#define CREATE_TRACE_POINTS
+#include "MODEL_NAME.h"
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+TRACEPOINT_HANDLERS_SKEL
+#define NR_TP NR_EVENTS
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+TRACEPOINT_HOOK_HELPERS
+};
+
+static int start_MODEL_NAME(void)
+{
+ int retval;
+
+ da_monitor_init_MODEL_NAME();
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .start = start_MODEL_NAME,
+ .stop = stop_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+int register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+void unregister_MODEL_NAME(void)
+{
+ if (rv_MODEL_NAME.enabled)
+ stop_MODEL_NAME();
+
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_global.h b/tools/tracing/rv/dot2/dot2k_templates/main_global.h
new file mode 100644
index 000000000000..d55cb8b83463
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_global.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_MODEL_NAME_BIG_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _MODEL_NAME_BIG_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_MODEL_NAME,
+
+ TP_PROTO(char state, char event, char next_state, bool safe),
+
+ TP_ARGS(state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%s x %s -> %s %s",
+ model_get_state_name_MODEL_NAME(__entry->state),
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_MODEL_NAME,
+
+ TP_PROTO(char state, char event),
+
+ TP_ARGS(state, event),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("event %s not expected in the state %s",
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->state))
+);
+
+#endif /* _MODEL_NAME_BIG_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE MODEL_NAME
+#include <trace/define_trace.h>
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c b/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
new file mode 100644
index 000000000000..e1eb7a89ada2
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
@@ -0,0 +1,96 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_PER_CPU(MODEL_NAME, MIN_TYPE);
+
+#define CREATE_TRACE_POINTS
+#include "MODEL_NAME.h"
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+TRACEPOINT_HANDLERS_SKEL
+#define NR_TP NR_EVENTS
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+TRACEPOINT_HOOK_HELPERS
+};
+
+static int start_MODEL_NAME(void)
+{
+ int retval;
+
+ da_monitor_init_MODEL_NAME();
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .start = start_MODEL_NAME,
+ .stop = stop_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+int register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+void unregister_MODEL_NAME(void)
+{
+ if (rv_MODEL_NAME.enabled)
+ stop_MODEL_NAME();
+
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h b/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
new file mode 100644
index 000000000000..d55cb8b83463
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_MODEL_NAME_BIG_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _MODEL_NAME_BIG_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_MODEL_NAME,
+
+ TP_PROTO(char state, char event, char next_state, bool safe),
+
+ TP_ARGS(state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%s x %s -> %s %s",
+ model_get_state_name_MODEL_NAME(__entry->state),
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_MODEL_NAME,
+
+ TP_PROTO(char state, char event),
+
+ TP_ARGS(state, event),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("event %s not expected in the state %s",
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->state))
+);
+
+#endif /* _MODEL_NAME_BIG_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE MODEL_NAME
+#include <trace/define_trace.h>
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_per_task.c b/tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
new file mode 100644
index 000000000000..5eab9c6f8ab3
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
@@ -0,0 +1,96 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_PER_TASK(MODEL_NAME, MIN_TYPE);
+
+#define CREATE_TRACE_POINTS
+#include "MODEL_NAME.h"
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+TRACEPOINT_HANDLERS_SKEL
+#define NR_TP NR_EVENTS
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+TRACEPOINT_HOOK_HELPERS
+};
+
+static int start_MODEL_NAME(void)
+{
+ int retval;
+
+ da_monitor_init_MODEL_NAME();
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .start = start_MODEL_NAME,
+ .stop = stop_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+int register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+void unregister_MODEL_NAME(void)
+{
+ if (rv_MODEL_NAME.enabled)
+ stop_MODEL_NAME();
+
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/tracing/rv/dot2/dot2k_templates/main_per_task.h b/tools/tracing/rv/dot2/dot2k_templates/main_per_task.h
new file mode 100644
index 000000000000..55fb47265344
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2k_templates/main_per_task.h
@@ -0,0 +1,70 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_MODEL_NAME_BIG_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _MODEL_NAME_BIG_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_MODEL_NAME,
+
+ TP_PROTO(pid_t pid, MIN_TYPE state, MIN_TYPE event, MIN_TYPE next_state, bool safe),
+
+ TP_ARGS(pid, state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( pid_t, pid )
+ __field( MIN_TYPE, state )
+ __field( MIN_TYPE, event )
+ __field( MIN_TYPE, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->pid = pid;
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%d: %s x %s -> %s %s",
+ __entry->pid,
+ model_get_state_name_MODEL_NAME(__entry->state),
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_MODEL_NAME,
+
+ TP_PROTO(pid_t pid, MIN_TYPE state, MIN_TYPE event),
+
+ TP_ARGS(pid, state, event),
+
+ TP_STRUCT__entry(
+ __field( pid_t, pid )
+ __field( MIN_TYPE, state )
+ __field( MIN_TYPE, event )
+ ),
+
+ TP_fast_assign(
+ __entry->pid = pid;
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("%d event %s not expected in the state %s",
+ __entry->pid,
+ model_get_event_name_MODEL_NAME(__entry->event),
+ model_get_state_name_MODEL_NAME(__entry->state))
+);
+
+#endif /* _MODEL_NAME_BIG_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE MODEL_NAME
+#include <trace/define_trace.h>
--
2.33.1
This is a simplification of the safe_wtd monitor, named safe_wtd_nwo.
The difference between these two monitors is that the latter enforces
the nowayout watchdog device option before opening the watchdog.
In this way, once the watchdog is starts, the watchdog hardware will
serve as an safety-monitor until the system shutdown.
For further information, please refer to:
Documentation/trace/rv/watchdog-monitor.rst
The monitor specification was developed together with Gabriele Paoloni,
in the context of the Linux Foundation Elisa Project.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 10 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitor_safe_wtd_nwo/model.h | 61 ++++
.../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c | 309 ++++++++++++++++++
.../rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h | 64 ++++
5 files changed, 445 insertions(+)
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/model.h
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c
create mode 100644 kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 93b36f215b2b..7e797e132f60 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -39,6 +39,16 @@ config RV_MON_SAFE_WTD
For futher information see:
Documentation/trace/rv/safety-monitor.rst
+config RV_MON_SAFE_WTD_NWO
+ tristate "Safety watchdog nowayout"
+ help
+ Enable safe_wtd_nwo, this monitor observes the interaction
+ between a user-space safety monitor and a watchdog device. It
+ enforces the usage of watchdog's nowayout config.
+
+ For futher information see:
+ Documentation/trace/rv/safety-monitor.rst
+
config RV_REACTORS
bool "Runtime verification reactors"
default y if RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 854d0f6e453b..44277103d178 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -4,6 +4,7 @@ obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_MON_WIP) += monitor_wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitor_wwnr/wwnr.o
obj-$(CONFIG_RV_MON_SAFE_WTD) += monitor_safe_wtd/safe_wtd.o
+obj-$(CONFIG_RV_MON_SAFE_WTD_NWO) += monitor_safe_wtd_nwo/safe_wtd_nwo.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o
diff --git a/kernel/trace/rv/monitor_safe_wtd_nwo/model.h b/kernel/trace/rv/monitor_safe_wtd_nwo/model.h
new file mode 100644
index 000000000000..504a93e35b93
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd_nwo/model.h
@@ -0,0 +1,61 @@
+enum states_safe_wtd_nwo {
+ init = 0,
+ closed_running,
+ nwo,
+ opened,
+ safe,
+ set,
+ started,
+ state_max
+};
+
+enum events_safe_wtd_nwo {
+ close = 0,
+ nowayout,
+ open,
+ other_threads,
+ ping,
+ set_safe_timeout,
+ start,
+ event_max
+};
+
+struct automaton_safe_wtd_nwo {
+ char *state_names[state_max];
+ char *event_names[event_max];
+ char function[state_max][event_max];
+ char initial_state;
+ char final_states[state_max];
+};
+
+struct automaton_safe_wtd_nwo automaton_safe_wtd_nwo = {
+ .state_names = {
+ "init",
+ "closed_running",
+ "nwo",
+ "opened",
+ "safe",
+ "set",
+ "started"
+ },
+ .event_names = {
+ "close",
+ "nowayout",
+ "open",
+ "other_threads",
+ "ping",
+ "set_safe_timeout",
+ "start"
+ },
+ .function = {
+ { -1, nwo, -1, -1, -1, -1, -1 },
+ { -1, closed_running, started, closed_running, -1, -1, -1 },
+ { -1, nwo, opened, nwo, -1, -1, -1 },
+ { nwo, -1, -1, -1, -1, -1, started },
+ { closed_running, -1, -1, -1, safe, -1, -1 },
+ { -1, -1, -1, -1, safe, -1, -1 },
+ { closed_running, -1, -1, -1, -1, set, -1 },
+ },
+ .initial_state = init,
+ .final_states = { 1, 0, 0, 0, 0, 0, 0 },
+};
diff --git a/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c b/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c
new file mode 100644
index 000000000000..e19e10da0dc1
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.c
@@ -0,0 +1,309 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#include <linux/watchdog.h>
+#include <linux/moduleparam.h>
+
+#define MODULE_NAME "safe_wtd_nwo"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_safe_wtd_nwo;
+DECLARE_DA_MON_GLOBAL(safe_wtd_nwo, char);
+
+#define CREATE_TRACE_POINTS
+#include "safe_wtd_nwo.h"
+
+/*
+ * custom: safe_timeout is the maximum value a watchdog monitor
+ * can set. This value is registered here to duplicate the information.
+ * In this way, a miss-behaving monitor can be detected.
+ */
+static int safe_timeout = ~0;
+module_param(safe_timeout, int, 0444);
+
+/*
+ * custom: if check_timeout is set, the monitor will check if the time left
+ * in the watchdog is less than or equals to the last safe timeout set by
+ * user-space. This check is done after each ping. In this way, if any
+ * code by-passed the watchdog dev interface setting a higher (so unsafe)
+ * timeout, this monitor will catch the side effect and react.
+ */
+static int last_timeout_set = 0;
+static int check_timeout = 0;
+module_param(check_timeout, int, 0444);
+
+/*
+ * custom: if dont_stop is set the monitor will react if stopped.
+ */
+static int dont_stop = 0;
+module_param(dont_stop, int, 0444);
+
+/*
+ * custom: there are some states that are kept after the watchdog is closed.
+ * For example, the nowayout state.
+ *
+ * Thus, the RV monitor needs to keep track of these states after a start/stop
+ * of the RV monitor itself, and should not reset after each restart - keeping the
+ * know state until the system shutdown.
+ *
+ * If for an unknown reason an RV monitor would like to reset the RV monitor at each
+ * RV monitor start, set it to one.
+ */
+static int reset_on_restart = 0;
+module_param(reset_on_restart, int, 0444);
+
+/*
+ * open_pid takes note of the first thread that opened the watchdog.
+ *
+ * Any other thread that generates an event will cause an "other_threads"
+ * event in the monitor.
+ */
+static int open_pid = 0;
+
+/*
+ * watchdog_id: the watchdog to monitor
+ */
+static int watchdog_id = 0;
+module_param(watchdog_id, int, 0444);
+
+static void handle_nowayout(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ da_handle_init_run_event_safe_wtd_nwo(nowayout);
+}
+
+static void handle_close(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ } else {
+ da_handle_event_safe_wtd_nwo(close);
+ open_pid = 0;
+ }
+}
+
+static void handle_open(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ } else {
+ da_handle_init_run_event_safe_wtd_nwo(open);
+ open_pid = current->pid;
+ }
+}
+
+static void blocked_events(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ return;
+ }
+ da_handle_event_safe_wtd_nwo(other_threads);
+}
+
+static void handle_ping(void *data, struct watchdog_device *wdd)
+{
+ char msg[128];
+ unsigned int timeout;
+
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd_nwo(ping);
+
+ if (!check_timeout)
+ return;
+
+ if (wdd->ops->get_timeleft) {
+ timeout = wdd->ops->get_timeleft(wdd);
+ if (timeout > last_timeout_set) {
+ snprintf(msg, 128,
+ "watchdog timout is %u > than previously set (%d)\n",
+ timeout, last_timeout_set);
+ cond_react(msg);
+ }
+ } else {
+ snprintf(msg, 128, "error getting timeout: option not supported\n");
+ cond_react(msg);
+ }
+}
+
+static void handle_set_safe_timeout(void *data, struct watchdog_device *wdd, unsigned long timeout)
+{
+ char msg[128];
+
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd_nwo(set_safe_timeout);
+
+ if (timeout > safe_timeout) {
+ snprintf(msg, 128, "set safety timeout is too high: %d", (int) timeout);
+ cond_react(msg);
+ }
+
+ if (check_timeout)
+ last_timeout_set = timeout;
+}
+
+static void handle_start(void *data, struct watchdog_device *wdd)
+{
+ if (wdd->id != watchdog_id)
+ return;
+
+ if (open_pid && current->pid != open_pid) {
+ da_handle_init_run_event_safe_wtd_nwo(other_threads);
+ return;
+ }
+
+ da_handle_event_safe_wtd_nwo(start);
+}
+
+#define NR_TP 9
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_close,
+ .name = "watchdog_close",
+ .registered = 0
+ },
+ {
+ .probe = handle_nowayout,
+ .name = "watchdog_nowayout",
+ .registered = 0
+ },
+ {
+ .probe = handle_open,
+ .name = "watchdog_open",
+ .registered = 0
+ },
+ {
+ .probe = handle_ping,
+ .name = "watchdog_ping",
+ .registered = 0
+ },
+ {
+ .probe = handle_set_safe_timeout,
+ .name = "watchdog_set_timeout",
+ .registered = 0
+ },
+ {
+ .probe = handle_start,
+ .name = "watchdog_start",
+ .registered = 0
+ },
+ {
+ .probe = blocked_events,
+ .name = "watchdog_stop",
+ .registered = 0
+ },
+ {
+ .probe = blocked_events,
+ .name = "watchdog_set_keep_alive",
+ .registered = 0
+ },
+ {
+ .probe = blocked_events,
+ .name = "watchdog_keep_alive",
+ .registered = 0
+ },
+};
+
+static int mon_started = 0;
+
+static int start_safe_wtd_nwo(void)
+{
+ int retval;
+
+ if (!mon_started || reset_on_restart) {
+ da_monitor_init_safe_wtd_nwo();
+ mon_started = 1;
+ }
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_safe_wtd_nwo(void)
+{
+ if (dont_stop)
+ cond_react("dont_stop safe_wtd_nwo is set.");
+
+ rv_safe_wtd_nwo.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_safe_wtd_nwo = {
+ .name = "safe_wtd_nwo",
+ .description = "A watchdog monitor guarding a safety monitor actions, nowayout required.",
+ .start = start_safe_wtd_nwo,
+ .stop = stop_safe_wtd_nwo,
+ .reset = da_monitor_reset_all_safe_wtd_nwo,
+ .enabled = 0,
+};
+
+int register_safe_wtd_nwo(void)
+{
+ rv_register_monitor(&rv_safe_wtd_nwo);
+ return 0;
+}
+
+void unregister_safe_wtd_nwo(void)
+{
+ if (rv_safe_wtd_nwo.enabled)
+ stop_safe_wtd_nwo();
+
+ rv_unregister_monitor(&rv_safe_wtd_nwo);
+}
+
+module_init(register_safe_wtd_nwo);
+module_exit(unregister_safe_wtd_nwo);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("Daniel Bristot de Oliveira <[email protected]>");
+MODULE_DESCRIPTION("Safe watchdog RV monitor nowayout");
diff --git a/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h b/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h
new file mode 100644
index 000000000000..0d33800b0972
--- /dev/null
+++ b/kernel/trace/rv/monitor_safe_wtd_nwo/safe_wtd_nwo.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_SAFETY_MONITOR_NWO_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _SAFETY_MONITOR_NWO_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_safe_wtd_nwo,
+
+ TP_PROTO(char state, char event, char next_state, bool safe),
+
+ TP_ARGS(state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%s x %s -> %s %s",
+ model_get_state_name_safe_wtd_nwo(__entry->state),
+ model_get_event_name_safe_wtd_nwo(__entry->event),
+ model_get_state_name_safe_wtd_nwo(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_safe_wtd_nwo,
+
+ TP_PROTO(char state, char event),
+
+ TP_ARGS(state, event),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("event %s not expected in the state %s",
+ model_get_event_name_safe_wtd_nwo(__entry->event),
+ model_get_state_name_safe_wtd_nwo(__entry->state))
+);
+
+#endif /* _SAFETY_MONITOR_NWO_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitor_safe_wtd_nwo/
+#define TRACE_INCLUDE_FILE safe_wtd_nwo
+#include <trace/define_trace.h>
--
2.33.1
This is the direct output this command line:
$ dot2k -d ~/wip.dot -t per_cpu
with wip.dot as:
----- %< -----
digraph state_automaton {
center = true;
size = "7,11";
rankdir = LR;
{node [shape = circle] "non_preemptive"};
{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
{node [shape = doublecircle] "preemptive"};
{node [shape = circle] "preemptive"};
"__init_preemptive" -> "preemptive";
"non_preemptive" [label = "non_preemptive"];
"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
"preemptive" [label = "preemptive"];
"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
{ rank = min ;
"__init_preemptive";
"preemptive";
}
}
----- >% -----
This model is broken because preempt_disable_notrace(). It is broken on
purpose to test the reactors.
It does not compile because it lacks the instrumentation, which will be
add next.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/monitor_wip/model.h | 38 +++++++++
kernel/trace/rv/monitor_wip/wip.c | 124 ++++++++++++++++++++++++++++
kernel/trace/rv/monitor_wip/wip.h | 64 ++++++++++++++
3 files changed, 226 insertions(+)
create mode 100644 kernel/trace/rv/monitor_wip/model.h
create mode 100644 kernel/trace/rv/monitor_wip/wip.c
create mode 100644 kernel/trace/rv/monitor_wip/wip.h
diff --git a/kernel/trace/rv/monitor_wip/model.h b/kernel/trace/rv/monitor_wip/model.h
new file mode 100644
index 000000000000..5212ba5b1dfb
--- /dev/null
+++ b/kernel/trace/rv/monitor_wip/model.h
@@ -0,0 +1,38 @@
+enum states_wip {
+ preemptive = 0,
+ non_preemptive,
+ state_max
+};
+
+enum events_wip {
+ preempt_disable = 0,
+ preempt_enable,
+ sched_waking,
+ event_max
+};
+
+struct automaton_wip {
+ char *state_names[state_max];
+ char *event_names[event_max];
+ char function[state_max][event_max];
+ char initial_state;
+ char final_states[state_max];
+};
+
+struct automaton_wip automaton_wip = {
+ .state_names = {
+ "preemptive",
+ "non_preemptive"
+ },
+ .event_names = {
+ "preempt_disable",
+ "preempt_enable",
+ "sched_waking"
+ },
+ .function = {
+ { non_preemptive, -1, -1 },
+ { -1, preemptive, non_preemptive },
+ },
+ .initial_state = preemptive,
+ .final_states = { 1, 0 },
+};
\ No newline at end of file
diff --git a/kernel/trace/rv/monitor_wip/wip.c b/kernel/trace/rv/monitor_wip/wip.c
new file mode 100644
index 000000000000..1aec75e683d2
--- /dev/null
+++ b/kernel/trace/rv/monitor_wip/wip.c
@@ -0,0 +1,124 @@
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "wip"
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "model.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+struct rv_monitor rv_wip;
+DECLARE_DA_MON_PER_CPU(wip, char);
+
+#define CREATE_TRACE_POINTS
+#include "wip.h"
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+
+void handle_preempt_disable(void *data, /* XXX: fill header */)
+{
+ da_handle_event_wip(preempt_disable);
+}
+
+void handle_preempt_enable(void *data, /* XXX: fill header */)
+{
+ da_handle_event_wip(preempt_enable);
+}
+
+void handle_sched_waking(void *data, /* XXX: fill header */)
+{
+ da_handle_event_wip(sched_waking);
+}
+
+#define NR_TP 3
+static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
+ {
+ .probe = handle_preempt_disable,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_preempt_enable,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+ {
+ .probe = handle_sched_waking,
+ .name = /* XXX: tracepoint name here */,
+ .registered = 0
+ },
+};
+
+static int start_wip(void)
+{
+ int retval;
+
+ da_monitor_init_wip();
+
+ retval = thh_hook_probes(tracepoints_to_hook, NR_TP);
+ if (retval)
+ goto out_err;
+
+ return 0;
+
+out_err:
+ return -EINVAL;
+}
+
+static void stop_wip(void)
+{
+ rv_wip.enabled = 0;
+ thh_unhook_probes(tracepoints_to_hook, NR_TP);
+ return;
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_wip = {
+ .name = "wip",
+ .description = "auto-generated wip",
+ .start = start_wip,
+ .stop = stop_wip,
+ .reset = da_monitor_reset_all_wip,
+ .enabled = 0,
+};
+
+int register_wip(void)
+{
+ rv_register_monitor(&rv_wip);
+ return 0;
+}
+
+void unregister_wip(void)
+{
+ if (rv_wip.enabled)
+ stop_wip();
+
+ rv_unregister_monitor(&rv_wip);
+}
+
+module_init(register_wip);
+module_exit(unregister_wip);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("wip");
diff --git a/kernel/trace/rv/monitor_wip/wip.h b/kernel/trace/rv/monitor_wip/wip.h
new file mode 100644
index 000000000000..7a751a8896e9
--- /dev/null
+++ b/kernel/trace/rv/monitor_wip/wip.h
@@ -0,0 +1,64 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM rv
+
+#if !defined(_WIP_TRACE_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _WIP_TRACE_H
+
+#include <linux/tracepoint.h>
+
+TRACE_EVENT(event_wip,
+
+ TP_PROTO(char state, char event, char next_state, bool safe),
+
+ TP_ARGS(state, event, next_state, safe),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ __field( char, next_state )
+ __field( bool, safe )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ __entry->next_state = next_state;
+ __entry->safe = safe;
+ ),
+
+ TP_printk("%s x %s -> %s %s",
+ model_get_state_name_wip(__entry->state),
+ model_get_event_name_wip(__entry->event),
+ model_get_state_name_wip(__entry->next_state),
+ __entry->safe ? "(safe)" : "")
+);
+
+TRACE_EVENT(error_wip,
+
+ TP_PROTO(char state, char event),
+
+ TP_ARGS(state, event),
+
+ TP_STRUCT__entry(
+ __field( char, state )
+ __field( char, event )
+ ),
+
+ TP_fast_assign(
+ __entry->state = state;
+ __entry->event = event;
+ ),
+
+ TP_printk("event %s not expected in the state %s",
+ model_get_event_name_wip(__entry->event),
+ model_get_state_name_wip(__entry->state))
+);
+
+#endif /* _WIP_H */
+
+/* This part ust be outside protection */
+#undef TRACE_INCLUDE_PATH
+#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_FILE wip
+#include <trace/define_trace.h>
--
2.33.1
Adds the instrumentation to the previously created wip monitor, as an
example of the developer work. It also adds a Makefile and Kconfig
entries.
This is a good example of the manual work that is left for the
developer to do.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 7 +++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitor_wip/wip.c | 16 ++++++++--------
kernel/trace/rv/monitor_wip/wip.h | 2 +-
4 files changed, 17 insertions(+), 9 deletions(-)
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 560408fec0c8..7338e661d78f 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -13,6 +13,13 @@ menuconfig RV
if RV
+config RV_MON_WIP
+ depends on PREEMPTIRQ_TRACEPOINTS
+ tristate "WIP monitor"
+ help
+ Enable WIP sample monitor, this is a sample monitor that
+ illustrates the usage of per-cpu monitors.
+
config RV_REACTORS
bool "Runtime verification reactors"
default y if RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index 8944274d9b41..20f30741b933 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -2,3 +2,4 @@
obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
+obj-$(CONFIG_RV_MON_WIP) += monitor_wip/wip.o
diff --git a/kernel/trace/rv/monitor_wip/wip.c b/kernel/trace/rv/monitor_wip/wip.c
index 1aec75e683d2..dd35a042e727 100644
--- a/kernel/trace/rv/monitor_wip/wip.c
+++ b/kernel/trace/rv/monitor_wip/wip.c
@@ -33,36 +33,36 @@ DECLARE_DA_MON_PER_CPU(wip, char);
*
*/
-void handle_preempt_disable(void *data, /* XXX: fill header */)
+void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
{
da_handle_event_wip(preempt_disable);
}
-void handle_preempt_enable(void *data, /* XXX: fill header */)
+void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
{
- da_handle_event_wip(preempt_enable);
+ da_handle_init_event_wip(preempt_enable);
}
-void handle_sched_waking(void *data, /* XXX: fill header */)
+void handle_sched_waking(void *data, struct task_struct *task)
{
da_handle_event_wip(sched_waking);
}
-#define NR_TP 3
+#define NR_TP 3
static struct tracepoint_hook_helper tracepoints_to_hook[NR_TP] = {
{
.probe = handle_preempt_disable,
- .name = /* XXX: tracepoint name here */,
+ .name = "preempt_disable",
.registered = 0
},
{
.probe = handle_preempt_enable,
- .name = /* XXX: tracepoint name here */,
+ .name = "preempt_enable",
.registered = 0
},
{
.probe = handle_sched_waking,
- .name = /* XXX: tracepoint name here */,
+ .name = "sched_wakeup",
.registered = 0
},
};
diff --git a/kernel/trace/rv/monitor_wip/wip.h b/kernel/trace/rv/monitor_wip/wip.h
index 7a751a8896e9..1ba58a5781ff 100644
--- a/kernel/trace/rv/monitor_wip/wip.h
+++ b/kernel/trace/rv/monitor_wip/wip.h
@@ -59,6 +59,6 @@ TRACE_EVENT(error_wip,
/* This part ust be outside protection */
#undef TRACE_INCLUDE_PATH
-#define TRACE_INCLUDE_PATH .
+#define TRACE_INCLUDE_PATH ../kernel/trace/rv/monitor_wip/
#define TRACE_INCLUDE_FILE wip
#include <trace/define_trace.h>
--
2.33.1
dot2c is a tool that transforms an automata in the graphiviz .dot file
into an C representation of the automata.
usage: dot2c [-h] dot_file
dot2c: converts a .dot file into a C structure
positional arguments:
dot_file The dot file to be converted
optional arguments:
-h, --help show this help message and exit
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
tools/tracing/rv/dot2/Makefile | 21 +++
tools/tracing/rv/dot2/automata.py | 179 ++++++++++++++++++++++
tools/tracing/rv/dot2/dot2c | 30 ++++
tools/tracing/rv/dot2/dot2c.py | 240 ++++++++++++++++++++++++++++++
4 files changed, 470 insertions(+)
create mode 100644 tools/tracing/rv/dot2/Makefile
create mode 100644 tools/tracing/rv/dot2/automata.py
create mode 100644 tools/tracing/rv/dot2/dot2c
create mode 100644 tools/tracing/rv/dot2/dot2c.py
diff --git a/tools/tracing/rv/dot2/Makefile b/tools/tracing/rv/dot2/Makefile
new file mode 100644
index 000000000000..9dd59ec8a733
--- /dev/null
+++ b/tools/tracing/rv/dot2/Makefile
@@ -0,0 +1,21 @@
+INSTALL=install
+
+prefix ?= /usr
+bindir ?= $(prefix)/bin
+mandir ?= $(prefix)/share/man
+miscdir ?= $(prefix)/share/dot2
+srcdir ?= $(prefix)/src
+
+PYLIB ?= $(shell python3 -c 'import distutils.sysconfig; print (distutils.sysconfig.get_python_lib())')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+clean:
+
+.PHONY: install
+install:
+ $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
+ $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+ $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
diff --git a/tools/tracing/rv/dot2/automata.py b/tools/tracing/rv/dot2/automata.py
new file mode 100644
index 000000000000..171ad4497983
--- /dev/null
+++ b/tools/tracing/rv/dot2/automata.py
@@ -0,0 +1,179 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# automata object: parse a dot file into a python object
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+import ntpath
+
+class Automata:
+ """Automata class: Reads a dot file and part it as an automata.
+
+ Attributes:
+ dot_file: A dot file with an state_automaton definition.
+ """
+
+ def __init__(self, file_path):
+ self.__dot_path=file_path
+ self.name=self.__get_model_name()
+ self.__dot_lines = self.__open_dot()
+ self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.events = self.__get_event_variables()
+ self.function = self.__create_matrix()
+
+ def __get_model_name(self):
+ basename=ntpath.basename(self.__dot_path)
+ if basename.endswith(".dot") == False:
+ print("not a dot file")
+ raise Exception("not a dot file: %s" % self.__dot_path)
+
+ model_name=basename[0:-4]
+ if model_name.__len__() == 0:
+ raise Exception("not a dot file: %s" % self.__dot_path)
+
+ return model_name
+
+ def __open_dot(self):
+ cursor = 0
+ dot_lines = []
+ try:
+ dot_file = open(self.__dot_path)
+ except:
+ raise Exception("Cannot open the file: %s" % self.__dot_path)
+
+ dot_lines = dot_file.read().splitlines()
+ dot_file.close()
+
+ # checking the first line:
+ line = dot_lines[cursor].split()
+
+ if (line[0] != "digraph") and (line[1] != "state_automaton"):
+ raise Exception("Not a valid .dot format: %s" % self.__dot_path)
+ else:
+ cursor = cursor + 1
+ return dot_lines
+
+ def __get_cursor_begin_states(self):
+ cursor = 0
+ while self.__dot_lines[cursor].split()[0] != "{node":
+ cursor += 1
+ return cursor
+
+ def __get_cursor_begin_events(self):
+ cursor = 0
+ while self.__dot_lines[cursor].split()[0] != "{node":
+ cursor += 1
+ while self.__dot_lines[cursor].split()[0] == "{node":
+ cursor += 1
+ # skip initial state transition
+ cursor += 1
+ return cursor
+
+ def __get_state_variables(self):
+ # wait for node declaration
+ states = []
+ final_states=[]
+
+ has_final_states = False
+ cursor = self.__get_cursor_begin_states()
+
+ # process nodes
+ while self.__dot_lines[cursor].split()[0] == "{node":
+ line = self.__dot_lines[cursor].split()
+ raw_state = line[-1]
+
+ # "enabled_fired"}; -> enabled_fired
+ state = raw_state.replace('"', '').replace('};', '').replace(',','_')
+ if state[0:7] == "__init_":
+ initial_state = state[7:]
+ else:
+ states.append(state)
+ if self.__dot_lines[cursor].__contains__("doublecircle") == True:
+ final_states.append(state)
+ has_final_states = True
+
+ if self.__dot_lines[cursor].__contains__("ellipse") == True:
+ final_states.append(state)
+ has_final_states = True
+
+ cursor = cursor + 1
+
+ states = sorted(set(states))
+ states.remove(initial_state)
+
+ # Insert the initial state at the bein og the states
+ states.insert(0, initial_state)
+
+ if has_final_states == False:
+ final_states.append(initial_state)
+
+ return states, initial_state, final_states
+
+ def __get_event_variables(self):
+ # here we are at the begin of transitions, take a note, we will return later.
+ cursor = self.__get_cursor_begin_events()
+
+ events = []
+ while self.__dot_lines[cursor][1] == '"':
+ # transitions have the format:
+ # "all_fired" -> "both_fired" [ label = "disable_irq" ];
+ # ------------ event is here ------------^^^^^
+ if self.__dot_lines[cursor].split()[1] == "->":
+ line = self.__dot_lines[cursor].split()
+ event = line[-2].replace('"','')
+
+ # when a transition has more than one lables, they are like this
+ # "local_irq_enable\nhw_local_irq_enable_n"
+ # so split them.
+
+ event = event.replace("\\n", " ")
+ for i in event.split():
+ events.append(i)
+ cursor = cursor + 1
+
+ return sorted(set(events))
+
+ def __create_matrix(self):
+ # transform the array into a dictionary
+ events = self.events
+ states = self.states
+ events_dict = {}
+ states_dict = {}
+ nr_event = 0
+ for event in events:
+ events_dict[event] = nr_event
+ nr_event += 1
+
+ nr_state = 0
+ for state in states:
+ states_dict[state] = nr_state
+ nr_state = nr_state + 1
+
+ # declare the matrix....
+ matrix = [['-1' for x in range(nr_event)] for y in range(nr_state)]
+
+ # and we are back! Let's fill the matrix
+ cursor = self.__get_cursor_begin_events()
+
+ while self.__dot_lines[cursor][1] == '"':
+ if self.__dot_lines[cursor].split()[1] == "->":
+ line = self.__dot_lines[cursor].split()
+ origin_state = line[0].replace('"','').replace(',','_')
+ dest_state = line[2].replace('"','').replace(',','_')
+ possible_events = line[-2].replace('"','').replace("\\n", " ")
+ for event in possible_events.split():
+ matrix[states_dict[origin_state]][events_dict[event]] = dest_state
+ cursor = cursor + 1
+
+ return matrix
diff --git a/tools/tracing/rv/dot2/dot2c b/tools/tracing/rv/dot2/dot2c
new file mode 100644
index 000000000000..0165f203dedc
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2c
@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2m: transform dot files into C structures.
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+if __name__ == '__main__':
+ from dot2 import dot2c
+ import argparse
+ import ntpath
+ import sys
+
+ parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+ parser.add_argument('dot_file', help='The dot file to be converted')
+
+
+ args = parser.parse_args()
+ d=dot2c.Dot2c(args.dot_file)
+ d.print_model_classic()
diff --git a/tools/tracing/rv/dot2/dot2c.py b/tools/tracing/rv/dot2/dot2c.py
new file mode 100644
index 000000000000..0a68851437c8
--- /dev/null
+++ b/tools/tracing/rv/dot2/dot2c.py
@@ -0,0 +1,240 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2c: transform dot files into C structures.
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+from dot2.automata import Automata
+
+class Dot2c(Automata):
+ enum_states_def="states"
+ enum_events_def="events"
+ struct_automaton_def="automaton"
+ var_automaton_def="aut"
+
+ def __init__(self, file_path):
+ super().__init__(file_path)
+ self.line_length=80
+
+ def __buff_to_string(self, buff):
+ string=""
+
+ for line in buff:
+ string=string + line + "\n"
+
+ # cut off the last \n
+ return string[:-1]
+
+ def __get_enum_states_content(self):
+ buff=[]
+ buff.append("\t%s = 0," % self.initial_state)
+ for state in self.states:
+ if state != self.initial_state:
+ buff.append("\t%s," % state)
+ buff.append("\tstate_max")
+
+ return buff
+
+ def get_enum_states_string(self):
+ buff=self.__get_enum_states_content()
+ return self.__buff_to_string(buff)
+
+ def format_states_enum(self):
+ buff=[]
+ buff.append("enum %s {" % self.enum_states_def)
+ buff.append(self.get_enum_states_string())
+ buff.append("};\n")
+
+ return buff
+
+ def __get_enum_events_content(self):
+ buff=[]
+ first=True
+ for event in self.events:
+ if first:
+ buff.append("\t%s = 0," % event)
+ first=False
+ else:
+ buff.append("\t%s," % event)
+ buff.append("\tevent_max")
+
+ return buff
+
+ def get_enum_events_string(self):
+ buff=self.__get_enum_events_content()
+ return self.__buff_to_string(buff)
+
+ def format_events_enum(self):
+ buff=[]
+ buff.append("enum %s {" % self.enum_events_def)
+ buff.append(self.get_enum_events_string())
+ buff.append("};\n")
+
+ return buff
+
+ def get_minimun_type(self):
+ min_type="char"
+
+ if self.states.__len__() > 255:
+ min_type="short"
+
+ if self.states.__len__() > 65535:
+ min_type="int"
+
+ return min_type
+
+ def format_automaton_definition(self):
+ min_type = self.get_minimun_type()
+ buff=[]
+ buff.append("struct %s {" % self.struct_automaton_def)
+ buff.append("\tchar *state_names[state_max];")
+ buff.append("\tchar *event_names[event_max];")
+ buff.append("\t%s function[state_max][event_max];" % min_type)
+ buff.append("\t%s initial_state;" % min_type)
+ buff.append("\tchar final_states[state_max];")
+ buff.append("};\n")
+ return buff
+
+ def format_aut_init_header(self):
+ buff=[]
+ buff.append("struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
+ return buff
+
+ def __get_string_vector_per_line_content(self, buff):
+ first=True
+ string=""
+ for entry in buff:
+ if first:
+ string = string + "\t\t\"" + entry
+ first=False;
+ else:
+ string = string + "\",\n\t\t\"" + entry
+ string = string + "\""
+
+ return string
+
+ def get_aut_init_events_string(self):
+ return self.__get_string_vector_per_line_content(self.events)
+
+ def get_aut_init_states_string(self):
+ return self.__get_string_vector_per_line_content(self.states)
+
+ def format_aut_init_events_string(self):
+ buff=[]
+ buff.append("\t.event_names = {")
+ buff.append(self.get_aut_init_events_string())
+ buff.append("\t},")
+ return buff
+
+ def format_aut_init_states_string(self):
+ buff=[]
+ buff.append("\t.state_names = {")
+ buff.append(self.get_aut_init_states_string())
+ buff.append("\t},")
+
+ return buff
+
+ def __get_max_strlen_of_states(self):
+ return max(self.states, key=len).__len__()
+
+ def __get_state_string_length(self):
+ maxlen = self.__get_max_strlen_of_states()
+ return "%" + str(maxlen) + "s"
+
+ def get_aut_init_function(self):
+ nr_states=self.states.__len__()
+ nr_events=self.events.__len__()
+ buff=[]
+
+ strformat = self.__get_state_string_length()
+
+ for x in range(nr_states):
+ line="\t\t{ "
+ for y in range(nr_events):
+ if y != nr_events-1:
+ line = line + strformat % self.function[x][y] + ", "
+ else:
+ line = line + strformat % self.function[x][y] + " },"
+ buff.append(line)
+
+ return self.__buff_to_string(buff)
+
+ def format_aut_init_function(self):
+ buff=[]
+ buff.append("\t.function = {")
+ buff.append(self.get_aut_init_function())
+ buff.append("\t},")
+
+ return buff
+
+ def get_aut_init_initial_state(self):
+ return self.initial_state
+
+ def format_aut_init_initial_state(self):
+ buff=[]
+ initial_state=self.get_aut_init_initial_state()
+ buff.append("\t.initial_state = " + initial_state + ",")
+
+ return buff
+
+
+ def get_aut_init_final_states(self):
+ line=""
+ first=True
+ for state in self.states:
+ if first == False:
+ line = line + ', '
+ else:
+ first = False
+
+ if self.final_states.__contains__(state):
+ line = line + '1'
+ else:
+ line = line + '0'
+ return line
+
+ def format_aut_init_final_states(self):
+ buff=[]
+ buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
+
+ return buff
+
+ def __get_automaton_initialization_footer_string(self):
+ footer="};"
+ return footer
+
+ def format_aut_init_footer(self):
+ buff=[]
+ buff.append(self.__get_automaton_initialization_footer_string())
+
+ return buff
+
+ def format_model(self):
+ buff=[]
+ buff += self.format_states_enum()
+ buff += self.format_events_enum()
+ buff += self.format_automaton_definition()
+ buff += self.format_aut_init_header()
+ buff += self.format_aut_init_states_string()
+ buff += self.format_aut_init_events_string()
+ buff += self.format_aut_init_function()
+ buff += self.format_aut_init_initial_state()
+ buff += self.format_aut_init_final_states()
+ buff += self.format_aut_init_footer()
+
+ return buff
+
+ def print_model_classic(self):
+ buff=self.format_model()
+ print(self.__buff_to_string(buff))
--
2.33.1
A runtime monitor can cause a reaction to the detection of an
exception on the model's execution. By default, the monitors have
tracing reactions, printing the monitor output via tracepoints.
But other reactions can be added (on-demand) via this interface.
The user interface resembles the kernel tracing interface and
presents these files:
"available_reactors"
- Reading shows the available reactors, one per line.
For example:
[root@f32 rv]# cat available_reactors
nop
panic
printk
"reacting_on"
- It is an on/off general switch for reactors, disabling
all reactions.
"monitors/MONITOR/reactors"
- List available reactors, with the select reaction for the given
MONITOR inside []. The default one is the nop (no operation)
reactor.
- Writing the name of a reactor enables it to the given
MONITOR.
For example:
[root@f32 rv]# cat monitors/wip/reactors
[nop]
panic
printk
[root@f32 rv]# echo panic > monitors/wip/reactors
[root@f32 rv]# cat monitors/wip/reactors
nop
[panic]
printk
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/linux/rv.h | 10 +
kernel/trace/rv/Kconfig | 14 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/rv.c | 17 +-
kernel/trace/rv/rv.h | 19 ++
kernel/trace/rv/rv_reactors.c | 478 ++++++++++++++++++++++++++++++++++
6 files changed, 537 insertions(+), 2 deletions(-)
create mode 100644 kernel/trace/rv/rv_reactors.c
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 6034eac8c01b..c7fc6464dc87 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -6,6 +6,11 @@
*
* Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
*/
+struct rv_reactor {
+ char *name;
+ char *description;
+ void (*react)(char *);
+};
struct rv_monitor {
const char *name;
@@ -14,8 +19,13 @@ struct rv_monitor {
int (*start)(void);
void (*stop)(void);
void (*reset)(void);
+ void (*react)(char *);
};
extern bool monitoring_on;
int rv_unregister_monitor(struct rv_monitor *monitor);
int rv_register_monitor(struct rv_monitor *monitor);
+
+extern bool reacting_on;
+int rv_unregister_reactor(struct rv_reactor *reactor);
+int rv_register_reactor(struct rv_reactor *reactor);
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 6d127cdb00dd..560408fec0c8 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -10,3 +10,17 @@ menuconfig RV
theorem proving). RV works by analyzing the trace of the system's
actual execution, comparing it against a formal specification of
the system behavior.
+
+if RV
+
+config RV_REACTORS
+ bool "Runtime verification reactors"
+ default y if RV
+ help
+ Enables the online runtime verification reactors. A runtime
+ monitor can cause a reaction to the detection of an exception
+ on the model's execution. By default, the monitors have
+ tracing reactions, printing the monitor output via tracepoints,
+ but other reactions can be added (on-demand) via this interface.
+
+endif # RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index fd995379df67..8944274d9b41 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -1,3 +1,4 @@
# SPDX-License-Identifier: GPL-2.0
obj-$(CONFIG_RV) += rv.o
+obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
index 7ec033f4bcda..1b50909c5736 100644
--- a/kernel/trace/rv/rv.c
+++ b/kernel/trace/rv/rv.c
@@ -312,8 +312,13 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
retval = -ENOMEM;
goto out_remove_root;
}
+#ifdef CONFIG_RV_REACTORS
+ retval = reactor_create_monitor_files(mdef);
+ if (retval)
+ goto out_remove_root;
+#endif
- return retval;
+ return 0;
out_remove_root:
rv_remove(mdef->root_d);
@@ -621,7 +626,11 @@ int rv_register_monitor(struct rv_monitor *monitor)
r->monitor = monitor;
- create_monitor_dir(r);
+ retval = create_monitor_dir(r);
+ if (retval) {
+ kfree(r);
+ goto out_unlock;
+ }
list_add_tail(&r->list, &rv_monitors_list);
@@ -681,6 +690,10 @@ int __init rv_init_interface(void)
rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL,
&monitoring_on_fops);
+#ifdef CONFIG_RV_REACTORS
+ init_rv_reactors(rv_root.root_dir);
+ reacting_on=true;
+#endif
monitoring_on=true;
return 0;
diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h
index 908a5e0357d4..c4d462d79b86 100644
--- a/kernel/trace/rv/rv.h
+++ b/kernel/trace/rv/rv.h
@@ -14,12 +14,25 @@ struct rv_interface {
#define rv_remove tracefs_remove
#define MAX_RV_MONITOR_NAME_SIZE 100
+#define MAX_RV_REACTOR_NAME_SIZE 100
extern struct mutex rv_interface_lock;
+#ifdef CONFIG_RV_REACTORS
+struct rv_reactor_def {
+ struct list_head list;
+ struct rv_reactor *reactor;
+ /* protected by the monitor interface lock */
+ int counter;
+};
+#endif
+
struct rv_monitor_def {
struct list_head list;
struct rv_monitor *monitor;
+#ifdef CONFIG_RV_REACTORS
+ struct rv_reactor_def *rdef;
+#endif
struct dentry *root_d;
bool enabled;
bool reacting;
@@ -29,3 +42,9 @@ extern bool monitoring_on;
struct dentry *get_monitors_root(void);
void reset_all_monitors(void);
int init_rv_monitors(struct dentry *root_dir);
+
+#ifdef CONFIG_RV_REACTORS
+extern bool reacting_on;
+int reactor_create_monitor_files(struct rv_monitor_def *mdef);
+int init_rv_reactors(struct dentry *root_dir);
+#endif
diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c
new file mode 100644
index 000000000000..9c08206c3085
--- /dev/null
+++ b/kernel/trace/rv/rv_reactors.c
@@ -0,0 +1,478 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Runtime reactor interface.
+ *
+ * A runtime monitor can cause a reaction to the detection of an
+ * exception on the model's execution. By default, the monitors have
+ * tracing reactions, printing the monitor output via tracepoints.
+ * But other reactions can be added (on-demand) via this interface.
+ *
+ * == Registering reactors ==
+ *
+ * The struct rv_reactor defines a callback function to be executed
+ * in case of a model exception happens. The callback function
+ * receives a message to be (optionally) printed before executing
+ * the reaction.
+ *
+ * A RV reactor is registered via:
+ * int rv_register_reactor(struct rv_reactor *reactor)
+ * And unregistered via:
+ * int rv_unregister_reactor(struct rv_reactor *reactor)
+ *
+ * These functions are exported to modules, enabling reactors to be
+ * dynamically loaded.
+ *
+ * == User interface ==
+ *
+ * The user interface resembles the kernel tracing interface and
+ * presents these files:
+ *
+ * "available_reactors"
+ * - List the available reactors, one per line.
+ *
+ * For example:
+ * [root@f32 rv]# cat available_reactors
+ * nop
+ * panic
+ * printk
+ *
+ * "reacting_on"
+ * - It is an on/off general switch for reactors, disabling
+ * all reactions.
+ *
+ * "monitors/MONITOR/reactors"
+ * - List available reactors, with the select reaction for the given
+ * MONITOR inside []. The defaul one is the nop (no operation)
+ * reactor.
+ * - Writing the name of an reactor enables it to the given
+ * MONITOR.
+ *
+ * For example:
+ * [root@f32 rv]# cat monitors/wip/reactors
+ * [nop]
+ * panic
+ * printk
+ * [root@f32 rv]# echo panic > monitors/wip/reactors
+ * [root@f32 rv]# cat monitors/wip/reactors
+ * nop
+ * [panic]
+ * printk
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#include <linux/slab.h>
+
+#include "rv.h"
+
+bool __read_mostly reacting_on = false;
+EXPORT_SYMBOL_GPL(reacting_on);
+
+/*
+ * Interface for the reactor register.
+ */
+LIST_HEAD(rv_reactors_list);
+
+struct rv_reactor_def *get_reactor_rdef_by_name(char *name)
+{
+ struct rv_reactor_def *r;
+ list_for_each_entry(r, &rv_reactors_list, list) {
+ if (strcmp(name, r->reactor->name) == 0)
+ return r;
+ }
+
+ return NULL;
+}
+
+/*
+ * Available reactors seq functions.
+ */
+static int reactors_show(struct seq_file *m, void *p)
+{
+ struct rv_reactor_def *rea_def = p;
+ seq_printf(m, "%s\n", rea_def->reactor->name);
+ return 0;
+}
+
+static void reactors_stop(struct seq_file *m, void *p)
+{
+ mutex_unlock(&rv_interface_lock);
+}
+
+static void *reactors_start(struct seq_file *m, loff_t *pos)
+{
+ mutex_lock(&rv_interface_lock);
+ return seq_list_start(&rv_reactors_list, *pos);
+}
+
+static void *reactors_next(struct seq_file *m, void *p, loff_t *pos)
+{
+ return seq_list_next(p, &rv_reactors_list, pos);
+}
+
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations available_reactors_seq_ops = {
+ .start = reactors_start,
+ .next = reactors_next,
+ .stop = reactors_stop,
+ .show = reactors_show
+};
+
+/*
+ * available_reactors interface.
+ */
+static int available_reactors_open(struct inode *inode, struct file *file)
+{
+ return seq_open(file, &available_reactors_seq_ops);
+};
+
+static struct file_operations available_reactors_ops = {
+ .open = available_reactors_open,
+ .read = seq_read,
+ .llseek = seq_lseek,
+ .release = seq_release
+};
+
+/*
+ * Monitor reactor file.
+ */
+static int monitor_reactor_show(struct seq_file *m, void *p)
+{
+ struct rv_monitor_def *mdef = m->private;
+ struct rv_reactor_def *rdef = p;
+
+ if (mdef->rdef == rdef)
+ seq_printf(m, "[%s]\n", rdef->reactor->name);
+ else
+ seq_printf(m, "%s\n", rdef->reactor->name);
+ return 0;
+}
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations monitor_reactors_seq_ops = {
+ .start = reactors_start,
+ .next = reactors_next,
+ .stop = reactors_stop,
+ .show = monitor_reactor_show
+};
+
+static ssize_t
+monitor_reactors_write(struct file *file, const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[MAX_RV_REACTOR_NAME_SIZE+1];
+ struct rv_monitor_def *mdef;
+ struct rv_reactor_def *rdef;
+ struct seq_file *seq_f;
+ int retval = -EINVAL;
+ char *ptr = buff;
+ int len;
+
+ if (count < 1 || count > MAX_RV_REACTOR_NAME_SIZE+1)
+ return -EINVAL;
+
+ memset(buff, 0, sizeof(buff));
+
+ retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf,
+ count);
+ if (!retval)
+ return -EFAULT;
+
+ len = strlen(ptr);
+ if (!len)
+ return count;
+ /*
+ * remove the \n
+ */
+ ptr[len-1]='\0';
+
+ /*
+ * See monitor_reactors_open()
+ */
+ seq_f = file->private_data;
+ mdef = seq_f->private;
+
+ mutex_lock(&rv_interface_lock);
+
+ retval = -EINVAL;
+
+ /*
+ * nop special case: disable reacting.
+ */
+ if (strcmp(ptr, "nop") == 0) {
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->stop();
+
+ mdef->rdef = get_reactor_rdef_by_name("nop");
+ mdef->reacting = false;
+ mdef->monitor->react = NULL;
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->start();
+
+ retval = count;
+ goto unlock;
+ }
+
+ list_for_each_entry(rdef, &rv_reactors_list, list) {
+ if (strcmp(ptr, rdef->reactor->name) == 0) {
+ /*
+ * found!
+ */
+ if (mdef->monitor->enabled)
+ mdef->monitor->stop();
+
+ mdef->rdef = rdef;
+ mdef->reacting = true;
+ mdef->monitor->react = rdef->reactor->react;
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->start();
+
+ retval=count;
+ break;
+ }
+ }
+
+unlock:
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+/*
+ * available_reactors interface.
+ */
+static int monitor_reactors_open(struct inode *inode, struct file *file)
+{
+ /*
+ * create file "private" info is stored in the inode->i_private
+ */
+ struct rv_monitor_def *mdef = inode->i_private;
+ struct seq_file *seq_f;
+ int ret;
+
+
+ ret = seq_open(file, &monitor_reactors_seq_ops);
+ if (ret < 0)
+ return ret;
+
+ /*
+ * seq_open stores the seq_file on the file->private data.
+ */
+ seq_f = file->private_data;
+ /*
+ * Copy the create file "private" data to the seq_file
+ * private data.
+ */
+ seq_f->private = mdef;
+
+ return 0;
+};
+
+static struct file_operations monitor_reactors_ops = {
+ .open = monitor_reactors_open,
+ .read = seq_read,
+ .llseek = seq_lseek,
+ .release = seq_release,
+ .write = monitor_reactors_write
+};
+
+static int __rv_register_reactor(struct rv_reactor *reactor)
+{
+ struct rv_reactor_def *r;
+
+ list_for_each_entry(r, &rv_reactors_list, list) {
+ if (strcmp(reactor->name, r->reactor->name) == 0) {
+ pr_info("Reactor %s is already registered\n",
+ reactor->name);
+ return -EINVAL;
+ }
+ }
+
+ r = kzalloc(sizeof(struct rv_reactor_def), GFP_KERNEL);
+ if (!r)
+ return -ENOMEM;
+
+ r->reactor = reactor;
+ r->counter = 0;
+
+ list_add_tail(&r->list, &rv_reactors_list);
+
+ return 0;
+}
+
+/**
+ * rv_register_reactor - register a rv reactor.
+ * @reactor: The rv_reactor to be registered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_register_reactor(struct rv_reactor *reactor)
+{
+ int retval = 0;
+
+ if (strlen(reactor->name) >= MAX_RV_REACTOR_NAME_SIZE) {
+ pr_info("Reactor %s has a name longer than %d\n",
+ reactor->name, MAX_RV_MONITOR_NAME_SIZE);
+ return -EINVAL;
+ }
+
+ mutex_lock(&rv_interface_lock);
+ retval = __rv_register_reactor(reactor);
+ mutex_unlock(&rv_interface_lock);
+ return retval;
+}
+EXPORT_SYMBOL_GPL(rv_register_reactor);
+
+/**
+ * rv_unregister_reactor - unregister a rv reactor.
+ * @reactor: The rv_reactor to be unregistered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_unregister_reactor(struct rv_reactor *reactor)
+{
+ struct rv_reactor_def *ptr, *next;
+
+ mutex_lock(&rv_interface_lock);
+
+ list_for_each_entry_safe(ptr, next, &rv_reactors_list, list) {
+ if (strcmp(reactor->name, ptr->reactor->name) == 0) {
+
+ if (!ptr->counter) {
+ list_del(&ptr->list);
+ } else {
+ printk("rv: the rv_reactor %s is in use by %d monitor(s)\n",
+ ptr->reactor->name, ptr->counter);
+ printk("rv: the rv_reactor %s cannot be removed\n",
+ ptr->reactor->name);
+ return -EBUSY;
+ }
+
+ }
+ }
+
+ mutex_unlock(&rv_interface_lock);
+ return 0;
+}
+EXPORT_SYMBOL_GPL(rv_unregister_reactor);
+
+/*
+ * reacting_on interface.
+ */
+static ssize_t reacting_on_read_data(struct file *filp,
+ char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[4];
+
+ memset(buff, 0, sizeof(buff));
+
+ mutex_lock(&rv_interface_lock);
+ sprintf(buff, "%d\n", reacting_on);
+ mutex_unlock(&rv_interface_lock);
+
+ return simple_read_from_buffer(user_buf, count, ppos,
+ buff, strlen(buff)+1);
+}
+
+static void turn_reacting_off(void)
+{
+ reacting_on=false;
+}
+
+static void turn_reacting_on(void)
+{
+ reacting_on=true;
+}
+
+static ssize_t
+reacting_on_write_data(struct file *filp, const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ int retval;
+ u64 val;
+
+ retval = kstrtoull_from_user(user_buf, count, 10, &val);
+ if (retval)
+ return retval;
+
+ retval = count;
+
+ mutex_lock(&rv_interface_lock);
+
+ switch (val) {
+ case 0:
+ turn_reacting_off();
+ break;
+ case 1:
+ turn_reacting_on();
+ break;
+ default:
+ retval = -EINVAL;
+ }
+
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+static const struct file_operations reacting_on_fops = {
+ .open = simple_open,
+ .llseek = no_llseek,
+ .write = reacting_on_write_data,
+ .read = reacting_on_read_data,
+};
+
+
+int reactor_create_monitor_files(struct rv_monitor_def *mdef)
+{
+ struct dentry *tmp;
+
+ tmp = rv_create_file("reactors", 0400, mdef->root_d, mdef,
+ &monitor_reactors_ops);
+ if (!tmp)
+ return -ENOMEM;
+
+ /*
+ * Configure as the rv_nop reactor.
+ */
+ mdef->rdef = get_reactor_rdef_by_name("nop");
+ mdef->reacting = false;
+ return 0;
+}
+
+/*
+ * None reactor register
+ */
+static void rv_nop_reaction(char *msg)
+{
+ return;
+}
+
+struct rv_reactor rv_nop = {
+ .name = "nop",
+ .description = "no-operation reactor: do nothing.",
+ .react = rv_nop_reaction
+};
+
+/*
+ * This section collects the rv/ root dir files and folders.
+ */
+int init_rv_reactors(struct dentry *root_dir)
+{
+ rv_create_file("available_reactors", 0400, root_dir, NULL,
+ &available_reactors_ops);
+ rv_create_file("reacting_on", 0600, root_dir, NULL, &reacting_on_fops);
+
+ __rv_register_reactor(&rv_nop);
+
+ return 0;
+}
--
2.33.1
Sample reactor that panics the system when an exception is found. This
is useful both to capture a vmcore, or to fail-safe a critical system.
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 8 ++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/reactor_panic.c | 44 +++++++++++++++++++++++++++++++++
3 files changed, 53 insertions(+)
create mode 100644 kernel/trace/rv/reactor_panic.c
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 490f1417def9..7940898a0504 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -45,4 +45,12 @@ config RV_REACT_PRINTK
Enables the printk reactor. The printk reactor emmits a printk()
message if an exception is found.
+config RV_REACT_PANIC
+ tristate "Panic reactor"
+ depends on RV_REACTORS
+ default y if RV_REACTORS
+ help
+ Enables the panic reactor. The panic reactor emmits a printk()
+ message if an exception is found and panic()s the system.
+
endif # RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index d86ceb103ef2..1f5747f065ce 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -5,3 +5,4 @@ obj-$(CONFIG_RV_MON_WIP) += monitor_wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitor_wwnr/wwnr.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
+obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o
diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c
new file mode 100644
index 000000000000..538cd3846a4e
--- /dev/null
+++ b/kernel/trace/rv/reactor_panic.c
@@ -0,0 +1,44 @@
+/*
+ * Panic RV reactor:
+ * Prints the exception msg to the kernel message log and panic().
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ *
+ * SPDX-License-Identifier: GPL-2.0
+ */
+
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+static void rv_panic_reaction(char *msg)
+{
+ panic(msg);
+}
+
+struct rv_reactor rv_panic = {
+ .name = "panic",
+ .description = "panic the system if an exception is found.",
+ .react = rv_panic_reaction
+};
+
+int register_react_panic(void)
+{
+ rv_register_reactor(&rv_panic);
+ return 0;
+}
+
+void unregister_react_panic(void)
+{
+ rv_unregister_reactor(&rv_panic);
+}
+
+module_init(register_react_panic);
+module_exit(unregister_react_panic);
+
+MODULE_LICENSE("GPL v2");
+MODULE_AUTHOR("Daniel Bristot de Oliveira");
+MODULE_DESCRIPTION("panic rv reactor: panic if an exception is found");
--
2.33.1
Add a set of tracepoints, enabling the observability of the watchdog
device interactions with user-space.
The events are:
watchdog:watchdog_open
watchdog:watchdog_close
watchdog:watchdog_start
watchdog:watchdog_stop
watchdog:watchdog_set_timeout
watchdog:watchdog_ping
watchdog:watchdog_nowayout
watchdog:watchdog_set_keep_alive
watchdog:watchdog_keep_alive
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
drivers/watchdog/watchdog_dev.c | 41 ++++++++++++-
include/linux/watchdog.h | 7 +--
include/trace/events/watchdog.h | 103 ++++++++++++++++++++++++++++++++
3 files changed, 142 insertions(+), 9 deletions(-)
create mode 100644 include/trace/events/watchdog.h
diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
index 3a3d8b5c7ad5..0beeac5d4541 100644
--- a/drivers/watchdog/watchdog_dev.c
+++ b/drivers/watchdog/watchdog_dev.c
@@ -44,6 +44,9 @@
#include <linux/watchdog.h> /* For watchdog specific items */
#include <linux/uaccess.h> /* For copy_to_user/put_user/... */
+#define CREATE_TRACE_POINTS
+#include <trace/events/watchdog.h>
+
#include "watchdog_core.h"
#include "watchdog_pretimeout.h"
@@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
if (watchdog_need_worker(wdd)) {
ktime_t t = watchdog_next_keepalive(wdd);
- if (t > 0)
+ if (t > 0) {
hrtimer_start(&wd_data->timer, t,
HRTIMER_MODE_REL_HARD);
+ trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
+ }
} else {
hrtimer_cancel(&wd_data->timer);
}
@@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
now = ktime_get();
if (ktime_after(earliest_keepalive, now)) {
- hrtimer_start(&wd_data->timer,
- ktime_sub(earliest_keepalive, now),
+ ktime_t t = ktime_sub(earliest_keepalive, now);
+ hrtimer_start(&wd_data->timer, t,
HRTIMER_MODE_REL_HARD);
+ trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
return 0;
}
wd_data->last_hw_keepalive = now;
+ trace_watchdog_ping(wdd);
if (wdd->ops->ping)
err = wdd->ops->ping(wdd); /* ping the watchdog */
else
@@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
wd_data = container_of(work, struct watchdog_core_data, work);
mutex_lock(&wd_data->lock);
+ trace_watchdog_keep_alive(wd_data->wdd);
if (watchdog_worker_should_ping(wd_data))
__watchdog_ping(wd_data->wdd);
mutex_unlock(&wd_data->lock);
@@ -252,6 +260,8 @@ static int watchdog_start(struct watchdog_device *wdd)
set_bit(_WDOG_KEEPALIVE, &wd_data->status);
+ trace_watchdog_start(wdd);
+
started_at = ktime_get();
if (watchdog_hw_running(wdd) && wdd->ops->ping) {
err = __watchdog_ping(wdd);
@@ -298,6 +308,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
return -EBUSY;
}
+ trace_watchdog_stop(wdd);
if (wdd->ops->stop) {
clear_bit(WDOG_HW_RUNNING, &wdd->status);
err = wdd->ops->stop(wdd);
@@ -370,6 +381,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
if (watchdog_timeout_invalid(wdd, timeout))
return -EINVAL;
+ trace_watchdog_set_timeout(wdd, timeout);
if (wdd->ops->set_timeout) {
err = wdd->ops->set_timeout(wdd, timeout);
} else {
@@ -432,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device *wdd,
return 0;
}
+/*
+ * watchdog_set_nowayout - set nowaout bit
+ * @wdd: The watchdog device to set nowayoutbit
+ * @nowayout A boolean on/off switcher
+ *
+ * If nowayout boolean is true, the nowayout option is set. No action is
+ * taken if nowayout is false.
+ */
+void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
+{
+ if (nowayout) {
+ set_bit(WDOG_NO_WAY_OUT, &wdd->status);
+ trace_watchdog_nowayout(wdd);
+ }
+}
+EXPORT_SYMBOL(watchdog_set_nowayout);
+
#ifdef CONFIG_WATCHDOG_SYSFS
static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
char *buf)
@@ -457,6 +486,7 @@ static ssize_t nowayout_store(struct device *dev, struct device_attribute *attr,
/* nowayout cannot be disabled once set */
if (test_bit(WDOG_NO_WAY_OUT, &wdd->status) && !value)
return -EPERM;
+
watchdog_set_nowayout(wdd, value);
return len;
}
@@ -858,6 +888,8 @@ static int watchdog_open(struct inode *inode, struct file *file)
goto out_clear;
}
+ trace_watchdog_open(wdd);
+
err = watchdog_start(wdd);
if (err < 0)
goto out_mod;
@@ -880,6 +912,7 @@ static int watchdog_open(struct inode *inode, struct file *file)
return stream_open(inode, file);
out_mod:
+ trace_watchdog_close(wdd);
module_put(wd_data->wdd->ops->owner);
out_clear:
clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
@@ -940,6 +973,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
/* make sure that /dev/watchdog can be re-opened */
clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
+ trace_watchdog_close(wdd);
done:
running = wdd && watchdog_hw_running(wdd);
mutex_unlock(&wd_data->lock);
@@ -952,6 +986,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
module_put(wd_data->cdev.owner);
put_device(&wd_data->dev);
}
+
return 0;
}
diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
index 99660197a36c..11d93407e492 100644
--- a/include/linux/watchdog.h
+++ b/include/linux/watchdog.h
@@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct watchdog_device *wdd)
return test_bit(WDOG_HW_RUNNING, &wdd->status);
}
-/* Use the following function to set the nowayout feature */
-static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
-{
- if (nowayout)
- set_bit(WDOG_NO_WAY_OUT, &wdd->status);
-}
+void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
/* Use the following function to stop the watchdog on reboot */
static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
new file mode 100644
index 000000000000..5d5617ab611a
--- /dev/null
+++ b/include/trace/events/watchdog.h
@@ -0,0 +1,103 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM watchdog
+
+#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _TRACE_WATCHDOG_H
+
+#include <linux/tracepoint.h>
+
+DECLARE_EVENT_CLASS(dev_operations_template,
+
+ TP_PROTO(struct watchdog_device *wdd),
+
+ TP_ARGS(wdd),
+
+ TP_STRUCT__entry(
+ __field(__u32, id)
+ ),
+
+ TP_fast_assign(
+ __entry->id = wdd->id;
+ ),
+
+ TP_printk("id=%d",
+ __entry->id)
+);
+
+/*
+ * Add a comment
+ */
+DEFINE_EVENT(dev_operations_template, watchdog_open,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_close,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_start,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_stop,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_ping,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+
+TRACE_EVENT(watchdog_set_timeout,
+
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+
+ TP_ARGS(wdd, timeout),
+
+ TP_STRUCT__entry(
+ __field(__u32, id)
+ __field(__u64, timeout)
+ ),
+
+ TP_fast_assign(
+ __entry->id = wdd->id;
+ __entry->timeout = timeout;
+ ),
+
+ TP_printk("id=%d timeout=%llus",
+ __entry->id, __entry->timeout)
+);
+
+TRACE_EVENT(watchdog_set_keep_alive,
+
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+
+ TP_ARGS(wdd, timeout),
+
+ TP_STRUCT__entry(
+ __field(__u32, id)
+ __field(__u64, timeout)
+ ),
+
+ TP_fast_assign(
+ __entry->id = wdd->id;
+ __entry->timeout = timeout;
+ ),
+
+ TP_printk("id=%d keep_alive=%llums",
+ __entry->id, __entry->timeout)
+);
+
+#endif /* _TRACE_WATCHDOG_H */
+
+/* This part must be outside protection */
+#include <trace/define_trace.h>
--
2.33.1
On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
> Add a set of tracepoints, enabling the observability of the watchdog
> device interactions with user-space.
>
> The events are:
> watchdog:watchdog_open
> watchdog:watchdog_close
> watchdog:watchdog_start
> watchdog:watchdog_stop
> watchdog:watchdog_set_timeout
> watchdog:watchdog_ping
> watchdog:watchdog_nowayout
> watchdog:watchdog_set_keep_alive
> watchdog:watchdog_keep_alive
Some watchdogs have a bark functionality, I think it should be event for that too.
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> drivers/watchdog/watchdog_dev.c | 41 ++++++++++++-
> include/linux/watchdog.h | 7 +--
> include/trace/events/watchdog.h | 103 ++++++++++++++++++++++++++++++++
> 3 files changed, 142 insertions(+), 9 deletions(-)
> create mode 100644 include/trace/events/watchdog.h
>
> diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
> index 3a3d8b5c7ad5..0beeac5d4541 100644
> --- a/drivers/watchdog/watchdog_dev.c
> +++ b/drivers/watchdog/watchdog_dev.c
> @@ -44,6 +44,9 @@
> #include <linux/watchdog.h> /* For watchdog specific items */
> #include <linux/uaccess.h> /* For copy_to_user/put_user/... */
>
> +#define CREATE_TRACE_POINTS
> +#include <trace/events/watchdog.h>
> +
> #include "watchdog_core.h"
> #include "watchdog_pretimeout.h"
>
> @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
> if (watchdog_need_worker(wdd)) {
> ktime_t t = watchdog_next_keepalive(wdd);
>
> - if (t > 0)
> + if (t > 0) {
> hrtimer_start(&wd_data->timer, t,
> HRTIMER_MODE_REL_HARD);
> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
> + }
> } else {
> hrtimer_cancel(&wd_data->timer);
> }
> @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
> now = ktime_get();
>
> if (ktime_after(earliest_keepalive, now)) {
> - hrtimer_start(&wd_data->timer,
> - ktime_sub(earliest_keepalive, now),
> + ktime_t t = ktime_sub(earliest_keepalive, now);
> + hrtimer_start(&wd_data->timer, t,
> HRTIMER_MODE_REL_HARD);
> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
> return 0;
> }
>
> wd_data->last_hw_keepalive = now;
>
> + trace_watchdog_ping(wdd);
> if (wdd->ops->ping)
> err = wdd->ops->ping(wdd); /* ping the watchdog */
> else
> @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
> wd_data = container_of(work, struct watchdog_core_data, work);
>
> mutex_lock(&wd_data->lock);
> + trace_watchdog_keep_alive(wd_data->wdd);
> if (watchdog_worker_should_ping(wd_data))
> __watchdog_ping(wd_data->wdd);
> mutex_unlock(&wd_data->lock);
> @@ -252,6 +260,8 @@ static int watchdog_start(struct watchdog_device *wdd)
>
> set_bit(_WDOG_KEEPALIVE, &wd_data->status);
>
> + trace_watchdog_start(wdd);
> +
> started_at = ktime_get();
> if (watchdog_hw_running(wdd) && wdd->ops->ping) {
> err = __watchdog_ping(wdd);
> @@ -298,6 +308,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
> return -EBUSY;
> }
>
> + trace_watchdog_stop(wdd);
> if (wdd->ops->stop) {
> clear_bit(WDOG_HW_RUNNING, &wdd->status);
> err = wdd->ops->stop(wdd);
> @@ -370,6 +381,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
> if (watchdog_timeout_invalid(wdd, timeout))
> return -EINVAL;
>
> + trace_watchdog_set_timeout(wdd, timeout);
> if (wdd->ops->set_timeout) {
> err = wdd->ops->set_timeout(wdd, timeout);
> } else {
> @@ -432,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device *wdd,
> return 0;
> }
>
> +/*
> + * watchdog_set_nowayout - set nowaout bit
> + * @wdd: The watchdog device to set nowayoutbit
> + * @nowayout A boolean on/off switcher
> + *
> + * If nowayout boolean is true, the nowayout option is set. No action is
> + * taken if nowayout is false.
> + */
> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
> +{
> + if (nowayout) {
> + set_bit(WDOG_NO_WAY_OUT, &wdd->status);
> + trace_watchdog_nowayout(wdd);
> + }
> +}
> +EXPORT_SYMBOL(watchdog_set_nowayout);
> +
> #ifdef CONFIG_WATCHDOG_SYSFS
> static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
> char *buf)
> @@ -457,6 +486,7 @@ static ssize_t nowayout_store(struct device *dev, struct device_attribute *attr,
> /* nowayout cannot be disabled once set */
> if (test_bit(WDOG_NO_WAY_OUT, &wdd->status) && !value)
> return -EPERM;
> +
> watchdog_set_nowayout(wdd, value);
> return len;
> }
> @@ -858,6 +888,8 @@ static int watchdog_open(struct inode *inode, struct file *file)
> goto out_clear;
> }
>
> + trace_watchdog_open(wdd);
> +
> err = watchdog_start(wdd);
> if (err < 0)
> goto out_mod;
> @@ -880,6 +912,7 @@ static int watchdog_open(struct inode *inode, struct file *file)
> return stream_open(inode, file);
>
> out_mod:
> + trace_watchdog_close(wdd);
> module_put(wd_data->wdd->ops->owner);
> out_clear:
> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
> @@ -940,6 +973,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
> /* make sure that /dev/watchdog can be re-opened */
> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>
> + trace_watchdog_close(wdd);
> done:
> running = wdd && watchdog_hw_running(wdd);
> mutex_unlock(&wd_data->lock);
> @@ -952,6 +986,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
> module_put(wd_data->cdev.owner);
> put_device(&wd_data->dev);
> }
> +
> return 0;
> }
>
> diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
> index 99660197a36c..11d93407e492 100644
> --- a/include/linux/watchdog.h
> +++ b/include/linux/watchdog.h
> @@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct watchdog_device *wdd)
> return test_bit(WDOG_HW_RUNNING, &wdd->status);
> }
>
> -/* Use the following function to set the nowayout feature */
> -static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
> -{
> - if (nowayout)
> - set_bit(WDOG_NO_WAY_OUT, &wdd->status);
> -}
> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
>
> /* Use the following function to stop the watchdog on reboot */
> static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
> diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
> new file mode 100644
> index 000000000000..5d5617ab611a
> --- /dev/null
> +++ b/include/trace/events/watchdog.h
> @@ -0,0 +1,103 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +#undef TRACE_SYSTEM
> +#define TRACE_SYSTEM watchdog
> +
> +#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
> +#define _TRACE_WATCHDOG_H
> +
> +#include <linux/tracepoint.h>
> +
> +DECLARE_EVENT_CLASS(dev_operations_template,
> +
> + TP_PROTO(struct watchdog_device *wdd),
> +
> + TP_ARGS(wdd),
> +
> + TP_STRUCT__entry(
> + __field(__u32, id)
> + ),
> +
> + TP_fast_assign(
> + __entry->id = wdd->id;
> + ),
> +
> + TP_printk("id=%d",
> + __entry->id)
> +);
> +
> +/*
> + * Add a comment
> + */
> +DEFINE_EVENT(dev_operations_template, watchdog_open,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_close,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_start,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_stop,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_ping,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +
> +TRACE_EVENT(watchdog_set_timeout,
> +
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> +
> + TP_ARGS(wdd, timeout),
> +
> + TP_STRUCT__entry(
> + __field(__u32, id)
> + __field(__u64, timeout)
> + ),
> +
> + TP_fast_assign(
> + __entry->id = wdd->id;
> + __entry->timeout = timeout;
> + ),
> +
> + TP_printk("id=%d timeout=%llus",
> + __entry->id, __entry->timeout)
> +);
> +
> +TRACE_EVENT(watchdog_set_keep_alive,
> +
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> +
> + TP_ARGS(wdd, timeout),
> +
> + TP_STRUCT__entry(
> + __field(__u32, id)
> + __field(__u64, timeout)
> + ),
> +
> + TP_fast_assign(
> + __entry->id = wdd->id;
> + __entry->timeout = timeout;
> + ),
> +
> + TP_printk("id=%d keep_alive=%llums",
> + __entry->id, __entry->timeout)
> +);
> +
> +#endif /* _TRACE_WATCHDOG_H */
> +
> +/* This part must be outside protection */
> +#include <trace/define_trace.h>
On 2/17/22 18:49, Gabriele Paoloni wrote:
>
> On 17/02/2022 18:27, Guenter Roeck wrote:
>> On 2/17/22 08:27, Daniel Bristot de Oliveira wrote:
>>> Hi Peter
>>>
>>> On 2/16/22 17:01, [email protected] wrote:
>>>> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>>>>> Add a set of tracepoints, enabling the observability of the watchdog
>>>>> device interactions with user-space.
>>>>>
>>>>> The events are:
>>>>> watchdog:watchdog_open
>>>>> watchdog:watchdog_close
>>>>> watchdog:watchdog_start
>>>>> watchdog:watchdog_stop
>>>>> watchdog:watchdog_set_timeout
>>>>> watchdog:watchdog_ping
>>>>> watchdog:watchdog_nowayout
>>>>> watchdog:watchdog_set_keep_alive
>>>>> watchdog:watchdog_keep_alive
>>>> Some watchdogs have a bark functionality, I think it should be event
>>>> for that too.
>>>>
>>> I understand. The problems is that I do not see the bark abstraction
>>> in the
>>> watchdog_dev layer.
>>>
>> I don't even know what "bark functionality" means. A new term for
>> pretimeout ?
>> Something else ?
> From my understanding the bark timeout is actually the pretimeout
> whereas the bite timeout is the actual timeout.
So, what Peter wants is tracepoints for the pretimeout actions?
-- Daniel
On 17/02/2022 18:27, Guenter Roeck wrote:
> On 2/17/22 08:27, Daniel Bristot de Oliveira wrote:
>> Hi Peter
>>
>> On 2/16/22 17:01, [email protected] wrote:
>>> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>>>> Add a set of tracepoints, enabling the observability of the watchdog
>>>> device interactions with user-space.
>>>>
>>>> The events are:
>>>> watchdog:watchdog_open
>>>> watchdog:watchdog_close
>>>> watchdog:watchdog_start
>>>> watchdog:watchdog_stop
>>>> watchdog:watchdog_set_timeout
>>>> watchdog:watchdog_ping
>>>> watchdog:watchdog_nowayout
>>>> watchdog:watchdog_set_keep_alive
>>>> watchdog:watchdog_keep_alive
>>>
>>> Some watchdogs have a bark functionality, I think it should be event
>>> for that too.
>>>
>>
>> I understand. The problems is that I do not see the bark abstraction
>> in the
>> watchdog_dev layer.
>>
>
> I don't even know what "bark functionality" means. A new term for
> pretimeout ?
> Something else ?
From my understanding the bark timeout is actually the pretimeout
whereas the bite timeout is the actual timeout.
I think in the Kernel ftwdt010_wdt and qcom-wdt are bark/bite WTDs
Gab
>
> Guenter
>
>> In the case I am investigating (the safety_monitor/safety_app) the
>> bark is
>> outside of the "OS" view, it is an hardware action - like. shutdown.
>>
>> Am I missing something? Thoughts?
>>
>> -- Daniel
>
On 2/17/22 09:49, Gabriele Paoloni wrote:
>
>
> On 17/02/2022 18:27, Guenter Roeck wrote:
>> On 2/17/22 08:27, Daniel Bristot de Oliveira wrote:
>>> Hi Peter
>>>
>>> On 2/16/22 17:01, [email protected] wrote:
>>>> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>>>>> Add a set of tracepoints, enabling the observability of the watchdog
>>>>> device interactions with user-space.
>>>>>
>>>>> The events are:
>>>>> watchdog:watchdog_open
>>>>> watchdog:watchdog_close
>>>>> watchdog:watchdog_start
>>>>> watchdog:watchdog_stop
>>>>> watchdog:watchdog_set_timeout
>>>>> watchdog:watchdog_ping
>>>>> watchdog:watchdog_nowayout
>>>>> watchdog:watchdog_set_keep_alive
>>>>> watchdog:watchdog_keep_alive
>>>>
>>>> Some watchdogs have a bark functionality, I think it should be event
>>>> for that too.
>>>>
>>>
>>> I understand. The problems is that I do not see the bark abstraction
>>> in the
>>> watchdog_dev layer.
>>>
>>
>> I don't even know what "bark functionality" means. A new term for
>> pretimeout ?
>> Something else ?
>
>>From my understanding the bark timeout is actually the pretimeout
> whereas the bite timeout is the actual timeout.
> I think in the Kernel ftwdt010_wdt and qcom-wdt are bark/bite WTDs
>
If that is the case, I would prefer if we could stick to existing
terminology to avoid issues like "I do not see the bark abstraction".
Thanks,
Guenter
Hi Peter
On 2/16/22 17:01, [email protected] wrote:
> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>> Add a set of tracepoints, enabling the observability of the watchdog
>> device interactions with user-space.
>>
>> The events are:
>> watchdog:watchdog_open
>> watchdog:watchdog_close
>> watchdog:watchdog_start
>> watchdog:watchdog_stop
>> watchdog:watchdog_set_timeout
>> watchdog:watchdog_ping
>> watchdog:watchdog_nowayout
>> watchdog:watchdog_set_keep_alive
>> watchdog:watchdog_keep_alive
>
> Some watchdogs have a bark functionality, I think it should be event for that too.
>
I understand. The problems is that I do not see the bark abstraction in the
watchdog_dev layer.
In the case I am investigating (the safety_monitor/safety_app) the bark is
outside of the "OS" view, it is an hardware action - like. shutdown.
Am I missing something? Thoughts?
-- Daniel
On 2/17/22 08:27, Daniel Bristot de Oliveira wrote:
> Hi Peter
>
> On 2/16/22 17:01, [email protected] wrote:
>> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>>> Add a set of tracepoints, enabling the observability of the watchdog
>>> device interactions with user-space.
>>>
>>> The events are:
>>> watchdog:watchdog_open
>>> watchdog:watchdog_close
>>> watchdog:watchdog_start
>>> watchdog:watchdog_stop
>>> watchdog:watchdog_set_timeout
>>> watchdog:watchdog_ping
>>> watchdog:watchdog_nowayout
>>> watchdog:watchdog_set_keep_alive
>>> watchdog:watchdog_keep_alive
>>
>> Some watchdogs have a bark functionality, I think it should be event for that too.
>>
>
> I understand. The problems is that I do not see the bark abstraction in the
> watchdog_dev layer.
>
I don't even know what "bark functionality" means. A new term for pretimeout ?
Something else ?
Guenter
> In the case I am investigating (the safety_monitor/safety_app) the bark is
> outside of the "OS" view, it is an hardware action - like. shutdown.
>
> Am I missing something? Thoughts?
>
> -- Daniel
On 2/17/22 19:17, Guenter Roeck wrote:
> On 2/17/22 09:49, Gabriele Paoloni wrote:
>>
>>
>> On 17/02/2022 18:27, Guenter Roeck wrote:
>>> On 2/17/22 08:27, Daniel Bristot de Oliveira wrote:
>>>> Hi Peter
>>>>
>>>> On 2/16/22 17:01, [email protected] wrote:
>>>>> On 2/14/22 11:45, Daniel Bristot de Oliveira wrote:
>>>>>> Add a set of tracepoints, enabling the observability of the watchdog
>>>>>> device interactions with user-space.
>>>>>>
>>>>>> The events are:
>>>>>> watchdog:watchdog_open
>>>>>> watchdog:watchdog_close
>>>>>> watchdog:watchdog_start
>>>>>> watchdog:watchdog_stop
>>>>>> watchdog:watchdog_set_timeout
>>>>>> watchdog:watchdog_ping
>>>>>> watchdog:watchdog_nowayout
>>>>>> watchdog:watchdog_set_keep_alive
>>>>>> watchdog:watchdog_keep_alive
>>>>>
>>>>> Some watchdogs have a bark functionality, I think it should be event
>>>>> for that too.
>>>>>
>>>>
>>>> I understand. The problems is that I do not see the bark abstraction
>>>> in the
>>>> watchdog_dev layer.
>>>>
>>>
>>> I don't even know what "bark functionality" means. A new term for
>>> pretimeout ?
>>> Something else ?
>>
>>> From my understanding the bark timeout is actually the pretimeout
>> whereas the bite timeout is the actual timeout.
>> I think in the Kernel ftwdt010_wdt and qcom-wdt are bark/bite WTDs
>>
>
> If that is the case, I would prefer if we could stick to existing
> terminology to avoid issues like "I do not see the bark abstraction".
I agree! I am using the terminology from watchdog dev. Like, I hear the term
"pet" for the "ping", I used "ping."
-- Daniel