Input/output automata provide a formal model, applicable in describing most types of an asynchronous concurrent system. On its own, the I/O automaton model contains a very basic structure that enables it to model various types of distributed systems. To describe specific types of asynchronous systems, additional structure must be added to this basic model. The model presents an explicit method for describing and reasoning about system components such as processes and message channels that interact with one another, operating at arbitrary relative speeds. The I/O automata were first introduced by Nancy A. Lynch and Mark R. Tuttle in "Hierarchical correctness proofs for distributed algorithms", 1987. "An I/O automaton models a distributed system component that can interact with other system components. It is a simple type of state machine in which the transitions are associated with named actions." There are three types of actions: input, output, and internal actions. The automaton uses its input and output actions to communicate with its environment, whereas the internal actions are only visible to the automaton itself. Unlike internal and output actions that are selected and carried out by the automaton, the input actions – which simply arrive from the environment - are not under automaton's control.
Examples I/O automata can be used to model individual components of a distributed system, such as a process, a message channel in a message passing system, or a shared data structure in a shared memory systems.
Process I/O automaton
Figure 1 depicts an example of an I/O automaton for a process in an asynchronous message-passing distributed system. In this setting, process Pi communicates with other processes by using a message passing system. Its output actions are of the form send(m)i,j, which represents process Pi sending a message with contents m to process Pj. The input actions are of form receive(m)k,i, representing the receipt of message with contents m by process Pi from process Pk. (The internal actions of Pi, which would correspond to the algorithm that the process is running are not shown.)
FIFO message channel
A message channel can also be modeled by an I/O automaton. Figure 2 illustrates a typical unidirectional FIFO channel automaton, named Ci,j. It has input actions of the form send(m)i,j, and output actions of the form receive(m)i,j. Each message m may contain 0 or 1 (m ∈ {0,1}). The state of the automaton stores a FIFO queue of all messages that have been sent but not yet received. In a typical distributed system where both process automata and communication channel automata exist, they are composed in a way that output actions of one automaton are matched and executed with identically-named input actions of the other automata. For example, consider a system composed of two process, Pi and Pj, and a communication channel Ci,j from process Pi to process Pj. In this setting, process Pi executes the output action send(m)i,j, if and only if channel Ci,j also executes its send(m)i,j input action.
Atomic read/write register
Figure 3 illustrates an atomic read/write register I/O automaton in a shared memory system with two processes, P1 and P2. The value V stored in the register is of type integer (V ∈ Z). The state of the automaton stores this value. Input actions consist of writei(V), which represents process Pi requesting to write a value V to the register (where i ∈ {1,2} and V ∈ Z), and readi, which corresponds to a process Pi requesting to read the value currently stored in the register. The output action acki is used to inform process Pi that the write request has successfully completed. The output action Vi represents the value V being returned as a response to a read request by process Pi. The automaton also includes internal actions perform_Write(V), which writes the value V to the register (by updating the state of the automaton), and perform_Read, which is used to read the value V stored in the state. (These internal actions are not shown in Figure 3.)
Formal specification An I/O automaton A, or simply an automaton, comprises five components:
sig(A) states(A) start(A) trans(A) tasks(A) These five components are described below.
Signature The initial step in formalization of an I/O automaton A is the definition of its signature, sig(A). A signature S describes the I/O automaton's actions using three disjoint sets of actions:
in(S): input actions, out(S): output actions, and int(S): internal actions. Based on the above formalization of input, output and internal actions, it is possible to define the following objects.
ext(S): the external actions, defined as in(S) ∪ out(S) local(S): the locally controlled actions, defined as out(S) ∪ int(S) extsig(S): the external signature, defined as (in(S), out(S), ø) acts(S) is defined as the set of all the actions of signature S.
States The set of states of automaton A, denoted states(A), need not be finite. This is a significant generalization of the usual notion of finite automata, as it enables modeling systems with unbounded data structures like counters and unbounded length queues. The set of start states (also known as initial states) is a non-empty subset of states. Multiple start states are allowed so that some input information can be included in the start states.
Transition relation The state-transition relation of automaton A is denoted trans(A) ⊆ states(A) × acts(sig(A)) × states(A). It satisfies the property that "for every state s and every input action π, there is a transition (s, π, s') ∈ trans(A)." A transition, also known as a step of I/O automaton A, is defined as an element (s, π, s') of trans(A). An input transition refers to a transition (s, π, s') when π is an input action, output transition indicates a transition (s, π, s') when π is an output action and so on. For any state s and action π, if the I/O automaton A has some transition of the form (s, π, s'), then π is said to be enabled in s. I/O automata are described as input-enabled because all input actions are required to be enabled in every state. A quiescent state s is defined as a state where only input actions are enabled.
… excerpt ends here. Continue reading the full article.
