From e3c9fc78f096b83e81329b213c25fb9a376e373a Mon Sep 17 00:00:00 2001 From: Daniel Bristot de Oliveira Date: Fri, 29 Jul 2022 11:38:46 +0200 Subject: tools/rv: Add dot2c dot2c is a tool that transforms an automata in the graphiviz .dot file into an C representation of the automata. usage: dot2c [-h] dot_file dot2c: converts a .dot file into a C structure positional arguments: dot_file The dot file to be converted optional arguments: -h, --help show this help message and exit Link: https://lkml.kernel.org/r/b26204ba9509c80bcda31b76cdea31ddb188cd24.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) --- tools/verification/dot2/automata.py | 171 ++++++++++++++++++++++++++++++++++++ 1 file changed, 171 insertions(+) create mode 100644 tools/verification/dot2/automata.py (limited to 'tools/verification/dot2/automata.py') diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/automata.py new file mode 100644 index 000000000000..f22e1dff19ce --- /dev/null +++ b/tools/verification/dot2/automata.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira +# +# Automata object: parse an automata in dot file digraph format into a python object + +import ntpath + +class Automata: + """Automata class: Reads a dot file and part it as an automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + invalid_state_str = "INVALID_STATE" + + def __init__(self, file_path): + self.__dot_path = file_path + self.name = self.__get_model_name() + self.__dot_lines = self.__open_dot() + self.states, self.initial_state, self.final_states = self.__get_state_variables() + self.events = self.__get_event_variables() + self.function = self.__create_matrix() + + def __get_model_name(self): + basename = ntpath.basename(self.__dot_path) + if basename.endswith(".dot") == False: + print("not a dot file") + raise Exception("not a dot file: %s" % self.__dot_path) + + model_name = basename[0:-4] + if model_name.__len__() == 0: + raise Exception("not a dot file: %s" % self.__dot_path) + + return model_name + + def __open_dot(self): + cursor = 0 + dot_lines = [] + try: + dot_file = open(self.__dot_path) + except: + raise Exception("Cannot open the file: %s" % self.__dot_path) + + dot_lines = dot_file.read().splitlines() + dot_file.close() + + # checking the first line: + line = dot_lines[cursor].split() + + if (line[0] != "digraph") and (line[1] != "state_automaton"): + raise Exception("Not a valid .dot format: %s" % self.__dot_path) + else: + cursor += 1 + return dot_lines + + def __get_cursor_begin_states(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + return cursor + + def __get_cursor_begin_events(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + while self.__dot_lines[cursor].split()[0] == "{node": + cursor += 1 + # skip initial state transition + cursor += 1 + return cursor + + def __get_state_variables(self): + # wait for node declaration + states = [] + final_states = [] + + has_final_states = False + cursor = self.__get_cursor_begin_states() + + # process nodes + while self.__dot_lines[cursor].split()[0] == "{node": + line = self.__dot_lines[cursor].split() + raw_state = line[-1] + + # "enabled_fired"}; -> enabled_fired + state = raw_state.replace('"', '').replace('};', '').replace(',','_') + if state[0:7] == "__init_": + initial_state = state[7:] + else: + states.append(state) + if self.__dot_lines[cursor].__contains__("doublecircle") == True: + final_states.append(state) + has_final_states = True + + if self.__dot_lines[cursor].__contains__("ellipse") == True: + final_states.append(state) + has_final_states = True + + cursor += 1 + + states = sorted(set(states)) + states.remove(initial_state) + + # Insert the initial state at the bein og the states + states.insert(0, initial_state) + + if has_final_states == False: + final_states.append(initial_state) + + return states, initial_state, final_states + + def __get_event_variables(self): + # here we are at the begin of transitions, take a note, we will return later. + cursor = self.__get_cursor_begin_events() + + events = [] + while self.__dot_lines[cursor][1] == '"': + # transitions have the format: + # "all_fired" -> "both_fired" [ label = "disable_irq" ]; + # ------------ event is here ------------^^^^^ + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + event = line[-2].replace('"','') + + # when a transition has more than one lables, they are like this + # "local_irq_enable\nhw_local_irq_enable_n" + # so split them. + + event = event.replace("\\n", " ") + for i in event.split(): + events.append(i) + cursor += 1 + + return sorted(set(events)) + + def __create_matrix(self): + # transform the array into a dictionary + events = self.events + states = self.states + events_dict = {} + states_dict = {} + nr_event = 0 + for event in events: + events_dict[event] = nr_event + nr_event += 1 + + nr_state = 0 + for state in states: + states_dict[state] = nr_state + nr_state += 1 + + # declare the matrix.... + matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)] + + # and we are back! Let's fill the matrix + cursor = self.__get_cursor_begin_events() + + while self.__dot_lines[cursor][1] == '"': + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + origin_state = line[0].replace('"','').replace(',','_') + dest_state = line[2].replace('"','').replace(',','_') + possible_events = line[-2].replace('"','').replace("\\n", " ") + for event in possible_events.split(): + matrix[states_dict[origin_state]][events_dict[event]] = dest_state + cursor += 1 + + return matrix -- cgit v1.2.3 From 4041b9bbfbcddd239ff2c090f0da43bb3df7818c Mon Sep 17 00:00:00 2001 From: Daniel Bristot de Oliveira Date: Fri, 29 Jul 2022 11:38:47 +0200 Subject: Documentation/rv: Add deterministic automaton documentation Add documentation about deterministic automaton and its possible representations (formal, graphic, .dot and C). Link: https://lkml.kernel.org/r/387edaed87630bd5eb37c4275045dfd229700aa6.1659052063.git.bristot@kernel.org Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira Signed-off-by: Steven Rostedt (Google) --- Documentation/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 (limited to 'tools/verification/dot2/automata.py') 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 # # 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 -- cgit v1.2.3