Acta Informatica manuscript No. (will be inserted by the editor)

A proof of Bloom’s two-writer protocol

Uri Abraham^{1}

Departments of Mathematics and Computer Science Ben Gurion University of the Neguev Be’er Sheva, Israel.

Received: date/ Revised version: date

Abstract. Bloom’s protocol implements an atomic two-writer multiplereader register from single-writer multiple-reader atomic registers. Despite its apparent simplicity, and the fact that several correctness proofs were published, the protocol is still a challenge. We give a proof in this paper in order to illustrate a framework for describing distributed programs and to prove their correctness. This framework is characterized by the usage of system executions in two levels: the lower level is related to the program’s text, and the higher-level with its abstract properties. We also define a variant of Bloom’s protocol in which data and control values are separated.

1 Introduction

The main aim of this paper is to employ Bloom’s two-writers protocol [4] to illustrate an approach for specifying and proving the correctness of distributed protocols. This approach is characterized by a clear division of the correctness proofs into two layers: the lower layer involves the program, but the higher level mentions only abstract higher-level properties of system executions. We also present a version of Bloom’s protocol which combines Vidyasankar elegant single-writer multi-reader register ([14]).

The advantage of Bloom’s protocol as an instructive example is that it is quite well-known, simple, and yet sufficiently intriguing (it appears in Lynch’s textbook [10]; and in [6]).

The method presented here is a continuation of Lamport’s work on system executions and his consideration of higher-level views (see [9]) This approach will be called “behavioral” since it describes the behavior of processes in terms of the generated events and the precedence relationship between them. It is in contrast to the “assertional” approach in which states and histories are used, and inductive proofs (of state assertions) are given. Sailing between the behavioral and assertional reasoning, the computer science community has by and large accepted the proposition that the semantics of concurrency should be understood by means of states and histories that represent the interleaving of atomic steps made by the concurrent processes. We present here a different point of view.

A detailed exposition of our thesis is in [2], and an aim of the present article is to exemplify some of its main traits. States and histories are used in our approach only in the very first stage, when the operations of leach of the serial processes are described. Then, system executions are build on top of these histories and are employed throughout the rest of the correctness proof.

The plan of the paper is to start with a very simple protocol, the Aimless Protocol, which is in fact the basis of Bloom’s protocol. Then we describe the basic terms of states, histories, and system executions, using this Aimless Protocol as an example. The protocol of Bloom is in Section 4, and the economical version in Section 5.

2 The Aimless Protocol

The heart of Bloom’s protocol is the following “aimless” protocol (Figure 1). There are two process: Copier and Changer. They communicate through two single-writer, single-reader serial registers, R_{0} owned by Copier, and R_{1} owned by Changer. These are boolean registers initially set to any values (for example to 0 and 0), and we assume initial writes of the initial values to the registers. An initialization write event precedes any non initialization read/write event. The owner of the register is its sole writer, and any other process can read it. The boolean values 0 and 1 will be called “colors” here. The protocol for Copier is to read R_{1} into its local variable t and then to copy into R_{0} the value returned by its read. The protocol for Changer is to reverse the value found in register R_{0} of Copier and to write the reversed value in R_{1}.

To emphasize the distinction between assignment to a local variable and read/write operations on a register we use ‘read(R; x)’, and ‘write(R; v)’ instead of x := R, and R := v. The protocol of Copier is called COPY, and the protocol for Changer is called CHANGE.

COPY

1. read(R_{1}; t);

2. write(R_{0}; t).

CHANGE

1. read(R_{0}; t);

2. t := 1 − t;

3. write(R_{1}; t).

Fig. 1 The Aimless Protocol. Variable t is local to the processes. It holds {0, 1}.

(We will use uppercase words to name both procedures and their executions.)

3 System executions on top of histories

We first describe the model of computation of histories (sequences of states), and we then expand it and show how on top of these extended histories system executions are built which will later be used in the behavioral proof.

A state is a map from variables to values. In particular, the values of some variables tell which instructions are enabled at the state. Typically, several instructions may be enabled at any state. Each instruction is (identified with) a binary relation on the states. When two states S and S′ are thus related by an instruction I then we say that the pair (S, S′) is an “execution of I”, and we also call that pair a “step”. (We note pairs interchangeably by (a, b) and ⟨a, b⟩.) The possibility that the two states in a step are equal is not excluded. A history is a sequence of states (finite or of order-type ω of the natural numbers), ⟨S_{i} | i ∈ ω⟩ if infinite, such that S_{0} is an initial state and for every i ∈ ω there is an instruction I that is enabled at state S_{i} and such that step (S_{i}, S_{i+1}) is an execution of I. The instructions are those of the protocol being investigated, and the collection of all resulting histories describe the possible executions of the protocol.

For example, the states for the Aimless Protocol are defined as follows. The variables are:

1. R_{1}, and R_{0}, which are the registers owned by Changer and Copier respectively. The possible values of these registers are 0 and 1.

2. t_{1} and t_{0} which are the local boolean variables of Changer and Copier respectively (denoted plainly t in the protocol).

3. P C_{1} and P C_{0} which are the program counters of Changer and Copier respectively. P C_{1} can hold the values 1, 2, or 3, referring to these lines in the CHANGE protocol, and similarly P C_{0} can refer to lines 1 and 2 in the COPY protocol. For example, P C_{1} = 3 indicate that the write on R_{1} is enabled.

A state S is any function from these variables into their ranges. An initial state S for example can assign any color (0 or 1) to the registers and to the variables t, but S(P C_{1}) = 1 and S(P C_{0}) = 1.

A step of the protocol is a pair of states (S_{1}, S_{2}) that represent an execution of an instruction (a line) of the protocol. We have the following possible steps in the Aimless Protocol. Steps by Copier: Let S_{1} and S_{2} be states.

1. (S_{1}, S_{2}) constitutes a read step (of register R_{1} by Copier) corresponding to line 1 of the COPY protocol if S_{1}(P C_{0}) = 1, S_{2}(P C_{0}) = 2, S_{2}(t_{0}) = S_{1}(R_{1}), and S_{2}(X) = S_{1}(X) for any variable X other than P C_{0} and t_{0}. The value of this step is defined to be the value “returned” by this read, namely we define Value(⟨S_{1}, S_{2}⟩) = S_{1}(R_{1}).

2. (S_{1}, S_{2}) is a write step (on register R_{0} by Copier) corresponding to line 2 of the COPY protocol if S_{1}(P C_{0}) = 2, S_{2}(P C_{0}) = 1, and S_{2}(R_{0}) = S_{1}(t_{0}). And for any variable X other than P C_{0} and R_{0} S_{2}(X) = S_{1}(X). The value of this step is defined to be the value written on R_{0} in this step. That is, Value(⟨S_{1}, S_{2}⟩) = S_{2}(R_{0}).

Steps by Changer:

1. Write steps (corresponding to line 3) and read steps (corresponding to line 1) are defined similarly. Also the function Value is defined an these steps. There is an additional local step:

2. (S_{1}, S_{2}) constitute a local step corresponding to an execution of line 2 by Changer if S_{1}(P C_{1}) = 2, S_{2}(P C_{1}) = 3, S_{2}(t_{1}) = 1 − S_{1}(t_{1}), and all other values remain unchanged at S_{2}.

In addition to the function Value, we also define predicates on the steps. If s = (S_{1}, S_{2}) is a step by Copier, then we define Copier(s), and if it is a step by Changer, then we define Changer(s). We also define Read(s) iff s is a read step (an execution of line 1 in the COPY or CHANGE protocol) and define Write(s) iff s is a write step.

A history or an interleaving execution of a protocol is a sequence H = ⟨S_{i} | i ∈ I⟩ of states S_{i} where the index set I is either a finite number I = {0, …, n − 1} or the set of all natural numbers. And such that

1. S_{0} is an initial state.

2. For every index i such that i + 1 ∈ I, (S_{i}, S_{i+1}) is a step of the protocol.

3. If I is the infinite set ω of all natural numbers then each process contains infinitely many steps in H. This is a rather strong “fairness” condition; we shall not be much preoccupied with fairness.

The steps in a history H are linearly ordered by the following definition of <_{H}:

(S_{i}, S_{i+1}) <_{H} (S_{j}, S_{j+1}) iff i + 1 ≤ j.

For steps x and y we use the notation x ≤_{H} y iff x <_{H} y or x = y. Thus <_{H} is the “temporal” ordering on the steps of the history. We may transform our point of view and view the sequence of

steps, rather than states, as constituting the history. Anyhow, we shall enrich this structure by adding the predicates and function defined on the steps. For the Aimless Protocol, we have defined the following predicates and function on steps of H.

1. Changer and Copier are used as predicates: Changer(S) holds iff S is a step by Changer, and similarly Copier(S) is defined.

2. Write(S) and Read(S) were defined when S is an execution of a write (respectively read) instruction.

3. For every read/write step S, Value(S) is the value (color) obtained or written.

4. It is convenient to have a function, Register, which associates to every read/write step S the register Register(S) on which it operates. Thus, for example, if Copier(S) and Read(S) then Register(S) = R_{1}, and if Copier(S) and Write(S) then Register(S) = R_{0}.

So let H be some history of an execution of the Aimless Protocol. Our aim is to define a function ω on the read steps in H which gives for every read its corresponding write step. We have said that the initial state determines the initial values of the registers (which are arbitrary in the Aimless Protocol) but it is convenient to assume a pair of initial write steps in the history that determine the initial values. These initial steps are required to be the first two steps in the history (they precede any other step). Now that the initial write steps are assumed to be in H, the function ω can be defined on the read steps in H as follows. Since the steps are linearly ordered in the order type of the natural numbers (or form a finite set) it is clear that for every read step R in H, say of register R_{0}, there is a write step W on register R_{0} in H such that W <_{H} R and there is no write step W′ on register R_{0} such that W <_{H} W′ <_{H} R. Namely, W is the last write step on that register that precedes R. We define W = ω(R).

