diff options
Diffstat (limited to 'Documentation/trace/rv')
| -rw-r--r-- | Documentation/trace/rv/da_monitor_instrumentation.rst | 171 | ||||
| -rw-r--r-- | Documentation/trace/rv/deterministic_automata.rst | 184 | ||||
| -rw-r--r-- | Documentation/trace/rv/hybrid_automata.rst | 341 | ||||
| -rw-r--r-- | Documentation/trace/rv/index.rst | 20 | ||||
| -rw-r--r-- | Documentation/trace/rv/linear_temporal_logic.rst | 134 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_deadline.rst | 84 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_rtapp.rst | 152 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_sched.rst | 371 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_stall.rst | 43 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_synthesis.rst | 382 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_wip.rst | 55 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_wwnr.rst | 45 | ||||
| -rw-r--r-- | Documentation/trace/rv/runtime-verification.rst | 231 |
13 files changed, 2213 insertions, 0 deletions
diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst new file mode 100644 index 000000000..9eff38a4a --- /dev/null +++ b/Documentation/trace/rv/da_monitor_instrumentation.rst @@ -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 diff --git a/Documentation/trace/rv/deterministic_automata.rst b/Documentation/trace/rv/deterministic_automata.rst new file mode 100644 index 000000000..7a1c2b20e --- /dev/null +++ b/Documentation/trace/rv/deterministic_automata.rst @@ -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. diff --git a/Documentation/trace/rv/hybrid_automata.rst b/Documentation/trace/rv/hybrid_automata.rst new file mode 100644 index 000000000..f20d489f1 --- /dev/null +++ b/Documentation/trace/rv/hybrid_automata.rst @@ -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. diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst new file mode 100644 index 000000000..29769f06b --- /dev/null +++ b/Documentation/trace/rv/index.rst @@ -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 diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst new file mode 100644 index 000000000..9eee09d9c --- /dev/null +++ b/Documentation/trace/rv/linear_temporal_logic.rst @@ -0,0 +1,134 @@ +Linear temporal logic +===================== + +Introduction +------------ + +Runtime verification monitor is a verification technique which checks that the +kernel follows a specification. It does so by using tracepoints to monitor the +kernel's execution trace, and verifying that the execution trace sastifies the +specification. + +Initially, the specification can only be written in the form of deterministic +automaton (DA). However, while attempting to implement DA monitors for some +complex specifications, deterministic automaton is found to be inappropriate as +the specification language. The automaton is complicated, hard to understand, +and error-prone. + +Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type +of monitor uses LTL as specification instead of DA. For some cases, writing the +specification as LTL is more concise and intuitive. + +Many materials explain LTL in details. One book is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT + Press, 2008. + +Grammar +------- + +Unlike some existing syntax, kernel's implementation of LTL is more verbose. +This is motivated by considering that the people who read the LTL specifications +may not be well-versed in LTL. + +Grammar: + ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl + +Operands (opd): + true, false, user-defined names consisting of upper-case characters, digits, + and underscore. + +Unary Operators (unop): + always + eventually + next + not + +Binary Operators (binop): + until + and + or + imply + equivalent + +This grammar is ambiguous: operator precedence is not defined. Parentheses must +be used. + +Example linear temporal logic +----------------------------- +.. code-block:: + + RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA) + +means: if it is raining, going outside means having an umbrella. + +.. code-block:: + + RAIN imply (WET until not RAIN) + +means: if it is raining, it is going to be wet until the rain stops. + +.. code-block:: + + RAIN imply eventually not RAIN + +means: if it is raining, rain will eventually stop. + +The above examples are referring to the current time instance only. For kernel +verification, the `always` operator is usually desirable, to specify that +something is always true at the present and for all future. For example:: + + always (RAIN imply eventually not RAIN) + +means: *all* rain eventually stops. + +In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the +"atomic propositions". + +Monitor synthesis +----------------- + +To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used: +`tools/verification/rvgen`. The specification needs to be provided as a file, +and it must have a "RULE = LTL" assignment. For example:: + + RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE)) + +which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or +`CRASHED`. + +The LTL can be broken down using sub-expressions. The above is equivalent to: + + .. code-block:: + + RULE = always (ACQUIRE imply (ALIVE until RELEASE)) + ALIVE = not KILLED and not CRASHED + +From this specification, `rvgen` generates the C implementation of a Buchi +automaton - a non-deterministic state machine which checks the satisfiability of +the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using +`rvgen`. + +References +---------- + +One book covering model checking and linear temporal logic is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT + Press, 2008. + +For an example of using linear temporal logic in software testing, see:: + + Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury. + 2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the + 44th International Conference on Software Engineering (ICSE '22). Association + for Computing Machinery, New York, NY, USA, 1343–1355. + https://doi.org/10.1145/3510003.3510082 + +The kernel's LTL monitor implementation is based on:: + + Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly + Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa, + M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP + Advances in Information and Communication Technology. Springer, Boston, MA. + https://doi.org/10.1007/978-0-387-34892-6_1 diff --git a/Documentation/trace/rv/monitor_deadline.rst b/Documentation/trace/rv/monitor_deadline.rst new file mode 100644 index 000000000..84506ed1e --- /dev/null +++ b/Documentation/trace/rv/monitor_deadline.rst @@ -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 ------+ diff --git a/Documentation/trace/rv/monitor_rtapp.rst b/Documentation/trace/rv/monitor_rtapp.rst new file mode 100644 index 000000000..b95994ade --- /dev/null +++ b/Documentation/trace/rv/monitor_rtapp.rst @@ -0,0 +1,152 @@ +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). 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 + 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. + - 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: + + - 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 and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + + 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 not NANOSLEEP_CLOCK_REALTIME + + RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + + ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI + +`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: + + - `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`. + +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. diff --git a/Documentation/trace/rv/monitor_sched.rst b/Documentation/trace/rv/monitor_sched.rst new file mode 100644 index 000000000..d3ba7edc2 --- /dev/null +++ b/Documentation/trace/rv/monitor_sched.rst @@ -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. diff --git a/Documentation/trace/rv/monitor_stall.rst b/Documentation/trace/rv/monitor_stall.rst new file mode 100644 index 000000000..d29e820b2 --- /dev/null +++ b/Documentation/trace/rv/monitor_stall.rst @@ -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 diff --git a/Documentation/trace/rv/monitor_synthesis.rst b/Documentation/trace/rv/monitor_synthesis.rst new file mode 100644 index 000000000..2c1b5a0ae --- /dev/null +++ b/Documentation/trace/rv/monitor_synthesis.rst @@ -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. diff --git a/Documentation/trace/rv/monitor_wip.rst b/Documentation/trace/rv/monitor_wip.rst new file mode 100644 index 000000000..a95763438 --- /dev/null +++ b/Documentation/trace/rv/monitor_wip.rst @@ -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 diff --git a/Documentation/trace/rv/monitor_wwnr.rst b/Documentation/trace/rv/monitor_wwnr.rst new file mode 100644 index 000000000..9f739030f --- /dev/null +++ b/Documentation/trace/rv/monitor_wwnr.rst @@ -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 diff --git a/Documentation/trace/rv/runtime-verification.rst b/Documentation/trace/rv/runtime-verification.rst new file mode 100644 index 000000000..c700dde92 --- /dev/null +++ b/Documentation/trace/rv/runtime-verification.rst @@ -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 |