mirrors/linux
2
0
Fork 0
mirror of https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git synced 2026-08-30 13:23:02 -04:00
Code Issues Packages Projects Releases Wiki Activity

Merge tag 'trace-rv-v7.3' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace

Browse Source 
Pull Real-time Verifier updates from Steven Rostedt:

 - Switch LTL and DOT parsers to Lark in code generation tool

   The rvgen code generation tool originally parsed DOT files and LTL
   specifications using custom string parsing and Ply, which is no
   longer maintained. The DOT parser was fragile and prone to failure on
   minor format variations. Both LTL and DOT parsers have been rewritten
   to use the Lark parsing library.

 - Simplify Hybrid Automata clock variables

   The clock variables in hybrid automata monitors now use a single
   representation of the elapsed time since the clock was reset, rather
   than converting between invariant and guard representations. This
   allows simpler code generation for the newly refactored parser.

 - Generate cleanup hook for per-obj monitor

   The code generation scripts now adds a cleanup function to per-obj
   monitors for the user to wire to the appropriate event (e.g.
   sched_process_exit for tasks).

 - Reduce read_lock scope during per-task cleanup

   Take the tasklist_lock only when necessary, that is when iterating
   over for_each_process_thread().

 - Simplify task monitor slot management

   Only rely on the slot array for per-task slot management to avoid
   inconsistency with the unused counter.

 - Improve rvgen code robustness and templates

   Use pathlib in rvgen and improve kernel path discovery. Also improve
   consistency across templates when generating code (e.g. author
   placeholder and monitor struct name).

 - Update rtapp sleep monitor

   Simplify the sleep monitor by excluding kernel threads and updating
   the nanosleep check to focus only on CLOCK_REALTIME. Also switch to
   use the sched_exit tracepoint to run in the context of the offending
   (wakee) task.

 - Add wakeup monitor

   Add the new rtapp/wakeup monitor to detect when lower-priority tasks
   wake up higher-priority ones, complementing the existing sleep
   monitor by running in the waker context and capturing its stack
   trace.

 - Fix tools/rv exit status on failure

   Ensure the rv tool returns a failure exit code when a monitor fails
   to start because it was already running.

 - Add automated selftests for tools/rv and rvgen

   Introduced automated bash selftests to validate rv monitor listing
   and execution under different configurations. Added tests for the
   rvgen code generator, validating generated files against expected
   output (golden). Tests are reachable via make check.

 - Add KUnit test coverage for verification monitors

   Added comprehensive KUnit tests to validate the functionality of
   deterministic, hybrid, and LTL monitors by emulating event sequences
   and timing in a mock environment without affecting the running kernel
   while expecting mock reactions to fire. Ensure real RV monitors
   cannot run during KUnit tests to avoid state corruption.

 - Mock current in rv monitors

   Mock the call to current in rv monitors when the KUnit tests are
   built to allow them to run the test on dummy tasks. No overhead is
   expected when KUnit tests aren't running.

 - Introduce rvgen kunit subcommand

   Added a new 'kunit' subcommand to rvgen to automatically patch an
   already generated monitor with KUnit integration templates by parsing
   its event handlers and creating the required mock structures and
   initializations.

 - Refine kernel verification selftests

   Added new selftests for the deadline and stall monitors and
   rearranged the existing wwnr_printk test to resolve flakiness.
   Additionally, fixed an issue in the selftests framework where
   negative assertion failures were not correctly propagated due to
   shell rules.

 - Fix 32-bit build of nomiss KUnit test

   A previous commit introduced a division between an u64 and a constant
   value and that doesn't build on 32-bit systems. Use div_u64()
   instead.

 - Document changes in sleep monitor

   The sleep monitor introduced some changes in the past like allowing
   epoll_wait() as a valid sleep and a task going to runnable before
   scheduling as a valid wakeup. Document both.

* tag 'trace-rv-v7.3' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: (40 commits)
  Documentation/rv: Explain epoll and aborted sleeps
  rv: Fix 32-bit build of nomiss KUnit test
  selftests/verification: Add selftests for deadline and stall monitors
  selftests/verification: Rearrange the wwnr_printk test
  selftests/verification: Fix wrong errexit assumption
  rv: Add KUnit tests for some LTL monitors
  rv: Add KUnit mock for current
  rv: Add KUnit tests for some DA/HA monitors
  rv: Export task monitor slot and react symbols
  verification/rvgen: Add selftests for rvgen kunit
  verification/rvgen: Add the rvgen kunit subcommand
  verification/rvgen: Add selftests
  verification/rvgen: Add golden and spec folders for tests
  tools/rv: Add selftests
  verification/rvgen: Improve consistency in template files
  verification/rvgen: Use pathlib instead of os.path
  verification/rvgen: Improve rv_dir discovery in RVGenerator
  tools/rv: Fix exit status when monitor execution fails
  rv: Use generic rv_this for the rv_monitor variable in LTL
  rv/rtapp: Add wakeup monitor
  ...
This commit is contained in:
Linus Torvalds
2026-08-19 13:29:22 -07:00
parent 98f21c54f9 7d81675d1b
commit 55ee4b931a
135 changed files with 6096 additions and 883 deletions
Download Patch File Download Diff File Expand all files Collapse all files

63
Documentation/trace/rv/monitor_rtapp.rst
View File

