Add documentation about deterministic automaton and its possible
representations (formal, graphic, .dot and C).
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: Tao Zhou <[email protected]>
Cc: Randy Dunlap <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
.../trace/rv/deterministic_automata.rst | 184 ++++++++++++++++++
Documentation/trace/rv/index.rst | 1 +
tools/verification/dot2/automata.py | 3 +
tools/verification/dot2/dot2c | 3 +
tools/verification/dot2/dot2c.py | 3 +
5 files changed, 194 insertions(+)
create mode 100644 Documentation/trace/rv/deterministic_automata.rst
diff --git a/Documentation/trace/rv/deterministic_automata.rst b/Documentation/trace/rv/deterministic_automata.rst
new file mode 100644
index 000000000000..d0638f95a455
--- /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/index.rst b/Documentation/trace/rv/index.rst
index b54e49b1d0de..013a41a410cf 100644
--- a/Documentation/trace/rv/index.rst
+++ b/Documentation/trace/rv/index.rst
@@ -7,3 +7,4 @@ Runtime Verification
:glob:
runtime-verification.rst
+ deterministic_automata.rst
diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/automata.py
index f22e1dff19ce..baffeb960ff0 100644
--- a/tools/verification/dot2/automata.py
+++ b/tools/verification/dot2/automata.py
@@ -4,6 +4,9 @@
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
#
# Automata object: parse an automata in dot file digraph format into a python object
+#
+# For further information, see:
+# Documentation/trace/rv/deterministic_automata.rst
import ntpath
diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c
index 8a8cd84bdfcf..3fe89ab88b65 100644
--- a/tools/verification/dot2/dot2c
+++ b/tools/verification/dot2/dot2c
@@ -9,6 +9,9 @@
# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
# "Efficient Formal Verification for the Linux Kernel." International
# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+# Documentation/trace/rv/deterministic_automata.rst
if __name__ == '__main__':
from dot2 import dot2c
diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2c.py
index bca902eec483..fa73353f7e56 100644
--- a/tools/verification/dot2/dot2c.py
+++ b/tools/verification/dot2/dot2c.py
@@ -9,6 +9,9 @@
# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
# "Efficient Formal Verification for the Linux Kernel." International
# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+# Documentation/trace/rv/deterministic_automata.rst
from dot2.automata import Automata
--
2.35.1