lastdragon/linux-kernel
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Resguardo inicial

Browse Source
This commit is contained in:
lastdragon
2026-09-06 12:53:21 -06:00
parent 662efe3c2a
commit ad2088d178
94853 changed files with 43200404 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
linux-7.2.3/Documentation/trace/rv/da_monitor_instrumentation.rst
+171
View File
@@ -0,0 +1,171 @@
Deterministic Automata Instrumentation
======================================
The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
includes a section dedicated to instrumentation.
In the example of the wip.dot monitor created on [1], it will look like::
/*
* 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_preempt_disable(void *data, /* XXX: fill header */)
{
da_handle_event_wip(preempt_disable_wip);
}
static void handle_preempt_enable(void *data, /* XXX: fill header */)
{
da_handle_event_wip(preempt_enable_wip);
}
static void handle_sched_waking(void *data, /* XXX: fill header */)
{
da_handle_event_wip(sched_waking_wip);
}
static int enable_wip(void)
{
int retval;
retval = da_monitor_init_wip();
if (retval)
return retval;
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
return 0;
}
The comment at the top of the section explains the general idea: the
instrumentation section translates *kernel events* into the *model's
event*.
Tracing callback functions
--------------------------
The first three functions are the starting point of the callback *handler
functions* for each of the three events from the wip model. The developer
does not necessarily need to use them: they are just starting points.
Using the example of::
void handle_preempt_disable(void *data, /* XXX: fill header */)
{
da_handle_event_wip(preempt_disable_wip);
}
The preempt_disable event from the model connects directly to the
preemptirq:preempt_disable. The preemptirq:preempt_disable event
has the following signature, from include/trace/events/preemptirq.h::
TP_PROTO(unsigned long ip, unsigned long parent_ip)
Hence, the handle_preempt_disable() function will look like::
void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
In this case, the kernel event translates one to one with the automata
event, and indeed, no other change is required for this function.
The next handler function, handle_preempt_enable() has the same argument
list from the handle_preempt_disable(). The difference is that the
preempt_enable event will be used to synchronize the system to the model.
Initially, the *model* is placed in the initial state. However, the *system*
might or might not be in the initial state. The monitor cannot start
processing events until it knows that the system has reached the initial state.
Otherwise, the monitor and the system could be out-of-sync.
Looking at the automata definition, it is possible to see that the system
and the model are expected to return to the initial state after the
preempt_enable execution. Hence, it can be used to synchronize the
system and the model at the initialization of the monitoring section.
The start is informed via a special handle function, the
"da_handle_start_event_$(MONITOR_NAME)(event)", in this case::
da_handle_start_event_wip(preempt_enable_wip);
So, the callback function will look like::
void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
{
da_handle_start_event_wip(preempt_enable_wip);
}
Finally, the "handle_sched_waking()" will look like::
void handle_sched_waking(void *data, struct task_struct *task)
{
da_handle_event_wip(sched_waking_wip);
}
And the explanation is left for the reader as an exercise.
enable and disable functions
----------------------------
dot2k automatically creates two special functions::
enable_$(MONITOR_NAME)()
disable_$(MONITOR_NAME)()
These functions are called when the monitor is enabled and disabled,
respectively.
They should be used to *attach* and *detach* the instrumentation to the running
system. The developer must add to the relative function all that is needed to
*attach* and *detach* its monitor to the system.
For the wip case, these functions were named::
enable_wip()
disable_wip()
But no change was required because: by default, these functions *attach* and
*detach* the tracepoints_to_attach, which was enough for this case.
Instrumentation helpers
-----------------------
To complete the instrumentation, the *handler functions* need to be attached to a
kernel event, at the monitoring enable phase.
The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
is used to connect the wip model events to the relative kernel event. dot2k automatically
adds "rv_attach_trace_probe()" function call for each model event in the enable phase, as
a suggestion.
For example, from the wip sample model::
static int enable_wip(void)
{
int retval;
retval = da_monitor_init_wip();
if (retval)
return retval;
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
return 0;
}
The probes then need to be detached at the disable phase.
[1] The wip model is presented in:
Documentation/trace/rv/deterministic_automata.rst
The wip monitor is presented in:
Documentation/trace/rv/monitor_synthesis.rst
linux-7.2.3/Documentation/trace/rv/deterministic_automata.rst
+184
View File
@@ -0,0 +1,184 @@
Deterministic Automata
======================
Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
*G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
where:
- *X* is the set of states;
- *E* is the finite set of events;
- x\ :subscript:`0` is the initial state;
- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
- *f* : *X* x *E* -> *X* is the transition function. It defines the state
transition in the occurrence of an event from *E* in the state *X*. In the
special case of deterministic automata, the occurrence of the event in *E*
in a state in *X* has a deterministic next state from *X*.
For example, a given automaton named 'wip' (wakeup in preemptive) can
be defined as:
- *X* = { ``preemptive``, ``non_preemptive``}
- *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
- x\ :subscript:`0` = ``preemptive``
- X\ :subscript:`m` = {``preemptive``}
- *f* =
- *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
- *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
- *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
One of the benefits of this formal definition is that it can be presented
in multiple formats. For example, using a *graphical representation*, using
vertices (nodes) and edges, which is very intuitive for *operating system*
practitioners, without any loss.
The previous 'wip' automaton can also be represented as::
preempt_enable
+---------------------------------+
v |
#============# preempt_disable +------------------+
--> H preemptive H -----------------> | non_preemptive |
#============# +------------------+
^ |
| sched_waking |
+--------------+
Deterministic Automaton in C
----------------------------
In the paper "Efficient formal verification for the Linux kernel",
the authors present a simple way to represent an automaton in C that can
be used as regular code in the Linux kernel.
For example, the 'wip' automata can be presented as (augmented with comments)::
/* enum representation of X (set of states) to be used as index */
enum states {
preemptive = 0,
non_preemptive,
state_max
};
#define INVALID_STATE state_max
/* enum representation of E (set of events) to be used as index */
enum events {
preempt_disable = 0,
preempt_enable,
sched_waking,
event_max
};
struct automaton {
char *state_names[state_max]; // X: the set of states
char *event_names[event_max]; // E: the finite set of events
unsigned char function[state_max][event_max]; // f: transition function
unsigned char initial_state; // x_0: the initial state
bool final_states[state_max]; // X_m: the set of marked states
};
struct automaton aut = {
.state_names = {
"preemptive",
"non_preemptive"
},
.event_names = {
"preempt_disable",
"preempt_enable",
"sched_waking"
},
.function = {
{ non_preemptive, INVALID_STATE, INVALID_STATE },
{ INVALID_STATE, preemptive, non_preemptive },
},
.initial_state = preemptive,
.final_states = { 1, 0 },
};
The *transition function* is represented as a matrix of states (lines) and
events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
in O(1). For example::
next_state = automaton_wip.function[curr_state][event];
Graphviz .dot format
--------------------
The Graphviz open-source tool can produce the graphical representation
of an automaton using the (textual) DOT language as the source code.
The DOT format is widely used and can be converted to many other formats.
For example, this is the 'wip' model in DOT::
digraph state_automaton {
{node [shape = circle] "non_preemptive"};
{node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
{node [shape = doublecircle] "preemptive"};
{node [shape = circle] "preemptive"};
"__init_preemptive" -> "preemptive";
"non_preemptive" [label = "non_preemptive"];
"non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
"non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
"preemptive" [label = "preemptive"];
"preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
{ rank = min ;
"__init_preemptive";
"preemptive";
}
}
This DOT format can be transformed into a bitmap or vectorial image
using the dot utility, or into an ASCII art using graph-easy. For
instance::
$ dot -Tsvg -o wip.svg wip.dot
$ graph-easy wip.dot > wip.txt
dot2c
-----
dot2c is a utility that can parse a .dot file containing an automaton as
in the example above and automatically convert it to the C representation
presented in [3].
For example, having the previous 'wip' model into a file named 'wip.dot',
the following command will transform the .dot file into the C
representation (previously shown) in the 'wip.h' file::
$ dot2c wip.dot > wip.h
The 'wip.h' content is the code sample in section 'Deterministic Automaton
in C'.
Remarks
-------
The automata formalism allows modeling discrete event systems (DES) in
multiple formats, suitable for different applications/users.
For example, the formal description using set theory is better suitable
for automata operations, while the graphical format for human interpretation;
and computer languages for machine execution.
References
----------
Many textbooks cover automata formalism. For a brief introduction see::
O'Regan, Gerard. Concise guide to software engineering. Springer,
Cham, 2017.
For a detailed description, including operations, and application on Discrete
Event Systems (DES), see::
Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
event systems. Boston, MA: Springer US, 2008.
For the C representation in kernel, see::
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
Silva. Efficient formal verification for the Linux kernel. In:
International Conference on Software Engineering and Formal Methods.
Springer, Cham, 2019. p. 315-332.
linux-7.2.3/Documentation/trace/rv/hybrid_automata.rst
+341
View File
@@ -0,0 +1,341 @@
Hybrid Automata
===============
Hybrid automata are an extension of deterministic automata, there are several
definitions of hybrid automata in the literature. The adaptation implemented
here is formally denoted by G and defined as a 7-tuple:
*G* = { *X*, *E*, *V*, *f*, x\ :subscript:`0`, X\ :subscript:`m`, *i* }
- *X* is the set of states;
- *E* is the finite set of events;
- *V* is the finite set of environment variables;
- x\ :subscript:`0` is the initial state;
- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
- *f* : *X* x *E* x *C(V)* -> *X* is the transition function.
It defines the state transition in the occurrence of an event from *E* in the
state *X*. Unlike deterministic automata, the transition function also
includes guards from the set of all possible constraints (defined as *C(V)*).
Guards can be true or false with the valuation of *V* when the event occurs,
and the transition is possible only when constraints are true. Similarly to
deterministic automata, the occurrence of the event in *E* in a state in *X*
has a deterministic next state from *X*, if the guard is true.
- *i* : *X* -> *C'(V)* is the invariant assignment function, this is a
constraint assigned to each state in *X*, every state in *X* must be left
before the invariant turns to false. We can omit the representation of
invariants whose value is true regardless of the valuation of *V*.
The set of all possible constraints *C(V)* is defined according to the
following grammar:
g = v < c | v > c | v <= c | v >= c | v == c | v != c | g && g | true
With v a variable in *V* and c a numerical value.
We define the special case of hybrid automata whose variables grow with uniform
rates as timed automata. In this case, the variables are called clocks.
As the name implies, timed automata can be used to describe real time.
Additionally, clocks support another type of guard which always evaluates to true:
reset(v)
The reset constraint is used to set the value of a clock to 0.
The set of invariant constraints *C'(V)* is a subset of *C(V)* including only
constraint of the form:
g = v < c | true
This simplifies the implementation as a clock expiration is a necessary and
sufficient condition for the violation of invariants while still allowing more
complex constraints to be specified as guards.
It is important to note that any hybrid automaton is a valid deterministic
automaton with additional guards and invariants. Those can only further
constrain what transitions are valid but it is not possible to define
transition functions starting from the same state in *X* and the same event in
*E* but ending up in different states in *X* based on the valuation of *V*.
Examples
--------
Wip as hybrid automaton
~~~~~~~~~~~~~~~~~~~~~~~
The 'wip' (wakeup in preemptive) example introduced as a deterministic automaton
can also be described as:
- *X* = { ``any_thread_running`` }
- *E* = { ``sched_waking`` }
- *V* = { ``preemptive`` }
- x\ :subscript:`0` = ``any_thread_running``
- X\ :subscript:`m` = {``any_thread_running``}
- *f* =
- *f*\ (``any_thread_running``, ``sched_waking``, ``preemptive==0``) = ``any_thread_running``
- *i* =
- *i*\ (``any_thread_running``) = ``true``
Which can be represented graphically as::
|
|
v
#====================# sched_waking;preemptive==0
H H ------------------------------+
H any_thread_running H |
H H <-----------------------------+
#====================#
In this example, by using the preemptive state of the system as an environment
variable, we can assert this constraint on ``sched_waking`` without requiring
preemption events (as we would in a deterministic automaton), which can be
useful in case those events are not available or not reliable on the system.
Since all the invariants in *i* are true, we can omit them from the representation.
Stall model with guards (iteration 1)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As a sample timed automaton we can define 'stall' as:
- *X* = { ``dequeued``, ``enqueued``, ``running``}
- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
- *V* = { ``clk`` }
- x\ :subscript:`0` = ``dequeue``
- X\ :subscript:`m` = {``dequeue``}
- *f* =
- *f*\ (``enqueued``, ``switch_in``, ``clk < threshold``) = ``running``
- *f*\ (``running``, ``dequeue``) = ``dequeued``
- *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
- *i* = *omitted as all true*
Graphically represented as::
|
|
v
#============================#
H dequeued H <+
#============================# |
| |
| enqueue; reset(clk) |
v |
+----------------------------+ |
| enqueued | | dequeue
+----------------------------+ |
| |
| switch_in; clk < threshold |
v |
+----------------------------+ |
| running | -+
+----------------------------+
This model imposes that the time between when a task is enqueued (it becomes
runnable) and when the task gets to run must be lower than a certain threshold.
A failure in this model means that the task is starving.
One problem in using guards on the edges in this case is that the model will
not report a failure until the ``switch_in`` event occurs. This means that,
according to the model, it is valid for the task never to run.
Stall model with invariants (iteration 2)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The first iteration isn't exactly what was intended, we can change the model as:
- *X* = { ``dequeued``, ``enqueued``, ``running``}
- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
- *V* = { ``clk`` }
- x\ :subscript:`0` = ``dequeue``
- X\ :subscript:`m` = {``dequeue``}
- *f* =
- *f*\ (``enqueued``, ``switch_in``) = ``running``
- *f*\ (``running``, ``dequeue``) = ``dequeued``
- *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
- *i* =
- *i*\ (``enqueued``) = ``clk < threshold``
Graphically::
|
|
v
#=========================#
H dequeued H <+
#=========================# |
| |
| enqueue; reset(clk) |
v |
+-------------------------+ |
| enqueued | |
| clk < threshold | | dequeue
+-------------------------+ |
| |
| switch_in |
v |
+-------------------------+ |
| running | -+
+-------------------------+
In this case, we moved the guard as an invariant to the ``enqueued`` state,
this means we not only forbid the occurrence of ``switch_in`` when ``clk`` is
past the threshold but also mark as invalid in case we are *still* in
``enqueued`` after the threshold. This model is effectively in an invalid state
as soon as a task is starving, rather than when the starving task finally runs.
Hybrid Automaton in C
---------------------
The definition of hybrid automata in C is heavily based on the deterministic
automata one. Specifically, we add the set of environment variables and the
constraints (both guards on transitions and invariants on states) as follows.
This is a combination of both iterations of the stall example::
/* enum representation of X (set of states) to be used as index */
enum states {
dequeued,
enqueued,
running,
state_max,
};
#define INVALID_STATE state_max
/* enum representation of E (set of events) to be used as index */
enum events {
dequeue,
enqueue,
switch_in,
event_max,
};
/* enum representation of V (set of environment variables) to be used as index */
enum envs {
clk,
env_max,
env_max_stored = env_max,
};
struct automaton {
char *state_names[state_max]; // X: the set of states
char *event_names[event_max]; // E: the finite set of events
char *env_names[env_max]; // V: the finite set of env vars
unsigned char function[state_max][event_max]; // f: transition function
unsigned char initial_state; // x_0: the initial state
bool final_states[state_max]; // X_m: the set of marked states
};
struct automaton aut = {
.state_names = {
"dequeued",
"enqueued",
"running",
},
.event_names = {
"dequeue",
"enqueue",
"switch_in",
},
.env_names = {
"clk",
},
.function = {
{ INVALID_STATE, enqueued, INVALID_STATE },
{ INVALID_STATE, INVALID_STATE, running },
{ dequeued, INVALID_STATE, INVALID_STATE },
},
.initial_state = dequeued,
.final_states = { 1, 0, 0 },
};
static bool verify_constraint(enum states curr_state, enum events event,
enum states next_state)
{
bool res = true;
/* Validate guards as part of f */
if (curr_state == enqueued && event == switch_in)
res = get_env(clk) < threshold;
else if (curr_state == dequeued && event == enqueue)
reset_env(clk);
/* Validate invariants in i */
if (next_state == curr_state || !res)
return res;
if (next_state == enqueued)
ha_start_timer_jiffy(ha_mon, clk, threshold_jiffies);
else if (curr_state == enqueued)
res = !ha_cancel_timer(ha_mon);
return res;
}
The function ``verify_constraint``, here reported as simplified, checks guards,
performs resets and starts timers to validate invariants according to
specification, those cannot easily be represented in the automaton struct.
Due to the complex nature of environment variables, the user needs to provide
functions to get and reset environment variables that are not common clocks
(e.g. clocks with ns or jiffy granularity).
Since invariants are only defined as clock expirations (e.g. *clk <
threshold*), reaching the expiration of a timer armed when entering the state
is in fact a failure in the model and triggers a reaction. Leaving the state
stops the timer.
It is important to note that timers implemented with hrtimers introduce
overhead, if the monitor has several instances (e.g. all tasks) this can become
an issue. The impact can be decreased using the timer wheel (``HA_TIMER_TYPE``
set to ``HA_TIMER_WHEEL``), this lowers the responsiveness of the timer without
damaging the accuracy of the model, since the invariant condition is checked
before disabling the timer in case the callback is late.
Alternatively, if the monitor is guaranteed to *eventually* leave the state and
the incurred delay to wait for the next event is acceptable, guards can be used
in place of invariants, as seen in the stall example.
Graphviz .dot format
--------------------
Also the Graphviz representation of hybrid automata is an extension of the
deterministic automata one. Specifically, guards can be provided in the event
name separated by ``;``::
"state_start" -> "state_dest" [ label = "sched_waking;preemptible==0;reset(clk)" ];
Invariant can be specified in the state label (not the node name!) separated by ``\n``::
"enqueued" [label = "enqueued\nclk < threshold_jiffies"];
Constraints can be specified as valid C comparisons and allow spaces, the first
element of the comparison must be the clock while the second is a numerical or
parametrised value. Guards allow comparisons to be combined with boolean
operations (``&&`` and ``||``), resets must be separated from other constraints.
This is the full example of the last version of the 'stall' model in DOT::
digraph state_automaton {
{node [shape = circle] "enqueued"};
{node [shape = plaintext, style=invis, label=""] "__init_dequeued"};
{node [shape = doublecircle] "dequeued"};
{node [shape = circle] "running"};
"__init_dequeued" -> "dequeued";
"enqueued" [label = "enqueued\nclk < threshold_jiffies"];
"running" [label = "running"];
"dequeued" [label = "dequeued"];
"enqueued" -> "running" [ label = "switch_in" ];
"running" -> "dequeued" [ label = "dequeue" ];
"dequeued" -> "enqueued" [ label = "enqueue;reset(clk)" ];
{ rank = min ;
"__init_dequeued";
"dequeued";
}
}
References
----------
One book covering model checking and timed automata is::
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking,
The MIT Press, 2008.
Hybrid automata are described in detail in::
Thomas Henzinger: The theory of hybrid automata,
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996.
linux-7.2.3/Documentation/trace/rv/index.rst
+20
View File
@@ -0,0 +1,20 @@
====================
Runtime Verification
====================
.. toctree::
:maxdepth: 2
:glob:
runtime-verification.rst
deterministic_automata.rst
linear_temporal_logic.rst
hybrid_automata.rst
monitor_synthesis.rst
da_monitor_instrumentation.rst
monitor_wip.rst
monitor_wwnr.rst
monitor_sched.rst
monitor_rtapp.rst
monitor_stall.rst
monitor_deadline.rst
linux-7.2.3/Documentation/trace/rv/linear_temporal_logic.rst
+134
View File
@@ -0,0 +1,134 @@
Linear temporal logic
=====================
Introduction
------------
Runtime verification monitor is a verification technique which checks that the
kernel follows a specification. It does so by using tracepoints to monitor the
kernel's execution trace, and verifying that the execution trace sastifies the
specification.
Initially, the specification can only be written in the form of deterministic
automaton (DA). However, while attempting to implement DA monitors for some
complex specifications, deterministic automaton is found to be inappropriate as
the specification language. The automaton is complicated, hard to understand,
and error-prone.
Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type
of monitor uses LTL as specification instead of DA. For some cases, writing the
specification as LTL is more concise and intuitive.
Many materials explain LTL in details. One book is::
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
Press, 2008.
Grammar
-------
Unlike some existing syntax, kernel's implementation of LTL is more verbose.
This is motivated by considering that the people who read the LTL specifications
may not be well-versed in LTL.
Grammar:
ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
Operands (opd):
true, false, user-defined names consisting of upper-case characters, digits,
and underscore.
Unary Operators (unop):
always
eventually
next
not
Binary Operators (binop):
until
and
or
imply
equivalent
This grammar is ambiguous: operator precedence is not defined. Parentheses must
be used.
Example linear temporal logic
-----------------------------
.. code-block::
RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)
means: if it is raining, going outside means having an umbrella.
.. code-block::
RAIN imply (WET until not RAIN)
means: if it is raining, it is going to be wet until the rain stops.
.. code-block::
RAIN imply eventually not RAIN
means: if it is raining, rain will eventually stop.
The above examples are referring to the current time instance only. For kernel
verification, the `always` operator is usually desirable, to specify that
something is always true at the present and for all future. For example::
always (RAIN imply eventually not RAIN)
means: *all* rain eventually stops.
In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the
"atomic propositions".
Monitor synthesis
-----------------
To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used:
`tools/verification/rvgen`. The specification needs to be provided as a file,
and it must have a "RULE = LTL" assignment. For example::
RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or
`CRASHED`.
The LTL can be broken down using sub-expressions. The above is equivalent to:
.. code-block::
RULE = always (ACQUIRE imply (ALIVE until RELEASE))
ALIVE = not KILLED and not CRASHED
From this specification, `rvgen` generates the C implementation of a Buchi
automaton - a non-deterministic state machine which checks the satisfiability of
the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using
`rvgen`.
References
----------
One book covering model checking and linear temporal logic is::
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
Press, 2008.
For an example of using linear temporal logic in software testing, see::
Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury.
2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the
44th International Conference on Software Engineering (ICSE '22). Association
for Computing Machinery, New York, NY, USA, 1343–1355.
https://doi.org/10.1145/3510003.3510082
The kernel's LTL monitor implementation is based on::
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly
Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa,
M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP
Advances in Information and Communication Technology. Springer, Boston, MA.
https://doi.org/10.1007/978-0-387-34892-6_1
linux-7.2.3/Documentation/trace/rv/monitor_deadline.rst
+84
View File
@@ -0,0 +1,84 @@
Deadline monitors
=================
- Name: deadline
- Type: container for multiple monitors
- Author: Gabriele Monaco <gmonaco@redhat.com>
Description
-----------
The deadline monitor is a set of specifications to describe the deadline
scheduler behaviour. It includes monitors per scheduling entity (deadline tasks
and servers) that work independently to verify different specifications the
deadline scheduler should follow.
Specifications
--------------
Monitor nomiss
~~~~~~~~~~~~~~
The nomiss monitor ensures dl entities get to run *and* run to completion
before their deadline, although deferrable servers may not run. An entity is
considered done if ``throttled``, either because it yielded or used up its
runtime, or when it voluntarily starts ``sleeping``.
The monitor includes a user configurable deadline threshold. If the total
utilisation of deadline tasks is larger than 1, they are only guaranteed
bounded tardiness. See Documentation/scheduler/sched-deadline.rst for more
details. The threshold (module parameter ``nomiss.deadline_thresh``) can be
configured to avoid the monitor to fail based on the acceptable tardiness in
the system. Since ``dl_throttle`` is a valid outcome for the entity to be done,
the minimum tardiness needs be 1 tick to consider the throttle delay, unless
the ``HRTICK_DL`` scheduler feature is active.
Servers have also an intermediate ``idle`` state, occurring as soon as no
runnable task is available from ready or running where no timing constraint
is applied. A server goes to sleep by stopping, there is no wakeup equivalent
as the order of a server starting and replenishing is not defined, hence a
server can run from sleeping without being ready::
|
sched_wakeup v
dl_replenish;reset(clk) -- #=========================#
| H H dl_replenish;reset(clk)
+-----------> H H <--------------------+
H H |
+- dl_server_stop ---- H ready H |
| +-----------------> H clk < DEADLINE_NS() H dl_throttle; |
| | H H is_defer == 1 |
| | sched_switch_in - H H -----------------+ |
| | | #=========================# | |
| | | | ^ | |
| | | dl_server_idle dl_replenish;reset(clk) | |
| | | v | | |
| | | +--------------+ | |
| | | +------ | | | |
| | | dl_server_idle | | dl_throttle | |
| | | | | idle | -----------------+ | |
| | | +-----> | | | | |
| | | | | | | |
| | | | | | | |
+--+--+---+--- dl_server_stop -- +--------------+ | | |
| | | | | ^ | | |
| | | | sched_switch_in dl_server_idle | | |
| | | | v | | | |
| | | | +---------- +---------------------+ | | |
| | | | sched_switch_in | | | | |
| | | | sched_wakeup | | | | |
| | | | dl_replenish; | running | -------+ | | |
| | | | reset(clk) | clk < DEADLINE_NS() | | | | |
| | | | +---------> | | dl_throttle | | |
| | | +----------------> | | | | | |
| | | +---------------------+ | | | |
| | sched_wakeup ^ sched_switch_suspend | | | |
v v dl_replenish;reset(clk) | dl_server_stop | | | |
+--------------+ | | v v v |
| | - sched_switch_in + | +---------------+
| | <---------------------+ dl_throttle +-- | |
| sleeping | sched_wakeup | | throttled |
| | -- dl_server_stop dl_server_idle +-> | |
| | dl_server_idle sched_switch_suspend +---------------+
+--------------+ <---------+ ^
| |
+------ dl_throttle;is_constr_dl == 1 || is_defer == 1 ------+
linux-7.2.3/Documentation/trace/rv/monitor_rtapp.rst
+133
View File
@@ -0,0 +1,133 @@
Real-time application monitors
==============================
- Name: rtapp
- Type: container for multiple monitors
- Author: Nam Cao <namcao@linutronix.de>
Description
-----------
Real-time applications may have design flaws such that they experience
unexpected latency and fail to meet their time requirements. Often, these flaws
follow a few patterns:
- Page faults: A real-time thread may access memory that does not have a
mapped physical backing or must first be copied (such as for copy-on-write).
Thus a page fault is raised and the kernel must first perform the expensive
action. This causes significant delays to the real-time thread
- Priority inversion: A real-time thread blocks waiting for a lower-priority
thread. This causes the real-time thread to effectively take on the
scheduling priority of the lower-priority thread. For example, the real-time
thread needs to access a shared resource that is protected by a
non-pi-mutex, but the mutex is currently owned by a non-real-time thread.
The `rtapp` monitor detects these patterns. It aids developers to identify
reasons for unexpected latency with real-time applications. It is a container of
multiple sub-monitors described in the following sections.
Monitor pagefault
+++++++++++++++++
The `pagefault` monitor reports real-time tasks raising page faults. Its
specification is::
RULE = always (RT imply not PAGEFAULT)
To fix warnings reported by this monitor, `mlockall()` or `mlock()` can be used
to ensure physical backing for memory.
This monitor may have false negatives because the pages used by the real-time
threads may just happen to be directly available during testing. To minimize
this, the system can be put under memory pressure (e.g. invoking the OOM killer
using a program that does `ptr = malloc(SIZE_OF_RAM); memset(ptr, 0,
SIZE_OF_RAM);`) so that the kernel executes aggressive strategies to recycle as
much physical memory as possible.
Monitor sleep
+++++++++++++
The `sleep` monitor reports real-time threads sleeping in a manner that may
cause undesirable latency. Real-time applications should only put a real-time
thread to sleep for one of the following reasons:
- Cyclic work: real-time thread sleeps waiting for the next cycle. For this
case, only the `clock_nanosleep` syscall should be used with `TIMER_ABSTIME`
(to avoid time drift) and `CLOCK_MONOTONIC` (to avoid the clock being
changed). No other method is safe for real-time. For example, threads
waiting for timerfd can be woken by softirq which provides no real-time
guarantee.
- Real-time thread waiting for something to happen (e.g. another thread
releasing shared resources, or a completion signal from another thread). In
this case, only futexes (FUTEX_LOCK_PI, FUTEX_LOCK_PI2 or one of
FUTEX_WAIT_*) should be used. Applications usually do not use futexes
directly, but use PI mutexes and PI condition variables which are built on
top of futexes. Be aware that the C library might not implement conditional
variables as safe for real-time. As an alternative, the librtpi library
exists to provide a conditional variable implementation that is correct for
real-time applications in Linux.
Beside the reason for sleeping, the eventual waker should also be
real-time-safe. Namely, one of:
- An equal-or-higher-priority thread
- Hard interrupt handler
- Non-maskable interrupt handler
This monitor's warning usually means one of the following:
- Real-time thread is blocked by a non-real-time thread (e.g. due to
contention on a mutex without priority inheritance). This is priority
inversion.
- Time-critical work waits for something which is not safe for real-time (e.g.
timerfd).
- The work executed by the real-time thread does not need to run at real-time
priority at all. This is not a problem for the real-time thread itself, but
it is potentially taking the CPU away from other important real-time work.
Application developers may purposely choose to have their real-time application
sleep in a way that is not safe for real-time. It is debatable whether that is a
problem. Application developers must analyze the warnings to make a proper
assessment.
The monitor's specification is::
RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
and ((not WAKE) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
and NANOSLEEP_CLOCK_MONOTONIC
RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
or KTHREAD_SHOULD_STOP
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI
or TASK_IS_RCU
or TASK_IS_MIGRATION
Beside the scenarios described above, this specification also handle some
special cases:
- `KERNEL_THREAD`: kernel tasks do not have any pattern that can be recognized
as valid real-time sleeping reasons. Therefore sleeping reason is not
checked for kernel tasks.
- `KTHREAD_SHOULD_STOP`: a non-real-time thread may stop a real-time kernel
thread by waking it and waiting for it to exit (`kthread_stop()`). This
wakeup is safe for real-time.
- `ALLOWLIST`: to handle known false positives with the kernel.
- `BLOCK_ON_RT_MUTEX` is included in the allowlist due to its implementation.
In the release path of rt_mutex, a boosted task is de-boosted before waking
the rt_mutex's waiter. Consequently, the monitor may see a real-time-unsafe
wakeup (e.g. non-real-time task waking real-time task). This is actually
real-time-safe because preemption is disabled for the duration.
- `FUTEX_LOCK_PI` is included in the allowlist for the same reason as
`BLOCK_ON_RT_MUTEX`.
linux-7.2.3/Documentation/trace/rv/monitor_sched.rst
+371
View File
@@ -0,0 +1,371 @@
Scheduler monitors
==================
- Name: sched
- Type: container for multiple monitors
- Author: Gabriele Monaco <gmonaco@redhat.com>, Daniel Bristot de Oliveira <bristot@kernel.org>
Description
-----------
Monitors describing complex systems, such as the scheduler, can easily grow to
the point where they are just hard to understand because of the many possible
state transitions.
Often it is possible to break such descriptions into smaller monitors,
sharing some or all events. Enabling those smaller monitors concurrently is,
in fact, testing the system as if we had one single larger monitor.
Splitting models into multiple specification is not only easier to
understand, but gives some more clues when we see errors.
The sched monitor is a set of specifications to describe the scheduler behaviour.
It includes several per-cpu and per-task monitors that work independently to verify
different specifications the scheduler should follow.
To make this system as straightforward as possible, sched specifications are *nested*
monitors, whereas sched itself is a *container*.
From the interface perspective, sched includes other monitors as sub-directories,
enabling/disabling or setting reactors to sched, propagates the change to all monitors,
however single monitors can be used independently as well.
It is important that future modules are built after their container (sched, in
this case), otherwise the linker would not respect the order and the nesting
wouldn't work as expected.
To do so, simply add them after sched in the Makefile.
Specifications
--------------
The specifications included in sched are currently a work in progress, adapting the ones
defined by Daniel Bristot in [1]_.
Currently we included the following:
Monitor sco
~~~~~~~~~~~
The scheduling context operations (sco) monitor ensures changes in a task state
happen only in thread context::
|
|
v
sched_set_state +------------------+
+------------------ | |
| | thread_context |
+-----------------> | | <+
+------------------+ |
| |
| schedule_entry | schedule_exit
v |
|
scheduling_context -+
Monitor snroc
~~~~~~~~~~~~~
The set non runnable on its own context (snroc) monitor ensures changes in a
task state happens only in the respective task's context. This is a per-task
monitor::
|
|
v
+------------------+
| other_context | <+
+------------------+ |
| |
| sched_switch_in | sched_switch_out
v |
sched_set_state |
+------------------ |
| own_context |
+-----------------> -+
Monitor scpd
~~~~~~~~~~~~
The schedule called with preemption disabled (scpd) monitor ensures schedule is
called with preemption disabled::
|
|
v
+------------------+
| cant_sched | <+
+------------------+ |
| |
| preempt_disable | preempt_enable
v |
schedule_entry |
schedule_exit |
+----------------- can_sched |
| |
+----------------> -+
Monitor snep
~~~~~~~~~~~~
The schedule does not enable preempt (snep) monitor ensures a schedule call
does not enable preemption::
|
|
v
preempt_disable +------------------------+
preempt_enable | |
+------------------ | non_scheduling_context |
| | |
+-----------------> | | <+
+------------------------+ |
| |
| schedule_entry | schedule_exit
v |
|
scheduling_contex -+
Monitor sts
~~~~~~~~~~~
The schedule implies task switch (sts) monitor ensures a task switch happens
only in scheduling context and up to once, as well as scheduling occurs with
interrupts enabled but no task switch can happen before interrupts are
disabled. When the next task picked for execution is the same as the previously
running one, no real task switch occurs but interrupts are disabled nonetheless::
irq_entry |
+----+ |
v | v
+------------+ irq_enable #===================# irq_disable
| | ------------> H H irq_entry
| cant_sched | <------------ H H irq_enable
| | irq_disable H can_sched H --------------+
+------------+ H H |
H H |
+---------------> H H <-------------+
| #===================#
| |
schedule_exit | schedule_entry
| v
| +-------------------+ irq_enable
| | scheduling | <---------------+
| +-------------------+ |
| | |
| | irq_disable +--------+ irq_entry
| v | | --------+
| +-------------------+ irq_entry | in_irq | |
| | | -----------> | | <-------+
| | disable_to_switch | +--------+
| | | --+
| +-------------------+ |
| | |
| | sched_switch |
| v |
| +-------------------+ |
| | switching | | irq_enable
| +-------------------+ |
| | |
| | irq_enable |
| v |
| +-------------------+ |
+-- | enable_to_exit | <-+
+-------------------+
^ | irq_disable
| | irq_entry
+---------------+ irq_enable
Monitor nrp
-----------
The need resched preempts (nrp) monitor ensures preemption requires
``need_resched``. Only kernel preemption is considered, since preemption
while returning to userspace, for this monitor, is indistinguishable from
``sched_switch_yield`` (described in the sssw monitor).
A kernel preemption is whenever ``__schedule`` is called with the preemption
flag set to true (e.g. from preempt_enable or exiting from interrupts). This
type of preemption occurs after the need for ``rescheduling`` has been set.
This is not valid for the *lazy* variant of the flag, which causes only
userspace preemption.
A ``schedule_entry_preempt`` may involve a task switch or not, in the latter
case, a task goes through the scheduler from a preemption context but it is
picked as the next task to run. Since the scheduler runs, this clears the need
to reschedule. The ``any_thread_running`` state does not imply the monitored
task is not running as this monitor does not track the outcome of scheduling.
In theory, a preemption can only occur after the ``need_resched`` flag is set. In
practice, however, it is possible to see a preemption where the flag is not
set. This can happen in one specific condition::
need_resched
preempt_schedule()
preempt_schedule_irq()
__schedule()
!need_resched
__schedule()
In the situation above, standard preemption starts (e.g. from preempt_enable
when the flag is set), an interrupt occurs before scheduling and, on its exit
path, it schedules, which clears the ``need_resched`` flag.
When the preempted task runs again, the standard preemption started earlier
resumes, although the flag is no longer set. The monitor considers this a
``nested_preemption``, this allows another preemption without re-setting the
flag. This condition relaxes the monitor constraints and may catch false
negatives (i.e. no real ``nested_preemptions``) but makes the monitor more
robust and able to validate other scenarios.
For simplicity, the monitor starts in ``preempt_irq``, although no interrupt
occurred, as the situation above is hard to pinpoint::
schedule_entry
irq_entry #===========================================#
+-------------------------- H H
| H H
+-------------------------> H any_thread_running H
H H
+-------------------------> H H
| #===========================================#
| schedule_entry | ^
| schedule_entry_preempt | sched_need_resched | schedule_entry
| | schedule_entry_preempt
| v |
| +----------------------+ |
| +--- | | |
| sched_need_resched | | rescheduling | -+
| +--> | |
| +----------------------+
| | irq_entry
| v
| +----------------------+
| | | ---+
| ---> | | | sched_need_resched
| | preempt_irq | | irq_entry
| | | <--+
| | | <--+
| +----------------------+ |
| | schedule_entry | sched_need_resched
| | schedule_entry_preempt |
| v |
| +-----------------------+ |
+-------------------------- | nested_preempt | --+
+-----------------------+
^ irq_entry |
+-------------------+
Due to how the ``need_resched`` flag on the preemption count works on arm64,
this monitor is unstable on that architecture, as it often records preemption
when the flag is not set, even in presence of the workaround above.
For the time being, the monitor is disabled by default on arm64.
Monitor sssw
------------
The set state sleep and wakeup (sssw) monitor ensures ``set_state`` to
sleepable leads to sleeping and sleeping tasks require wakeup. It includes the
following types of switch:
* ``switch_suspend``:
a task puts itself to sleep, this can happen only after explicitly setting
the task to ``sleepable``. After a task is suspended, it needs to be woken up
(``waking`` state) before being switched in again.
Setting the task's state to ``sleepable`` can be reverted before switching if it
is woken up or set to ``runnable``.
* ``switch_blocking``:
a special case of a ``switch_suspend`` where the task is waiting on a
sleeping RT lock (``PREEMPT_RT`` only), it is common to see wakeup and set
state events racing with each other and this leads the model to perceive this
type of switch when the task is not set to sleepable. This is a limitation of
the model in SMP system and workarounds may slow down the system.
* ``switch_preempt``:
a task switch as a result of kernel preemption (``schedule_entry_preempt`` in
the nrp model).
* ``switch_yield``:
a task explicitly calls the scheduler or is preempted while returning to
userspace. It can happen after a ``yield`` system call, from the idle task or
if the ``need_resched`` flag is set. By definition, a task cannot yield while
``sleepable`` as that would be a suspension. A special case of a yield occurs
when a task in ``TASK_INTERRUPTIBLE`` calls the scheduler while a signal is
pending. The task doesn't go through the usual blocking/waking and is set
back to runnable, the resulting switch (if there) looks like a yield to the
``signal_wakeup`` state and is followed by the signal delivery. From this
state, the monitor expects a signal even if it sees a wakeup event, although
not necessary, to rule out false negatives.
This monitor doesn't include a running state, ``sleepable`` and ``runnable``
are only referring to the task's desired state, which could be scheduled out
(e.g. due to preemption). However, it does include the event
``sched_switch_in`` to represent when a task is allowed to become running. This
can be triggered also by preemption, but cannot occur after the task got to
``sleeping`` before a ``wakeup`` occurs::
+--------------------------------------------------------------------------+
| |
| |
| switch_suspend | |
| switch_blocking | |
v v |
+----------+ #==========================# set_state_runnable |
| | H H wakeup |
| | H H switch_in |
| | H H switch_yield |
| sleeping | H H switch_preempt |
| | H H signal_deliver |
| | switch_ H H ------+ |
| | _blocking H runnable H | |
| | <----------- H H <-----+ |
+----------+ H H |
| wakeup H H |
+---------------------> H H |
H H |
+---------> H H |
| #==========================# |
| | ^ |
| | | set_state_runnable |
| | | wakeup |
| set_state_sleepable | +------------------------+
| v | |
| +--------------------------+ set_state_sleepable
| | | switch_in
| | | switch_preempt
signal_deliver | sleepable | signal_deliver
| | | ------+
| | | |
| | | <-----+
| +--------------------------+
| | ^
| switch_yield | set_state_sleepable
| v |
| +---------------+ |
+---------- | signal_wakeup | -+
+---------------+
^ | switch_in
| | switch_preempt
| | switch_yield
+-----------+ wakeup
Monitor opid
------------
The operations with preemption and irq disabled (opid) monitor ensures
operations like ``wakeup`` and ``need_resched`` occur with interrupts and
preemption disabled.
``need_resched`` can be set by some RCU internals functions, in which case it
doesn't match a task wakeup and might occur with only interrupts disabled.
The interrupt and preemption status are validated by the hybrid automaton
constraints when processing the events::
|
|
v
#=========# sched_need_resched;irq_off == 1
H H sched_waking;irq_off == 1 && preempt_off == 1
H any H ------------------------------------------------+
H H |
H H <-----------------------------------------------+
#=========#
References
----------
.. [1] Daniel Bristot de Oliveira et al.:
`A thread synchronization model for the PREEMPT_RT Linux kernel
<https://www.iris.sssup.it/bitstream/11382/533630/1/Elsevier-JSA-2020.pdf>`_,
J. Syst. Archit., 2020.
linux-7.2.3/Documentation/trace/rv/monitor_stall.rst
+43
View File
@@ -0,0 +1,43 @@
Monitor stall
=============
- Name: stall - stalled task monitor
- Type: per-task hybrid automaton
- Author: Gabriele Monaco <gmonaco@redhat.com>
Description
-----------
The stalled task (stall) monitor is a sample per-task timed monitor that checks
if tasks are scheduled within a defined threshold after they are ready::
|
|
v
#==========================#
+-----------------> H dequeued H
| #==========================#
| |
sched_switch_wait | sched_wakeup;reset(clk)
| v
| +--------------------------+ <+
| | enqueued | | sched_wakeup
| | clk < threshold_jiffies | -+
| +--------------------------+
| | ^
| sched_switch_in sched_switch_preempt;reset(clk)
| v |
| +--------------------------+
+------------------ | running |
+--------------------------+
^ sched_switch_in |
| sched_wakeup |
+----------------------+
The threshold can be configured as a parameter by either booting with the
``stall.threshold_jiffies=<new value>`` argument or writing a new value to
``/sys/module/stall/parameters/threshold_jiffies``.
Specification
-------------
Graphviz Dot file in tools/verification/models/stall.dot
linux-7.2.3/Documentation/trace/rv/monitor_synthesis.rst
+382
View File
@@ -0,0 +1,382 @@
Runtime Verification Monitor Synthesis
======================================
The starting point for the application of runtime verification (RV) techniques
is the *specification* or *modeling* of the desired (or undesired) behavior
of the system under scrutiny.
The formal representation needs to be then *synthesized* into a *monitor*
that can then be used in the analysis of the trace of the system. The
*monitor* connects to the system via an *instrumentation* that converts
the events from the *system* to the events of the *specification*.
In Linux terms, the runtime verification monitors are encapsulated inside
the *RV monitor* abstraction. The RV monitor includes a set of instances
of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
functions that glue the monitor to the system reference model, and the
trace output as a reaction to event parsing and exceptions, as depicted
below::
Linux +---- RV Monitor ----------------------------------+ Formal
Realm | | Realm
+-------------------+ +----------------+ +-----------------+
| Linux kernel | | Monitor | | Reference |
| Tracing | -> | Instance(s) | <- | Model |
| (instrumentation) | | (verification) | | (specification) |
+-------------------+ +----------------+ +-----------------+
| | |
| V |
| +----------+ |
| | Reaction | |
| +--+--+--+-+ |
| | | | |
| | | +-> trace output ? |
+------------------------|--|----------------------+
| +----> panic ?
+-------> <user-specified>
RV monitor synthesis
--------------------
The synthesis of a specification into the Linux *RV monitor* abstraction is
automated by the rvgen tool and the header file containing common code for
creating monitors. The header files are:
* rv/da_monitor.h for deterministic automaton monitor.
* rv/ltl_monitor.h for linear temporal logic monitor.
* rv/ha_monitor.h for hybrid automaton monitor.
rvgen
-----
The rvgen utility converts a specification into the C presentation and creating
the skeleton of a kernel monitor in C.
For example, it is possible to transform the wip.dot model present in
[1] into a per-cpu monitor with the following command::
$ rvgen monitor -c da -s wip.dot -t per_cpu
This will create a directory named wip/ with the following files:
- wip.h: the wip model in C
- wip.c: the RV monitor
The wip.c file contains the monitor declaration and the starting point for
the system instrumentation.
Similarly, a linear temporal logic monitor can be generated with the following
command::
$ rvgen monitor -c ltl -s pagefault.ltl -t per_task
This generates pagefault/ directory with:
- pagefault.h: The Buchi automaton (the non-deterministic state machine to
verify the specification)
- pagefault.c: The skeleton for the RV monitor
Monitor header files
--------------------
The header files:
- `rv/da_monitor.h` for deterministic automaton monitor
- `rv/ltl_monitor` for linear temporal logic monitor
include common macros and static functions for implementing *Monitor
Instance(s)*.
The benefits of having all common functionalities in a single header file are
3-fold:
- Reduce the code duplication;
- Facilitate the bug fix/improvement;
- Avoid the case of developers changing the core of the monitor code to
manipulate the model in a (let's say) non-standard way.
rv/da_monitor.h
+++++++++++++++
This initial implementation presents three different types of monitor instances:
- ``#define RV_MON_TYPE RV_MON_GLOBAL``
- ``#define RV_MON_TYPE RV_MON_PER_CPU``
- ``#define RV_MON_TYPE RV_MON_PER_TASK``
The first sets up functions declaration for a global deterministic automata
monitor, the second for monitors with per-cpu instances, and the third with
per-task instances.
In all cases, the C file must include the $(MODEL_NAME).h file (generated by
`rvgen`), for example, to define the per-cpu 'wip' monitor, the `wip.c` source
file must include::
#define RV_MON_TYPE RV_MON_PER_CPU
#include "wip.h"
#include <rv/da_monitor.h>
The monitor is executed by sending events to be processed via the functions
presented below::
da_handle_event($(event from event enum));
da_handle_start_event($(event from event enum));
da_handle_start_run_event($(event from event enum));
The function ``da_handle_event()`` is the regular case where
the event will be processed if the monitor is processing events.
When a monitor is enabled, it is placed in the initial state of the automata.
However, the monitor does not know if the system is in the *initial state*.
The ``da_handle_start_event()`` function is used to notify the
monitor that the system is returning to the initial state, so the monitor can
start monitoring the next event.
The ``da_handle_start_run_event()`` function is used to notify
the monitor that the system is known to be in the initial state, so the
monitor can start monitoring and monitor the current event.
Using the wip model as example, the events "preempt_disable" and
"sched_waking" should be sent to monitor, respectively, via [2]::
da_handle_event(preempt_disable_wip);
da_handle_event(sched_waking_wip);
While the event "preempt_enabled" will use::
da_handle_start_event(preempt_enable_wip);
To notify the monitor that the system will be returning to the initial state,
so the system and the monitor should be in sync.
rv/ltl_monitor.h
++++++++++++++++
This file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`)
to be complete. For example, for the `pagefault` monitor, the `pagefault.c`
source file must include::
#include "pagefault.h"
#include <rv/ltl_monitor.h>
(the skeleton monitor file generated by `rvgen` already does this).
`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the
implementation of the Buchi automaton - a non-deterministic state machine that
verifies the LTL specification. While `rv/ltl_monitor.h` includes the common
helper functions to interact with the Buchi automaton and to implement an RV
monitor. An important definition in `$(MODEL_NAME).h` is::
enum ltl_atom {
LTL_$(FIRST_ATOMIC_PROPOSITION),
LTL_$(SECOND_ATOMIC_PROPOSITION),
...
LTL_NUM_ATOM
};
which is the list of atomic propositions present in the LTL specification
(prefixed with "LTL\_" to avoid name collision). This `enum` is passed to the
functions interacting with the Buchi automaton.
While generating code, `rvgen` cannot understand the meaning of the atomic
propositions. Thus, that task is left for manual work. The recommended practice
is adding tracepoints to places where the atomic propositions change; and in the
tracepoints' handlers: the Buchi automaton is executed using::
void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)
which tells the Buchi automaton that the atomic proposition `atom` is now
`value`. The Buchi automaton checks whether the LTL specification is still
satisfied, and invokes the monitor's error tracepoint and the reactor if
violation is detected.
Tracepoints and `ltl_atom_update()` should be used whenever possible. However,
it is sometimes not the most convenient. For some atomic propositions which are
changed in multiple places in the kernel, it is cumbersome to trace all those
places. Furthermore, it may not be important that the atomic propositions are
updated at precise times. For example, considering the following linear temporal
logic::
RULE = always (RT imply not PAGEFAULT)
This LTL states that a real-time task does not raise page faults. For this
specification, it is not important when `RT` changes, as long as it has the
correct value when `PAGEFAULT` is true. Motivated by this case, another
function is introduced::
void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
This function is called whenever the Buchi automaton is triggered. Therefore, it
can be manually implemented to "fetch" `RT`::
void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
{
ltl_atom_set(mon, LTL_RT, rt_task(task));
}
Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_update()`,
`RT` is also fetched. Thus, the LTL specification can be verified without
tracing `RT` everywhere.
For atomic propositions which act like events, they usually need to be set (or
cleared) and then immediately cleared (or set). A convenient function is
provided::
void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)
which is equivalent to::
ltl_atom_update(task, atom, value);
ltl_atom_update(task, atom, !value);
To initialize the atomic propositions, the following function must be
implemented::
ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
This function is called for all running tasks when the monitor is enabled. It is
also called for new tasks created after the enabling the monitor. It should
initialize as many atomic propositions as possible, for example::
void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
{
ltl_atom_set(mon, LTL_RT, rt_task(task));
if (task_creation)
ltl_atom_set(mon, LTL_PAGEFAULT, false);
}
Atomic propositions not initialized by `ltl_atom_init()` will stay in the
unknown state until relevant tracepoints are hit, which can take some time. As
monitoring for a task cannot be done until all atomic propositions is known for
the task, the monitor may need some time to start validating tasks which have
been running before the monitor is enabled. Therefore, it is recommended to
start the tasks of interest after enabling the monitor.
rv/ha_monitor.h
+++++++++++++++
The implementation of hybrid automaton monitors derives directly from the
deterministic automaton one. Despite using a different header
(``ha_monitor.h``) the functions to handle events are the same (e.g.
``da_handle_event``).
Additionally, the `rvgen` tool populates skeletons for the
``ha_verify_constraint``, ``ha_get_env`` and ``ha_reset_env`` based on the
monitor specification in the monitor source file.
``ha_verify_constraint`` is typically ready as it is generated by `rvgen`:
* standard constraints on edges are turned into the form::
res = ha_get_env(ha_mon, ENV) < VALUE;
* reset constraints are turned into the form::
ha_reset_env(ha_mon, ENV);
* constraints on the state are implemented using timers
- armed before entering the state
- cancelled while entering any other state
- untouched if the state does not change as a result of the event
- checked if the timer expired but the callback did not run
- available implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL`
- hrtimers are more precise but may have higher overhead
- select by defining `HA_TIMER_TYPE` before including the header::
#define HA_TIMER_TYPE HA_TIMER_HRTIMER
Constraint values can be specified in different forms:
* literal value (with optional unit). E.g.::
preemptive == 0
clk < 100ns
threshold <= 10j
* constant value (uppercase string). E.g.::
clk < MAX_NS
* parameter (lowercase string). E.g.::
clk <= threshold_jiffies
* macro (uppercase string with parentheses). E.g.::
clk < MAX_NS()
* function (lowercase string with parentheses). E.g.::
clk <= threshold_jiffies()
In all cases, `rvgen` will try to understand the type of the environment
variable from the name or unit. For instance, constants or parameters
terminating with ``_NS`` or ``_jiffies`` are intended as clocks with ns and jiffy
granularity, respectively. Literals with measure unit `j` are jiffies and if a
time unit is specified (`ns` to `s`), `rvgen` will convert the value to `ns`.
Constants need to be defined by the user (but unlike the name, they don't
necessarily need to be defined as constants). Parameters get converted to
module parameters and the user needs to provide a default value.
Also function and macros are defined by the user, by default they get as an
argument the ``ha_monitor``, a common usage would be to get the required value
from the target, e.g. the task in per-task monitors, using the helper
``ha_get_target(ha_mon)``.
If `rvgen` determines that the variable is a clock, it provides the getter and
resetter based on the unit. Otherwise, the user needs to provide an appropriate
definition.
Typically non-clock environment variables are not reset. In such case only the
getter skeleton will be present in the file generated by `rvgen`.
For instance, the getter for preemptive can be filled as::
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env)
{
if (env == preemptible)
return preempt_count() == 0;
return ENV_INVALID_VALUE;
}
The function is supplied the ``ha_mon`` parameter in case some storage is
required (as it is for clocks), but environment variables without reset do not
require a storage and can ignore that argument.
The number of environment variables requiring a storage is limited by
``MAX_HA_ENV_LEN``, however such limitation doesn't stand for other variables.
Finally, constraints on states are only valid for clocks and only if the
constraint is of the form `clk < N`. This is because such constraints are
implemented with the expiration of a timer.
Typically the clock variables are reset just before arming the timer, but this
doesn't have to be the case and the available functions take care of it.
It is a responsibility of per-task monitors to make sure no timer is left
running when the task exits.
By default the generator implements timers with hrtimers (setting
``HA_TIMER_TYPE`` to ``HA_TIMER_HRTIMER``), this gives better responsiveness
but higher overhead. The timer wheel (``HA_TIMER_WHEEL``) is a good alternative
for monitors with several instances (e.g. per-task) that achieves lower
overhead with increased latency, yet without compromising precision.
Final remarks
-------------
With the monitor synthesis in place using the header files and
rvgen, the developer's work should be limited to the instrumentation
of the system, increasing the confidence in the overall approach.
[1] For details about deterministic automata format and the translation
from one representation to another, see::
Documentation/trace/rv/deterministic_automata.rst
[2] rvgen appends the monitor's name suffix to the events enums to
avoid conflicting variables when exporting the global vmlinux.h
use by BPF programs.
linux-7.2.3/Documentation/trace/rv/monitor_wip.rst
+55
View File
@@ -0,0 +1,55 @@
Monitor wip
===========
- Name: wip - wakeup in preemptive
- Type: per-cpu deterministic automaton
- Author: Daniel Bristot de Oliveira <bristot@kernel.org>
Description
-----------
The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
that verifies if the wakeup events always take place with
preemption disabled::
|
|
v
#==================#
H preemptive H <+
#==================# |
| |
| preempt_disable | preempt_enable
v |
sched_waking +------------------+ |
+--------------- | | |
| | non_preemptive | |
+--------------> | | -+
+------------------+
The wakeup event always takes place with preemption disabled because
of the scheduler synchronization. However, because the preempt_count
and its trace event are not atomic with regard to interrupts, some
inconsistencies might happen. For example::
preempt_disable() {
__preempt_count_add(1)
-------> smp_apic_timer_interrupt() {
preempt_disable()
do not trace (preempt count >= 1)
wake up a thread
preempt_enable()
do not trace (preempt count >= 1)
}
<------
trace_preempt_disable();
}
This problem was reported and discussed here:
https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
Specification
-------------
Grapviz Dot file in tools/verification/models/wip.dot
linux-7.2.3/Documentation/trace/rv/monitor_wwnr.rst
+45
View File
@@ -0,0 +1,45 @@
Monitor wwnr
============
- Name: wwrn - wakeup while not running
- Type: per-task deterministic automaton
- Author: Daniel Bristot de Oliveira <bristot@kernel.org>
Description
-----------
This is a per-task sample monitor, with the following
definition::
|
|
v
wakeup +-------------+
+--------- | |
| | not_running |
+--------> | | <+
+-------------+ |
| |
| switch_in | switch_out
v |
+-------------+ |
| running | -+
+-------------+
This model is broken, the reason is that a task can be running
in the processor without being set as RUNNABLE. Think about a
task about to sleep::
1: set_current_state(TASK_UNINTERRUPTIBLE);
2: schedule();
And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.
- Why do we need this model, so?
- To test the reactors.
Specification
-------------
Grapviz Dot file in tools/verification/models/wwnr.dot
linux-7.2.3/Documentation/trace/rv/runtime-verification.rst
+231
View File
@@ -0,0 +1,231 @@
====================
Runtime Verification
====================
Runtime Verification (RV) is a lightweight (yet rigorous) method that
complements classical exhaustive verification techniques (such as *model
checking* and *theorem proving*) with a more practical approach for complex
systems.
Instead of relying on a fine-grained model of a system (e.g., a
re-implementation at instruction level), RV works by analyzing the trace of the
system's actual execution, comparing it against a formal specification of
the system behavior.
The main advantage is that RV can give precise information on the runtime
behavior of the monitored system, without the pitfalls of developing models
that require a re-implementation of the entire system in a modeling language.
Moreover, given an efficient monitoring method, it is possible to execute an
*online* verification of a system, enabling the *reaction* for unexpected
events, avoiding, for example, the propagation of a failure on safety-critical
systems.
Runtime Monitors and Reactors
=============================
A monitor is the central part of the runtime verification of a system. The
monitor stands in between the formal specification of the desired (or
undesired) behavior, and the trace of the actual system.
In Linux terms, the runtime verification monitors are encapsulated inside the
*RV monitor* abstraction. A *RV monitor* includes a reference model of the
system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
and so on), and the helper functions that glue the monitor to the system via
trace, as depicted below::
Linux +---- RV Monitor ----------------------------------+ Formal
Realm | | Realm
+-------------------+ +----------------+ +-----------------+
| Linux kernel | | Monitor | | Reference |
| Tracing | -> | Instance(s) | <- | Model |
| (instrumentation) | | (verification) | | (specification) |
+-------------------+ +----------------+ +-----------------+
| | |
| V |
| +----------+ |
| | Reaction | |
| +--+--+--+-+ |
| | | | |
| | | +-> trace output ? |
+------------------------|--|----------------------+
| +----> panic ?
+-------> <user-specified>
In addition to the verification and monitoring of the system, a monitor can
react to an unexpected event. The forms of reaction can vary from logging the
event occurrence to the enforcement of the correct behavior to the extreme
action of taking a system down to avoid the propagation of a failure.
In Linux terms, a *reactor* is an reaction method available for *RV monitors*.
By default, all monitors should provide a trace output of their actions,
which is already a reaction. In addition, other reactions will be available
so the user can enable them as needed.
For further information about the principles of runtime verification and
RV applied to Linux:
Bartocci, Ezio, et al. *Introduction to runtime verification.* In: Lectures on
Runtime Verification. Springer, Cham, 2018. p. 1-33.
Falcone, Ylies, et al. *A taxonomy for classifying runtime verification tools.*
In: International Conference on Runtime Verification. Springer, Cham, 2018. p.
241-262.
De Oliveira, Daniel Bristot. *Automata-based formal analysis and
verification of the real-time Linux kernel.* Ph.D. Thesis, 2020.
Online RV monitors
==================
Monitors can be classified as *offline* and *online* monitors. *Offline*
monitor process the traces generated by a system after the events, generally by
reading the trace execution from a permanent storage system. *Online* monitors
process the trace during the execution of the system. Online monitors are said
to be *synchronous* if the processing of an event is attached to the system
execution, blocking the system during the event monitoring. On the other hand,
an *asynchronous* monitor has its execution detached from the system. Each type
of monitor has a set of advantages. For example, *offline* monitors can be
executed on different machines but require operations to save the log to a
file. In contrast, *synchronous online* method can react at the exact moment
a violation occurs.
Another important aspect regarding monitors is the overhead associated with the
event analysis. If the system generates events at a frequency higher than the
monitor's ability to process them in the same system, only the *offline*
methods are viable. On the other hand, if the tracing of the events incurs
on higher overhead than the simple handling of an event by a monitor, then a
*synchronous online* monitors will incur on lower overhead.
Indeed, the research presented in:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva.
*Efficient formal verification for the Linux kernel.* In: International
Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
p. 315-332.
Shows that for Deterministic Automata models, the synchronous processing of
events in-kernel causes lower overhead than saving the same events to the trace
buffer, not even considering collecting the trace for user-space analysis.
This motivated the development of an in-kernel interface for online monitors.
For further information about modeling of Linux kernel behavior using automata,
see:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread
synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
Architecture, 2020, 107: 101729.
The user interface
==================
The user interface resembles the tracing interface (on purpose). It is
currently at "/sys/kernel/tracing/rv/".
The following files/folders are currently available:
**available_monitors**
- Reading list the available monitors, one per line
For example::
# cat available_monitors
wip
wwnr
**available_reactors**
- Reading shows the available reactors, one per line.
For example::
# cat available_reactors
nop
panic
printk
**enabled_monitors**:
- Reading lists the enabled monitors, one per line
- Writing to it enables a given monitor
- Writing a monitor name with a '!' prefix disables it
- Truncating the file disables all enabled monitors
For example::
# cat enabled_monitors
# echo wip > enabled_monitors
# echo wwnr >> enabled_monitors
# cat enabled_monitors
wip
wwnr
# echo '!wip' >> enabled_monitors
# cat enabled_monitors
wwnr
# echo > enabled_monitors
# cat enabled_monitors
#
Note that it is possible to enable more than one monitor concurrently.
**monitoring_on**
This is an on/off general switcher for monitoring. It resembles the
"tracing_on" switcher in the trace interface.
- Writing "0" stops the monitoring
- Writing "1" continues the monitoring
- Reading returns the current status of the monitoring
Note that it does not disable enabled monitors but stop the per-entity
monitors monitoring the events received from the system.
**reacting_on**
- Writing "0" prevents reactions for happening
- Writing "1" enable reactions
- Reading returns the current status of the reaction
**monitors/**
Each monitor will have its own directory inside "monitors/". There the
monitor-specific files will be presented. The "monitors/" directory resembles
the "events" directory on tracefs.
For example::
# cd monitors/wip/
# ls
desc enable
# cat desc
wakeup in preemptive per-cpu testing monitor.
# cat enable
0
**monitors/MONITOR/desc**
- Reading shows a description of the monitor *MONITOR*
**monitors/MONITOR/enable**
- Writing "0" disables the *MONITOR*
- Writing "1" enables the *MONITOR*
- Reading return the current status of the *MONITOR*
**monitors/MONITOR/reactors**
- List available reactors, with the select reaction for the given *MONITOR*
inside "[]". The default one is the nop (no operation) reactor.
- Writing the name of a reactor enables it to the given MONITOR.
For example::
# cat monitors/wip/reactors
[nop]
panic
printk
# echo panic > monitors/wip/reactors
# cat monitors/wip/reactors
nop
[panic]
printk