Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 32

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 32)

The eect is described in terms of equations relating thetwo. We remark that this notation is very similar to that used by Lamport in his languageTLA (Temporal Logic of Actions). An alternative notation that is also popular suppressesexplicit mention of the states, and describes the eect using assignment statements. This isthe syntax used in Ken Goldman's Spectrum system, for instance.156Fair Executions. Consider the executions in which the system does not violate the cyclicbehavior. All these executions must involve rst doing choose : this action is enabled, nothingelse is enabled, and the fairness requires that the execution can't stop if something is enabled.By the code, the next step must be try i .

Then the execution can stop, if no crit i ever occurs.But if crit i occurs, a later exit i must occur. Again, at this point the execution can stop, butif a later rem i occurs, then the automaton stops if it chose 1, else the execution continues.That is, have fair executions (omitting states that are determined):choose , 1, trychoose , 1, try , crit , exitchoose , 1, try , crit , exit , remchoose , 2, try , crit , exit , rem , try ,etc.There are also some fair executions in which the system violates the cyclic behavior, e.g.:choose 1 critBut, for instance, the following is not fair:choose 2 try crit exit remNote that for the automaton above, all the fair executions with correct cyclic behavior arenite.To model the rest of the shared memory system, we use one big IOA to model all theprocesses and the memory together.

The outputs are the crit and rem actions. The internalactions are any local computation actions and the shared memory actions. The states setconsists of the states of all the processes plus the state of the shared memory. The partitionis dened by having one class per process, which contains all the non-input actions belongingto that process.

The IOA fairness condition captures exactly our requirement on fairness ofprocess execution in the shared memory system. Of course, there are extra constraints thatare not implied by the general model, e.g., types of memory (read-write, etc.), and localityof process action (i.e., that it can only aect its own state, only access one variable at a time,etc.).13.2.2 Object ModelIn this section we dene formally an alternative way to model shared memory systems, theobject model, which was discussed briey in Lecture 10. We will use this model for thenext few lectures.

In the object model, each process is a separate IOA (usually with onlyone fairness class), and each shared memory object is also an IOA. Thus, for example, a157read-write object is an IOA with inputs of the form read ix, where i is a process and x anobject name, and write ix(v), where i is a process, x is an object and v is a value to bewritten. Now, note that a read is supposed to return a value. Since this is an IOA, thiswill be a separate output action read-respondix(v). For uniformity, also give the write awrite-respondix.

The write-respondix action serves only as an \ack", saying that the writeactivation has terminated.This is essentially the same interface that we have already described for atomic read-writeobjects | the only dierence is that now we are adding an identier for the specic objectinto all the actions. (This is because IOA's have a \global naming scheme" for actions.)Of course, we could also have other objects: queue, read-modify-write registers, andsnapshot objects, as discussed earlier.

Each has its own characteristic interface, with inputsbeing invocations of operations and outputs being responses.The processes are automata with inputs as before, plus the responses to their data operations, e.g., read-respondix(v) is an input to process i. The outputs of the processes now alsocontain the invocations of their data operations, e.g., read ix. Usually, each process wouldhave only one fairness class that is, we think of it as a sequential process. (But we wouldlike to be able to generalize this when convenient.)For the objects, we usually don't want to consider just any automata with the giveninterface | we want some extra conditions on the correctness of the responses. For example,the atomic object conditions dened earlier are an important example. We recall theseconditions below (see notes of Lecture 10 for more complete specication).1. Preserving well-formedness.

Recall that \preserves" has a formal denition for IOA's.2. Giving \atomic" responses based on serialization points, in all executions. (Recall thatit is required that all complete operations and an arbitrary subset of the incompleteoperations have serialization points.)3. In fair executions, every invocation has a response. Note that this now makes sensefor automata that have some organization other than the process-variable architecturewe have been studying, because IOA's in general have a notion of fairness.After composing the process automata and the object automata, we hide the communication actions between them.13.3 Modularity ResultsNow that we have described the two kinds of models, instantaneous access and atomicobjects, more-or-less precisely in terms of IOA's, we can state our modularity results.15813.3.1 Transforming from Instantaneous to Atomic ObjectsIn this section we discuss how to transform algorithms which are specied for instantaneous objects to work with atomic versions of the objects.

