mbox series

[00/10] RV: Linear temporal logic monitors for RT application

Message ID cover.1741708239.git.namcao@linutronix.de (mailing list archive)
Headers show
Series RV: Linear temporal logic monitors for RT application | expand

Message

Nam Cao March 11, 2025, 5:05 p.m. UTC 
Realtime applications often 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.

This series adds runtime verification monitors to detect these flaws.

This monitors was tried on pipewire and detected some issues. One of them
has been reported to pipewire's maintainers and is being fixed:
https://gitlab.freedesktop.org/pipewire/pipewire/-/merge_requests/2285

Patch 1 and patch 2 fix some minor issues with RV.

Patch 3 adds the infrastructure for linear temporal logic monitor.

Patch 4 adds the first monitor: rtapp_block. This monitor detects if a
realtime task is undesirable blocked.

Patch 5-8 prepare the pagefault tracepoints, so that patch 9 can add the
rtapp_pagefault monitor.  This monitor task detects if an RT task raise
page fault.

Patch 10 raises the max number of per-task monitor to 2, so that the above
monitors can be enabled simultaneously.
---
Cc: Petr Mladek <pmladek@suse.com>
Cc: John Ogness <john.ogness@linutronix.de>
Cc: Sergey Senozhatsky <senozhatsky@chromium.org>
Cc: Ingo Molnar <mingo@redhat.com>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Waiman Long <longman@redhat.com>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Borislav Petkov <bp@alien8.de>
Cc: Dave Hansen <dave.hansen@linux.intel.com>
Cc: x86@kernel.org
Cc: H. Peter Anvin <hpa@zytor.com>
Cc: Andy Lutomirski <luto@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Catalin Marinas <catalin.marinas@arm.com>
Cc: linux-arm-kernel@lists.infradead.org
Cc: Paul Walmsley <paul.walmsley@sifive.com>
Cc: Palmer Dabbelt <palmer@dabbelt.com>
Cc: Albert Ou <aou@eecs.berkeley.edu>
Cc: Alexandre Ghiti <alex@ghiti.fr>
Cc: linux-riscv@lists.infradead.org
---
Nam Cao (10):
  rv: Add #undef TRACE_INCLUDE_FILE
  rv: Let the reactors take care of buffers
  rv: Add infrastructure for linear temporal logic monitor
  rv: Add rtapp_block 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: raise the number of per-task monitor to 2

 .../trace/rv/linear_temporal_logic.rst        |  73 +++
 .../trace/rv/monitor_rtapp_block.rst          |  34 ++
 .../trace/rv/monitor_rtapp_pagefault.rst      |  36 ++
 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/tracepoint.c                  |  21 -
 arch/x86/mm/fault.c                           |   5 +-
 include/linux/printk.h                        |   1 +
 include/linux/rv.h                            |  39 +-
 include/rv/da_monitor.h                       |  61 +-
 .../trace/events}/exceptions.h                |  27 +-
 include/trace/events/lock.h                   |  12 +
 kernel/fork.c                                 |   5 +-
 kernel/locking/rtmutex.c                      |   4 +
 kernel/printk/internal.h                      |   1 -
 kernel/trace/rv/Kconfig                       |  20 +-
 kernel/trace/rv/Makefile                      |   4 +
 kernel/trace/rv/monitors/rtapp_block/ba.c     | 146 +++++
 kernel/trace/rv/monitors/rtapp_block/ba.h     | 166 ++++++
 kernel/trace/rv/monitors/rtapp_block/ltl      |   9 +
 .../rv/monitors/rtapp_block/rtapp_block.c     | 232 ++++++++
 kernel/trace/rv/monitors/rtapp_pagefault/ba.c | 139 +++++
 kernel/trace/rv/monitors/rtapp_pagefault/ba.h | 158 +++++
 kernel/trace/rv/monitors/rtapp_pagefault/ltl  |   1 +
 .../rtapp_pagefault/rtapp_pagefault.c         |  84 +++
 kernel/trace/rv/reactor_panic.c               |   7 +-
 kernel/trace/rv/reactor_printk.c              |   8 +-
 kernel/trace/rv/rv_reactors.c                 |   2 +-
 kernel/trace/rv/rv_trace.h                    |  67 ++-
 lib/Kconfig.debug                             |   3 +
 tools/verification/ltl2ba/.gitignore          |   3 +
 tools/verification/ltl2ba/generate.py         | 154 +++++
 tools/verification/ltl2ba/ltl.py              | 556 ++++++++++++++++++
 tools/verification/ltl2ba/template.c          | 131 +++++
 tools/verification/ltl2ba/template.h          | 157 +++++
 37 files changed, 2262 insertions(+), 133 deletions(-)
 create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
 create mode 100644 Documentation/trace/rv/monitor_rtapp_block.rst
 create mode 100644 Documentation/trace/rv/monitor_rtapp_pagefault.rst
 delete mode 100644 arch/x86/include/asm/trace/common.h
 delete mode 100644 arch/x86/kernel/tracepoint.c
 rename {arch/x86/include/asm/trace => include/trace/events}/exceptions.h (55%)
 create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.c
 create mode 100644 kernel/trace/rv/monitors/rtapp_block/ba.h
 create mode 100644 kernel/trace/rv/monitors/rtapp_block/ltl
 create mode 100644 kernel/trace/rv/monitors/rtapp_block/rtapp_block.c
 create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ba.c
 create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ba.h
 create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/ltl
 create mode 100644 kernel/trace/rv/monitors/rtapp_pagefault/rtapp_pagefault.c
 create mode 100644 tools/verification/ltl2ba/.gitignore
 create mode 100755 tools/verification/ltl2ba/generate.py
 create mode 100644 tools/verification/ltl2ba/ltl.py
 create mode 100644 tools/verification/ltl2ba/template.c
 create mode 100644 tools/verification/ltl2ba/template.h