Claim. V alue(R) = Value(ω(R)), for every read step.

This claim is an example of an assertion that can be proved by induction on the index i of state S_{i} in the history. The first steps (S_{0}, S_{1}) and (S_{1}, S_{2}) in our history H are the assumed initial write steps on registers R_{0} and R_{1}. For every subsequent state S_{i} (for i ≥ 2) the value S_{i}(R_{1}) of register R_{1} at that state is equal to the last preceding write on R_{1}. Namely

S_{i}(R_{1}) = Value(s) where s is the maximal write step on R_{1} among (S_{0}, S_{1}), …, (S_{i−1}, S_{i}).

(1)

Similarly, S_{i}(R_{0}) = Value(s) where s is the maximal write step on R_{0} among (S_{0}, S_{1}), …, (S_{i−1}, S_{i}). These two assertions should first be proved by induction on i, and then the claim is easily derived. The details of this proof are left to the reader. Note the difference between this proof and a traditional assertional proof. Both are inductive proofs, but there the assertion is a statement concerning the state (its truth is determined by S alone), and here the assertion speaks about the sequence of states ⟨S_{0}, …, S_{i}⟩ and the resulting steps and it involves predicates and functions defined over these steps. This extension of the range of assertions that can be proved by induction should not be considered as illegitimate or problematic.

We recall now the notion of a structure as defined by Tarski. A structure consists of a universe of “elements” which are just characterless (plain) points, together with predicates and functions defined on them. A function of a structure has an arity k (which means that it is defined on k-tuples) and it returns values that are elements of the universe. Associated with a structure is a (first-order) language in which statements about the structure can be expressed. Sometimes, multi-sorted structures are more convenient. In these, the universe consists of several “sorts”, and each function is defined on a sort (or all k-tuples from specified sorts) rather than on all the universe. As an example we see how histories of the Aimless Protocol can be transformed into structures.

Let H = ⟨S_{i} | i ∈ ω⟩ be a history of the Aimless Protocol (the set of indexes is infinite for simplicity of notation). We want to define the system execution M = M_{H} that corresponds to H. As a first approximation let the universe of M be the set of steps of H, let the predicates of M be the predicates <_{H}, Changer, Copier, Read, and Write defined above on the steps, and let the functions of M be Value, Register and ω as defied above.

A slight wrinkle is that the function Value(S) gives values (0 and 1) which are not in M. Since any structure should be closed under its functions, we must add the set of colors {0, 1} to M. Similarly, two constants R_{0} and R_{1} are added to M to represent the registers and to be values for the function Register which assigns to each read/write event its register. Thus M becomes a two-sorted structure with events consisting of steps as one sort, and with atemporal objects consisting of colors and register constants as the second sort.

Another wrinkle is that the steps of H are not plain elements of the universe, but are rather complex objects (consisting of states which are themselves quite complex). We must therefore denature the steps and present them as plain points of the structure. (Formally, the notion of isomorphism of structures can be helpful here.) To mark this transformation, we call the steps “events” (specifically lowerlevel events) and consider them as plain objects devoid of any inner structure.

To sum up, the structure M has the following form:

M = (E, C; <_{M}, Value, Register, ω, P_{1}, …, P_{n}),

where E is the set of events (each event stands for a step), C = {0, 1, R_{0}, R_{1}} is the set of colors and registers (together E and C form the universe of M), <_{M} is the linear ordering of the events (namely the step ordering <_{H}), and Value etc. are the function and predicates as defined above.

The next stage in this transformation of the history H into a richer structure which will finally become a system execution is the addition of higher-level events. In general a higher-level event is a set of (lower-level) events that represent some operation execution. In our protocol, for example, we define the following higher-level events (also called compound events).

1. If R and W are the read and write events corresponding to a certain execution of the COPY protocol, then the compound event {R, W } is formed and called a COPY event. In details, the requirement is that R <_{M} W, R is an execution of line 1 and W of line 2 of the COPY protocol, and there is no event S by Copier between R and W.

2. Similarly, if R and W are the read and write events corresponding to a certain execution of the CHANGE protocol (of lines 1 and 3 respectively), then the compound event X = {R, W } is formed and called a CHANGE event. We could have added to X the event corresponding to the execution of line 2 (switching the value of t), but it seems more natural to represent a higher-level CHANGE event by its read/write lower-level events.

3. Finally, two higher-level initial events are formed. Let w_{cpy} and w_{chng} be the assumed initial write events in E on registers R_{0} and R_{1} respectively. Then we form higher-level events

Init_{0} = {w_{cpy}} and Init_{1} = {w_{chng}},

which are the singletons containing the initial writes. These higherlevel events will allow for somewhat simpler definitions later on.

Let HL be the collection of all higher-level events thus defined. We extend the structure M as follows.

1. Add HL to the set of events of M. So now E (the new sort of events) consists of the lower-level events (which are essentially the steps of the history H) together with the higher-level events HL defined above.

2. A membership relation x ∈ A is introduced, which holds between a lower-level event x and a higher-level event A in HL that contains it.

3. We can add HL as a predicate on E for convenience, but we can do without it since all higher-level events are non-empty and thus HL(X) iff ∃a(a ∈ X).

4. The linear-ordering <_{M} of the lower-level events is now extended to a partial ordering of E defined by the following rules.

If A and B are higher-level events, then

A <_{M} B iff ∀a ∈ A ∀b ∈ B a <_{M} b.

(2)

If A is a higher-level event and b a lower-level event then

A <_{M} b iff ∀a ∈ A a <_{M} b.

Similarly, b <_{M} A is defined iff b <_{M} a for all a ∈ A.

(3)

5. The predicates Copier and Changer are extended naturally on the higher-level events. We also define predicates COPY and CHANGE on the compound events. For example COPY (X) iff X = {R, W } represents an execution of the COPY protocol as defined above. The predicate COPY applies only to the higher-level events that describe executions of the COPY protocol, but the predicate Copier applies, in addition, to the higher-level Init_{0} event as well. Similarly, the predicate CHANGE applies to all operation executions of the CHANGE protocol, but the predicate Changer applies to these events and in addition to the Init_{1} event.

The resulting structure M is called a system execution. It represents an execution of the Copier/Changer system.

It is not difficult to prove that the relation <_{M} defined above on the events of M satisfies the following two properties.

Lamport Finiteness condition. For every event X (lower-level or compound) there is a finite set of events F such that if Y is any event in E \ F, then X <_{M} Y. That is, for every event X, X <_{M} Y holds for all events Y but for a finite number of exceptions.

Russell–Wiener property. If A, B, C, D are events such that

A <_{M} B, ¬(C <_{M} B), and C <_{M} D,

then

A <_{M} D.

Here ¬(C <_{M} B) is the negation of C <_{M} B. This negation is so basic that we give it a special symbol and define

B > |_{M} C iff ¬(C <_{M} B).

The introduction of compound events has led us to consider a precedence relation (namely <_{M}) on the higher-level events that is not necessarily serial but satisfies the Lamport Finiteness condition and the Russell–Wiener property. We next return to the general discussion and define system executions abstractly, that is, not as structures that are necessarily built over histories. More details about this notion can be found in Lamport’s [8], [9], in Pratt’s [12], and in [1], [2].

3.1 System Executions

We begin by defining interval-orderings as partial orderings that satisfy the Russell–Wiener property. An irreflexive and transitive relation R on E is called an interval-ordering iff

∀a, b, c, d ∈ E (a R b ∧ ¬(c R b) ∧ c R d ⟹ a R d)  (4)

It is easy to prove that if a = (a_{1}, a_{2}), b = (b_{1}, b_{2}) etc. are intervals of some linear ordering ≤, and R is defined by (a_{1}, a_{2}) R (b_{1}, b_{2}) iff a_{2} ≤ b_{1}, then (4) holds. Wiener [15] proved that any interval ordering can be represented by intervals of a linear ordering. This is the justification for the choice of interval orderings to model the precedence relation of system executions.

Definition 1 (Lamport [9]). A global-time model is a structure S = (E, <_{S} ) where E is a set (called the set of events) and <_{S} is a partial irreflexive ordering relation on E such that the following holds, where > |_{S} is defined on E by a > |_{S} b iff ¬(b <_{S} a):

1. <_{S} is an interval-ordering on E. That is for every a, b, c, d ∈ E

a <_{S} b > |_{S} c <_{S} d implies a <_{S} d.

2. For any a ∈ E, {x ∈ E | x > |_{S} a} is finite. (Lamport’s Finiteness condition) It follows that a global-time model is countable, and it can be infinite.

We write x ≤_{S} y as a shorthand for x <_{S} y or x = y.

Global-time models only give the precedence relations among the events but not any other useful information. Nor do the models describe those atemporal objects which are not situated in time and do not fall under the precedence relation (such as the set of possible register values). For this reason the definition of “system execution” given here involves not only events with their temporal ordering, but also atemporal objects, relations, and functions.

Definition 2. A system execution is a structure S = (E, C, <_{S} , F) such that (E, <_{S} ) is a global-time model, C is a set (of ‘atemporal’ objects), and F is a collection of functions and relations on E ∪ C.

A System execution is thus a structure in the sense of Tarski, it has a signature which determines its language, and a formal definition is given to explicate when a formula holds in the structure. As we shall see, the correctness of a protocol is expressed by a sentence, and the correctness proof consists in showing that this statement holds in each system execution that describes an execution of the protocol. It is often the case that the correctness sentence involves higher-level events and so we show how to introduce them into our system executions.