Let A be an algorithm in theinstantaneous shared memory model satisfying the following conditions.Each process can only access one shared variable at a time (this is the usual restriction).For each user i of A, suppose that there is a notion of user well-formedness, consistingof a subset of alternating sequences of input and output actions. We require that Apreserve user well-formedness.Suppose that pi's states are classied as \input states" and \output states", based onwhich is supposed to happen next in a well-formed execution (initially, only \input"actions are enabled).

We require that non-input steps of pi are only enabled in \output"states.We remark that this is the case for all the examples we have considered. For mutualexclusion algorithms, the output states are the T E states, which occur between try andcrit actions, and between exit and rem actions, respectively. For snapshot implementations,the output states are just those while an invocation of update or snap is active. For consensusalgorithms, the output states are those between the init and decide.Assuming A satises the above conditions, we can now transform A into a new algorithmT (A), designed for the atomic object model. T (A) includes an atomic object for each sharedmemory location.

Each access to an object is expanded to an invocation and a response.After the invocation, the process waits until the response occurs, doing nothing else in themeantime. When the response comes in, the process resumes as in A.Lemma 6T (A) preserves user well-formedness for each user i.2. If is any (not necessarily fair) user well-formed execution of T (A), then there is a1.user well-formed execution 0 of A such that beh () = beh (0 ).3. If is any fair user well-formed execution of T (A) (i.e., both the processes and theatomic objects have fair executions), then there is a fair user well-formed execution 0of A such that beh () = beh (0).Proof Sketch: Here is a sketch of the argument. We start with and modify it to get0 as follows.

First, by the denition, we have the serialization points within the operationintervals, for all the invocations of the atomic objects. Now consider the execution obtained159by moving the invocation and response actions to the serialization points, and adjusting thestates accordingly. In the case of incomplete operation intervals, there are two cases. If thereis a serialization point for the interval, then put the invocation from , together with a newlymanufactured response event, at the serialization point (the response event should be theone whose existence is asserted by the atomic object denition). If there is no serializationpoint, then just remove the invocation.We now claim that we can move all the events we have moved without changing the orderof any events of a particular process pi .

This follows from two facts. First, by construction,pi does no locally-controlled actions while waiting for a response from an operation. Second,when pi invokes an operation, it is in an output state, and by assumption, no inputs willcome in when pi is in an output state. Similarly, we can remove the invocations we haveremoved and add the responses we have added without aecting the external behavior, sincea process with an incomplete invocation does not do anything afterwards anyway (it doesn'tmatter if it stops just before issuing the invocation, while waiting for the response, or justafter receiving the response).In the resulting execution, all the invocations and responses occur in consecutive pairs.We can replace those pairs by instantaneous access steps, thus obtaining an execution of the instantaneous access system A.

Thus and 0 have the same behavior at the userinterface, proving Part 2.For Part 3, notice that if is fair, then all embedded executions of the atomic objectsalways respond to all invocations. Coupling this with the fairness assumption for processes,yields fairness for the simulated algorithm A (i.e., that the simulated processes continuetaking steps).So, Lemma 6 says that any algorithm for the instantaneous shared memory model can beused (in a transformed version) in the atomic object shared memory model, and no externaluser of the algorithm could ever tell the dierence.In the special case where A itself is an atomic object implementation (in the instantaneousshared memory model), this lemma implies that T (A) is also an atomic object implementation. To see this, note that Property 1 (preserving well-formedness) follows immediatelyfrom Part 1 of Lemma 6 Property 2 follows from Part 2 of Lemma 6 and the fact that A isan atomic object (property 2 of the atomic object denition for A) and Property 3 followsfrom Part 3 of Lemma 6 and the fact that A is an atomic object (Property 3 of the atomicobject denition for A).

Therefore, we can build atomic objects hierarchically.16013.3.2 Composition in the Object ModelNow we want to consider building objects that are not necessarily atomic hierarchically. Todo this, we have to generalize the notion of an object specication to include other kinds ofobjects. Later in the course we shall see some examples for such objects, including safe andregular objects, and the special concurrent timestamp object to be considered next time.Object SpecicationsWe dene the general notion of an object specication, generalizing the specication foratomic objects. Formally, an object specication consists of the following.1.

Характеристики

Список файлов книги