1Hybrid Automata 2=============== 3 4Hybrid automata are an extension of deterministic automata, there are several 5definitions of hybrid automata in the literature. The adaptation implemented 6here 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 28The set of all possible constraints *C(V)* is defined according to the 29following grammar: 30 31 g = v < c | v > c | v <= c | v >= c | v == c | v != c | g && g | true 32 33With v a variable in *V* and c a numerical value. 34 35We define the special case of hybrid automata whose variables grow with uniform 36rates as timed automata. In this case, the variables are called clocks. 37As the name implies, timed automata can be used to describe real time. 38Additionally, clocks support another type of guard which always evaluates to true: 39 40 reset(v) 41 42The reset constraint is used to set the value of a clock to 0. 43 44The set of invariant constraints *C'(V)* is a subset of *C(V)* including only 45constraint of the form: 46 47 g = v < c | true 48 49This simplifies the implementation as a clock expiration is a necessary and 50sufficient condition for the violation of invariants while still allowing more 51complex constraints to be specified as guards. 52 53It is important to note that any hybrid automaton is a valid deterministic 54automaton with additional guards and invariants. Those can only further 55constrain what transitions are valid but it is not possible to define 56transition 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 59Examples 60-------- 61 62Wip as hybrid automaton 63~~~~~~~~~~~~~~~~~~~~~~~ 64 65The 'wip' (wakeup in preemptive) example introduced as a deterministic automaton 66can 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 78Which 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 89In this example, by using the preemptive state of the system as an environment 90variable, we can assert this constraint on ``sched_waking`` without requiring 91preemption events (as we would in a deterministic automaton), which can be 92useful in case those events are not available or not reliable on the system. 93 94Since all the invariants in *i* are true, we can omit them from the representation. 95 96Stall model with guards (iteration 1) 97~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 98 99As 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 112Graphically 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 133This model imposes that the time between when a task is enqueued (it becomes 134runnable) and when the task gets to run must be lower than a certain threshold. 135A failure in this model means that the task is starving. 136One problem in using guards on the edges in this case is that the model will 137not report a failure until the ``switch_in`` event occurs. This means that, 138according to the model, it is valid for the task never to run. 139 140Stall model with invariants (iteration 2) 141~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 142 143The 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 157Graphically:: 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 179In this case, we moved the guard as an invariant to the ``enqueued`` state, 180this means we not only forbid the occurrence of ``switch_in`` when ``clk`` is 181past 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 183as soon as a task is starving, rather than when the starving task finally runs. 184 185Hybrid Automaton in C 186--------------------- 187 188The definition of hybrid automata in C is heavily based on the deterministic 189automata one. Specifically, we add the set of environment variables and the 190constraints (both guards on transitions and invariants on states) as follows. 191This 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 271The function ``verify_constraint``, here reported as simplified, checks guards, 272performs resets and starts timers to validate invariants according to 273specification, those cannot easily be represented in the automaton struct. 274Due to the complex nature of environment variables, the user needs to provide 275functions to get and reset environment variables that are not common clocks 276(e.g. clocks with ns or jiffy granularity). 277Since invariants are only defined as clock expirations (e.g. *clk < 278threshold*), reaching the expiration of a timer armed when entering the state 279is in fact a failure in the model and triggers a reaction. Leaving the state 280stops the timer. 281 282It is important to note that timers implemented with hrtimers introduce 283overhead, if the monitor has several instances (e.g. all tasks) this can become 284an issue. The impact can be decreased using the timer wheel (``HA_TIMER_TYPE`` 285set to ``HA_TIMER_WHEEL``), this lowers the responsiveness of the timer without 286damaging the accuracy of the model, since the invariant condition is checked 287before disabling the timer in case the callback is late. 288Alternatively, if the monitor is guaranteed to *eventually* leave the state and 289the incurred delay to wait for the next event is acceptable, guards can be used 290in place of invariants, as seen in the stall example. 291 292Graphviz .dot format 293-------------------- 294 295Also the Graphviz representation of hybrid automata is an extension of the 296deterministic automata one. Specifically, guards can be provided in the event 297name separated by ``;``:: 298 299 "state_start" -> "state_dest" [ label = "sched_waking;preemptible==0;reset(clk)" ]; 300 301Invariant can be specified in the state label (not the node name!) separated by ``\n``:: 302 303 "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; 304 305Constraints can be specified as valid C comparisons and allow spaces, the first 306element of the comparison must be the clock while the second is a numerical or 307parametrised value. Guards allow comparisons to be combined with boolean 308operations (``&&`` and ``||``), resets must be separated from other constraints. 309 310This 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 330References 331---------- 332 333One 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 338Hybrid 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. 342