Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 31
Текст из файла (страница 31)
Then Scheds (Ai) =i2IQ Scheds (A ), Fairscheds (A) = Q Fairscheds (A ), Behs (A) =iiii2Ii2IQi2I BehsQ(Ai) and Fairbehs (A) = i2I Fairbehs (Ai).i2ICorresponding to our hiding operation for automata, we dene hide hide H to be the schedule module H 0 obtained from H by replacing sig (H ) with sig (H 0) = hidesig (H ).Finally, we are ready to dene a problem specication and what it means for an automaton to satisfy a specication. A problem is simply a schedule module P .
An automaton Asolves10 a problem P if A and P have the same external action signature and fairbehs (A) fairbehs (P ). An automaton A implements a problem P if A and P have the same externalaction signature (that is, the same external interface) and nbehs (A) nbehs (P ). Notice that if A solves P , then A cannot be a trivial solution of P since the fact that A isinput-enabled ensures that fairbehs (A) contains a response by A to every possible sequenceof input actions. For analogous reasons, the same is true if A implements P .Since we may want to carry out correctness proofs hierarchically in several stages, it isconvenient to state the denitions of `solves' and `implements' more generally.
For example,we may want to prove that one automaton solves a problem by showing that the automaton`solves' another automaton, which in turn `solves' another automaton, and so on, untilsome nal automaton solves the original problem. Therefore, let M and M 0 be modules10This concept is sometimes called satisfying.152(either automata or schedule modules) with the same external action signature. We say thatM solves M 0 if fairbehs (M ) fairbehs (M 0) and that M implements M 0 if nbehs (M ) nbehs (M 0).As we have seen, there are many ways to argue that an automaton A solves a problemP .
We now turn our attention to two more general techniques.13.1.2 Proof TechniquesModular DecompositionOne common technique for reasoning about the behavior of an automaton is modular decomposition, in which we reason about the behavior of a composition by reasoning about thebehavior of the component automata individually.It is often the case that an automaton behaves correctly only in the context of certainrestrictions on its input.
These restrictions may be guaranteed in the context of the composition with other automata comprising the remainder of the system, or may be restrictionsdened by a problem statement describing conditions under which a solution is required tobehave correctly. A useful notion for discussing such restrictions is that of a module `preserving' a property of behaviors: as long as the environment does not violate this property,neither does the module.In practice, this notion is of most interest when the property is prex-closed, and whenthe property does not concern the module's internal actions. A set of sequences P is said tobe prex-closed if 2 P whenever both is a prex of and 2 P . A module M (eitheran automaton or schedule module) is said to be prex-closed provided that nbehs (M ) isprex-closed.Let M be a prex-closed module and let P be a nonempty, prex-closed set of sequencesof actions from a set ( satisfying ( \ int (M ) = . We say that M preserves P if j( 2 Pwhenever j( 2 P , 2 out (M ), and jM 2 nbehs (M ).In general, if a module preserves a property P , then the module is not the rst to violateP : as long as the environment only provides inputs such that the cumulative behaviorsatises P , the module will only perform outputs such that the cumulative behavior satisesP .
This denition, however, deserves closer inspection. First, notice that we consider onlysequences with the property that jM 2 nbehs (M ). This implies that we consider onlysequences that contain no internal actions of M . Second, notice that we require sequences to satisfy only j( 2 P rather than the stronger property 2 P . Suppose, for example,that P is a property of the actions ( at one of two interfaces to the module M . In this case,it may be that for no 2 P and 2 out (M ) is it the case that jM 2 nbehs (M ), since153all nite behaviors of M containing outputs include activity at both interfaces to M .
Byconsidering satisfying only j( 2 P , we consider all sequences determining nite behaviorsof M that, at the interface concerning P , do not violate the property P .One can prove that a composition preserves a property by showing that each of thecomponent automata preserves the property:Proposition2 Let fA g I be a strongly compatible collection of automata and let A =Q A .
If A preserves iPi2forevery i 2 I , then A preserves P .ii2I iIn fact, we can prove a slightly stronger result. An automaton is said to be closed if ithas no input actions. In other words, it models a closed system that does not interact withits environment.Proposition 3 Let A be a closed automaton. Let P be a set of sequences over (. If Apreserves P , then nbehs (A)j( P .In the special case that ( is the set of external actions of A, the conclusion of thisproposition reduces to the fact that nbehs (A) P .
The proof of the proposition dependson the fact that ( does not contain any of A's input actions, and hence that if the propertyP is violated then it is not an input action of A committing the violation. In fact, thisproposition follows as a corollary from the following slightly more general statement: If Apreserves P and in (A) \ ( = , then nbehs (A)j( P .Combining Propositions 2 and 3, we have the following technique for proving that anautomaton implements a problem:CorollaryQ 4 Let fAigi2I be a strongly compatible collection of automata with the propertythat A = i2I Ai is a closed automaton. Let P be a problem with the external action signatureof A.
If Ai preserves nbehs (P ) for all i 2 I , then A implements P .That is, if we can prove that each component Ai preserves the external behavior required by the problem P , then we will have shown that the composition A preserves thedesired external behavior and since A has no input actions that could be responsible for violating the behavior required by P , it follows that all nite behaviors of A are behaviors of P .Hierarchical DecompositionA second common technique for proving that an automaton solves a problem is hierarchicaldecomposition in which we prove that the given automaton solves a second, that the secondsolves a third, and so on until the nal automaton solves the given problem. One way ofproving that one automaton A solves another automaton B is to establish a relationshipbetween the states of A and B and use this relationship to argue that the fair behaviors of Aare fair behaviors of B .
In order to establish such a relationship in between two automata we154can use a \simulation" relation f . Below, for binary relation f , we use the notation u 2 f (s)as an alternative way of writing (s u) 2 f .Denition 1 Suppose A and B are input/output automata with the same external actionsignature, and suppose f is a binary relation from states(A) to states(B ). Then f is aforward simulation from A to B provided that both of the following are true:1. If s 2 start (A) then f (s) \ start (B ) 6= .2. If s is a reachable state of A, u 2 f (s) is a reachable state of B , and (s s0) is a stepof A, then there is an `extended step' (u u0) such that u0 2 f (s0 ) and jext (B ) =jext (A).An extended step of an automaton A is a triple of the form (s s0), where s and s0 arestates of A, is a nite sequence of actions of A, and there is an execution fragment of Ahaving s as its rst state, s0 as its last state, and as its schedule.
The following theoremgives the key property of forward simulations:Theorem 5 If there is a forward simulation from A to B , then behs(A) behs(B ).13.2 Shared Memory Systems as I/O Automata13.2.1 Instantaneous Memory AccessAs a case study, we consider a mutual exclusion system. In this section we model the users asIO automata. Specically, each user i is an IOA, with inputs crit i and rem i, and outputs try iand exit i.
The user automata have arbitrary internal actions, states sets and start states.There is only one constraint | that any such automaton \preserves" the cyclic behavior,i.e., if the system is not the rst to violate it, the user does not violate it. (The formaldenition of \preserves" is given in the notes above.)The following example shows a particular user IOA. Note the language that is used todescribe the automaton. We rst describe the IOA intuitively.
The \example user" choosesan arbitrary number from 1 to 3, and then makes exactly that many requests for the resourcein succession.In the precondition-eects language, the user is described as follows.states: As before, we can write it as consisting of components. Here we have the following.region , values in fR T C E g, initially Rcount , a number from 1 to 3 or nil , initially arbitrary155chosen , a Boolean, initially falsestart: Given by the initializations.acts : The external actions are described above. Also, there is an internal action choose .part : we have only one class that contains all the non-input actions.trans : We describe the allowed triples (s s0) by organizing them according to action.choose iPrecondition:s:chosen = falseEect:s :chosen = trues :count 2 f1 2 3g00try iPrecondition:s:chosen = trues:region = Rs:count > 0Eect:s :region = Ts :count = s:count ; 100crit iEect:s :region = C0exit iPrecondition:s:region = CEect:s :region = E0rem iEect:s :region = R0Note that the automaton is input-enabled, i.e., it can accommodate unexpected inputs (whichdo not necessarily induce interesting behavior in this case, though.)Here, we are describing the transitions of the form (s s0) using explicit mentions ofthe pre- and post- states s and s0.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
