diff options
| author | Linus Torvalds <torvalds@linux-foundation.org> | 2025-07-30 16:23:12 -0700 |
|---|---|---|
| committer | Linus Torvalds <torvalds@linux-foundation.org> | 2025-07-30 16:23:12 -0700 |
| commit | 4ff261e725d7376c12e745fdbe8a33cd6dbd5a83 (patch) | |
| tree | 20ea818ed1425630b9fc7c0de0adac7497fb9de5 | |
| parent | d50b07d05ca53fdb6c6d1581b9084c09d4e98f54 (diff) | |
| parent | 614384533dfe99293a7ff1bce3d4389adadbb759 (diff) | |
Merge tag 'trace-rv-6.17' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace
Pull runtime verification updates from Steven Rostedt:
- Added Linear temporal logic monitors for RT application
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.
- Make printk_deferred() public
The new monitors needed access to printk_deferred(). Make them
visible for the entire kernel.
- Add a vpanic() to allow for va_list to be passed to panic.
- Add rtapp container monitor.
A collection of monitors that check for common problems with
real-time applications that cause unexpected latency.
- Add page fault tracepoints to risc-v
These tracepoints are necessary to for the RV monitor to run on
risc-v.
- Fix the behaviour of the rv tool with -s and idle tasks.
- Allow the rv tool to gracefully terminate with SIGTERM
- Adjusts dot2c not to create lines over 100 columns
- Properly order nested monitors in the RV Kconfig file
- Return the registration error in all DA monitor instead of 0
- Update and add new sched collection monitors
Replace tss and sncid monitors with more complete sts:
Not only prove that switches occur in scheduling context and scheduling
needs interrupt disabled but also that each call to the scheduler
disables interrupts to (optionally) switch.
New monitor: nrp
Preemption requires need resched which is cleared by any switch
(includes a non optimal workaround for /nested/ preemptions)
New monitor: sssw
suspension requires setting the task to sleepable and, after the
switch occurs, the task requires a wakeup to come back to runnable
New monitor: opid
waking and need-resched operations occur with interrupts and
preemption disabled or in IRQ without explicitly disabling
preemption"
* tag 'trace-rv-6.17' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: (48 commits)
rv: Add opid per-cpu monitor
rv: Add nrp and sssw per-task monitors
rv: Replace tss and sncid monitors with more complete sts
sched: Adapt sched tracepoints for RV task model
rv: Retry when da monitor detects race conditions
rv: Adjust monitor dependencies
rv: Use strings in da monitors tracepoints
rv: Remove trailing whitespace from tracepoint string
rv: Add da_handle_start_run_event_ to per-task monitors
rv: Fix wrong type cast in reactors_show() and monitor_reactor_show()
rv: Fix wrong type cast in monitors_show()
rv: Remove struct rv_monitor::reacting
rv: Remove rv_reactor's reference counter
rv: Merge struct rv_reactor_def into struct rv_reactor
rv: Merge struct rv_monitor_def into struct rv_monitor
rv: Remove unused field in struct rv_monitor_def
rv: Return init error when registering monitors
verification/rvgen: Organise Kconfig entries for nested monitors
tools/dot2c: Fix generated files going over 100 column limit
tools/rv: Stop gracefully also on SIGTERM
...
101 files changed, 4860 insertions, 1265 deletions
diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/da_monitor_synthesis.rst deleted file mode 100644 index 0a92729c8a9b..000000000000 --- a/Documentation/trace/rv/da_monitor_synthesis.rst +++ /dev/null @@ -1,147 +0,0 @@ -Deterministic Automata Monitor Synthesis -======================================== - -The starting point for the application of runtime verification (RV) techniques -is the *specification* or *modeling* of the desired (or undesired) behavior -of the system under scrutiny. - -The formal representation needs to be then *synthesized* into a *monitor* -that can then be used in the analysis of the trace of the system. The -*monitor* connects to the system via an *instrumentation* that converts -the events from the *system* to the events of the *specification*. - - -In Linux terms, the runtime verification monitors are encapsulated inside -the *RV monitor* abstraction. The RV monitor includes a set of instances -of the monitor (per-cpu monitor, per-task monitor, and so on), the helper -functions that glue the monitor to the system reference model, and the -trace output as a reaction to event parsing and exceptions, as depicted -below:: - - Linux +----- RV Monitor ----------------------------------+ Formal - Realm | | Realm - +-------------------+ +----------------+ +-----------------+ - | Linux kernel | | Monitor | | Reference | - | Tracing | -> | Instance(s) | <- | Model | - | (instrumentation) | | (verification) | | (specification) | - +-------------------+ +----------------+ +-----------------+ - | | | - | V | - | +----------+ | - | | Reaction | | - | +--+--+--+-+ | - | | | | | - | | | +-> trace output ? | - +------------------------|--|----------------------+ - | +----> panic ? - +-------> <user-specified> - -DA monitor synthesis --------------------- - -The synthesis of automata-based models into the Linux *RV monitor* abstraction -is automated by the dot2k tool and the rv/da_monitor.h header file that -contains a set of macros that automatically generate the monitor's code. - -dot2k ------ - -The dot2k utility leverages dot2c by converting an automaton model in -the DOT format into the C representation [1] and creating the skeleton of -a kernel monitor in C. - -For example, it is possible to transform the wip.dot model present in -[1] into a per-cpu monitor with the following command:: - - $ dot2k -d wip.dot -t per_cpu - -This will create a directory named wip/ with the following files: - -- wip.h: the wip model in C -- wip.c: the RV monitor - -The wip.c file contains the monitor declaration and the starting point for -the system instrumentation. - -Monitor macros --------------- - -The rv/da_monitor.h enables automatic code generation for the *Monitor -Instance(s)* using C macros. - -The benefits of the usage of macro for monitor synthesis are 3-fold as it: - -- Reduces the code duplication; -- Facilitates the bug fix/improvement; -- Avoids the case of developers changing the core of the monitor code - to manipulate the model in a (let's say) non-standard way. - -This initial implementation presents three different types of monitor instances: - -- ``#define DECLARE_DA_MON_GLOBAL(name, type)`` -- ``#define DECLARE_DA_MON_PER_CPU(name, type)`` -- ``#define DECLARE_DA_MON_PER_TASK(name, type)`` - -The first declares the functions for a global deterministic automata monitor, -the second for monitors with per-cpu instances, and the third with per-task -instances. - -In all cases, the 'name' argument is a string that identifies the monitor, and -the 'type' argument is the data type used by dot2k on the representation of -the model in C. - -For example, the wip model with two states and three events can be -stored in an 'unsigned char' type. Considering that the preemption control -is a per-cpu behavior, the monitor declaration in the 'wip.c' file is:: - - DECLARE_DA_MON_PER_CPU(wip, unsigned char); - -The monitor is executed by sending events to be processed via the functions -presented below:: - - da_handle_event_$(MONITOR_NAME)($(event from event enum)); - da_handle_start_event_$(MONITOR_NAME)($(event from event enum)); - da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum)); - -The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where -the event will be processed if the monitor is processing events. - -When a monitor is enabled, it is placed in the initial state of the automata. -However, the monitor does not know if the system is in the *initial state*. - -The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the -monitor that the system is returning to the initial state, so the monitor can -start monitoring the next event. - -The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify -the monitor that the system is known to be in the initial state, so the -monitor can start monitoring and monitor the current event. - -Using the wip model as example, the events "preempt_disable" and -"sched_waking" should be sent to monitor, respectively, via [2]:: - - da_handle_event_wip(preempt_disable_wip); - da_handle_event_wip(sched_waking_wip); - -While the event "preempt_enabled" will use:: - - da_handle_start_event_wip(preempt_enable_wip); - -To notify the monitor that the system will be returning to the initial state, -so the system and the monitor should be in sync. - -Final remarks -------------- - -With the monitor synthesis in place using the rv/da_monitor.h and -dot2k, the developer's work should be limited to the instrumentation -of the system, increasing the confidence in the overall approach. - -[1] For details about deterministic automata format and the translation -from one representation to another, see:: - - Documentation/trace/rv/deterministic_automata.rst - -[2] dot2k appends the monitor's name suffix to the events enums to -avoid conflicting variables when exporting the global vmlinux.h -use by BPF programs. diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst index e80e0057feb4..a2812ac5cfeb 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -8,8 +8,10 @@ Runtime Verification runtime-verification.rst deterministic_automata.rst - da_monitor_synthesis.rst + linear_temporal_logic.rst + monitor_synthesis.rst da_monitor_instrumentation.rst monitor_wip.rst monitor_wwnr.rst monitor_sched.rst + monitor_rtapp.rst diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst new file mode 100644 index 000000000000..9eee09d9cacf --- /dev/null +++ b/Documentation/trace/rv/linear_temporal_logic.rst @@ -0,0 +1,134 @@ +Linear temporal logic +===================== + +Introduction +------------ + +Runtime verification monitor is a verification technique which checks that the +kernel follows a specification. It does so by using tracepoints to monitor the +kernel's execution trace, and verifying that the execution trace sastifies the +specification. + +Initially, the specification can only be written in the form of deterministic +automaton (DA). However, while attempting to implement DA monitors for some +complex specifications, deterministic automaton is found to be inappropriate as +the specification language. The automaton is complicated, hard to understand, +and error-prone. + +Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type +of monitor uses LTL as specification instead of DA. For some cases, writing the +specification as LTL is more concise and intuitive. + +Many materials explain LTL in details. One book is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT + Press, 2008. + +Grammar +------- + +Unlike some existing syntax, kernel's implementation of LTL is more verbose. +This is motivated by considering that the people who read the LTL specifications +may not be well-versed in LTL. + +Grammar: + ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl + +Operands (opd): + true, false, user-defined names consisting of upper-case characters, digits, + and underscore. + +Unary Operators (unop): + always + eventually + next + not + +Binary Operators (binop): + until + and + or + imply + equivalent + +This grammar is ambiguous: operator precedence is not defined. Parentheses must +be used. + +Example linear temporal logic +----------------------------- +.. code-block:: + + RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA) + +means: if it is raining, going outside means having an umbrella. + +.. code-block:: + + RAIN imply (WET until not RAIN) + +means: if it is raining, it is going to be wet until the rain stops. + +.. code-block:: + + RAIN imply eventually not RAIN + +means: if it is raining, rain will eventually stop. + +The above examples are referring to the current time instance only. For kernel +verification, the `always` operator is usually desirable, to specify that +something is always true at the present and for all future. For example:: + + always (RAIN imply eventually not RAIN) + +means: *all* rain eventually stops. + +In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the +"atomic propositions". + +Monitor synthesis +----------------- + +To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used: +`tools/verification/rvgen`. The specification needs to be provided as a file, +and it must have a "RULE = LTL" assignment. For example:: + + RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE)) + +which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or +`CRASHED`. + +The LTL can be broken down using sub-expressions. The above is equivalent to: + + .. code-block:: + + RULE = always (ACQUIRE imply (ALIVE until RELEASE)) + ALIVE = not KILLED and not CRASHED + +From this specification, `rvgen` generates the C implementation of a Buchi +automaton - a non-deterministic state machine which checks the satisfiability of +the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using +`rvgen`. + +References +---------- + +One book covering model checking and linear temporal logic is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT + Press, 2008. + +For an example of using linear temporal logic in software testing, see:: + + Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury. + 2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the + 44th International Conference on Software Engineering (ICSE '22). Association + for Computing Machinery, New York, NY, USA, 1343–1355. + https://doi.org/10.1145/3510003.3510082 + +The kernel's LTL monitor implementation is based on:: + + Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly + Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa, + M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP + Advances in Information and Communication Technology. Springer, Boston, MA. + https://doi.org/10.1007/978-0-387-34892-6_1 diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst new file mode 100644 index 000000000000..c8104eda924a --- /dev/null +++ b/Documentation/trace/rv/monitor_rtapp.rst @@ -0,0 +1,133 @@ +Real-time application monitors +============================== + +- Name: rtapp +- Type: container for multiple monitors +- Author: Nam Cao <namcao@linutronix.de> + +Description +----------- + +Real-time applications may have design flaws such that they experience +unexpected latency and fail to meet their time requirements. Often, these flaws +follow a few patterns: + + - Page faults: A real-time thread may access memory that does not have a + mapped physical backing or must first be copied (such as for copy-on-write). + Thus a page fault is raised and the kernel must first perform the expensive + action. This causes significant delays to the real-time thread + - Priority inversion: A real-time thread blocks waiting for a lower-priority + thread. This causes the real-time thread to effectively take on the + scheduling priority of the lower-priority thread. For example, the real-time + thread needs to access a shared resource that is protected by a + non-pi-mutex, but the mutex is currently owned by a non-real-time thread. + +The `rtapp` monitor detects these patterns. It aids developers to identify +reasons for unexpected latency with real-time applications. It is a container of +multiple sub-monitors described in the following sections. + +Monitor pagefault ++++++++++++++++++ + +The `pagefault` monitor reports real-time tasks raising page faults. Its +specification is:: + + RULE = always (RT imply not PAGEFAULT) + +To fix warnings reported by this monitor, `mlockall()` or `mlock()` can be used +to ensure physical backing for memory. + +This monitor may have false negatives because the pages used by the real-time +threads may just happen to be directly available during testing. To minimize +this, the system can be put under memory pressure (e.g. invoking the OOM killer +using a program that does `ptr = malloc(SIZE_OF_RAM); memset(ptr, 0, +SIZE_OF_RAM);`) so that the kernel executes aggressive strategies to recycle as +much physical memory as possible. + +Monitor sleep ++++++++++++++ + +The `sleep` monitor reports real-time threads sleeping in a manner that may +cause undesirable latency. Real-time applications should only put a real-time +thread to sleep for one of the following reasons: + + - Cyclic work: real-time thread sleeps waiting for the next cycle. For this + case, only the `clock_nanosleep` syscall should be used with `TIMER_ABSTIME` + (to avoid time drift) and `CLOCK_MONOTONIC` (to avoid the clock being + changed). No other method is safe for real-time. For example, threads + waiting for timerfd can be woken by softirq which provides no real-time + guarantee. + - Real-time thread waiting for something to happen (e.g. another thread + releasing shared resources, or a completion signal from another thread). In + this case, only futexes (FUTEX_LOCK_PI, FUTEX_LOCK_PI2 or one of + FUTEX_WAIT_*) should be used. Applications usually do not use futexes + directly, but use PI mutexes and PI condition variables which are built on + top of futexes. Be aware that the C library might not implement conditional + variables as safe for real-time. As an alternative, the librtpi library + exists to provide a conditional variable implementation that is correct for + real-time applications in Linux. + +Beside the reason for sleeping, the eventual waker should also be +real-time-safe. Namely, one of: + + - An equal-or-higher-priority thread + - Hard interrupt handler + - Non-maskable interrupt handler + +This monitor's warning usually means one of the following: + + - Real-time thread is blocked by a non-real-time thread (e.g. due to + contention on a mutex without priority inheritance). This is priority + inversion. + - Time-critical work waits for something which is not safe for real-time (e.g. + timerfd). + - The work executed by the real-time thread does not need to run at real-time + priority at all. This is not a problem for the real-time thread itself, but + it is potentially taking the CPU away from other important real-time work. + +Application developers may purposely choose to have their real-time application +sleep in a way that is not safe for real-time. It is debatable whether that is a +problem. Application developers must analyze the warnings to make a proper +assessment. + +The monitor's specification is:: + + RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + + RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) + and ((not WAKE) until RT_FRIENDLY_WAKE) + + RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + + RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and NANOSLEEP_CLOCK_MONOTONIC + + RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or KTHREAD_SHOULD_STOP + + ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI + or TASK_IS_RCU + or TASK_IS_MIGRATION + +Beside the scenarios described above, this specification also handle some +special cases: + + - `KERNEL_THREAD`: kernel tasks do not have any pattern that can be recognized + as valid real-time sleeping reasons. Therefore sleeping reason is not + checked for kernel tasks. + - `KTHREAD_SHOULD_STOP`: a non-real-time thread may stop a real-time kernel + thread by waking it and waiting for it to exit (`kthread_stop()`). This + wakeup is safe for real-time. + - `ALLOWLIST`: to handle known false positives with the kernel. + - `BLOCK_ON_RT_MUTEX` is included in the allowlist due to its implementation. + In the release path of rt_mutex, a boosted task is de-boosted before waking + the rt_mutex's waiter. Consequently, the monitor may see a real-time-unsafe + wakeup (e.g. non-real-time task waking real-time task). This is actually + real-time-safe because preemption is disabled for the duration. + - `FUTEX_LOCK_PI` is included in the allowlist for the same reason as + `BLOCK_ON_RT_MUTEX`. diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst index 24b2c62a3bc2..3f8381ad9ec7 100644 --- a/Documentation/trace/rv/monitor_sched.rst +++ b/Documentation/trace/rv/monitor_sched.rst @@ -40,26 +40,6 @@ defined in by Daniel Bristot in [1]. Currently we included the following: -Monitor tss -~~~~~~~~~~~ - -The task switch while scheduling (tss) monitor ensures a task switch happens -only in scheduling context, that is inside a call to `__schedule`:: - - | - | - v - +-----------------+ - | thread | <+ - +-----------------+ | - | | - | schedule_entry | schedule_exit - v | - sched_switch | - +--------------- | - | sched | - +--------------> -+ - Monitor sco ~~~~~~~~~~~ @@ -144,26 +124,277 @@ does not enable preemption:: | scheduling_contex -+ -Monitor sncid -~~~~~~~~~~~~~ +Monitor sts +~~~~~~~~~~~ -The schedule not called with interrupt disabled (sncid) monitor ensures -schedule is not called with interrupt disabled:: +The schedule implies task switch (sts) monitor ensures a task switch happens +only in scheduling context and up to once, as well as scheduling occurs with +interrupts enabled but no task switch can happen before interrupts are +disabled. When the next task picked for execution is the same as the previously +running one, no real task switch occurs but interrupts are disabled nonetheless:: - | - | - v - schedule_entry +--------------+ - schedule_exit | | - +----------------- | can_sched | - | | | - +----------------> | | <+ - +--------------+ | - | | - | irq_disable | irq_enable - v | - | - cant_sched -+ + irq_entry | + +----+ | + v | v + +------------+ irq_enable #===================# irq_disable + | | ------------> H H irq_entry + | cant_sched | <------------ H H irq_enable + | | irq_disable H can_sched H --------------+ + +------------+ H H | + H H | + +---------------> H H <-------------+ + | #===================# + | | + schedule_exit | schedule_entry + | v + | +-------------------+ irq_enable + | | scheduling | <---------------+ + | +-------------------+ | + | | | + | | irq_disable +--------+ irq_entry + | v | | --------+ + | +-------------------+ irq_entry | in_irq | | + | | | -----------> | | <-------+ + | | disable_to_switch | +--------+ + | | | --+ + | +-------------------+ | + | | | + | | sched_switch | + | v | + | +-------------------+ | + | | switching | | irq_enable + | +-------------------+ | + | | | + | | irq_enable | + | v | + | +-------------------+ | + +-- | enable_to_exit | <-+ + +-------------------+ + ^ | irq_disable + | | irq_entry + +---------------+ irq_enable + +Monitor nrp +----------- + +The need resched preempts (nrp) monitor ensures preemption requires +``need_resched``. Only kernel preemption is considered, since preemption +while returning to userspace, for this monitor, is indistinguishable from +``sched_switch_yield`` (described in the sssw monitor). +A kernel preemption is whenever ``__schedule`` is called with the preemption +flag set to true (e.g. from preempt_enable or exiting from interrupts). This +type of preemption occurs after the need for ``rescheduling`` has been set. +This is not valid for the *lazy* variant of the flag, which causes only +userspace preemption. +A ``schedule_entry_preempt`` may involve a task switch or not, in the latter +case, a task goes through the scheduler from a preemption context but it is +picked as the next task to run. Since the scheduler runs, this clears the need +to reschedule. The ``any_thread_running`` state does not imply the monitored +task is not running as this monitor does not track the outcome of scheduling. + +In theory, a preemption can only occur after the ``need_resched`` flag is set. In +practice, however, it is possible to see a preemption where the flag is not +set. This can happen in one specific condition:: + + need_resched + preempt_schedule() + preempt_schedule_irq() + __schedule() + !need_resched + __schedule() + +In the situation above, standard preemption starts (e.g. from preempt_enable +when the flag is set), an interrupt occurs before scheduling and, on its exit +path, it schedules, which clears the ``need_resched`` flag. +When the preempted task runs again, the standard preemption started earlier +resumes, although the flag is no longer set. The monitor considers this a +``nested_preemption``, this allows another preemption without re-setting the +flag. This condition relaxes the monitor constraints and may catch false +negatives (i.e. no real ``nested_preemptions``) but makes the monitor more +robust and able to validate other scenarios. +For simplicity, the monitor starts in ``preempt_irq``, although no interrupt +occurred, as the situation above is hard to pinpoint:: + + schedule_entry + irq_entry #===========================================# + +-------------------------- H H + | H H + +-------------------------> H any_thread_running H + H H + +-------------------------> H H + | #===========================================# + | schedule_entry | ^ + | schedule_entry_preempt | sched_need_resched | schedule_entry + | | schedule_entry_preempt + | v | + | +----------------------+ | + | +--- | | | + | sched_need_resched | | rescheduling | -+ + | +--> | | + | +----------------------+ + | | irq_entry + | v + | +----------------------+ + | | | ---+ + | ---> | | | sched_need_resched + | | preempt_irq | | irq_entry + | | | <--+ + | | | <--+ + | +----------------------+ | + | | schedule_entry | sched_need_resched + | | schedule_entry_preempt | + | v | + | +-----------------------+ | + +-------------------------- | nested_preempt | --+ + +-----------------------+ + ^ irq_entry | + +-------------------+ + +Due to how the ``need_resched`` flag on the preemption count works on arm64, +this monitor is unstable on that architecture, as it often records preemption +when the flag is not set, even in presence of the workaround above. +For the time being, the monitor is disabled by default on arm64. + +Monitor sssw +------------ + +The set state sleep and wakeup (sssw) monitor ensures ``set_state`` to +sleepable leads to sleeping and sleeping tasks require wakeup. It includes the +following types of switch: + +* ``switch_suspend``: + a task puts itself to sleep, this can happen only after explicitly setting + the task to ``sleepable``. After a task is suspended, it needs to be woken up + (``waking`` state) before being switched in again. + Setting the task's state to ``sleepable`` can be reverted before switching if it + is woken up or set to ``runnable``. +* ``switch_blocking``: + a special case of a ``switch_suspend`` where the task is waiting on a + sleeping RT lock (``PREEMPT_RT`` only), it is common to see wakeup and set + state events racing with each other and this leads the model to perceive this + type of switch when the task is not set to sleepable. This is a limitation of + the model in SMP system and workarounds may slow down the system. +* ``switch_preempt``: + a task switch as a result of kernel preemption (``schedule_entry_preempt`` in + the nrp model). +* ``switch_yield``: + a task explicitly calls the scheduler or is preempted while returning to + userspace. It can happen after a ``yield`` system call, from the idle task or + if the ``need_resched`` flag is set. By definition, a task cannot yield while + ``sleepable`` as that would be a suspension. A special case of a yield occurs + when a task in ``TASK_INTERRUPTIBLE`` calls the scheduler while a signal is + pending. The task doesn't go through the usual blocking/waking and is set + back to runnable, the resulting switch (if there) looks like a yield to the + ``signal_wakeup`` state and is followed by the signal delivery. From this + state, the monitor expects a signal even if it sees a wakeup event, although + not necessary, to rule out false negatives. + +This monitor doesn't include a running state, ``sleepable`` and ``runnable`` +are only referring to the task's desired state, which could be scheduled out +(e.g. due to preemption). However, it does include the event +``sched_switch_in`` to represent when a task is allowed to become running. This +can be triggered also by preemption, but cannot occur after the task got to +``sleeping`` before a ``wakeup`` occurs:: + + +--------------------------------------------------------------------------+ + | | + | | + | switch_suspend | | + | switch_blocking | | + v v | + +----------+ #==========================# set_state_runnable | + | | H H wakeup | + | | H H switch_in | + | | H H switch_yield | + | sleeping | H H switch_preempt | + | | H H signal_deliver | + | | switch_ H H ------+ | + | | _blocking H runnable H | | + | | <----------- H H <-----+ | + +----------+ H H | + | wakeup H H | + +---------------------> H H | + H H | + +---------> H H | + | #==========================# | + | | ^ | + | | | set_state_runnable | + | | | wakeup | + | set_state_sleepable | +------------------------+ + | v | | + | +--------------------------+ set_state_sleepable + | | | switch_in + | | | switch_preempt + signal_deliver | sleepable | signal_deliver + | | | ------+ + | | | | + | | | <-----+ + | +--------------------------+ + | | ^ + | switch_yield | set_state_sleepable + | v | + | +---------------+ | + +---------- | signal_wakeup | -+ + +---------------+ + ^ | switch_in + | | switch_preempt + | | switch_yield + +-----------+ wakeup + +Monitor opid +------------ + +The operations with preemption and irq disabled (opid) monitor ensures +operations like ``wakeup`` and ``need_resched`` occur with interrupts and +preemption disabled or during interrupt context, in such case preemption may +not be disabled explicitly. +``need_resched`` can be set by some RCU internals functions, in which case it +doesn't match a task wakeup and might occur with only interrupts disabled:: + + | sched_need_resched + | sched_waking + | irq_entry + | +--------------------+ + v v | + +------------------------------------------------------+ + +----------- | disabled | <+ + | +------------------------------------------------------+ | + | | ^ | + | | preempt_disable sched_need_resched | + | preempt_enable | +--------------------+ | + | v | v | | + | +------------------------------------------------------+ | + | | irq_disabled | | + | +------------------------------------------------------+ | + | | | ^ | + | irq_entry irq_entry | | | + | sched_need_resched v | irq_disable | + | sched_waking +--------------+ | | | + | +----- | | irq_enable | | + | | | in_irq | | | | + | +----> | | | | | + | +--------------+ | | irq_disable + | | | | | + | irq_enable | irq_enable | | | + | v v | | + | #======================================================# | + | H enabled H | + | #======================================================# | + | | ^ ^ preempt_enable | | + | preempt_disable preempt_enable +--------------------+ | + | v | | + | +------------------+ | | + +----------> | preempt_disabled | -+ | + +------------------+ | + | | + +-------------------------------------------------------+ + +This monitor is designed to work on ``PREEMPT_RT`` kernels, the special case of +events occurring in interrupt context is a shortcut to identify valid scenarios +where the preemption tracepoints might not be visible, during interrupts +preemption is always disabled. On non- ``PREEMPT_RT`` kernels, the interrupts +might invoke a softirq to set ``need_resched`` and wake up a task. This is +another special case that is currently not supported by the monitor. References ---------- diff --git a/Documentation/trace/rv/monitor_synthesis.rst b/Documentation/trace/rv/monitor_synthesis.rst new file mode 100644 index 000000000000..ac808a7554f5 --- /dev/null +++ b/Documentation/trace/rv/monitor_synthesis.rst @@ -0,0 +1,271 @@ +Runtime Verification Monitor Synthesis +====================================== + +The starting point for the application of runtime verification (RV) techniques +is the *specification* or *modeling* of the desired (or undesired) behavior +of the system under scrutiny. + +The formal representation needs to be then *synthesized* into a *monitor* +that can then be used in the analysis of the trace of the system. The +*monitor* connects to the system via an *instrumentation* that converts +the events from the *system* to the events of the *specification*. + + +In Linux terms, the runtime verification monitors are encapsulated inside +the *RV monitor* abstraction. The RV monitor includes a set of instances +of the monitor (per-cpu monitor, per-task monitor, and so on), the helper +functions that glue the monitor to the system reference model, and the +trace output as a reaction to event parsing and exceptions, as depicted +below:: + + Linux +----- RV Monitor ----------------------------------+ Formal + Realm | | Realm + +-------------------+ +----------------+ +-----------------+ + | Linux kernel | | Monitor | | Reference | + | Tracing | -> | Instance(s) | <- | Model | + | (instrumentation) | | (verification) | | (specification) | + +-------------------+ +----------------+ +-----------------+ + | | | + | V | + | +----------+ | + | | Reaction | | + | +--+--+--+-+ | + | | | | | + | | | +-> trace output ? | + +------------------------|--|----------------------+ + | +----> panic ? + +-------> <user-specified> + +RV monitor synthesis +-------------------- + +The synthesis of a specification into the Linux *RV monitor* abstraction is +automated by the rvgen tool and the header file containing common code for +creating monitors. The header files are: + + * rv/da_monitor.h for deterministic automaton monitor. + * rv/ltl_monitor.h for linear temporal logic monitor. + +rvgen +----- + +The rvgen utility converts a specification into the C presentation and creating +the skeleton of a kernel monitor in C. + +For example, it is possible to transform the wip.dot model present in +[1] into a per-cpu monitor with the following command:: + + $ rvgen monitor -c da -s wip.dot -t per_cpu + +This will create a directory named wip/ with the following files: + +- wip.h: the wip model in C +- wip.c: the RV monitor + +The wip.c file contains the monitor declaration and the starting point for +the system instrumentation. + +Similarly, a linear temporal logic monitor can be generated with the following +command:: + + $ rvgen monitor -c ltl -s pagefault.ltl -t per_task + +This generates pagefault/ directory with: + +- pagefault.h: The Buchi automaton (the non-deterministic state machine to + verify the specification) +- pagefault.c: The skeleton for the RV monitor + +Monitor header files +-------------------- + +The header files: + +- `rv/da_monitor.h` for deterministic automaton monitor +- `rv/ltl_monitor` for linear temporal logic monitor + +include common macros and static functions for implementing *Monitor +Instance(s)*. + +The benefits of having all common functionalities in a single header file are +3-fold: + + - Reduce the code duplication; + - Facilitate the bug fix/improvement; + - Avoid the case of developers changing the core of the monitor code to + manipulate the model in a (let's say) non-standard way. + +rv/da_monitor.h ++++++++++++++++ + +This initial implementation presents three different types of monitor instances: + +- ``#define DECLARE_DA_MON_GLOBAL(name, type)`` +- ``#define DECLARE_DA_MON_PER_CPU(name, type)`` +- ``#define DECLARE_DA_MON_PER_TASK(name, type)`` + +The first declares the functions for a global deterministic automata monitor, +the second for monitors with per-cpu instances, and the third with per-task +instances. + +In all cases, the 'name' argument is a string that identifies the monitor, and +the 'type' argument is the data type used by rvgen on the representation of +the model in C. + +For example, the wip model with two states and three events can be +stored in an 'unsigned char' type. Considering that the preemption control +is a per-cpu behavior, the monitor declaration in the 'wip.c' file is:: + + DECLARE_DA_MON_PER_CPU(wip, unsigned char); + +The monitor is executed by sending events to be processed via the functions +presented below:: + + da_handle_event_$(MONITOR_NAME)($(event from event enum)); + da_handle_start_event_$(MONITOR_NAME)($(event from event enum)); + da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum)); + +The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where +the event will be processed if the monitor is processing events. + +When a monitor is enabled, it is placed in the initial state of the automata. +However, the monitor does not know if the system is in the *initial state*. + +The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the +monitor that the system is returning to the initial state, so the monitor can +start monitoring the next event. + +The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify +the monitor that the system is known to be in the initial state, so the +monitor can start monitoring and monitor the current event. + +Using the wip model as example, the events "preempt_disable" and +"sched_waking" should be sent to monitor, respectively, via [2]:: + + da_handle_event_wip(preempt_disable_wip); + da_handle_event_wip(sched_waking_wip); + +While the event "preempt_enabled" will use:: + + da_handle_start_event_wip(preempt_enable_wip); + +To notify the monitor that the system will be returning to the initial state, +so the system and the monitor should be in sync. + +rv/ltl_monitor.h +++++++++++++++++ +This file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`) +to be complete. For example, for the `pagefault` monitor, the `pagefault.c` +source file must include:: + + #include "pagefault.h" + #include <rv/ltl_monitor.h> + +(the skeleton monitor file generated by `rvgen` already does this). + +`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the +implementation of the Buchi automaton - a non-deterministic state machine that +verifies the LTL specification. While `rv/ltl_monitor.h` includes the common +helper functions to interact with the Buchi automaton and to implement an RV +monitor. An important definition in `$(MODEL_NAME).h` is:: + + enum ltl_atom { + LTL_$(FIRST_ATOMIC_PROPOSITION), + LTL_$(SECOND_ATOMIC_PROPOSITION), + ... + LTL_NUM_ATOM + }; + +which is the list of atomic propositions present in the LTL specification +(prefixed with "LTL\_" to avoid name collision). This `enum` is passed to the +functions interacting with the Buchi automaton. + +While generating code, `rvgen` cannot understand the meaning of the atomic +propositions. Thus, that task is left for manual work. The recommended pratice +is adding tracepoints to places where the atomic propositions change; and in the +tracepoints' handlers: the Buchi automaton is executed using:: + + void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value) + +which tells the Buchi automaton that the atomic proposition `atom` is now +`value`. The Buchi automaton checks whether the LTL specification is still +satisfied, and invokes the monitor's error tracepoint and the reactor if +violation is detected. + +Tracepoints and `ltl_atom_update()` should be used whenever possible. However, +it is sometimes not the most convenient. For some atomic propositions which are +changed in multiple places in the kernel, it is cumbersome to trace all those +places. Furthermore, it may not be important that the atomic propositions are +updated at precise times. For example, considering the following linear temporal +logic:: + + RULE = always (RT imply not PAGEFAULT) + +This LTL states that a real-time task does not raise page faults. For this +specification, it is not important when `RT` changes, as long as it has the +correct value when `PAGEFAULT` is true. Motivated by this case, another +function is introduced:: + + void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon) + +This function is called whenever the Buchi automaton is triggered. Therefore, it +can be manually implemented to "fetch" `RT`:: + + void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon) + { + ltl_atom_set(mon, LTL_RT, rt_task(task)); + } + +Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_update()`, +`RT` is also fetched. Thus, the LTL specification can be verified without +tracing `RT` everywhere. + +For atomic propositions which act like events, they usually need to be set (or +cleared) and then immediately cleared (or set). A convenient function is +provided:: + + void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value) + +which is equivalent to:: + + ltl_atom_update(task, atom, value); + ltl_atom_update(task, atom, !value); + +To initialize the atomic propositions, the following function must be +implemented:: + + ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) + +This function is called for all running tasks when the monitor is enabled. It is +also called for new tasks created after the enabling the monitor. It should +initialize as many atomic propositions as possible, for example:: + + void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) + { + ltl_atom_set(mon, LTL_RT, rt_task(task)); + if (task_creation) + ltl_atom_set(mon, LTL_PAGEFAULT, false); + } + +Atomic propositions not initialized by `ltl_atom_init()` will stay in the +unknown state until relevant tracepoints are hit, which can take some time. As +monitoring for a task cannot be done until all atomic propositions is known for +the task, the monitor may need some time to start validating tasks which have +been running before the monitor is enabled. Therefore, it is recommended to +start the tasks of interest after enabling the monitor. + +Final remarks +------------- + +With the monitor synthesis in place using the header files and +rvgen, the developer's work should be limited to the instrumentation +of the system, increasing the confidence in the overall approach. + +[1] For details about deterministic automata format and the translation +from one representation to another, see:: + + Documentation/trace/rv/deterministic_automata.rst + +[2] rvgen appends the monitor's name suffix to the events enums to +avoid conflicting variables when exporting the global vmlinux.h +use by BPF programs. diff --git a/arch/riscv/mm/fault.c b/arch/riscv/mm/fault.c index 0194324a0c50..04ed6f8acae4 100644 --- a/arch/riscv/mm/fault.c +++ b/arch/riscv/mm/fault.c @@ -20,6 +20,9 @@ #include <asm/ptrace.h> #include <asm/tlbflush.h> +#define CREATE_TRACE_POINTS +#include <trace/events/exceptions.h> + #include "../kernel/head.h" static void show_pte(unsigned long addr) @@ -291,6 +294,11 @@ void handle_page_fault(struct pt_regs *regs) if (kprobe_page_fault(regs, cause)) return; + if (user_mode(regs)) + trace_page_fault_user(addr, regs, cause); + else + trace_page_fault_kernel(addr, regs, cause); + /* * Fault-in kernel-space virtual memory on-demand. * The 'reference' page table is init_mm.pgd. diff --git a/include/linux/panic.h b/include/linux/panic.h index 8f2b5d92ac05..7be742628c25 100644 --- a/include/linux/panic.h +++ b/include/linux/panic.h @@ -3,6 +3,7 @@ #define _LINUX_PANIC_H #include <linux/compiler_attributes.h> +#include <linux/stdarg.h> #include <linux/types.h> struct pt_regs; @@ -10,6 +11,8 @@ struct pt_regs; extern long (*panic_blink)(int state); __printf(1, 2) void panic(const char *fmt, ...) __noreturn __cold; +__printf(1, 0) +void vpanic(const char *fmt, va_list args) __noreturn __cold; void nmi_panic(struct pt_regs *regs, const char *msg); void check_panic_on_warn(const char *origin); extern void oops_enter(void); diff --git a/include/linux/printk.h b/include/linux/printk.h index 5b462029d03c..5d22b803f51e 100644 --- a/include/linux/printk.h +++ b/include/linux/printk.h @@ -154,6 +154,8 @@ int vprintk_emit(int facility, int level, asmlinkage __printf(1, 0) int vprintk(const char *fmt, va_list args); +__printf(1, 0) +int vprintk_deferred(const char *fmt, va_list args); asmlinkage __printf(1, 2) __cold int _printk(const char *fmt, ...); @@ -214,6 +216,11 @@ int vprintk(const char *s, va_list args) { return 0; } +static inline __printf(1, 0) +int vprintk_deferred(const char *fmt, va_list args) +{ + return 0; +} static inline __printf(1, 2) __cold int _printk(const char *s, ...) { diff --git a/include/linux/rv.h b/include/linux/rv.h index 3452b5e4b29e..14410a42faef 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -7,9 +7,17 @@ #ifndef _LINUX_RV_H #define _LINUX_RV_H -#define MAX_DA_NAME_LEN 32 +#include <linux/types.h> +#include <linux/list.h> + +#define MAX_DA_NAME_LEN 32 +#define MAX_DA_RETRY_RACING_EVENTS 3 #ifdef CONFIG_RV +#include <linux/bitops.h> +#include <linux/types.h> +#include <linux/array_size.h> + /* * Deterministic automaton per-object variables. */ @@ -18,27 +26,72 @@ struct da_monitor { unsigned int curr_state; }; +#ifdef CONFIG_RV_LTL_MONITOR + /* - * Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS. - * If we find justification for more monitors, we can think about - * adding more or developing a dynamic method. So far, none of - * these are justified. + * In the future, if the number of atomic propositions or the size of Buchi + * automaton is larger, we can switch to dynamic allocation. For now, the code + * is simpler this way. */ -#define RV_PER_TASK_MONITORS 1 -#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS) +#define RV_MAX_LTL_ATOM 32 +#define RV_MAX_BA_STATES 32 -/* - * Futher monitor types are expected, so make this a union. +/** + * struct ltl_monitor - A linear temporal logic runtime verification monitor + * @states: States in the Buchi automaton. As Buchi automaton is a + * non-deterministic state machine, the monitor can be in multiple + * states simultaneously. This is a bitmask of all possible states. + * If this is zero, that means either: + * - The monitor has not started yet (e.g. because not all + * atomic propositions are known). + * - There is no possible state to be in. In other words, a + * violation of the LTL property is detected. + * @atoms: The values of atomic propositions. + * @unknown_atoms: Atomic propositions which are still unknown. */ +struct ltl_monitor { + DECLARE_BITMAP(states, RV_MAX_BA_STATES); + DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM); + DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM); +}; + +static inline bool rv_ltl_valid_state(struct ltl_monitor *mon) +{ + for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) { + if (mon->states[i]) + return true; + } + return false; +} + +static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon) +{ + for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) { + if (mon->unknown_atoms[i]) + return false; + } + return true; +} + +#else + +struct ltl_monitor {}; + +#endif /* CONFIG_RV_LTL_MONITOR */ + +#define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS) + union rv_task_monitor { - struct da_monitor da_mon; + struct da_monitor da_mon; + struct ltl_monitor ltl_mon; }; #ifdef CONFIG_RV_REACTORS struct rv_reactor { const char *name; const char *description; - void (*react)(char *msg); + __printf(1, 2) void (*react)(const char *msg, ...); + struct list_head list; }; #endif @@ -50,8 +103,12 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS - void (*react)(char *msg); + struct rv_reactor *reactor; + __printf(1, 2) void (*react)(const char *msg, ...); #endif + struct list_head list; + struct rv_monitor *parent; + struct dentry *root_d; }; bool rv_monitoring_on(void); @@ -64,6 +121,11 @@ void rv_put_task_monitor_slot(int slot); bool rv_reacting_on(void); int rv_unregister_reactor(struct rv_reactor *reactor); int rv_register_reactor(struct rv_reactor *reactor); +#else +static inline bool rv_reacting_on(void) +{ + return false; +} #endif /* CONFIG_RV_REACTORS */ #endif /* CONFIG_RV */ diff --git a/include/linux/sched.h b/include/linux/sched.h index 40d2fa90df42..a9693f179c58 100644 --- a/include/linux/sched.h +++ b/include/linux/sched.h @@ -340,9 +340,11 @@ extern void io_schedule_finish(int token); extern long io_schedule_timeout(long timeout); extern void io_schedule(void); -/* wrapper function to trace from this header file */ +/* wrapper functions to trace from this header file */ DECLARE_TRACEPOINT(sched_set_state_tp); extern void __trace_set_current_state(int state_value); +DECLARE_TRACEPOINT(sched_set_need_resched_tp); +extern void __trace_set_need_resched(struct task_struct *curr, int tif); /** * struct prev_cputime - snapshot of system and user cputime @@ -1634,12 +1636,10 @@ struct task_struct { #ifdef CONFIG_RV /* - * Per-task RV monitor. Nowadays fixed in RV_PER_TASK_MONITORS. - * If we find justification for more monitors, we can think - * about adding more or developing a dynamic method. So far, - * none of these are justified. + * Per-task RV monitor, fixed in CONFIG_RV_PER_TASK_MONITORS. + * If memory becomes a concern, we can think about a dynamic method. */ - union rv_task_monitor rv[RV_PER_TASK_MONITORS]; + union rv_task_monitor rv[CONFIG_RV_PER_TASK_MONITORS]; #endif #ifdef CONFIG_USER_EVENTS @@ -2030,6 +2030,9 @@ static inline int test_tsk_thread_flag(struct task_struct *tsk, int flag) static inline void set_tsk_need_resched(struct task_struct *tsk) { + if (tracepoint_enabled(sched_set_need_resched_tp) && + !test_tsk_thread_flag(tsk, TIF_NEED_RESCHED)) + __trace_set_need_resched(tsk, TIF_NEED_RESCHED); set_tsk_thread_flag(tsk,TIF_NEED_RESCHED); } diff --git a/include/rv/da_monitor.h b/include/rv/da_monitor.h index 510c88bfabd4..17fa4f6e5ea6 100644 --- a/include/rv/da_monitor.h +++ b/include/rv/da_monitor.h @@ -19,45 +19,22 @@ #ifdef CONFIG_RV_REACTORS #define DECLARE_RV_REACTING_HELPERS(name, type) \ -static char REACT_MSG_##name[1024]; \ - \ -static inline char *format_react_msg_##name(type curr_state, type event) \ -{ \ - snprintf(REACT_MSG_##name, 1024, \ - "rv: monitor %s does not allow event %s on state %s\n", \ - #name, \ - model_get_event_name_##name(event), \ - model_get_state_name_##name(curr_state)); \ - return REACT_MSG_##name; \ -} \ - \ -static void cond_react_##name(char *msg) \ +static void cond_react_##name(type curr_state, type event) \ { \ - if (rv_##name.react) \ - rv_##name.react(msg); \ -} \ - \ -static bool rv_reacting_on_##name(void) \ -{ \ - return rv_reacting_on(); \ + if (!rv_reacting_on() || !rv_##name.react) \ + return; \ + rv_##name.react("rv: monitor %s does not allow event %s on state %s\n", \ + #name, \ + model_get_event_name_##name(event), \ + model_get_state_name_##name(curr_state)); \ } #else /* CONFIG_RV_REACTOR */ #define DECLARE_RV_REACTING_HELPERS(name, type) \ -static inline char *format_react_msg_##name(type curr_state, type event) \ -{ \ - return NULL; \ -} \ - \ -static void cond_react_##name(char *msg) \ +static void cond_react_##name(type curr_state, type event) \ { \ return; \ -} \ - \ -static bool rv_reacting_on_##name(void) \ -{ \ - return 0; \ } #endif @@ -78,23 +55,6 @@ static inline void da_monitor_reset_##name(struct da_monitor *da_mon) \ } \ \ /* \ - * da_monitor_curr_state_##name - return the current state \ - */ \ -static inline type da_monitor_curr_state_##name(struct da_monitor *da_mon) \ -{ \ - return da_mon->curr_state; \ -} \ - \ -/* \ - * da_monitor_set_state_##name - set the new current state \ - */ \ -static inline void \ -da_monitor_set_state_##name(struct da_monitor *da_mon, enum states_##name state) \ -{ \ - da_mon->curr_state = state; \ -} \ - \ -/* \ * da_monitor_start_##name - start monitoring \ * \ * The monitor will ignore all events until monitoring is set to true. This \ @@ -150,65 +110,81 @@ static inline bool da_monitor_handling_event_##name(struct da_monitor *da_mon) * Event handler for implicit monitors. Implicit monitor is the one which the * handler does not need to specify which da_monitor to manipulate. Examples * of implicit monitor are the per_cpu or the global ones. + * + * Retry in case there is a race between getting and setting the next state, + * warn and reset the monitor if it runs out of retries. The monitor should be + * able to handle various orders. */ #define DECLARE_DA_MON_MODEL_HANDLER_IMPLICIT(name, type) \ \ static inline bool \ da_event_##name(struct da_monitor *da_mon, enum events_##name event) \ { \ - type curr_state = da_monitor_curr_state_##name(da_mon); \ - type next_state = model_get_next_state_##name(curr_state, event); \ - \ - if (next_state != INVALID_STATE) { \ - da_monitor_set_state_##name(da_mon, next_state); \ - \ - trace_event_##name(model_get_state_name_##name(curr_state), \ - model_get_event_name_##name(event), \ - model_get_state_name_##name(next_state), \ - model_is_final_state_##name(next_state)); \ - \ - return true; \ + enum states_##name curr_state, next_state; \ + \ + curr_state = READ_ONCE(da_mon->curr_state); \ + for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \ + next_state = model_get_next_state_##name(curr_state, event); \ + if (next_state == INVALID_STATE) { \ + cond_react_##name(curr_state, event); \ + trace_error_##name(model_get_state_name_##name(curr_state), \ + model_get_event_name_##name(event)); \ + return false; \ + } \ + if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \ + trace_event_##name(model_get_state_name_##name(curr_state), \ + model_get_event_name_##name(event), \ + model_get_state_name_##name(next_state), \ + model_is_final_state_##name(next_state)); \ + return true; \ + } \ } \ \ - if (rv_reacting_on_##name()) \ - cond_react_##name(format_react_msg_##name(curr_state, event)); \ - \ - trace_error_##name(model_get_state_name_##name(curr_state), \ - model_get_event_name_##name(event)); \ - \ + trace_rv_retries_error(#name, model_get_event_name_##name(event)); \ + pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \ + " retries reached for event %s, resetting monitor %s", \ + model_get_event_name_##name(event), #name); \ return false; \ } \ /* * Event handler for per_task monitors. + * + * Retry in case there is a race between getting and setting the next state, + * warn and reset the monitor if it runs out of retries. The monitor should be + * able to handle various orders. */ #define DECLARE_DA_MON_MODEL_HANDLER_PER_TASK(name, type) \ \ static inline bool da_event_##name(struct da_monitor *da_mon, struct task_struct *tsk, \ enum events_##name event) \ { \ - type curr_state = da_monitor_curr_state_##name(da_mon); \ - type next_state = model_get_next_state_##name(curr_state, event); \ - \ - if (next_state != INVALID_STATE) { \ - da_monitor_set_state_##name(da_mon, next_state); \ - \ - trace_event_##name(tsk->pid, \ - model_get_state_name_##name(curr_state), \ - model_get_event_name_##name(event), \ - model_get_state_name_##name(next_state), \ - model_is_final_state_##name(next_state)); \ - \ - return true; \ + enum states_##name curr_state, next_state; \ + \ + curr_state = READ_ONCE(da_mon->curr_state); \ + for (int i = 0; i < MAX_DA_RETRY_RACING_EVENTS; i++) { \ + next_state = model_get_next_state_##name(curr_state, event); \ + if (next_state == INVALID_STATE) { \ + cond_react_##name(curr_state, event); \ + trace_error_##name(tsk->pid, \ + model_get_state_name_##name(curr_state), \ + model_get_event_name_##name(event)); \ + return false; \ + } \ + if (likely(try_cmpxchg(&da_mon->curr_state, &curr_state, next_state))) { \ + trace_event_##name(tsk->pid, \ + model_get_state_name_##name(curr_state), \ + model_get_event_name_##name(event), \ + model_get_state_name_##name(next_state), \ + model_is_final_state_##name(next_state)); \ + return true; \ + } \ } \ \ - if (rv_reacting_on_##name()) \ - cond_react_##name(format_react_msg_##name(curr_state, event)); \ - \ - trace_error_##name(tsk->pid, \ - model_get_state_name_##name(curr_state), \ - model_get_event_name_##name(event)); \ - \ + trace_rv_retries_error(#name, model_get_event_name_##name(event)); \ + pr_warn("rv: " __stringify(MAX_DA_RETRY_RACING_EVENTS) \ + " retries reached for event %s, resetting monitor %s", \ + model_get_event_name_##name(event), #name); \ return false; \ } @@ -512,6 +488,30 @@ da_handle_start_event_##name(struct task_struct *tsk, enum events_##name event) __da_handle_event_##name(da_mon, tsk, event); \ \ return 1; \ +} \ + \ +/* \ + * da_handle_start_run_event_##name - start monitoring and handle event \ + * \ + * This function is used to notify the monitor that the system is in the \ + * initial state, so the monitor can start monitoring and handling event. \ + */ \ +static inline bool \ +da_handle_start_run_event_##name(struct task_struct *tsk, enum events_##name event) \ +{ \ + struct da_monitor *da_mon; \ + \ + if (!da_monitor_enabled_##name()) \ + return 0; \ + \ + da_mon = da_get_monitor_##name(tsk); \ + \ + if (unlikely(!da_monitoring_##name(da_mon))) \ + da_monitor_start_##name(da_mon); \ + \ + __da_handle_event_##name(da_mon, tsk, event); \ + \ + return 1; \ } /* diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h new file mode 100644 index 000000000000..67031a774e3d --- /dev/null +++ b/include/rv/ltl_monitor.h @@ -0,0 +1,186 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/** + * This file must be combined with the $(MODEL_NAME).h file generated by + * tools/verification/rvgen. + */ + +#include <linux/args.h> +#include <linux/rv.h> +#include <linux/stringify.h> +#include <linux/seq_buf.h> +#include <rv/instrumentation.h> +#include <trace/events/task.h> +#include <trace/events/sched.h> + +#ifndef MONITOR_NAME +#error "Please include $(MODEL_NAME).h generated by rvgen" +#endif + +#ifdef CONFIG_RV_REACTORS +#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME) +static struct rv_monitor RV_MONITOR_NAME; + +static void rv_cond_react(struct task_struct *task) +{ + if (!rv_reacting_on() || !RV_MONITOR_NAME.react) + return; + RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n", + task->comm, task->pid); +} +#else +static void rv_cond_react(struct task_struct *task) +{ +} +#endif + +static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon); +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation); + +static struct ltl_monitor *ltl_get_monitor(struct task_struct *task) +{ + return &task->rv[ltl_monitor_slot].ltl_mon; +} + +static void ltl_task_init(struct task_struct *task, bool task_creation) +{ + struct ltl_monitor *mon = ltl_get_monitor(task); + + memset(&mon->states, 0, sizeof(mon->states)); + + for (int i = 0; i < LTL_NUM_ATOM; ++i) + __set_bit(i, mon->unknown_atoms); + + ltl_atoms_init(task, mon, task_creation); + ltl_atoms_fetch(task, mon); +} + +static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags) +{ + ltl_task_init(task, true); +} + +static int ltl_monitor_init(void) +{ + struct task_struct *g, *p; + int ret, cpu; + + ret = rv_get_task_monitor_slot(); + if (ret < 0) + return ret; + + ltl_monitor_slot = ret; + + rv_attach_trace_probe(name, task_newtask, handle_task_newtask); + + read_lock(&tasklist_lock); + + for_each_process_thread(g, p) + ltl_task_init(p, false); + + for_each_present_cpu(cpu) + ltl_task_init(idle_task(cpu), false); + + read_unlock(&tasklist_lock); + + return 0; +} + +static void ltl_monitor_destroy(void) +{ + rv_detach_trace_probe(name, task_newtask, handle_task_newtask); + + rv_put_task_monitor_slot(ltl_monitor_slot); + ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT; +} + +static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon) +{ + CONCATENATE(trace_error_, MONITOR_NAME)(task); + rv_cond_react(task); +} + +static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon) +{ + if (rv_ltl_all_atoms_known(mon)) + ltl_start(task, mon); +} + +static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value) +{ + __clear_bit(atom, mon->unknown_atoms); + if (value) + __set_bit(atom, mon->atoms); + else + __clear_bit(atom, mon->atoms); +} + +static void +ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state) +{ + const char *format_str = "%s"; + DECLARE_SEQ_BUF(atoms, 64); + char states[32], next[32]; + int i; + + if (!CONCATENATE(CONCATENATE(trace_event_, MONITOR_NAME), _enabled)()) + return; + + snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states); + snprintf(next, sizeof(next), "%*pbl", RV_MAX_BA_STATES, next_state); + + for (i = 0; i < LTL_NUM_ATOM; ++i) { + if (test_bit(i, mon->atoms)) { + seq_buf_printf(&atoms, format_str, ltl_atom_str(i)); + format_str = ",%s"; + } + } + + CONCATENATE(trace_event_, MONITOR_NAME)(task, states, atoms.buffer, next); +} + +static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon) +{ + DECLARE_BITMAP(next_states, RV_MAX_BA_STATES) = {0}; + + if (!rv_ltl_valid_state(mon)) + return; + + for (unsigned int i = 0; i < RV_NUM_BA_STATES; ++i) { + if (test_bit(i, mon->states)) + ltl_possible_next_states(mon, i, next_states); + } + + ltl_trace_event(task, mon, next_states); + + memcpy(mon->states, next_states, sizeof(next_states)); + + if (!rv_ltl_valid_state(mon)) + ltl_illegal_state(task, mon); +} + +static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value) +{ + struct ltl_monitor *mon = ltl_get_monitor(task); + + ltl_atom_set(mon, atom, value); + ltl_atoms_fetch(task, mon); + + if (!rv_ltl_valid_state(mon)) { + ltl_attempt_start(task, mon); + return; + } + + ltl_validate(task, mon); +} + +static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value) +{ + struct ltl_monitor *mon = ltl_get_monitor(task); + + ltl_atom_update(task, atom, value); + + ltl_atom_set(mon, atom, !value); + ltl_validate(task, mon); +} diff --git a/include/trace/events/sched.h b/include/trace/events/sched.h index 4e6b2910cec3..c08893bde255 100644 --- a/include/trace/events/sched.h +++ b/include/trace/events/sched.h @@ -882,18 +882,22 @@ DECLARE_TRACE(sched_compute_energy, TP_ARGS(p, dst_cpu, energy, max_util, busy_time)); DECLARE_TRACE(sched_entry, - TP_PROTO(bool preempt, unsigned long ip), - TP_ARGS(preempt, ip)); + TP_PROTO(bool preempt), + TP_ARGS(preempt)); DECLARE_TRACE(sched_exit, - TP_PROTO(bool is_switch, unsigned long ip), - TP_ARGS(is_switch, ip)); + TP_PROTO(bool is_switch), + TP_ARGS(is_switch)); DECLARE_TRACE_CONDITION(sched_set_state, TP_PROTO(struct task_struct *tsk, int state), TP_ARGS(tsk, state), TP_CONDITION(!!(tsk->__state) != !!state)); +DECLARE_TRACE(sched_set_need_resched, + TP_PROTO(struct task_struct *tsk, int cpu, int tif), + TP_ARGS(tsk, cpu, tif)); + #endif /* _TRACE_SCHED_H */ /* This part must be outside protection */ diff --git a/kernel/fork.c b/kernel/fork.c index aef41211c72c..52901fe4a3c2 100644 --- a/kernel/fork.c +++ b/kernel/fork.c @@ -1890,10 +1890,7 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk) #ifdef CONFIG_RV static void rv_task_fork(struct task_struct *p) { - int i; - - for (i = 0; i < RV_PER_TASK_MONITORS; i++) - p->rv[i].da_mon.monitoring = false; + memset(&p->rv, 0, sizeof(p->rv)); } #else #define rv_task_fork(p) do {} while (0) diff --git a/kernel/panic.c b/kernel/panic.c index 64e58835086d..43817111c979 100644 --- a/kernel/panic.c +++ b/kernel/panic.c @@ -367,15 +367,15 @@ static void panic_other_cpus_shutdown(bool crash_kexec) } /** - * panic - halt the system + * vpanic - halt the system * @fmt: The text string to print + * @args: Arguments for the format string * * Display a message, then perform cleanups. This function never returns. */ -void panic(const char *fmt, ...) +void vpanic(const char *fmt, va_list args) { static char buf[1024]; - va_list args; long i, i_next = 0, len; int state = 0; int old_cpu, this_cpu; @@ -426,9 +426,7 @@ void panic(const char *fmt, ...) console_verbose(); bust_spinlocks(1); - va_start(args, fmt); len = vscnprintf(buf, sizeof(buf), fmt, args); - va_end(args); if (len && buf[len - 1] == '\n') buf[len - 1] = '\0'; @@ -565,7 +563,17 @@ void panic(const char *fmt, ...) mdelay(PANIC_TIMER_STEP); } } +EXPORT_SYMBOL(vpanic); +/* Identical to vpanic(), except it takes variadic arguments instead of va_list */ +void panic(const char *fmt, ...) +{ + va_list args; + + va_start(args, fmt); + vpanic(fmt, args); + va_end(args); +} EXPORT_SYMBOL(panic); #define TAINT_FLAG(taint, _c_true, _c_false, _module) \ diff --git a/kernel/printk/internal.h b/kernel/printk/internal.h index 48a24e7b309d..bbed41ad29cf 100644 --- a/kernel/printk/internal.h +++ b/kernel/printk/internal.h @@ -72,7 +72,6 @@ int vprintk_store(int facility, int level, const char *fmt, va_list args); __printf(1, 0) int vprintk_default(const char *fmt, va_list args); -__printf(1, 0) int vprintk_deferred(const char *fmt, va_list args); void __printk_safe_enter(void); void __printk_safe_exit(void); diff --git a/kernel/sched/core.c b/kernel/sched/core.c index 3ec00d08d46a..66d93a872968 100644 --- a/kernel/sched/core.c +++ b/kernel/sched/core.c @@ -1113,6 +1113,7 @@ static void __resched_curr(struct rq *rq, int tif) cpu = cpu_of(rq); + trace_sched_set_need_resched_tp(curr, cpu, tif); if (cpu == smp_processor_id()) { set_ti_thread_flag(cti, tif); if (tif == TIF_NEED_RESCHED) @@ -1128,6 +1129,11 @@ static void __resched_curr(struct rq *rq, int tif) } } +void __trace_set_need_resched(struct task_struct *curr, int tif) +{ + trace_sched_set_need_resched_tp(curr, smp_processor_id(), tif); +} + void resched_curr(struct rq *rq) { __resched_curr(rq, TIF_NEED_RESCHED); @@ -5279,7 +5285,7 @@ asmlinkage __visible void schedule_tail(struct task_struct *prev) * switched the context for the first time. It is returning from * schedule for the first time in this path. */ - trace_sched_exit_tp(true, CALLER_ADDR0); + trace_sched_exit_tp(true); preempt_enable(); if (current->set_child_tid) @@ -6822,7 +6828,8 @@ static void __sched notrace __schedule(int sched_mode) struct rq *rq; int cpu; - trace_sched_entry_tp(preempt, CALLER_ADDR0); + /* Trace preemptions consistently with task switches */ + trace_sched_entry_tp(sched_mode == SM_PREEMPT); cpu = smp_processor_id(); rq = cpu_rq(cpu); @@ -6961,7 +6968,7 @@ keep_resched: __balance_callbacks(rq); raw_spin_rq_unlock_irq(rq); } - trace_sched_exit_tp(is_switch, CALLER_ADDR0); + trace_sched_exit_tp(is_switch); } void __noreturn do_task_dead(void) diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index b39f36013ef2..5b4be87ba59d 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -1,19 +1,31 @@ # SPDX-License-Identifier: GPL-2.0-only # -config DA_MON_EVENTS +config RV_MON_EVENTS + bool + +config RV_MON_MAINTENANCE_EVENTS bool config DA_MON_EVENTS_IMPLICIT - select DA_MON_EVENTS + select RV_MON_EVENTS + select RV_MON_MAINTENANCE_EVENTS bool config DA_MON_EVENTS_ID - select DA_MON_EVENTS + select RV_MON_EVENTS + select RV_MON_MAINTENANCE_EVENTS + bool + +config LTL_MON_EVENTS_ID + select RV_MON_EVENTS + bool + +config RV_LTL_MONITOR bool menuconfig RV bool "Runtime Verification" - depends on TRACING + select TRACING help Enable the kernel runtime verification infrastructure. RV is a lightweight (yet rigorous) method that complements classical @@ -25,15 +37,34 @@ menuconfig RV For further information, see: Documentation/trace/rv/runtime-verification.rst +config RV_PER_TASK_MONITORS + int "Maximum number of per-task monitor" + depends on RV + range 1 8 + default 2 + help + This option configures the maximum number of per-task RV monitors that can run + simultaneously. + source "kernel/trace/rv/monitors/wip/Kconfig" source "kernel/trace/rv/monitors/wwnr/Kconfig" + source "kernel/trace/rv/monitors/sched/Kconfig" -source "kernel/trace/rv/monitors/tss/Kconfig" source "kernel/trace/rv/monitors/sco/Kconfig" source "kernel/trace/rv/monitors/snroc/Kconfig" source "kernel/trace/rv/monitors/scpd/Kconfig" source "kernel/trace/rv/monitors/snep/Kconfig" -source "kernel/trace/rv/monitors/sncid/Kconfig" +source "kernel/trace/rv/monitors/sts/Kconfig" +source "kernel/trace/rv/monitors/nrp/Kconfig" +source "kernel/trace/rv/monitors/sssw/Kconfig" +source "kernel/trace/rv/monitors/opid/Kconfig" +# Add new sched monitors here + +source "kernel/trace/rv/monitors/rtapp/Kconfig" +source "kernel/trace/rv/monitors/pagefault/Kconfig" +source "kernel/trace/rv/monitors/sleep/Kconfig" +# Add new rtapp monitors here + # Add new monitors here config RV_REACTORS diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index f9b2cd0483c3..750e4ad6fa0f 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -6,12 +6,17 @@ obj-$(CONFIG_RV) += rv.o obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o obj-$(CONFIG_RV_MON_SCHED) += monitors/sched/sched.o -obj-$(CONFIG_RV_MON_TSS) += monitors/tss/tss.o obj-$(CONFIG_RV_MON_SCO) += monitors/sco/sco.o obj-$(CONFIG_RV_MON_SNROC) += monitors/snroc/snroc.o obj-$(CONFIG_RV_MON_SCPD) += monitors/scpd/scpd.o obj-$(CONFIG_RV_MON_SNEP) += monitors/snep/snep.o -obj-$(CONFIG_RV_MON_SNCID) += monitors/sncid/sncid.o +obj-$(CONFIG_RV_MON_RTAPP) += monitors/rtapp/rtapp.o +obj-$(CONFIG_RV_MON_PAGEFAULT) += monitors/pagefault/pagefault.o +obj-$(CONFIG_RV_MON_SLEEP) += monitors/sleep/sleep.o +obj-$(CONFIG_RV_MON_STS) += monitors/sts/sts.o +obj-$(CONFIG_RV_MON_NRP) += monitors/nrp/nrp.o +obj-$(CONFIG_RV_MON_SSSW) += monitors/sssw/sssw.o +obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o # Add new monitors here obj-$(CONFIG_RV_REACTORS) += rv_reactors.o obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o diff --git a/kernel/trace/rv/monitors/tss/Kconfig b/kernel/trace/rv/monitors/nrp/Kconfig index 479f86f52e60..f5ec08f65535 100644 --- a/kernel/trace/rv/monitors/tss/Kconfig +++ b/kernel/trace/rv/monitors/nrp/Kconfig @@ -1,14 +1,16 @@ # SPDX-License-Identifier: GPL-2.0-only # -config RV_MON_TSS +config RV_MON_NRP depends on RV depends on RV_MON_SCHED - default y - select DA_MON_EVENTS_IMPLICIT - bool "tss monitor" + default y if !ARM64 + select DA_MON_EVENTS_ID + bool "nrp monitor" help - Monitor to ensure sched_switch happens only in scheduling context. + Monitor to ensure preemption requires need resched. This monitor is part of the sched monitors collection. + This monitor is unstable on arm64, say N unless you are testing it. + For further information, see: Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/nrp/nrp.c b/kernel/trace/rv/monitors/nrp/nrp.c new file mode 100644 index 000000000000..5a83b7171432 --- /dev/null +++ b/kernel/trace/rv/monitors/nrp/nrp.c @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> +#include <rv/da_monitor.h> + +#define MODULE_NAME "nrp" + +#include <trace/events/irq.h> +#include <trace/events/sched.h> +#include <rv_trace.h> +#include <monitors/sched/sched.h> + +#include "nrp.h" + +static struct rv_monitor rv_nrp; +DECLARE_DA_MON_PER_TASK(nrp, unsigned char); + +#ifdef CONFIG_X86_LOCAL_APIC +#include <asm/trace/irq_vectors.h> + +static void handle_vector_irq_entry(void *data, int vector) +{ + da_handle_event_nrp(current, irq_entry_nrp); +} + +static void attach_vector_irq(void) +{ + rv_attach_trace_probe("nrp", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_attach_trace_probe("nrp", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_attach_trace_probe("nrp", reschedule_entry, handle_vector_irq_entry); + rv_attach_trace_probe("nrp", call_function_entry, handle_vector_irq_entry); + rv_attach_trace_probe("nrp", call_function_single_entry, handle_vector_irq_entry); + } +} + +static void detach_vector_irq(void) +{ + rv_detach_trace_probe("nrp", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_detach_trace_probe("nrp", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_detach_trace_probe("nrp", reschedule_entry, handle_vector_irq_entry); + rv_detach_trace_probe("nrp", call_function_entry, handle_vector_irq_entry); + rv_detach_trace_probe("nrp", call_function_single_entry, handle_vector_irq_entry); + } +} + +#else +/* We assume irq_entry tracepoints are sufficient on other architectures */ +static void attach_vector_irq(void) { } +static void detach_vector_irq(void) { } +#endif + +static void handle_irq_entry(void *data, int irq, struct irqaction *action) +{ + da_handle_event_nrp(current, irq_entry_nrp); +} + +static void handle_sched_need_resched(void *data, struct task_struct *tsk, + int cpu, int tif) +{ + /* + * Although need_resched leads to both the rescheduling and preempt_irq + * states, it is safer to start the monitor always in preempt_irq, + * which may not mirror the system state but makes the monitor simpler, + */ + if (tif == TIF_NEED_RESCHED) + da_handle_start_event_nrp(tsk, sched_need_resched_nrp); +} + +static void handle_schedule_entry(void *data, bool preempt) +{ + if (preempt) + da_handle_event_nrp(current, schedule_entry_preempt_nrp); + else + da_handle_event_nrp(current, schedule_entry_nrp); +} + +static int enable_nrp(void) +{ + int retval; + + retval = da_monitor_init_nrp(); + if (retval) + return retval; + + rv_attach_trace_probe("nrp", irq_handler_entry, handle_irq_entry); + rv_attach_trace_probe("nrp", sched_set_need_resched_tp, handle_sched_need_resched); + rv_attach_trace_probe("nrp", sched_entry_tp, handle_schedule_entry); + attach_vector_irq(); + + return 0; +} + +static void disable_nrp(void) +{ + rv_nrp.enabled = 0; + + rv_detach_trace_probe("nrp", irq_handler_entry, handle_irq_entry); + rv_detach_trace_probe("nrp", sched_set_need_resched_tp, handle_sched_need_resched); + rv_detach_trace_probe("nrp", sched_entry_tp, handle_schedule_entry); + detach_vector_irq(); + + da_monitor_destroy_nrp(); +} + +static struct rv_monitor rv_nrp = { + .name = "nrp", + .description = "need resched preempts.", + .enable = enable_nrp, + .disable = disable_nrp, + .reset = da_monitor_reset_all_nrp, + .enabled = 0, +}; + +static int __init register_nrp(void) +{ + return rv_register_monitor(&rv_nrp, &rv_sched); +} + +static void __exit unregister_nrp(void) +{ + rv_unregister_monitor(&rv_nrp); +} + +module_init(register_nrp); +module_exit(unregister_nrp); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); +MODULE_DESCRIPTION("nrp: need resched preempts."); diff --git a/kernel/trace/rv/monitors/nrp/nrp.h b/kernel/trace/rv/monitors/nrp/nrp.h new file mode 100644 index 000000000000..c9f12207cbf6 --- /dev/null +++ b/kernel/trace/rv/monitors/nrp/nrp.h @@ -0,0 +1,75 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of nrp automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +enum states_nrp { + preempt_irq_nrp = 0, + any_thread_running_nrp, + nested_preempt_nrp, + rescheduling_nrp, + state_max_nrp +}; + +#define INVALID_STATE state_max_nrp + +enum events_nrp { + irq_entry_nrp = 0, + sched_need_resched_nrp, + schedule_entry_nrp, + schedule_entry_preempt_nrp, + event_max_nrp +}; + +struct automaton_nrp { + char *state_names[state_max_nrp]; + char *event_names[event_max_nrp]; + unsigned char function[state_max_nrp][event_max_nrp]; + unsigned char initial_state; + bool final_states[state_max_nrp]; +}; + +static const struct automaton_nrp automaton_nrp = { + .state_names = { + "preempt_irq", + "any_thread_running", + "nested_preempt", + "rescheduling" + }, + .event_names = { + "irq_entry", + "sched_need_resched", + "schedule_entry", + "schedule_entry_preempt" + }, + .function = { + { + preempt_irq_nrp, + preempt_irq_nrp, + nested_preempt_nrp, + nested_preempt_nrp + }, + { + any_thread_running_nrp, + rescheduling_nrp, + any_thread_running_nrp, + INVALID_STATE + }, + { + nested_preempt_nrp, + preempt_irq_nrp, + any_thread_running_nrp, + any_thread_running_nrp + }, + { + preempt_irq_nrp, + rescheduling_nrp, + any_thread_running_nrp, + any_thread_running_nrp + }, + }, + .initial_state = preempt_irq_nrp, + .final_states = { 0, 1, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/nrp/nrp_trace.h b/kernel/trace/rv/monitors/nrp/nrp_trace.h new file mode 100644 index 000000000000..2e13497de3b6 --- /dev/null +++ b/kernel/trace/rv/monitors/nrp/nrp_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_NRP +DEFINE_EVENT(event_da_monitor_id, event_nrp, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_nrp, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_NRP */ diff --git a/kernel/trace/rv/monitors/opid/Kconfig b/kernel/trace/rv/monitors/opid/Kconfig new file mode 100644 index 000000000000..561d32da572b --- /dev/null +++ b/kernel/trace/rv/monitors/opid/Kconfig @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_OPID + depends on RV + depends on TRACE_IRQFLAGS + depends on TRACE_PREEMPT_TOGGLE + depends on RV_MON_SCHED + default y if PREEMPT_RT + select DA_MON_EVENTS_IMPLICIT + bool "opid monitor" + help + Monitor to ensure operations like wakeup and need resched occur with + interrupts and preemption disabled or during IRQs, where preemption + may not be disabled explicitly. + + This monitor is unstable on !PREEMPT_RT, say N unless you are testing it. + + For further information, see: + Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/opid/opid.c b/kernel/trace/rv/monitors/opid/opid.c new file mode 100644 index 000000000000..50d64e7fb8c4 --- /dev/null +++ b/kernel/trace/rv/monitors/opid/opid.c @@ -0,0 +1,168 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> +#include <rv/da_monitor.h> + +#define MODULE_NAME "opid" + +#include <trace/events/sched.h> +#include <trace/events/irq.h> +#include <trace/events/preemptirq.h> +#include <rv_trace.h> +#include <monitors/sched/sched.h> + +#include "opid.h" + +static struct rv_monitor rv_opid; +DECLARE_DA_MON_PER_CPU(opid, unsigned char); + +#ifdef CONFIG_X86_LOCAL_APIC +#include <asm/trace/irq_vectors.h> + +static void handle_vector_irq_entry(void *data, int vector) +{ + da_handle_event_opid(irq_entry_opid); +} + +static void attach_vector_irq(void) +{ + rv_attach_trace_probe("opid", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_attach_trace_probe("opid", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_attach_trace_probe("opid", reschedule_entry, handle_vector_irq_entry); + rv_attach_trace_probe("opid", call_function_entry, handle_vector_irq_entry); + rv_attach_trace_probe("opid", call_function_single_entry, handle_vector_irq_entry); + } +} + +static void detach_vector_irq(void) +{ + rv_detach_trace_probe("opid", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_detach_trace_probe("opid", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_detach_trace_probe("opid", reschedule_entry, handle_vector_irq_entry); + rv_detach_trace_probe("opid", call_function_entry, handle_vector_irq_entry); + rv_detach_trace_probe("opid", call_function_single_entry, handle_vector_irq_entry); + } +} + +#else +/* We assume irq_entry tracepoints are sufficient on other architectures */ +static void attach_vector_irq(void) { } +static void detach_vector_irq(void) { } +#endif + +static void handle_irq_disable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_opid(irq_disable_opid); +} + +static void handle_irq_enable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_opid(irq_enable_opid); +} + +static void handle_irq_entry(void *data, int irq, struct irqaction *action) +{ + da_handle_event_opid(irq_entry_opid); +} + +static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_opid(preempt_disable_opid); +} + +static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_opid(preempt_enable_opid); +} + +static void handle_sched_need_resched(void *data, struct task_struct *tsk, int cpu, int tif) +{ + /* The monitor's intitial state is not in_irq */ + if (this_cpu_read(hardirq_context)) + da_handle_event_opid(sched_need_resched_opid); + else + da_handle_start_event_opid(sched_need_resched_opid); +} + +static void handle_sched_waking(void *data, struct task_struct *p) +{ + /* The monitor's intitial state is not in_irq */ + if (this_cpu_read(hardirq_context)) + da_handle_event_opid(sched_waking_opid); + else + da_handle_start_event_opid(sched_waking_opid); +} + +static int enable_opid(void) +{ + int retval; + + retval = da_monitor_init_opid(); + if (retval) + return retval; + + rv_attach_trace_probe("opid", irq_disable, handle_irq_disable); + rv_attach_trace_probe("opid", irq_enable, handle_irq_enable); + rv_attach_trace_probe("opid", irq_handler_entry, handle_irq_entry); + rv_attach_trace_probe("opid", preempt_disable, handle_preempt_disable); + rv_attach_trace_probe("opid", preempt_enable, handle_preempt_enable); + rv_attach_trace_probe("opid", sched_set_need_resched_tp, handle_sched_need_resched); + rv_attach_trace_probe("opid", sched_waking, handle_sched_waking); + attach_vector_irq(); + + return 0; +} + +static void disable_opid(void) +{ + rv_opid.enabled = 0; + + rv_detach_trace_probe("opid", irq_disable, handle_irq_disable); + rv_detach_trace_probe("opid", irq_enable, handle_irq_enable); + rv_detach_trace_probe("opid", irq_handler_entry, handle_irq_entry); + rv_detach_trace_probe("opid", preempt_disable, handle_preempt_disable); + rv_detach_trace_probe("opid", preempt_enable, handle_preempt_enable); + rv_detach_trace_probe("opid", sched_set_need_resched_tp, handle_sched_need_resched); + rv_detach_trace_probe("opid", sched_waking, handle_sched_waking); + detach_vector_irq(); + + da_monitor_destroy_opid(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_opid = { + .name = "opid", + .description = "operations with preemption and irq disabled.", + .enable = enable_opid, + .disable = disable_opid, + .reset = da_monitor_reset_all_opid, + .enabled = 0, +}; + +static int __init register_opid(void) +{ + return rv_register_monitor(&rv_opid, &rv_sched); +} + +static void __exit unregister_opid(void) +{ + rv_unregister_monitor(&rv_opid); +} + +module_init(register_opid); +module_exit(unregister_opid); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); +MODULE_DESCRIPTION("opid: operations with preemption and irq disabled."); diff --git a/kernel/trace/rv/monitors/opid/opid.h b/kernel/trace/rv/monitors/opid/opid.h new file mode 100644 index 000000000000..b4b8c2ff7f64 --- /dev/null +++ b/kernel/trace/rv/monitors/opid/opid.h @@ -0,0 +1,104 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of opid automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +enum states_opid { + disabled_opid = 0, + enabled_opid, + in_irq_opid, + irq_disabled_opid, + preempt_disabled_opid, + state_max_opid +}; + +#define INVALID_STATE state_max_opid + +enum events_opid { + irq_disable_opid = 0, + irq_enable_opid, + irq_entry_opid, + preempt_disable_opid, + preempt_enable_opid, + sched_need_resched_opid, + sched_waking_opid, + event_max_opid +}; + +struct automaton_opid { + char *state_names[state_max_opid]; + char *event_names[event_max_opid]; + unsigned char function[state_max_opid][event_max_opid]; + unsigned char initial_state; + bool final_states[state_max_opid]; +}; + +static const struct automaton_opid automaton_opid = { + .state_names = { + "disabled", + "enabled", + "in_irq", + "irq_disabled", + "preempt_disabled" + }, + .event_names = { + "irq_disable", + "irq_enable", + "irq_entry", + "preempt_disable", + "preempt_enable", + "sched_need_resched", + "sched_waking" + }, + .function = { + { + INVALID_STATE, + preempt_disabled_opid, + disabled_opid, + INVALID_STATE, + irq_disabled_opid, + disabled_opid, + disabled_opid + }, + { + irq_disabled_opid, + INVALID_STATE, + INVALID_STATE, + preempt_disabled_opid, + enabled_opid, + INVALID_STATE, + INVALID_STATE + }, + { + INVALID_STATE, + enabled_opid, + in_irq_opid, + INVALID_STATE, + INVALID_STATE, + in_irq_opid, + in_irq_opid + }, + { + INVALID_STATE, + enabled_opid, + in_irq_opid, + disabled_opid, + INVALID_STATE, + irq_disabled_opid, + INVALID_STATE + }, + { + disabled_opid, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + enabled_opid, + INVALID_STATE, + INVALID_STATE + }, + }, + .initial_state = disabled_opid, + .final_states = { 0, 1, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/sncid/sncid_trace.h b/kernel/trace/rv/monitors/opid/opid_trace.h index 3ce42a57671d..3df6ff955c30 100644 --- a/kernel/trace/rv/monitors/sncid/sncid_trace.h +++ b/kernel/trace/rv/monitors/opid/opid_trace.h @@ -4,12 +4,12 @@ * Snippet to be included in rv_trace.h */ -#ifdef CONFIG_RV_MON_SNCID -DEFINE_EVENT(event_da_monitor, event_sncid, +#ifdef CONFIG_RV_MON_OPID +DEFINE_EVENT(event_da_monitor, event_opid, TP_PROTO(char *state, char *event, char *next_state, bool final_state), TP_ARGS(state, event, next_state, final_state)); -DEFINE_EVENT(error_da_monitor, error_sncid, +DEFINE_EVENT(error_da_monitor, error_opid, TP_PROTO(char *state, char *event), TP_ARGS(state, event)); -#endif /* CONFIG_RV_MON_SNCID */ +#endif /* CONFIG_RV_MON_OPID */ diff --git a/kernel/trace/rv/monitors/pagefault/Kconfig b/kernel/trace/rv/monitors/pagefault/Kconfig new file mode 100644 index 000000000000..5e16625f1653 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/Kconfig @@ -0,0 +1,20 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_PAGEFAULT + depends on RV + select RV_LTL_MONITOR + depends on RV_MON_RTAPP + depends on X86 || RISCV + default y + select LTL_MON_EVENTS_ID + bool "pagefault monitor" + help + Monitor that real-time tasks do not raise page faults, causing + undesirable latency. + + If you are developing a real-time system and not entirely sure whether + the applications are designed correctly for real-time, you want to say + Y here. + + This monitor does not affect execution speed while it is not running, + therefore it is safe to enable this in production kernel. diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.c b/kernel/trace/rv/monitors/pagefault/pagefault.c new file mode 100644 index 000000000000..9fe6123b2200 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault.c @@ -0,0 +1,88 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/init.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/rv.h> +#include <linux/sched/deadline.h> +#include <linux/sched/rt.h> +#include <linux/tracepoint.h> +#include <rv/instrumentation.h> + +#define MODULE_NAME "pagefault" + +#include <rv_trace.h> +#include <trace/events/exceptions.h> +#include <monitors/rtapp/rtapp.h> + +#include "pagefault.h" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + /* + * This includes "actual" real-time tasks and also PI-boosted + * tasks. A task being PI-boosted means it is blocking an "actual" + * real-task, therefore it should also obey the monitor's rule, + * otherwise the "actual" real-task may be delayed. + */ + ltl_atom_set(mon, LTL_RT, rt_or_dl_task(task)); +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + if (task_creation) + ltl_atom_set(mon, LTL_PAGEFAULT, false); +} + +static void handle_page_fault(void *data, unsigned long address, struct pt_regs *regs, + unsigned long error_code) +{ + ltl_atom_pulse(current, LTL_PAGEFAULT, true); +} + +static int enable_pagefault(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault); + rv_attach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault); + + return 0; +} + +static void disable_pagefault(void) +{ + rv_detach_trace_probe("rtapp_pagefault", page_fault_kernel, handle_page_fault); + rv_detach_trace_probe("rtapp_pagefault", page_fault_user, handle_page_fault); + + ltl_monitor_destroy(); +} + +static struct rv_monitor rv_pagefault = { + .name = "pagefault", + .description = "Monitor that RT tasks do not raise page faults", + .enable = enable_pagefault, + .disable = disable_pagefault, +}; + +static int __init register_pagefault(void) +{ + return rv_register_monitor(&rv_pagefault, &rv_rtapp); +} + +static void __exit unregister_pagefault(void) +{ + rv_unregister_monitor(&rv_pagefault); +} + +module_init(register_pagefault); +module_exit(unregister_pagefault); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>"); +MODULE_DESCRIPTION("pagefault: Monitor that RT tasks do not raise page faults"); diff --git a/kernel/trace/rv/monitors/pagefault/pagefault.h b/kernel/trace/rv/monitors/pagefault/pagefault.h new file mode 100644 index 000000000000..c580ec194009 --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault.h @@ -0,0 +1,64 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * C implementation of Buchi automaton, automatically generated by + * tools/verification/rvgen from the linear temporal logic specification. + * For further information, see kernel documentation: + * Documentation/trace/rv/linear_temporal_logic.rst + */ + +#include <linux/rv.h> + +#define MONITOR_NAME pagefault + +enum ltl_atom { + LTL_PAGEFAULT, + LTL_RT, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "pa", + "rt", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); + bool val3 = !pagefault; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val4 = val1 || val3; + + if (val4) + __set_bit(S0, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms); + bool val3 = !pagefault; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val4 = val1 || val3; + + switch (state) { + case S0: + if (val4) + __set_bit(S0, next); + break; + } +} diff --git a/kernel/trace/rv/monitors/pagefault/pagefault_trace.h b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h new file mode 100644 index 000000000000..fe1f82597b1a --- /dev/null +++ b/kernel/trace/rv/monitors/pagefault/pagefault_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_PAGEFAULT +DEFINE_EVENT(event_ltl_monitor_id, event_pagefault, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_pagefault, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_PAGEFAULT */ diff --git a/kernel/trace/rv/monitors/rtapp/Kconfig b/kernel/trace/rv/monitors/rtapp/Kconfig new file mode 100644 index 000000000000..1ce9370a9ba8 --- /dev/null +++ b/kernel/trace/rv/monitors/rtapp/Kconfig @@ -0,0 +1,11 @@ +config RV_MON_RTAPP + depends on RV + depends on RV_PER_TASK_MONITORS >= 2 + bool "rtapp monitor" + help + Collection of monitors to check for common problems with real-time + application that may cause unexpected latency. + + If you are developing a real-time system and not entirely sure whether + the applications are designed correctly for real-time, you want to say + Y here. diff --git a/kernel/trace/rv/monitors/rtapp/rtapp.c b/kernel/trace/rv/monitors/rtapp/rtapp.c new file mode 100644 index 000000000000..fd75fc927d65 --- /dev/null +++ b/kernel/trace/rv/monitors/rtapp/rtapp.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> + +#define MODULE_NAME "rtapp" + +#include "rtapp.h" + +struct rv_monitor rv_rtapp; + +struct rv_monitor rv_rtapp = { + .name = "rtapp", + .description = "Collection of monitors for detecting problems with real-time applications", +}; + +static int __init register_rtapp(void) +{ + return rv_register_monitor(&rv_rtapp, NULL); +} + +static void __exit unregister_rtapp(void) +{ + rv_unregister_monitor(&rv_rtapp); +} + +module_init(register_rtapp); +module_exit(unregister_rtapp); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>"); +MODULE_DESCRIPTION("Collection of monitors for detecting problems with real-time applications"); diff --git a/kernel/trace/rv/monitors/rtapp/rtapp.h b/kernel/trace/rv/monitors/rtapp/rtapp.h new file mode 100644 index 000000000000..4c200d67c7f6 --- /dev/null +++ b/kernel/trace/rv/monitors/rtapp/rtapp.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_rtapp; diff --git a/kernel/trace/rv/monitors/sched/Kconfig b/kernel/trace/rv/monitors/sched/Kconfig index ae3eb410abd7..aa16456da864 100644 --- a/kernel/trace/rv/monitors/sched/Kconfig +++ b/kernel/trace/rv/monitors/sched/Kconfig @@ -2,6 +2,7 @@ # config RV_MON_SCHED depends on RV + depends on RV_PER_TASK_MONITORS >= 3 bool "sched monitor" help Collection of monitors to check the scheduler behaves according to specifications. diff --git a/kernel/trace/rv/monitors/sched/sched.c b/kernel/trace/rv/monitors/sched/sched.c index 905e03c3c934..d04db4b543f9 100644 --- a/kernel/trace/rv/monitors/sched/sched.c +++ b/kernel/trace/rv/monitors/sched/sched.c @@ -21,8 +21,7 @@ struct rv_monitor rv_sched = { static int __init register_sched(void) { - rv_register_monitor(&rv_sched, NULL); - return 0; + return rv_register_monitor(&rv_sched, NULL); } static void __exit unregister_sched(void) diff --git a/kernel/trace/rv/monitors/sco/sco.c b/kernel/trace/rv/monitors/sco/sco.c index 4cff59220bfc..04c36405e2e3 100644 --- a/kernel/trace/rv/monitors/sco/sco.c +++ b/kernel/trace/rv/monitors/sco/sco.c @@ -24,12 +24,12 @@ static void handle_sched_set_state(void *data, struct task_struct *tsk, int stat da_handle_start_event_sco(sched_set_state_sco); } -static void handle_schedule_entry(void *data, bool preempt, unsigned long ip) +static void handle_schedule_entry(void *data, bool preempt) { da_handle_event_sco(schedule_entry_sco); } -static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip) +static void handle_schedule_exit(void *data, bool is_switch) { da_handle_start_event_sco(schedule_exit_sco); } @@ -71,8 +71,7 @@ static struct rv_monitor rv_sco = { static int __init register_sco(void) { - rv_register_monitor(&rv_sco, &rv_sched); - return 0; + return rv_register_monitor(&rv_sco, &rv_sched); } static void __exit unregister_sco(void) diff --git a/kernel/trace/rv/monitors/scpd/Kconfig b/kernel/trace/rv/monitors/scpd/Kconfig index b9114fbf680f..682d0416188b 100644 --- a/kernel/trace/rv/monitors/scpd/Kconfig +++ b/kernel/trace/rv/monitors/scpd/Kconfig @@ -2,7 +2,7 @@ # config RV_MON_SCPD depends on RV - depends on PREEMPT_TRACER + depends on TRACE_PREEMPT_TOGGLE depends on RV_MON_SCHED default y select DA_MON_EVENTS_IMPLICIT diff --git a/kernel/trace/rv/monitors/scpd/scpd.c b/kernel/trace/rv/monitors/scpd/scpd.c index cbdd6a5f8d7f..1e351ba52fee 100644 --- a/kernel/trace/rv/monitors/scpd/scpd.c +++ b/kernel/trace/rv/monitors/scpd/scpd.c @@ -30,12 +30,12 @@ static void handle_preempt_enable(void *data, unsigned long ip, unsigned long pa da_handle_start_event_scpd(preempt_enable_scpd); } -static void handle_schedule_entry(void *data, bool preempt, unsigned long ip) +static void handle_schedule_entry(void *data, bool preempt) { da_handle_event_scpd(schedule_entry_scpd); } -static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip) +static void handle_schedule_exit(void *data, bool is_switch) { da_handle_event_scpd(schedule_exit_scpd); } @@ -79,8 +79,7 @@ static struct rv_monitor rv_scpd = { static int __init register_scpd(void) { - rv_register_monitor(&rv_scpd, &rv_sched); - return 0; + return rv_register_monitor(&rv_scpd, &rv_sched); } static void __exit unregister_scpd(void) diff --git a/kernel/trace/rv/monitors/sleep/Kconfig b/kernel/trace/rv/monitors/sleep/Kconfig new file mode 100644 index 000000000000..6b7a122e7b47 --- /dev/null +++ b/kernel/trace/rv/monitors/sleep/Kconfig @@ -0,0 +1,22 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_SLEEP + depends on RV + select RV_LTL_MONITOR + depends on HAVE_SYSCALL_TRACEPOINTS + depends on RV_MON_RTAPP + select TRACE_IRQFLAGS + default y + select LTL_MON_EVENTS_ID + bool "sleep monitor" + help + Monitor that real-time tasks do not sleep in a manner that may + cause undesirable latency. + + If you are developing a real-time system and not entirely sure whether + the applications are designed correctly for real-time, you want to say + Y here. + + Enabling this monitor may have performance impact (due to select + TRACE_IRQFLAGS). Therefore, you probably should say N for + production kernel. diff --git a/kernel/trace/rv/monitors/sleep/sleep.c b/kernel/trace/rv/monitors/sleep/sleep.c new file mode 100644 index 000000000000..eea447b06907 --- /dev/null +++ b/kernel/trace/rv/monitors/sleep/sleep.c @@ -0,0 +1,237 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/init.h> +#include <linux/irqflags.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/rv.h> +#include <linux/sched/deadline.h> +#include <linux/sched/rt.h> +#include <rv/instrumentation.h> + +#define MODULE_NAME "sleep" + +#include <trace/events/syscalls.h> +#include <trace/events/sched.h> +#include <trace/events/lock.h> +#include <uapi/linux/futex.h> +#include <rv_trace.h> +#include <monitors/rtapp/rtapp.h> + +#include "sleep.h" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + /* + * This includes "actual" real-time tasks and also PI-boosted + * tasks. A task being PI-boosted means it is blocking an "actual" + * real-task, therefore it should also obey the monitor's rule, + * otherwise the "actual" real-task may be delayed. + */ + ltl_atom_set(mon, LTL_RT, rt_or_dl_task(task)); +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + ltl_atom_set(mon, LTL_SLEEP, false); + ltl_atom_set(mon, LTL_WAKE, false); + ltl_atom_set(mon, LTL_ABORT_SLEEP, false); + ltl_atom_set(mon, LTL_WOKEN_BY_HARDIRQ, false); + ltl_atom_set(mon, LTL_WOKEN_BY_NMI, false); + ltl_atom_set(mon, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, false); + + if (task_creation) { + ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); + ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); + ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false); + ltl_atom_set(mon, LTL_FUTEX_WAIT, false); + ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false); + ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false); + } + + if (task->flags & PF_KTHREAD) { + ltl_atom_set(mon, LTL_KERNEL_THREAD, true); + + /* kernel tasks do not do syscall */ + ltl_atom_set(mon, LTL_FUTEX_WAIT, false); + ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); + ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); + ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false); + + if (strstarts(task->comm, "migration/")) + ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, true); + else + ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false); + + if (strstarts(task->comm, "rcu")) + ltl_atom_set(mon, LTL_TASK_IS_RCU, true); + else + ltl_atom_set(mon, LTL_TASK_IS_RCU, false); + } else { + ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false); + ltl_atom_set(mon, LTL_KERNEL_THREAD, false); + ltl_atom_set(mon, LTL_TASK_IS_RCU, false); + ltl_atom_set(mon, LTL_TASK_IS_MIGRATION, false); + } + +} + +static void handle_sched_set_state(void *data, struct task_struct *task, int state) +{ + if (state & TASK_INTERRUPTIBLE) + ltl_atom_pulse(task, LTL_SLEEP, true); + else if (state == TASK_RUNNING) + ltl_atom_pulse(task, LTL_ABORT_SLEEP, true); +} + +static void handle_sched_wakeup(void *data, struct task_struct *task) +{ + ltl_atom_pulse(task, LTL_WAKE, true); +} + +static void handle_sched_waking(void *data, struct task_struct *task) +{ + if (this_cpu_read(hardirq_context)) { + ltl_atom_pulse(task, LTL_WOKEN_BY_HARDIRQ, true); + } else if (in_task()) { + if (current->prio <= task->prio) + ltl_atom_pulse(task, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, true); + } else if (in_nmi()) { + ltl_atom_pulse(task, LTL_WOKEN_BY_NMI, true); + } +} + +static void handle_contention_begin(void *data, void *lock, unsigned int flags) +{ + if (flags & LCB_F_RT) + ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, true); +} + +static void handle_contention_end(void *data, void *lock, int ret) +{ + ltl_atom_update(current, LTL_BLOCK_ON_RT_MUTEX, false); +} + +static void handle_sys_enter(void *data, struct pt_regs *regs, long id) +{ + struct ltl_monitor *mon; + unsigned long args[6]; + int op, cmd; + + mon = ltl_get_monitor(current); + + switch (id) { + case __NR_clock_nanosleep: +#ifdef __NR_clock_nanosleep_time64 + case __NR_clock_nanosleep_time64: +#endif + syscall_get_arguments(current, regs, args); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, args[0] == CLOCK_MONOTONIC); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, args[0] == CLOCK_TAI); + ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, args[1] == TIMER_ABSTIME); + ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, true); + break; + + case __NR_futex: +#ifdef __NR_futex_time64 + case __NR_futex_time64: +#endif + syscall_get_arguments(current, regs, args); + op = args[1]; + cmd = op & FUTEX_CMD_MASK; + + switch (cmd) { + case FUTEX_LOCK_PI: + case FUTEX_LOCK_PI2: + ltl_atom_update(current, LTL_FUTEX_LOCK_PI, true); + break; + case FUTEX_WAIT: + case FUTEX_WAIT_BITSET: + case FUTEX_WAIT_REQUEUE_PI: + ltl_atom_update(current, LTL_FUTEX_WAIT, true); + break; + } + break; + } +} + +static void handle_sys_exit(void *data, struct pt_regs *regs, long ret) +{ + struct ltl_monitor *mon = ltl_get_monitor(current); + + ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false); + ltl_atom_set(mon, LTL_FUTEX_WAIT, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); + ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); + ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, false); +} + +static void handle_kthread_stop(void *data, struct task_struct *task) +{ + /* FIXME: this could race with other tracepoint handlers */ + ltl_atom_update(task, LTL_KTHREAD_SHOULD_STOP, true); +} + +static int enable_sleep(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking); + rv_attach_trace_probe("rtapp_sleep", sched_wakeup, handle_sched_wakeup); + rv_attach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state); + rv_attach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin); + rv_attach_trace_probe("rtapp_sleep", contention_end, handle_contention_end); + rv_attach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop); + rv_attach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter); + rv_attach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit); + return 0; +} + +static void disable_sleep(void) +{ + rv_detach_trace_probe("rtapp_sleep", sched_waking, handle_sched_waking); + rv_detach_trace_probe("rtapp_sleep", sched_wakeup, handle_sched_wakeup); + rv_detach_trace_probe("rtapp_sleep", sched_set_state_tp, handle_sched_set_state); + rv_detach_trace_probe("rtapp_sleep", contention_begin, handle_contention_begin); + rv_detach_trace_probe("rtapp_sleep", contention_end, handle_contention_end); + rv_detach_trace_probe("rtapp_sleep", sched_kthread_stop, handle_kthread_stop); + rv_detach_trace_probe("rtapp_sleep", sys_enter, handle_sys_enter); + rv_detach_trace_probe("rtapp_sleep", sys_exit, handle_sys_exit); + + ltl_monitor_destroy(); +} + +static struct rv_monitor rv_sleep = { + .name = "sleep", + .description = "Monitor that RT tasks do not undesirably sleep", + .enable = enable_sleep, + .disable = disable_sleep, +}; + +static int __init register_sleep(void) +{ + return rv_register_monitor(&rv_sleep, &rv_rtapp); +} + +static void __exit unregister_sleep(void) +{ + rv_unregister_monitor(&rv_sleep); +} + +module_init(register_sleep); +module_exit(unregister_sleep); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>"); +MODULE_DESCRIPTION("sleep: Monitor that RT tasks do not undesirably sleep"); diff --git a/kernel/trace/rv/monitors/sleep/sleep.h b/kernel/trace/rv/monitors/sleep/sleep.h new file mode 100644 index 000000000000..2ab46fd218d2 --- /dev/null +++ b/kernel/trace/rv/monitors/sleep/sleep.h @@ -0,0 +1,257 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * C implementation of Buchi automaton, automatically generated by + * tools/verification/rvgen from the linear temporal logic specification. + * For further information, see kernel documentation: + * Documentation/trace/rv/linear_temporal_logic.rst + */ + +#include <linux/rv.h> + +#define MONITOR_NAME sleep + +enum ltl_atom { + LTL_ABORT_SLEEP, + LTL_BLOCK_ON_RT_MUTEX, + LTL_CLOCK_NANOSLEEP, + LTL_FUTEX_LOCK_PI, + LTL_FUTEX_WAIT, + LTL_KERNEL_THREAD, + LTL_KTHREAD_SHOULD_STOP, + LTL_NANOSLEEP_CLOCK_MONOTONIC, + LTL_NANOSLEEP_CLOCK_TAI, + LTL_NANOSLEEP_TIMER_ABSTIME, + LTL_RT, + LTL_SLEEP, + LTL_TASK_IS_MIGRATION, + LTL_TASK_IS_RCU, + LTL_WAKE, + LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, + LTL_WOKEN_BY_HARDIRQ, + LTL_WOKEN_BY_NMI, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ab_sl", + "bl_on_rt_mu", + "cl_na", + "fu_lo_pi", + "fu_wa", + "ker_th", + "kth_sh_st", + "na_cl_mo", + "na_cl_ta", + "na_ti_ab", + "rt", + "sl", + "ta_mi", + "ta_rc", + "wak", + "wo_eq_hi_pr", + "wo_ha", + "wo_nm", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + S5, + S6, + S7, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms); + bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms); + bool val40 = task_is_rcu || task_is_migration; + bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); + bool val41 = futex_lock_pi || val40; + bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); + bool val5 = block_on_rt_mutex || val41; + bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms); + bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms); + bool val32 = abort_sleep || kthread_should_stop; + bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms); + bool val33 = woken_by_nmi || val32; + bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms); + bool val34 = woken_by_hardirq || val33; + bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, + mon->atoms); + bool val14 = woken_by_equal_or_higher_prio || val34; + bool wake = test_bit(LTL_WAKE, mon->atoms); + bool val13 = !wake; + bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms); + bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms); + bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); + bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai; + bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms); + bool val25 = nanosleep_timer_abstime && val24; + bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms); + bool val18 = clock_nanosleep && val25; + bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms); + bool val9 = futex_wait || val18; + bool val11 = val9 || kernel_thread; + bool sleep = test_bit(LTL_SLEEP, mon->atoms); + bool val2 = !sleep; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val3 = val1 || val2; + + if (val3) + __set_bit(S0, mon->states); + if (val11 && val13) + __set_bit(S1, mon->states); + if (val11 && val14) + __set_bit(S4, mon->states); + if (val5) + __set_bit(S5, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms); + bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms); + bool val40 = task_is_rcu || task_is_migration; + bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms); + bool val41 = futex_lock_pi || val40; + bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms); + bool val5 = block_on_rt_mutex || val41; + bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms); + bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms); + bool val32 = abort_sleep || kthread_should_stop; + bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms); + bool val33 = woken_by_nmi || val32; + bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms); + bool val34 = woken_by_hardirq || val33; + bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, + mon->atoms); + bool val14 = woken_by_equal_or_higher_prio || val34; + bool wake = test_bit(LTL_WAKE, mon->atoms); + bool val13 = !wake; + bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms); + bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms); + bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); + bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai; + bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms); + bool val25 = nanosleep_timer_abstime && val24; + bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms); + bool val18 = clock_nanosleep && val25; + bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms); + bool val9 = futex_wait || val18; + bool val11 = val9 || kernel_thread; + bool sleep = test_bit(LTL_SLEEP, mon->atoms); + bool val2 = !sleep; + bool rt = test_bit(LTL_RT, mon->atoms); + bool val1 = !rt; + bool val3 = val1 || val2; + + switch (state) { + case S0: + if (val3) + __set_bit(S0, next); + if (val11 && val13) + __set_bit(S1, next); + if (val11 && val14) + __set_bit(S4, next); + if (val5) + __set_bit(S5, next); + break; + case S1: + if (val11 && val13) + __set_bit(S1, next); + if (val13 && val3) + __set_bit(S2, next); + if (val14 && val3) + __set_bit(S3, next); + if (val11 && val14) + __set_bit(S4, next); + if (val13 && val5) + __set_bit(S6, next); + if (val14 && val5) + __set_bit(S7, next); + break; + case S2: + if (val11 && val13) + __set_bit(S1, next); + if (val13 && val3) + __set_bit(S2, next); + if (val14 && val3) + __set_bit(S3, next); + if (val11 && val14) + __set_bit(S4, next); + if (val13 && val5) + __set_bit(S6, next); + if (val14 && val5) + __set_bit(S7, next); + break; + case S3: + if (val3) + __set_bit(S0, next); + if (val11 && val13) + __set_bit(S1, next); + if (val11 && val14) + __set_bit(S4, next); + if (val5) + __set_bit(S5, next); + break; + case S4: + if (val3) + __set_bit(S0, next); + if (val11 && val13) + __set_bit(S1, next); + if (val11 && val14) + __set_bit(S4, next); + if (val5) + __set_bit(S5, next); + break; + case S5: + if (val3) + __set_bit(S0, next); + if (val11 && val13) + __set_bit(S1, next); + if (val11 && val14) + __set_bit(S4, next); + if (val5) + __set_bit(S5, next); + break; + case S6: + if (val11 && val13) + __set_bit(S1, next); + if (val13 && val3) + __set_bit(S2, next); + if (val14 && val3) + __set_bit(S3, next); + if (val11 && val14) + __set_bit(S4, next); + if (val13 && val5) + __set_bit(S6, next); + if (val14 && val5) + __set_bit(S7, next); + break; + case S7: + if (val3) + __set_bit(S0, next); + if (val11 && val13) + __set_bit(S1, next); + if (val11 && val14) + __set_bit(S4, next); + if (val5) + __set_bit(S5, next); + break; + } +} diff --git a/kernel/trace/rv/monitors/sleep/sleep_trace.h b/kernel/trace/rv/monitors/sleep/sleep_trace.h new file mode 100644 index 000000000000..22eaf31da987 --- /dev/null +++ b/kernel/trace/rv/monitors/sleep/sleep_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_SLEEP +DEFINE_EVENT(event_ltl_monitor_id, event_sleep, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_sleep, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_SLEEP */ diff --git a/kernel/trace/rv/monitors/sncid/sncid.c b/kernel/trace/rv/monitors/sncid/sncid.c deleted file mode 100644 index f5037cd6214c..000000000000 --- a/kernel/trace/rv/monitors/sncid/sncid.c +++ /dev/null @@ -1,96 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "sncid" - -#include <trace/events/sched.h> -#include <trace/events/preemptirq.h> -#include <rv_trace.h> -#include <monitors/sched/sched.h> - -#include "sncid.h" - -static struct rv_monitor rv_sncid; -DECLARE_DA_MON_PER_CPU(sncid, unsigned char); - -static void handle_irq_disable(void *data, unsigned long ip, unsigned long parent_ip) -{ - da_handle_event_sncid(irq_disable_sncid); -} - -static void handle_irq_enable(void *data, unsigned long ip, unsigned long parent_ip) -{ - da_handle_start_event_sncid(irq_enable_sncid); -} - -static void handle_schedule_entry(void *data, bool preempt, unsigned long ip) -{ - da_handle_start_event_sncid(schedule_entry_sncid); -} - -static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip) -{ - da_handle_start_event_sncid(schedule_exit_sncid); -} - -static int enable_sncid(void) -{ - int retval; - - retval = da_monitor_init_sncid(); - if (retval) - return retval; - - rv_attach_trace_probe("sncid", irq_disable, handle_irq_disable); - rv_attach_trace_probe("sncid", irq_enable, handle_irq_enable); - rv_attach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry); - rv_attach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit); - - return 0; -} - -static void disable_sncid(void) -{ - rv_sncid.enabled = 0; - - rv_detach_trace_probe("sncid", irq_disable, handle_irq_disable); - rv_detach_trace_probe("sncid", irq_enable, handle_irq_enable); - rv_detach_trace_probe("sncid", sched_entry_tp, handle_schedule_entry); - rv_detach_trace_probe("sncid", sched_exit_tp, handle_schedule_exit); - - da_monitor_destroy_sncid(); -} - -static struct rv_monitor rv_sncid = { - .name = "sncid", - .description = "schedule not called with interrupt disabled.", - .enable = enable_sncid, - .disable = disable_sncid, - .reset = da_monitor_reset_all_sncid, - .enabled = 0, -}; - -static int __init register_sncid(void) -{ - rv_register_monitor(&rv_sncid, &rv_sched); - return 0; -} - -static void __exit unregister_sncid(void) -{ - rv_unregister_monitor(&rv_sncid); -} - -module_init(register_sncid); -module_exit(unregister_sncid); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); -MODULE_DESCRIPTION("sncid: schedule not called with interrupt disabled."); diff --git a/kernel/trace/rv/monitors/sncid/sncid.h b/kernel/trace/rv/monitors/sncid/sncid.h deleted file mode 100644 index 21304725142b..000000000000 --- a/kernel/trace/rv/monitors/sncid/sncid.h +++ /dev/null @@ -1,49 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ -/* - * Automatically generated C representation of sncid automaton - * For further information about this format, see kernel documentation: - * Documentation/trace/rv/deterministic_automata.rst - */ - -enum states_sncid { - can_sched_sncid = 0, - cant_sched_sncid, - state_max_sncid -}; - -#define INVALID_STATE state_max_sncid - -enum events_sncid { - irq_disable_sncid = 0, - irq_enable_sncid, - schedule_entry_sncid, - schedule_exit_sncid, - event_max_sncid -}; - -struct automaton_sncid { - char *state_names[state_max_sncid]; - char *event_names[event_max_sncid]; - unsigned char function[state_max_sncid][event_max_sncid]; - unsigned char initial_state; - bool final_states[state_max_sncid]; -}; - -static const struct automaton_sncid automaton_sncid = { - .state_names = { - "can_sched", - "cant_sched" - }, - .event_names = { - "irq_disable", - "irq_enable", - "schedule_entry", - "schedule_exit" - }, - .function = { - { cant_sched_sncid, INVALID_STATE, can_sched_sncid, can_sched_sncid }, - { INVALID_STATE, can_sched_sncid, INVALID_STATE, INVALID_STATE }, - }, - .initial_state = can_sched_sncid, - .final_states = { 1, 0 }, -}; diff --git a/kernel/trace/rv/monitors/snep/Kconfig b/kernel/trace/rv/monitors/snep/Kconfig index 77527f971232..7dd54f434ff7 100644 --- a/kernel/trace/rv/monitors/snep/Kconfig +++ b/kernel/trace/rv/monitors/snep/Kconfig @@ -2,7 +2,7 @@ # config RV_MON_SNEP depends on RV - depends on PREEMPT_TRACER + depends on TRACE_PREEMPT_TOGGLE depends on RV_MON_SCHED default y select DA_MON_EVENTS_IMPLICIT diff --git a/kernel/trace/rv/monitors/snep/snep.c b/kernel/trace/rv/monitors/snep/snep.c index 0076ba6d7ea4..558950f524a5 100644 --- a/kernel/trace/rv/monitors/snep/snep.c +++ b/kernel/trace/rv/monitors/snep/snep.c @@ -30,12 +30,12 @@ static void handle_preempt_enable(void *data, unsigned long ip, unsigned long pa da_handle_start_event_snep(preempt_enable_snep); } -static void handle_schedule_entry(void *data, bool preempt, unsigned long ip) +static void handle_schedule_entry(void *data, bool preempt) { da_handle_event_snep(schedule_entry_snep); } -static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip) +static void handle_schedule_exit(void *data, bool is_switch) { da_handle_start_event_snep(schedule_exit_snep); } @@ -79,8 +79,7 @@ static struct rv_monitor rv_snep = { static int __init register_snep(void) { - rv_register_monitor(&rv_snep, &rv_sched); - return 0; + return rv_register_monitor(&rv_snep, &rv_sched); } static void __exit unregister_snep(void) diff --git a/kernel/trace/rv/monitors/snep/snep.h b/kernel/trace/rv/monitors/snep/snep.h index 6d16b9ad931e..4cd9abb77b7b 100644 --- a/kernel/trace/rv/monitors/snep/snep.h +++ b/kernel/trace/rv/monitors/snep/snep.h @@ -41,8 +41,18 @@ static const struct automaton_snep automaton_snep = { "schedule_exit" }, .function = { - { non_scheduling_context_snep, non_scheduling_context_snep, scheduling_contex_snep, INVALID_STATE }, - { INVALID_STATE, INVALID_STATE, INVALID_STATE, non_scheduling_context_snep }, + { + non_scheduling_context_snep, + non_scheduling_context_snep, + scheduling_contex_snep, + INVALID_STATE + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + non_scheduling_context_snep + }, }, .initial_state = non_scheduling_context_snep, .final_states = { 1, 0 }, diff --git a/kernel/trace/rv/monitors/snroc/snroc.c b/kernel/trace/rv/monitors/snroc/snroc.c index bb1f60d55296..540e686e699f 100644 --- a/kernel/trace/rv/monitors/snroc/snroc.c +++ b/kernel/trace/rv/monitors/snroc/snroc.c @@ -68,8 +68,7 @@ static struct rv_monitor rv_snroc = { static int __init register_snroc(void) { - rv_register_monitor(&rv_snroc, &rv_sched); - return 0; + return rv_register_monitor(&rv_snroc, &rv_sched); } static void __exit unregister_snroc(void) diff --git a/kernel/trace/rv/monitors/sncid/Kconfig b/kernel/trace/rv/monitors/sssw/Kconfig index 76bcfef4fd10..23b7eeb38bbf 100644 --- a/kernel/trace/rv/monitors/sncid/Kconfig +++ b/kernel/trace/rv/monitors/sssw/Kconfig @@ -1,14 +1,14 @@ # SPDX-License-Identifier: GPL-2.0-only # -config RV_MON_SNCID +config RV_MON_SSSW depends on RV - depends on IRQSOFF_TRACER depends on RV_MON_SCHED default y - select DA_MON_EVENTS_IMPLICIT - bool "sncid monitor" + select DA_MON_EVENTS_ID + bool "sssw monitor" help - Monitor to ensure schedule is not called with interrupt disabled. + Monitor to ensure sched_set_state to sleepable leads to sleeping and + sleeping tasks require wakeup. This monitor is part of the sched monitors collection. For further information, see: diff --git a/kernel/trace/rv/monitors/sssw/sssw.c b/kernel/trace/rv/monitors/sssw/sssw.c new file mode 100644 index 000000000000..84b8d890d9d4 --- /dev/null +++ b/kernel/trace/rv/monitors/sssw/sssw.c @@ -0,0 +1,116 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> +#include <rv/da_monitor.h> + +#define MODULE_NAME "sssw" + +#include <trace/events/sched.h> +#include <trace/events/signal.h> +#include <rv_trace.h> +#include <monitors/sched/sched.h> + +#include "sssw.h" + +static struct rv_monitor rv_sssw; +DECLARE_DA_MON_PER_TASK(sssw, unsigned char); + +static void handle_sched_set_state(void *data, struct task_struct *tsk, int state) +{ + if (state == TASK_RUNNING) + da_handle_start_event_sssw(tsk, sched_set_state_runnable_sssw); + else + da_handle_event_sssw(tsk, sched_set_state_sleepable_sssw); +} + +static void handle_sched_switch(void *data, bool preempt, + struct task_struct *prev, + struct task_struct *next, + unsigned int prev_state) +{ + if (preempt) + da_handle_event_sssw(prev, sched_switch_preempt_sssw); + else if (prev_state == TASK_RUNNING) + da_handle_event_sssw(prev, sched_switch_yield_sssw); + else if (prev_state == TASK_RTLOCK_WAIT) + /* special case of sleeping task with racy conditions */ + da_handle_event_sssw(prev, sched_switch_blocking_sssw); + else + da_handle_event_sssw(prev, sched_switch_suspend_sssw); + da_handle_event_sssw(next, sched_switch_in_sssw); +} + +static void handle_sched_wakeup(void *data, struct task_struct *p) +{ + /* + * Wakeup can also lead to signal_wakeup although the system is + * actually runnable. The monitor can safely start with this event. + */ + da_handle_start_event_sssw(p, sched_wakeup_sssw); +} + +static void handle_signal_deliver(void *data, int sig, + struct kernel_siginfo *info, + struct k_sigaction *ka) +{ + da_handle_event_sssw(current, signal_deliver_sssw); +} + +static int enable_sssw(void) +{ + int retval; + + retval = da_monitor_init_sssw(); + if (retval) + return retval; + + rv_attach_trace_probe("sssw", sched_set_state_tp, handle_sched_set_state); + rv_attach_trace_probe("sssw", sched_switch, handle_sched_switch); + rv_attach_trace_probe("sssw", sched_wakeup, handle_sched_wakeup); + rv_attach_trace_probe("sssw", signal_deliver, handle_signal_deliver); + + return 0; +} + +static void disable_sssw(void) +{ + rv_sssw.enabled = 0; + + rv_detach_trace_probe("sssw", sched_set_state_tp, handle_sched_set_state); + rv_detach_trace_probe("sssw", sched_switch, handle_sched_switch); + rv_detach_trace_probe("sssw", sched_wakeup, handle_sched_wakeup); + rv_detach_trace_probe("sssw", signal_deliver, handle_signal_deliver); + + da_monitor_destroy_sssw(); +} + +static struct rv_monitor rv_sssw = { + .name = "sssw", + .description = "set state sleep and wakeup.", + .enable = enable_sssw, + .disable = disable_sssw, + .reset = da_monitor_reset_all_sssw, + .enabled = 0, +}; + +static int __init register_sssw(void) +{ + return rv_register_monitor(&rv_sssw, &rv_sched); +} + +static void __exit unregister_sssw(void) +{ + rv_unregister_monitor(&rv_sssw); +} + +module_init(register_sssw); +module_exit(unregister_sssw); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); +MODULE_DESCRIPTION("sssw: set state sleep and wakeup."); diff --git a/kernel/trace/rv/monitors/sssw/sssw.h b/kernel/trace/rv/monitors/sssw/sssw.h new file mode 100644 index 000000000000..243d54050c94 --- /dev/null +++ b/kernel/trace/rv/monitors/sssw/sssw.h @@ -0,0 +1,105 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of sssw automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +enum states_sssw { + runnable_sssw = 0, + signal_wakeup_sssw, + sleepable_sssw, + sleeping_sssw, + state_max_sssw +}; + +#define INVALID_STATE state_max_sssw + +enum events_sssw { + sched_set_state_runnable_sssw = 0, + sched_set_state_sleepable_sssw, + sched_switch_blocking_sssw, + sched_switch_in_sssw, + sched_switch_preempt_sssw, + sched_switch_suspend_sssw, + sched_switch_yield_sssw, + sched_wakeup_sssw, + signal_deliver_sssw, + event_max_sssw +}; + +struct automaton_sssw { + char *state_names[state_max_sssw]; + char *event_names[event_max_sssw]; + unsigned char function[state_max_sssw][event_max_sssw]; + unsigned char initial_state; + bool final_states[state_max_sssw]; +}; + +static const struct automaton_sssw automaton_sssw = { + .state_names = { + "runnable", + "signal_wakeup", + "sleepable", + "sleeping" + }, + .event_names = { + "sched_set_state_runnable", + "sched_set_state_sleepable", + "sched_switch_blocking", + "sched_switch_in", + "sched_switch_preempt", + "sched_switch_suspend", + "sched_switch_yield", + "sched_wakeup", + "signal_deliver" + }, + .function = { + { + runnable_sssw, + sleepable_sssw, + sleeping_sssw, + runnable_sssw, + runnable_sssw, + INVALID_STATE, + runnable_sssw, + runnable_sssw, + runnable_sssw + }, + { + INVALID_STATE, + sleepable_sssw, + INVALID_STATE, + signal_wakeup_sssw, + signal_wakeup_sssw, + INVALID_STATE, + signal_wakeup_sssw, + signal_wakeup_sssw, + runnable_sssw + }, + { + runnable_sssw, + sleepable_sssw, + sleeping_sssw, + sleepable_sssw, + sleepable_sssw, + sleeping_sssw, + signal_wakeup_sssw, + runnable_sssw, + sleepable_sssw + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + runnable_sssw, + INVALID_STATE + }, + }, + .initial_state = runnable_sssw, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/sssw/sssw_trace.h b/kernel/trace/rv/monitors/sssw/sssw_trace.h new file mode 100644 index 000000000000..6c03cfc6960b --- /dev/null +++ b/kernel/trace/rv/monitors/sssw/sssw_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_SSSW +DEFINE_EVENT(event_da_monitor_id, event_sssw, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_sssw, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_SSSW */ diff --git a/kernel/trace/rv/monitors/sts/Kconfig b/kernel/trace/rv/monitors/sts/Kconfig new file mode 100644 index 000000000000..7d1ff0f6fc91 --- /dev/null +++ b/kernel/trace/rv/monitors/sts/Kconfig @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_STS + depends on RV + depends on TRACE_IRQFLAGS + depends on RV_MON_SCHED + default y + select DA_MON_EVENTS_IMPLICIT + bool "sts monitor" + help + Monitor to ensure relationships between scheduler and task switches + * the scheduler is called and returns with interrupts disabled + * each call to the scheduler has up to one switch + * switches only happen inside the scheduler + * each call to the scheduler disables interrupts to switch + This monitor is part of the sched monitors collection. + + For further information, see: + Documentation/trace/rv/monitor_sched.rst diff --git a/kernel/trace/rv/monitors/sts/sts.c b/kernel/trace/rv/monitors/sts/sts.c new file mode 100644 index 000000000000..c4a9cd67c1d2 --- /dev/null +++ b/kernel/trace/rv/monitors/sts/sts.c @@ -0,0 +1,156 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> +#include <rv/da_monitor.h> + +#define MODULE_NAME "sts" + +#include <trace/events/sched.h> +#include <trace/events/irq.h> +#include <trace/events/preemptirq.h> +#include <rv_trace.h> +#include <monitors/sched/sched.h> + +#include "sts.h" + +static struct rv_monitor rv_sts; +DECLARE_DA_MON_PER_CPU(sts, unsigned char); + +#ifdef CONFIG_X86_LOCAL_APIC +#include <asm/trace/irq_vectors.h> + +static void handle_vector_irq_entry(void *data, int vector) +{ + da_handle_event_sts(irq_entry_sts); +} + +static void attach_vector_irq(void) +{ + rv_attach_trace_probe("sts", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_attach_trace_probe("sts", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_attach_trace_probe("sts", reschedule_entry, handle_vector_irq_entry); + rv_attach_trace_probe("sts", call_function_entry, handle_vector_irq_entry); + rv_attach_trace_probe("sts", call_function_single_entry, handle_vector_irq_entry); + } +} + +static void detach_vector_irq(void) +{ + rv_detach_trace_probe("sts", local_timer_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_IRQ_WORK)) + rv_detach_trace_probe("sts", irq_work_entry, handle_vector_irq_entry); + if (IS_ENABLED(CONFIG_SMP)) { + rv_detach_trace_probe("sts", reschedule_entry, handle_vector_irq_entry); + rv_detach_trace_probe("sts", call_function_entry, handle_vector_irq_entry); + rv_detach_trace_probe("sts", call_function_single_entry, handle_vector_irq_entry); + } +} + +#else +/* We assume irq_entry tracepoints are sufficient on other architectures */ +static void attach_vector_irq(void) { } +static void detach_vector_irq(void) { } +#endif + +static void handle_irq_disable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_sts(irq_disable_sts); +} + +static void handle_irq_enable(void *data, unsigned long ip, unsigned long parent_ip) +{ + da_handle_event_sts(irq_enable_sts); +} + +static void handle_irq_entry(void *data, int irq, struct irqaction *action) +{ + da_handle_event_sts(irq_entry_sts); +} + +static void handle_sched_switch(void *data, bool preempt, + struct task_struct *prev, + struct task_struct *next, + unsigned int prev_state) +{ + da_handle_event_sts(sched_switch_sts); +} + +static void handle_schedule_entry(void *data, bool preempt) +{ + da_handle_event_sts(schedule_entry_sts); +} + +static void handle_schedule_exit(void *data, bool is_switch) +{ + da_handle_start_event_sts(schedule_exit_sts); +} + +static int enable_sts(void) +{ + int retval; + + retval = da_monitor_init_sts(); + if (retval) + return retval; + + rv_attach_trace_probe("sts", irq_disable, handle_irq_disable); + rv_attach_trace_probe("sts", irq_enable, handle_irq_enable); + rv_attach_trace_probe("sts", irq_handler_entry, handle_irq_entry); + rv_attach_trace_probe("sts", sched_switch, handle_sched_switch); + rv_attach_trace_probe("sts", sched_entry_tp, handle_schedule_entry); + rv_attach_trace_probe("sts", sched_exit_tp, handle_schedule_exit); + attach_vector_irq(); + + return 0; +} + +static void disable_sts(void) +{ + rv_sts.enabled = 0; + + rv_detach_trace_probe("sts", irq_disable, handle_irq_disable); + rv_detach_trace_probe("sts", irq_enable, handle_irq_enable); + rv_detach_trace_probe("sts", irq_handler_entry, handle_irq_entry); + rv_detach_trace_probe("sts", sched_switch, handle_sched_switch); + rv_detach_trace_probe("sts", sched_entry_tp, handle_schedule_entry); + rv_detach_trace_probe("sts", sched_exit_tp, handle_schedule_exit); + detach_vector_irq(); + + da_monitor_destroy_sts(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_sts = { + .name = "sts", + .description = "schedule implies task switch.", + .enable = enable_sts, + .disable = disable_sts, + .reset = da_monitor_reset_all_sts, + .enabled = 0, +}; + +static int __init register_sts(void) +{ + return rv_register_monitor(&rv_sts, &rv_sched); +} + +static void __exit unregister_sts(void) +{ + rv_unregister_monitor(&rv_sts); +} + +module_init(register_sts); +module_exit(unregister_sts); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); +MODULE_DESCRIPTION("sts: schedule implies task switch."); diff --git a/kernel/trace/rv/monitors/sts/sts.h b/kernel/trace/rv/monitors/sts/sts.h new file mode 100644 index 000000000000..3368b6599a00 --- /dev/null +++ b/kernel/trace/rv/monitors/sts/sts.h @@ -0,0 +1,117 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of sts automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +enum states_sts { + can_sched_sts = 0, + cant_sched_sts, + disable_to_switch_sts, + enable_to_exit_sts, + in_irq_sts, + scheduling_sts, + switching_sts, + state_max_sts +}; + +#define INVALID_STATE state_max_sts + +enum events_sts { + irq_disable_sts = 0, + irq_enable_sts, + irq_entry_sts, + sched_switch_sts, + schedule_entry_sts, + schedule_exit_sts, + event_max_sts +}; + +struct automaton_sts { + char *state_names[state_max_sts]; + char *event_names[event_max_sts]; + unsigned char function[state_max_sts][event_max_sts]; + unsigned char initial_state; + bool final_states[state_max_sts]; +}; + +static const struct automaton_sts automaton_sts = { + .state_names = { + "can_sched", + "cant_sched", + "disable_to_switch", + "enable_to_exit", + "in_irq", + "scheduling", + "switching" + }, + .event_names = { + "irq_disable", + "irq_enable", + "irq_entry", + "sched_switch", + "schedule_entry", + "schedule_exit" + }, + .function = { + { + cant_sched_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + scheduling_sts, + INVALID_STATE + }, + { + INVALID_STATE, + can_sched_sts, + cant_sched_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + INVALID_STATE, + enable_to_exit_sts, + in_irq_sts, + switching_sts, + INVALID_STATE, + INVALID_STATE + }, + { + enable_to_exit_sts, + enable_to_exit_sts, + enable_to_exit_sts, + INVALID_STATE, + INVALID_STATE, + can_sched_sts + }, + { + INVALID_STATE, + scheduling_sts, + in_irq_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + disable_to_switch_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + { + INVALID_STATE, + enable_to_exit_sts, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE + }, + }, + .initial_state = can_sched_sts, + .final_states = { 1, 0, 0, 0, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/tss/tss_trace.h b/kernel/trace/rv/monitors/sts/sts_trace.h index 4619dbb50cc0..d78beb58d5b3 100644 --- a/kernel/trace/rv/monitors/tss/tss_trace.h +++ b/kernel/trace/rv/monitors/sts/sts_trace.h @@ -4,12 +4,12 @@ * Snippet to be included in rv_trace.h */ -#ifdef CONFIG_RV_MON_TSS -DEFINE_EVENT(event_da_monitor, event_tss, +#ifdef CONFIG_RV_MON_STS +DEFINE_EVENT(event_da_monitor, event_sts, TP_PROTO(char *state, char *event, char *next_state, bool final_state), TP_ARGS(state, event, next_state, final_state)); -DEFINE_EVENT(error_da_monitor, error_tss, +DEFINE_EVENT(error_da_monitor, error_sts, TP_PROTO(char *state, char *event), TP_ARGS(state, event)); -#endif /* CONFIG_RV_MON_TSS */ +#endif /* CONFIG_RV_MON_STS */ diff --git a/kernel/trace/rv/monitors/tss/tss.c b/kernel/trace/rv/monitors/tss/tss.c deleted file mode 100644 index 542787e6524f..000000000000 --- a/kernel/trace/rv/monitors/tss/tss.c +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "tss" - -#include <trace/events/sched.h> -#include <rv_trace.h> -#include <monitors/sched/sched.h> - -#include "tss.h" - -static struct rv_monitor rv_tss; -DECLARE_DA_MON_PER_CPU(tss, unsigned char); - -static void handle_sched_switch(void *data, bool preempt, - struct task_struct *prev, - struct task_struct *next, - unsigned int prev_state) -{ - da_handle_event_tss(sched_switch_tss); -} - -static void handle_schedule_entry(void *data, bool preempt, unsigned long ip) -{ - da_handle_event_tss(schedule_entry_tss); -} - -static void handle_schedule_exit(void *data, bool is_switch, unsigned long ip) -{ - da_handle_start_event_tss(schedule_exit_tss); -} - -static int enable_tss(void) -{ - int retval; - - retval = da_monitor_init_tss(); - if (retval) - return retval; - - rv_attach_trace_probe("tss", sched_switch, handle_sched_switch); - rv_attach_trace_probe("tss", sched_entry_tp, handle_schedule_entry); - rv_attach_trace_probe("tss", sched_exit_tp, handle_schedule_exit); - - return 0; -} - -static void disable_tss(void) -{ - rv_tss.enabled = 0; - - rv_detach_trace_probe("tss", sched_switch, handle_sched_switch); - rv_detach_trace_probe("tss", sched_entry_tp, handle_schedule_entry); - rv_detach_trace_probe("tss", sched_exit_tp, handle_schedule_exit); - - da_monitor_destroy_tss(); -} - -static struct rv_monitor rv_tss = { - .name = "tss", - .description = "task switch while scheduling.", - .enable = enable_tss, - .disable = disable_tss, - .reset = da_monitor_reset_all_tss, - .enabled = 0, -}; - -static int __init register_tss(void) -{ - rv_register_monitor(&rv_tss, &rv_sched); - return 0; -} - -static void __exit unregister_tss(void) -{ - rv_unregister_monitor(&rv_tss); -} - -module_init(register_tss); -module_exit(unregister_tss); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>"); -MODULE_DESCRIPTION("tss: task switch while scheduling."); diff --git a/kernel/trace/rv/monitors/tss/tss.h b/kernel/trace/rv/monitors/tss/tss.h deleted file mode 100644 index f0a36fda1b87..000000000000 --- a/kernel/trace/rv/monitors/tss/tss.h +++ /dev/null @@ -1,47 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ -/* - * Automatically generated C representation of tss automaton - * For further information about this format, see kernel documentation: - * Documentation/trace/rv/deterministic_automata.rst - */ - -enum states_tss { - thread_tss = 0, - sched_tss, - state_max_tss -}; - -#define INVALID_STATE state_max_tss - -enum events_tss { - sched_switch_tss = 0, - schedule_entry_tss, - schedule_exit_tss, - event_max_tss -}; - -struct automaton_tss { - char *state_names[state_max_tss]; - char *event_names[event_max_tss]; - unsigned char function[state_max_tss][event_max_tss]; - unsigned char initial_state; - bool final_states[state_max_tss]; -}; - -static const struct automaton_tss automaton_tss = { - .state_names = { - "thread", - "sched" - }, - .event_names = { - "sched_switch", - "schedule_entry", - "schedule_exit" - }, - .function = { - { INVALID_STATE, sched_tss, INVALID_STATE }, - { sched_tss, INVALID_STATE, thread_tss }, - }, - .initial_state = thread_tss, - .final_states = { 1, 0 }, -}; diff --git a/kernel/trace/rv/monitors/wip/Kconfig b/kernel/trace/rv/monitors/wip/Kconfig index e464b9294865..87a26195792b 100644 --- a/kernel/trace/rv/monitors/wip/Kconfig +++ b/kernel/trace/rv/monitors/wip/Kconfig @@ -2,7 +2,7 @@ # config RV_MON_WIP depends on RV - depends on PREEMPT_TRACER + depends on TRACE_PREEMPT_TOGGLE select DA_MON_EVENTS_IMPLICIT bool "wip monitor" help diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/wip/wip.c index ed758fec8608..4b4e99615a11 100644 --- a/kernel/trace/rv/monitors/wip/wip.c +++ b/kernel/trace/rv/monitors/wip/wip.c @@ -71,8 +71,7 @@ static struct rv_monitor rv_wip = { static int __init register_wip(void) { - rv_register_monitor(&rv_wip, NULL); - return 0; + return rv_register_monitor(&rv_wip, NULL); } static void __exit unregister_wip(void) diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitors/wwnr/wwnr.c index 172f31c4b0f3..4145bea2729e 100644 --- a/kernel/trace/rv/monitors/wwnr/wwnr.c +++ b/kernel/trace/rv/monitors/wwnr/wwnr.c @@ -70,8 +70,7 @@ static struct rv_monitor rv_wwnr = { static int __init register_wwnr(void) { - rv_register_monitor(&rv_wwnr, NULL); - return 0; + return rv_register_monitor(&rv_wwnr, NULL); } static void __exit unregister_wwnr(void) diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c index 0186ff4cbd0b..74c6bcc2c749 100644 --- a/kernel/trace/rv/reactor_panic.c +++ b/kernel/trace/rv/reactor_panic.c @@ -13,9 +13,13 @@ #include <linux/init.h> #include <linux/rv.h> -static void rv_panic_reaction(char *msg) +__printf(1, 2) static void rv_panic_reaction(const char *msg, ...) { - panic(msg); + va_list args; + + va_start(args, msg); + vpanic(msg, args); + va_end(args); } static struct rv_reactor rv_panic = { diff --git a/kernel/trace/rv/reactor_printk.c b/kernel/trace/rv/reactor_printk.c index 178759dbf89f..2dae2916c05f 100644 --- a/kernel/trace/rv/reactor_printk.c +++ b/kernel/trace/rv/reactor_printk.c @@ -12,9 +12,13 @@ #include <linux/init.h> #include <linux/rv.h> -static void rv_printk_reaction(char *msg) +__printf(1, 2) static void rv_printk_reaction(const char *msg, ...) { - printk_deferred(msg); + va_list args; + + va_start(args, msg); + vprintk_deferred(msg, args); + va_end(args); } static struct rv_reactor rv_printk = { diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c index e4077500a91d..bd7d56dbf6c2 100644 --- a/kernel/trace/rv/rv.c +++ b/kernel/trace/rv/rv.c @@ -143,7 +143,7 @@ #include <linux/init.h> #include <linux/slab.h> -#ifdef CONFIG_DA_MON_EVENTS +#ifdef CONFIG_RV_MON_EVENTS #define CREATE_TRACE_POINTS #include <rv_trace.h> #endif @@ -165,7 +165,7 @@ struct dentry *get_monitors_root(void) LIST_HEAD(rv_monitors_list); static int task_monitor_count; -static bool task_monitor_slots[RV_PER_TASK_MONITORS]; +static bool task_monitor_slots[CONFIG_RV_PER_TASK_MONITORS]; int rv_get_task_monitor_slot(void) { @@ -173,12 +173,12 @@ int rv_get_task_monitor_slot(void) lockdep_assert_held(&rv_interface_lock); - if (task_monitor_count == RV_PER_TASK_MONITORS) + if (task_monitor_count == CONFIG_RV_PER_TASK_MONITORS) return -EBUSY; task_monitor_count++; - for (i = 0; i < RV_PER_TASK_MONITORS; i++) { + for (i = 0; i < CONFIG_RV_PER_TASK_MONITORS; i++) { if (task_monitor_slots[i] == false) { task_monitor_slots[i] = true; return i; @@ -194,7 +194,7 @@ void rv_put_task_monitor_slot(int slot) { lockdep_assert_held(&rv_interface_lock); - if (slot < 0 || slot >= RV_PER_TASK_MONITORS) { + if (slot < 0 || slot >= CONFIG_RV_PER_TASK_MONITORS) { WARN_ONCE(1, "RV releasing an invalid slot!: %d\n", slot); return; } @@ -210,9 +210,9 @@ void rv_put_task_monitor_slot(int slot) * Monitors with a parent are nested, * Monitors without a parent could be standalone or containers. */ -bool rv_is_nested_monitor(struct rv_monitor_def *mdef) +bool rv_is_nested_monitor(struct rv_monitor *mon) { - return mdef->parent != NULL; + return mon->parent != NULL; } /* @@ -223,16 +223,16 @@ bool rv_is_nested_monitor(struct rv_monitor_def *mdef) * for enable()/disable(). Use this condition to find empty containers. * Keep both conditions in case we have some non-compliant containers. */ -bool rv_is_container_monitor(struct rv_monitor_def *mdef) +bool rv_is_container_monitor(struct rv_monitor *mon) { - struct rv_monitor_def *next; + struct rv_monitor *next; - if (list_is_last(&mdef->list, &rv_monitors_list)) + if (list_is_last(&mon->list, &rv_monitors_list)) return false; - next = list_next_entry(mdef, list); + next = list_next_entry(mon, list); - return next->parent == mdef->monitor || !mdef->monitor->enable; + return next->parent == mon || !mon->enable; } /* @@ -241,10 +241,10 @@ bool rv_is_container_monitor(struct rv_monitor_def *mdef) static ssize_t monitor_enable_read_data(struct file *filp, char __user *user_buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef = filp->private_data; + struct rv_monitor *mon = filp->private_data; const char *buff; - buff = mdef->monitor->enabled ? "1\n" : "0\n"; + buff = mon->enabled ? "1\n" : "0\n"; return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+1); } @@ -252,14 +252,14 @@ static ssize_t monitor_enable_read_data(struct file *filp, char __user *user_buf /* * __rv_disable_monitor - disabled an enabled monitor */ -static int __rv_disable_monitor(struct rv_monitor_def *mdef, bool sync) +static int __rv_disable_monitor(struct rv_monitor *mon, bool sync) { lockdep_assert_held(&rv_interface_lock); - if (mdef->monitor->enabled) { - mdef->monitor->enabled = 0; - if (mdef->monitor->disable) - mdef->monitor->disable(); + if (mon->enabled) { + mon->enabled = 0; + if (mon->disable) + mon->disable(); /* * Wait for the execution of all events to finish. @@ -273,90 +273,90 @@ static int __rv_disable_monitor(struct rv_monitor_def *mdef, bool sync) return 0; } -static void rv_disable_single(struct rv_monitor_def *mdef) +static void rv_disable_single(struct rv_monitor *mon) { - __rv_disable_monitor(mdef, true); + __rv_disable_monitor(mon, true); } -static int rv_enable_single(struct rv_monitor_def *mdef) +static int rv_enable_single(struct rv_monitor *mon) { int retval; lockdep_assert_held(&rv_interface_lock); - if (mdef->monitor->enabled) + if (mon->enabled) return 0; - retval = mdef->monitor->enable(); + retval = mon->enable(); if (!retval) - mdef->monitor->enabled = 1; + mon->enabled = 1; return retval; } -static void rv_disable_container(struct rv_monitor_def *mdef) +static void rv_disable_container(struct rv_monitor *mon) { - struct rv_monitor_def *p = mdef; + struct rv_monitor *p = mon; int enabled = 0; list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (p->parent != mdef->monitor) + if (p->parent != mon) break; enabled += __rv_disable_monitor(p, false); } if (enabled) tracepoint_synchronize_unregister(); - mdef->monitor->enabled = 0; + mon->enabled = 0; } -static int rv_enable_container(struct rv_monitor_def *mdef) +static int rv_enable_container(struct rv_monitor *mon) { - struct rv_monitor_def *p = mdef; + struct rv_monitor *p = mon; int retval = 0; list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (retval || p->parent != mdef->monitor) + if (retval || p->parent != mon) break; retval = rv_enable_single(p); } if (retval) - rv_disable_container(mdef); + rv_disable_container(mon); else - mdef->monitor->enabled = 1; + mon->enabled = 1; return retval; } /** * rv_disable_monitor - disable a given runtime monitor - * @mdef: Pointer to the monitor definition structure. + * @mon: Pointer to the monitor definition structure. * * Returns 0 on success. */ -int rv_disable_monitor(struct rv_monitor_def *mdef) +int rv_disable_monitor(struct rv_monitor *mon) { - if (rv_is_container_monitor(mdef)) - rv_disable_container(mdef); + if (rv_is_container_monitor(mon)) + rv_disable_container(mon); else - rv_disable_single(mdef); + rv_disable_single(mon); return 0; } /** * rv_enable_monitor - enable a given runtime monitor - * @mdef: Pointer to the monitor definition structure. + * @mon: Pointer to the monitor definition structure. * * Returns 0 on success, error otherwise. */ -int rv_enable_monitor(struct rv_monitor_def *mdef) +int rv_enable_monitor(struct rv_monitor *mon) { int retval; - if (rv_is_container_monitor(mdef)) - retval = rv_enable_container(mdef); + if (rv_is_container_monitor(mon)) + retval = rv_enable_container(mon); else - retval = rv_enable_single(mdef); + retval = rv_enable_single(mon); return retval; } @@ -367,7 +367,7 @@ int rv_enable_monitor(struct rv_monitor_def *mdef) static ssize_t monitor_enable_write_data(struct file *filp, const char __user *user_buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef = filp->private_data; + struct rv_monitor *mon = filp->private_data; int retval; bool val; @@ -378,9 +378,9 @@ static ssize_t monitor_enable_write_data(struct file *filp, const char __user *u mutex_lock(&rv_interface_lock); if (val) - retval = rv_enable_monitor(mdef); + retval = rv_enable_monitor(mon); else - retval = rv_disable_monitor(mdef); + retval = rv_disable_monitor(mon); mutex_unlock(&rv_interface_lock); @@ -399,12 +399,12 @@ static const struct file_operations interface_enable_fops = { static ssize_t monitor_desc_read_data(struct file *filp, char __user *user_buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef = filp->private_data; + struct rv_monitor *mon = filp->private_data; char buff[256]; memset(buff, 0, sizeof(buff)); - snprintf(buff, sizeof(buff), "%s\n", mdef->monitor->description); + snprintf(buff, sizeof(buff), "%s\n", mon->description); return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) + 1); } @@ -419,37 +419,37 @@ static const struct file_operations interface_desc_fops = { * the monitor dir, where the specific options of the monitor * are exposed. */ -static int create_monitor_dir(struct rv_monitor_def *mdef, struct rv_monitor_def *parent) +static int create_monitor_dir(struct rv_monitor *mon, struct rv_monitor *parent) { struct dentry *root = parent ? parent->root_d : get_monitors_root(); - const char *name = mdef->monitor->name; + const char *name = mon->name; struct dentry *tmp; int retval; - mdef->root_d = rv_create_dir(name, root); - if (!mdef->root_d) + mon->root_d = rv_create_dir(name, root); + if (!mon->root_d) return -ENOMEM; - tmp = rv_create_file("enable", RV_MODE_WRITE, mdef->root_d, mdef, &interface_enable_fops); + tmp = rv_create_file("enable", RV_MODE_WRITE, mon->root_d, mon, &interface_enable_fops); if (!tmp) { retval = -ENOMEM; goto out_remove_root; } - tmp = rv_create_file("desc", RV_MODE_READ, mdef->root_d, mdef, &interface_desc_fops); + tmp = rv_create_file("desc", RV_MODE_READ, mon->root_d, mon, &interface_desc_fops); if (!tmp) { retval = -ENOMEM; goto out_remove_root; } - retval = reactor_populate_monitor(mdef); + retval = reactor_populate_monitor(mon); if (retval) goto out_remove_root; return 0; out_remove_root: - rv_remove(mdef->root_d); + rv_remove(mon->root_d); return retval; } @@ -458,13 +458,12 @@ out_remove_root: */ static int monitors_show(struct seq_file *m, void *p) { - struct rv_monitor_def *mon_def = p; + struct rv_monitor *mon = container_of(p, struct rv_monitor, list); - if (mon_def->parent) - seq_printf(m, "%s:%s\n", mon_def->parent->name, - mon_def->monitor->name); + if (mon->parent) + seq_printf(m, "%s:%s\n", mon->parent->name, mon->name); else - seq_printf(m, "%s\n", mon_def->monitor->name); + seq_printf(m, "%s\n", mon->name); return 0; } @@ -496,13 +495,13 @@ static void *available_monitors_next(struct seq_file *m, void *p, loff_t *pos) */ static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos) { - struct rv_monitor_def *m_def = p; + struct rv_monitor *mon = p; (*pos)++; - list_for_each_entry_continue(m_def, &rv_monitors_list, list) { - if (m_def->monitor->enabled) - return m_def; + list_for_each_entry_continue(mon, &rv_monitors_list, list) { + if (mon->enabled) + return mon; } return NULL; @@ -510,7 +509,7 @@ static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *pos) static void *enabled_monitors_start(struct seq_file *m, loff_t *pos) { - struct rv_monitor_def *m_def; + struct rv_monitor *mon; loff_t l; mutex_lock(&rv_interface_lock); @@ -518,15 +517,15 @@ static void *enabled_monitors_start(struct seq_file *m, loff_t *pos) if (list_empty(&rv_monitors_list)) return NULL; - m_def = list_entry(&rv_monitors_list, struct rv_monitor_def, list); + mon = list_entry(&rv_monitors_list, struct rv_monitor, list); for (l = 0; l <= *pos; ) { - m_def = enabled_monitors_next(m, m_def, &l); - if (!m_def) + mon = enabled_monitors_next(m, mon, &l); + if (!mon) break; } - return m_def; + return mon; } /* @@ -566,13 +565,13 @@ static const struct file_operations available_monitors_ops = { */ static void disable_all_monitors(void) { - struct rv_monitor_def *mdef; + struct rv_monitor *mon; int enabled = 0; mutex_lock(&rv_interface_lock); - list_for_each_entry(mdef, &rv_monitors_list, list) - enabled += __rv_disable_monitor(mdef, false); + list_for_each_entry(mon, &rv_monitors_list, list) + enabled += __rv_disable_monitor(mon, false); if (enabled) { /* @@ -598,7 +597,7 @@ static ssize_t enabled_monitors_write(struct file *filp, const char __user *user size_t count, loff_t *ppos) { char buff[MAX_RV_MONITOR_NAME_SIZE + 2]; - struct rv_monitor_def *mdef; + struct rv_monitor *mon; int retval = -EINVAL; bool enable = true; char *ptr, *tmp; @@ -633,17 +632,17 @@ static ssize_t enabled_monitors_write(struct file *filp, const char __user *user if (tmp) ptr = tmp+1; - list_for_each_entry(mdef, &rv_monitors_list, list) { - if (strcmp(ptr, mdef->monitor->name) != 0) + list_for_each_entry(mon, &rv_monitors_list, list) { + if (strcmp(ptr, mon->name) != 0) continue; /* * Monitor found! */ if (enable) - retval = rv_enable_monitor(mdef); + retval = rv_enable_monitor(mon); else - retval = rv_disable_monitor(mdef); + retval = rv_disable_monitor(mon); if (!retval) retval = count; @@ -702,11 +701,11 @@ static void turn_monitoring_off(void) static void reset_all_monitors(void) { - struct rv_monitor_def *mdef; + struct rv_monitor *mon; - list_for_each_entry(mdef, &rv_monitors_list, list) { - if (mdef->monitor->enabled && mdef->monitor->reset) - mdef->monitor->reset(); + list_for_each_entry(mon, &rv_monitors_list, list) { + if (mon->enabled && mon->reset) + mon->reset(); } } @@ -768,10 +767,9 @@ static const struct file_operations monitoring_on_fops = { .read = monitoring_on_read_data, }; -static void destroy_monitor_dir(struct rv_monitor_def *mdef) +static void destroy_monitor_dir(struct rv_monitor *mon) { - reactor_cleanup_monitor(mdef); - rv_remove(mdef->root_d); + rv_remove(mon->root_d); } /** @@ -783,7 +781,7 @@ static void destroy_monitor_dir(struct rv_monitor_def *mdef) */ int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent) { - struct rv_monitor_def *r, *p = NULL; + struct rv_monitor *r; int retval = 0; if (strlen(monitor->name) >= MAX_RV_MONITOR_NAME_SIZE) { @@ -795,49 +793,31 @@ int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent) mutex_lock(&rv_interface_lock); list_for_each_entry(r, &rv_monitors_list, list) { - if (strcmp(monitor->name, r->monitor->name) == 0) { + if (strcmp(monitor->name, r->name) == 0) { pr_info("Monitor %s is already registered\n", monitor->name); retval = -EEXIST; goto out_unlock; } } - if (parent) { - list_for_each_entry(r, &rv_monitors_list, list) { - if (strcmp(parent->name, r->monitor->name) == 0) { - p = r; - break; - } - } - } - - if (p && rv_is_nested_monitor(p)) { + if (parent && rv_is_nested_monitor(parent)) { pr_info("Parent monitor %s is already nested, cannot nest further\n", parent->name); retval = -EINVAL; goto out_unlock; } - r = kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL); - if (!r) { - retval = -ENOMEM; - goto out_unlock; - } - - r->monitor = monitor; - r->parent = parent; + monitor->parent = parent; - retval = create_monitor_dir(r, p); - if (retval) { - kfree(r); - goto out_unlock; - } + retval = create_monitor_dir(monitor, parent); + if (retval) + return retval; /* keep children close to the parent for easier visualisation */ - if (p) - list_add(&r->list, &p->list); + if (parent) + list_add(&monitor->list, &parent->list); else - list_add_tail(&r->list, &rv_monitors_list); + list_add_tail(&monitor->list, &rv_monitors_list); out_unlock: mutex_unlock(&rv_interface_lock); @@ -852,17 +832,11 @@ out_unlock: */ int rv_unregister_monitor(struct rv_monitor *monitor) { - struct rv_monitor_def *ptr, *next; - mutex_lock(&rv_interface_lock); - list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) { - if (strcmp(monitor->name, ptr->monitor->name) == 0) { - rv_disable_monitor(ptr); - list_del(&ptr->list); - destroy_monitor_dir(ptr); - } - } + rv_disable_monitor(monitor); + list_del(&monitor->list); + destroy_monitor_dir(monitor); mutex_unlock(&rv_interface_lock); return 0; diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index 98fca0a1adbc..1485a70c1bf4 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -23,48 +23,21 @@ struct rv_interface { extern struct mutex rv_interface_lock; extern struct list_head rv_monitors_list; -#ifdef CONFIG_RV_REACTORS -struct rv_reactor_def { - struct list_head list; - struct rv_reactor *reactor; - /* protected by the monitor interface lock */ - int counter; -}; -#endif - -struct rv_monitor_def { - struct list_head list; - struct rv_monitor *monitor; - struct rv_monitor *parent; - struct dentry *root_d; -#ifdef CONFIG_RV_REACTORS - struct rv_reactor_def *rdef; - bool reacting; -#endif - bool task_monitor; -}; - struct dentry *get_monitors_root(void); -int rv_disable_monitor(struct rv_monitor_def *mdef); -int rv_enable_monitor(struct rv_monitor_def *mdef); -bool rv_is_container_monitor(struct rv_monitor_def *mdef); -bool rv_is_nested_monitor(struct rv_monitor_def *mdef); +int rv_disable_monitor(struct rv_monitor *mon); +int rv_enable_monitor(struct rv_monitor *mon); +bool rv_is_container_monitor(struct rv_monitor *mon); +bool rv_is_nested_monitor(struct rv_monitor *mon); #ifdef CONFIG_RV_REACTORS -int reactor_populate_monitor(struct rv_monitor_def *mdef); -void reactor_cleanup_monitor(struct rv_monitor_def *mdef); +int reactor_populate_monitor(struct rv_monitor *mon); int init_rv_reactors(struct dentry *root_dir); #else -static inline int reactor_populate_monitor(struct rv_monitor_def *mdef) +static inline int reactor_populate_monitor(struct rv_monitor *mon) { return 0; } -static inline void reactor_cleanup_monitor(struct rv_monitor_def *mdef) -{ - return; -} - static inline int init_rv_reactors(struct dentry *root_dir) { return 0; diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c index 9501ca886d83..d32859fec238 100644 --- a/kernel/trace/rv/rv_reactors.c +++ b/kernel/trace/rv/rv_reactors.c @@ -70,12 +70,12 @@ */ static LIST_HEAD(rv_reactors_list); -static struct rv_reactor_def *get_reactor_rdef_by_name(char *name) +static struct rv_reactor *get_reactor_rdef_by_name(char *name) { - struct rv_reactor_def *r; + struct rv_reactor *r; list_for_each_entry(r, &rv_reactors_list, list) { - if (strcmp(name, r->reactor->name) == 0) + if (strcmp(name, r->name) == 0) return r; } return NULL; @@ -86,9 +86,9 @@ static struct rv_reactor_def *get_reactor_rdef_by_name(char *name) */ static int reactors_show(struct seq_file *m, void *p) { - struct rv_reactor_def *rea_def = p; + struct rv_reactor *reactor = container_of(p, struct rv_reactor, list); - seq_printf(m, "%s\n", rea_def->reactor->name); + seq_printf(m, "%s\n", reactor->name); return 0; } @@ -138,13 +138,13 @@ static const struct file_operations available_reactors_ops = { */ static int monitor_reactor_show(struct seq_file *m, void *p) { - struct rv_monitor_def *mdef = m->private; - struct rv_reactor_def *rdef = p; + struct rv_monitor *mon = m->private; + struct rv_reactor *reactor = container_of(p, struct rv_reactor, list); - if (mdef->rdef == rdef) - seq_printf(m, "[%s]\n", rdef->reactor->name); + if (mon->reactor == reactor) + seq_printf(m, "[%s]\n", reactor->name); else - seq_printf(m, "%s\n", rdef->reactor->name); + seq_printf(m, "%s\n", reactor->name); return 0; } @@ -158,43 +158,37 @@ static const struct seq_operations monitor_reactors_seq_ops = { .show = monitor_reactor_show }; -static void monitor_swap_reactors_single(struct rv_monitor_def *mdef, - struct rv_reactor_def *rdef, - bool reacting, bool nested) +static void monitor_swap_reactors_single(struct rv_monitor *mon, + struct rv_reactor *reactor, + bool nested) { bool monitor_enabled; /* nothing to do */ - if (mdef->rdef == rdef) + if (mon->reactor == reactor) return; - monitor_enabled = mdef->monitor->enabled; + monitor_enabled = mon->enabled; if (monitor_enabled) - rv_disable_monitor(mdef); + rv_disable_monitor(mon); - /* swap reactor's usage */ - mdef->rdef->counter--; - rdef->counter++; - - mdef->rdef = rdef; - mdef->reacting = reacting; - mdef->monitor->react = rdef->reactor->react; + mon->reactor = reactor; + mon->react = reactor->react; /* enable only once if iterating through a container */ if (monitor_enabled && !nested) - rv_enable_monitor(mdef); + rv_enable_monitor(mon); } -static void monitor_swap_reactors(struct rv_monitor_def *mdef, - struct rv_reactor_def *rdef, bool reacting) +static void monitor_swap_reactors(struct rv_monitor *mon, struct rv_reactor *reactor) { - struct rv_monitor_def *p = mdef; + struct rv_monitor *p = mon; - if (rv_is_container_monitor(mdef)) + if (rv_is_container_monitor(mon)) list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (p->parent != mdef->monitor) + if (p->parent != mon) break; - monitor_swap_reactors_single(p, rdef, reacting, true); + monitor_swap_reactors_single(p, reactor, true); } /* * This call enables and disables the monitor if they were active. @@ -202,7 +196,7 @@ static void monitor_swap_reactors(struct rv_monitor_def *mdef, * All nested monitors are enabled also if they were off, we may refine * this logic in the future. */ - monitor_swap_reactors_single(mdef, rdef, reacting, false); + monitor_swap_reactors_single(mon, reactor, false); } static ssize_t @@ -210,11 +204,10 @@ monitor_reactors_write(struct file *file, const char __user *user_buf, size_t count, loff_t *ppos) { char buff[MAX_RV_REACTOR_NAME_SIZE + 2]; - struct rv_monitor_def *mdef; - struct rv_reactor_def *rdef; + struct rv_monitor *mon; + struct rv_reactor *reactor; struct seq_file *seq_f; int retval = -EINVAL; - bool enable; char *ptr; int len; @@ -237,22 +230,17 @@ monitor_reactors_write(struct file *file, const char __user *user_buf, * See monitor_reactors_open() */ seq_f = file->private_data; - mdef = seq_f->private; + mon = seq_f->private; mutex_lock(&rv_interface_lock); retval = -EINVAL; - list_for_each_entry(rdef, &rv_reactors_list, list) { - if (strcmp(ptr, rdef->reactor->name) != 0) + list_for_each_entry(reactor, &rv_reactors_list, list) { + if (strcmp(ptr, reactor->name) != 0) continue; - if (rdef == get_reactor_rdef_by_name("nop")) - enable = false; - else - enable = true; - - monitor_swap_reactors(mdef, rdef, enable); + monitor_swap_reactors(mon, reactor); retval = count; break; @@ -268,7 +256,7 @@ monitor_reactors_write(struct file *file, const char __user *user_buf, */ static int monitor_reactors_open(struct inode *inode, struct file *file) { - struct rv_monitor_def *mdef = inode->i_private; + struct rv_monitor *mon = inode->i_private; struct seq_file *seq_f; int ret; @@ -284,7 +272,7 @@ static int monitor_reactors_open(struct inode *inode, struct file *file) /* * Copy the create file "private" data to the seq_file private data. */ - seq_f->private = mdef; + seq_f->private = mon; return 0; }; @@ -299,23 +287,16 @@ static const struct file_operations monitor_reactors_ops = { static int __rv_register_reactor(struct rv_reactor *reactor) { - struct rv_reactor_def *r; + struct rv_reactor *r; list_for_each_entry(r, &rv_reactors_list, list) { - if (strcmp(reactor->name, r->reactor->name) == 0) { + if (strcmp(reactor->name, r->name) == 0) { pr_info("Reactor %s is already registered\n", reactor->name); return -EINVAL; } } - r = kzalloc(sizeof(struct rv_reactor_def), GFP_KERNEL); - if (!r) - return -ENOMEM; - - r->reactor = reactor; - r->counter = 0; - - list_add_tail(&r->list, &rv_reactors_list); + list_add_tail(&reactor->list, &rv_reactors_list); return 0; } @@ -350,30 +331,10 @@ int rv_register_reactor(struct rv_reactor *reactor) */ int rv_unregister_reactor(struct rv_reactor *reactor) { - struct rv_reactor_def *ptr, *next; - int ret = 0; - mutex_lock(&rv_interface_lock); - - list_for_each_entry_safe(ptr, next, &rv_reactors_list, list) { - if (strcmp(reactor->name, ptr->reactor->name) == 0) { - - if (!ptr->counter) { - list_del(&ptr->list); - } else { - printk(KERN_WARNING - "rv: the rv_reactor %s is in use by %d monitor(s)\n", - ptr->reactor->name, ptr->counter); - printk(KERN_WARNING "rv: the rv_reactor %s cannot be removed\n", - ptr->reactor->name); - ret = -EBUSY; - break; - } - } - } - + list_del(&reactor->list); mutex_unlock(&rv_interface_lock); - return ret; + return 0; } /* @@ -454,43 +415,30 @@ static const struct file_operations reacting_on_fops = { /** * reactor_populate_monitor - creates per monitor reactors file - * @mdef: monitor's definition. + * @mon: The monitor. * * Returns 0 if successful, error otherwise. */ -int reactor_populate_monitor(struct rv_monitor_def *mdef) +int reactor_populate_monitor(struct rv_monitor *mon) { struct dentry *tmp; - tmp = rv_create_file("reactors", RV_MODE_WRITE, mdef->root_d, mdef, &monitor_reactors_ops); + tmp = rv_create_file("reactors", RV_MODE_WRITE, mon->root_d, mon, &monitor_reactors_ops); if (!tmp) return -ENOMEM; /* * Configure as the rv_nop reactor. */ - mdef->rdef = get_reactor_rdef_by_name("nop"); - mdef->rdef->counter++; - mdef->reacting = false; + mon->reactor = get_reactor_rdef_by_name("nop"); return 0; } -/** - * reactor_cleanup_monitor - cleanup a monitor reference - * @mdef: monitor's definition. - */ -void reactor_cleanup_monitor(struct rv_monitor_def *mdef) -{ - lockdep_assert_held(&rv_interface_lock); - mdef->rdef->counter--; - WARN_ON_ONCE(mdef->rdef->counter < 0); -} - /* * Nop reactor register */ -static void rv_nop_reaction(char *msg) +__printf(1, 2) static void rv_nop_reaction(const char *msg, ...) { } diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index 422b75f58891..4a6faddac614 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -16,24 +16,24 @@ DECLARE_EVENT_CLASS(event_da_monitor, TP_ARGS(state, event, next_state, final_state), TP_STRUCT__entry( - __array( char, state, MAX_DA_NAME_LEN ) - __array( char, event, MAX_DA_NAME_LEN ) - __array( char, next_state, MAX_DA_NAME_LEN ) - __field( bool, final_state ) + __string( state, state ) + __string( event, event ) + __string( next_state, next_state ) + __field( bool, final_state ) ), TP_fast_assign( - memcpy(__entry->state, state, MAX_DA_NAME_LEN); - memcpy(__entry->event, event, MAX_DA_NAME_LEN); - memcpy(__entry->next_state, next_state, MAX_DA_NAME_LEN); - __entry->final_state = final_state; + __assign_str(state); + __assign_str(event); + __assign_str(next_state); + __entry->final_state = final_state; ), - TP_printk("%s x %s -> %s %s", - __entry->state, - __entry->event, - __entry->next_state, - __entry->final_state ? "(final)" : "") + TP_printk("%s x %s -> %s%s", + __get_str(state), + __get_str(event), + __get_str(next_state), + __entry->final_state ? " (final)" : "") ); DECLARE_EVENT_CLASS(error_da_monitor, @@ -43,26 +43,26 @@ DECLARE_EVENT_CLASS(error_da_monitor, TP_ARGS(state, event), TP_STRUCT__entry( - __array( char, state, MAX_DA_NAME_LEN ) - __array( char, event, MAX_DA_NAME_LEN ) + __string( state, state ) + __string( event, event ) ), TP_fast_assign( - memcpy(__entry->state, state, MAX_DA_NAME_LEN); - memcpy(__entry->event, event, MAX_DA_NAME_LEN); + __assign_str(state); + __assign_str(event); ), TP_printk("event %s not expected in the state %s", - __entry->event, - __entry->state) + __get_str(event), + __get_str(state)) ); #include <monitors/wip/wip_trace.h> -#include <monitors/tss/tss_trace.h> #include <monitors/sco/sco_trace.h> #include <monitors/scpd/scpd_trace.h> #include <monitors/snep/snep_trace.h> -#include <monitors/sncid/sncid_trace.h> +#include <monitors/sts/sts_trace.h> +#include <monitors/opid/opid_trace.h> // Add new monitors based on CONFIG_DA_MON_EVENTS_IMPLICIT here #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */ @@ -75,27 +75,27 @@ DECLARE_EVENT_CLASS(event_da_monitor_id, TP_ARGS(id, state, event, next_state, final_state), TP_STRUCT__entry( - __field( int, id ) - __array( char, state, MAX_DA_NAME_LEN ) - __array( char, event, MAX_DA_NAME_LEN ) - __array( char, next_state, MAX_DA_NAME_LEN ) - __field( bool, final_state ) + __field( int, id ) + __string( state, state ) + __string( event, event ) + __string( next_state, next_state ) + __field( bool, final_state ) ), TP_fast_assign( - memcpy(__entry->state, state, MAX_DA_NAME_LEN); - memcpy(__entry->event, event, MAX_DA_NAME_LEN); - memcpy(__entry->next_state, next_state, MAX_DA_NAME_LEN); - __entry->id = id; - __entry->final_state = final_state; + __assign_str(state); + __assign_str(event); + __assign_str(next_state); + __entry->id = id; + __entry->final_state = final_state; ), - TP_printk("%d: %s x %s -> %s %s", + TP_printk("%d: %s x %s -> %s%s", __entry->id, - __entry->state, - __entry->event, - __entry->next_state, - __entry->final_state ? "(final)" : "") + __get_str(state), + __get_str(event), + __get_str(next_state), + __entry->final_state ? " (final)" : "") ); DECLARE_EVENT_CLASS(error_da_monitor_id, @@ -105,32 +105,108 @@ DECLARE_EVENT_CLASS(error_da_monitor_id, TP_ARGS(id, state, event), TP_STRUCT__entry( - __field( int, id ) - __array( char, state, MAX_DA_NAME_LEN ) - __array( char, event, MAX_DA_NAME_LEN ) + __field( int, id ) + __string( state, state ) + __string( event, event ) ), TP_fast_assign( - memcpy(__entry->state, state, MAX_DA_NAME_LEN); - memcpy(__entry->event, event, MAX_DA_NAME_LEN); - __entry->id = id; + __assign_str(state); + __assign_str(event); + __entry->id = id; ), TP_printk("%d: event %s not expected in the state %s", __entry->id, - __entry->event, - __entry->state) + __get_str(event), + __get_str(state)) ); #include <monitors/wwnr/wwnr_trace.h> #include <monitors/snroc/snroc_trace.h> +#include <monitors/nrp/nrp_trace.h> +#include <monitors/sssw/sssw_trace.h> // Add new monitors based on CONFIG_DA_MON_EVENTS_ID here #endif /* CONFIG_DA_MON_EVENTS_ID */ +#ifdef CONFIG_LTL_MON_EVENTS_ID +DECLARE_EVENT_CLASS(event_ltl_monitor_id, + + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + + TP_ARGS(task, states, atoms, next), + + TP_STRUCT__entry( + __string(comm, task->comm) + __field(pid_t, pid) + __string(states, states) + __string(atoms, atoms) + __string(next, next) + ), + + TP_fast_assign( + __assign_str(comm); + __entry->pid = task->pid; + __assign_str(states); + __assign_str(atoms); + __assign_str(next); + ), + + TP_printk("%s[%d]: (%s) x (%s) -> (%s)", __get_str(comm), __entry->pid, + __get_str(states), __get_str(atoms), __get_str(next)) +); + +DECLARE_EVENT_CLASS(error_ltl_monitor_id, + + TP_PROTO(struct task_struct *task), + + TP_ARGS(task), + + TP_STRUCT__entry( + __string(comm, task->comm) + __field(pid_t, pid) + ), + + TP_fast_assign( + __assign_str(comm); + __entry->pid = task->pid; + ), + + TP_printk("%s[%d]: violation detected", __get_str(comm), __entry->pid) +); +#include <monitors/pagefault/pagefault_trace.h> +#include <monitors/sleep/sleep_trace.h> +// Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here +#endif /* CONFIG_LTL_MON_EVENTS_ID */ + +#ifdef CONFIG_RV_MON_MAINTENANCE_EVENTS +/* Tracepoint useful for monitors development, currenly only used in DA */ +TRACE_EVENT(rv_retries_error, + + TP_PROTO(char *name, char *event), + + TP_ARGS(name, event), + + TP_STRUCT__entry( + __string( name, name ) + __string( event, event ) + ), + + TP_fast_assign( + __assign_str(name); + __assign_str(event); + ), + + TP_printk(__stringify(MAX_DA_RETRY_RACING_EVENTS) + " retries reached for event %s, resetting monitor %s", + __get_str(event), __get_str(name)) +); +#endif /* CONFIG_RV_MON_MAINTENANCE_EVENTS */ #endif /* _TRACE_RV_H */ -/* This part ust be outside protection */ +/* This part must be outside protection */ #undef TRACE_INCLUDE_PATH #define TRACE_INCLUDE_PATH . +#undef TRACE_INCLUDE_FILE #define TRACE_INCLUDE_FILE rv_trace #include <trace/define_trace.h> diff --git a/tools/objtool/noreturns.h b/tools/objtool/noreturns.h index eacfe3b0a8d1..6a922d046b8e 100644 --- a/tools/objtool/noreturns.h +++ b/tools/objtool/noreturns.h @@ -38,6 +38,7 @@ NORETURN(mpt_halt_firmware) NORETURN(mwait_play_dead) NORETURN(nmi_panic_self_stop) NORETURN(panic) +NORETURN(vpanic) NORETURN(panic_smp_self_stop) NORETURN(rest_init) NORETURN(rewind_stack_and_make_dead) diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile deleted file mode 100644 index 021beb07a521..000000000000 --- a/tools/verification/dot2/Makefile +++ /dev/null @@ -1,26 +0,0 @@ -INSTALL=install - -prefix ?= /usr -bindir ?= $(prefix)/bin -mandir ?= $(prefix)/share/man -miscdir ?= $(prefix)/share/dot2 -srcdir ?= $(prefix)/src - -PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') - -.PHONY: all -all: - -.PHONY: clean -clean: - -.PHONY: install -install: - $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py - $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py - $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ - - mkdir -p ${miscdir}/ - cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k deleted file mode 100644 index 767064f415e7..000000000000 --- a/tools/verification/dot2/dot2k +++ /dev/null @@ -1,53 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-License-Identifier: GPL-2.0-only -# -# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> -# -# dot2k: transform dot files into a monitor for the Linux kernel. -# -# For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst - -if __name__ == '__main__': - from dot2.dot2k import dot2k - import argparse - import sys - - def is_container(): - """Should work even before parsing the arguments""" - return "-c" in sys.argv or "--container" in sys.argv - - parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') - parser.add_argument('-d', "--dot", dest="dot_file", required=not is_container()) - parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=not is_container(), - help=f"Available options: {', '.join(dot2k.monitor_types.keys())}") - parser.add_argument('-n', "--model_name", dest="model_name", required=is_container()) - parser.add_argument("-D", "--description", dest="description", required=False) - parser.add_argument("-a", "--auto_patch", dest="auto_patch", - action="store_true", required=False, - help="Patch the kernel in place") - parser.add_argument("-p", "--parent", dest="parent", - required=False, help="Create a monitor nested to parent") - parser.add_argument("-c", "--container", dest="container", - action="store_true", required=False, - help="Create an empty monitor to be used as a container") - params = parser.parse_args() - - if not is_container(): - print("Opening and parsing the dot file %s" % params.dot_file) - try: - monitor=dot2k(params.dot_file, params.monitor_type, vars(params)) - except Exception as e: - print('Error: '+ str(e)) - print("Sorry : :-(") - sys.exit(1) - - print("Writing the monitor into the directory %s" % monitor.name) - monitor.print_files() - print("Almost done, checklist") - if not is_container(): - print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) - print(monitor.fill_tracepoint_tooltip()) - print(monitor.fill_makefile_tooltip()) - print(monitor.fill_kconfig_tooltip()) - print(monitor.fill_monitor_tooltip()) diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000000..d7ce62102733 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT) diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl new file mode 100644 index 000000000000..6379bbeb6212 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,22 @@ +RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) + and ((not WAKE) until RT_FRIENDLY_WAKE) + +RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + +RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI) + +RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + or KTHREAD_SHOULD_STOP + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI + or TASK_IS_RCU + or TASK_IS_MIGRATION diff --git a/tools/verification/models/sched/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000000..77bb64669416 --- /dev/null +++ b/tools/verification/models/sched/nrp.dot @@ -0,0 +1,29 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = doublecircle] "any_thread_running"}; + {node [shape = circle] "any_thread_running"}; + {node [shape = circle] "nested_preempt"}; + {node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"}; + {node [shape = circle] "preempt_irq"}; + {node [shape = circle] "rescheduling"}; + "__init_preempt_irq" -> "preempt_irq"; + "any_thread_running" [label = "any_thread_running", color = green3]; + "any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ]; + "any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ]; + "nested_preempt" [label = "nested_preempt"]; + "nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "nested_preempt" -> "nested_preempt" [ label = "irq_entry" ]; + "nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ]; + "preempt_irq" [label = "preempt_irq"]; + "preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ]; + "rescheduling" [label = "rescheduling"]; + "rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "rescheduling" -> "preempt_irq" [ label = "irq_entry" ]; + "rescheduling" -> "rescheduling" [ label = "sched_need_resched" ]; + { rank = min ; + "__init_preempt_irq"; + "preempt_irq"; + } +} diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot new file mode 100644 index 000000000000..840052f6952b --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,35 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_disabled"}; + {node [shape = circle] "disabled"}; + {node [shape = doublecircle] "enabled"}; + {node [shape = circle] "enabled"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "irq_disabled"}; + {node [shape = circle] "preempt_disabled"}; + "__init_disabled" -> "disabled"; + "disabled" [label = "disabled"]; + "disabled" -> "disabled" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "disabled" -> "irq_disabled" [ label = "preempt_enable" ]; + "disabled" -> "preempt_disabled" [ label = "irq_enable" ]; + "enabled" [label = "enabled", color = green3]; + "enabled" -> "enabled" [ label = "preempt_enable" ]; + "enabled" -> "irq_disabled" [ label = "irq_disable" ]; + "enabled" -> "preempt_disabled" [ label = "preempt_disable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "enabled" [ label = "irq_enable" ]; + "in_irq" -> "in_irq" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "irq_disabled" [label = "irq_disabled"]; + "irq_disabled" -> "disabled" [ label = "preempt_disable" ]; + "irq_disabled" -> "enabled" [ label = "irq_enable" ]; + "irq_disabled" -> "in_irq" [ label = "irq_entry" ]; + "irq_disabled" -> "irq_disabled" [ label = "sched_need_resched" ]; + "preempt_disabled" [label = "preempt_disabled"]; + "preempt_disabled" -> "disabled" [ label = "irq_disable" ]; + "preempt_disabled" -> "enabled" [ label = "preempt_enable" ]; + { rank = min ; + "__init_disabled"; + "disabled"; + } +} diff --git a/tools/verification/models/sched/sncid.dot b/tools/verification/models/sched/sncid.dot deleted file mode 100644 index 072851721b50..000000000000 --- a/tools/verification/models/sched/sncid.dot +++ /dev/null @@ -1,18 +0,0 @@ -digraph state_automaton { - center = true; - size = "7,11"; - {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; - {node [shape = ellipse] "can_sched"}; - {node [shape = plaintext] "can_sched"}; - {node [shape = plaintext] "cant_sched"}; - "__init_can_sched" -> "can_sched"; - "can_sched" [label = "can_sched", color = green3]; - "can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ]; - "can_sched" -> "cant_sched" [ label = "irq_disable" ]; - "cant_sched" [label = "cant_sched"]; - "cant_sched" -> "can_sched" [ label = "irq_enable" ]; - { rank = min ; - "__init_can_sched"; - "can_sched"; - } -} diff --git a/tools/verification/models/sched/sssw.dot b/tools/verification/models/sched/sssw.dot new file mode 100644 index 000000000000..4994c3e876be --- /dev/null +++ b/tools/verification/models/sched/sssw.dot @@ -0,0 +1,30 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_runnable"}; + {node [shape = doublecircle] "runnable"}; + {node [shape = circle] "runnable"}; + {node [shape = circle] "signal_wakeup"}; + {node [shape = circle] "sleepable"}; + {node [shape = circle] "sleeping"}; + "__init_runnable" -> "runnable"; + "runnable" [label = "runnable", color = green3]; + "runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ]; + "runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "runnable" -> "sleeping" [ label = "sched_switch_blocking" ]; + "signal_wakeup" [label = "signal_wakeup"]; + "signal_wakeup" -> "runnable" [ label = "signal_deliver" ]; + "signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ]; + "signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "sleepable" [label = "sleepable"]; + "sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ]; + "sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ]; + "sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ]; + "sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "runnable" [ label = "sched_wakeup" ]; + { rank = min ; + "__init_runnable"; + "runnable"; + } +} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/models/sched/sts.dot new file mode 100644 index 000000000000..8f5f38be04d5 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; + {node [shape = doublecircle] "can_sched"}; + {node [shape = circle] "can_sched"}; + {node [shape = circle] "cant_sched"}; + {node [shape = circle] "disable_to_switch"}; + {node [shape = circle] "enable_to_exit"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "scheduling"}; + {node [shape = circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label = "can_sched", color = green3]; + "can_sched" -> "cant_sched" [ label = "irq_disable" ]; + "can_sched" -> "scheduling" [ label = "schedule_entry" ]; + "cant_sched" [label = "cant_sched"]; + "cant_sched" -> "can_sched" [ label = "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label = "irq_entry" ]; + "disable_to_switch" [label = "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label = "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label = "irq_entry" ]; + "disable_to_switch" -> "switching" [ label = "sched_switch" ]; + "enable_to_exit" [label = "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label = "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label = "irq_disable\nirq_entry\nirq_enable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "in_irq" [ label = "irq_entry" ]; + "in_irq" -> "scheduling" [ label = "irq_enable" ]; + "scheduling" [label = "scheduling"]; + "scheduling" -> "disable_to_switch" [ label = "irq_disable" ]; + "switching" [label = "switching"]; + "switching" -> "enable_to_exit" [ label = "irq_enable" ]; + { rank = min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/models/sched/tss.dot b/tools/verification/models/sched/tss.dot deleted file mode 100644 index 7dfa1d9121bb..000000000000 --- a/tools/verification/models/sched/tss.dot +++ /dev/null @@ -1,18 +0,0 @@ -digraph state_automaton { - center = true; - size = "7,11"; - {node [shape = plaintext] "sched"}; - {node [shape = plaintext, style=invis, label=""] "__init_thread"}; - {node [shape = ellipse] "thread"}; - {node [shape = plaintext] "thread"}; - "__init_thread" -> "thread"; - "sched" [label = "sched"]; - "sched" -> "sched" [ label = "sched_switch" ]; - "sched" -> "thread" [ label = "schedule_exit" ]; - "thread" [label = "thread", color = green3]; - "thread" -> "sched" [ label = "schedule_entry" ]; - { rank = min ; - "__init_thread"; - "thread"; - } -} diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index c0dcee795c0d..4bb746ea6e17 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -431,7 +431,7 @@ ikm_event_handler(struct trace_seq *s, struct tep_record *record, if (config_has_id && (config_my_pid == id)) return 0; - else if (config_my_pid && (config_my_pid == pid)) + else if (config_my_pid == pid) return 0; tep_print_event(trace_event->tep, s, record, "%16s-%-8d [%.3d] ", @@ -734,7 +734,7 @@ static int parse_arguments(char *monitor_name, int argc, char **argv) config_reactor = optarg; break; case 's': - config_my_pid = 0; + config_my_pid = -1; break; case 't': config_trace = 1; diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index 239de054d1e0..b8fe24a87d97 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -191,6 +191,7 @@ int main(int argc, char **argv) * and exit. */ signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); rv_mon(argc - 1, &argv[1]); } diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore new file mode 100644 index 000000000000..1e288a076560 --- /dev/null +++ b/tools/verification/rvgen/.gitignore @@ -0,0 +1,3 @@ +__pycache__/ +parser.out +parsetab.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile new file mode 100644 index 000000000000..cfc4056c1e87 --- /dev/null +++ b/tools/verification/rvgen/Makefile @@ -0,0 +1,27 @@ +INSTALL=install + +prefix ?= /usr +bindir ?= $(prefix)/bin +mandir ?= $(prefix)/share/man +srcdir ?= $(prefix)/src + +PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') + +.PHONY: all +all: + +.PHONY: clean +clean: + +.PHONY: install +install: + $(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py + $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py + $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ + $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py + $(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py + $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py + $(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py + $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen + cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py new file mode 100644 index 000000000000..fa6fc1f4de2f --- /dev/null +++ b/tools/verification/rvgen/__main__.py @@ -0,0 +1,67 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +if __name__ == '__main__': + from rvgen.dot2k import dot2k + from rvgen.generator import Monitor + from rvgen.container import Container + from rvgen.ltl2k import ltl2k + import argparse + import sys + + parser = argparse.ArgumentParser(description='Generate kernel rv monitor') + parser.add_argument("-D", "--description", dest="description", required=False) + parser.add_argument("-a", "--auto_patch", dest="auto_patch", + action="store_true", required=False, + help="Patch the kernel in place") + + subparsers = parser.add_subparsers(dest="subcmd", required=True) + + monitor_parser = subparsers.add_parser("monitor") + monitor_parser.add_argument('-n', "--model_name", dest="model_name") + monitor_parser.add_argument("-p", "--parent", dest="parent", + required=False, help="Create a monitor nested to parent") + monitor_parser.add_argument('-c', "--class", dest="monitor_class", + help="Monitor class, either \"da\" or \"ltl\"") + monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file") + monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", + help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") + + container_parser = subparsers.add_parser("container") + container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + + params = parser.parse_args() + + try: + if params.subcmd == "monitor": + print("Opening and parsing the specification file %s" % params.spec) + if params.monitor_class == "da": + monitor = dot2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ltl": + monitor = ltl2k(params.spec, params.monitor_type, vars(params)) + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) + else: + monitor = Container(vars(params)) + except Exception as e: + print('Error: '+ str(e)) + print("Sorry : :-(") + sys.exit(1) + + print("Writing the monitor into the directory %s" % monitor.name) + monitor.print_files() + print("Almost done, checklist") + if params.subcmd == "monitor": + print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) + print(monitor.fill_tracepoint_tooltip()) + print(monitor.fill_makefile_tooltip()) + print(monitor.fill_kconfig_tooltip()) + print(monitor.fill_monitor_tooltip()) diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c index 3fe89ab88b65..bf0c67c5b66c 100644 --- a/tools/verification/dot2/dot2c +++ b/tools/verification/rvgen/dot2c @@ -14,7 +14,7 @@ # Documentation/trace/rv/deterministic_automata.rst if __name__ == '__main__': - from dot2 import dot2c + from rvgen import dot2c import argparse import sys diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py index d9a3fe2b74bf..d9a3fe2b74bf 100644 --- a/tools/verification/dot2/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py new file mode 100644 index 000000000000..51f188530b4d --- /dev/null +++ b/tools/verification/rvgen/rvgen/container.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Generator for runtime verification monitor container + +from . import generator + + +class Container(generator.RVGenerator): + template_dir = "container" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.name = extra_params.get("model_name") + self.main_h = self._read_template_file("main.h") + + def fill_model_h(self): + main_h = self.main_h + main_h = main_h.replace("%%MODEL_NAME%%", self.name) + return main_h + + def fill_kconfig_tooltip(self): + """Override to produce a marker for this container in the Kconfig""" + container_marker = self._kconfig_marker(self.name) + "\n" + result = super().fill_kconfig_tooltip() + if self.auto_patch: + self._patch_file("Kconfig", + self._kconfig_marker(), container_marker) + return result + return result + container_marker diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py index fa2816ac7b61..b9b6f14cc536 100644 --- a/tools/verification/dot2/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -13,7 +13,7 @@ # For further information, see: # Documentation/trace/rv/deterministic_automata.rst -from dot2.automata import Automata +from .automata import Automata class Dot2c(Automata): enum_suffix = "" @@ -152,28 +152,30 @@ class Dot2c(Automata): max_state_name = max(self.states, key = len).__len__() return max(max_state_name, self.invalid_state_str.__len__()) - def __get_state_string_length(self): - maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__() - return "%" + str(maxlen) + "s" - def get_aut_init_function(self): nr_states = self.states.__len__() nr_events = self.events.__len__() buff = [] - strformat = self.__get_state_string_length() - + maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) + tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" + comma_space = 2 # ", " count last comma here + linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length for x in range(nr_states): - line = "\t\t{ " + line = "\t\t{\n" if linetoolong else "\t\t{ " for y in range(nr_events): next_state = self.function[x][y] if next_state != self.invalid_state_str: next_state = self.function[x][y] + self.enum_suffix + if linetoolong: + line += "\t\t\t%s" % next_state + else: + line += "%*s" % (maxlen, next_state) if y != nr_events-1: - line = line + strformat % next_state + ", " + line += ",\n" if linetoolong else ", " else: - line = line + strformat % next_state + " }," + line += "\n\t\t}," if linetoolong else " }," buff.append(line) return self.__buff_to_string(buff) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py new file mode 100644 index 000000000000..ed0a3c901106 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +from .dot2c import Dot2c +from .generator import Monitor + + +class dot2k(Monitor, Dot2c): + template_dir = "dot2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + self.monitor_type = MonitorType + Monitor.__init__(self, extra_params) + Dot2c.__init__(self, file_path, extra_params.get("model_name")) + self.enum_suffix = "_%s" % self.name + + def fill_monitor_type(self): + return self.monitor_type.upper() + + def fill_tracepoint_handlers_skel(self): + buff = [] + for event in self.events: + buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) + buff.append("{") + handle = "handle_event" + if self.is_start_event(event): + buff.append("\t/* XXX: validate that this event always leads to the initial state */") + handle = "handle_start_event" + elif self.is_start_run_event(event): + buff.append("\t/* XXX: validate that this event is only valid in the initial state */") + handle = "handle_start_run_event" + if self.monitor_type == "per_task": + buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); + buff.append("\tda_%s_%s(p, %s%s);" % (handle, self.name, event, self.enum_suffix)); + else: + buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix)); + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + buff = [] + for event in self.events: + buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_tracepoint_detach_helper(self): + buff = [] + for event in self.events: + buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_model_h_header(self): + buff = [] + buff.append("/* SPDX-License-Identifier: GPL-2.0 */") + buff.append("/*") + buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) + buff.append(" * For further information about this format, see kernel documentation:") + buff.append(" * Documentation/trace/rv/deterministic_automata.rst") + buff.append(" */") + buff.append("") + + return buff + + def fill_model_h(self): + # + # Adjust the definition names + # + self.enum_states_def = "states_%s" % self.name + self.enum_events_def = "events_%s" % self.name + self.struct_automaton_def = "automaton_%s" % self.name + self.var_automaton_def = "automaton_%s" % self.name + + buff = self.fill_model_h_header() + buff += self.format_model() + + return '\n'.join(buff) + + def fill_monitor_class_type(self): + if self.monitor_type == "per_task": + return "DA_MON_EVENTS_ID" + return "DA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self): + if self.monitor_type == "per_task": + return "da_monitor_id" + return "da_monitor" + + def fill_tracepoint_args_skel(self, tp_type): + buff = [] + tp_args_event = [ + ("char *", "state"), + ("char *", "event"), + ("char *", "next_state"), + ("bool ", "final_state"), + ] + tp_args_error = [ + ("char *", "state"), + ("char *", "event"), + ] + tp_args_id = ("int ", "id") + tp_args = tp_args_event if tp_type == "event" else tp_args_error + if self.monitor_type == "per_task": + tp_args.insert(0, tp_args_id) + tp_proto_c = ", ".join([a+b for a,b in tp_args]) + tp_args_c = ", ".join([b for a,b in tp_args]) + buff.append(" TP_PROTO(%s)," % tp_proto_c) + buff.append(" TP_ARGS(%s)" % tp_args_c) + return '\n'.join(buff) + + def fill_main_c(self): + main_c = super().fill_main_c() + + min_type = self.get_minimun_type() + nr_events = len(self.events) + monitor_type = self.fill_monitor_type() + + main_c = main_c.replace("%%MIN_TYPE%%", min_type) + main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) + main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) + + return main_c diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/rvgen/rvgen/generator.py index 745d35a4a379..3441385c1177 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -3,74 +3,27 @@ # # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> # -# dot2k: transform dot files into a monitor for the Linux kernel. -# -# For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst +# Abtract class for generating kernel runtime verification monitors from specification file -from dot2.dot2c import Dot2c import platform import os -class dot2k(Dot2c): - monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir = "dot2/dot2k_templates/" + +class RVGenerator: rv_dir = "kernel/trace/rv" - monitor_type = "per_cpu" - def __init__(self, file_path, MonitorType, extra_params={}): - self.container = extra_params.get("container") + def __init__(self, extra_params={}): + self.name = extra_params.get("model_name") self.parent = extra_params.get("parent") - self.__fill_rv_templates_dir() - - if self.container: - if file_path: - raise ValueError("A container does not require a dot file") - if MonitorType: - raise ValueError("A container does not require a monitor type") - if self.parent: - raise ValueError("A container cannot have a parent") - self.name = extra_params.get("model_name") - self.events = [] - self.states = [] - self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c") - self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h") - else: - super().__init__(file_path, extra_params.get("model_name")) - - self.monitor_type = self.monitor_types.get(MonitorType) - if self.monitor_type is None: - raise ValueError("Unknown monitor type: %s" % MonitorType) - self.monitor_type = MonitorType - self.main_c = self.__read_file(self.monitor_templates_dir + "main.c") - self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h") - self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig") - self.enum_suffix = "_%s" % self.name + self.abs_template_dir = \ + os.path.join(os.path.dirname(__file__), "templates", self.template_dir) + self.main_c = self._read_template_file("main.c") + self.kconfig = self._read_template_file("Kconfig") self.description = extra_params.get("description", self.name) or "auto-generated" self.auto_patch = extra_params.get("auto_patch") if self.auto_patch: self.__fill_rv_kernel_dir() - def __fill_rv_templates_dir(self): - - if os.path.exists(self.monitor_templates_dir): - return - - if platform.system() != "Linux": - raise OSError("I can only run on Linux.") - - kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release()) - - if os.path.exists(kernel_path): - self.monitor_templates_dir = kernel_path - return - - if os.path.exists("/usr/share/dot2/dot2k_templates/"): - self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/" - return - - raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?") - def __fill_rv_kernel_dir(self): # first try if we are running in the kernel tree root @@ -97,7 +50,7 @@ class dot2k(Dot2c): raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") - def __read_file(self, path): + def _read_file(self, path): try: fd = open(path, 'r') except OSError: @@ -108,17 +61,15 @@ class dot2k(Dot2c): fd.close() return content - def __buff_to_string(self, buff): - string = "" - - for line in buff: - string = string + line + "\n" - - # cut off the last \n - return string[:-1] - - def fill_monitor_type(self): - return self.monitor_type.upper() + def _read_template_file(self, file): + try: + path = os.path.join(self.abs_template_dir, file) + return self._read_file(path) + except Exception: + # Specific template file not found. Try the generic template file in the template/ + # directory, which is one level up + path = os.path.join(self.abs_template_dir, "..", file) + return self._read_file(path) def fill_parent(self): return "&rv_%s" % self.parent if self.parent else "NULL" @@ -129,53 +80,23 @@ class dot2k(Dot2c): return "" def fill_tracepoint_handlers_skel(self): - buff = [] - for event in self.events: - buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) - buff.append("{") - handle = "handle_event" - if self.is_start_event(event): - buff.append("\t/* XXX: validate that this event always leads to the initial state */") - handle = "handle_start_event" - elif self.is_start_run_event(event): - buff.append("\t/* XXX: validate that this event is only valid in the initial state */") - handle = "handle_start_run_event" - if self.monitor_type == "per_task": - buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); - buff.append("\tda_%s_%s(p, %s%s);" % (handle, self.name, event, self.enum_suffix)); - else: - buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix)); - buff.append("}") - buff.append("") - return self.__buff_to_string(buff) + return "NotImplemented" def fill_tracepoint_attach_probe(self): - buff = [] - for event in self.events: - buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) + return "NotImplemented" def fill_tracepoint_detach_helper(self): - buff = [] - for event in self.events: - buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) + return "NotImplemented" def fill_main_c(self): main_c = self.main_c - monitor_type = self.fill_monitor_type() - min_type = self.get_minimun_type() - nr_events = len(self.events) tracepoint_handlers = self.fill_tracepoint_handlers_skel() tracepoint_attach = self.fill_tracepoint_attach_probe() tracepoint_detach = self.fill_tracepoint_detach_helper() parent = self.fill_parent() parent_include = self.fill_include_parent() - main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) - main_c = main_c.replace("%%MIN_TYPE%%", min_type) main_c = main_c.replace("%%MODEL_NAME%%", self.name) - main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers) main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach) main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach) @@ -185,63 +106,17 @@ class dot2k(Dot2c): return main_c - def fill_model_h_header(self): - buff = [] - buff.append("/* SPDX-License-Identifier: GPL-2.0 */") - buff.append("/*") - buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) - buff.append(" * For further information about this format, see kernel documentation:") - buff.append(" * Documentation/trace/rv/deterministic_automata.rst") - buff.append(" */") - buff.append("") - - return buff - def fill_model_h(self): - # - # Adjust the definition names - # - self.enum_states_def = "states_%s" % self.name - self.enum_events_def = "events_%s" % self.name - self.struct_automaton_def = "automaton_%s" % self.name - self.var_automaton_def = "automaton_%s" % self.name - - buff = self.fill_model_h_header() - buff += self.format_model() - - return self.__buff_to_string(buff) + return "NotImplemented" def fill_monitor_class_type(self): - if self.monitor_type == "per_task": - return "DA_MON_EVENTS_ID" - return "DA_MON_EVENTS_IMPLICIT" + return "NotImplemented" def fill_monitor_class(self): - if self.monitor_type == "per_task": - return "da_monitor_id" - return "da_monitor" + return "NotImplemented" def fill_tracepoint_args_skel(self, tp_type): - buff = [] - tp_args_event = [ - ("char *", "state"), - ("char *", "event"), - ("char *", "next_state"), - ("bool ", "final_state"), - ] - tp_args_error = [ - ("char *", "state"), - ("char *", "event"), - ] - tp_args_id = ("int ", "id") - tp_args = tp_args_event if tp_type == "event" else tp_args_error - if self.monitor_type == "per_task": - tp_args.insert(0, tp_args_id) - tp_proto_c = ", ".join([a+b for a,b in tp_args]) - tp_args_c = ", ".join([b for a,b in tp_args]) - buff.append(" TP_PROTO(%s)," % tp_proto_c) - buff.append(" TP_ARGS(%s)" % tp_args_c) - return self.__buff_to_string(buff) + return "NotImplemented" def fill_monitor_deps(self): buff = [] @@ -249,21 +124,7 @@ class dot2k(Dot2c): if self.parent: buff.append(" depends on RV_MON_%s" % self.parent.upper()) buff.append(" default y") - return self.__buff_to_string(buff) - - def fill_trace_h(self): - trace_h = self.trace_h - monitor_class = self.fill_monitor_class() - monitor_class_type = self.fill_monitor_class_type() - tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") - tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") - trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) - trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) - trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) - trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) - trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) - trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) - return trace_h + return '\n'.join(buff) def fill_kconfig(self): kconfig = self.kconfig @@ -276,21 +137,17 @@ class dot2k(Dot2c): kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) return kconfig - def fill_main_container_h(self): - main_h = self.main_h - main_h = main_h.replace("%%MODEL_NAME%%", self.name) - return main_h - - def __patch_file(self, file, marker, line): + def _patch_file(self, file, marker, line): + assert self.auto_patch file_to_patch = os.path.join(self.rv_dir, file) - content = self.__read_file(file_to_patch) + content = self._read_file(file_to_patch) content = content.replace(marker, line + "\n" + marker) self.__write_file(file_to_patch, content) def fill_tracepoint_tooltip(self): monitor_class_type = self.fill_monitor_class_type() if self.auto_patch: - self.__patch_file("rv_trace.h", + self._patch_file("rv_trace.h", "// Add new monitors based on CONFIG_%s here" % monitor_class_type, "#include <monitors/%s/%s_trace.h>" % (self.name, self.name)) return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir @@ -300,10 +157,15 @@ Add this line where other tracepoints are included and %s is defined: #include <monitors/%s/%s_trace.h> """ % (self.rv_dir, monitor_class_type, self.name, self.name) + def _kconfig_marker(self, container=None) -> str: + return "# Add new %smonitors here" % (container + " " + if container else "") + def fill_kconfig_tooltip(self): if self.auto_patch: - self.__patch_file("Kconfig", - "# Add new monitors here", + # monitors with a container should stay together in the Kconfig + self._patch_file("Kconfig", + self._kconfig_marker(self.parent), "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name)) return " - Patching %s/Kconfig, double check the result" % self.rv_dir @@ -316,7 +178,7 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\" name = self.name name_up = name.upper() if self.auto_patch: - self.__patch_file("Makefile", + self._patch_file("Makefile", "# Add new monitors here", "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name)) return " - Patching %s/Makefile, double check the result" % self.rv_dir @@ -352,7 +214,7 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o file.close() - def __create_file(self, file_name, content): + def _create_file(self, file_name, content): path = "%s/%s" % (self.name, file_name) if self.auto_patch: path = os.path.join(self.rv_dir, "monitors", path) @@ -370,20 +232,39 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o self.__create_directory() path = "%s.c" % self.name - self.__create_file(path, main_c) - - if self.container: - main_h = self.fill_main_container_h() - path = "%s.h" % self.name - self.__create_file(path, main_h) - else: - model_h = self.fill_model_h() - path = "%s.h" % self.name - self.__create_file(path, model_h) + self._create_file(path, main_c) - trace_h = self.fill_trace_h() - path = "%s_trace.h" % self.name - self.__create_file(path, trace_h) + model_h = self.fill_model_h() + path = "%s.h" % self.name + self._create_file(path, model_h) kconfig = self.fill_kconfig() - self.__create_file("Kconfig", kconfig) + self._create_file("Kconfig", kconfig) + + +class Monitor(RVGenerator): + monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.trace_h = self._read_template_file("trace.h") + + def fill_trace_h(self): + trace_h = self.trace_h + monitor_class = self.fill_monitor_class() + monitor_class_type = self.fill_monitor_class_type() + tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") + tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") + trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) + trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) + trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) + trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) + return trace_h + + def print_files(self): + super().print_files() + trace_h = self.fill_trace_h() + path = "%s_trace.h" % self.name + self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000000..f14e6760ac3d --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,566 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Implementation based on +# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). +# Simple On-the-fly Automatic Verification of Linear Temporal Logic. +# https://doi.org/10.1007/978-0-387-34892-6_1 +# With extra optimizations + +from ply.lex import lex +from ply.yacc import yacc + +# Grammar: +# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl +# +# Operands (opd): +# true, false, user-defined names +# +# Unary Operators (unop): +# always +# eventually +# next +# not +# +# Binary Operators (binop): +# until +# and +# or +# imply +# equivalent + +tokens = ( + 'AND', + 'OR', + 'IMPLY', + 'UNTIL', + 'ALWAYS', + 'EVENTUALLY', + 'NEXT', + 'VARIABLE', + 'LITERAL', + 'NOT', + 'LPAREN', + 'RPAREN', + 'ASSIGN', +) + +t_AND = r'and' +t_OR = r'or' +t_IMPLY = r'imply' +t_UNTIL = r'until' +t_ALWAYS = r'always' +t_NEXT = r'next' +t_EVENTUALLY = r'eventually' +t_VARIABLE = r'[A-Z_0-9]+' +t_LITERAL = r'true|false' +t_NOT = r'not' +t_LPAREN = r'\(' +t_RPAREN = r'\)' +t_ASSIGN = r'=' +t_ignore_COMMENT = r'\#.*' +t_ignore = ' \t\n' + +def t_error(t): + raise ValueError(f"Illegal character '{t.value[0]}'") + +lexer = lex() + +class GraphNode: + uid = 0 + + def __init__(self, incoming: set['GraphNode'], new, old, _next): + self.init = False + self.outgoing = set() + self.labels = set() + self.incoming = incoming.copy() + self.new = new.copy() + self.old = old.copy() + self.next = _next.copy() + self.id = GraphNode.uid + GraphNode.uid += 1 + + def expand(self, node_set): + if not self.new: + for nd in node_set: + if nd.old == self.old and nd.next == self.next: + nd.incoming |= self.incoming + return node_set + + new_current_node = GraphNode({self}, self.next, set(), set()) + return new_current_node.expand({self} | node_set) + n = self.new.pop() + return n.expand(self, node_set) + + def __lt__(self, other): + return self.id < other.id + +class ASTNode: + uid = 1 + + def __init__(self, op): + self.op = op + self.id = ASTNode.uid + ASTNode.uid += 1 + + def __hash__(self): + return hash(self.op) + + def __eq__(self, other): + return self is other + + def __iter__(self): + yield self + yield from self.op + + def negate(self): + self.op = self.op.negate() + return self + + def expand(self, node, node_set): + return self.op.expand(self, node, node_set) + + def __str__(self): + if isinstance(self.op, Literal): + return str(self.op.value) + if isinstance(self.op, Variable): + return self.op.name.lower() + return "val" + str(self.id) + + def normalize(self): + # Get rid of: + # - ALWAYS + # - EVENTUALLY + # - IMPLY + # And move all the NOT to be inside + self.op = self.op.normalize() + return self + +class BinaryOp: + op_str = "not_supported" + + def __init__(self, left: ASTNode, right: ASTNode): + self.left = left + self.right = right + + def __hash__(self): + return hash((self.left, self.right)) + + def __iter__(self): + yield from self.left + yield from self.right + + def normalize(self): + raise NotImplementedError + + def negate(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.left.op.is_temporal(): + return True + if self.right.op.is_temporal(): + return True + return self._is_temporal() + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + raise NotImplementedError + +class AndOp(BinaryOp): + op_str = '&&' + + def normalize(self): + return self + + def negate(self): + return OrOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old.add(n) + return node.expand(node_set) + + tmp = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return tmp.expand(node_set) + +class OrOp(BinaryOp): + op_str = '||' + + def normalize(self): + return self + + def negate(self): + return AndOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old |= {n} + return node.expand(node_set) + + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class UntilOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return VOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class VOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return UntilOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class ImplyOp(BinaryOp): + def normalize(self): + # P -> Q === !P | Q + return OrOp(self.left.negate(), self.right) + + def _is_temporal(self): + return False + + def negate(self): + # !(P -> Q) === !(!P | Q) === P & !Q + return AndOp(self.left, self.right.negate()) + +class UnaryOp: + def __init__(self, child: ASTNode): + self.child = child + + def __iter__(self): + yield from self.child + + def __hash__(self): + return hash(self.child) + + def normalize(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.child.op.is_temporal(): + return True + return self._is_temporal() + + def negate(self): + raise NotImplementedError + +class EventuallyOp(UnaryOp): + def __str__(self): + return "eventually " + str(self.child) + + def normalize(self): + # <>F == true U F + return UntilOp(ASTNode(Literal(True)), self.child) + + def _is_temporal(self): + return True + + def negate(self): + # !<>F == [](!F) + return AlwaysOp(self.child.negate()).normalize() + +class AlwaysOp(UnaryOp): + def normalize(self): + # []F === !(true U !F) == false V F + new = ASTNode(Literal(False)) + return VOp(new, self.child) + + def _is_temporal(self): + return True + + def negate(self): + # ![]F == <>(!F) + return EventuallyOp(self.child.negate()).normalize() + +class NextOp(UnaryOp): + def normalize(self): + return self + + def _is_temporal(self): + return True + + def negate(self): + # not (next A) == next (not A) + self.child = self.child.negate() + return self + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + tmp = GraphNode(node.incoming, + node.new, + node.old | {n}, + node.next | {n.op.child}) + return tmp.expand(node_set) + +class NotOp(UnaryOp): + def __str__(self): + return "!" + str(self.child) + + def normalize(self): + return self.child.op.negate() + + def negate(self): + return self.child.op + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if n.op.child is f: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Variable: + def __init__(self, name: str): + self.name = name + + def __hash__(self): + return hash(self.name) + + def __iter__(self): + yield from () + + def negate(self): + new = ASTNode(self) + return NotOp(new) + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if isinstance(f, NotOp) and f.op.child is n: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Literal: + def __init__(self, value: bool): + self.value = value + + def __iter__(self): + yield from () + + def __hash__(self): + return hash(self.value) + + def __str__(self): + if self.value: + return "true" + return "false" + + def negate(self): + self.value = not self.value + return self + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.value: + return node_set + node.old |= {n} + return node.expand(node_set) + +def p_spec(p): + ''' + spec : assign + | assign spec + ''' + if len(p) == 3: + p[2].append(p[1]) + p[0] = p[2] + else: + p[0] = [p[1]] + +def p_assign(p): + ''' + assign : VARIABLE ASSIGN ltl + ''' + p[0] = (p[1], p[3]) + +def p_ltl(p): + ''' + ltl : opd + | binop + | unop + ''' + p[0] = p[1] + +def p_opd(p): + ''' + opd : VARIABLE + | LITERAL + | LPAREN ltl RPAREN + ''' + if p[1] == "true": + p[0] = ASTNode(Literal(True)) + elif p[1] == "false": + p[0] = ASTNode(Literal(False)) + elif p[1] == '(': + p[0] = p[2] + else: + p[0] = ASTNode(Variable(p[1])) + +def p_unop(p): + ''' + unop : ALWAYS ltl + | EVENTUALLY ltl + | NEXT ltl + | NOT ltl + ''' + if p[1] == "always": + op = AlwaysOp(p[2]) + elif p[1] == "eventually": + op = EventuallyOp(p[2]) + elif p[1] == "next": + op = NextOp(p[2]) + elif p[1] == "not": + op = NotOp(p[2]) + else: + raise ValueError(f"Invalid unary operator {p[1]}") + + p[0] = ASTNode(op) + +def p_binop(p): + ''' + binop : opd UNTIL ltl + | opd AND ltl + | opd OR ltl + | opd IMPLY ltl + ''' + if p[2] == "and": + op = AndOp(p[1], p[3]) + elif p[2] == "until": + op = UntilOp(p[1], p[3]) + elif p[2] == "or": + op = OrOp(p[1], p[3]) + elif p[2] == "imply": + op = ImplyOp(p[1], p[3]) + else: + raise ValueError(f"Invalid binary operator {p[2]}") + + p[0] = ASTNode(op) + +parser = yacc() + +def parse_ltl(s: str) -> ASTNode: + spec = parser.parse(s) + + rule = None + subexpr = {} + + for assign in spec: + if assign[0] == "RULE": + rule = assign[1] + else: + subexpr[assign[0]] = assign[1] + + if rule is None: + raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format") + + for node in rule: + if not isinstance(node.op, Variable): + continue + replace = subexpr.get(node.op.name) + if replace is not None: + node.op = replace.op + + return rule + +def create_graph(s: str): + atoms = set() + + ltl = parse_ltl(s) + for c in ltl: + c.normalize() + if isinstance(c.op, Variable): + atoms.add(c.op.name) + + init = GraphNode(set(), set(), set(), set()) + head = GraphNode({init}, {ltl}, set(), set()) + graph = sorted(head.expand(set())) + + for i, node in enumerate(graph): + # The id assignment during graph generation has gaps. Reassign them + node.id = i + + for incoming in node.incoming: + if incoming is init: + node.init = True + else: + incoming.outgoing.add(node) + for o in node.old: + if not o.op.is_temporal(): + node.labels.add(str(o)) + + return sorted(atoms), graph, ltl diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py new file mode 100644 index 000000000000..b075f98d50c4 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba + +COLUMN_LIMIT = 100 + +def line_len(line: str) -> int: + tabs = line.count('\t') + return tabs * 7 + len(line) + +def break_long_line(line: str, indent='') -> list[str]: + result = [] + while line_len(line) > COLUMN_LIMIT: + i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ') + result.append(line[:i]) + line = indent + line[i + 1:] + if line: + result.append(line) + return result + +def build_condition_string(node: ltl2ba.GraphNode): + if not node.labels: + return "(true)" + + result = "(" + + first = True + for label in sorted(node.labels): + if not first: + result += " && " + result += label + first = False + + result += ")" + + return result + +def abbreviate_atoms(atoms: list[str]) -> list[str]: + def shorten(s: str) -> str: + skip = ["is", "by", "or", "and"] + return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip]) + + abbrs = [] + for atom in atoms: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + break + share = atom[:i] + unique = atom[i:] + abbrs.append((shorten(share) + shorten(unique))) + return abbrs + +class ltl2k(generator.Monitor): + template_dir = "ltl2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + if MonitorType != "per_task": + raise NotImplementedError("Only per_task monitor is supported for LTL") + super().__init__(extra_params) + with open(file_path) as f: + self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read()) + self.atoms_abbr = abbreviate_atoms(self.atoms) + self.name = extra_params.get("model_name") + if not self.name: + self.name = Path(file_path).stem + + def _fill_states(self) -> str: + buf = [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append("\tS%i," % node.id) + buf.append("\tRV_NUM_BA_STATES") + buf.append("};") + buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);") + return buf + + def _fill_atoms(self): + buf = ["enum ltl_atom {"] + for a in sorted(self.atoms): + buf.append("\tLTL_%s," % a) + buf.append("\tLTL_NUM_ATOM") + buf.append("};") + buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);") + return buf + + def _fill_atoms_to_string(self): + buf = [ + "static const char *ltl_atom_str(enum ltl_atom atom)", + "{", + "\tstatic const char *const names[] = {" + ] + + for name in self.atoms_abbr: + buf.append("\t\t\"%s\"," % name) + + buf.extend([ + "\t};", + "", + "\treturn names[atom];", + "}" + ]) + return buf + + def _fill_atom_values(self, required_values): + buf = [] + for node in self.ltl: + if str(node) not in required_values: + continue + + if isinstance(node.op, ltl2ba.AndOp): + buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.OrOp): + buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.NotOp): + buf.append("\tbool %s = !%s;" % (node, node.op.child)) + required_values.add(str(node.op.child)) + + for atom in self.atoms: + if atom.lower() not in required_values: + continue + buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom)) + + buf.reverse() + + buf2 = [] + for line in buf: + buf2.extend(break_long_line(line, "\t ")) + return buf2 + + def _fill_transitions(self): + buf = [ + "static void", + "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)", + "{" + ] + + required_values = set() + for node in self.ba: + for o in sorted(node.outgoing): + required_values |= o.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.extend([ + "", + "\tswitch (state) {" + ]) + + for node in self.ba: + buf.append("\tcase S%i:" % node.id) + + for o in sorted(node.outgoing): + line = "\t\tif " + indent = "\t\t " + + line += build_condition_string(o) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t\t__set_bit(S%i, next);" % o.id) + buf.append("\t\tbreak;") + buf.extend([ + "\t}", + "}" + ]) + + return buf + + def _fill_start(self): + buf = [ + "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)", + "{" + ] + + required_values = set() + for node in self.ba: + if node.init: + required_values |= node.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.append("") + + for node in self.ba: + if not node.init: + continue + + line = "\tif " + indent = "\t " + + line += build_condition_string(node) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) + buf.append("}") + return buf + + def fill_tracepoint_handlers_skel(self): + buff = [] + buff.append("static void handle_example_event(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0]) + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \ + % self.name + + def fill_tracepoint_detach_helper(self): + return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \ + % self.name + + def fill_atoms_init(self): + buff = [] + for a in self.atoms: + buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a) + return '\n'.join(buff) + + def fill_model_h(self): + buf = [ + "/* SPDX-License-Identifier: GPL-2.0 */", + "", + "/*", + " * C implementation of Buchi automaton, automatically generated by", + " * tools/verification/rvgen from the linear temporal logic specification.", + " * For further information, see kernel documentation:", + " * Documentation/trace/rv/linear_temporal_logic.rst", + " */", + "", + "#include <linux/rv.h>", + "", + "#define MONITOR_NAME " + self.name, + "" + ] + + buf.extend(self._fill_atoms()) + buf.append('') + + buf.extend(self._fill_atoms_to_string()) + buf.append('') + + buf.extend(self._fill_states()) + buf.append('') + + buf.extend(self._fill_start()) + buf.append('') + + buf.extend(self._fill_transitions()) + buf.append('') + + return '\n'.join(buf) + + def fill_monitor_class_type(self): + return "LTL_MON_EVENTS_ID" + + def fill_monitor_class(self): + return "ltl_monitor_id" + + def fill_main_c(self): + main_c = super().fill_main_c() + main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + + return main_c diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig index 291b29ea28db..291b29ea28db 100644 --- a/tools/verification/dot2/dot2k_templates/Kconfig +++ b/tools/verification/rvgen/rvgen/templates/Kconfig diff --git a/tools/verification/rvgen/rvgen/templates/container/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig new file mode 100644 index 000000000000..a606111949c2 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig @@ -0,0 +1,5 @@ +config RV_MON_%%MODEL_NAME_UP%% + depends on RV + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/rvgen/rvgen/templates/container/main.c index 89fc17cf8958..7d9b2f95c7e9 100644 --- a/tools/verification/dot2/dot2k_templates/main_container.c +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -21,8 +21,7 @@ struct rv_monitor rv_%%MODEL_NAME%% = { static int __init register_%%MODEL_NAME%%(void) { - rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); - return 0; + return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); } static void __exit unregister_%%MODEL_NAME%%(void) diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/rvgen/rvgen/templates/container/main.h index 0f6883ab4bcc..0f6883ab4bcc 100644 --- a/tools/verification/dot2/dot2k_templates/main_container.h +++ b/tools/verification/rvgen/rvgen/templates/container/main.h diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c index 83044a20c89a..e0fd1134bd85 100644 --- a/tools/verification/dot2/dot2k_templates/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -74,8 +74,7 @@ static struct rv_monitor rv_%%MODEL_NAME%% = { static int __init register_%%MODEL_NAME%%(void) { - rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); - return 0; + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); } static void __exit unregister_%%MODEL_NAME%%(void) diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h index 87d3a1308926..87d3a1308926 100644 --- a/tools/verification/dot2/dot2k_templates/trace.h +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c new file mode 100644 index 000000000000..f85d076fbf78 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> + +#define MODULE_NAME "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +%%INCLUDE_PARENT%% + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "%%MODEL_NAME%%.h" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + /* + * This is called everytime the Buchi automaton is triggered. + * + * This function could be used to fetch the atomic propositions which + * are expensive to trace. It is possible only if the atomic proposition + * does not need to be updated at precise time. + * + * It is recommended to use tracepoints and ltl_atom_update() instead. + */ +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + /* + * This should initialize as many atomic propositions as possible. + * + * @task_creation indicates whether the task is being created. This is + * false if the task is already running before the monitor is enabled. + */ +%%ATOMS_INIT%% +} + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel events + * are translated into model's event. + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ +%%TRACEPOINT_DETACH%% + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR(/* TODO */); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h new file mode 100644 index 000000000000..49394c4b0f1c --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ |