Documentation/trace/rv/deterministic_automata.rst

   1 Deterministic Automata
   2 ======================
   3
   4 Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
   5
   6         *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
   7
   8 where:
   9
  10 - *X* is the set of states;
  11 - *E* is the finite set of events;
  12 - x\ :subscript:`0` is the initial state;
  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
  15   transition in the occurrence of an event from *E* in the state *X*. In the
  16   special case of deterministic automata, the occurrence of the event in *E*
  17   in a state in *X* has a deterministic next state from *X*.
  18
  19 For example, a given automaton named 'wip' (wakeup in preemptive) can
  20 be defined as:
  21
  22 - *X* = { ``preemptive``, ``non_preemptive``}
  23 - *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
  24 - x\ :subscript:`0` = ``preemptive``
  25 - X\ :subscript:`m` = {``preemptive``}
  26 - *f* =
  27    - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
  28    - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
  29    - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
  30
  31 One of the benefits of this formal definition is that it can be presented
  32 in multiple formats. For example, using a *graphical representation*, using
  33 vertices (nodes) and edges, which is very intuitive for *operating system*
  34 practitioners, without any loss.
  35
  36 The previous 'wip' automaton can also be represented as::
  37
  38                        preempt_enable
  39           +---------------------------------+
  40           v                                 |
  41         #============#  preempt_disable   +------------------+
  42     --> H preemptive H -----------------> |  non_preemptive  |
  43         #============#                    +------------------+
  44                                             ^              |
  45                                             | sched_waking |
  46                                             +--------------+
  47
  48 Deterministic Automaton in C
  49 ----------------------------
  50
  51 In the paper "Efficient formal verification for the Linux kernel",
  52 the authors present a simple way to represent an automaton in C that can
  53 be used as regular code in the Linux kernel.
  54
  55 For example, the 'wip' automata can be presented as (augmented with comments)::
  56
  57   /* enum representation of X (set of states) to be used as index */
  58   enum states {
  59         preemptive = 0,
  60         non_preemptive,
  61         state_max
  62   };
  63
  64   #define INVALID_STATE state_max
  65
  66   /* enum representation of E (set of events) to be used as index */
  67   enum events {
  68         preempt_disable = 0,
  69         preempt_enable,
  70         sched_waking,
  71         event_max
  72   };
  73
  74   struct automaton {
  75         char *state_names[state_max];                   // X: the set of states
  76         char *event_names[event_max];                   // E: the finite set of events
  77         unsigned char function[state_max][event_max];   // f: transition function
  78         unsigned char initial_state;                    // x_0: the initial state
  79         bool final_states[state_max];                   // X_m: the set of marked states
  80   };
  81
  82   struct automaton aut = {
  83         .state_names = {
  84                 "preemptive",
  85                 "non_preemptive"
  86         },
  87         .event_names = {
  88                 "preempt_disable",
  89                 "preempt_enable",
  90                 "sched_waking"
  91         },
  92         .function = {
  93                 { non_preemptive,  INVALID_STATE,  INVALID_STATE },
  94                 {  INVALID_STATE,     preemptive, non_preemptive },
  95         },
  96         .initial_state = preemptive,
  97         .final_states = { 1, 0 },
  98   };
  99
 100 The *transition function* is represented as a matrix of states (lines) and
 101 events (columns), and so the function *f* : *X* x *E* -> *X* can be solved
 102 in O(1). For example::
 103
 104   next_state = automaton_wip.function[curr_state][event];
 105
 106 Graphviz .dot format
 107 --------------------
 108
 109 The Graphviz open-source tool can produce the graphical representation
 110 of an automaton using the (textual) DOT language as the source code.
 111 The DOT format is widely used and can be converted to many other formats.
 112
 113 For example, this is the 'wip' model in DOT::
 114
 115   digraph state_automaton {
 116         {node [shape = circle] "non_preemptive"};
 117         {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
 118         {node [shape = doublecircle] "preemptive"};
 119         {node [shape = circle] "preemptive"};
 120         "__init_preemptive" -> "preemptive";
 121         "non_preemptive" [label = "non_preemptive"];
 122         "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
 123         "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
 124         "preemptive" [label = "preemptive"];
 125         "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
 126         { rank = min ;
 127                 "__init_preemptive";
 128                 "preemptive";
 129         }
 130   }
 131
 132 This DOT format can be transformed into a bitmap or vectorial image
 133 using the dot utility, or into an ASCII art using graph-easy. For
 134 instance::
 135
 136   $ dot -Tsvg -o wip.svg wip.dot
 137   $ graph-easy wip.dot > wip.txt
 138
 139 dot2c
 140 -----
 141
 142 dot2c is a utility that can parse a .dot file containing an automaton as
 143 in the example above and automatically convert it to the C representation
 144 presented in [3].
 145
 146 For example, having the previous 'wip' model into a file named 'wip.dot',
 147 the following command will transform the .dot file into the C
 148 representation (previously shown) in the 'wip.h' file::
 149
 150   $ dot2c wip.dot > wip.h
 151
 152 The 'wip.h' content is the code sample in section 'Deterministic Automaton
 153 in C'.
 154
 155 Remarks
 156 -------
 157
 158 The automata formalism allows modeling discrete event systems (DES) in
 159 multiple formats, suitable for different applications/users.
 160
 161 For example, the formal description using set theory is better suitable
 162 for automata operations, while the graphical format for human interpretation;
 163 and computer languages for machine execution.
 164
 165 References
 166 ----------
 167
 168 Many textbooks cover automata formalism. For a brief introduction see::
 169
 170   O'Regan, Gerard. Concise guide to software engineering. Springer,
 171   Cham, 2017.
 172
 173 For a detailed description, including operations, and application on Discrete
 174 Event Systems (DES), see::
 175
 176   Cassandras, Christos G., and Stephane Lafortune, eds. Introduction to discrete
 177   event systems. Boston, MA: Springer US, 2008.
 178
 179 For the C representation in kernel, see::
 180
 181   De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
 182   Silva. Efficient formal verification for the Linux kernel. In:
 183   International Conference on Software Engineering and Formal Methods.
 184   Springer, Cham, 2019. p. 315-332.