결정적 오토마타

형식 정의와 wip 예제

형식적으로 `G`로 나타내는 결정적 오토마타는 5-튜플 `G = { X, E, f, x₀, Xₘ }`로 정의한다.

결정적 오토마타에서는 어떤 state에서 특정 event가 발생하면 다음 state가 하나로 결정된다.

`wip`(wakeup in preemptive) 오토마타는 state `preemptive`, `non_preemptive`, event `preempt_enable`, `preempt_disable`, `sched_waking`을 갖는다. initial·marked state는 모두 `preemptive`다.

형식 정의의 장점은 정보를 잃지 않고 여러 표현으로 나타낼 수 있다는 것이다. 예를 들어 정점과 간선으로 된 그래프는 운영체제 실무자가 직관적으로 이해하기 좋다.

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 |
                                            +--------------+

C 표현

논문 ‘Efficient formal verification for the Linux kernel’은 Linux kernel에서 일반 코드처럼 사용할 수 있는 간단한 C 오토마타 표현을 제시한다.

`wip`에서는 `enum states`와 `enum events`가 각각 `X`와 `E`를 배열 index로 바꾸며 `INVALID_STATE`는 정의되지 않은 transition을 표시한다. `struct automaton`은 state·event 이름, 2차원 transition matrix, initial state, final state bitmap을 보관한다.

  /* 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 },
  };

transition function은 행이 state, 열이 event인 matrix다. 따라서 `f: X × E → X`는 배열 index 한 번으로 O(1)에 계산할 수 있다.

  next_state = automaton_wip.function[curr_state][event];

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 형식

Graphviz open-source 도구는 텍스트 DOT 언어를 source code로 사용해 오토마타의 그래픽 표현을 만들 수 있다. DOT는 널리 쓰이며 다양한 형식으로 변환할 수 있다.

`wip` DOT 모델은 보이지 않는 initial node, double-circle final state, 일반 state와 event label이 붙은 edge로 같은 오토마타를 표현한다.

  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";
        }
  }

`dot` utility로 bitmap 또는 vector image를 만들고 `graph-easy`로 ASCII art를 만들 수 있다.

  $ dot -Tsvg -o wip.svg wip.dot
  $ graph-easy wip.dot > wip.txt

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`는 앞 예제와 같은 오토마타를 담은 `.dot` 파일을 해석해 앞 절의 C 표현으로 자동 변환하는 utility다.

`wip.dot` 파일을 다음 명령으로 변환하면 C 표현을 담은 `wip.h`가 생성된다.

  $ dot2c wip.dot > wip.h

생성된 `wip.h` 내용은 ‘Deterministic Automaton in C’ 절의 code sample과 같다.

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'.

비고와 참고 문헌

오토마타 형식론은 discrete event system(DES)을 여러 형식으로 모델링할 수 있게 하며, 각 표현은 서로 다른 응용과 사용자에게 적합하다.

집합론을 사용한 형식 기술은 오토마타 연산에 적합하고, 그래픽 형식은 사람이 해석하기 좋으며, computer language 표현은 machine execution에 적합하다.

간단한 입문 자료로 Gerard O'Regan의 ‘Concise guide to software engineering’(Springer, 2017)을 제시한다. DES의 연산과 응용을 포함한 상세 자료로 Cassandras와 Lafortune의 ‘Introduction to discrete event systems’(Springer US, 2008)을 제시한다.

kernel C 표현은 Daniel Bristot de Oliveira, Tommaso Cucinotta, Romulo Silva de Oliveira의 ‘Efficient formal verification for the Linux kernel’(SEFM 2019, pp. 315-332)을 참조한다.

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.

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.