On Wed, 2025-04-30 at 13:02 +0200, Nam Cao wrote:

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.

Steve,

From my point of view this series is ready for inclusion, what do you
think?

We may still need Acks from the x86 and arm64 maintainers regarding the
tracepoints changes, though.

Thanks,
Gabriele

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.

v5->v6
https://lore.kernel.org/lkml/cover.1745926331.git.namcao@linutronix.de (local)
  - sleep monitor: Drop the block_on_rt_mutex tracepoints. The
contention
    tracepoints are sufficient.

v4->v5
https://lore.kernel.org/lkml/cover.1745390829.git.namcao@linutronix.de (local)
  - sleep monitor: Fix a false positive due to a race with waking and
    scheduling.
  - sleep monitor: Add block_on_rt_mutex tracepoints and use them for
    BLOCK_ON_RT_MUTEX, instead of trace_sched_pi_setprio
  - sleep monitor: tighten the rule on nanosleep: only
clock_nanosleep()
    with TIMER_ABSTIME and CLOCK_MONOTONIC is allowed
  - add comments explaining why it is correct to treat PI-boosted
tasks as
    real-time tasks.

    It should be noted that due to the changes in v5, 'perf' does not
work
    as well as before, because sometimes the errors happen out of the
    real-time tasks' contexts. Fixing this is left for future work.

    stress-ng is also far noisier in v5, because the rule on
nanosleep is
    tightened.

v3->v4
https://lore.kernel.org/lkml/cover.1744785335.git.namcao@linutronix.de (local)
  - support deadline tasks
  - rtapp_sleep: use sched_pi_setprio tracepoint instead of
contention
    tracepoints for BLOCK_ON_RT_MUTEX, so that proxy lock is covered.
  - fix the scripts generating an "slightly" incorrect verification
automaton
  - makes rtapp monitor depends on RV_PER_TASK_MONITORS >= 2
  - make the event tracepoint output a bit more readable
  - some documentation's format fixes

v2->v3
https://lore.kernel.org/lkml/cover.1744355018.git.namcao@linutronix.de/ (local)
  - 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/ (local)
  - 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