linux-trace-devel.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
* [PATCH V4 00/20] The Runtime Verification (RV) interface
@ 2022-06-16  8:44 Daniel Bristot de Oliveira
  2022-06-16  8:44 ` [PATCH V4 01/20] rv: Add " Daniel Bristot de Oliveira
                   ` (21 more replies)
  0 siblings, 22 replies; 82+ messages in thread
From: Daniel Bristot de Oliveira @ 2022-06-16  8:44 UTC (permalink / raw)
  To: Steven Rostedt
  Cc: Daniel Bristot de Oliveira, Wim Van Sebroeck, Guenter Roeck,
	Jonathan Corbet, Ingo Molnar, Thomas Gleixner, Peter Zijlstra,
	Will Deacon, Catalin Marinas, Marco Elver, Dmitry Vyukov,
	Paul E. McKenney, Shuah Khan, Gabriele Paoloni, Juri Lelli,
	Clark Williams, linux-doc, linux-kernel, linux-trace-devel

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).

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 (trave/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;

Things kept for a second moment (after this patchset):
	- 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)
	- Export symbols for external modules
	- dot2bpf

Daniel Bristot de Oliveira (20):
  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
  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/safety_app: Add a safety_app sample
  Documentation/rv: Add watchdog-monitor documentation

 Documentation/trace/index.rst                 |   1 +
 .../trace/rv/da_monitor_instrumentation.rst   | 223 ++++++
 .../trace/rv/da_monitor_synthesis.rst         | 284 +++++++
 Documentation/trace/rv/index.rst              |   9 +
 .../trace/rv/runtime-verification.rst         | 233 ++++++
 Documentation/trace/rv/watchdog-monitor.rst   | 250 ++++++
 drivers/watchdog/watchdog_dev.c               |  43 +-
 drivers/watchdog/watchdog_pretimeout.c        |   2 +
 include/linux/rv.h                            |  38 +
 include/linux/sched.h                         |  11 +
 include/linux/watchdog.h                      |   7 +-
 include/rv/automata.h                         |  49 ++
 include/rv/da_monitor.h                       | 419 ++++++++++
 include/rv/instrumentation.h                  |  23 +
 include/rv/rv.h                               |  32 +
 include/trace/events/rv.h                     | 153 ++++
 include/trace/events/watchdog.h               | 101 +++
 kernel/fork.c                                 |  14 +
 kernel/trace/Kconfig                          |   2 +
 kernel/trace/Makefile                         |   2 +
 kernel/trace/rv/Kconfig                       |  84 ++
 kernel/trace/rv/Makefile                      |   9 +
 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c  | 300 +++++++
 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h  |  84 ++
 kernel/trace/rv/monitors/wip/wip.c            | 110 +++
 kernel/trace/rv/monitors/wip/wip.h            |  38 +
 kernel/trace/rv/monitors/wwnr/wwnr.c          | 109 +++
 kernel/trace/rv/monitors/wwnr/wwnr.h          |  38 +
 kernel/trace/rv/reactor_panic.c               |  44 +
 kernel/trace/rv/reactor_printk.c              |  43 +
 kernel/trace/rv/rv.c                          | 757 ++++++++++++++++++
 kernel/trace/rv/rv.h                          |  54 ++
 kernel/trace/rv/rv_reactors.c                 | 476 +++++++++++
 kernel/trace/trace.c                          |   4 +
 kernel/trace/trace.h                          |   2 +
 tools/verification/dot2/Makefile              |  26 +
 tools/verification/dot2/automata.py           | 179 +++++
 tools/verification/dot2/dot2c                 |  30 +
 tools/verification/dot2/dot2c.py              | 244 ++++++
 tools/verification/dot2/dot2k                 |  50 ++
 tools/verification/dot2/dot2k.py              | 177 ++++
 .../dot2/dot2k_templates/main_global.c        |  94 +++
 .../dot2/dot2k_templates/main_per_cpu.c       |  94 +++
 .../dot2/dot2k_templates/main_per_task.c      |  94 +++
 tools/verification/safety_app/Makefile        |  51 ++
 tools/verification/safety_app/safety_app.c    | 614 ++++++++++++++
 46 files changed, 5691 insertions(+), 10 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/instrumentation.h
 create mode 100644 include/rv/rv.h
 create mode 100644 include/trace/events/rv.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/monitors/safe_wtd/safe_wtd.c
 create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h
 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/safety_app/Makefile
 create mode 100644 tools/verification/safety_app/safety_app.c

-- 
2.35.1


^ permalink raw reply	[flat|nested] 82+ messages in thread

