Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 29
Текст из файла (страница 29)
For the moment, these denitions do not include any notion offairness. In the subsequent sections, we dene composition of I/O automata and show thatit has the nice properties that it should. Then we introduce the notion of fairness and show143how it interacts with the composition notions. We then describe some useful conventionsfor stating problems to be solved by I/O automata, in terms of their external behavior,and describe what it means for an I/O automaton to solve a problem.
Finally, we describetwo important proof techniques for verifying systems described as I/O automata { based onmodular decomposition and on hierarchical decomposition. These notes are adapted fromthe Lynch, Tuttle CWI paper.Actions and Action SignaturesWe assume a universal set of actions. Sequences of actions are used in this world, fordescribing the behavior of modules in concurrent systems. Since the same action may occurseveral times in a sequence, it is convenient to distinguish the dierent occurrences.
We referto a particular occurrence of an action in a sequence as an event.The actions of each automaton are classied as either `input', `output', or `internal'. Thedistinctions are that input actions are not under the automaton's control, output actions areunder the automaton's control and externally observable, and internal actions are under theautomaton's control but not externally observable.
In order to describe this classication,each automaton comes equipped with an `action signature'.An action signature S is an ordered triple consisting of three disjoint sets of actions. Wewrite in (S ) out (S ) and int (S ) for the three components of S , and refer to the actions in thethree sets as the input actions, output actions and internal actions of S , respectively. We letext (S ) =2 (S ) out (S ) and refer to the actions in ext (S ) as the external actions of S. Also,we let local (S ) = out (S ) int (S ), and refer to the actions in local (S ) as the locally-controlledactions of S . Finally, we let acts (S ) =2 S out (S ) int (S ), and refer to the actions inacts (S ) as the actions of S . An external action signature is an action signature consistingentirely of external actions, that is, having no internal actions.
If S is an action signature,then the external action signature of S is the action signature extsig (S ) = (2 S out (S ) ),i.e., the action signature that is obtained from S by removing the internal actions.Input/Output AutomataNow we are ready to dene the basic component of our model. An input/output automatonA (also called an I/O automaton or simply an automaton) consists of ve components:an action signature sig(A),a set states (A) of states,a nonempty set start (A) states (A) of start states,144a transition relation trans (()A) states (A) acts (sig (A)) states (A), with the property that for every state s and input action there is a transition (s s0) in trans (()A),andan equivalence relation part (A) on local (sig (A)), having at most countably many equivalence classes.We refer to an element (s s0) of trans (A) as a transition, or step of A.
The transition(s s0) is called an input transition of A if is an input action. Output transitions, internaltransitions, external transitions and locally-controlled transitions are dened analogously. If(s s0) is a transition of A, then is said to be enabled in s. Since every input action isenabled in every state, automata are said to be input-enabled. The input-enabling propertymeans that the automaton is not able to block input actions. The partition part (A) iswhat was described in the introduction as an abstract description of the `components' of theautomaton. We shall use it to dene fairness later.An execution fragment of A is a nite sequence s0,1,s1,2,...,n,sn or an innite sequences0,1,s1,2,...,n,sn,...
of alternating states and actions of A such that (si,i+1,si+1) is atransition of A for every i. An execution fragment beginning with a start state is called anexecution. We denote the set of executions of A by execs (A), and the set of nite executionsof A by it nexecs(A). A state is said to be reachable in A if it is the nal state of a niteexecution of A.The schedule of an execution fragment of A is the subsequence of consisting ofactions, and is denoted by sched(). We say that is a schedule of A if is the schedule ofan execution of A. We denote the set of schedules of A by scheds (A) and the set of niteschedules of A by nscheds (A). The behavior of an execution or schedule of A is thesubsequence of consisting of external actions, and is denoted by beh (). We say that isa behavior of A if is the behavior of an execution of A.
We denote the set of behaviors ofA by behs (A) and the set of nite behaviors of A by nbehs (A).CompositionFor motivation, consider the composition of user automata and a shared memory systemautomaton.Generally speaking, we can construct an automaton modeling a complex system by composing automata modeling the simpler system components. The essence of this compositionis quite simple: when we compose a collection of automata, we identify an output action of one automaton with the input action of each automaton having as an input action.Consequently, when one automaton having as an output action performs , all automata145having as an input action perform simultaneously (automata not having as an actiondo nothing).We impose certain restrictions on the composition of automata.
Since internal actionsof an automaton A are intended to be unobservable by any other automaton B , we cannotallow A to be composed with B unless the internal actions of A are disjoint from the actionsof B , since otherwise one of A's internal actions could force B to take a step. Furthermore,in keeping with our philosophy that at most one system component controls the performanceof any given action, we cannot allow A and B to be composed unless the output actions ofA and B form disjoint sets. Finally, since we do not preclude the possibility of composinga countable collection of automata, each action of a composition must be an action of onlynitely many of the composition's components.
Note that with innite products we canhandle systems that can create processes dynamically.Since the action signature of a composition (the composition's interface with its environment) is determined uniquely by the action signatures of its components, it is convenientto dene a composition of action signatures before dening the composition of automata.The preceding discussion motivates the following denition. A countable collection Sii2I ofaction signatures is said to be strongly compatible if for all i j 2 I satisfying i 6= j we have1. out (Si) \ out (Sj ) = ,2. int (Si) \ acts (Sj ) = , and3.
no action is contained in innitely many sets acts (Si).We say that a collection of automata are strongly compatible if their action signatures arestrongly compatible.When we compose a collection of automata, internal actions of the components becomeinternal actions of the composition, output actions become output actions, and all otheractions (each of which can only an input action of a component) become input actions.As motivation for this decision, consider one automaton A having as an output actionand two automata B1 and B2 having as an input action. Notice that is essentially abroadcast from A to B1 and B2 in the composition A B1 B2 of the three automata. Notice,however, that if we hide communication, then the composition (A B1) B2 would not bethe same as the composition A B1 B2 since would be made internal to A B1 beforecomposing with B2, and hence would no longer be a broadcast to both B1 and B2.
Thisis problematic if we want to reason about the system A B1 B2 in a modular way by rstreasoning about A B1 and then reasoning about A B1 B2. We will dene another operationto hide such communication actions explicitly.146The preceding discussion motivates the following denitions. The composition S =Q S of a countable collection of strongly compatible action signatures fS g is denedi i2Ii2I ito be the action signature within (S ) = i2I in (Si) ; i2I out (Si ),out (S ) = i2I out (Si ), andint (S ) = i2I int (Si).Illustration: users and shared memory system automaton.
List the various actions, showsignatures are compatible.The composition A = Qi2I Ai of a countable collection of strongly compatible automatafAi gi2I is the automaton dened as follows:8sig (A) = Q sig (A ),i2Iistates (A) = Qi2I states (Ai),Qstart (A) = i2I start (Ai ),trans (A) is the set of triples (s~1 s~2) such that, for all i 2 I , if (s~1 i] s~2 i]) 2 trans (Ai), and if 62 acts (Ai) then s~1 i] = s~2 i], and2acts (Ai) thenpart (A) = i2I part (Ai ).When I is the nite set 1 ::: n, we often denote Qi2I Ai by A1 An.Notice that since the automata Ai are input-enabled, so is their composition.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
