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

[Nam Cao]

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 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 (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

-- 
2.39.5