[PATCH v3 00/22] RV: Linear temporal logic monitors for RT application
Nam Cao
namcao at linutronix.de
Tue Apr 15 23:51:06 PDT 2025
Real-time applications may have design flaws causing them to have
unexpected latency. For example, the applications may raise page faults, or
may be blocked trying to take a mutex without priority inheritance.
However, while attempting to implement DA monitors for these real-time
rules, deterministic automaton is found to be inappropriate as the
specification language. The automaton is complicated, hard to understand,
and error-prone.
For these cases, linear temporal logic is found to be more suitable. The
LTL is more concise and intuitive.
This series adds support for LTL RV monitor, and use it to implement two
monitors for reporting problems with real-time tasks.
Patch 1-12 cleanup and prepare the RV code for the integration of LTL
monitors.
Patch 13 adds support for LTL monitors.
Patch 14 adds the container monitor "rtapp". This encapsulates the
sub-monitors for real-time.
Patch 15-18 prepares the pagefault tracepoints, so that patch 19 can add
the monitor which watches real-time tasks doing page faults.
Patch 20 adds the "sleep" monitor: it detects potential undesirable latency
with real-time threads.
Patch 21 adds documentation on the new monitors.
Patch 22 allows the number of per-task monitors to be configurable, so that
the two new monitors can be enabled simultaneously.
v2->v3 https://lore.kernel.org/lkml/cover.1744355018.git.namcao@linutronix.de/
- fix a problem with sleep monitor's specification (around
KTHREAD_SHOULD_STOP)
- merge the patches that move the dot2k/rvgen scripts around
- pull panic/printk changes into separate patches
- fixup some build errors
- fixup monitor's init function return code
- fix some flake8 warnings with the scripts
- add some references to LTL documentation
- fixup some mistakes with rtapp documentation
- fixup capitalization mistake with monitor_synthesis.rst
- remove the now-redundant macro RV_PER_TASK_MONITORS
v1->v2 https://lore.kernel.org/lkml/cover.1741708239.git.namcao@linutronix.de/
- Integrate the LTL scripts into the existing dot2k tool, taking
advantage of the existing monitor generation scripts.
- Switch the struct ltl_monitor to use bitmap instead of an array, to
optimize memory usage.
- Correct the generated code to be non-deterministic state machine,
instead of deterministic state machine
- Put common code for all LTL monitors into a single file
(include/rv/ltl_monitor.h), reducing code duplication
- Change the LTL monitors to make user of container. Add a bug fix to
container while at it.
- Make the number of per-task monitor configurable
Cc: Petr Mladek <pmladek at suse.com>
Cc: John Ogness <john.ogness at linutronix.de>
Cc: Sergey Senozhatsky <senozhatsky at chromium.org>
Cc: Ingo Molnar <mingo at redhat.com>
Cc: Boqun Feng <boqun.feng at gmail.com>
Cc: Waiman Long <longman at redhat.com>
Cc: Thomas Gleixner <tglx at linutronix.de>
Cc: Borislav Petkov <bp at alien8.de>
Cc: Dave Hansen <dave.hansen at linux.intel.com>
Cc: x86 at kernel.org
Cc: H. Peter Anvin <hpa at zytor.com>
Cc: Andy Lutomirski <luto at kernel.org>
Cc: Peter Zijlstra <peterz at infradead.org>
Cc: Catalin Marinas <catalin.marinas at arm.com>
Cc: linux-arm-kernel at lists.infradead.org
Cc: Paul Walmsley <paul.walmsley at sifive.com>
Cc: Palmer Dabbelt <palmer at dabbelt.com>
Cc: Albert Ou <aou at eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex at ghiti.fr>
Cc: linux-riscv at lists.infradead.org
Nam Cao (22):
rv: Add #undef TRACE_INCLUDE_FILE
printk: Make vprintk_deferred() public
panic: Add vpanic()
rv: Let the reactors take care of buffers
verification/dot2k: Make a separate dot2k_templates/Kconfig_container
verification/dot2k: Remove __buff_to_string()
verification/dot2k: Replace is_container() hack with subparsers
rv: rename CONFIG_DA_MON_EVENTS to CONFIG_RV_MON_EVENTS
verification/dot2k: Prepare the frontend for LTL inclusion
Documentation/rv: Prepare monitor synthesis document for LTL inclusion
verification/rvgen: Restructure the templates files
verification/rvgen: Restructure the classes to prepare for LTL
inclusion
rv: Add support for LTL monitors
rv: Add rtapp container monitor
x86/tracing: Remove redundant trace_pagefault_key
x86/tracing: Move page fault trace points to generic
arm64: mm: Add page fault trace points
riscv: mm: Add page fault trace points
rv: Add rtapp_pagefault monitor
rv: Add rtapp_sleep monitor
rv: Add documentation for rtapp monitor
rv: Allow to configure the number of per-task monitor
.../trace/rv/da_monitor_synthesis.rst | 147 -----
Documentation/trace/rv/index.rst | 3 +-
.../trace/rv/linear_temporal_logic.rst | 119 ++++
Documentation/trace/rv/monitor_rtapp.rst | 107 ++++
Documentation/trace/rv/monitor_synthesis.rst | 256 ++++++++
arch/arm64/mm/fault.c | 8 +
arch/riscv/mm/fault.c | 8 +
arch/x86/include/asm/trace/common.h | 12 -
arch/x86/include/asm/trace/irq_vectors.h | 1 -
arch/x86/kernel/Makefile | 1 -
arch/x86/kernel/tracepoint.c | 21 -
arch/x86/mm/fault.c | 5 +-
include/linux/panic.h | 3 +
include/linux/printk.h | 5 +
include/linux/rv.h | 74 ++-
include/linux/sched.h | 8 +-
include/rv/da_monitor.h | 45 +-
include/rv/ltl_monitor.h | 184 ++++++
.../trace/events}/exceptions.h | 27 +-
kernel/fork.c | 5 +-
kernel/panic.c | 17 +-
kernel/printk/internal.h | 1 -
kernel/trace/rv/Kconfig | 27 +-
kernel/trace/rv/Makefile | 3 +
kernel/trace/rv/monitors/pagefault/Kconfig | 11 +
.../trace/rv/monitors/pagefault/pagefault.c | 80 +++
.../trace/rv/monitors/pagefault/pagefault.h | 57 ++
.../rv/monitors/pagefault/pagefault_trace.h | 14 +
kernel/trace/rv/monitors/rtapp/Kconfig | 6 +
kernel/trace/rv/monitors/rtapp/rtapp.c | 34 ++
kernel/trace/rv/monitors/rtapp/rtapp.h | 3 +
kernel/trace/rv/monitors/sleep/Kconfig | 13 +
kernel/trace/rv/monitors/sleep/sleep.c | 216 +++++++
kernel/trace/rv/monitors/sleep/sleep.h | 293 +++++++++
kernel/trace/rv/monitors/sleep/sleep_trace.h | 14 +
kernel/trace/rv/reactor_panic.c | 8 +-
kernel/trace/rv/reactor_printk.c | 8 +-
kernel/trace/rv/rv.c | 10 +-
kernel/trace/rv/rv_reactors.c | 2 +-
kernel/trace/rv/rv_trace.h | 52 +-
tools/verification/dot2/Makefile | 26 -
tools/verification/dot2/dot2k | 53 --
tools/verification/models/rtapp/pagefault.ltl | 1 +
tools/verification/models/rtapp/sleep.ltl | 15 +
tools/verification/rvgen/.gitignore | 3 +
tools/verification/rvgen/Makefile | 27 +
tools/verification/rvgen/__main__.py | 67 +++
tools/verification/{dot2 => rvgen}/dot2c | 2 +-
.../{dot2 => rvgen/rvgen}/automata.py | 0
tools/verification/rvgen/rvgen/container.py | 22 +
.../{dot2 => rvgen/rvgen}/dot2c.py | 2 +-
tools/verification/rvgen/rvgen/dot2k.py | 129 ++++
.../dot2k.py => rvgen/rvgen/generator.py} | 249 ++------
tools/verification/rvgen/rvgen/ltl2ba.py | 558 ++++++++++++++++++
tools/verification/rvgen/rvgen/ltl2k.py | 242 ++++++++
.../rvgen/templates}/Kconfig | 0
.../rvgen/rvgen/templates/container/Kconfig | 5 +
.../rvgen/templates/container/main.c} | 0
.../rvgen/templates/container/main.h} | 0
.../rvgen/templates/dot2k}/main.c | 0
.../rvgen/templates/dot2k}/trace.h | 0
.../rvgen/rvgen/templates/ltl2k/main.c | 102 ++++
.../rvgen/rvgen/templates/ltl2k/trace.h | 14 +
63 files changed, 2875 insertions(+), 550 deletions(-)
delete mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
create mode 100644 Documentation/trace/rv/monitor_rtapp.rst
create mode 100644 Documentation/trace/rv/monitor_synthesis.rst
delete mode 100644 arch/x86/include/asm/trace/common.h
delete mode 100644 arch/x86/kernel/tracepoint.c
create mode 100644 include/rv/ltl_monitor.h
rename {arch/x86/include/asm/trace => include/trace/events}/exceptions.h (55%)
create mode 100644 kernel/trace/rv/monitors/pagefault/Kconfig
create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.c
create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault.h
create mode 100644 kernel/trace/rv/monitors/pagefault/pagefault_trace.h
create mode 100644 kernel/trace/rv/monitors/rtapp/Kconfig
create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.c
create mode 100644 kernel/trace/rv/monitors/rtapp/rtapp.h
create mode 100644 kernel/trace/rv/monitors/sleep/Kconfig
create mode 100644 kernel/trace/rv/monitors/sleep/sleep.c
create mode 100644 kernel/trace/rv/monitors/sleep/sleep.h
create mode 100644 kernel/trace/rv/monitors/sleep/sleep_trace.h
delete mode 100644 tools/verification/dot2/Makefile
delete mode 100644 tools/verification/dot2/dot2k
create mode 100644 tools/verification/models/rtapp/pagefault.ltl
create mode 100644 tools/verification/models/rtapp/sleep.ltl
create mode 100644 tools/verification/rvgen/.gitignore
create mode 100644 tools/verification/rvgen/Makefile
create mode 100644 tools/verification/rvgen/__main__.py
rename tools/verification/{dot2 => rvgen}/dot2c (97%)
rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%)
create mode 100644 tools/verification/rvgen/rvgen/container.py
rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%)
create mode 100644 tools/verification/rvgen/rvgen/dot2k.py
rename tools/verification/{dot2/dot2k.py => rvgen/rvgen/generator.py} (52%)
create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py
create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py
rename tools/verification/{dot2/dot2k_templates => rvgen/rvgen/templates}/Kconfig (100%)
create mode 100644 tools/verification/rvgen/rvgen/templates/container/Kconfig
rename tools/verification/{dot2/dot2k_templates/main_container.c => rvgen/rvgen/templates/container/main.c} (100%)
rename tools/verification/{dot2/dot2k_templates/main_container.h => rvgen/rvgen/templates/container/main.h} (100%)
rename tools/verification/{dot2/dot2k_templates => rvgen/rvgen/templates/dot2k}/main.c (100%)
rename tools/verification/{dot2/dot2k_templates => rvgen/rvgen/templates/dot2k}/trace.h (100%)
create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/main.c
create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/trace.h
--
2.39.5
More information about the linux-arm-kernel
mailing list