@@ -51,12 +51,13 @@ 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.
- 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). Additionally,
`CLOCK_REALTIME` should not be used (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
@@ -66,6 +67,8 @@ thread to sleep for one of the following reasons:
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.
- Real-time thread waiting for events using `epoll_wait`, which is a
real-time-safe syscall for sleeping as it uses PI-aware locking.
Beside the reason for sleeping, the eventual waker should also be
real-time-safe. Namely, one of:
@@ -92,38 +95,34 @@ assessment.
The monitor's specification is::
RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
and ((not WAKE) until RT_FRIENDLY_WAKE)
RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
or EPOLL_WAIT
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
and NANOSLEEP_CLOCK_MONOTONIC
and not NANOSLEEP_CLOCK_REALTIME
RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
or KTHREAD_SHOULD_STOP
or ABORT_SLEEP
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:
`ABORT_SLEEP` represents a task restoring its state to `TASK_RUNNING` before
entering the scheduler. In this case, the task does not actually block, so the
task is back to runnable without any wakeup sequence unsafe for real-time.
Beside the scenarios described above, this specification also defines an allow list
to 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
@@ -131,3 +130,23 @@ special cases:
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`.
Monitor wakeup
++++++++++++++
The `wakeup` monitor reports real-time threads being woken by lower-priority threads,
which is a hint of priority inversion. Its specification is::
RULE = always (((RT and USER_THREAD) imply
(not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI
The `sleep` monitor already reports this type of problem. The difference is the
context in which the problem is reported. While the `sleep` monitor reports the problem
in the context of the wakee, this `wakeup` monitor reports the problem in the context of
the waker. This monitor complement the `sleep` monitor, giving user better
understanding of the issue. For instance, to debug a lower-priority task waking a
higher-priority task scenario, user can enable both `wakeup` monitor and `sleep`
monitor to get the stack traces of both tasks.

31
include/rv/da_monitor.h
View File

@@ -16,6 +16,7 @@
#include <rv/automata.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <linux/stringify.h>
#include <linux/bug.h>
#include <linux/sched.h>
@@ -311,6 +312,11 @@ static inline struct da_monitor *da_get_monitor(struct task_struct *tsk)
return &tsk->rv[task_mon_slot].da_mon;
}
static inline void da_reset(struct task_struct *tsk)
{
da_monitor_reset(da_get_monitor(tsk));
}
/*
* da_get_target - return the task associated to the monitor
*/
@@ -334,12 +340,12 @@ static void __da_monitor_reset_all(void (*reset)(struct da_monitor *))
struct task_struct *g, *p;
int cpu;
read_lock(&tasklist_lock);
for_each_process_thread(g, p)
reset(da_get_monitor(p));
scoped_guard(read_lock, &tasklist_lock) {
for_each_process_thread(g, p)
reset(da_get_monitor(p));
}
for_each_present_cpu(cpu)
reset(da_get_monitor(idle_task(cpu)));
read_unlock(&tasklist_lock);
}
static void da_monitor_reset_all(void)
@@ -908,4 +914,21 @@ static inline void da_reset(da_id_type id, monitor_target target)
}
#endif /* RV_MON_TYPE */
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#if RV_MON_TYPE == RV_MON_PER_TASK
#define RV_MON_OPS_INIT() { \
.rv_this = &rv_this, \
.is_per_task = true, \
.task_slot = &task_mon_slot, \
.task_reset = da_reset, \
}
#else
#define RV_MON_OPS_INIT() { \
.rv_this = &rv_this, \
.monitor_init = da_monitor_init, \
.monitor_destroy = da_monitor_destroy, \
}
#endif /* RV_MON_TYPE */
#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
#endif

85
include/rv/ha_monitor.h
View File

@@ -327,19 +327,8 @@ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
}
/*
* The clock variables have 2 different representations in the env_store:
* - The guard representation is the timestamp of the last reset
* - The invariant representation is the timestamp when the invariant expires
* As the representations are incompatible, care must be taken when switching
* between them: the invariant representation can only be used when starting a
* timer when the previous representation was guard (e.g. no other invariant
* started since the last reset operation).
* Likewise, switching from invariant to guard representation without a reset
* can be done only by subtracting the exact value used to start the invariant.
*
* Reading the environment variable (ha_get_clk) also reflects this difference
* any reads in states that have an invariant return the (possibly negative)
* time since expiration, other reads return the time since last reset.
* The clock variables store the time epoch - the timestamp when the clock was last reset.
* They are read by subtracting the time epoch from the current time.
*/
/*
@@ -353,31 +342,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64
{
WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
u64 value, u64 time_ns)
static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
u64 time_ns, u64 expire_ns)
{
WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
}
static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
enum envs env, u64 time_ns)
{
return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
return READ_ONCE(ha_mon->env_store[env]) >= time_ns - expire_ns;
}
/*
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
*/
static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
u64 passed = 0;
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
passed = ha_get_env(ha_mon, env, time_ns);
ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
return passed;
return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -391,32 +370,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
enum envs env, u64 value)
static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 time_ns, u64 expire_jiffy)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
}
static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
enum envs env, u64 time_ns)
{
return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() - expire_jiffy);
}
/*
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
*/
static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
u64 passed = 0;
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
passed = ha_get_env(ha_mon, env, time_ns);
ha_set_invariant_jiffy(ha_mon, env, expire - passed);
return passed;
return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -463,14 +431,14 @@ static inline void ha_setup_timer(struct ha_monitor *ha_mon)
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
@@ -516,7 +484,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
int mode = HRTIMER_MODE_REL_HARD;
u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
if (RV_MON_TYPE == RV_MON_PER_CPU)
mode |= HRTIMER_MODE_PINNED;
@@ -525,7 +493,7 @@ static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
ha_start_timer_ns(ha_mon, ENV_MAX_STORED,
jiffies_to_nsecs(expire - passed), time_ns);
@@ -558,4 +526,25 @@ static inline bool ha_cancel_timer(struct ha_monitor *ha_mon)
static inline void ha_cancel_timer_sync(struct ha_monitor *ha_mon) { }
#endif
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#ifdef RV_MON_OPS_INIT
#undef RV_MON_OPS_INIT
#endif
#if RV_MON_TYPE == RV_MON_PER_TASK
#define RV_MON_OPS_INIT() { \
.rv_this = &rv_this, \
.is_per_task = true, \
.task_slot = &task_mon_slot, \
.task_reset = da_reset, \
}
#else
#define RV_MON_OPS_INIT() { \
.rv_this = &rv_this, \
.monitor_init = ha_monitor_init, \
.monitor_destroy = ha_monitor_destroy, \
}
#endif /* RV_MON_TYPE */
#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
#endif

73
include/rv/kunit.h Normal file
View File

@@ -0,0 +1,73 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
*
* Declaration of wrappers to allow mocking core functionality, like current,
* and other testing utilities.
* Necessary only when mocking may be needed. If the RV KUnit test is
* enabled, the wrappers incur an additional function call overhead.
*/
#ifndef _RV_KUNIT_H
#define _RV_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/test.h>
#include <kunit/test-bug.h>
#include <linux/delay.h>
int rv_set_testing(struct kunit_suite *suite);
void rv_clear_testing(struct kunit_suite *suite);
#define RV_KUNIT_MAX_MOCK_TASKS 8
struct rv_kunit_ctx {
int reactions, expected;
int mock_task_count;
struct task_struct *mock_tasks[RV_KUNIT_MAX_MOCK_TASKS];
};
#define RV_KUNIT_EXPECT_REACTION(test, ctx) \
do { \
KUNIT_EXPECT_EQ(test, ctx->reactions, ++ctx->expected); \
if (ctx->reactions != ctx->expected) \
ctx->expected = ctx->reactions; \
} while (0)
#define RV_KUNIT_EXPECT_NO_REACTION(test, ctx) \
do { \
KUNIT_EXPECT_EQ(test, ctx->reactions, ctx->expected); \
if (ctx->reactions != ctx->expected) \
ctx->expected = ctx->reactions; \
} while (0)
#define RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) \
for (int __done = ({ RV_KUNIT_EXPECT_NO_REACTION(test, ctx); 0; }); \
!__done; \
__done = ({ RV_KUNIT_EXPECT_REACTION(test, ctx); 1; }))
struct rv_kunit_mon {
struct rv_monitor *rv_this;
int (*monitor_init)(void);
void (*monitor_destroy)(void);
bool is_per_task;
int *task_slot;
void (*task_reset)(struct task_struct *task);
};
void prepare_test(struct kunit *test, const struct rv_kunit_mon *mon);
void teardown_test(void *arg);
struct task_struct *rv_kunit_alloc_mock_task(struct kunit *test);
void rv_mock_current(struct task_struct *tsk);
struct task_struct *rv_get_mock_current(void);
#define rv_get_current() (unlikely(kunit_get_current_test()) ? rv_get_mock_current() : current)
#else /* !CONFIG_RV_MONITORS_KUNIT_TEST */
#define rv_get_current() current
#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */
#endif /* _RV_KUNIT_H */

14
include/rv/ltl_monitor.h
View File

@@ -9,6 +9,7 @@
#include <linux/stringify.h>
#include <linux/seq_buf.h>
#include <rv/instrumentation.h>
#include <rv/kunit.h>
#include <trace/events/task.h>
#include <trace/events/sched.h>
@@ -16,8 +17,7 @@
#error "Please include $(MODEL_NAME).h generated by rvgen"
#endif
#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
static struct rv_monitor RV_MONITOR_NAME;
static struct rv_monitor rv_this;
static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
@@ -85,7 +85,7 @@ static void ltl_monitor_destroy(void)
static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)
{
CONCATENATE(trace_error_, MONITOR_NAME)(task);
rv_react(&RV_MONITOR_NAME, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n",
rv_react(&rv_this, "rv: "__stringify(MONITOR_NAME)": %s[%d]: violation detected\n",
task->comm, task->pid);
}
@@ -172,3 +172,11 @@ static void __maybe_unused ltl_atom_pulse(struct task_struct *task, enum ltl_ato
ltl_atom_set(mon, atom, !value);
ltl_validate(task, mon);
}
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#define RV_MON_OPS_INIT() { \
.rv_this = &rv_this, \
.is_per_task = true, \
.task_slot = &ltl_monitor_slot, \
}
#endif /* CONFIG_RV_MONITORS_KUNIT_TEST */

15
kernel/trace/rv/Kconfig
View File

@@ -76,6 +76,7 @@ source "kernel/trace/rv/monitors/opid/Kconfig"
source "kernel/trace/rv/monitors/rtapp/Kconfig"
source "kernel/trace/rv/monitors/pagefault/Kconfig"
source "kernel/trace/rv/monitors/sleep/Kconfig"
source "kernel/trace/rv/monitors/wakeup/Kconfig"
# Add new rtapp monitors here
source "kernel/trace/rv/monitors/stall/Kconfig"
@@ -111,3 +112,17 @@ config RV_REACT_PANIC
help
Enables the panic reactor. The panic reactor emits a printk()
message if an exception is found and panic()s the system.
config RV_MONITORS_KUNIT_TEST
tristate "KUnit tests for RV monitors" if !KUNIT_ALL_TESTS
depends on KUNIT && RV && RV_REACTORS
default KUNIT_ALL_TESTS
help
Enable KUnit tests for the RV (Runtime Verification) monitors.
These tests verify that monitors correctly detect violations by
triggering fake events and validating the expected reactions.
Enabling this may slightly increase overhead of some monitors if any
unrelated KUnit test is running.
If unsure, say N.

2
kernel/trace/rv/Makefile
View File

@@ -20,7 +20,9 @@ obj-$(CONFIG_RV_MON_OPID) += monitors/opid/opid.o
obj-$(CONFIG_RV_MON_STALL) += monitors/stall/stall.o
obj-$(CONFIG_RV_MON_DEADLINE) += monitors/deadline/deadline.o
obj-$(CONFIG_RV_MON_NOMISS) += monitors/nomiss/nomiss.o
obj-$(CONFIG_RV_MON_WAKEUP) += monitors/wakeup/wakeup.o
# Add new monitors here
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o
obj-$(CONFIG_RV_MONITORS_KUNIT_TEST) += rv_monitors_test.o

36
kernel/trace/rv/monitors/nomiss/nomiss.c
View File

@@ -57,24 +57,12 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == ready_nomiss)
return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
else if (curr_state == running_nomiss)
return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
return true;
}
static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
{
if (curr_state == next_state)
return;
if (curr_state == ready_nomiss)
ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
else if (curr_state == running_nomiss)
ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
}
static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
@@ -122,8 +110,6 @@ static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
return false;
ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
return false;
@@ -291,3 +277,21 @@ module_exit(unregister_nomiss);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("nomiss: dl entities run to completion before their deadline.");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "nomiss_kunit.h"
const struct rv_nomiss_ops rv_nomiss_ops = {
.mon = RV_MON_OPS_INIT(),
.deadline_thresh = &deadline_thresh,
.handle_dl_replenish = handle_dl_replenish,
.handle_dl_throttle = handle_dl_throttle,
.handle_dl_server_stop = handle_dl_server_stop,
.handle_sched_switch = handle_sched_switch,
.handle_sched_wakeup = handle_sched_wakeup,
.handle_sys_enter = handle_sys_enter,
.handle_newtask = handle_newtask,
};
EXPORT_SYMBOL_IF_KUNIT(rv_nomiss_ops);
#endif

38
kernel/trace/rv/monitors/nomiss/nomiss_kunit.c Normal file
View File

@@ -0,0 +1,38 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/sched.h>
#include "nomiss_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_NOMISS)
static void rv_test_nomiss(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct task_struct *other = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_nomiss_ops.mon);
target->pid = 99;
target->policy = SCHED_DEADLINE;
target->dl.runtime = 10000;
target->dl.dl_deadline = 20000;
rv_nomiss_ops.handle_newtask(NULL, target, 0);
/* Task gets preempted and can't terminate before deadline */
rv_nomiss_ops.handle_sched_switch(NULL, 0, other, target, TASK_RUNNING);
rv_nomiss_ops.handle_dl_replenish(NULL, &target->dl, 0, DL_TASK);
udelay(10);
rv_nomiss_ops.handle_sched_switch(NULL, 0, target, other, TASK_RUNNING);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) {
udelay(15 + div_u64(*rv_nomiss_ops.deadline_thresh, 1000));
rv_nomiss_ops.handle_sched_switch(NULL, 0, other, target, TASK_RUNNING);
}
}
#else
#define rv_test_nomiss rv_test_stub
#endif

35
kernel/trace/rv/monitors/nomiss/nomiss_kunit.h Normal file
View File

@@ -0,0 +1,35 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __NOMISS_KUNIT_H
#define __NOMISS_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_nomiss_ops {
struct rv_kunit_mon mon;
const u64 *deadline_thresh;
void (*handle_dl_replenish)(void *data, struct sched_dl_entity *dl_se,
int cpu, u8 type);
void (*handle_dl_throttle)(void *data, struct sched_dl_entity *dl_se,
int cpu, u8 type);
void (*handle_dl_server_stop)(void *data, struct sched_dl_entity *dl_se,
int cpu, u8 type);
void (*handle_sched_switch)(void *data, bool preempt,
struct task_struct *prev,
struct task_struct *next,
unsigned int prev_state);
void (*handle_sched_wakeup)(void *data, struct task_struct *tsk);
void (*handle_sys_enter)(void *data, struct pt_regs *regs, long id);
void (*handle_newtask)(void *data, struct task_struct *task, u64 flags);
} rv_nomiss_ops;
#endif
#endif /* __NOMISS_KUNIT_H */

12
kernel/trace/rv/monitors/opid/opid.c
View File

@@ -115,3 +115,15 @@ module_exit(unregister_opid);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("opid: operations with preemption and irq disabled.");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "opid_kunit.h"
const struct rv_opid_ops rv_opid_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_sched_need_resched = handle_sched_need_resched,
.handle_sched_waking = handle_sched_waking,
};
EXPORT_SYMBOL_IF_KUNIT(rv_opid_ops);
#endif

33
kernel/trace/rv/monitors/opid/opid_kunit.c Normal file
View File

@@ -0,0 +1,33 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/sched.h>
#include "opid_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_OPID)
static void rv_test_opid(struct kunit *test)
{
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_opid_ops.mon);
/* Ensure we keep the same per-cpu monitor */
guard(migrate)();
KUNIT_EXPECT_TRUE(test, preemptible());
/* Wakeup with preemption and interrupts enabled */
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_opid_ops.handle_sched_waking(NULL, NULL);
/* Need resched with interrupts enabled */
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) {
scoped_guard(preempt)
rv_opid_ops.handle_sched_need_resched(NULL, NULL, 0, TIF_NEED_RESCHED);
}
}
#else
#define rv_test_opid rv_test_stub
#endif

23
kernel/trace/rv/monitors/opid/opid_kunit.h Normal file
View File

@@ -0,0 +1,23 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __OPID_KUNIT_H
#define __OPID_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_opid_ops {
struct rv_kunit_mon mon;
void (*handle_sched_need_resched)(void *data, struct task_struct *tsk, int cpu, int tif);
void (*handle_sched_waking)(void *data, struct task_struct *p);
} rv_opid_ops;
#endif
#endif /* __OPID_KUNIT_H */

20
kernel/trace/rv/monitors/pagefault/pagefault.c
View File

@@ -38,7 +38,7 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
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);
ltl_atom_pulse(rv_get_current(), LTL_PAGEFAULT, true);
}
static int enable_pagefault(void)
@@ -63,7 +63,7 @@ static void disable_pagefault(void)
ltl_monitor_destroy();
}
static struct rv_monitor rv_pagefault = {
static struct rv_monitor rv_this = {
.name = "pagefault",
.description = "Monitor that RT tasks do not raise page faults",
.enable = enable_pagefault,
@@ -72,12 +72,12 @@ static struct rv_monitor rv_pagefault = {
static int __init register_pagefault(void)
{
return rv_register_monitor(&rv_pagefault, &rv_rtapp);
return rv_register_monitor(&rv_this, &rv_rtapp);
}
static void __exit unregister_pagefault(void)
{
rv_unregister_monitor(&rv_pagefault);
rv_unregister_monitor(&rv_this);
}
module_init(register_pagefault);
@@ -86,3 +86,15 @@ 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");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "pagefault_kunit.h"
const struct rv_pagefault_ops rv_pagefault_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_page_fault = handle_page_fault,
.handle_task_newtask = handle_task_newtask,
};
EXPORT_SYMBOL_IF_KUNIT(rv_pagefault_ops);
#endif

34
kernel/trace/rv/monitors/pagefault/pagefault_kunit.c Normal file
View File

@@ -0,0 +1,34 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <linux/sched/deadline.h>
#include <linux/sched/rt.h>
#include "pagefault_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_PAGEFAULT)
static void rv_test_pagefault(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_pagefault_ops.mon);
/* Initial pagefault when non-RT to start the model without failure */
target->policy = SCHED_NORMAL;
target->prio = MAX_RT_PRIO + 20;
rv_pagefault_ops.handle_task_newtask(NULL, target, 0);
rv_mock_current(target);
rv_pagefault_ops.handle_page_fault(NULL, 0, NULL, 0);
/* RT task has a page fault */
target->policy = SCHED_FIFO;
target->prio = MAX_RT_PRIO - 1;
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_pagefault_ops.handle_page_fault(NULL, 0, NULL, 0);
}
#else
#define rv_test_pagefault rv_test_stub
#endif

24
kernel/trace/rv/monitors/pagefault/pagefault_kunit.h Normal file
View File

@@ -0,0 +1,24 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __PAGEFAULT_KUNIT_H
#define __PAGEFAULT_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_pagefault_ops {
struct rv_kunit_mon mon;
void (*handle_page_fault)(void *data, unsigned long address, struct pt_regs *regs,
unsigned long error_code);
void (*handle_task_newtask)(void *data, struct task_struct *task, u64 flags);
} rv_pagefault_ops;
#endif
#endif /* __PAGEFAULT_KUNIT_H */

2
kernel/trace/rv/monitors/rtapp/Kconfig
View File

@@ -1,6 +1,6 @@
config RV_MON_RTAPP
depends on RV
depends on RV_PER_TASK_MONITORS >= 2
depends on RV_PER_TASK_MONITORS >= 3
bool "rtapp monitor"
help
Collection of monitors to check for common problems with real-time

13
kernel/trace/rv/monitors/sco/sco.c
View File

@@ -83,3 +83,16 @@ module_exit(unregister_sco);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("sco: scheduling context operations.");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "sco_kunit.h"
const struct rv_sco_ops rv_sco_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_sched_set_state = handle_sched_set_state,
.handle_schedule_entry = handle_schedule_entry,
.handle_schedule_exit = handle_schedule_exit,
};
EXPORT_SYMBOL_IF_KUNIT(rv_sco_ops);
#endif

29
kernel/trace/rv/monitors/sco/sco_kunit.c Normal file
View File

@@ -0,0 +1,29 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/sched.h>
#include "sco_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_SCO)
static void rv_test_sco(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_sco_ops.mon);
/* Ensure we keep the same per-cpu monitor */
guard(migrate)();
/* Set state while scheduling */
rv_sco_ops.handle_sched_set_state(NULL, target, TASK_INTERRUPTIBLE);
rv_sco_ops.handle_schedule_entry(NULL, false);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sco_ops.handle_sched_set_state(NULL, target, TASK_INTERRUPTIBLE);
}
#else
#define rv_test_sco rv_test_stub
#endif

24
kernel/trace/rv/monitors/sco/sco_kunit.h Normal file
View File

@@ -0,0 +1,24 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __SCO_KUNIT_H
#define __SCO_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_sco_ops {
struct rv_kunit_mon mon;
void (*handle_sched_set_state)(void *data, struct task_struct *tsk, int state);
void (*handle_schedule_entry)(void *data, bool preempt);
void (*handle_schedule_exit)(void *data, bool is_switch);
} rv_sco_ops;
#endif
#endif /* __SCO_KUNIT_H */

1
kernel/trace/rv/monitors/sleep/Kconfig
View File

@@ -5,7 +5,6 @@ config RV_MON_SLEEP
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"

107
kernel/trace/rv/monitors/sleep/sleep.c
View File

@@ -36,16 +36,14 @@ 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)
{
ltl_atom_set(mon, LTL_SLEEP, false);
ltl_atom_set(mon, LTL_WAKE, false);
ltl_atom_set(mon, LTL_SCHEDULE_IN, 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_CLOCK_REALTIME, 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);
@@ -54,34 +52,7 @@ static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bo
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);
ltl_atom_set(mon, LTL_EPOLL_WAIT, 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);
}
ltl_atom_set(mon, LTL_USER_THREAD, !(task->flags & PF_KTHREAD));
}
static void handle_sched_set_state(void *data, struct task_struct *task, int state)
@@ -92,17 +63,17 @@ static void handle_sched_set_state(void *data, struct task_struct *task, int sta
ltl_atom_pulse(task, LTL_ABORT_SLEEP, true);
}
static void handle_sched_wakeup(void *data, struct task_struct *task)
static void handle_sched_exit(void *data, bool is_switch)
{
ltl_atom_pulse(task, LTL_WAKE, true);
ltl_atom_pulse(rv_get_current(), LTL_SCHEDULE_IN, true);
}
static void handle_sched_waking(void *data, struct task_struct *task)
{
if (this_cpu_read(hardirq_context)) {
if (in_hardirq()) {
ltl_atom_pulse(task, LTL_WOKEN_BY_HARDIRQ, true);
} else if (in_task()) {
if (current->prio <= task->prio)
if (rv_get_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);
@@ -112,12 +83,12 @@ static void handle_sched_waking(void *data, struct task_struct *task)
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);
ltl_atom_update(rv_get_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);
ltl_atom_update(rv_get_current(), LTL_BLOCK_ON_RT_MUTEX, false);
}
static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
@@ -126,7 +97,7 @@ static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
unsigned long args[6];
int op, cmd;
mon = ltl_get_monitor(current);
mon = ltl_get_monitor(rv_get_current());
switch (id) {
#ifdef __NR_clock_nanosleep
@@ -135,11 +106,10 @@ static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
#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);
syscall_get_arguments(rv_get_current(), regs, args);
ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, args[0] == CLOCK_REALTIME);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, args[1] == TIMER_ABSTIME);
ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, true);
ltl_atom_update(rv_get_current(), LTL_CLOCK_NANOSLEEP, true);
break;
#ifdef __NR_futex
@@ -148,25 +118,25 @@ static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
#ifdef __NR_futex_time64
case __NR_futex_time64:
#endif
syscall_get_arguments(current, regs, args);
syscall_get_arguments(rv_get_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);
ltl_atom_update(rv_get_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);
ltl_atom_update(rv_get_current(), LTL_FUTEX_WAIT, true);
break;
}
break;
#ifdef __NR_epoll_wait
case __NR_epoll_wait:
ltl_atom_update(current, LTL_EPOLL_WAIT, true);
ltl_atom_update(rv_get_current(), LTL_EPOLL_WAIT, true);
break;
#endif
}
@@ -174,21 +144,14 @@ static void handle_sys_enter(void *data, struct pt_regs *regs, long id)
static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
{
struct ltl_monitor *mon = ltl_get_monitor(current);
struct ltl_monitor *mon = ltl_get_monitor(rv_get_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_CLOCK_REALTIME, false);
ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false);
ltl_atom_set(mon, LTL_EPOLL_WAIT, 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);
ltl_atom_update(rv_get_current(), LTL_CLOCK_NANOSLEEP, false);
}
static int enable_sleep(void)
@@ -200,11 +163,10 @@ static int enable_sleep(void)
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_exit_tp, handle_sched_exit);
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;
@@ -213,18 +175,17 @@ static int enable_sleep(void)
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_exit_tp, handle_sched_exit);
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 = {
static struct rv_monitor rv_this = {
.name = "sleep",
.description = "Monitor that RT tasks do not undesirably sleep",
.enable = enable_sleep,
@@ -233,12 +194,12 @@ static struct rv_monitor rv_sleep = {
static int __init register_sleep(void)
{
return rv_register_monitor(&rv_sleep, &rv_rtapp);
return rv_register_monitor(&rv_this, &rv_rtapp);
}
static void __exit unregister_sleep(void)
{
rv_unregister_monitor(&rv_sleep);
rv_unregister_monitor(&rv_this);
}
module_init(register_sleep);
@@ -247,3 +208,21 @@ 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");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "sleep_kunit.h"
const struct rv_sleep_ops rv_sleep_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_sched_waking = handle_sched_waking,
.handle_sched_exit = handle_sched_exit,
.handle_sched_set_state = handle_sched_set_state,
.handle_contention_begin = handle_contention_begin,
.handle_contention_end = handle_contention_end,
.handle_sys_enter = handle_sys_enter,
.handle_sys_exit = handle_sys_exit,
.handle_task_newtask = handle_task_newtask,
};
EXPORT_SYMBOL_IF_KUNIT(rv_sleep_ops);
#endif

142
kernel/trace/rv/monitors/sleep/sleep.h
View File

@@ -18,16 +18,12 @@ enum ltl_atom {
LTL_EPOLL_WAIT,
LTL_FUTEX_LOCK_PI,
LTL_FUTEX_WAIT,
LTL_KERNEL_THREAD,
LTL_KTHREAD_SHOULD_STOP,
LTL_NANOSLEEP_CLOCK_MONOTONIC,
LTL_NANOSLEEP_CLOCK_TAI,
LTL_NANOSLEEP_CLOCK_REALTIME,
LTL_NANOSLEEP_TIMER_ABSTIME,
LTL_RT,
LTL_SCHEDULE_IN,
LTL_SLEEP,
LTL_TASK_IS_MIGRATION,
LTL_TASK_IS_RCU,
LTL_WAKE,
LTL_USER_THREAD,
LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
LTL_WOKEN_BY_HARDIRQ,
LTL_WOKEN_BY_NMI,
@@ -44,16 +40,12 @@ static const char *ltl_atom_str(enum ltl_atom atom)
"ep_wa",
"fu_lo_pi",
"fu_wa",
"ker_th",
"kth_sh_st",
"na_cl_mo",
"na_cl_ta",
"na_cl_re",
"na_ti_ab",
"rt",
"sl",
"ta_mi",
"ta_rc",
"wak",
"sch_in",
"sle",
"us_th",
"wo_eq_hi_pr",
"wo_ha",
"wo_nm",
@@ -81,47 +73,41 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
bool wake = test_bit(LTL_WAKE, mon->atoms);
bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, 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 kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
bool val42 = task_is_rcu || task_is_migration;
bool val43 = futex_lock_pi || val42;
bool val5 = block_on_rt_mutex || val43;
bool val34 = abort_sleep || kthread_should_stop;
bool val35 = woken_by_nmi || val34;
bool val36 = woken_by_hardirq || val35;
bool val14 = woken_by_equal_or_higher_prio || val36;
bool val13 = !wake;
bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
bool val27 = nanosleep_timer_abstime && val26;
bool val18 = clock_nanosleep && val27;
bool val7 = block_on_rt_mutex || futex_lock_pi;
bool val32 = woken_by_nmi || abort_sleep;
bool val33 = woken_by_hardirq || val32;
bool val14 = woken_by_equal_or_higher_prio || val33;
bool val13 = !schedule_in;
bool val25 = !nanosleep_clock_realtime;
bool val26 = nanosleep_timer_abstime && val25;
bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
bool val9 = futex_wait || val20;
bool val11 = val9 || kernel_thread;
bool val11 = futex_wait || val20;
bool val3 = !user_thread;
bool val2 = !sleep;
bool val4 = val2 || val3;
bool val1 = !rt;
bool val3 = val1 || val2;
bool val5 = val1 || val4;
if (val3)
if (val5)
__set_bit(S0, mon->states);
if (val11 && val13)
__set_bit(S1, mon->states);
if (val11 && val14)
__set_bit(S4, mon->states);
if (val5)
if (val7)
__set_bit(S5, mon->states);
}
@@ -132,131 +118,125 @@ ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned l
bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
mon->atoms);
bool wake = test_bit(LTL_WAKE, mon->atoms);
bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool sleep = test_bit(LTL_SLEEP, mon->atoms);
bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, 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 kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
bool val42 = task_is_rcu || task_is_migration;
bool val43 = futex_lock_pi || val42;
bool val5 = block_on_rt_mutex || val43;
bool val34 = abort_sleep || kthread_should_stop;
bool val35 = woken_by_nmi || val34;
bool val36 = woken_by_hardirq || val35;
bool val14 = woken_by_equal_or_higher_prio || val36;
bool val13 = !wake;
bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai;
bool val27 = nanosleep_timer_abstime && val26;
bool val18 = clock_nanosleep && val27;
bool val7 = block_on_rt_mutex || futex_lock_pi;
bool val32 = woken_by_nmi || abort_sleep;
bool val33 = woken_by_hardirq || val32;
bool val14 = woken_by_equal_or_higher_prio || val33;
bool val13 = !schedule_in;
bool val25 = !nanosleep_clock_realtime;
bool val26 = nanosleep_timer_abstime && val25;
bool val18 = clock_nanosleep && val26;
bool val20 = val18 || epoll_wait;
bool val9 = futex_wait || val20;
bool val11 = val9 || kernel_thread;
bool val11 = futex_wait || val20;
bool val3 = !user_thread;
bool val2 = !sleep;
bool val4 = val2 || val3;
bool val1 = !rt;
bool val3 = val1 || val2;
bool val5 = val1 || val4;
switch (state) {
case S0:
if (val3)
if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
if (val5)
if (val7)
__set_bit(S5, next);
break;
case S1:
if (val11 && val13)
__set_bit(S1, next);
if (val13 && val3)
if (val13 && val5)
__set_bit(S2, next);
if (val14 && val3)
if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
if (val13 && val5)
if (val13 && val7)
__set_bit(S6, next);
if (val14 && val5)
if (val14 && val7)
__set_bit(S7, next);
break;
case S2:
if (val11 && val13)
__set_bit(S1, next);
if (val13 && val3)
if (val13 && val5)
__set_bit(S2, next);
if (val14 && val3)
if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
if (val13 && val5)
if (val13 && val7)
__set_bit(S6, next);
if (val14 && val5)
if (val14 && val7)
__set_bit(S7, next);
break;
case S3:
if (val3)
if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
if (val5)
if (val7)
__set_bit(S5, next);
break;
case S4:
if (val3)
if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
if (val5)
if (val7)
__set_bit(S5, next);
break;
case S5:
if (val3)
if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
if (val5)
if (val7)
__set_bit(S5, next);
break;
case S6:
if (val11 && val13)
__set_bit(S1, next);
if (val13 && val3)
if (val13 && val5)
__set_bit(S2, next);
if (val14 && val3)
if (val14 && val5)
__set_bit(S3, next);
if (val11 && val14)
__set_bit(S4, next);
if (val13 && val5)
if (val13 && val7)
__set_bit(S6, next);
if (val14 && val5)
if (val14 && val7)
__set_bit(S7, next);
break;
case S7:
if (val3)
if (val5)
__set_bit(S0, next);
if (val11 && val13)
__set_bit(S1, next);
if (val11 && val14)
__set_bit(S4, next);
if (val5)
if (val7)
__set_bit(S5, next);
break;
}

59
kernel/trace/rv/monitors/sleep/sleep_kunit.c Normal file
View File

@@ -0,0 +1,59 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/syscalls.h>
#include <trace/events/sched.h>
#include <uapi/linux/futex.h>
#include "sleep_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_SLEEP)
static void rv_test_sleep(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct task_struct *other = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
unsigned long args[6] = {0};
struct pt_regs regs = {0};
prepare_test(test, &rv_sleep_ops.mon);
target->policy = SCHED_FIFO;
target->prio = MAX_RT_PRIO - 2;
other->policy = SCHED_FIFO;
other->prio = MAX_RT_PRIO - 1;
rv_sleep_ops.handle_task_newtask(NULL, target, 0);
/* RT task sleeps on a non RT-friendly nanosleep */
rv_mock_current(target);
args[0] = CLOCK_REALTIME;
syscall_set_arguments(target, &regs, args);
#ifdef __NR_clock_nanosleep
rv_sleep_ops.handle_sys_enter(NULL, &regs, __NR_clock_nanosleep);
#elif defined(__NR_clock_nanosleep_time64)
rv_sleep_ops.handle_sys_enter(NULL, &regs, __NR_clock_nanosleep_time64);
#endif
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sleep_ops.handle_sched_set_state(NULL, target, TASK_INTERRUPTIBLE);
rv_sleep_ops.handle_sys_exit(NULL, NULL, 0);
/* RT task woken up by lower priority task */
args[1] = FUTEX_WAIT;
syscall_set_arguments(target, &regs, args);
rv_mock_current(target);
#ifdef __NR_futex
rv_sleep_ops.handle_sys_enter(NULL, &regs, __NR_futex);
#elif defined(__NR_futex_time64)
rv_sleep_ops.handle_sys_enter(NULL, &regs, __NR_futex_time64);
#endif
rv_sleep_ops.handle_sched_set_state(NULL, target, TASK_INTERRUPTIBLE);
rv_mock_current(other);
rv_sleep_ops.handle_sched_waking(NULL, target);
rv_mock_current(target);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sleep_ops.handle_sched_exit(NULL, true);
}
#else
#define rv_test_sleep rv_test_stub
#endif

29
kernel/trace/rv/monitors/sleep/sleep_kunit.h Normal file
View File

@@ -0,0 +1,29 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __SLEEP_KUNIT_H
#define __SLEEP_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_sleep_ops {
struct rv_kunit_mon mon;
void (*handle_sched_waking)(void *data, struct task_struct *task);
void (*handle_sched_exit)(void *data, bool is_switch);
void (*handle_sched_set_state)(void *data, struct task_struct *task, int state);
void (*handle_contention_begin)(void *data, void *lock, unsigned int flags);
void (*handle_contention_end)(void *data, void *lock, int ret);
void (*handle_sys_enter)(void *data, struct pt_regs *regs, long id);
void (*handle_sys_exit)(void *data, struct pt_regs *regs, long ret);
void (*handle_task_newtask)(void *data, struct task_struct *task, u64 flags);
} rv_sleep_ops;
#endif
#endif /* __SLEEP_KUNIT_H */

14
kernel/trace/rv/monitors/sssw/sssw.c
View File

@@ -112,3 +112,17 @@ module_exit(unregister_sssw);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("sssw: set state sleep and wakeup.");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "sssw_kunit.h"
const struct rv_sssw_ops rv_sssw_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_sched_set_state = handle_sched_set_state,
.handle_sched_switch = handle_sched_switch,
.handle_sched_wakeup = handle_sched_wakeup,
.handle_signal_deliver = handle_signal_deliver,
};
EXPORT_SYMBOL_IF_KUNIT(rv_sssw_ops);
#endif

33
kernel/trace/rv/monitors/sssw/sssw_kunit.c Normal file
View File

@@ -0,0 +1,33 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/sched.h>
#include "sssw_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_SSSW)
static void rv_test_sssw(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct task_struct *other = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_sssw_ops.mon);
/* Suspend without setting to sleepable */
rv_sssw_ops.handle_sched_set_state(NULL, target, TASK_RUNNING);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sssw_ops.handle_sched_switch(NULL, 0, target, other, TASK_INTERRUPTIBLE);
/* Switch in after suspension without wakeup */
rv_sssw_ops.handle_sched_wakeup(NULL, target);
rv_sssw_ops.handle_sched_set_state(NULL, target, TASK_INTERRUPTIBLE);
rv_sssw_ops.handle_sched_switch(NULL, 0, target, other, TASK_INTERRUPTIBLE);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sssw_ops.handle_sched_switch(NULL, 0, other, target, TASK_RUNNING);
}
#else
#define rv_test_sssw rv_test_stub
#endif

30
kernel/trace/rv/monitors/sssw/sssw_kunit.h Normal file
View File

@@ -0,0 +1,30 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __SSSW_KUNIT_H
#define __SSSW_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_sssw_ops {
struct rv_kunit_mon mon;
void (*handle_sched_set_state)(void *data, struct task_struct *tsk, int state);
void (*handle_sched_switch)(void *data, bool preempt,
struct task_struct *prev,
struct task_struct *next,
unsigned int prev_state);
void (*handle_sched_wakeup)(void *data, struct task_struct *p);
void (*handle_signal_deliver)(void *data, int sig,
struct kernel_siginfo *info,
struct k_sigaction *ka);
} rv_sssw_ops;
#endif
#endif /* __SSSW_KUNIT_H */

2
kernel/trace/rv/monitors/stall/stall.c
View File

@@ -38,7 +38,7 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == enqueued_stall)
return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns);
return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns, threshold_jiffies);
return true;
}

19
kernel/trace/rv/monitors/sts/sts.c
View File

@@ -152,3 +152,22 @@ module_exit(unregister_sts);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("sts: schedule implies task switch.");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "sts_kunit.h"
const struct rv_sts_ops rv_sts_ops = {
.mon = RV_MON_OPS_INIT(),
#ifdef CONFIG_X86_LOCAL_APIC
.handle_vector_irq_entry = handle_vector_irq_entry,
#endif
.handle_irq_disable = handle_irq_disable,
.handle_irq_enable = handle_irq_enable,
.handle_irq_entry = handle_irq_entry,
.handle_sched_switch = handle_sched_switch,
.handle_schedule_entry = handle_schedule_entry,
.handle_schedule_exit = handle_schedule_exit,
};
EXPORT_SYMBOL_IF_KUNIT(rv_sts_ops);
#endif

39
kernel/trace/rv/monitors/sts/sts_kunit.c Normal file
View File

@@ -0,0 +1,39 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
#include <trace/events/sched.h>
#include "sts_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_STS)
static void rv_test_sts(struct kunit *test)
{
struct task_struct *target = rv_kunit_alloc_mock_task(test);
struct task_struct *other = rv_kunit_alloc_mock_task(test);
struct rv_kunit_ctx *ctx = test->priv;
prepare_test(test, &rv_sts_ops.mon);
/* Per-CPU monitor, make sure we don't change CPU mid-test */
guard(migrate)();
/* Switch without disabling interrupts */
rv_sts_ops.handle_schedule_exit(NULL, false);
rv_sts_ops.handle_schedule_entry(NULL, false);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sts_ops.handle_sched_switch(NULL, 0, target, other, TASK_RUNNING);
rv_sts_ops.handle_schedule_exit(NULL, false);
/* Schedule from interrupt context */
rv_sts_ops.handle_schedule_entry(NULL, false);
rv_sts_ops.handle_irq_disable(NULL, 0, 0);
rv_sts_ops.handle_irq_entry(NULL, 0, NULL);
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_sts_ops.handle_sched_switch(NULL, 0, target, other, TASK_RUNNING);
rv_sts_ops.handle_irq_enable(NULL, 0, 0);
}
#else
#define rv_test_sts rv_test_stub
#endif

33
kernel/trace/rv/monitors/sts/sts_kunit.h Normal file
View File

@@ -0,0 +1,33 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __STS_KUNIT_H
#define __STS_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_sts_ops {
struct rv_kunit_mon mon;
#ifdef CONFIG_X86_LOCAL_APIC
void (*handle_vector_irq_entry)(void *data, int vector);
#endif
void (*handle_irq_disable)(void *data, unsigned long ip, unsigned long parent_ip);
void (*handle_irq_enable)(void *data, unsigned long ip, unsigned long parent_ip);
void (*handle_irq_entry)(void *data, int irq, struct irqaction *action);
void (*handle_sched_switch)(void *data, bool preempt,
struct task_struct *prev,
struct task_struct *next,
unsigned int prev_state);
void (*handle_schedule_entry)(void *data, bool preempt);
void (*handle_schedule_exit)(void *data, bool is_switch);
} rv_sts_ops;
#endif
#endif /* __STS_KUNIT_H */

16
kernel/trace/rv/monitors/wakeup/Kconfig Normal file
View File

@@ -0,0 +1,16 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_WAKEUP
depends on RV
depends on RV_MON_RTAPP
depends on HAVE_SYSCALL_TRACEPOINTS
default y
select LTL_MON_EVENTS_ID
bool "wakeup monitor"
help
This monitor detects a lower-priority task waking up a
higher-priority task. The RV_MON_SLEEP monitor already
detects this case, but this monitor detects in the context
of the waker task instead. This and RV_MON_SLEEP can be
enabled together to get the stacktrace of both the waker
task and the wakee task.

153
kernel/trace/rv/monitors/wakeup/wakeup.c Normal file
View File

@@ -0,0 +1,153 @@
// 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 "wakeup"
#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>
#ifndef __NR_futex
#define __NR_futex (-__COUNTER__)
#endif
#ifndef __NR_futex_time64
#define __NR_futex_time64 (-__COUNTER__)
#endif
#include "wakeup.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_WOKEN_BY_LOWER_PRIO, false);
ltl_atom_set(mon, LTL_WOKEN_BY_SOFTIRQ, false);
if (task_creation) {
ltl_atom_set(mon, LTL_BLOCK_ON_RT_MUTEX, false);
ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false);
}
ltl_atom_set(mon, LTL_USER_THREAD, !(task->flags & PF_KTHREAD));
}
static void handle_sched_waking(void *data, struct task_struct *task)
{
if (in_task()) {
if (current->prio > task->prio)
ltl_atom_pulse(task, LTL_WOKEN_BY_LOWER_PRIO, true);
} else if (in_serving_softirq()) {
ltl_atom_pulse(task, LTL_WOKEN_BY_SOFTIRQ, 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)
{
unsigned long args[6];
int op, cmd;
switch (id) {
case __NR_futex:
case __NR_futex_time64:
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;
}
break;
}
}
static void handle_sys_exit(void *data, struct pt_regs *regs, long ret)
{
ltl_atom_update(current, LTL_FUTEX_LOCK_PI, false);
}
static int enable_wakeup(void)
{
int retval;
retval = ltl_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("rtapp_wakeup", sched_waking, handle_sched_waking);
rv_attach_trace_probe("rtapp_wakeup", contention_begin, handle_contention_begin);
rv_attach_trace_probe("rtapp_wakeup", contention_end, handle_contention_end);
rv_attach_trace_probe("rtapp_wakeup", sys_enter, handle_sys_enter);
rv_attach_trace_probe("rtapp_wakeup", sys_exit, handle_sys_exit);
return 0;
}
static void disable_wakeup(void)
{
rv_detach_trace_probe("rtapp_wakeup", sched_waking, handle_sched_waking);
rv_detach_trace_probe("rtapp_wakeup", contention_begin, handle_contention_begin);
rv_detach_trace_probe("rtapp_wakeup", contention_end, handle_contention_end);
rv_detach_trace_probe("rtapp_wakeup", sys_enter, handle_sys_enter);
rv_detach_trace_probe("rtapp_wakeup", sys_exit, handle_sys_exit);
ltl_monitor_destroy();
}
static struct rv_monitor rv_wakeup = {
.name = "wakeup",
.description = "Monitor that real-time tasks are not woken by lower-priority tasks",
.enable = enable_wakeup,
.disable = disable_wakeup,
};
static int __init register_wakeup(void)
{
return rv_register_monitor(&rv_wakeup, &rv_rtapp);
}
static void __exit unregister_wakeup(void)
{
rv_unregister_monitor(&rv_wakeup);
}
module_init(register_wakeup);
module_exit(unregister_wakeup);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("Nam Cao <namcao@linutronix.de>");
MODULE_DESCRIPTION("Monitor that real-time tasks are not woken by lower-priority tasks");

92
kernel/trace/rv/monitors/wakeup/wakeup.h Normal file
View File

@@ -0,0 +1,92 @@
/* 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 wakeup
enum ltl_atom {
LTL_BLOCK_ON_RT_MUTEX,
LTL_FUTEX_LOCK_PI,
LTL_RT,
LTL_USER_THREAD,
LTL_WOKEN_BY_LOWER_PRIO,
LTL_WOKEN_BY_SOFTIRQ,
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[] = {
"bl_on_rt_mu",
"fu_lo_pi",
"rt",
"us_th",
"wo_lo_pr",
"wo_so",
};
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 woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool val9 = block_on_rt_mutex || futex_lock_pi;
bool val6 = !woken_by_softirq;
bool val5 = !woken_by_lower_prio;
bool val8 = val5 && val6;
bool val10 = val8 || val9;
bool val3 = !user_thread;
bool val2 = !rt;
bool val4 = val2 || val3;
bool val11 = val4 || val10;
if (val11)
__set_bit(S0, mon->states);
}
static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
bool woken_by_softirq = test_bit(LTL_WOKEN_BY_SOFTIRQ, mon->atoms);
bool woken_by_lower_prio = test_bit(LTL_WOKEN_BY_LOWER_PRIO, mon->atoms);
bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
bool rt = test_bit(LTL_RT, mon->atoms);
bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
bool val9 = block_on_rt_mutex || futex_lock_pi;
bool val6 = !woken_by_softirq;
bool val5 = !woken_by_lower_prio;
bool val8 = val5 && val6;
bool val10 = val8 || val9;
bool val3 = !user_thread;
bool val2 = !rt;
bool val4 = val2 || val3;
bool val11 = val4 || val10;
switch (state) {
case S0:
if (val11)
__set_bit(S0, next);
break;
}
}

14
kernel/trace/rv/monitors/wakeup/wakeup_trace.h Normal file
View File

@@ -0,0 +1,14 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_WAKEUP
DEFINE_EVENT(event_ltl_monitor_id, event_wakeup,
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_wakeup,
TP_PROTO(struct task_struct *task),
TP_ARGS(task));
#endif /* CONFIG_RV_MON_WAKEUP */

86
kernel/trace/rv/rv.c
View File

@@ -164,7 +164,6 @@ struct dentry *get_monitors_root(void)
*/
LIST_HEAD(rv_monitors_list);
static int task_monitor_count;
static bool task_monitor_slots[CONFIG_RV_PER_TASK_MONITORS];
int rv_get_task_monitor_slot(void)
@@ -173,22 +172,16 @@ int rv_get_task_monitor_slot(void)
lockdep_assert_held(&rv_interface_lock);
if (task_monitor_count == CONFIG_RV_PER_TASK_MONITORS)
return -EBUSY;
task_monitor_count++;
for (i = 0; i < CONFIG_RV_PER_TASK_MONITORS; i++) {
if (task_monitor_slots[i] == false) {
if (!task_monitor_slots[i]) {
task_monitor_slots[i] = true;
return i;
}
}
WARN_ONCE(1, "RV task_monitor_count and slots are out of sync\n");
return -EINVAL;
return -EBUSY;
}
EXPORT_SYMBOL_GPL(rv_get_task_monitor_slot);
void rv_put_task_monitor_slot(int slot)
{
@@ -199,12 +192,13 @@ void rv_put_task_monitor_slot(int slot)
return;
}
WARN_ONCE(!task_monitor_slots[slot], "RV releasing unused task_monitor_slots: %d\n",
slot);
if (WARN_ONCE(!task_monitor_slots[slot],
"RV releasing unused task monitor slot: %d\n", slot))
return;
task_monitor_count--;
task_monitor_slots[slot] = false;
}
EXPORT_SYMBOL_GPL(rv_put_task_monitor_slot);
/*
* Monitors with a parent are nested,
@@ -852,3 +846,69 @@ int __init rv_init_interface(void)
return 0;
}
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <rv/kunit.h>
#include <kunit/visibility.h>
/*
* rv_set_testing - ensure mutual exclusion between KUnit tests and real monitors
*
* KUnit tests for RV monitors rely on stubs that are incompatible with
* the execution of real monitors. Ensure mutual exclusion by acquiring
* the rv_interface_lock for the duration of the suite.
*
* Returns 0 on success, -EBUSY if any real monitor is already enabled.
*/
int rv_set_testing(struct kunit_suite *suite)
{
struct rv_monitor *mon;
mutex_lock(&rv_interface_lock);
list_for_each_entry(mon, &rv_monitors_list, list) {
if (mon->enabled) {
mutex_unlock(&rv_interface_lock);
return -EBUSY;
}
}
return 0;
}
EXPORT_SYMBOL_IF_KUNIT(rv_set_testing);
/*
* rv_clear_testing - allow real monitors to run again after KUnit tests
*/
void rv_clear_testing(struct kunit_suite *suite)
{
mutex_unlock(&rv_interface_lock);
}
EXPORT_SYMBOL_IF_KUNIT(rv_clear_testing);
/*
* rv_get_mock_current() is called only if we are running from a KUnit test.
* This can occur from a legitimate RV test or any unrelated test running when
* a real RV monitor is active and triggering events.
* We assume the former case is the only one where mock_current is not NULL and
* can occur only sequentially (KUnit doesn't run tests in parallel).
* We cannot rely on the test's context because there is no way to safely
* understand from which test we are running and KUnit utilities require
* locking, which is unsafe from NMI or scheduling context.
* Note that it is not possible for a real RV monitor to run when the RV KUnit
* tests are running (see rv_set_testing()).
*/
static struct task_struct *mock_current;
void rv_mock_current(struct task_struct *tsk)
{
mock_current = tsk;
}
EXPORT_SYMBOL_IF_KUNIT(rv_mock_current);
struct task_struct *rv_get_mock_current(void)
{
return mock_current ?: current;
}
EXPORT_SYMBOL_GPL(rv_get_mock_current);
#endif

182
kernel/trace/rv/rv_monitors_test.c Normal file
View File

@@ -0,0 +1,182 @@
// SPDX-License-Identifier: GPL-2.0
/*
* Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
*
* RV monitor kunit tests:
* Tests the RV monitors by triggering fake events to verify monitor
* behavior and reactions. Tests start from the first defined event and
* trigger events in order to verify error detection.
*/
#include <rv/kunit.h>
#include <kunit/test-bug.h>
#include <linux/kernel.h>
#include <linux/rv.h>
#include "rv.h"
/*
* An easy way to pass the context is to use kunit_get_current_test()->priv,
* but this doesn't always work (e.g. a reactor running from another context
* like softirq). Store the current value here whenever a test is running.
*/
static struct rv_kunit_ctx *active_ctx;
__printf(1, 0)
static void rv_kunit_mock_react(const char *msg, va_list args)
{
if (active_ctx)
++active_ctx->reactions;
}
/*
* teardown_test - Disable the monitor for a kunit test
*
* Since per-task monitors are special, make sure we reset all the ones we
* started manually here, if required.
*/
void teardown_test(void *arg)
{
const struct rv_kunit_mon *mon = arg;
struct kunit *test = kunit_get_current_test();
if (test) {
struct rv_kunit_ctx *ctx = test->priv;
RV_KUNIT_EXPECT_NO_REACTION(test, ctx);
if (mon->is_per_task && mon->task_reset) {
for (int i = 0; i < ctx->mock_task_count; i++)
mon->task_reset(ctx->mock_tasks[i]);
synchronize_rcu();
}
}
mon->rv_this->enabled = 0;
if (mon->rv_this->reactor)
mon->rv_this->react = mon->rv_this->reactor->react;
else
mon->rv_this->react = NULL;
active_ctx = NULL;
rv_mock_current(NULL);
if (mon->is_per_task)
*mon->task_slot = RV_PER_TASK_MONITOR_INIT;
else
mon->monitor_destroy();
}
/*
* prepare_test - Enable the monitor for a kunit test
*
* Do the bare minimum to set up the monitor, per-task monitors are special as
* "real" initialisation/destruction iterates over real tasks, and may register
* handlers. All we need is to select the right slot in the task_struct.
*/
void prepare_test(struct kunit *test, const struct rv_kunit_mon *mon)
{
KUNIT_ASSERT_FALSE(test, mon->rv_this->enabled);
active_ctx = test->priv;
mon->rv_this->react = rv_kunit_mock_react;
if (mon->is_per_task)
*mon->task_slot = 0;
else
KUNIT_ASSERT_EQ(test, mon->monitor_init(), 0);
mon->rv_this->enabled = 1;
KUNIT_ASSERT_EQ(test, 0,
kunit_add_action_or_reset(test, teardown_test, (void *)mon));
}
struct task_struct *rv_kunit_alloc_mock_task(struct kunit *test)
{
struct rv_kunit_ctx *ctx = test->priv;
struct task_struct *tsk;
KUNIT_ASSERT_LT(test, ctx->mock_task_count, RV_KUNIT_MAX_MOCK_TASKS);
tsk = kunit_kzalloc(test, sizeof(struct task_struct), GFP_KERNEL);
KUNIT_ASSERT_NOT_NULL(test, tsk);
if (!IS_ENABLED(CONFIG_THREAD_INFO_IN_TASK)) {
tsk->stack = kunit_kzalloc(test, sizeof(struct thread_info), GFP_KERNEL);
KUNIT_ASSERT_NOT_NULL(test, tsk->stack);
}
ctx->mock_tasks[ctx->mock_task_count++] = tsk;
return tsk;
}
static int rv_mon_test_init(struct kunit *test)
{
struct rv_kunit_ctx *ctx;
ctx = kunit_kzalloc(test, sizeof(*ctx), GFP_KERNEL);
KUNIT_ASSERT_NOT_ERR_OR_NULL(test, ctx);
test->priv = ctx;
return 0;
}
static void __maybe_unused rv_test_stub(struct kunit *test)
{
kunit_skip(test, "Monitor not enabled\n");
}
/*
* rv_test_dummy - test reactions work as expected
*/
static void rv_test_dummy(struct kunit *test)
{
struct rv_kunit_ctx *ctx = test->priv;
static struct rv_monitor dummy_monitor = {
.name = "dummy",
.react = rv_kunit_mock_react,
};
active_ctx = ctx;
RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
rv_react(&dummy_monitor, "dummy");
RV_KUNIT_EXPECT_NO_REACTION(test, ctx);
active_ctx = NULL;
}
#include "monitors/sco/sco_kunit.c"
#include "monitors/sssw/sssw_kunit.c"
#include "monitors/sts/sts_kunit.c"
#include "monitors/opid/opid_kunit.c"
#include "monitors/nomiss/nomiss_kunit.c"
#include "monitors/pagefault/pagefault_kunit.c"
#include "monitors/sleep/sleep_kunit.c"
static struct kunit_case rv_mon_test_cases[] = {
KUNIT_CASE(rv_test_dummy),
KUNIT_CASE(rv_test_sco),
KUNIT_CASE(rv_test_sssw),
KUNIT_CASE(rv_test_sts),
KUNIT_CASE(rv_test_opid),
KUNIT_CASE(rv_test_nomiss),
KUNIT_CASE(rv_test_pagefault),
KUNIT_CASE(rv_test_sleep),
{}
};
static struct kunit_suite rv_mon_test_suite = {
.name = "rv_mon",
.suite_init = rv_set_testing,
.suite_exit = rv_clear_testing,
.init = rv_mon_test_init,
.test_cases = rv_mon_test_cases,
};
kunit_test_suites(&rv_mon_test_suite);
MODULE_AUTHOR("Gabriele Monaco <gmonaco@redhat.com>");
MODULE_DESCRIPTION("RV monitor kunit tests: test monitors by triggering reactions");
MODULE_LICENSE("GPL");
MODULE_IMPORT_NS("EXPORTED_FOR_KUNIT_TESTING");

1
kernel/trace/rv/rv_reactors.c
View File

@@ -479,3 +479,4 @@ void rv_react(struct rv_monitor *monitor, const char *msg, ...)
va_end(args);
}
EXPORT_SYMBOL_GPL(rv_react);

1
kernel/trace/rv/rv_trace.h
View File

@@ -241,6 +241,7 @@ DECLARE_EVENT_CLASS(error_ltl_monitor_id,
);
#include <monitors/pagefault/pagefault_trace.h>
#include <monitors/sleep/sleep_trace.h>
#include <monitors/wakeup/wakeup_trace.h>
// Add new monitors based on CONFIG_LTL_MON_EVENTS_ID here
#endif /* CONFIG_LTL_MON_EVENTS_ID */

23
tools/testing/selftests/verification/test.d/rv_deadline.tc Normal file
View File

@@ -0,0 +1,23 @@
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0-or-later
# description: Test deadline monitors trigger no reaction
# requires: available_reactors deadline:monitor printk:reactor stress-ng:program
load() { # returns true if there was a reaction
local lines_before
lines_before=$(dmesg | wc -l)
stress-ng --cpu 2 --sched deadline --sched-period 100000000 \
--sched-deadline 100000000 --sched-runtime 20000000 -t 5 &
stress-ng --cpu 2 --sched rr --sched-prio 50 --cyclic 1 \
--cyclic-policy rr --cyclic-prio 50 -t 5 &
wait
dmesg | tail -n +$((lines_before + 1)) | grep -q "rv: monitor [a-z]\+ does not allow event"
}
echo 1 > monitors/deadline/enable
echo printk > monitors/deadline/reactors
! load || false
echo nop > monitors/deadline/reactors
echo 0 > monitors/deadline/enable

10
tools/testing/selftests/verification/test.d/rv_monitor_enable_disable.tc
View File

@@ -10,7 +10,7 @@ test_simple_monitor() {
grep -q "$monitor$" enabled_monitors
echo 0 > "monitors/$prefix$monitor/enable"
! grep -q "$monitor$" enabled_monitors
! grep -q "$monitor$" enabled_monitors || false
echo "$monitor" >> enabled_monitors
grep -q 1 "monitors/$prefix$monitor/enable"
@@ -34,12 +34,12 @@ test_container_monitor() {
test -n "$nested"
echo 0 > "monitors/$monitor/enable"
! grep -q "^$monitor$" enabled_monitors
! grep -q "^$monitor$" enabled_monitors || false
for nested_dir in "monitors/$monitor"/*; do
[ -d "$nested_dir" ] || continue
nested=$(basename "$nested_dir")
! grep -q "^$monitor:$nested$" enabled_monitors
! grep -q "^$monitor:$nested$" enabled_monitors || false
done
echo "$monitor" >> enabled_monitors
@@ -71,5 +71,5 @@ for monitor_dir in monitors/*; do
fi
done
! echo non_existent_monitor > enabled_monitors
! grep -q "^non_existent_monitor$" enabled_monitors
! echo non_existent_monitor > enabled_monitors || false
! grep -q "^non_existent_monitor$" enabled_monitors || false

4
tools/testing/selftests/verification/test.d/rv_monitor_reactor.tc
View File

@@ -64,5 +64,5 @@ done
monitor=$(ls /sys/kernel/tracing/rv/monitors -1 | head -n 1)
test -f "monitors/$monitor/reactors"
! echo non_existent_reactor > "monitors/$monitor/reactors"
! grep -q "\\[non_existent_reactor\\]" "monitors/$monitor/reactors"
! echo non_existent_reactor > "monitors/$monitor/reactors" || false
! grep -q "\\[non_existent_reactor\\]" "monitors/$monitor/reactors" || false

33
tools/testing/selftests/verification/test.d/rv_stall.tc Normal file
View File

@@ -0,0 +1,33 @@
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0-or-later
# description: Test stall monitor
# requires: available_reactors stall:monitor printk:reactor stress-ng:program
THRESHOLD=/sys/module/stall/parameters/threshold_jiffies
ORIG_THRESHOLD=$(cat $THRESHOLD)
trap 'echo $ORIG_THRESHOLD > $THRESHOLD' EXIT
load() { # returns true if there was a reaction
local lines_before cpu
cpu=$(($(nproc) - 1))
lines_before=$(dmesg | wc -l)
stress-ng --cpu 1 --taskset "$cpu" --sched rr --sched-prio 1 -t 3 &
stress-ng --cpu 5 --taskset "$cpu" -t 3 &
wait
dmesg | tail -n +$((lines_before + 1)) | grep -q "rv: monitor stall does not allow event"
}
echo 5000 > $THRESHOLD
echo 1 > monitors/stall/enable
echo printk > monitors/stall/reactors
! load || false
echo 0 > monitors/stall/enable
echo 70 > $THRESHOLD
echo 1 > monitors/stall/enable
load
echo nop > monitors/stall/reactors
echo 0 > monitors/stall/enable

32
tools/testing/selftests/verification/test.d/rv_wwnr_printk.tc
View File

@@ -4,11 +4,29 @@
# requires: available_reactors wwnr:monitor printk:reactor stress-ng:program
load() { # returns true if there was a reaction
local lines_before num
local lines_before num load_pid ret
num=$((($(nproc) + 1) / 2))
lines_before=$(dmesg | wc -l)
stress-ng --cpu-sched "$num" --timer "$num" -t 5 -q
dmesg | tail -n $((lines_before + 1)) | grep -q "rv: monitor wwnr does not allow event"
stress-ng --cpu-sched "$num" --timer "$num" -t 5 -q &
load_pid=$!
timeout 5 dmesg -w | tail -n +$((lines_before + 1)) | \
grep -m 1 -q "rv: monitor wwnr does not allow event"
ret=$?
kill "$load_pid" || true
wait "$load_pid" || true
return $ret
}
# loads may flood the ringbuffer, wait for all pending printks (timeout at 2 minutes)
wait_dmesg_flush() {
local last_before last_after
for _ in $(seq 400); do
last_before=$last_after
last_after=$(dmesg | grep "rv:" | tail -n 1 || true)
[ "$last_before" = "$last_after" ] && return 0
sleep .3
done
return 1
}
echo 1 > monitors/wwnr/enable
@@ -17,13 +35,17 @@ echo printk > monitors/wwnr/reactors
load
echo 0 > monitoring_on
! load
wait_dmesg_flush
! load || false
echo 1 > monitoring_on
load
echo 0 > reacting_on
! load
wait_dmesg_flush
! load || false
echo 1 > reacting_on
echo nop > monitors/wwnr/reactors

11
tools/verification/models/rtapp/sleep.ltl
View File

@@ -1,7 +1,7 @@
RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
and ((not WAKE) until RT_FRIENDLY_WAKE)
RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
@@ -9,15 +9,12 @@ RT_VALID_SLEEP_REASON = FUTEX_WAIT
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI)
and not NANOSLEEP_CLOCK_REALTIME
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

5
tools/verification/models/rtapp/wakeup.ltl Normal file
View File

@@ -0,0 +1,5 @@
RULE = always (((RT and USER_THREAD) imply
(not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI

5
tools/verification/rv/Makefile
View File

@@ -78,4 +78,7 @@ clean: doc_clean fixdep-clean
$(Q)rm -f rv rv-static fixdep FEATURE-DUMP rv-*
$(Q)rm -rf feature
.PHONY: FORCE clean
check: $(RV)
RV=$(RV) prove -o --directives -f tests/
.PHONY: FORCE clean check

24
tools/verification/rv/src/rv.c
View File

@@ -50,23 +50,23 @@ static void rv_list(int argc, char **argv)
" [container]: list only monitors in this container",
NULL,
};
int i, print_help = 0, retval = 0;
int i, print_help = 0, retval = EXIT_SUCCESS;
char *container = NULL;
if (argc == 2) {
if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) {
print_help = 1;
retval = 0;
retval = EXIT_SUCCESS;
} else if (argv[1][0] == '-') {
/* assume invalid option */
print_help = 1;
retval = 1;
retval = EXIT_FAILURE;
} else
container = argv[1];
} else if (argc > 2) {
/* more than 2 is always usage */
print_help = 1;
retval = 1;
retval = EXIT_FAILURE;
}
if (print_help) {
fprintf(stderr, "rv version %s\n", VERSION);
@@ -77,7 +77,7 @@ static void rv_list(int argc, char **argv)
ikm_list_monitors(container);
exit(0);
exit(EXIT_SUCCESS);
}
/*
@@ -108,14 +108,14 @@ static void rv_mon(int argc, char **argv)
for (i = 0; usage[i]; i++)
fprintf(stderr, "%s\n", usage[i]);
exit(1);
exit(EXIT_FAILURE);
} else if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) {
fprintf(stderr, "rv version %s\n", VERSION);
for (i = 0; usage[i]; i++)
fprintf(stderr, "%s\n", usage[i]);
exit(0);
exit(EXIT_SUCCESS);
}
monitor_name = argv[1];
@@ -127,7 +127,7 @@ static void rv_mon(int argc, char **argv)
if (!run)
err_msg("rv: monitor %s does not exist\n", monitor_name);
exit(!run);
exit(run > 0 ? EXIT_SUCCESS : EXIT_FAILURE);
}
static void usage(int exit_val, const char *fmt, ...)
@@ -174,13 +174,13 @@ static void usage(int exit_val, const char *fmt, ...)
int main(int argc, char **argv)
{
if (geteuid())
usage(1, "%s needs root permission", argv[0]);
usage(EXIT_FAILURE, "%s needs root permission", argv[0]);
if (argc <= 1)
usage(1, "%s requires a command", argv[0]);
usage(EXIT_FAILURE, "%s requires a command", argv[0]);
if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help"))
usage(0, "help");
usage(EXIT_SUCCESS, "help");
if (!strcmp(argv[1], "list"))
rv_list(--argc, &argv[1]);
@@ -197,5 +197,5 @@ int main(int argc, char **argv)
}
/* invalid sub-command */
usage(1, "%s does not know the %s command, old version?", argv[0], argv[1]);
usage(EXIT_FAILURE, "%s does not know the %s command, old version?", argv[0], argv[1]);
}

48
tools/verification/rv/tests/rv_list.t Normal file
View File

@@ -0,0 +1,48 @@
#!/bin/bash
# SPDX-License-Identifier: GPL-2.0
source ../tests/engine.sh
test_begin
set_timeout 30s
RVDIR=/sys/kernel/tracing/rv/
# Help and basic tests
check "verify help page" \
"$RV --help" 0 "usage: rv command"
check "verify list subcommand help" \
"$RV list --help" 0 "list all available monitors"
all_nested=$(grep : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
all_non_nested=$(grep -v : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
sched_monitors=$(grep sched: $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g')
description_state="[[:space:]]\+[[:print:]]\+\[\(OFF\|ON\)\]"
line_nested=" - \($all_nested\)${description_state}"
line_non_nested="\($all_non_nested\)${description_state}"
# List monitors and containers
check "list all monitors" \
"$RV list" 0 "" "" "^\($line_nested\|$line_non_nested\)$"
check_if_exists "list container" \
"$RV list sched" "$RVDIR/monitors/sched" \
"" "-- No monitor found in container sched --" \
"^\($sched_monitors\)${description_state}$"
check_if_exists "list non-container" \
"$RV list wwnr" "$RVDIR/monitors/wwnr" \
"-- No monitor found in container wwnr --" \
"^\( - \)\?[[:alnum:]]\+${description_state}$"
check "list incomplete container name" \
"$RV list s" 0 "-- No monitor found in container s --"
# Error handling tests
check "no command" \
"$RV" 1 "rv requires a command"
check "invalid command" \
"$RV invalid" 1 "rv does not know the invalid command"
test_end

95
tools/verification/rv/tests/rv_mon.t Normal file
View File

@@ -0,0 +1,95 @@
#!/bin/bash
# SPDX-License-Identifier: GPL-2.0
source ../tests/engine.sh
test_begin
set_timeout 30s
RVDIR=/sys/kernel/tracing/rv/
# Help and basic tests
check "verify mon subcommand help" \
"$RV mon --help" 0 "run a monitor"
# Error handling tests
check "mon without monitor name" \
"$RV mon" 1 "usage: rv mon"
check "invalid monitor name" \
"$RV mon invalid" 1 "monitor invalid does not exist"
if [ -d $RVDIR/monitors/wwnr ]; then
check "invalid reactor name" \
"$RV mon wwnr -r invalid" 1 "failed to set invalid reactor, is it available?"
check "monitor name is substring of another monitor" \
"$RV mon nr" 1 "monitor nr does not exist"
check "already enabled monitor returns error" \
"echo 1 > $RVDIR/monitors/wwnr/enable; $RV mon wwnr" 1 \
"monitor wwnr (in-kernel) is already enabled"
echo 0 > $RVDIR/monitors/wwnr/enable
fi
# rv mon runs until terminated
set_expected_timeout 2s
# Run monitors with different configurations
check_if_exists "run the monitor without parameters" \
"$RV mon wwnr" "$RVDIR/monitors/wwnr" "" "."
check_if_exists "run the monitor as verbose" \
"$RV mon wwnr -v" "$RVDIR/monitors/wwnr" \
"my pid is \$pid" "\(event\|error\)"
check_if_exists "run the monitor with a reactor" \
"$RV mon wwnr -r printk & sleep .5 && cat $RVDIR/monitors/wwnr/reactors && wait" \
"$RVDIR/monitors/wwnr/reactors" "\[printk\]"
check_if_exists "reactor is restored after exit" \
"cat $RVDIR/monitors/wwnr/reactors" \
"$RVDIR/monitors/wwnr/reactors" "\[nop\]"
check_if_exists "run a nested monitor with a reactor" \
"$RV mon snroc -r printk & sleep .5 && cat $RVDIR/monitors/sched/snroc/reactors && wait" \
"$RVDIR/monitors/sched/snroc/reactors" "\[printk\]"
check_if_exists "run an explicitly nested monitor with a reactor" \
"$RV mon sched:sssw -r printk & sleep .5 && cat $RVDIR/monitors/sched/sssw/reactors && wait" \
"$RVDIR/monitors/sched/sssw/reactors" "\[printk\]"
check_if_exists "run container monitor" \
"$RV mon sched & sleep .5 && cat $RVDIR/monitors/sched/{sssw,sco}/enable && wait" \
"$RVDIR/monitors/sched" "1" "0" "^1$"
# Regexes for the trace
header="^[[:space:]]\+\(\([][A-Z_x<>-]\+\||\)[[:space:]]*\)\+$"
type="\(event\|error\)[[:space:]]\+"
genpid="[0-9]\+[[:space:]]\+"
selfpid="\$pid[[:space:]]\+"
cpu="\[[0-9]\{3\}\][[:space:]]\+"
state="[a-z_]\+ "
trace_task="${genpid}${cpu}${type}${genpid}${state}"
trace_task_self="${genpid}${cpu}${type}${selfpid}${state}"
trace_cpu="${genpid}${cpu}${type}${state}"
trace_cpu_self="${selfpid}${cpu}${type}${state}"
check_if_exists "run per-task monitor with tracing" \
"$RV mon sssw -t" "$RVDIR/monitors/sched/sssw" \
"$header" "$trace_task_self" "\($header\|$trace_task\)"
check_if_exists "run per-task monitor tracing also self" \
"$RV mon sched:sssw -t -s" "$RVDIR/monitors/sched/sssw" \
"$trace_task_self" "" "\($header\|$trace_task\)"
check_if_exists "run per-cpu monitor with tracing" \
"$RV mon sched:sco -t" "$RVDIR/monitors/sched/sco" \
"$header" "$trace_cpu_self" "\($header\|$trace_cpu\)"
check_if_exists "run per-cpu monitor tracing also self" \
"$RV mon sco -t -s" "$RVDIR/monitors/sched/sco" \
"$trace_cpu_self" "" "\($header\|$trace_cpu\)"
test_end

5
tools/verification/rvgen/Makefile
View File

@@ -13,12 +13,17 @@ all:
.PHONY: clean
clean:
.PHONY: check
check:
prove -o --directives -f tests/
.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/kunit.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/kunit.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

22
tools/verification/rvgen/__main__.py
View File

@@ -6,14 +6,16 @@
# dot2k: transform dot files into a monitor for the Linux kernel.
#
# For further information, see:
# Documentation/trace/rv/da_monitor_synthesis.rst
# Documentation/trace/rv/monitor_synthesis.rst
if __name__ == '__main__':
from rvgen.dot2k import da2k, ha2k
from rvgen.generator import Monitor
from rvgen.container import Container
from rvgen.ltl2k import ltl2k
from rvgen.kunit import KUnit, KUnitError
from rvgen.automata import AutomataError
from rvgen.ltl2ba import LTLError
import argparse
import sys
@@ -41,6 +43,11 @@ if __name__ == '__main__':
container_parser = subparsers.add_parser("container", parents=[parent_parser])
container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
kunit_parser = subparsers.add_parser("kunit", parents=[parent_parser])
kunit_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
kunit_parser.add_argument('-l', "--local", dest="local", action="store_true", required=False,
help="Force looking for the monitor in the current directory only")
params = parser.parse_args()
try:
@@ -55,10 +62,17 @@ if __name__ == '__main__':
else:
print("Unknown monitor class:", params.monitor_class)
sys.exit(1)
else:
elif params.subcmd == "container":
monitor = Container(vars(params))
except AutomataError as e:
print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
elif params.subcmd == "kunit":
monitor = KUnit(vars(params))
monitor.print_files()
sys.exit(0)
except (AutomataError, LTLError) as e:
print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
sys.exit(1)
except KUnitError as e:
print(f"There was an error generating KUnit files:\n{e}", file=sys.stderr)
sys.exit(1)
print(f"Writing the monitor into the directory {monitor.name}")

635
tools/verification/rvgen/rvgen/automata.py
View File

@@ -9,22 +9,349 @@
# Documentation/trace/rv/deterministic_automata.rst
import ntpath
import re
from typing import Iterator
from itertools import islice
class _ConstraintKey:
"""Base class for constraint keys."""
import lark
class _StateConstraintKey(_ConstraintKey, int):
"""Key for a state constraint. Under the hood just state_id."""
def __new__(cls, state_id: int):
return super().__new__(cls, state_id)
class ParseTree:
# based on https://graphviz.org/doc/info/lang.html
# with the irrelevant stuffs (port and compass) removed
grammar = r'''
start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
class _EventConstraintKey(_ConstraintKey, tuple):
"""Key for an event constraint. Under the hood just tuple(state_id,event_id)."""
def __new__(cls, state_id: int, event_id: int):
return super().__new__(cls, (state_id, event_id))
stmt_list: (stmt ";"? stmt_list)?
stmt: node_stmt
| edge_stmt
| attr_stmt
| ID "=" ID
| subgraph
attr_stmt: attr_type attr_list
attr_type: "graph" -> graph
| "node" -> node
| "edge" -> edge
attr_list: "[" a_list? "]" attr_list?
a_list: ID "=" ID (";" | ",")? a_list?
edge_stmt: (node_id | subgraph) edgerhs attr_list?
edgerhs: edgeop (node_id | subgraph) edgerhs?
edgeop: "->" | "--"
node_stmt: node_id attr_list?
node_id: ID
subgraph: ("subgraph" ID?)? "{" stmt_list "}"
ID: CNAME
| /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
| ESCAPED_STRING
%import common.CNAME
%import common.ESCAPED_STRING
%import common.WS
%ignore WS
'''
@staticmethod
def parse_edge(tree: lark.Tree) -> tuple[str, str]:
# only support a simple node-to-node edge
nodes = []
for node in tree.iter_subtrees_topdown():
if node.data == "node_id":
nodes.append(node.children[0].strip('"'))
if len(nodes) != 2:
raise AutomataError("Only state-to-state transition is supported")
return tuple(nodes)
class ParseNodes(lark.visitors.Visitor):
def __init__(self, *args, **kwargs):
self.nodes = set()
super().__init__(*args, **kwargs)
def node_stmt(self, tree):
node_id = tree.children[0]
node = node_id.children[0].strip('"')
self.nodes.add(node)
class ParseEdges(lark.visitors.Visitor):
def __init__(self, *args, **kwargs):
self.edges = set()
super().__init__(*args, **kwargs)
def edge_stmt(self, tree):
edge = ParseTree.parse_edge(tree)
self.edges.add(edge)
class ParseAttributes(lark.visitors.Interpreter):
def __init__(self, *args, **kwargs):
'''
Stacks of default attributes. [0] is the default
attributes for the outermost scope, while [-1] is the
default attributes for the current scope.
'''
self.default_node_attrs = [{}]
self.default_edge_attrs = [{}]
self.node_attrs = {}
self.edge_attrs = {}
super().__init__(*args, **kwargs)
@staticmethod
def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
attrs = {}
for node in stmt.iter_subtrees():
if node.data == "a_list":
attrs[node.children[0]] = node.children[1].strip('"')
return attrs
def subgraph(self, tree):
# We are entering a new scope, inherit the default
# attributes of the outer scope
self.default_node_attrs.append(self.default_node_attrs[-1].copy())
self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
children = self.visit_children(tree)
# Exiting the scope
del self.default_node_attrs[-1]
del self.default_edge_attrs[-1]
return children
def node_stmt(self, tree):
node_id = tree.children[0]
node = node_id.children[0].strip('"')
attrs = self.default_node_attrs[-1].copy()
attrs |= self.__get_attrs(tree)
if attrs:
if node in self.node_attrs:
self.node_attrs[node] = attrs | self.node_attrs[node]
else:
self.node_attrs[node] = attrs
return self.visit_children(tree)
def edge_stmt(self, tree):
edge = ParseTree.parse_edge(tree)
attrs = self.default_edge_attrs[-1].copy()
attrs |= self.__get_attrs(tree)
if attrs:
if edge in self.edge_attrs:
self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
else:
self.edge_attrs[edge] = attrs
return self.visit_children(tree)
def attr_stmt(self, tree):
attr_type = tree.children[0].data
attrs = self.__get_attrs(tree)
if attr_type == "node":
self.default_node_attrs[-1] |= attrs
elif attr_type == "edge":
self.default_edge_attrs[-1] |= attrs
else:
# graph attributes are irrelevant
pass
self.visit_children(tree)
def __init__(self, dot_file):
parser = lark.Lark(self.grammar, parser='lalr')
node_parser = self.ParseNodes()
edge_parser = self.ParseEdges()
attributes_parser = self.ParseAttributes()
try:
with open(dot_file, "r") as f:
tree = parser.parse(f.read())
attributes_parser.visit(tree)
node_parser.visit(tree)
edge_parser.visit(tree)
except OSError as exc:
raise AutomataError(exc.strerror) from exc
except lark.exceptions.UnexpectedInput as exc:
raise AutomataError(str(exc))
self.nodes = node_parser.nodes
self.edges = edge_parser.edges
self.node_attrs = attributes_parser.node_attrs
self.edge_attrs = attributes_parser.edge_attrs
class ConstraintCondition:
def __init__(self, env: str, op: str, val: str, unit=None):
self.env = env
self.op = op
self.val = val
self.unit = unit
if unit is None:
# try to infer unit from constants or parameters
val_for_unit = val.lower().replace("()", "")
if val_for_unit.endswith("_ns"):
self.unit = "ns"
if val_for_unit.endswith("_jiffies"):
self.unit = "j"
class ConstraintRule:
grammar = r'''
rule: condition (OP condition)*
OP: "&&" | "||"
condition: ENV CMP_OP VAL UNIT?
ENV: CNAME
CMP_OP: "==" | "!=" | "<=" | "<" | ">=" | ">"
VAL: /[0-9]+/
| /[A-Z_]+\(\)/
| /[A-Z_]+/
| /[a-z_]+\(\)/
| /[a-z_]+/
UNIT: "ns" | "us" | "ms" | "s" | "j"
'''
def __init__(self, c: ConstraintCondition):
'''
A list of pairs of
- the condition (e.g. is_constr_dl == 1)
- the logical operator ("||" or "&&") combining this
condition with the next one if it exists, otherwise None
TODO: Perhaps use an abstract syntax tree instead, because
this representation cannot capture precedence
'''
self.rules = [[c, None]]
def chain(self, op: str, c: ConstraintCondition):
self.rules[-1][1] = op
self.rules.append([c, None])
class ConstraintReset:
def __init__(self, env):
self.env = env
class StateLabelParser:
grammar = r'''
label: CNAME ("\\n" condition)?
%import common.CNAME
%import common.WS
%ignore WS
''' + ConstraintRule.grammar
parser = lark.Lark(grammar, parser='lalr', start="label")
def __init__(self, label: str):
try:
tree = self.parser.parse(label)
except lark.exceptions.UnexpectedInput as exc:
raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}"))
self.state = tree.children[0]
self.constraint = None
if len(tree.children) == 2:
self.constraint = ConstraintCondition(*tree.children[1].children)
if self.constraint.op not in ("<", "<="):
raise AutomataError("State constraints must be clock expirations like"
f" clk<N ({label})")
class EventLabelParser:
grammar = r'''
events: event ("\\n" event)*
event: name (";" guard)?
guard: reset
| rule
| rule ";" reset
| reset ";" rule
name: CNAME
reset: "reset" "(" ENV ")"
%import common.CNAME
%import common.WS
%ignore WS
''' + ConstraintRule.grammar
parser = lark.Lark(grammar, parser='lalr', start="events")
class GetEvents(lark.visitors.Transformer):
def guard(self, args):
reset = None
rule = None
for arg in args:
if arg.data == "reset":
reset = ConstraintReset(arg.children[0])
elif arg.data == "rule":
conditions = arg.children
rule = ConstraintRule(conditions[0])
for i in range(1, len(conditions), 2):
rule.chain(conditions[i], conditions[i + 1])
return reset, rule
def OP(self, args):
return args
def condition(self, args):
return ConstraintCondition(*args)
def event(self, args):
assert(len(args) <= 2)
name = args[0]
rule, reset = None, None
if len(args) == 2:
reset, rule = args[1]
return name, reset, rule
def events(self, args):
return args
def name(self, args):
return args[0]
def __init__(self, label: str):
try:
tree = self.parser.parse(label)
self.events = self.GetEvents().transform(tree)
except lark.exceptions.UnexpectedInput as exc:
raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}"))
class Transition:
def __init__(self, src: str, dst: str, event: str,
reset: ConstraintReset, rule: ConstraintRule):
self.src = src
self.dst = dst
self.event = event
self.rule = rule
self.reset = reset
class State:
def __init__(self, name: str, inv: ConstraintCondition):
self.name = name
self.inv = inv
class AutomataError(Exception):
"""Exception raised for errors in automata parsing and validation.
@@ -44,35 +371,19 @@ class Automata:
invalid_state_str = "INVALID_STATE"
init_marker = "__init_"
node_marker = "{node"
# val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
# only numerical values should have units
constraint_rule = re.compile(r"""
^
(?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env var
(?P<op>[!<=>]{1,2}) # operator
(?P<val>
[0-9]+ | # numerical value
[A-Z_]+\(\) | # macro
[A-Z_]+ | # constant
[a-z_]+\(\) | # function
[a-z_]+ # parameter
)
(?P<unit>[a-z]{1,2})? # optional unit for numerical values
""", re.VERBOSE)
constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)")
def __init__(self, file_path, model_name=None):
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.__parse_tree = ParseTree(file_path)
self.transitions = self.__parse_transitions()
self.states, self.initial_state, self.final_states = self.__parse_states()
self.env_types = {}
self.env_stored = set()
self.constraint_vars = set()
self.self_loop_reset_events = set()
self.events, self.envs = self.__get_event_variables()
self.function, self.constraints = self.__create_matrix()
self.function = self.__create_matrix()
self.events_start, self.events_start_run = self.__store_init_events()
self.env_stored = sorted(self.env_stored)
self.constraint_vars = sorted(self.constraint_vars)
@@ -90,194 +401,94 @@ class Automata:
return model_name
def __open_dot(self) -> list[str]:
dot_lines = []
try:
with open(self.__dot_path) as dot_file:
dot_lines = dot_file.readlines()
except OSError as exc:
raise AutomataError(exc.strerror) from exc
def __parse_transitions(self):
transitions = []
if not dot_lines:
raise AutomataError(f"{self.__dot_path} is empty")
# checking the first line:
line = dot_lines[0].split()
if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
return dot_lines
def __get_cursor_begin_states(self) -> int:
for cursor, line in enumerate(self.__dot_lines):
split_line = line.split()
if len(split_line) and split_line[0] == self.node_marker:
return cursor
raise AutomataError("Could not find a beginning state")
def __get_cursor_begin_events(self) -> int:
state = 0
cursor = 0 # make pyright happy
for cursor, line in enumerate(self.__dot_lines):
line = line.split()
if not line:
for edge in self.__parse_tree.edges:
attr = self.__parse_tree.edge_attrs.get(edge)
if not attr:
continue
if state == 0:
if line[0] == self.node_marker:
state = 1
elif line[0] != self.node_marker:
break
else:
raise AutomataError("Could not find beginning event")
label = attr.get("label")
cursor += 1 # skip initial state transition
if cursor == len(self.__dot_lines):
raise AutomataError("Dot file ended after event beginning")
src, dst = edge
return cursor
parser = EventLabelParser(label)
for event, reset, rule in parser.events:
transitions.append(Transition(src, dst, event, reset, rule))
def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
# wait for node declaration
transitions.sort(key=lambda t : (t.src, t.event))
return transitions
def __parse_states(self):
initial_state = ""
states = []
final_states = []
initial_state = ""
has_final_states = False
cursor = self.__get_cursor_begin_states()
for node in self.__parse_tree.nodes:
attr = self.__parse_tree.node_attrs[node]
label = attr.get("label")
# process nodes
for line in islice(self.__dot_lines, cursor, None):
split_line = line.split()
if not split_line or split_line[0] != self.node_marker:
break
if node.startswith(Automata.init_marker):
initial_state = node[len(Automata.init_marker):]
raw_state = split_line[-1]
if not label:
continue
# "enabled_fired"}; -> enabled_fired
state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
if state.startswith(self.init_marker):
initial_state = state[len(self.init_marker):]
else:
states.append(state)
if "doublecircle" in line:
final_states.append(state)
has_final_states = True
parser = StateLabelParser(label)
state = State(parser.state, parser.constraint)
if "ellipse" in line:
final_states.append(state)
has_final_states = True
states.append(state)
shape = attr.get("shape")
if shape in ("doublecircle", "ellipse"):
final_states.append(state)
initial_state = next((s for s in states if s.name == initial_state), None)
if not initial_state:
raise AutomataError("The automaton doesn't have an initial state")
states = sorted(set(states))
states.remove(initial_state)
# Insert the initial state at the beginning of the states
states.insert(0, initial_state)
if not has_final_states:
if not final_states:
final_states.append(initial_state)
states.remove(initial_state)
states.sort(key=lambda s : s.name)
states.insert(0, initial_state)
return states, initial_state, final_states
def __get_event_variables(self) -> tuple[list[str], list[str]]:
events: list[str] = []
envs: list[str] = []
# here we are at the begin of transitions, take a note, we will return later.
cursor = self.__get_cursor_begin_events()
for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
if not line.startswith('"'):
break
for transition in self.transitions:
events.append(transition.event)
# transitions have the format:
# "all_fired" -> "both_fired" [ label = "disable_irq" ];
# ------------ event is here ------------^^^^^
split_line = line.split()
if len(split_line) > 1 and split_line[1] == "->":
event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
if transition.reset:
envs.append(transition.reset.env)
self.env_stored.add(transition.reset.env)
if transition.rule:
for c, _ in transition.rule.rules:
envs.append(c.env)
self.__extract_env_var(c)
# when a transition has more than one label, they are like this
# "local_irq_enable\nhw_local_irq_enable_n"
# so split them.
for i in event.split("\\n"):
# if the event contains a constraint (hybrid automata),
# it will be separated by a ";":
# "sched_switch;x<1000;reset(x)"
ev, *constr = i.split(";")
if constr:
if len(constr) > 2:
raise AutomataError("Only 1 constraint and 1 reset are supported")
envs += self.__extract_env_var(constr)
events.append(ev)
else:
# state labels have the format:
# "enable_fired" [label = "enable_fired\ncondition"];
# ----- label is here -----^^^^^
# label and node name must be the same, condition is optional
state = line.split("label")[1].split('"')[1]
_, *constr = state.split("\\n")
if constr:
if len(constr) > 1:
raise AutomataError("Only 1 constraint is supported in the state")
envs += self.__extract_env_var([constr[0].replace(" ", "")])
for state in self.states:
if state.inv:
envs.append(state.inv.env)
self.__extract_env_var(state.inv)
return sorted(set(events)), sorted(set(envs))
def _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str,
str | None]]:
"""
Get a list of strings of the type constr1 && constr2 and returns a list of
constraints and separators: [[constr1,"&&"],[constr2,None]]
"""
exprs = []
seps = []
for c in constr:
while "&&" in c or "||" in c:
a = c.find("&&")
o = c.find("||")
pos = a if o < 0 or 0 < a < o else o
exprs.append(c[:pos].replace(" ", ""))
seps.append(c[pos:pos + 2].replace(" ", ""))
c = c[pos + 2:].replace(" ", "")
exprs.append(c)
seps.append(None)
return zip(exprs, seps)
def __extract_env_var(self, constraint: ConstraintCondition):
if constraint.unit:
self.env_types[constraint.env] = constraint.unit
if constraint.val[0].isalpha():
self.constraint_vars.add(constraint.val)
def __extract_env_var(self, constraint: list[str]) -> list[str]:
env = []
for c, _ in self._split_constraint_expr(constraint):
rule = self.constraint_rule.search(c)
reset = self.constraint_reset.search(c)
if rule:
env.append(rule["env"])
if rule.groupdict().get("unit"):
self.env_types[rule["env"]] = rule["unit"]
if rule["val"][0].isalpha():
self.constraint_vars.add(rule["val"])
# try to infer unit from constants or parameters
val_for_unit = rule["val"].lower().replace("()", "")
if val_for_unit.endswith("_ns"):
self.env_types[rule["env"]] = "ns"
if val_for_unit.endswith("_jiffies"):
self.env_types[rule["env"]] = "j"
if reset:
env.append(reset["env"])
# environment variables that are reset need a storage
self.env_stored.add(reset["env"])
return env
def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
states = self.states
states = [s.name for s in self.states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -292,39 +503,16 @@ class Automata:
# declare the matrix....
matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
constraints: dict[_ConstraintKey, list[str]] = {}
# and we are back! Let's fill the matrix
cursor = self.__get_cursor_begin_events()
for transition in self.transitions:
src, dst = transition.src, transition.dst
event = transition.event
if src == dst and transition.reset:
# those events reset also on self loops
self.self_loop_reset_events.add(event)
matrix[states_dict[src]][events_dict[event]] = dst
for line in map(str.lstrip,
islice(self.__dot_lines, cursor, None)):
if not line or line[0] != '"':
break
split_line = line.split()
if len(split_line) > 2 and split_line[1] == "->":
origin_state = split_line[0].replace('"', '').replace(',', '_')
dest_state = split_line[2].replace('"', '').replace(',', '_')
possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
for event in possible_events.split("\\n"):
event, *constr = event.split(";")
if constr:
key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
constraints[key] = constr
# those events reset also on self loops
if origin_state == dest_state and "reset" in "".join(constr):
self.self_loop_reset_events.add(event)
matrix[states_dict[origin_state]][events_dict[event]] = dest_state
else:
state = line.split("label")[1].split('"')[1]
state, *constr = state.replace(" ", "").split("\\n")
if constr:
constraints[_StateConstraintKey(states_dict[state])] = constr
return matrix, constraints
return matrix
def __store_init_events(self) -> tuple[list[bool], list[bool]]:
events_start = [False] * len(self.events)
@@ -336,7 +524,7 @@ class Automata:
for j in range(len(self.states)):
if self.function[j][i] != self.invalid_state_str:
curr_event_used += 1
if self.function[j][i] == self.initial_state:
if self.function[j][i] == self.initial_state.name:
curr_event_will_init += 1
if self.function[0][i] != self.invalid_state_str:
curr_event_from_init = True
@@ -359,10 +547,3 @@ class Automata:
def is_hybrid_automata(self) -> bool:
return bool(self.envs)
def is_event_constraint(self, key: _ConstraintKey) -> bool:
"""
Given the key in self.constraints return true if it is an event
constraint, false if it is a state constraint
"""
return isinstance(key, _EventConstraintKey)

10
tools/verification/rvgen/rvgen/dot2c.py
View File

@@ -29,10 +29,10 @@ class Dot2c(Automata):
def __get_enum_states_content(self) -> list[str]:
buff = []
buff.append(f"\t{self.initial_state}{self.enum_suffix},")
buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
for state in self.states:
if state != self.initial_state:
buff.append(f"\t{state}{self.enum_suffix},")
buff.append(f"\t{state.name}{self.enum_suffix},")
buff.append(f"\tstate_max{self.enum_suffix},")
return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata):
def format_aut_init_states_string(self) -> list[str]:
buff = []
buff.append("\t.state_names = {")
buff.append(self.__get_string_vector_per_line_content(self.states))
buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
buff.append("\t},")
return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata):
return buff
def __get_max_strlen_of_states(self) -> int:
max_state_name = len(max(self.states, key=len))
max_state_name = max((len(s.name) for s in self.states))
return max(max_state_name, len(self.invalid_state_str))
def get_aut_init_function(self) -> str:
@@ -199,7 +199,7 @@ class Dot2c(Automata):
return buff
def get_aut_init_initial_state(self) -> str:
return self.initial_state
return self.initial_state.name
def format_aut_init_initial_state(self) -> list[str]:
buff = []

321
tools/verification/rvgen/rvgen/dot2k.py
View File

@@ -6,17 +6,18 @@
# dot2k: transform dot files into a monitor for the Linux kernel.
#
# For further information, see:
# Documentation/trace/rv/da_monitor_synthesis.rst
# Documentation/trace/rv/monitor_synthesis.rst
from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
from .automata import ConstraintCondition, AutomataError
class dot2k(Monitor, Dot2c):
template_dir = "dot2k"
# only needed for the per-obj cleanup hook
cleanup_marker = "obj_cleanup"
def __init__(self, file_path, MonitorType, extra_params={}):
self.monitor_type = MonitorType
Monitor.__init__(self, extra_params)
@@ -56,18 +57,30 @@ class dot2k(Monitor, Dot2c):
buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
buff.append("}")
buff.append("")
if self.monitor_type == "per_obj":
buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */")
buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)")
buff.append("{")
buff.append("\tint id = /* XXX: how do I get the id? */;")
buff.append("\tda_destroy_storage(id);")
buff.append("}")
buff.append("")
return '\n'.join(buff)
def fill_tracepoint_attach_probe(self) -> str:
buff = []
for event in self.events:
buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
if self.monitor_type == "per_obj":
buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
return '\n'.join(buff)
def fill_tracepoint_detach_helper(self) -> str:
buff = []
for event in self.events:
buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
if self.monitor_type == "per_obj":
buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
return '\n'.join(buff)
def fill_model_h_header(self) -> list[str]:
@@ -176,7 +189,14 @@ class ha2k(dot2k):
if not self.is_hybrid_automata():
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
self.has_invariant = False
self.has_guard = False
for state in self.states:
if state.inv:
self.has_invariant = True
for transition in self.transitions:
if transition.rule or transition.reset:
self.has_guard = True
def fill_monitor_class_type(self) -> str:
if self._is_id_monitor():
@@ -209,38 +229,52 @@ class ha2k(dot2k):
value *= 10**9
return str(value) + "ull"
def __parse_single_constraint(self, rule: dict, value: str) -> str:
return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
def __parse_guard_rule(self, rule) -> list[str]:
buff = []
for c, sep in rule.rules:
env = c.env + self.enum_suffix
op = c.op
val = self.__adjust_value(c.val, c.unit)
def __get_constraint_env(self, constr: str) -> str:
"""Extract the second argument from an ha_ function"""
env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
assert env.removesuffix(f"_{self.name}") in self.envs
return env
cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
if sep:
cond += f" {sep}"
buff.append(cond)
return buff
def __start_to_invariant_check(self, constr: str) -> str:
# by default assume the timer has ns expiration
env = self.__get_constraint_env(constr)
clock_type = "ns"
if self.env_types.get(env.removesuffix(f"_{self.name}")) == "j":
clock_type = "jiffy"
return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
def __start_to_conv(self, constr: str) -> str:
"""
Undo the storage conversion done by ha_start_timer_
"""
return "ha_inv_to_guard" + constr[constr.find("("):]
def __parse_timer_constraint(self, rule: dict, value: str) -> str:
def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
# by default assume the timer has ns expiration
clock_type = "ns"
if self.env_types.get(rule["env"]) == "j":
if inv.unit == "j":
clock_type = "jiffy"
return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
f" {value}, time_ns)")
value = self.__adjust_value(inv.val, inv.unit)
return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
def __parse_invariant(self, inv):
# by default assume the timer has ns expiration
clock_type = "ns"
if inv.unit == "j":
clock_type = "jiffy"
env = inv.env + self.enum_suffix
try:
val = int(inv.val)
except ValueError:
# it's a constant, a parameter or a function
val = inv.val.replace("()", "(ha_mon)")
match inv.unit:
case "us":
val *= 10**3
case "ms":
val *= 10**6
case "s":
val *= 10**9
return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
f" {val}, time_ns)")
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
@@ -259,124 +293,35 @@ class ha2k(dot2k):
rules = invalid_checks + rules
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
return ["res = " + separator.join(rules)]
def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
rule, reset) -> None:
# event constrains are tuples and allow both rules and reset
# state constraints are only used for expirations (e.g. clk<N)
if self.is_event_constraint(key):
if not rule and not reset:
raise AutomataError("Unrecognised event constraint "
f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
if rule and (rule["env"] in self.env_types and
rule["env"] not in self.env_stored):
raise AutomataError("Clocks in hybrid automata always require a storage"
f" ({rule["env"]})")
else:
if not rule:
raise AutomataError("Unrecognised state constraint "
f"({self.states[key]}: {constr})")
if rule["env"] not in self.env_stored:
raise AutomataError("State constraints always require a storage "
f"({rule["env"]})")
if rule["op"] not in ["<", "<="]:
raise AutomataError("State constraints must be clock expirations like"
f" clk<N ({rule.string})")
def __parse_constraints(self) -> None:
self.guards: dict[_EventConstraintKey, str] = {}
self.invariants: dict[_StateConstraintKey, str] = {}
for key, constraint in self.constraints.items():
rules = []
resets = []
for c, sep in self._split_constraint_expr(constraint):
rule = self.constraint_rule.search(c)
reset = self.constraint_reset.search(c)
self.__validate_constraint(key, c, rule, reset)
if rule:
value = rule["val"]
value_len = len(rule["val"])
unit = None
if rule.groupdict().get("unit"):
value_len += len(rule["unit"])
unit = rule["unit"]
c = c[:-(value_len)]
value = self.__adjust_value(value, unit)
if self.is_event_constraint(key):
c = self.__parse_single_constraint(rule, value)
if sep:
c += f" {sep}"
else:
c = self.__parse_timer_constraint(rule, value)
rules.append(c)
if reset:
c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
resets.append(c)
if self.is_event_constraint(key):
res = self.__format_guard_rules(rules) + resets
self.guards[key] = ";".join(res)
else:
self.invariants[key] = rules[0]
return ["res = " + separator.join(rules) + ";"]
def __fill_verify_invariants_func(self) -> list[str]:
buff = []
if not self.invariants:
if not self.has_invariant:
return []
buff.append(
buff = [
f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
{{""")
{{"""]
_else = ""
for state, constr in sorted(self.invariants.items()):
check_str = self.__start_to_invariant_check(constr)
buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
for state in self.states:
if not state.inv:
continue
check_str = self.__start_to_invariant_check(state.inv)
buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
buff.append(f"\t\t{check_str};")
_else = "else "
buff.append("\treturn true;\n}\n")
return buff
def __fill_convert_inv_guard_func(self) -> list[str]:
buff = []
if not self.invariants:
return []
conflict_guards, conflict_invs = self.__find_inv_conflicts()
if not conflict_guards and not conflict_invs:
return []
buff.append(
f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
{{""")
buff.append("\tif (curr_state == next_state)\n\t\treturn;")
_else = ""
for state, constr in sorted(self.invariants.items()):
# a state with invariant can reach us without reset
# multiple conflicts must have the same invariant, otherwise we cannot
# know how to reset the value
conf_i = [start for start, end in conflict_invs if end == state]
# we can reach a guard without reset
conf_g = [e for s, e in conflict_guards if s == state]
if not conf_i and not conf_g:
continue
buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
buff.append(f"\t\t{self.__start_to_conv(constr)};")
_else = "else "
buff.append("}\n")
return buff
def __fill_verify_guards_func(self) -> list[str]:
buff = []
if not self.guards:
if not self.has_guard:
return []
buff.append(
@@ -388,14 +333,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
""")
_else = ""
for edge, constr in sorted(self.guards.items()):
for transition in self.transitions:
if not transition.rule and not transition.reset:
continue
buff.append(f"\t{_else}if (curr_state == "
f"{self.states[edge[0]]}{self.enum_suffix} && "
f"event == {self.events[edge[1]]}{self.enum_suffix})")
if constr.count(";") > 0:
f"{transition.src}{self.enum_suffix} && "
f"event == {transition.event}{self.enum_suffix})")
rule = transition.rule
reset = transition.reset
if rule and reset:
buff[-1] += " {"
buff += [f"\t\t{c};" for c in constr.split(";")]
if constr.count(";") > 0:
if rule:
buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
if reset:
buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
if rule and reset:
_else = "} else "
else:
_else = "else "
@@ -404,64 +357,15 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
buff.append("\treturn res;\n}\n")
return buff
def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
set[tuple[int, _StateConstraintKey]]]:
"""
Run a breadth first search from all states with an invariant.
Find any conflicting constraints reachable from there, this can be
another state with an invariant or an edge with a non-reset guard.
Stop when we find a reset.
Return the set of conflicting guards and invariants as tuples of
conflicting state and constraint key.
"""
conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
for start_idx in self.invariants:
queue = deque([(start_idx, 0)]) # (state_idx, distance)
env = self.__get_constraint_env(self.invariants[start_idx])
while queue:
curr_idx, distance = queue.popleft()
# Check state condition
if curr_idx != start_idx and curr_idx in self.invariants:
conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
continue
# Check if we should stop
if distance > len(self.states):
break
if curr_idx != start_idx and distance > 1:
continue
for event_idx, next_state_name in enumerate(self.function[curr_idx]):
if next_state_name == self.invalid_state_str:
continue
curr_guard = self.guards.get((curr_idx, event_idx), "")
if "reset" in curr_guard and env in curr_guard:
continue
if env in curr_guard:
conflict_guards.add((start_idx,
_EventConstraintKey(curr_idx, event_idx)))
continue
next_idx = self.states.index(next_state_name)
queue.append((next_idx, distance + 1))
return conflict_guards, conflict_invs
def __fill_setup_invariants_func(self) -> list[str]:
buff = []
if not self.invariants:
if not self.has_invariant:
return []
buff.append(
buff = [
f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
{{"""]
conditions = ["next_state == curr_state"]
conditions += [f"event != {e}{self.enum_suffix}"
@@ -470,13 +374,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
for state, constr in sorted(self.invariants.items()):
buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
buff.append(f"\t\t{constr};")
for state in self.states:
inv = state.inv
if not inv:
continue
inv = self.__parse_invariant(inv)
buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
buff.append(f"\t\t{inv};")
_else = "else "
for state in self.invariants:
buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
for state in self.states:
inv = state.inv
if not inv:
continue
buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")
buff.append("}\n")
@@ -484,7 +395,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
def __fill_constr_func(self) -> list[str]:
buff = []
if not self.constraints:
if not self.has_invariant and not self.has_guard:
return []
buff.append(
@@ -496,16 +407,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
* the next state has a constraint, cancel it in any other case and to check
* that it didn't expire before the callback run. Transitions to the same state
* without a reset never affect timers.
* Due to the different representations between invariants and guards, there is
* a function to convert it in case invariants or guards are reachable from
* another invariant without reset. Those are not present if not required in
* the model. This is all automatic but is worth checking because it may show
* errors in the model (e.g. missing resets).
*/""")
buff += self.__fill_verify_invariants_func()
inv_conflicts = self.__fill_convert_inv_guard_func()
buff += inv_conflicts
buff += self.__fill_verify_guards_func()
buff += self.__fill_setup_invariants_func()
@@ -515,18 +419,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
if self.invariants:
if self.has_invariant:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
if inv_conflicts:
buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
"next_state, time_ns);\n")
if self.guards:
if self.has_guard:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
"next_state, time_ns))\n\t\treturn false;\n")
if self.invariants:
if self.has_invariant:
buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
buff.append("\treturn true;\n}\n")
@@ -603,7 +504,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
def _fill_timer_type(self) -> list:
if self.invariants:
if self.has_invariant:
return [
"/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
"#define HA_TIMER_TYPE HA_TIMER_HRTIMER"

51
tools/verification/rvgen/rvgen/generator.py
View File

@@ -6,7 +6,7 @@
# Abstract class for generating kernel runtime verification monitors from specification file
import platform
import os
from pathlib import Path
class RVGenerator:
@@ -16,36 +16,38 @@ class RVGenerator:
self.name = extra_params.get("model_name")
self.parent = extra_params.get("parent")
self.abs_template_dir = \
os.path.join(os.path.dirname(__file__), "templates", self.template_dir)
Path(__file__).resolve().parent / "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()
self._fill_rv_kernel_dir()
def __fill_rv_kernel_dir(self):
def _fill_rv_kernel_dir(self):
# find the kernel tree root relative to this file's location
resolved_path = Path(__file__).resolve()
if len(resolved_path.parents) > 4:
kernel_root = resolved_path.parents[4]
kernel_path = kernel_root / self.rv_dir
# first try if we are running in the kernel tree root
if os.path.exists(self.rv_dir):
return
if kernel_path.exists():
self.rv_dir = str(kernel_path)
return
# offset if we are running inside the kernel tree from verification/dot2
kernel_path = os.path.join("../..", self.rv_dir)
if os.path.exists(kernel_path):
self.rv_dir = kernel_path
# best effort if rvgen is installed and we are at the root of a kernel tree
if Path(self.rv_dir).exists():
return
if platform.system() != "Linux":
raise OSError("I can only run on Linux.")
kernel_path = os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
kernel_path = Path(f"/lib/modules/{platform.release()}/build") / self.rv_dir
# if the current kernel is from a distro this may not be a full kernel tree
# verify that one of the files we are going to modify is available
if os.path.exists(os.path.join(kernel_path, "rv_trace.h")):
self.rv_dir = kernel_path
if (kernel_path / "rv_trace.h").exists():
self.rv_dir = str(kernel_path)
return
raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
@@ -57,12 +59,12 @@ class RVGenerator:
def _read_template_file(self, file):
try:
path = os.path.join(self.abs_template_dir, file)
path = self.abs_template_dir / file
return self._read_file(path)
except OSError:
# 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)
path = self.abs_template_dir.parent / file
return self._read_file(path)
def fill_parent(self):
@@ -133,7 +135,7 @@ class RVGenerator:
def _patch_file(self, file, marker, line):
assert self.auto_patch
file_to_patch = os.path.join(self.rv_dir, file)
file_to_patch = Path(self.rv_dir) / file
content = self._read_file(file_to_patch)
content = content.replace(marker, line + "\n" + marker)
self.__write_file(file_to_patch, content)
@@ -187,22 +189,19 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
return f" - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
def __create_directory(self):
path = self.name
path = Path(self.name)
if self.auto_patch:
path = os.path.join(self.rv_dir, "monitors", path)
try:
os.mkdir(path)
except FileExistsError:
return
path = Path(self.rv_dir) / "monitors" / path
path.mkdir(exist_ok=True)
def __write_file(self, file_name, content):
with open(file_name, 'w') as file:
file.write(content)
def _create_file(self, file_name, content):
path = f"{self.name}/{file_name}"
path = Path(self.name) / file_name
if self.auto_patch:
path = os.path.join(self.rv_dir, "monitors", path)
path = Path(self.rv_dir) / "monitors" / self.name / file_name
self.__write_file(path, content)
def print_files(self):

194
tools/verification/rvgen/rvgen/kunit.py Normal file
View File

@@ -0,0 +1,194 @@
#!/usr/bin/env python3
# SPDX-License-Identifier: GPL-2.0-only
#
# Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com>
#
# Generator for runtime verification kunit files
import re
from pathlib import Path
from . import generator
class KUnitError(Exception):
"""Exception raised for errors in KUnit generation and file handling."""
class KUnit(generator.RVGenerator):
template_dir = ""
def __init__(self, extra_params={}):
super().__init__(extra_params)
self.local = extra_params.get("local", False)
self.kunit_c = self._read_template_file("kunit.c")
if not self.local:
self._fill_rv_kernel_dir()
try:
self.monitor_path = self.__find_monitor_c_file()
with open(self.monitor_path, 'r') as f:
self.content = f.read()
except OSError as e:
raise KUnitError(e) from e
self.monitor_class = self.__detect_monitor_class()
def _read_template_file(self, file):
if file in ("main.c", "Kconfig"):
return ""
return super()._read_template_file(file)
def __find_monitor_c_file(self) -> str:
"""Look for the monitor file in the kernel tree or in the current folder."""
if not self.local:
path = Path(self.rv_dir) / "monitors" / self.name / f"{self.name}.c"
if path.exists():
return str(path)
path = Path(self.name) / f"{self.name}.c"
if path.exists():
return str(path)
raise FileNotFoundError(f"Could not find monitor C file for '{self.name}'")
def __extract_function_args(self, handler_name: str) -> str:
pattern = re.compile(
r'^\s*(.*?)\b' + re.escape(handler_name) + r'\(([^)]*)\)',
re.MULTILINE | re.DOTALL
)
match = pattern.search(self.content)
if not match:
return "/* XXX: fill handlers argument. */"
return match.group(2).strip()
def __parse_attach_handlers(self) -> list[str]:
"""Find handlers by parsing when they are attached to tracepoints."""
probe_pattern = re.compile(
r'rv_attach_trace_probe\(.*, ([a-zA-Z0-9_]+)\)'
)
handlers = []
for match in probe_pattern.finditer(self.content):
handler = match.group(1)
if handler not in handlers:
handlers.append(handler)
return handlers
def __detect_monitor_class(self) -> str:
for c in ("da", "ha", "ltl"):
if f"{c}_monitor.h" in self.content:
return c
return "da"
def __fill_kunit_c(self, struct_name: str) -> str:
kunit_c = self.kunit_c
kunit_c = kunit_c.replace("%%MODEL_NAME%%", self.name)
kunit_c = kunit_c.replace("%%MODEL_NAME_UP%%", self.name.upper())
kunit_c = kunit_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
kunit_c = kunit_c.replace("%%STRUCT_NAME%%", struct_name)
return kunit_c
def __fill_kunit_h(self, struct_name, prototypes) -> str:
return f"""/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __{self.name.upper()}_KUNIT_H
#define __{self.name.upper()}_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct {struct_name} {{
\tstruct rv_kunit_mon mon;
\t{"\n\t".join(prototypes)}
}} {struct_name};
#endif
#endif /* __{self.name.upper()}_KUNIT_H */
"""
def __fill_monitor_handlers(self, struct_name, assignments):
struct_definition = f"""#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "{self.name}_kunit.h"
const struct {struct_name} {struct_name} = {{
\t.mon = RV_MON_OPS_INIT(),
\t{"\n\t".join(assignments)}
}};
EXPORT_SYMBOL_IF_KUNIT({struct_name});
#endif"""
if self.auto_patch:
try:
with open(self.monitor_path, 'w') as f:
f.write(f"{self.content}\n{struct_definition}\n")
except OSError as e:
raise KUnitError(f"Error patching monitor file {self.monitor_path}: {e}") from e
else:
print(f"Append the following to {self.name}.c:\n")
print(struct_definition)
print("Now complete the test and add it to rv_monitors_test.c")
def print_files(self):
handlers = self.__parse_attach_handlers()
if not handlers:
raise KUnitError(f"No handlers found in {self.monitor_path}")
prototypes = []
assignments = []
for handler in handlers:
arguments = self.__extract_function_args(handler)
prototypes.append(f"void (*{handler})({arguments});")
assignments.append(f".{handler} = {handler},")
struct_name = f"rv_{self.name}_ops"
self.__fill_monitor_handlers(struct_name, assignments)
dir_path = Path(self.monitor_path).parent
header_file_path = dir_path / f"{self.name}_kunit.h"
kunit_c_file_path = dir_path / f"{self.name}_kunit.c"
use_backup = True
if header_file_path.exists() or kunit_c_file_path.exists():
try:
response = input("KUnit file(s) already exist. Backup? [Y/n] ")
if response.strip().lower() in ("n", "no"):
use_backup = False
except EOFError:
print("Non-interactive session detected, backing up existing files.")
else:
use_backup = False
if use_backup:
for path in (header_file_path, kunit_c_file_path):
if path.exists():
try:
path.rename(path.with_suffix(path.suffix + ".bak"))
except OSError as e:
raise KUnitError(f"Error backing up file {path}: {e}") from e
header_content = self.__fill_kunit_h(struct_name, prototypes)
try:
with open(header_file_path, 'w') as f:
f.write(header_content)
print(f"Successfully created KUnit header file: {header_file_path}")
except OSError as e:
raise KUnitError(f"Error writing to file {header_file_path}: {e}") from e
kunit_c_content = self.__fill_kunit_c(struct_name)
try:
with open(kunit_c_file_path, 'w') as f:
f.write(kunit_c_content)
print(f"Successfully created KUnit C file: {kunit_c_file_path}")
except OSError as e:
raise KUnitError(f"Error writing to file {kunit_c_file_path}: {e}") from e

184
tools/verification/rvgen/rvgen/ltl2ba.py
View File

@@ -7,9 +7,7 @@
# https://doi.org/10.1007/978-0-387-34892-6_1
# With extra optimizations
from ply.lex import lex
from ply.yacc import yacc
from .automata import AutomataError
import lark
# Grammar:
# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -30,42 +28,41 @@ from .automata import AutomataError
# imply
# equivalent
tokens = (
'AND',
'OR',
'IMPLY',
'UNTIL',
'ALWAYS',
'EVENTUALLY',
'NEXT',
'VARIABLE',
'LITERAL',
'NOT',
'LPAREN',
'RPAREN',
'ASSIGN',
)
GRAMMAR = r'''
start: 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'
assign: VARIABLE "=" _ltl
def t_error(t):
raise AutomataError(f"Illegal character '{t.value[0]}'")
_ltl: _opd | binop | unop
lexer = lex()
_opd : VARIABLE
| LITERAL
| "(" _ltl ")"
unop: UNOP _ltl
UNOP: "always"
| "eventually"
| "next"
| "not"
binop: _opd BINOP _ltl
BINOP: "until"
| "and"
| "or"
| "imply"
VARIABLE: /[A-Z_][A-Z0-9_]*/
LITERAL: "true" | "false"
COMMENT: "#" /.*/ "\n"
%ignore COMMENT
%import common.WS
%ignore WS
'''
class LTLError(Exception):
"Exception raised for malformed linear temporal logic"
class GraphNode:
uid = 0
@@ -97,7 +94,7 @@ class GraphNode:
return self.id < other.id
class ASTNode:
uid = 1
uid = 0
def __init__(self, op):
self.op = op
@@ -433,90 +430,49 @@ class Literal:
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]]
class Transform(lark.visitors.Transformer):
def unop(self, node):
if node[0] == "always":
return ASTNode(AlwaysOp(node[1]))
if node[0] == "eventually":
return ASTNode(EventuallyOp(node[1]))
if node[0] == "next":
return ASTNode(NextOp(node[1]))
if node[0] == "not":
return ASTNode(NotOp(node[1]))
raise ValueError("Unknown operator %s" % node[0])
def p_assign(p):
'''
assign : VARIABLE ASSIGN ltl
'''
p[0] = (p[1], p[3])
def binop(self, node):
if node[1] == "until":
return ASTNode(UntilOp(node[0], node[2]))
if node[1] == "and":
return ASTNode(AndOp(node[0], node[2]))
if node[1] == "or":
return ASTNode(OrOp(node[0], node[2]))
if node[1] == "imply":
return ASTNode(ImplyOp(node[0], node[2]))
raise ValueError("Unknown operator %s" % node[1])
def p_ltl(p):
'''
ltl : opd
| binop
| unop
'''
p[0] = p[1]
def VARIABLE(self, args):
return ASTNode(Variable(args))
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 LITERAL(self, args):
return ASTNode(Literal(args == "true"))
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 AutomataError(f"Invalid unary operator {p[1]}")
def start(self, node):
return node
p[0] = ASTNode(op)
def assign(self, node):
return node[0].op.name, node[1]
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 AutomataError(f"Invalid binary operator {p[2]}")
p[0] = ASTNode(op)
parser = yacc()
parser = lark.Lark(GRAMMAR)
def parse_ltl(s: str) -> ASTNode:
spec = parser.parse(s)
try:
spec = parser.parse(s)
except lark.exceptions.UnexpectedInput as e:
raise LTLError(str(e))
spec = Transform().transform(spec)
rule = None
subexpr = {}
@@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode:
subexpr[assign[0]] = assign[1]
if rule is None:
raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format")
for node in rule:
if not isinstance(node.op, Variable):

2
tools/verification/rvgen/rvgen/ltl2k.py
View File

@@ -222,7 +222,7 @@ class ltl2k(generator.Monitor):
return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
def fill_tracepoint_detach_helper(self):
return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_sample_event);"
return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
def fill_atoms_init(self):
buff = []

2
tools/verification/rvgen/rvgen/templates/container/main.c
View File

@@ -31,5 +31,5 @@ module_init(register_%%MODEL_NAME%%);
module_exit(unregister_%%MODEL_NAME%%);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("dot2k: auto-generated");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");

2
tools/verification/rvgen/rvgen/templates/dot2k/main.c
View File

@@ -79,5 +79,5 @@ module_init(register_%%MODEL_NAME%%);
module_exit(unregister_%%MODEL_NAME%%);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("dot2k: auto-generated");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");

33
tools/verification/rvgen/rvgen/templates/kunit.c Normal file
View File

@@ -0,0 +1,33 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
/*
* XXX: include required headers, e.g.,
* #include <linux/sched.h>
*/
#include "%%MODEL_NAME%%_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%)
static void rv_test_%%MODEL_NAME%%(struct kunit *test)
{
struct rv_kunit_ctx *ctx = test->priv;
/*
* If you need to create task_structs with rv_kunit_alloc_mock_task()
* do it BEFORE preparing the test.
*/
prepare_test(test, &%%STRUCT_NAME%%.mon);
/*
* XXX: write the test here
* e.g.
* RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
* %%STRUCT_NAME%%.handle_event(args);
*/
}
#else
#define rv_test_%%MODEL_NAME%% rv_test_stub
#endif

8
tools/verification/rvgen/rvgen/templates/ltl2k/main.c
View File

@@ -77,7 +77,7 @@ static void disable_%%MODEL_NAME%%(void)
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_%%MODEL_NAME%% = {
static struct rv_monitor rv_this = {
.name = "%%MODEL_NAME%%",
.description = "%%DESCRIPTION%%",
.enable = enable_%%MODEL_NAME%%,
@@ -86,17 +86,17 @@ static struct rv_monitor rv_%%MODEL_NAME%% = {
static int __init register_%%MODEL_NAME%%(void)
{
return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%);
return rv_register_monitor(&rv_this, %%PARENT%%);
}
static void __exit unregister_%%MODEL_NAME%%(void)
{
rv_unregister_monitor(&rv_%%MODEL_NAME%%);
rv_unregister_monitor(&rv_this);
}
module_init(register_%%MODEL_NAME%%);
module_exit(unregister_%%MODEL_NAME%%);
MODULE_LICENSE("GPL");
MODULE_AUTHOR(/* TODO */);
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%");

9
tools/verification/rvgen/tests/golden/da_global/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_DA_GLOBAL
depends on RV
# XXX: add dependencies if there
select DA_MON_EVENTS_IMPLICIT
bool "da_global monitor"
help
auto-generated

95
tools/verification/rvgen/tests/golden/da_global/da_global.c Normal file
View File

@@ -0,0 +1,95 @@
// 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 "da_global"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_GLOBAL
#include "da_global.h"
#include <rv/da_monitor.h>
/*
* 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.
*
*/
static void handle_event_1(void *data, /* XXX: fill header */)
{
da_handle_event(event_1_da_global);
}
static void handle_event_2(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event always leads to the initial state */
da_handle_start_event(event_2_da_global);
}
static int enable_da_global(void)
{
int retval;
retval = da_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1);
rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2);
return 0;
}
static void disable_da_global(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1);
rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2);
da_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "da_global",
.description = "auto-generated",
.enable = enable_da_global,
.disable = disable_da_global,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_da_global(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_da_global(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_da_global);
module_exit(unregister_da_global);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("da_global: auto-generated");

47
tools/verification/rvgen/tests/golden/da_global/da_global.h Normal file
View File

@@ -0,0 +1,47 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Automatically generated C representation of da_global automaton
* For further information about this format, see kernel documentation:
* Documentation/trace/rv/deterministic_automata.rst
*/
#define MONITOR_NAME da_global
enum states_da_global {
state_a_da_global,
state_b_da_global,
state_max_da_global,
};
#define INVALID_STATE state_max_da_global
enum events_da_global {
event_1_da_global,
event_2_da_global,
event_max_da_global,
};
struct automaton_da_global {
char *state_names[state_max_da_global];
char *event_names[event_max_da_global];
unsigned char function[state_max_da_global][event_max_da_global];
unsigned char initial_state;
bool final_states[state_max_da_global];
};
static const struct automaton_da_global automaton_da_global = {
.state_names = {
"state_a",
"state_b",
},
.event_names = {
"event_1",
"event_2",
},
.function = {
{ state_b_da_global, state_a_da_global },
{ INVALID_STATE, state_a_da_global },
},
.initial_state = state_a_da_global,
.final_states = { 1, 0 },
};

15
tools/verification/rvgen/tests/golden/da_global/da_global_trace.h Normal file
View File

@@ -0,0 +1,15 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_DA_GLOBAL
DEFINE_EVENT(event_da_monitor, event_da_global,
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_da_global,
TP_PROTO(char *state, char *event),
TP_ARGS(state, event));
#endif /* CONFIG_RV_MON_DA_GLOBAL */

11
tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig Normal file
View File

@@ -0,0 +1,11 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_DA_PEROBJ_PARENT
depends on RV
# XXX: add dependencies if there
depends on RV_MON_PARENT_MON
default y
select DA_MON_EVENTS_ID
bool "da_perobj_parent monitor"
help
auto-generated

119
tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c Normal file
View File

@@ -0,0 +1,119 @@
// 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 "da_perobj_parent"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
#include <monitors/parent_mon/parent_mon.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_PER_OBJ
typedef /* XXX: define the target type */ *monitor_target;
#include "da_perobj_parent.h"
#include <rv/da_monitor.h>
/*
* 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.
*
*/
static void handle_event_1(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event is only valid in the initial state */
int id = /* XXX: how do I get the id? */;
monitor_target t = /* XXX: how do I get t? */;
da_handle_start_run_event(id, t, event_1_da_perobj_parent);
}
static void handle_event_2(void *data, /* XXX: fill header */)
{
int id = /* XXX: how do I get the id? */;
monitor_target t = /* XXX: how do I get t? */;
da_handle_event(id, t, event_2_da_perobj_parent);
}
static void handle_event_3(void *data, /* XXX: fill header */)
{
int id = /* XXX: how do I get the id? */;
monitor_target t = /* XXX: how do I get t? */;
da_handle_event(id, t, event_3_da_perobj_parent);
}
/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */
static void handle_obj_cleanup(void *data, /* XXX: fill header */)
{
int id = /* XXX: how do I get the id? */;
da_destroy_storage(id);
}
static int enable_da_perobj_parent(void)
{
int retval;
retval = da_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1);
rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2);
rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3);
rv_attach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup);
return 0;
}
static void disable_da_perobj_parent(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1);
rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2);
rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3);
rv_detach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup);
da_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "da_perobj_parent",
.description = "auto-generated",
.enable = enable_da_perobj_parent,
.disable = disable_da_perobj_parent,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_da_perobj_parent(void)
{
return rv_register_monitor(&rv_this, &rv_parent_mon);
}
static void __exit unregister_da_perobj_parent(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_da_perobj_parent);
module_exit(unregister_da_perobj_parent);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("da_perobj_parent: auto-generated");

64
tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h Normal file
View File

@@ -0,0 +1,64 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Automatically generated C representation of da_perobj_parent automaton
* For further information about this format, see kernel documentation:
* Documentation/trace/rv/deterministic_automata.rst
*/
#define MONITOR_NAME da_perobj_parent
enum states_da_perobj_parent {
state_a_da_perobj_parent,
state_b_da_perobj_parent,
state_c_da_perobj_parent,
state_max_da_perobj_parent,
};
#define INVALID_STATE state_max_da_perobj_parent
enum events_da_perobj_parent {
event_1_da_perobj_parent,
event_2_da_perobj_parent,
event_3_da_perobj_parent,
event_max_da_perobj_parent,
};
struct automaton_da_perobj_parent {
char *state_names[state_max_da_perobj_parent];
char *event_names[event_max_da_perobj_parent];
unsigned char function[state_max_da_perobj_parent][event_max_da_perobj_parent];
unsigned char initial_state;
bool final_states[state_max_da_perobj_parent];
};
static const struct automaton_da_perobj_parent automaton_da_perobj_parent = {
.state_names = {
"state_a",
"state_b",
"state_c",
},
.event_names = {
"event_1",
"event_2",
"event_3",
},
.function = {
{
state_b_da_perobj_parent,
state_c_da_perobj_parent,
INVALID_STATE,
},
{
INVALID_STATE,
state_a_da_perobj_parent,
state_c_da_perobj_parent,
},
{
INVALID_STATE,
INVALID_STATE,
INVALID_STATE,
},
},
.initial_state = state_a_da_perobj_parent,
.final_states = { 1, 0, 0 },
};

15
tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h Normal file
View File

@@ -0,0 +1,15 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_DA_PEROBJ_PARENT
DEFINE_EVENT(event_da_monitor_id, event_da_perobj_parent,
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_da_perobj_parent,
TP_PROTO(int id, char *state, char *event),
TP_ARGS(id, state, event));
#endif /* CONFIG_RV_MON_DA_PEROBJ_PARENT */

9
tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_DA_PERTASK_DESC
depends on RV
# XXX: add dependencies if there
select DA_MON_EVENTS_ID
bool "da_pertask_desc monitor"
help
Custom description for testing

105
tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c Normal file
View File

@@ -0,0 +1,105 @@
// 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 "da_pertask_desc"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_PER_TASK
#include "da_pertask_desc.h"
#include <rv/da_monitor.h>
/*
* 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.
*
*/
static void handle_event_1(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event is only valid in the initial state */
struct task_struct *p = /* XXX: how do I get p? */;
da_handle_start_run_event(p, event_1_da_pertask_desc);
}
static void handle_event_2(void *data, /* XXX: fill header */)
{
struct task_struct *p = /* XXX: how do I get p? */;
da_handle_event(p, event_2_da_pertask_desc);
}
static void handle_event_3(void *data, /* XXX: fill header */)
{
struct task_struct *p = /* XXX: how do I get p? */;
da_handle_event(p, event_3_da_pertask_desc);
}
static int enable_da_pertask_desc(void)
{
int retval;
retval = da_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1);
rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2);
rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3);
return 0;
}
static void disable_da_pertask_desc(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1);
rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2);
rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3);
da_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "da_pertask_desc",
.description = "Custom description for testing",
.enable = enable_da_pertask_desc,
.disable = disable_da_pertask_desc,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_da_pertask_desc(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_da_pertask_desc(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_da_pertask_desc);
module_exit(unregister_da_pertask_desc);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("da_pertask_desc: Custom description for testing");

64
tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h Normal file
View File

@@ -0,0 +1,64 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Automatically generated C representation of da_pertask_desc automaton
* For further information about this format, see kernel documentation:
* Documentation/trace/rv/deterministic_automata.rst
*/
#define MONITOR_NAME da_pertask_desc
enum states_da_pertask_desc {
state_a_da_pertask_desc,
state_b_da_pertask_desc,
state_c_da_pertask_desc,
state_max_da_pertask_desc,
};
#define INVALID_STATE state_max_da_pertask_desc
enum events_da_pertask_desc {
event_1_da_pertask_desc,
event_2_da_pertask_desc,
event_3_da_pertask_desc,
event_max_da_pertask_desc,
};
struct automaton_da_pertask_desc {
char *state_names[state_max_da_pertask_desc];
char *event_names[event_max_da_pertask_desc];
unsigned char function[state_max_da_pertask_desc][event_max_da_pertask_desc];
unsigned char initial_state;
bool final_states[state_max_da_pertask_desc];
};
static const struct automaton_da_pertask_desc automaton_da_pertask_desc = {
.state_names = {
"state_a",
"state_b",
"state_c",
},
.event_names = {
"event_1",
"event_2",
"event_3",
},
.function = {
{
state_b_da_pertask_desc,
state_c_da_pertask_desc,
INVALID_STATE,
},
{
INVALID_STATE,
state_a_da_pertask_desc,
state_c_da_pertask_desc,
},
{
INVALID_STATE,
INVALID_STATE,
INVALID_STATE,
},
},
.initial_state = state_a_da_pertask_desc,
.final_states = { 1, 0, 0 },
};

15
tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h Normal file
View File

@@ -0,0 +1,15 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_DA_PERTASK_DESC
DEFINE_EVENT(event_da_monitor_id, event_da_pertask_desc,
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_da_pertask_desc,
TP_PROTO(int id, char *state, char *event),
TP_ARGS(id, state, event));
#endif /* CONFIG_RV_MON_DA_PERTASK_DESC */

9
tools/verification/rvgen/tests/golden/ha_percpu/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_HA_PERCPU
depends on RV
# XXX: add dependencies if there
select HA_MON_EVENTS_IMPLICIT
bool "ha_percpu monitor"
help
auto-generated

227
tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c Normal file
View File

@@ -0,0 +1,227 @@
// 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 "ha_percpu"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_PER_CPU
/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
#define HA_TIMER_TYPE HA_TIMER_HRTIMER
#include "ha_percpu.h"
#include <rv/ha_monitor.h>
/*
* 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.
*
*/
#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
#define FOO_NS /* XXX: what is FOO_NS? */
static inline u64 bar_ns(struct ha_monitor *ha_mon)
{
return /* XXX: what is bar_ns(ha_mon)? */;
}
static u64 foo_ns = /* XXX: default value */;
module_param(foo_ns, ullong, 0644);
/*
* These functions define how to read and reset the environment variable.
*
* Common environment variables like ns-based and jiffy-based clocks have
* pre-define getters and resetters you can use. The parser can infer the type
* of the environment variable if you supply a measure unit in the constraint.
* If you define your own functions, make sure to add appropriate memory
* barriers if required.
* Some environment variables don't require a storage as they read a system
* state (e.g. preemption count). Those variables are never reset, so we don't
* define a reset function on monitors only relying on this type of variables.
*/
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
{
if (env == clk_ha_percpu)
return ha_get_clk_ns(ha_mon, env, time_ns);
else if (env == env1_ha_percpu)
return /* XXX: how do I read env1? */
else if (env == env2_ha_percpu)
return /* XXX: how do I read env2? */
return ENV_INVALID_VALUE;
}
static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns)
{
if (env == clk_ha_percpu)
ha_reset_clk_ns(ha_mon, env, time_ns);
}
/*
* These functions are used to validate state transitions.
*
* They are generated by parsing the model, there is usually no need to change them.
* If the monitor requires a timer, there are functions responsible to arm it when
* the next state has a constraint, cancel it in any other case and to check
* that it didn't expire before the callback run. Transitions to the same state
* without a reset never affect timers.
*/
static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
{
if (curr_state == S0_ha_percpu)
return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon));
else if (curr_state == S2_ha_percpu)
return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon));
return true;
}
static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
{
bool res = true;
if (curr_state == S0_ha_percpu && event == event0_ha_percpu)
ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
else if (curr_state == S0_ha_percpu && event == event1_ha_percpu)
ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
else if (curr_state == S1_ha_percpu && event == event0_ha_percpu)
ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) {
res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull;
ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
} else if (curr_state == S2_ha_percpu && event == event1_ha_percpu)
res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns;
else if (curr_state == S3_ha_percpu && event == event0_ha_percpu)
res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
(ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS &&
ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull);
else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) {
res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) ||
(ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull &&
ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull);
ha_reset_env(ha_mon, clk_ha_percpu, time_ns);
}
return res;
}
static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
{
if (next_state == curr_state && event != event0_ha_percpu)
return;
if (next_state == S0_ha_percpu)
ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns);
else if (next_state == S2_ha_percpu)
ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns);
else if (curr_state == S0_ha_percpu)
ha_cancel_timer(ha_mon);
else if (curr_state == S2_ha_percpu)
ha_cancel_timer(ha_mon);
}
static bool ha_verify_constraint(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
{
if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
return false;
if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
return false;
ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
return true;
}
static void handle_event0(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event always leads to the initial state */
da_handle_start_event(event0_ha_percpu);
}
static void handle_event1(void *data, /* XXX: fill header */)
{
da_handle_event(event1_ha_percpu);
}
static void handle_event2(void *data, /* XXX: fill header */)
{
da_handle_event(event2_ha_percpu);
}
static int enable_ha_percpu(void)
{
int retval;
retval = ha_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
return 0;
}
static void disable_ha_percpu(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0);
rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1);
rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2);
ha_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "ha_percpu",
.description = "auto-generated",
.enable = enable_ha_percpu,
.disable = disable_ha_percpu,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_ha_percpu(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_ha_percpu(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_ha_percpu);
module_exit(unregister_ha_percpu);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("ha_percpu: auto-generated");

72
tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h Normal file
View File

@@ -0,0 +1,72 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Automatically generated C representation of ha_percpu automaton
* For further information about this format, see kernel documentation:
* Documentation/trace/rv/deterministic_automata.rst
*/
#define MONITOR_NAME ha_percpu
enum states_ha_percpu {
S0_ha_percpu,
S1_ha_percpu,
S2_ha_percpu,
S3_ha_percpu,
state_max_ha_percpu,
};
#define INVALID_STATE state_max_ha_percpu
enum events_ha_percpu {
event0_ha_percpu,
event1_ha_percpu,
event2_ha_percpu,
event_max_ha_percpu,
};
enum envs_ha_percpu {
clk_ha_percpu,
env1_ha_percpu,
env2_ha_percpu,
env_max_ha_percpu,
env_max_stored_ha_percpu = env1_ha_percpu,
};
_Static_assert(env_max_stored_ha_percpu <= MAX_HA_ENV_LEN, "Not enough slots");
#define HA_CLK_NS
struct automaton_ha_percpu {
char *state_names[state_max_ha_percpu];
char *event_names[event_max_ha_percpu];
char *env_names[env_max_ha_percpu];
unsigned char function[state_max_ha_percpu][event_max_ha_percpu];
unsigned char initial_state;
bool final_states[state_max_ha_percpu];
};
static const struct automaton_ha_percpu automaton_ha_percpu = {
.state_names = {
"S0",
"S1",
"S2",
"S3",
},
.event_names = {
"event0",
"event1",
"event2",
},
.env_names = {
"clk",
"env1",
"env2",
},
.function = {
{ S0_ha_percpu, S1_ha_percpu, INVALID_STATE },
{ S0_ha_percpu, INVALID_STATE, S2_ha_percpu },
{ INVALID_STATE, S2_ha_percpu, S3_ha_percpu },
{ S0_ha_percpu, S1_ha_percpu, INVALID_STATE },
},
.initial_state = S0_ha_percpu,
.final_states = { 1, 0, 0, 0 },
};

19
tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h Normal file
View File

@@ -0,0 +1,19 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_HA_PERCPU
DEFINE_EVENT(event_da_monitor, event_ha_percpu,
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_ha_percpu,
TP_PROTO(char *state, char *event),
TP_ARGS(state, event));
DEFINE_EVENT(error_env_da_monitor, error_env_ha_percpu,
TP_PROTO(char *state, char *event, char *env),
TP_ARGS(state, event, env));
#endif /* CONFIG_RV_MON_HA_PERCPU */

9
tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_LTL_PERTASK
depends on RV
# XXX: add dependencies if there
select LTL_MON_EVENTS_ID
bool "ltl_pertask monitor"
help
auto-generated

107
tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c Normal file
View File

@@ -0,0 +1,107 @@
// 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 "ltl_pertask"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#include "ltl_pertask.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.
*/
ltl_atom_set(mon, LTL_EVENT_A, true/false);
ltl_atom_set(mon, LTL_EVENT_B, true/false);
}
/*
* 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.
*/
static void handle_example_event(void *data, /* XXX: fill header */)
{
ltl_atom_update(task, LTL_EVENT_A, true/false);
}
static int enable_ltl_pertask(void)
{
int retval;
retval = ltl_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event);
return 0;
}
static void disable_ltl_pertask(void)
{
rv_detach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event);
ltl_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "ltl_pertask",
.description = "auto-generated",
.enable = enable_ltl_pertask,
.disable = disable_ltl_pertask,
};
static int __init register_ltl_pertask(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_ltl_pertask(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_ltl_pertask);
module_exit(unregister_ltl_pertask);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("ltl_pertask: auto-generated");

108
tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h Normal file
View File

@@ -0,0 +1,108 @@
/* 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 ltl_pertask
enum ltl_atom {
LTL_EVENT_A,
LTL_EVENT_B,
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[] = {
"ev_a",
"ev_b",
};
return names[atom];
}
enum ltl_buchi_state {
S0,
S1,
S2,
S3,
S4,
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 event_b = test_bit(LTL_EVENT_B, mon->atoms);
bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
bool val1 = !event_a;
if (val1)
__set_bit(S0, mon->states);
if (true)
__set_bit(S1, mon->states);
if (event_b)
__set_bit(S4, mon->states);
}
static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
bool val1 = !event_a;
switch (state) {
case S0:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
case S1:
if (true)
__set_bit(S1, next);
if (true && val1)
__set_bit(S2, next);
if (event_b && val1)
__set_bit(S3, next);
if (event_b)
__set_bit(S4, next);
break;
case S2:
if (true)
__set_bit(S1, next);
if (true && val1)
__set_bit(S2, next);
if (event_b && val1)
__set_bit(S3, next);
if (event_b)
__set_bit(S4, next);
break;
case S3:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
case S4:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
}
}

14
tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h Normal file
View File

@@ -0,0 +1,14 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_LTL_PERTASK
DEFINE_EVENT(event_ltl_monitor_id, event_ltl_pertask,
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_ltl_pertask,
TP_PROTO(struct task_struct *task),
TP_ARGS(task));
#endif /* CONFIG_RV_MON_LTL_PERTASK */

9
tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_TEST_BAK_KUNIT
depends on RV
# XXX: add dependencies if there
select LTL_MON_EVENTS_ID
bool "test_bak_kunit monitor"
help
auto-generated

107
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c Normal file
View File

@@ -0,0 +1,107 @@
// 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 "test_bak_kunit"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#include "test_bak_kunit.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.
*/
ltl_atom_set(mon, LTL_EVENT_A, true/false);
ltl_atom_set(mon, LTL_EVENT_B, true/false);
}
/*
* 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.
*/
static void handle_example_event(void *data, /* XXX: fill header */)
{
ltl_atom_update(task, LTL_EVENT_A, true/false);
}
static int enable_test_bak_kunit(void)
{
int retval;
retval = ltl_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
return 0;
}
static void disable_test_bak_kunit(void)
{
rv_detach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
ltl_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "test_bak_kunit",
.description = "auto-generated",
.enable = enable_test_bak_kunit,
.disable = disable_test_bak_kunit,
};
static int __init register_test_bak_kunit(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_test_bak_kunit(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_test_bak_kunit);
module_exit(unregister_test_bak_kunit);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("test_bak_kunit: auto-generated");

108
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h Normal file
View File

@@ -0,0 +1,108 @@
/* 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 test_bak_kunit
enum ltl_atom {
LTL_EVENT_A,
LTL_EVENT_B,
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[] = {
"ev_a",
"ev_b",
};
return names[atom];
}
enum ltl_buchi_state {
S0,
S1,
S2,
S3,
S4,
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 event_b = test_bit(LTL_EVENT_B, mon->atoms);
bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
bool val1 = !event_a;
if (val1)
__set_bit(S0, mon->states);
if (true)
__set_bit(S1, mon->states);
if (event_b)
__set_bit(S4, mon->states);
}
static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
bool val1 = !event_a;
switch (state) {
case S0:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
case S1:
if (true)
__set_bit(S1, next);
if (true && val1)
__set_bit(S2, next);
if (event_b && val1)
__set_bit(S3, next);
if (event_b)
__set_bit(S4, next);
break;
case S2:
if (true)
__set_bit(S1, next);
if (true && val1)
__set_bit(S2, next);
if (event_b && val1)
__set_bit(S3, next);
if (event_b)
__set_bit(S4, next);
break;
case S3:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
case S4:
if (val1)
__set_bit(S0, next);
if (true)
__set_bit(S1, next);
if (event_b)
__set_bit(S4, next);
break;
}
}

33
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c Normal file
View File

@@ -0,0 +1,33 @@
// SPDX-License-Identifier: GPL-2.0
#include <linux/kernel.h>
#include <linux/rv.h>
#include <rv/kunit.h>
/*
* XXX: include required headers, e.g.,
* #include <linux/sched.h>
*/
#include "test_bak_kunit_kunit.h"
#if IS_REACHABLE(CONFIG_RV_MON_TEST_BAK_KUNIT)
static void rv_test_test_bak_kunit(struct kunit *test)
{
struct rv_kunit_ctx *ctx = test->priv;
/*
* If you need to create task_structs with rv_kunit_alloc_mock_task()
* do it BEFORE preparing the test.
*/
prepare_test(test, &rv_test_bak_kunit_ops.mon);
/*
* XXX: write the test here
* e.g.
* RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
* rv_test_bak_kunit_ops.handle_event(args);
*/
}
#else
#define rv_test_test_bak_kunit rv_test_stub
#endif

1
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.bak Normal file
View File

@@ -0,0 +1 @@
DUMMY

22
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h Normal file
View File

@@ -0,0 +1,22 @@
/* SPDX-License-Identifier: GPL-2.0-only */
/*
* Automatically generated by rvgen kunit.
* May need manual intervention for function prototypes that couldn't be
* found (e.g. are in another file) or variables to be exported.
*/
#ifndef __TEST_BAK_KUNIT_KUNIT_H
#define __TEST_BAK_KUNIT_KUNIT_H
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <linux/rv.h>
#include <rv/kunit.h>
extern const struct rv_test_bak_kunit_ops {
struct rv_kunit_mon mon;
void (*handle_example_event)(void *data, /* XXX: fill header */);
} rv_test_bak_kunit_ops;
#endif
#endif /* __TEST_BAK_KUNIT_KUNIT_H */

14
tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h Normal file
View File

@@ -0,0 +1,14 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_TEST_BAK_KUNIT
DEFINE_EVENT(event_ltl_monitor_id, event_test_bak_kunit,
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_test_bak_kunit,
TP_PROTO(struct task_struct *task),
TP_ARGS(task));
#endif /* CONFIG_RV_MON_TEST_BAK_KUNIT */

5
tools/verification/rvgen/tests/golden/test_container/Kconfig Normal file
View File

@@ -0,0 +1,5 @@
config RV_MON_TEST_CONTAINER
depends on RV
bool "test_container monitor"
help
Test container for grouping monitors

35
tools/verification/rvgen/tests/golden/test_container/test_container.c Normal file
View File

@@ -0,0 +1,35 @@
// 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 "test_container"
#include "test_container.h"
struct rv_monitor rv_test_container = {
.name = "test_container",
.description = "Test container for grouping monitors",
.enable = NULL,
.disable = NULL,
.reset = NULL,
.enabled = 0,
};
static int __init register_test_container(void)
{
return rv_register_monitor(&rv_test_container, NULL);
}
static void __exit unregister_test_container(void)
{
rv_unregister_monitor(&rv_test_container);
}
module_init(register_test_container);
module_exit(unregister_test_container);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("test_container: Test container for grouping monitors");

3
tools/verification/rvgen/tests/golden/test_container/test_container.h Normal file
View File

@@ -0,0 +1,3 @@
/* SPDX-License-Identifier: GPL-2.0 */
extern struct rv_monitor rv_test_container;

9
tools/verification/rvgen/tests/golden/test_da/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_TEST_DA
depends on RV
# XXX: add dependencies if there
select DA_MON_EVENTS_IMPLICIT
bool "test_da monitor"
help
auto-generated

95
tools/verification/rvgen/tests/golden/test_da/test_da.c Normal file
View File

@@ -0,0 +1,95 @@
// 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 "test_da"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_PER_CPU
#include "test_da.h"
#include <rv/da_monitor.h>
/*
* 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.
*
*/
static void handle_event_1(void *data, /* XXX: fill header */)
{
da_handle_event(event_1_test_da);
}
static void handle_event_2(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event always leads to the initial state */
da_handle_start_event(event_2_test_da);
}
static int enable_test_da(void)
{
int retval;
retval = da_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1);
rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2);
return 0;
}
static void disable_test_da(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1);
rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2);
da_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "test_da",
.description = "auto-generated",
.enable = enable_test_da,
.disable = disable_test_da,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_test_da(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_test_da(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_test_da);
module_exit(unregister_test_da);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("test_da: auto-generated");

47
tools/verification/rvgen/tests/golden/test_da/test_da.h Normal file
View File

@@ -0,0 +1,47 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Automatically generated C representation of test_da automaton
* For further information about this format, see kernel documentation:
* Documentation/trace/rv/deterministic_automata.rst
*/
#define MONITOR_NAME test_da
enum states_test_da {
state_a_test_da,
state_b_test_da,
state_max_test_da,
};
#define INVALID_STATE state_max_test_da
enum events_test_da {
event_1_test_da,
event_2_test_da,
event_max_test_da,
};
struct automaton_test_da {
char *state_names[state_max_test_da];
char *event_names[event_max_test_da];
unsigned char function[state_max_test_da][event_max_test_da];
unsigned char initial_state;
bool final_states[state_max_test_da];
};
static const struct automaton_test_da automaton_test_da = {
.state_names = {
"state_a",
"state_b",
},
.event_names = {
"event_1",
"event_2",
},
.function = {
{ state_b_test_da, state_a_test_da },
{ INVALID_STATE, state_a_test_da },
},
.initial_state = state_a_test_da,
.final_states = { 1, 0 },
};

15
tools/verification/rvgen/tests/golden/test_da/test_da_trace.h Normal file
View File

@@ -0,0 +1,15 @@
/* SPDX-License-Identifier: GPL-2.0 */
/*
* Snippet to be included in rv_trace.h
*/
#ifdef CONFIG_RV_MON_TEST_DA
DEFINE_EVENT(event_da_monitor, event_test_da,
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_test_da,
TP_PROTO(char *state, char *event),
TP_ARGS(state, event));
#endif /* CONFIG_RV_MON_TEST_DA */

9
tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig Normal file
View File

@@ -0,0 +1,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
config RV_MON_TEST_DA_KUNIT
depends on RV
# XXX: add dependencies if there
select DA_MON_EVENTS_IMPLICIT
bool "test_da_kunit monitor"
help
auto-generated

107
tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c Normal file
View File

@@ -0,0 +1,107 @@
// 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 "test_da_kunit"
/*
* XXX: include required tracepoint headers, e.g.,
* #include <trace/events/sched.h>
*/
#include <rv_trace.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
* to touch this section.
*/
#define RV_MON_TYPE RV_MON_PER_CPU
#include "test_da_kunit.h"
#include <rv/da_monitor.h>
/*
* 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.
*
*/
static void handle_event_1(void *data, /* XXX: fill header */)
{
da_handle_event(event_1_test_da_kunit);
}
static void handle_event_2(void *data, /* XXX: fill header */)
{
/* XXX: validate that this event always leads to the initial state */
da_handle_start_event(event_2_test_da_kunit);
}
static int enable_test_da_kunit(void)
{
int retval;
retval = da_monitor_init();
if (retval)
return retval;
rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
return 0;
}
static void disable_test_da_kunit(void)
{
rv_this.enabled = 0;
rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
da_monitor_destroy();
}
/*
* This is the monitor register section.
*/
static struct rv_monitor rv_this = {
.name = "test_da_kunit",
.description = "auto-generated",
.enable = enable_test_da_kunit,
.disable = disable_test_da_kunit,
.reset = da_monitor_reset_all,
.enabled = 0,
};
static int __init register_test_da_kunit(void)
{
return rv_register_monitor(&rv_this, NULL);
}
static void __exit unregister_test_da_kunit(void)
{
rv_unregister_monitor(&rv_this);
}
module_init(register_test_da_kunit);
module_exit(unregister_test_da_kunit);
MODULE_LICENSE("GPL");
MODULE_AUTHOR("rvgen: auto-generated");
MODULE_DESCRIPTION("test_da_kunit: auto-generated");
#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
#include <kunit/visibility.h>
#include "test_da_kunit_kunit.h"
const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = {
.mon = RV_MON_OPS_INIT(),
.handle_event_1 = handle_event_1,
.handle_event_2 = handle_event_2,
};
EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops);
#endif

Some files were not shown because too many files have changed in this diff Show More