From: Daniel Bristot de Oliveira <bristot@kernel.org>
To: Steven Rostedt <rostedt@goodmis.org>
Cc: Daniel Bristot de Oliveira <bristot@kernel.org>,
Wim Van Sebroeck <wim@linux-watchdog.org>,
Guenter Roeck <linux@roeck-us.net>,
Jonathan Corbet <corbet@lwn.net>, Ingo Molnar <mingo@redhat.com>,
Thomas Gleixner <tglx@linutronix.de>,
Peter Zijlstra <peterz@infradead.org>,
Will Deacon <will@kernel.org>,
Catalin Marinas <catalin.marinas@arm.com>,
Marco Elver <elver@google.com>,
Dmitry Vyukov <dvyukov@google.com>,
"Paul E. McKenney" <paulmck@kernel.org>,
Shuah Khan <skhan@linuxfoundation.org>,
Gabriele Paoloni <gpaoloni@redhat.com>,
Juri Lelli <juri.lelli@redhat.com>,
Clark Williams <williams@redhat.com>,
Tao Zhou <tao.zhou@linux.dev>,
Randy Dunlap <rdunlap@infradead.org>,
linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org,
linux-trace-devel@vger.kernel.org
Subject: [PATCH V9 00/16] The Runtime Verification (RV) interface
Date: Fri, 29 Jul 2022 11:38:39 +0200 [thread overview]
Message-ID: <cover.1659052063.git.bristot@kernel.org> (raw)
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;
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).
Features to be added after this patchset:
- safe_wtd monitor (requires further discussion with watchdog maintainers)
- Export symbols for external modules
- dot2bpf
- Add a reactor that 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)
Changes from v8:
- Change the da_monitor curr state type from int to
unsigned int (Daniel)
- Fix a compilation problem because of the usage of a
function from patch 2 in patch 1 (last minute change)
(Tao).
Changes from v7:
- Optmize the check for monitor enabled (Tao)
- add lockdep checks on rv_enable/disable_monitor (Steven)
- Adjusted the "------" of documentation titles (Steven)
- Adjusted turn_monitoring_on(), and added a
turn_monitoring_on_with_reset() (Steven)
- Moved all tracepoint_synchronize_unregister() to run with
interface lock taken, and added a comment about it (Steven)
- lockdep, WARN, and call reactor_cleanup_monitor() (Steven)
- Improve comments on synchronization (Steven)
Changes from v6:
- Remove lock protection when reading static data (Steven)
- Add lock protection in disable_all_monitors() (Steven)
- Re-arrange enable_monitor (Steven/Tao)
- Fix monitor_desc_read_data() Description (Tao)
- Wait for tracepoint_synchronize_unregister() anytime a monitor
is Disabled (daniel)
- Add memory barriers around monitoring_on and reacting_on (Steven)
- Make rv reactor name and description const char * (Tao)
- Append missing _##name for some da_automata functions/variables (Steven)
- rv_unregister_monitor() will disable the monitor if necessary, and
take care of synchronization (Daniel)
- Fixed da_monitor_instrumentation.rst (Tao)
- Fix !CONFIG_Rv_REACTORS (kbuild test)
- Moved struct rv/rv.h to linux/rv.h (Daniel)
- Add rv_ prefix on get/put task slot (Daniel)
Changes from v5:
- Add task monitor slot checks (Daniel/Tao)
- Reset the monitors only after initializing the data (Daniel)
- Add static for static data (Daniel/0-day)
- Change start/stop *functions to enable/disable (like the user-
interface (Daniel)
- s/init/start/ for the functions starting the monitoring (Daniel)
- Access monitoring_on and reacting_on via functions (Daniel)
- Improved vector access checks (Tao)
- cleanups (Daniel/Tao)
Changes from v4:
- The watchdog monitor will be discussed on another thread (Daniel)
- s/safe/final/ in the tracepoint definition (Daniel)
- Improved error handling at __init functions (Daniel)
- Remove the hostname from example of commands in a shell (Bagas Sanjaya)
- Added documentation about automata representation in C/DOT/Formal
and this documentation is cited in a comment on all model.h
(Steven)
- Make wwnr a single patch (Daniel/Steven)
- Add the .dot file for each monitor (Daniel)
- Add a document for each monitor (Daniel)
- Add an order for documentation in the index.rst (Daniel)
- Add wip/wwnr/... long description (Steven/Randy)
- Add comments for helper functions (Steven)
- Improve checks in da_monitor.h (Tao Zhou)
- Change final states set to bool (Tao/Daniel)
- Adjust indentation on enabling monitor/reactor (Steven)
- Use strim on buffers from user-space (Steven)
- Remove ifdefs inside functions (Steven)
- Adjust depends on RV in Kconfig (Steven)
- Check empty enabled monitor list (Tao Zhou)
- Fixed Copyright (Steven)
- Adjusted structures' indentation (Steven)
- Fix rv/monitors/$monitor/enabled return value (Song Liu)
- Typos (Punit Agrawal/Randy)
- Improved python scripts w.r.t. consistency (Steve)
- Blamed myself for so many problems :-) (Daniel's mind)
Changes from v3:
- Rebased on 5.19
(rostedt's request were made on 1x1 meetings)
- Moved monitors to monitors/$name/ (Rostedt)
- Consolidate the tracepoints into a single include file in the default
directory (trace/events/rv.h) (Rostedt)
- The tracepoints now record the entire string to the buffer.
- Change the enable_monitors to disable monitors with ! (instead of -).
(Rostedt)
- Add a suffix to the state/events enums, to avoid conflict in the
vmlinux.h used by eBPF.
- The models are now placed in the $name.h (it used to store the
tracepoints, but they are now consolidated in a single file)
- dot2c and dot2k updated to the changes
- models re-generated with these new standards.
- user-space tools moved to an directory outside of tools/tracing as
other methods of verification/log sources are planned.
Changes from v2:
- Tons of checkpatch and kernel test robot
- Moved files to better places
- Adjusted watchdog tracepoints patch (Guenter Roeck)
- Added pretimeout watchdog events (Peter Enderborg)
- Used task struct to store per-task monitors (Peter Zijlstra)
- Changed the instrumentation to use internal definition of tracepoint
and check the callback signature (Steven Rostedt)
- Used printk_deferred() and removed the comment about deadlocks
(Shuah Khan/John Ogness)
- Some simplifications:
- Removed the safe watchdog nowayout for now (myself)
- Removed export symbols for now (myself)
Changes from V1:
- rebased to the latest kernel;
- code cleanup;
- the watchdog dev monitor;
- safety app;
Daniel Bristot de Oliveira (16):
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 instrumentation helper functions
Documentation/rv: Add a basic documentation
tools/rv: Add dot2c
Documentation/rv: Add deterministic automaton documentation
tools/rv: Add dot2k
Documentation/rv: Add deterministic automata monitor synthesis
documentation
Documentation/rv: Add deterministic automata instrumentation
documentation
rv/monitor: Add the wip monitor skeleton created by dot2k
rv/monitor: Add the wip monitor
rv/monitor: Add the wwnr monitor
rv/reactor: Add the printk reactor
rv/reactor: Add the panic reactor
Documentation/trace/index.rst | 1 +
.../trace/rv/da_monitor_instrumentation.rst | 171 ++++
.../trace/rv/da_monitor_synthesis.rst | 147 ++++
.../trace/rv/deterministic_automata.rst | 184 ++++
Documentation/trace/rv/index.rst | 14 +
Documentation/trace/rv/monitor_wip.rst | 55 ++
Documentation/trace/rv/monitor_wwnr.rst | 45 +
.../trace/rv/runtime-verification.rst | 231 +++++
include/linux/rv.h | 70 ++
include/linux/sched.h | 11 +
include/rv/automata.h | 75 ++
include/rv/da_monitor.h | 544 ++++++++++++
include/rv/instrumentation.h | 29 +
include/trace/events/rv.h | 142 ++++
kernel/fork.c | 14 +
kernel/trace/Kconfig | 2 +
kernel/trace/Makefile | 1 +
kernel/trace/rv/Kconfig | 78 ++
kernel/trace/rv/Makefile | 8 +
kernel/trace/rv/monitors/wip/wip.c | 88 ++
kernel/trace/rv/monitors/wip/wip.h | 46 +
kernel/trace/rv/monitors/wwnr/wwnr.c | 87 ++
kernel/trace/rv/monitors/wwnr/wwnr.h | 46 +
kernel/trace/rv/reactor_panic.c | 43 +
kernel/trace/rv/reactor_printk.c | 42 +
kernel/trace/rv/rv.c | 799 ++++++++++++++++++
kernel/trace/rv/rv.h | 68 ++
kernel/trace/rv/rv_reactors.c | 508 +++++++++++
kernel/trace/trace.c | 2 +
kernel/trace/trace.h | 9 +
tools/verification/dot2/Makefile | 26 +
tools/verification/dot2/automata.py | 174 ++++
tools/verification/dot2/dot2c | 26 +
tools/verification/dot2/dot2c.py | 254 ++++++
tools/verification/dot2/dot2k | 47 ++
tools/verification/dot2/dot2k.py | 177 ++++
.../dot2/dot2k_templates/main_global.c | 91 ++
.../dot2/dot2k_templates/main_per_cpu.c | 91 ++
.../dot2/dot2k_templates/main_per_task.c | 91 ++
tools/verification/models/wip.dot | 16 +
tools/verification/models/wwnr.dot | 16 +
41 files changed, 4569 insertions(+)
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/deterministic_automata.rst
create mode 100644 Documentation/trace/rv/index.rst
create mode 100644 Documentation/trace/rv/monitor_wip.rst
create mode 100644 Documentation/trace/rv/monitor_wwnr.rst
create mode 100644 Documentation/trace/rv/runtime-verification.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/instrumentation.h
create mode 100644 include/trace/events/rv.h
create mode 100644 kernel/trace/rv/Kconfig
create mode 100644 kernel/trace/rv/Makefile
create mode 100644 kernel/trace/rv/monitors/wip/wip.c
create mode 100644 kernel/trace/rv/monitors/wip/wip.h
create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
create mode 100644 kernel/trace/rv/monitors/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/verification/dot2/Makefile
create mode 100644 tools/verification/dot2/automata.py
create mode 100644 tools/verification/dot2/dot2c
create mode 100644 tools/verification/dot2/dot2c.py
create mode 100644 tools/verification/dot2/dot2k
create mode 100644 tools/verification/dot2/dot2k.py
create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c
create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c
create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c
create mode 100644 tools/verification/models/wip.dot
create mode 100644 tools/verification/models/wwnr.dot
--
2.35.1
next reply other threads:[~2022-07-29 9:39 UTC|newest]
Thread overview: 31+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-07-29 9:38 Daniel Bristot de Oliveira [this message]
2022-07-29 9:38 ` [PATCH V9 01/16] rv: Add Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-07-30 14:08 ` Tao Zhou
2022-07-30 17:01 ` Steven Rostedt
2022-07-30 22:05 ` Tao Zhou
2022-07-30 18:07 ` Daniel Bristot de Oliveira
2022-07-31 15:06 ` Tao Zhou
2022-07-31 15:56 ` Daniel Bristot de Oliveira
2022-07-31 16:48 ` Steven Rostedt
2022-07-31 16:47 ` Steven Rostedt
2022-07-31 17:01 ` Steven Rostedt
2022-07-31 17:49 ` Daniel Bristot de Oliveira
2022-07-31 17:53 ` Steven Rostedt
2022-07-29 9:38 ` [PATCH V9 02/16] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 03/16] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-07-31 15:13 ` Tao Zhou
2022-07-31 16:02 ` Daniel Bristot de Oliveira
2022-07-31 18:17 ` Tao Zhou
2022-07-29 9:38 ` [PATCH V9 04/16] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 05/16] rv/include: Add instrumentation helper functions Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 06/16] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 07/16] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 08/16] Documentation/rv: Add deterministic automaton documentation Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 09/16] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 10/16] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 11/16] Documentation/rv: Add deterministic automata instrumentation documentation Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 12/16] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 13/16] rv/monitor: Add the wip monitor Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 14/16] rv/monitor: Add the wwnr monitor Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 15/16] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-07-29 9:38 ` [PATCH V9 16/16] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=cover.1659052063.git.bristot@kernel.org \
--to=bristot@kernel.org \
--cc=catalin.marinas@arm.com \
--cc=corbet@lwn.net \
--cc=dvyukov@google.com \
--cc=elver@google.com \
--cc=gpaoloni@redhat.com \
--cc=juri.lelli@redhat.com \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-trace-devel@vger.kernel.org \
--cc=linux@roeck-us.net \
--cc=mingo@redhat.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=rdunlap@infradead.org \
--cc=rostedt@goodmis.org \
--cc=skhan@linuxfoundation.org \
--cc=tao.zhou@linux.dev \
--cc=tglx@linutronix.de \
--cc=will@kernel.org \
--cc=williams@redhat.com \
--cc=wim@linux-watchdog.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.