A system execution with higher-level events is a system execution with a membership relation ∈ (in F) such that <_{S} satisfies requirements (2) and (3). Usually there are only two levels in S: lower-level events have no members, and higher-level events are non-empty sets and are not themselves members of events. Extensionality holds for higher-level events: they are equal if they contain the same members.

1. If x ∈ X are a lower-level and a higher-level events and x is not a member of any other event, then we write X = [x]. (Usually, distinct events in E are disjoint in E).

2. We define the relation A <_{S} end(B) for higher-level events A, B by requiring that B has a last event b and

∀a ∈ A (a ≤_{S} b).

If A <_{S} end(B) then for every C such that B <_{S} C, A <_{S} C holds. This last property can be taken as the definition of A <_{S} end(B).

Lamport [9] identified and classified different types of registers, and in particular atomic and regular registers. Since we use these registers here we briefly discuss them and explain how histories combined with system-executions can deal with regular registers.

Registers can be characterized by the number of writing processes (owners) and the number of reading processes that can access them. An n-writer m-reader register is one with n owners (only these can issue write instructions) and m readers (that can issue read instructions). We can also say n-writer multiple-reader register, if the number of reading processes is not fixed.

Another way to classify registers is according to the degree of concurrency allowed and their behavior when a read and a write are concurrent. Suppose a system execution S with predicates Read(x) and Write(x) (saying that x is a read, respectively write, event) and with a function Value defined on the read/write events (Value(x) ∈ C is the message returned or written by the read/write event x). We also assume in S a function ω defined on the read events and such that ω(r) is a write event for every read r. We say that the read/write events and the functions ω and Value represent a register if ω(r) > |_{S} r and Value(r) = Value(ω(r)) for every read event r, and there exists a write event (the initial write) that precedes every other event. We classify registers as

– serial iff the read/write events are linearly ordered by <_{S} and ω(r) is the <_{S} rightmost write event w such that w <_{S} r;

– atomic if there exists an extension of <_{S} to a linear ordering <^{∗} on the read/write events such that, as above, ω(r) is the <^{∗} rightmost write event w such that w <^{∗} r;

– regular iff ω(r) > |_{S} r and there is no write event w such that

ω(r) <_{S} w <_{S} r.

In the framework of histories, regular registers are somewhat more difficult to represent than serial ones. There are two obstacles. The first is that the steps (and in particular the read/write steps) are atomic in any history H and are serially ordered. Yet regularity is meaningful only when the read and write events can be concurrent. Thus, instead of representing each read/write event by a single step of the history (as for serial registers), we associate with each read/write event two steps: start and conclude. But now comes the second problem: how should the value of the regular register be represented in each state? For a serial register this is simple: the value of the register is determined in each write step and it remains fixed until the following write. The read of the serial register just obtains the value registered by the state. For regular registers we must keep a set of possible values for each ongoing read event, and this is rather cumbersome. Fortunately this difficulty disappears when system executions are built on top of the histories. The register itself is not a state variable, and its regularity is expressed only by means of the functions ω and Value as above.

The term “regular” is employed here in a more general sense. Suppose that S is a system-execution and A, B ⊆ E are two sets of events (or unary predicates defined on sort of events E).

Definition 3. A function f : A → B is regular if it satisfies the following two properties.

1. f(a) > |_{S} a for every a ∈ A.

2. There is never b ∈ B such that f(a) <_{S} b <_{S} a.

3.2 Higher-level relations for the aimless protocol

Suppose that system execution S = (E, C, <_{S} , F) describes an execution of the aimless protocol, and that higher-level events were introduced as in the previous subsection. So E contains both the lowerlevel and the higher-level events. We assume a membership predicate e ∈ X to indicate that a lower-level event e belongs to a higher-level X. The collection of higher-level events in S is denoted HL. Sort C contains the atemporal elements of S, these are the values {0, 1} and the registers R_{0} and R_{1}. The registers R_{0} and R_{1} are assumed to be serial in S. Recall the function ρ, in F, that associates to each read event, r ∈ E a write event ρ(r) on the same register as described above.

Except for the Init events, the events in HL are of two types: CHANGE (in Changer) and COPY (in Copier), according as to whether the lower-level view of the event is an execution of the CHANGE or the COPY protocol.

Definition 4. Additional functions color and observe are defined on the higher-level events in S as follows. These are definable functions, that is the functional relation y = G(x) can be expressed by some formula with free variables x and y. Hence these functions are dispensable. Yet they are quite useful and so we introduce them into F.

1. The function color(X) is defined on the events in HL. color(X) is the value (0 or 1) of the variable t written onto register R_{0} (if X is a COPY) or R_{1} (if X is a CHANGE). In details, this definition uses the function Value. For any higher-level CHANGE or COPY event X = {R, W }, where W ∈ X is its write event, we define color(X) = Value(W). If X = {w} is an initial event, we define color(X) = Value(w). We assumed that color(I) = 0 for an Init event I, but this is not essential.

2. The function ‘observe’ is defined on the COPY and CHANGE events in HL by observe(U) = V iff for the (unique) read event r ∈ U, V = [ρ(r)]. When the write ρ(r) is the initial write onto the register, we say that U observes the Init event.

So observe takes COPY events into Changer events, and CHANGE events into Copier events. For example, if U = {r_{0}, w_{0}} is a COPY event, and r_{0} is the read there of R_{1}, then ω(r_{0}) is the corresponding write on R_{1}, executed by Changer. There are two possibilities. If ω(r_{0}) is the initial write on R_{1} then observe(U) = Init_{1}. Otherwise, ω(r_{0}) is the write event in some CHANGE event V. That is, ω(r_{0}) ∈ V (or V = [ω(r_{0})]), and then V = observe(U).

The following lemma lists some properties of these functions which are all easy to prove.

Lemma 1. The function observe, and the boolean function color, satisfy the following.

1. If U is a CHANGE/COPY event then:

(a) observe(U) <_{S} U,

(b) If V = observe(U) and V′ is in the same process as V (Copier or Changer) then V <_{S} V′ <_{S} U does not hold.

(c) For any higher-level events U_{1} ≤_{S} U_{2} in the same process,

observe(U_{1}) ≤_{S} observe(U_{2}).

2. If U is a CHANGE event then observe(U) is in Copier and

color(U) ≠ color(observe(U)).

3. If U is a COPY then observe(U) is in Changer and

color(U) = color(observe(U)).

We shall prove in details only (a) and (c) of the first claim, and then make an observation concerning the type of correctness proofs employed here. So let U be a CHANGE event (for example). We follow the definition of observe(U) in order to prove that observe(U) <_{S} U. Being a higher-level CHANGE event, U has the form U = {R, W } where R <_{S} W are its Read and Write events. Then we defined observe(U) = [ω(R)]. Since R is a read of Register(R) = R_{0}, ω(R) is a write on that register and

ω(R) <_{S} R

by properties of ω. Every write on R_{0} belongs to a unique higher-level Copier event, and so there are two possibilities for ω(R):

1. [ω(R)] = Init_{0} = {w_{cpy}} is the initial Copier event, and

2. [ω(R)] = {A, B} is a COPY event, where A <_{S} B are its read and write events.

In the first case w_{cpy} = ω(R) <_{S} R <_{S} W, and in the second case A <_{S} B = ω(R) <_{S} R <_{S} W. In both cases observe(U) <_{S} U follows from (2).

We prove now item 1(c) of the lemma. Put W_{i} = observe(U_{i}), for i = 1, 2. Then W_{1} and W_{2} are by the same process. If W_{1} ≤_{S} W_{2} does not hold, then W_{2} <_{S} W_{1} by the seriality of Changer and Copier. But W_{1} <_{S} U_{1} by Lemma 1.1(a). So W_{2} <_{S} W_{1} <_{S} U_{1} ≤_{S} U_{2} follows in contradiction to the regularity of observe (Lemma 1.1(b)).

When we analyze this proof we find, for example, that the following property was used: that each CHANGE event consists of two lower-level events which are a Read R (of register R_{0}) and a Write W (on register R_{1}) such that R <_{S} W. This property speaks only about events of the serial process Changer, and depends only on the text of CHANGE. We conclude that the proof of item 1(a) of the lemma depends only on:

1. Properties of Changer, such as the one given above as an example, which depend only on the CHANGE text and can be proved by methods that are applicable to serial processes, since no concurrency is involved.

2. Properties of Copier which depend only on the COPY text and not on any other protocol that may operate concurrently with Copier.

3. Properties of the reading function ω (expressed with the function Value).

4. Properties that hold in any system execution, namely the Lamport finiteness property and the Russell-Wiener property. It turns out that this separation of concerns is typical of the cor-

rectness proofs described here. The texts of the protocols are used to derive properties of each of the serial protocols, no interleaving or interactions between the processes is needed, and then properties of the communication devices (such as those expressed by ω and Value) are combined to derive the properties (such as those of Lemma 1) that are then used abstractly to conclude the correctness proofs.

Consider our system execution S which describes an execution of the Aimless Protocol, and let H be its reduct to the higher-level events. That is,

H = (HL, CH, <H, FH)

where HL is the set of higher-level events of S, CH = C is the sort of atemporal objects of S, <_{H} is the restriction of <_{S} to (the pairs of) HL, and FH consists of the functions and predicates from S that are defined on the higher-level events. Then all the properties derived in Lemma 1 hold in H. In the following definition we take an abstract approach and define the Changer/Copier system as the family of all system execution that satisfy these properties, whether they are reducts of executions of the protocol or not.

