--- /dev/null
+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.
trace output as a reaction to event parsing and exceptions, as depicted
below::
- Linux +----- RV Monitor ----------------------------------+ Formal
- Realm | | Realm
+ Linux +---- RV Monitor ----------------------------------+ Formal
+ Realm | | Realm
+-------------------+ +----------------+ +-----------------+
| Linux kernel | | Monitor | | Reference |
| Tracing | -> | Instance(s) | <- | Model |
* 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
-----
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
-------------
projects / thirdparty / linux.git / commitdiff
