Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
kernel
os
linux
Documentation/rv: Add documentation about hybrid automata
Describe theory and implementation of hybrid automata in the dedicated
page hybrid_automata.rst
Include a section on how to integrate a hybrid automaton in
monitor_synthesis.rst
Also remove a hanging $ in deterministic_automata.rst
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Juri Lelli <juri.lelli@redhat.com>
Link: https://lore.kernel.org/r/20260330111010.153663-6-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
+458
-3
+1
-1
Documentation/trace/rv/deterministic_automata.rst
+1
-1
Documentation/trace/rv/deterministic_automata.rst
···
11
11
- *E* is the finite set of events;
12
12
- x\ :subscript:`0` is the initial state;
13
13
- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
14
-
- *f* : *X* x *E* -> *X* $ is the transition function. It defines the state
14
+
- *f* : *X* x *E* -> *X* is the transition function. It defines the state
15
15
transition in the occurrence of an event from *E* in the state *X*. In the
16
16
special case of deterministic automata, the occurrence of the event in *E*
17
17
in a state in *X* has a deterministic next state from *X*.
+341
Documentation/trace/rv/hybrid_automata.rst
+341
Documentation/trace/rv/hybrid_automata.rst
···
1
+
Hybrid Automata
2
+
===============
3
+
4
+
Hybrid automata are an extension of deterministic automata, there are several
5
+
definitions of hybrid automata in the literature. The adaptation implemented
6
+
here is formally denoted by G and defined as a 7-tuple:
7
+
8
+
*G* = { *X*, *E*, *V*, *f*, x\ :subscript:`0`, X\ :subscript:`m`, *i* }
9
+
10
+
- *X* is the set of states;
11
+
- *E* is the finite set of events;
12
+
- *V* is the finite set of environment variables;
13
+
- x\ :subscript:`0` is the initial state;
14
+
- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
15
+
- *f* : *X* x *E* x *C(V)* -> *X* is the transition function.
16
+
It defines the state transition in the occurrence of an event from *E* in the
17
+
state *X*. Unlike deterministic automata, the transition function also
18
+
includes guards from the set of all possible constraints (defined as *C(V)*).
19
+
Guards can be true or false with the valuation of *V* when the event occurs,
20
+
and the transition is possible only when constraints are true. Similarly to
21
+
deterministic automata, the occurrence of the event in *E* in a state in *X*
22
+
has a deterministic next state from *X*, if the guard is true.
23
+
- *i* : *X* -> *C'(V)* is the invariant assignment function, this is a
24
+
constraint assigned to each state in *X*, every state in *X* must be left
25
+
before the invariant turns to false. We can omit the representation of
26
+
invariants whose value is true regardless of the valuation of *V*.
27
+
28
+
The set of all possible constraints *C(V)* is defined according to the
29
+
following grammar:
30
+
31
+
g = v < c | v > c | v <= c | v >= c | v == c | v != c | g && g | true
32
+
33
+
With v a variable in *V* and c a numerical value.
34
+
35
+
We define the special case of hybrid automata whose variables grow with uniform
36
+
rates as timed automata. In this case, the variables are called clocks.
37
+
As the name implies, timed automata can be used to describe real time.
38
+
Additionally, clocks support another type of guard which always evaluates to true:
39
+
40
+
reset(v)
41
+
42
+
The reset constraint is used to set the value of a clock to 0.
43
+
44
+
The set of invariant constraints *C'(V)* is a subset of *C(V)* including only
45
+
constraint of the form:
46
+
47
+
g = v < c | true
48
+
49
+
This simplifies the implementation as a clock expiration is a necessary and
50
+
sufficient condition for the violation of invariants while still allowing more
51
+
complex constraints to be specified as guards.
52
+
53
+
It is important to note that any hybrid automaton is a valid deterministic
54
+
automaton with additional guards and invariants. Those can only further
55
+
constrain what transitions are valid but it is not possible to define
56
+
transition functions starting from the same state in *X* and the same event in
57
+
*E* but ending up in different states in *X* based on the valuation of *V*.
58
+
59
+
Examples
60
+
--------
61
+
62
+
Wip as hybrid automaton
63
+
~~~~~~~~~~~~~~~~~~~~~~~
64
+
65
+
The 'wip' (wakeup in preemptive) example introduced as a deterministic automaton
66
+
can also be described as:
67
+
68
+
- *X* = { ``any_thread_running`` }
69
+
- *E* = { ``sched_waking`` }
70
+
- *V* = { ``preemptive`` }
71
+
- x\ :subscript:`0` = ``any_thread_running``
72
+
- X\ :subscript:`m` = {``any_thread_running``}
73
+
- *f* =
74
+
- *f*\ (``any_thread_running``, ``sched_waking``, ``preemptive==0``) = ``any_thread_running``
75
+
- *i* =
76
+
- *i*\ (``any_thread_running``) = ``true``
77
+
78
+
Which can be represented graphically as::
79
+
80
+
|
81
+
|
82
+
v
83
+
#====================# sched_waking;preemptive==0
84
+
H H ------------------------------+
85
+
H any_thread_running H |
86
+
H H <-----------------------------+
87
+
#====================#
88
+
89
+
In this example, by using the preemptive state of the system as an environment
90
+
variable, we can assert this constraint on ``sched_waking`` without requiring
91
+
preemption events (as we would in a deterministic automaton), which can be
92
+
useful in case those events are not available or not reliable on the system.
93
+
94
+
Since all the invariants in *i* are true, we can omit them from the representation.
95
+
96
+
Stall model with guards (iteration 1)
97
+
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
98
+
99
+
As a sample timed automaton we can define 'stall' as:
100
+
101
+
- *X* = { ``dequeued``, ``enqueued``, ``running``}
102
+
- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
103
+
- *V* = { ``clk`` }
104
+
- x\ :subscript:`0` = ``dequeue``
105
+
- X\ :subscript:`m` = {``dequeue``}
106
+
- *f* =
107
+
- *f*\ (``enqueued``, ``switch_in``, ``clk < threshold``) = ``running``
108
+
- *f*\ (``running``, ``dequeue``) = ``dequeued``
109
+
- *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
110
+
- *i* = *omitted as all true*
111
+
112
+
Graphically represented as::
113
+
114
+
|
115
+
|
116
+
v
117
+
#============================#
118
+
H dequeued H <+
119
+
#============================# |
120
+
| |
121
+
| enqueue; reset(clk) |
122
+
v |
123
+
+----------------------------+ |
124
+
| enqueued | | dequeue
125
+
+----------------------------+ |
126
+
| |
127
+
| switch_in; clk < threshold |
128
+
v |
129
+
+----------------------------+ |
130
+
| running | -+
131
+
+----------------------------+
132
+
133
+
This model imposes that the time between when a task is enqueued (it becomes
134
+
runnable) and when the task gets to run must be lower than a certain threshold.
135
+
A failure in this model means that the task is starving.
136
+
One problem in using guards on the edges in this case is that the model will
137
+
not report a failure until the ``switch_in`` event occurs. This means that,
138
+
according to the model, it is valid for the task never to run.
139
+
140
+
Stall model with invariants (iteration 2)
141
+
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
142
+
143
+
The first iteration isn't exactly what was intended, we can change the model as:
144
+
145
+
- *X* = { ``dequeued``, ``enqueued``, ``running``}
146
+
- *E* = { ``enqueue``, ``dequeue``, ``switch_in``}
147
+
- *V* = { ``clk`` }
148
+
- x\ :subscript:`0` = ``dequeue``
149
+
- X\ :subscript:`m` = {``dequeue``}
150
+
- *f* =
151
+
- *f*\ (``enqueued``, ``switch_in``) = ``running``
152
+
- *f*\ (``running``, ``dequeue``) = ``dequeued``
153
+
- *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued``
154
+
- *i* =
155
+
- *i*\ (``enqueued``) = ``clk < threshold``
156
+
157
+
Graphically::
158
+
159
+
|
160
+
|
161
+
v
162
+
#=========================#
163
+
H dequeued H <+
164
+
#=========================# |
165
+
| |
166
+
| enqueue; reset(clk) |
167
+
v |
168
+
+-------------------------+ |
169
+
| enqueued | |
170
+
| clk < threshold | | dequeue
171
+
+-------------------------+ |
172
+
| |
173
+
| switch_in |
174
+
v |
175
+
+-------------------------+ |
176
+
| running | -+
177
+
+-------------------------+
178
+
179
+
In this case, we moved the guard as an invariant to the ``enqueued`` state,
180
+
this means we not only forbid the occurrence of ``switch_in`` when ``clk`` is
181
+
past the threshold but also mark as invalid in case we are *still* in
182
+
``enqueued`` after the threshold. This model is effectively in an invalid state
183
+
as soon as a task is starving, rather than when the starving task finally runs.
184
+
185
+
Hybrid Automaton in C
186
+
---------------------
187
+
188
+
The definition of hybrid automata in C is heavily based on the deterministic
189
+
automata one. Specifically, we add the set of environment variables and the
190
+
constraints (both guards on transitions and invariants on states) as follows.
191
+
This is a combination of both iterations of the stall example::
192
+
193
+
/* enum representation of X (set of states) to be used as index */
194
+
enum states {
195
+
dequeued,
196
+
enqueued,
197
+
running,
198
+
state_max,
199
+
};
200
+
201
+
#define INVALID_STATE state_max
202
+
203
+
/* enum representation of E (set of events) to be used as index */
204
+
enum events {
205
+
dequeue,
206
+
enqueue,
207
+
switch_in,
208
+
event_max,
209
+
};
210
+
211
+
/* enum representation of V (set of environment variables) to be used as index */
212
+
enum envs {
213
+
clk,
214
+
env_max,
215
+
env_max_stored = env_max,
216
+
};
217
+
218
+
struct automaton {
219
+
char *state_names[state_max]; // X: the set of states
220
+
char *event_names[event_max]; // E: the finite set of events
221
+
char *env_names[env_max]; // V: the finite set of env vars
222
+
unsigned char function[state_max][event_max]; // f: transition function
223
+
unsigned char initial_state; // x_0: the initial state
224
+
bool final_states[state_max]; // X_m: the set of marked states
225
+
};
226
+
227
+
struct automaton aut = {
228
+
.state_names = {
229
+
"dequeued",
230
+
"enqueued",
231
+
"running",
232
+
},
233
+
.event_names = {
234
+
"dequeue",
235
+
"enqueue",
236
+
"switch_in",
237
+
},
238
+
.env_names = {
239
+
"clk",
240
+
},
241
+
.function = {
242
+
{ INVALID_STATE, enqueued, INVALID_STATE },
243
+
{ INVALID_STATE, INVALID_STATE, running },
244
+
{ dequeued, INVALID_STATE, INVALID_STATE },
245
+
},
246
+
.initial_state = dequeued,
247
+
.final_states = { 1, 0, 0 },
248
+
};
249
+
250
+
static bool verify_constraint(enum states curr_state, enum events event,
251
+
enum states next_state)
252
+
{
253
+
bool res = true;
254
+
255
+
/* Validate guards as part of f */
256
+
if (curr_state == enqueued && event == switch_in)
257
+
res = get_env(clk) < threshold;
258
+
else if (curr_state == dequeued && event == enqueue)
259
+
reset_env(clk);
260
+
261
+
/* Validate invariants in i */
262
+
if (next_state == curr_state || !res)
263
+
return res;
264
+
if (next_state == enqueued)
265
+
ha_start_timer_jiffy(ha_mon, clk, threshold_jiffies);
266
+
else if (curr_state == enqueued)
267
+
res = !ha_cancel_timer(ha_mon);
268
+
return res;
269
+
}
270
+
271
+
The function ``verify_constraint``, here reported as simplified, checks guards,
272
+
performs resets and starts timers to validate invariants according to
273
+
specification, those cannot easily be represented in the automaton struct.
274
+
Due to the complex nature of environment variables, the user needs to provide
275
+
functions to get and reset environment variables that are not common clocks
276
+
(e.g. clocks with ns or jiffy granularity).
277
+
Since invariants are only defined as clock expirations (e.g. *clk <
278
+
threshold*), reaching the expiration of a timer armed when entering the state
279
+
is in fact a failure in the model and triggers a reaction. Leaving the state
280
+
stops the timer.
281
+
282
+
It is important to note that timers implemented with hrtimers introduce
283
+
overhead, if the monitor has several instances (e.g. all tasks) this can become
284
+
an issue. The impact can be decreased using the timer wheel (``HA_TIMER_TYPE``
285
+
set to ``HA_TIMER_WHEEL``), this lowers the responsiveness of the timer without
286
+
damaging the accuracy of the model, since the invariant condition is checked
287
+
before disabling the timer in case the callback is late.
288
+
Alternatively, if the monitor is guaranteed to *eventually* leave the state and
289
+
the incurred delay to wait for the next event is acceptable, guards can be used
290
+
in place of invariants, as seen in the stall example.
291
+
292
+
Graphviz .dot format
293
+
--------------------
294
+
295
+
Also the Graphviz representation of hybrid automata is an extension of the
296
+
deterministic automata one. Specifically, guards can be provided in the event
297
+
name separated by ``;``::
298
+
299
+
"state_start" -> "state_dest" [ label = "sched_waking;preemptible==0;reset(clk)" ];
300
+
301
+
Invariant can be specified in the state label (not the node name!) separated by ``\n``::
302
+
303
+
"enqueued" [label = "enqueued\nclk < threshold_jiffies"];
304
+
305
+
Constraints can be specified as valid C comparisons and allow spaces, the first
306
+
element of the comparison must be the clock while the second is a numerical or
307
+
parametrised value. Guards allow comparisons to be combined with boolean
308
+
operations (``&&`` and ``||``), resets must be separated from other constraints.
309
+
310
+
This is the full example of the last version of the 'stall' model in DOT::
311
+
312
+
digraph state_automaton {
313
+
{node [shape = circle] "enqueued"};
314
+
{node [shape = plaintext, style=invis, label=""] "__init_dequeued"};
315
+
{node [shape = doublecircle] "dequeued"};
316
+
{node [shape = circle] "running"};
317
+
"__init_dequeued" -> "dequeued";
318
+
"enqueued" [label = "enqueued\nclk < threshold_jiffies"];
319
+
"running" [label = "running"];
320
+
"dequeued" [label = "dequeued"];
321
+
"enqueued" -> "running" [ label = "switch_in" ];
322
+
"running" -> "dequeued" [ label = "dequeue" ];
323
+
"dequeued" -> "enqueued" [ label = "enqueue;reset(clk)" ];
324
+
{ rank = min ;
325
+
"__init_dequeued";
326
+
"dequeued";
327
+
}
328
+
}
329
+
330
+
References
331
+
----------
332
+
333
+
One book covering model checking and timed automata is::
334
+
335
+
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking,
336
+
The MIT Press, 2008.
337
+
338
+
Hybrid automata are described in detail in::
339
+
340
+
Thomas Henzinger: The theory of hybrid automata,
341
+
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996.
+1
Documentation/trace/rv/index.rst
+1
Documentation/trace/rv/index.rst
+115
-2
Documentation/trace/rv/monitor_synthesis.rst
+115
-2
Documentation/trace/rv/monitor_synthesis.rst
···
18
18
trace output as a reaction to event parsing and exceptions, as depicted
19
19
below::
20
20
21
-
Linux +----- RV Monitor ----------------------------------+ Formal
22
-
Realm | | Realm
21
+
Linux +---- RV Monitor ----------------------------------+ Formal
22
+
Realm | | Realm
23
23
+-------------------+ +----------------+ +-----------------+
24
24
| Linux kernel | | Monitor | | Reference |
25
25
| Tracing | -> | Instance(s) | <- | Model |
···
45
45
46
46
* rv/da_monitor.h for deterministic automaton monitor.
47
47
* rv/ltl_monitor.h for linear temporal logic monitor.
48
+
* rv/ha_monitor.h for hybrid automaton monitor.
48
49
49
50
rvgen
50
51
-----
···
252
251
the task, the monitor may need some time to start validating tasks which have
253
252
been running before the monitor is enabled. Therefore, it is recommended to
254
253
start the tasks of interest after enabling the monitor.
254
+
255
+
rv/ha_monitor.h
256
+
+++++++++++++++
257
+
258
+
The implementation of hybrid automaton monitors derives directly from the
259
+
deterministic automaton one. Despite using a different header
260
+
(``ha_monitor.h``) the functions to handle events are the same (e.g.
261
+
``da_handle_event``).
262
+
263
+
Additionally, the `rvgen` tool populates skeletons for the
264
+
``ha_verify_constraint``, ``ha_get_env`` and ``ha_reset_env`` based on the
265
+
monitor specification in the monitor source file.
266
+
267
+
``ha_verify_constraint`` is typically ready as it is generated by `rvgen`:
268
+
269
+
* standard constraints on edges are turned into the form::
270
+
271
+
res = ha_get_env(ha_mon, ENV) < VALUE;
272
+
273
+
* reset constraints are turned into the form::
274
+
275
+
ha_reset_env(ha_mon, ENV);
276
+
277
+
* constraints on the state are implemented using timers
278
+
279
+
- armed before entering the state
280
+
281
+
- cancelled while entering any other state
282
+
283
+
- untouched if the state does not change as a result of the event
284
+
285
+
- checked if the timer expired but the callback did not run
286
+
287
+
- available implementation are `HA_TIMER_HRTIMER` and `HA_TIMER_WHEEL`
288
+
289
+
- hrtimers are more precise but may have higher overhead
290
+
291
+
- select by defining `HA_TIMER_TYPE` before including the header::
292
+
293
+
#define HA_TIMER_TYPE HA_TIMER_HRTIMER
294
+
295
+
Constraint values can be specified in different forms:
296
+
297
+
* literal value (with optional unit). E.g.::
298
+
299
+
preemptive == 0
300
+
clk < 100ns
301
+
threshold <= 10j
302
+
303
+
* constant value (uppercase string). E.g.::
304
+
305
+
clk < MAX_NS
306
+
307
+
* parameter (lowercase string). E.g.::
308
+
309
+
clk <= threshold_jiffies
310
+
311
+
* macro (uppercase string with parentheses). E.g.::
312
+
313
+
clk < MAX_NS()
314
+
315
+
* function (lowercase string with parentheses). E.g.::
316
+
317
+
clk <= threshold_jiffies()
318
+
319
+
In all cases, `rvgen` will try to understand the type of the environment
320
+
variable from the name or unit. For instance, constants or parameters
321
+
terminating with ``_NS`` or ``_jiffies`` are intended as clocks with ns and jiffy
322
+
granularity, respectively. Literals with measure unit `j` are jiffies and if a
323
+
time unit is specified (`ns` to `s`), `rvgen` will convert the value to `ns`.
324
+
325
+
Constants need to be defined by the user (but unlike the name, they don't
326
+
necessarily need to be defined as constants). Parameters get converted to
327
+
module parameters and the user needs to provide a default value.
328
+
Also function and macros are defined by the user, by default they get as an
329
+
argument the ``ha_monitor``, a common usage would be to get the required value
330
+
from the target, e.g. the task in per-task monitors, using the helper
331
+
``ha_get_target(ha_mon)``.
332
+
333
+
If `rvgen` determines that the variable is a clock, it provides the getter and
334
+
resetter based on the unit. Otherwise, the user needs to provide an appropriate
335
+
definition.
336
+
Typically non-clock environment variables are not reset. In such case only the
337
+
getter skeleton will be present in the file generated by `rvgen`.
338
+
For instance, the getter for preemptive can be filled as::
339
+
340
+
static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs env)
341
+
{
342
+
if (env == preemptible)
343
+
return preempt_count() == 0;
344
+
return ENV_INVALID_VALUE;
345
+
}
346
+
347
+
The function is supplied the ``ha_mon`` parameter in case some storage is
348
+
required (as it is for clocks), but environment variables without reset do not
349
+
require a storage and can ignore that argument.
350
+
The number of environment variables requiring a storage is limited by
351
+
``MAX_HA_ENV_LEN``, however such limitation doesn't stand for other variables.
352
+
353
+
Finally, constraints on states are only valid for clocks and only if the
354
+
constraint is of the form `clk < N`. This is because such constraints are
355
+
implemented with the expiration of a timer.
356
+
Typically the clock variables are reset just before arming the timer, but this
357
+
doesn't have to be the case and the available functions take care of it.
358
+
It is a responsibility of per-task monitors to make sure no timer is left
359
+
running when the task exits.
360
+
361
+
By default the generator implements timers with hrtimers (setting
362
+
``HA_TIMER_TYPE`` to ``HA_TIMER_HRTIMER``), this gives better responsiveness
363
+
but higher overhead. The timer wheel (``HA_TIMER_WHEEL``) is a good alternative
364
+
for monitors with several instances (e.g. per-task) that achieves lower
365
+
overhead with increased latency, yet without compromising precision.
255
366
256
367
Final remarks
257
368
-------------