Definition 5. Let H be a system execution. We say that H is a (higher-level) Changer/Copier system execution if it has two (disjoint) serial processes: Changer and Copier; with events called CHANGE and COPY (respectively) and initialization events (that precede all other events), and it has functions called observe (defined on the CHANGE/COPY events) and color (defined on all events) so that the list of properties established in Lemma 1 holds for H.

From this point on, we shall not refer to the text of the Aimless Protocol, but instead rely only on the list of properties established in Lemma 1. Any property of the Aimless Protocol executions that we shall obtain will be derived by proving that it holds in any higherlevel Changer/Copier system execution. The import of this division of labor is that anyone wishing to give a formal correctness proof along the lines presented here, may use assertions and states in order to prove Lemma 1, but will have to use a general first-order deductive proof system in order to deal with the second, higher-level part of the proof.

We shall define a binary relation ≺ on the higher-level events and prove that it is a linear ordering of the higher-level events. Transitivity of ≺ is an example of a statement that is derived from the Changer/Copier list of properties, without any reference to the lowerlevel aspects of the protocol.

In any system-execution H of the aimless protocol we define the aimless ordering on the higher-level events as follows.

Definition 6 (The Aimless Ordering). Suppose that H is a higherlevel Changer/Copier system execution. For every events U and V in H define the relation U ≺ V to hold if and only if:

1. U <_{H} V, or

2. U and V are <_{H} incomparable (namely V > |_{H} U and U > |_{H} V) and one of the following options is the case:

(a) color(U) ≠ color(V), V is a Changer and U a Copier, or

(b) color(U) = color(V), V is a Copier and U a Changer.

So ≺ extends the <_{H} relation on the Changer/Copier events, and in case that <_{H} does not decide the priority, it is the Copier that wins if U and V have the same color, and the Changer otherwise.

The reader may prefer the following version (noted by a referee). If the processors Copier and Changer are denoted by the indexes 0 and 1 (respectively) then the ≺ ordering defined above could be defined succinctly by U ≺ V iff U <_{H} V or else (U > |_{H} V), id(U) ≠ id(V), and

color(U) = color(V) ⊕ id(V)

where ⊕ denotes addition modulo 2. The advantage of this is that it conforms to the notations of [4] and that it renders the proof of the following theorem shorter (no need to consider two separate cases). However, in this notation, the intuition that the Changer gets the advantage when the values are different and the Copier when they are equal is not as transparent as in the explicit definition.

Theorem 1. ≺ is a linear ordering of the Changer/Copier events that extends <_{H} .

Proof. It is clear that ≺ is irreflexive (for all V: ¬(V ≺ V)). Let U and V be any two events in Copier ∪ Changer. We shall prove the U ≺ V or V ≺ U. If U and V are <_{H} comparable, then this is obvious. Otherwise, U and V are <_{H} incomparable, and hence belong to different processes (since each process is serial). Say U is a Copier and V a Changer event. Then either color(U) = color(V) and then V ≺ U, or else color(U) ≠ color(V) and then U ≺ V.

Observe next that it is not possible for both U ≺ V and V ≺ U to hold. This is a direct consequence of the definition of ≺ and the fact that <_{H} is antisymmetric.

It follows that if V and U are <_{H} comparable and V ≺ U, then

V <_{H} U.  (5)

Indeed, otherwise U <_{H} V and then U ≺ V (since ≺ extends <_{H} ) and this contradicts the previous observation.

To prove transitivity of ≺, we first remark that if U ≺ V ≺ W then U, V, and W are three distinct events (U = W contradicts the observation made above). The following lemma deals first with the case that U <_{H} V.

Lemma 2. If U <_{H} V ≺ W, then U ≺ W.

Proof. Given any event W, the finiteness condition (Definition 1) implies that the set of predecessors p(W) = {X | X <_{H} W } is finite. Thus, if the lemma does not hold, there is a counter-example, W, with least cardinality of p(W). Then:

1. For some events U and V, U <_{H} V ≺ W and yet ¬(U ≺ W).

2. If W′ is an event such that p(W′) has smaller cardinality than p(W), then the theorem holds for W′. Namely for every U and V, U <_{H} V ≺ W′ implies U ≺ W′.

Assume that this minimal counter-example W is a Changer event. In case W is a Copier event the proof is almost the same. Suppose that U <_{H} V ≺ W but it is not the case that U ≺ W, and hence

W ≺ U  (6)

by our remark above that every two events are ≺ comparable.

If V and W are both in Changer, then V ≺ W implies that V <_{H} W (by (5), since they are different and comparable). In this case, U <_{H} V and V <_{H} W imply that U <_{H} W by the transitivity of <_{H} , and this contradicts (6). So we conclude that V is a Copier event.

By definition, there are two possible reasons for W ≺ U. The first is that W <_{H} U, and in this case U <_{H} V implies W <_{H} V which contradicts V ≺ W. Hence it must be the case that

W and U are <_{H} incomparable, they belong to different processes, and

color(W) = color(U).

And thus U is a Copier event.

(7)

So both U and V are Copier events, and we may assume in addition that:

V and W are <_{H} incomparable

(since otherwise V <_{H} W follows from V ≺ W and thence U <_{H} W can be concluded). So V ≺ W implies that

color(V) ≠ color(W).  (8)

Since U <_{H} V, V is a COPY event (and not the initial Copier event). So V_{0} = observe(V) is defined, it is a Changer event, color(V_{0}) = color(V), and V_{0} <_{H} V by the assumed Changer/Copier properties (of Lemma 1). Since V_{0} <_{H} V, V_{0} <_{H} W follows (or else W ≤_{H} V_{0} <_{H} V, which contradicts the fact that W and V are <_{H} incomparable). Thus V_{0} <_{H} W ≺ U.

We claim that ¬(V_{0} ≺ U). So that U is also a counter-example to the lemma. Yet |p(U)| < |p(W)|, as we shall see, and this contradiction to the minimality of W proves the lemma.

Why ¬(V_{0} ≺ U)? It follows from (8) that

color(V_{0}) = color(V) ≠ color(U),

and it suffices to prove that V_{0} and U are <_{H} incomparable in order to conclude that U ≺ V_{0}. Since U and W are <_{H} incomparable, it is clear that U <_{H} V_{0} is impossible. But V_{0} <_{H} U is also impossible, since in such a case V_{0} = observe(U) can be concluded, which is impossible since color(U) ≠ color(V_{0}).

Why V_{0} = observe(U) follows from V_{0} <_{H} U? Because V_{0} <_{H} U and the fact that these events belong to different processes imply that V_{0} ≤_{H} observe(U) by the regularity of observe. Yet U <_{H} V implies that observe(U) <_{H} observe(V) = V_{0}. Hence observe(U) = V_{0}, which leads to a contradiction, and so the incomparability of V_{0} and U is finally concluded.

Why |p(U)| < |p(W)|? Because if X ∈ p(U), then

X <_{H} U > |_{H} V_{0} <_{H} W

implies that X <_{H} W by the Russell–Wiener property. Thus p(U) ⊆ p(W). Yet V_{0} ∈ p(W) and V_{0} ∉ p(U). Hence p(U) is a proper subset of p(W).

Thus W is not a minimal counter-example, and a contradiction is obtained. ⊓ ⊔

Now we can prove that ≺ is transitive. Suppose that A ≺ B ≺ C. If A <_{H} C then A ≺ C as required. So C > |_{H} A can be assumed. If C <_{H} A, then C <_{H} A ≺ B gives C ≺ B by the lemma, which contradicts B ≺ C. Hence A and C are <_{H} incomparable. Thus A and C belong to different processes. But then B is either in the same process as A or in the same process as C. In the first case A <_{H} B (since each process is serial and A ≺ B). Then the lemma gives A ≺ C. In the second case B <_{H} C (since B ≺ C), and then A ≺ C is concluded, or else C ≺ A and then (by the lemma again) B ≺ A which is impossible. This proves Theorem 1.

The following interesting property of the Aimless Ordering says that at the point where color changes, the definition of ≺ is especially simple.

Lemma 3. Suppose that U <_{H} V are by the same process and V is the successor of U (there is no U′ by that same process such that U <_{H} U′ <_{H} V). If color(U) ≠ color(V), then for every event W, V ≺ W iff V <_{H} W.

Proof. One direction is trivial: if V <_{H} W then V ≺ W. Assume now V ≺ W and for the sake of a contradiction assume the negation of V <_{H} W. Since V ≺ W, V and W are <_{H} incomparable, they belong to different processes, and there are two cases depending on the colors of V and W. For example, assume that color(V) = color(W) = c, and then that V is a Changer and W a Copier (the case where the colors differ is similar).

W is certainly not the initial Copier event (for then W <_{H} V holds), and so observe(W) <_{H} W is defined. As V ≤_{H} observe(W) is impossible (it leads to V <_{H} W), observe(W) <_{H} V by the seriality of Changer. But V is the successor of U, and hence observe(W) ≤_{H} U. Equality (observe(W) = U) is impossible since W, observe(W), and V have the same color c, but color(U) ≠ c. So observe(W) <_{H} U, and hence it is not the case that U <_{H} W (by regularity of observe). Since W <_{H} U is also impossible (as it entails W <_{H} V) it must be that W and U are <_{H} incomparable. Yet U <_{H} V ≺ W implies, as we know, that U ≺ W. And hence color(U) = color(W), which is a contradiction since color(U) ≠ c.

4 Bloom’s two-writer protocol