end of thread, other threads:[~2022-07-13 19:30 UTC | newest]

Thread overview: 82+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-06-16  8:44 [PATCH V4 00/20] The Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 01/20] rv: Add " Daniel Bristot de Oliveira
2022-06-23 17:21   ` Punit Agrawal
2022-07-01 13:24     ` Daniel Bristot de Oliveira
2022-06-23 20:26   ` Steven Rostedt
2022-07-04 19:49     ` Daniel Bristot de Oliveira
2022-07-06 17:49   ` Tao Zhou
2022-07-06 17:53     ` Matthew Wilcox
2022-07-08 15:36       ` Tao Zhou
2022-07-08 15:55         ` Matthew Wilcox
2022-07-08 14:39     ` Daniel Bristot de Oliveira
2022-07-10 15:11       ` Tao Zhou
2022-07-10 15:42         ` Steven Rostedt
2022-07-10 22:28           ` Tao Zhou
2022-06-16  8:44 ` [PATCH V4 02/20] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-06-23 20:40   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 03/20] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-06-28 17:48   ` Steven Rostedt
2022-07-06 18:35   ` Tao Zhou
2022-07-13 18:38     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 04/20] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-07-06 18:56   ` Tao Zhou
2022-07-13 18:39     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 05/20] rv/include: Add instrumentation helper functions Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 06/20] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-06-28 18:10   ` Steven Rostedt
2022-06-28 18:16   ` Steven Rostedt
2022-07-13 18:41     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 07/20] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 08/20] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-06-28 19:02   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 09/20] rv/monitor: wip instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-06-16 11:21   ` kernel test robot
2022-06-16 21:00   ` Randy Dunlap
2022-06-17 16:07     ` Daniel Bristot de Oliveira
2022-06-28 19:02     ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 10/20] rv/monitor: Add the wwnr monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-07-06 20:08   ` Tao Zhou
2022-06-16  8:44 ` [PATCH V4 11/20] rv/monitor: wwnr instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-06-16 13:47   ` kernel test robot
2022-06-28 19:05   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 12/20] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 13/20] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira
2022-06-16 15:20   ` kernel test robot
2022-06-16 21:03   ` Randy Dunlap
2022-06-17 16:09     ` Daniel Bristot de Oliveira
2022-07-13 18:47     ` Daniel Bristot de Oliveira
2022-06-28 19:06   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 14/20] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-06-29  3:35   ` Bagas Sanjaya
2022-07-13 19:30     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 15/20] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-06-28 19:09   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 16/20] Documentation/rv: Add deterministic automata instrumentation documentation Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 17/20] watchdog/dev: Add tracepoints Daniel Bristot de Oliveira
2022-06-16 13:44   ` Guenter Roeck
2022-06-16 15:47     ` Daniel Bristot de Oliveira
2022-06-16 23:55       ` Guenter Roeck
2022-06-17 16:16         ` Daniel Bristot de Oliveira
2022-07-13 18:49         ` Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 18/20] rv/monitor: Add safe watchdog monitor Daniel Bristot de Oliveira
2022-06-16 13:36   ` Guenter Roeck
2022-06-16 15:29     ` Daniel Bristot de Oliveira
     [not found]       ` <CA+wEVJbvcMZbCroO2_rdVxLvYkUo-ePxCwsp5vbDpoqys4HGWQ@mail.gmail.com>
2022-06-16 23:53         ` Guenter Roeck
2022-06-17 17:06           ` Daniel Bristot de Oliveira
2022-06-28 19:32           ` Steven Rostedt
2022-07-01 14:45             ` Guenter Roeck
2022-07-01 15:38               ` Steven Rostedt
2022-07-04 12:41                 ` Daniel Bristot de Oliveira
2022-06-16 20:57   ` Randy Dunlap
2022-06-17 16:17     ` Daniel Bristot de Oliveira
2022-07-13 19:13   ` Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 19/20] rv/safety_app: Add a safety_app sample Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 20/20] Documentation/rv: Add watchdog-monitor documentation Daniel Bristot de Oliveira
2022-07-07 12:41   ` Tao Zhou
2022-07-13 18:51     ` Daniel Bristot de Oliveira
2022-06-22  7:24 ` [PATCH V4 00/20] The Runtime Verification (RV) interface Song Liu
2022-06-23 16:41   ` Daniel Bristot de Oliveira
2022-06-23 17:52     ` Song Liu
2022-06-23 20:29       ` Daniel Bristot de Oliveira
2022-06-23 21:10         ` Song Liu
2022-07-06 16:18 ` Tao Zhou

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).