The problem of implementing an atomic two-writer protocol (with single writer serial registers) can be described informally as follows. Suppose two processes, Writer_{0} and Writer_{1}, that repeatedly and independently write messages to a set of Readers. The communication means are single-writer multiple-reader serial registers that connect any Writer to the other processes. The problem is to find a protocol that implements atomic read/write operations with these means. The protocol should consist of a finite number k of instructions, with no loops or go-to instructions, which ensures that each operation execution takes ≤ k steps. The WRITE operation takes a Message parameter, the value to be written, and an index parameter (so that the protocol is specific to Writer_{0} and Writer_{1}). The READ operation returns a value. Atomicity of the operations means that there exists a linear ordering, ≺ extending <_{H} , of all operation executions, and such that, for any read event R, the value returned by R equals the value written by the ≺-maximal write W such that W ≺ R.

Bloom [4] was the first to solve this problem, and his solution is in Figure 2. Registers R_{0}, and R_{1}, are written by Writer_{0}, and Writer_{1} respectively, and read by the other process. These registers are assumed to be serial. Each register has two fields: color and message. Field color is boolean (its values are {0, 1}), and the message field carries values of a determined type, Message, which the implemented register has to transmit. An instruction read(R_{1}; ⟨t, v⟩), for example, reads register R_{1} and assigns its two fields to variables t and v

WRITE (a : Message); (* for Writer_{0} *)

1. read(R_{1}; ⟨t, v⟩);

2. write(R_{0}; ⟨t, a⟩);

WRITE (a : Message); (* for Writer_{1} *)

1. read(R_{0}; ⟨t, v⟩);

2. t := 1 − t;

3. write(R_{1}; ⟨t, a⟩).

READ

1. read(R_{0}; ⟨t_{0}, v_{0}⟩);

2. read(R_{1}; ⟨t_{1}, v_{1}⟩);

3. r := \{ \begin{matrix}0 & IF t_{0} = t_{1} \\ 1 & IF t_{0} ≠ t_{1}; \end{matrix}

4. read(R_{r}; ⟨t_{2}, v_{2}⟩);

5. return v_{2}.

Fig. 2 The Protocol of Bloom.

(color and message fields respectively). The local variables t, t_{0}, t_{1} are boolean, and v, v_{0}, v_{1}, v_{2}, a are of type Message.

We continue with some informal remarks. Observe that the Writers are executing the aimless protocol with only one additional feature: the message a is also written into the registers. Thus Writer_{0} corresponds to Copier: it reads register R_{1}, retains the color t obtained, and writes on R_{0} the value ⟨t, a⟩, which has the color t and message a (the invocation parameter) as fields. Similarly, Writer_{1} corresponds to Changer.

Both Writer_{0} and Writer_{1} are serial, repeatedly executing their WRITE protocol with arbitrarily chosen message parameters. Reader is not serial, and different READ events may be concurrent. We can require that Reader consists of a finite number of serial processes, repeatedly executing the READ protocol.

Reader does not write on any register, it only reads three times the writers’ registers. At first, it reads the registers of Writer_{0} and Writer_{1}, then it computes the index r to be returned, and finally it reads again the register of Writer_{r} and returns the message found there. So the first two reads serve to choose the return index, and the third one to find the message. Hesselink [6] has proved that the order in which the first two reads of the READ protocol are executed is immaterial–they can be read in any order and, in fact concurrently.

Let R be an execution of the READ protocol; the last read (the execution of line 4) is the one that brings the return value of R. The intuition behind the choice of the return index r is the following. The READ wants to determine who is the winner in the aimless game, the Copier or the Changer, and it is the index of the process that seems to be the winner that is returned.

It is instructive to see what goes wrong when the third read is omitted from the READ protocol, and lines 4 and 5 are replaced by return v_{r}. There may be W_{0} <_{H} W_{1} <_{H} R where W_{0} and W_{1} are WRITE events by Writer_{0} and Writer_{1} respectively, and R a READ, and R returns W_{0}.

Let L = (L, C; <_{L} , F) be a system execution which is an execution of the protocol (built on top of a history as in Section 3). We assume that the processes in L are Writer_{0}, Writer_{1}, and a number of reading processes which repeatedly execute the READ protocol. The registers, R_{0} and R_{1}, used by the Writers for writing and reading, and by the Readers for reading are assumed to be serial in L. The function ρ in F associates, to every read r ∈ L of register R_{i}, the <_{L} rightmost write w to R_{i} such that w <_{L} r. For some initial message a_{0}, the pair (0, a_{0}) is assumed to be initially written to R_{0} and to R_{1} (color 0 is for definiteness–any colors will do).

System execution L also contains higher-level events obtained by collecting sets of lower-level events as follows.

1. Every single execution of the READ or WRITE protocol forms a higher-level event.

2. The two singletons formed from the two initial write events form initial higher-level events. Thus Init_{0} and Init_{1} are formed in Writer_{0} and Writer_{1}.

The collection of higher-level events thus obtained and assumed to be in L is called HL. the events in HL are thus of type READ or WRITE, or the two special events Init_{0} and Init_{1}. We say that X is a Writer event if X is in Writer_{i} for i = 0 or i = 1; that is, X is either a WRITE event (an execution of the protocol) or one of the Init events. A Reader event (synonymous with READ) is an execution of the READ operation.

We are going to define and add to L functions defined on the set HL of higher-level events.

1. To begin with, set id(W) = i iff W is executed by Writer_{i}.

2. The function color associates to a Writer event W the value of the field color, as written on its register.

3. The function observe, from WRITE events in Writer_{k} into Writer_{1−k} is defined as follows. For a WRITE event, W, observe(W) = V iff for the read event r ∈ W, V = [ρ(r)] holds (namely ω(r) ∈ V).

4. For any event X in HL, define message(X) to be of type Message: for a Writer event this is the value of the parameter a (or a_{0} for an Init event); and for a READ event it is the value returned (in line 5 of the READ protocol).

5. The definition of the return function Ω : READ⟶Writer is natural. For every READ event, R, let r ∈ R be the read (of registers R_{0} or R_{1}) executed for line 4 of the protocol. Let w = ρ(r), and let W be the unique Writer event in HL such that W includes w. Then define W = Ω(R). id(Ω(R)) is called “the return index of R”. We will later see that there is no WRITE event W_{1} such that Ω(R) <_{L} W_{1} <_{L} R. For now, it suffices to observe the obvious property that there is no such W_{1} with id(W_{1}) = id(Ω(R)).

6. We need to introduce to L another function: consider(R, i) defined for a READ event R and an index i = 0, 1. Let r_{0} and r_{1} be the two reads in R of registers R_{0} and R_{1} respectively executed for lines 1 and 2 of the READ protocol. Then define:

consider(R, 0) = [ρ(r_{0})], consider(R, 1) = [ρ(r_{1})].

As before, L continues to denote the system execution in which the higher-level functions were added. If now we collect all the higherlevel events HL, and restrict the precedence relation <_{L} of L to HL, and take only the functions and predicates defined on HL, then the resulting system execution H (a reduct of L) is called a higher-level view of an execution of Bloom’s protocol.

By repeating the corresponding proofs of the Aimless Protocol, the reader can check that Lemma 1 holds in any higher-level view of Bloom’s protocol as well. These properties of the lemma and additional properties concerned with the readers events are listed in the following subsection. Their proofs are not difficult and are left to the reader.

4.1 The abstract properties of Bloom’s protocol

This section lists abstracts properties of a system execution

H = (HL, C; <_{H} , G).

These hold whenever H is a higher-level view of an execution of Bloom’s protocol, and hence we shall refer to this list as the “abstract (higher-level) properties of Bloom’s protocol”. Yet, these properties may hold for other protocols as well (as we will see in Section 5). In section 4.3 it will be proved that atomicity is a consequence of these properties.

The signature of H (that is the language interpreted by H) contains the following unary predicates: Reader, Writer_{0}, Writer_{1}, READ, WRITE defined on the events. Unary predicate Message defined on the atemporal sort C (to specify which are the data values). Binary predicate < (= <_{H} ) which is the temporal precedence relation.

Functions id, consider, color, observe, message, and Ω. And constants 0 and 1 in C (considered both as colors and indexes for the writers).

The events of H are partitioned into the following processes (unary predicates, considered as subsets of HL) Reader, Writer_{0}, and Writer_{1}:

1. The Reader process is not necessarily serial. (Predicate Reader and READ have the same extension.)

2. Each of the two writer processes is serial. Writer_{i} contains the event Init_{i}, and its other events are called WRITE events. We assume that Init_{i} <_{H} X for any WRITE or READ event X. We define Writer as the union of Writer_{0} and Writer_{1}. We define id(X) = i if X is in Writer_{i}.

The set G of functions and predicates of H also contains the following functions (with properties as defined below). For any READ event R and Writer’s index i = 0, 1 consider(R, i) is in Writer_{i}. For any Writer event W, color(W) is in C = {0, 1}, and observe(W) is in Writer. Ω is a function defined on the READ events and taking in Writer events values. For any event X, message(X) is of type Message. If R is a READ event, message(R) is called the return value of R.

The remaining part of the abstract properties of Bloom’s protocol is formed by three group of specifications: cons, obs, and ret. consider properties

cons.1 Defined on any Reader event R, consider(R, 0) and consider(R, 1) are regular functions (into Writer_{0} and Writer_{1} respectively). This means that for every i = 0, 1 and READ event R

consider(R, i) > |_{H} R

is in Writer_{i} and there is no Writer_{i} event W such that

consider(R, i) <_{H} W <_{H} R.

It follows from this assumption that if W is a Writer_{i} event such that W <_{H} R, then W ≤_{H} consider(R, i). Indeed, if it were not so and consider(R, i) is neither W nor a later Writer_{i} event, then the seriality of Writer_{i} would lead to consider(R, i) <_{H} W <_{H} R which is impossible.

cons.2 : Suppose that i is the return index of R (that is i = id(Ω(R))).

Then

consider(R, i) ≤_{H} Ω(R).

observe and color properties

obs.1 For any WRITE event W, observe(W) satisfies:

1. id(observe(W)) ≠ id(W).

2. observe(W) <_{H} W.

3. There is no WRITE V with id(V) = id(observe(W)) such that observe(W) <_{H} V <_{H} W.

It follows immediately that if W is a WRITE and V_{0} <_{H} W is a Writer event with id(V_{0}) ≠ id(W), then V_{0} ≤_{H} observe(W).

obs.2 For any WRITE, W:

id(W) = 1 iff color(W) ≠ color(observe(W)).

obs.3 For every READ event R and every index i, if V = consider(R, i) is a WRITE event (that is, not an initial Writer event) then observe(V) is defined, and we have that

observe(V) ≤_{H} Ω(R).

Ω properties

ret.1 message(R) = message(Ω(R)). ret.2 If V_{i} = consider(R, i) for i = 0, 1, then id(Ω(R)), the return

index, equals 0 if color(V_{0}) = color(V_{1}); the return index is 1 otherwise. Again, using the addition mod 2 operator, ⊕, this property can be succinctly written as

id(Ω(R)) = color(V_{0}) ⊕ color(V_{1}).

ret.3 Ω(R) <_{H} end(R), and there is no WRITE, W, such that id(W) = id(Ω(R)) and Ω(R) <_{H} W <_{H} R.

This ends the list of abstract properties of Bloom’s protocol. It is easy to prove that they hold in every execution of the protocol of Bloom. As an example we prove here obs.3. In the following subsection it will be proved that they imply atomicity.

Figure 3 illustrates the following argument. So let R be a READ event, and i = 0, 1 be any index. We assume that V = consider(R, i) is a WRITE event. By definition, if s ∈ R is the read of register R_{i} done in executing line 1 (if i = 0 or line 2 (if i = 1), then V = [ω(s)]. Clearly V <_{H} s, since ω(s) is the last event in V. (If V is an initial event then V = {ω(s)}, and otherwise V is a WRITE event and then V = {a, b} with a <_{H} b = ω(s).) In any case, ω(s) <_{H} s implies that V <_{H} s.

Define U = observe(V). Then id(U) = 1 − i and U <_{H} V.

Let r ∈ {0, 1} be the return index of R, and let t ∈ R be the read of register R_{r} corresponding to line 4 of the READ protocol (the last read in R). Then Ω(R) is defined to be [ω(t)]. Clearly s <_{H} t. There

[figure: U = observe(V); V = consider(R, i); R; s; t]

Fig. 3 An illustration for the proof of obs.3. A horizontal line represents time (flowing from left to right), and thin rectangles on such a line represent temporal intervals of higher-level events. Arrows represent lower-level reads.

are two possibilities according to whether r = i or not. But since U <_{H} V <_{H} s, U <_{H} V <_{H} t. So in case r = i, V ≤_{H} Ω(R), and in case r = 1 − i, U ≤_{H} Ω(R) follow the regularity of ω. In both cases U ≤_{H} Ω(R) as required.

Let H be any system execution in which these abstract higherlevel properties of Bloom’s protocol hold. Restrict H to Writer_{0} and Writer_{1}, and let H_{1} be the resulting system execution. So H_{1} is obtained by throwing away the Reader events from H. If the processes Writer_{0} and Writer_{1} are now called Copier and Changer respectively, then H_{1} becomes a Changer/Copier system execution, because the statements of Lemma 1 are restated in the obs specifications. Hence the Aimless Ordering ≺ (see Definition 6) is defined on the events in H_{1} and Theorem 1 holds, which says that ≺ is a linear ordering extending <_{H} .

For convenience, we repeat this Aimless Ordering in our context. Let U and V be any Writer events in H. Define U ≺ V to hold iff:

1. U <_{H} V, or

2. U and V are <_{H} incomparable (namely V > |_{H} U and U > |_{H} V) and one of the following options is the case:

(a) color(U) ≠ color(V), V is in Writer_{1} and U in Writer_{0}, or (b) color(U) = color(V), V is in Writer_{0} and U in Writer_{1}. For future reference we state as a theorem our observation above

that the higher-level properties of Bloom’s protocol implies the translation of Theorem 1

Theorem 2. If H satisfies the higher-level properties of Bloom’s protocol, and if ≺ is defined on the Writer events as above, then ≺ is a linear ordering of the Writer events that extends the precedence relation H.

4.2 Atomicity

We want to prove that if H satisfies the abstract properties of section 4.1, then the implemented register is atomic. In order to do this, we will formulate four properties, P0—P3, in the language involving the relations <_{H} , ≺, READ, Reader, WRITE, Writer, and the functions message and Ω. Then we will prove that these properties imply atomicity of the READ/WRITE operations, and finally we will prove that they are a consequence of the abstract Bloom’s properties of section 4.1.

P0 The predicates READ and Reader are equivalent (we have both for flexibility of expression). Predicate WRITE is included in Writer and the events that fall under Writer but not under WRITE are the initial events (they precede any other events). The processes Reader and Writer are not assumed to be serial.

P1 For any READ event, R, Ω(R) = W is a Writer event in H and

message(W) = message(R).

P2 Ω(R) > |_{H} R, and even Ω(R) <_{H} end(R). (This is the ‘Bloom con-

dition’) P3 Relation ≺ is a linear ordering of the Writer events, which ex-

tends the precedence relation <_{H} on these events. It is never the case that W_{1} ≺ W_{2} <_{H} R where W_{i} are Writer events for i = 1, 2 and R a READ event such that W_{1} = Ω(R).

Theorem 3. If properties P0—P3 hold in H, then the Reader/Writer events in H satisfy the requirement for atomicity. That is, there is an extension of <_{H} to a linear ordering <^{∗} so that the return value message(R) of any READ R is equal to the value message(W) of the <^{∗} rightmost Writer event W in H such that W <^{∗} R.

Proof. Consider the serial ordering ≺ of the Writer events. For every Writer event W define the “block” of W, B(W), to consist of W together with all READ events R such that W = Ω(R). So R ∈ B(Ω(R)). Now define <^{∗} as follows.

If W_{1} ≺ W_{2}, then for every X ∈ B(W_{1}) and Y ∈ B(W_{2}) define X <^{∗} Y. For events that are in the same block, B(W), we define <^{∗} by making W the first event in its block (W <^{∗} R for every READ R ∈ B(W)), and defining <^{∗} on the READ events in B(W) in any way that extends <_{H} on these events (any partial ordering can be linearized). Clearly, <^{∗} is a linear ordering. We must prove the following:

1. message(Ω(R)) = message(R) for every READ R.

2. Ω(R) <^{∗} R and there is no Writer event W such that Ω(R) <^{∗} W <^{∗} R.

3. <^{∗} extends <_{H} .

Now (1) is stated in P1. Ω(R) <^{∗} R is a direct consequence of the definition of <^{∗}. Namely, if W = Ω(R), then R is in B(W) and we define W <^{∗} R. It is equally clear that Ω(R) <^{∗} W <^{∗} R is impossible, since if Ω(R) <^{∗} W, then Ω(R) ≺ W (by definition of <^{∗}) and then X <^{∗} Y for every X ∈ B(Ω(R)), Y ∈ B(W), Thus R <^{∗} W (because R is in the block of Ω(R) and W is in B(W)). The only non-trivial property to prove is that <^{∗} extends <_{H} . For Writer events, this is clear since W_{1} <_{H} W_{2} implies W_{1} ≺ W_{2}, and hence W_{1} <^{∗} W_{2}. There are thus three cases to check, which involve: two reads, a read followed by a write, and a writer event followed by a read. A. Let R_{1} <_{H} R_{2} be two READ events. If they belong to the same

block, then R_{1} <^{∗} R_{2} by the explicit requirement on <^{∗} restricted to any block that it extends <_{H} . So assume that Ω(R_{1}) ≠ Ω(R_{2}). We want to prove that Ω(R_{1}) ≺ Ω(R_{2}) in order to conclude that R_{1} <^{∗} R_{2}. But if this were not the case, then Ω(R_{2}) ≺ Ω(R_{1}). Yet Ω(R_{1}) <_{H} end(R_{1}) by P2, and then R_{1} <_{H} R_{2} implies that Ω(R_{1}) <_{H} R_{2}. Thus Ω(R_{2}) ≺ Ω(R_{1}) <_{H} R_{2} in contradiction to P3.

B. Suppose that R <_{H} W where R is a READ and W a WRITE event. Then Ω(R) <_{H} W since Ω(R) <_{H} end(R) by P2. Hence the block of Ω(R) is to the left (in <^{∗}) of the block of W, and in particular R <^{∗} W.

C. Finally suppose that W <_{H} R, where R is a READ and W a Writer event. Compare W and Ω(R) in the ≺ ordering. If W = Ω(R), then W <^{∗} R since the write is the first event in its block. If W ≺ Ω(R), then W <^{∗} R follows. But Ω(R) ≺ W <_{H} R is impossible by P3. It remains to show how P0–P3 are derived from the specifications

of section 4.1.

4.3 The abstract properties imply atomicity

This subsection is devoted to the proof of the following. Theorem 4. Assume that system execution H satisfies the abstract properties of Bloom’s protocol of section 4.1. Then properties P0— P3 hold in H, and hence the READ/WRITE events in H implement an atomic register (by Theorem 3).

Properties P0, P1, and P2 are explicitly stated (ret.1 and ret.3). Before proving P3 we need the following.

Lemma 4. Let R be a READ event and V, U be the two Writer events considered by R. That is

{V, U} = {consider(R, 0), consider(R, 1)}.

Suppose that V ≺ U and yet id(V) is the return index of R. Then

V <_{H} observe(U) ≤_{H} Ω(R).

Proof. Suppose that id(U) = 0; the proof in case id(U) = 1 is almost the same and is hence left to the reader. So we assume that U = consider(R, 0), and V = consider(R, 1). So 1 is the return index of R, and this implies (ret.3) that

color(U) ≠ color(V).

We analyze the reasons for V ≺ U. Suppose first that V and U are <_{H} incomparable. Then the definition of ≺ and the difference of colors imply that U ≺ V which is a contradiction to the fact that ≺ is a linear ordering (see Theorem 2).

Next suppose that V and U are <_{H} comparable, and hence that V <_{H} U (as U <_{H} V is impossible, since ≺ extends <_{H} ). So U is not the initial event, and hence observe(U) is defined. obs.1 implies that V ≤_{H} observe(U). Equality V = observe(U) is impossible, because it implies that color(V) = color(U) since U is a “copier”. So V <_{H} observe(U), and observe(U) ≤_{H} Ω(R) by obs.3. This gives the desired conclusion. ⊓ ⊔

To prove P3, suppose that

W_{1} ≺ W_{2}, W_{2} <_{H} R, and W_{1} = Ω(R)

and we shall get a contradiction. If W_{1} and W_{2} have the same index then they are <_{H} comparable and hence W_{1} <_{H} W_{2} (since W_{1} ≺ W_{2}). But then W_{1} <_{H} W_{2} <_{H} R contradicts W_{1} = Ω(R) (by ret.3). Thus we may assume that id(W_{1}) ≠ id(W_{2}). Say i = id(W_{1}), and j = id(W_{2}). So i is the return index of R.

Define V_{1} = consider(R, i) and V_{2} = consider(R, j). Then V_{1} ≤_{H} W_{1} (by cons.2).

Also W_{2} <_{H} R implies that

W_{2} ≤_{H} V_{2}

by cons.1. Thus V_{1} ≤_{H} W_{1} ≺ W_{2} ≤_{H} V_{2} and V_{1} ≺ V_{2} follows (since ≺ extends <_{H} and is transitive). By the previous lemma

V_{1} <_{H} observe(V_{2}) ≤_{H} Ω(R) = W_{1}.

So V_{1} <_{H} W_{1}. Hence W_{1} is not an initial event. But then neither W_{2} is an initial event (or else W_{2} <_{H} W_{1} in contradiction to W_{1} ≺ W_{2}).

Define V = observe(V_{2}). We claim that color(V_{1}) ≠ color(V) and V is the successor of V_{1} in their process. For example, assume that V_{1} is in Writer_{1}, and V_{2} in Writer_{0}. So the return index i is 1, and this implies that the two colors considered by R are different, namely that color(V_{1}) ≠ color(V_{2}). Yet V = observe(V_{2}) and V_{2} have the same color, since V_{2} in Writer_{0} is the copier. This shows that V_{1} and V have distinct colors.

Now V is the successor of V_{1}, for otherwise there would be an event X in the process of V_{1} and V such that V_{1} <_{H} X <_{H} V. But then R > |_{H} X (or else V_{1} <_{H} X <_{H} R will contradicts V_{1} = consider(R, i)). Hence

W_{2} <_{H} R > |_{H} X <_{H} V ≤_{H} W_{1}

yields W_{2} <_{H} W_{1} in contradiction to W_{1} ≺ W_{2}.

Lemma 3 can be applied now to V_{1} <_{H} V. Since V ≤_{H} W_{1} ≺ W_{2}, V ≺ W_{2} and the lemma concludes that V <_{H} W_{2}. So V <_{H} R, but then V_{1} <_{H} V <_{H} R is impossible.

5 A variant of Bloom’s protocol

The Writers in Bloom’s protocol are required to access a record that contains two fields: color and message. The message field may be very long and the necessity to access such heavy registers may slow down the writers. Even though the writers do not really read (use) the message field, the system has to provide atomically both fields to the processes and is thus an expensive system. Moreover this association of the control and data fields may be undesirable if privacy is important and it is required that a writer should not be able to access the messages of the other writer. We are going to describe a variant of Bloom’s protocol which does not require the Writers to read such heavy registers. Our aim is to separate the control values from the data values, to assign different registers for control and for data, and to ensure that the WRITE protocol requires reading only of control registers.

The main reason for bringing this variant is to exemplify an advantage of our two-tier proof method. In the lower-level part of the

(* Protocol for Writer_{0} *)

WRITE (a : Message);

1. read(R_{1}; t);

2. write(B_{0}; a);

3. write(R_{0}; t).

(* Protocol for Writer_{1} *) WRITE (a : Message);

1. read(R_{0}; t);

2. t := 1 − t;

3. write(B_{1}; a);

4. write(R_{1}; t);

5. parity := 1 − parity.

READ

1. read(R_{0}; t_{0});

2. read(R_{1}; t_{1});

3. r := \{ \begin{matrix}0 & IF t_{0} = t_{1} \\ 1 & IF t_{0} ≠ t_{1}; \end{matrix}

4. read(B_{r}; v);

5. return v;

Fig. 4 Erroneous Protocol. An unsuccessful attempt to separate control and data registers.

correctness proof of the variant we prove that its executions satisfy the abstract higher-level properties of Bloom’s protocol (listed in section 4.1), and then for the second part of the proof we need just to quote Theorem 4 which yields immediately that the implemented register of the variant is atomic.

At first, it may seem easy to separate control from data registers. Let R_{0}, R_{1} be boolean, serial registers (to carry the control values of Bloom’s protocol) and let B_{0} and B_{1} (written by Writer_{0} and Writer_{1} respectively) be the data registers (assumed to be serial). A register that only carry messages and no control information is called here a buffer. Then try the (erroneous) protocol of Figure 4. It is soon discovered that the implemented register is not atomic (see Figure 5 for a hint). Observe that all properties from the list of section 4.1, except for obs.3 hold. We are going to see how the usage of two buffers per writer can remedy this.

We are going to use the elegant construction by Vidyasankar [14]. This construction implements a single-writer multiple-reader atomic register with a single-writer multiple-reader serial (or atomic) register that carry only (boolean) control values, and two single-writer multiple-reader regular registers that carry the messages.

Combining Bloom’s protocol with the construction of Vidyasankar, the control serial registers are no longer boolean, since they have the double role of serving both Bloom and Vidyasankar protocols. Thus

[figure: A_{0}; B_{0}; A; R_{1}; B; b; w; R_{2}]

Fig. 5 An illustration for the Erroneous protocol of Figure 4. A_{0} <_{H} B_{0} <_{H} A <_{H} B are WRITE events. Writes A_{0} and A are by one the the writers, say Writer_{i} and writes B_{0} and B are by Writer_{1−i}. The lower writes by B on its registers B_{i−1} and R_{i−1} are denoted b and w. R_{1} <_{H} R_{2} are READ events, where the return index of R_{1} is 1 − i (because it considered A_{0} and B_{0}. Yet R_{1} returned the value written by B (since it obtained the value written by the write b on B_{1−i}. The return index of R_{2} however is i because it considered B_{0} and A. This shows that if the implemented register is atomic then B ought to be ordered before A. Yet this is impossible since A precedes B. Observe that B = Ω(R_{1}) shows that ret.3 fails since Ω(R_{1}) <_{H} end(R_{1}) does not hold.

registers R_{0} and R_{1} here contain two bits each. The resulting protocol is displayed in Figure 6.

We need for this variant protocol two regular buffers per writer, B_{i}[0] and B_{i}[1] which are written by Writer_{i} and read by Reader, for i = 0, 1.

In any system execution S of the protocol, we assume a return function ρ defined on the lower-level reads as before. But now, for reads of the buffers B_{i}[ℓ], which are regular, we only assume regularity of ρ. This means that for any read r of a buffer B_{i}[ℓ], ω(r) is a write on that buffer such that

1. Value(ρ(r)) = Value(r).

2. ρ(r) > |_{S} r.

3. There is no write event, w, onto B_{i}[ℓ] such that ρ(r) <_{S} w <_{S} r.

For each i, Writer_{i} alternates the use of buffers B_{i}[0] and B_{i}[1]: in the k-th execution of the WRITE, Writer_{i}, writes its message onto B_{i}[p], where p = k (mod 2).

The serial registers R_{0} and R_{1} carry control information only. This is a record containing a pair ⟨t, p⟩ of boolean values: p is called the parity, and t the color. The initial value of R_{i} is the pair ⟨0, 1⟩. The initial value of the buffers is some initial message. There is a local boolean variable, parity, initialized to 1.

(* Protocol for Writer_{0} *)

WRITE (a : Message);

1. read(R_{1}; ⟨t, p⟩);

2. write(B_{0}[parity]; a);

3. write(R_{0}; ⟨t, parity⟩);

4. parity := 1 − parity.

(* Protocol for Writer_{1} *) WRITE (a : Message);

1. read(R_{0}; ⟨t, p⟩);

2. t := 1 − t;

3. write(B_{1}[parity]; a);

4. write(R_{1}; ⟨t, parity⟩);

5. parity := 1 − parity.

READ

1. read(R_{0}; ⟨t_{0}, p_{0}⟩)

2. read(R_{1}; ⟨t_{1}, p_{1}⟩)

3. r := \{ \begin{matrix}0 & IF t_{0} = t_{1} \\ 1 & IF t_{0} ≠ t_{1} \end{matrix}

4. read(B_{r}[p_{r}]; v_{0});

5. read(R_{r}; ⟨t′, p′⟩)

6. IF p_{r} = p′ THEN return v_{0}; ELSE

(a) read(B_{r}[p′]; v_{1});

(b) read(R_{r}; ⟨t′′, p′′⟩)

(c) IF p′′ = p′ THEN return v_{1} ELSE return v_{0}. (* necessarily p′′ = p_{r} in this case *)

Fig. 6 The Variant Protocol, combining Bloom and Vidyasankar’s protocols.

As in Bloom’s protocol, W riter_{0} is copying the color observed in register R_{1} of Writer_{1}, and Writer_{1} is reversing the color observed in Writer_{0}. The first three lines of the READ protocol resemble the corresponding lines in Bloom’s protocol: the reader first considers Writer_{0} and Writer_{1}. The determination of the return index, r, is made in line 3 as before, but now only control variables are read (in lines 1 and 2). Then either the read of one or two buffers is needed to determine the return value (as opposed to three reads of message carrying registers in Bloom’s protocol). The value returned is obtained in reading B_{r}[x] where x = 0, 1 is so chosen that there are two reads of register R_{r}, one preceding and one following the read of B_{r}[x], so that the parity of both reads of R_{r} is x. ^{1}

We notice that the Variant Protocol is not obtained by simply replacing read and write operations in Bloom’s protocol by the read and write procedures of Vidyasankar’s protocol. Hence we cannot simply quote and assume the correctness of Vidyasankar’s protocol and obtain the correctness of the variant.

1 This procedure employed by the READ to decide which value to return is quite involved; it was devised by by [14] and also employed by [5] (Construction MC4).

5.1 The higher-level properties hold

Given a lower-level execution of the variant protocol, the higherlevel view H is defined similarly as for Bloom’s protocol by collecting lower-level read/write events into READ and WRITE events, and two higher level initialization events. A higher-level initialization event contains two lower-level writes on B_{i}[parity] and on R_{i}, that is the initial writes onto the message and the coordinating registers. Remark that since the higher-level events consist of read/write lowerlevel events, the last lower-level event in a WRITE is a write onto R_{i} and not the local change of the parity.

The function color(W) for a WRITE event is the value of variable t written on the color field of register R_{i}. The parity of W is the parity field value as written on R_{i}. So, If W is the k-th WRITE execution by its Writer (k = 1, 2, …) then parity(W) = k mod 2, and W writes on buffer B_{i}[parity(W)] (where i = id(W)).

The return function Ω is defined by looking, for a given READ R, at the “return read”, s, and setting Ω(R) = [ρ(s)]. This return read is determined as follows. In case p_{r} = p′, or p_{r} = p′′, the return read is the read of B_{r}[p_{r}] (in line 4). Otherwise (p_{r} ≠ p′ = p′′) the return read is the read of B_{r}[p′] in line 6. The other functions are defined as for Bloom’s protocol.

So for every WRITE event W in Writer_{k}, observe(W) = [ω(r)] where r ∈ W is the read there of register R_{1−k}. For every READ R

consider(R, 0) = [ω(r_{0})], consider(R, 1) = [ω(r_{1})]

where r_{0} and r_{1} are the reads in R of registers R_{0} and R_{1} done in lines 1 and 2 of the Variant READ protocol.

The reader will easily recognize that the abstract higher-level properties of Bloom’s protocol of section 4.1 hold, and that the only non-trivial part is the proof that Ω(R) <_{H} end(R).

To prove this, let R be any READ event, and suppose that r is the return index of R, ℓ is the parity of Ω(R), s is the return read of B_{r}[ℓ] in line 5 or 7, and r_{1} is the last read of register R_{r} in R. If Ω(R) is the initial Writer_{r} event, then Ω(R) <_{S} R holds, and so we can assume that Ω(R) is a WRITE event. Then

1. [ρ(s)] = Ω(R),

2. s <_{S} r_{1}, and

3. ℓ is the parity field value of ρ(r_{1}).

Now let w_{1} be the write in Ω(R) on register R_{r}. We claim that w_{1} <_{S} r_{1}, and this clearly implies Ω(R) <_{H} end(R). If this is not the case, then r_{1} <_{S} w_{1} by the seriality of R_{r}. The parity of w_{1} is ℓ which is the parity of Ω(R). Let w_{0} be the last write on R_{r} preceding w_{1} (since Ω(R) is not the initial WRITE, w_{0} exists). So w_{0} <_{H} Ω(R). Then (by the alternation of parities of successive writes) the parity of w_{0} is 1 − ℓ. But w_{0} <_{S} Ω(s) > |_{S} s <_{S} r_{1} implies that w_{0} <_{S} r_{1} and hence r_{1} is between two successive writes w_{0} and w_{1} onto R_{r}. Hence w_{0} = ρ(r_{1}) and its parity is 1 − ℓ in contradiction to 3 above.

6 Conclusion

The ‘behavioral’ approach (and ours could probably be characterize as such) has been criticized for being prone to mistakes. For example, L. Lamport and F. B. Schneider write ([7] p. 203):

“Most computer scientists find it natural to reason about a concurrent program in terms of its behavior—the sequence of events generated by its execution. Experience has taught us that such reasoning is not reliable; we have seen too many convincing proofs of incorrect algorithms. This has led to assertional proof methods, in which one reasons about the program’s state instead of its behavior. Unlike behavioral reasoning, assertional proofs can be formalized—i.e., reduced to a series of precise steps that can, in principle, be machine-verified.”

I agree that it is natural to reason in terms of behavior: this type of reasoning can also use diagrams, and is easier to communicate. However, I think that natural and reliable reasoning about concurrent programs can be established in terms of behavior analysis. The aim of [2] is to show how behavioral reasoning can be formalized in a way that does not forsake intuition, and the aim of this paper is to exemplify the main traits of our approach by proving the correctness of Bloom’s atomic register protocol ([4]). Key elements in this approach are the following.

1. The notion of system execution of Lamport ([9]) is expanded, and now these are structures in the model theoretic sense, having a signature and assigning truth values to sentences in its language.

2. The semantics of concurrently operating (serial) processes that execute a certain protocol, P, is formally defined by assigning a family of system execution that describe the manifold of all possible executions of P. This is done as follows.

(a) The semantics of each of the serial processes is expressed with states and histories in the traditional way. Properties of each serial processes can be proved by any of the methods that use assertions and inductive proofs.

(b) The combined histories can be formed, and then system executions are built on top of these histories. This is exemplified in Section 3, where system executions of the Aimless Protocol are built over interleaving histories. (In [2] system executions of protocols are defined in a more general way which does not require interleaving histories. Only histories of the serial processes are used.)

3. Higher-level events are defined in the system executions, and the reducts of these system executions to the higher-level events are investigated abstractly. This means that higher-level properties are formulated (such as those of the Aimless Protocol, listed in Section 3.2) and then consequences of these properties are derived abstractly, not in connection with the text of the protocol. In this higher-level derivation only the higher-level properties of the protocol are used, together with the properties that are common to all system executions: the Russell-Wiener property of the temporal precedence relation and its Lamport finiteness property.

An advantage of this two-level proof is that it allows abstract reasoning and mathematical proofs about higher-level properties, and it simplifies the correctness proofs of different protocols that share the same higher-level properties. For example, a variant of Bloom’s two-writer protocol is presented here and its correctness is proved in this modular fashion that involves two levels. Since this variant satisfies the abstract properties of Bloom’s protocol, its correctness proof is reduced to the lower-level. The improvement in this variant is the separation between the data and coordination values which are now carried by different registers. The writing processes in this variant read only coordinating registers. The protocol is obtained by combining Vidyasankar’s [14] algorithm into Bloom’s.

References

1. U. Abraham, On interprocess communication and the implementation of multi-writer atomic registers, Theoretical computer science, 149, (1995) 257– 298.

2. U. Abraham, Models for Concurrency, Gordon and Breach, 1999.

3. F. Anger, On Lamport’s interprocess communication. ACM Transactions on Programming Languages and Systems, 11, No. 3, (1989) 404 - 417.

4. B. Bloom, Constructing two-writer atomic registers. 6th ACM Symp. on Principles of Distributed Computing, (1987) pp. 249 - 259. and IEEE Transactions on Communications, 37, (12) (1988) 1506–1514.

5. S. Haldar and K. Vidyasankar, Simple Extensions of 1-Writer Atomic Variable Constructions to Multiwriter Ones, Acta Informatica, 33, (1996) pp. 177–202.

6. W. H. Hesselink, An assertional Criterion for Atomicity. Acta Informatica 7. L. Lamport and F. Schneider, Chapter 5 in: Distributed Systems. M. Paul and

H. J. Sieger (eds) Lecture Notes in Computer Science 190, Springer. 1985.

8. L. Lamport, A new approach to proving the correctness of multiprocess programs, ACM Trans. on Prog. Lang. and systems bf 1, (1979) 84-97.

9. L. Lamport, On Interprocess Communication, Part I: Basic formalism, Part II: Algorithms, Distributed Computing, 1, (1986) 77 - 101.

10. N. A. Lynch, Distributed Algorithms. Morgan Kaufmann, 1996.

11. G.L Peterson and J.E. Burns, Concurrent reading while writing II : the multiwriter case. FOCS-87 (1987).

12. V. Pratt, Modeling Concurrency with Partial Orders. International J. of Parallel Programming, 15, (1986) 33 - 71.

13. W. P. de Roever, Concurrency Verification, Cambridge Tracts No. 54 (2001).

14. K. Vidyasankar, An elegant 1-writer multireader multivalued atomic register. Information Processing Letters, 30, (5) (1989) 221-223.

15. N. Wiener, A contribution to the theory of relative position. Proc. Camb. Philos. Soc. 17, (1914) 441-449.