The elusive atomic register.
We present a construction of a single-writer, multiple-reader atomic register from single-writer, single-reader atomic registers. The complexity of our construction is asymptotically optimal; O(M2 shared single-writer, single-reader safe bits are required to construct a single-writer, M-reader, N-bit atomic register.
Introduction
The currently accepted theory of concurrent computing is deeply rooted in the concept of
atomic registers. An atomic register is a data object that is read or written by one or
more processes according to the following assumption: if several read or write operations
of the register are enabled simultaneously in different processes, then these operations are
executed in some sequence, one after the other, and not concurrently. This assumption
strongly suggests the well-known interleaving semantics of concurrent computations. The
validity of this assumption is thus a cornerstone in justifying the present theory of concurrent
computing.
One way to check the validity of this assumption is to show that an atomic register
can be constructed using a set of more realistic registers that can be read and written
concurrently by different processes. In such a construction, a process reads or writes the
constructed atomic register by invoking a program; within such a program, only registers of
the more realistic kind are read or written. Different programs can be invoked by different
processes concurrently; it is required, however, that the net effect resembles that of a serial
invocation. The programs are restricted to be wait-free, i.e., synchronization primitives,
such as P , V , or await, and unbounded busy-wait loops are not allowed. This restriction
guarantees that a process reads or writes the constructed atomic register in a finite amount
of time, regardless of the activities of other processes. (This also means that the read or
write of a process is immune to the failure of other processes that also access the register.)
The wait-freedom restriction distinguishes the problem of constructing an atomic register
from the classic readers-writers problem [6].
Peterson [16] was the first to suggest the problem of constructing atomic registers from
safe registers. A safe register is a data object that can be read or written concurrently by
different processes; if a read operation overlaps a write operation then it may return any
value from the value domain of the register, and if a read operation does not overlap any
operation then it obtains the most recently written value. The leap from safe registers
to atomic registers is quite large; fortunately, it can be divided into a number of smaller
steps.

Figure

1 depicts two chains of register constructions that lead from single-writer,
single-reader, single-bit safe registers to K-writer, M-reader, N -bit atomic registers. The
notation K=M=N denotes a register that can be written by K processes, can be read by M
processes, and can store an N -bit value. Each step in the figure is labeled by a reference to
the papers in which the given construction is presented.
Henceforth, we concern ourselves only with single-writer atomic registers. The problem
of constructing a multiple-reader atomic register from single-reader atomic registers was
mentioned as an open problem by Lamport [12] and by Vitanyi and Awerbuch [23]. The
first solution to the problem was presented by us in [2], where a two-reader construction is
given and then generalized to construct an M-reader register from (M \Gamma 1)-reader registers.
This solution, though easy to explain and understand, uses an exponential number of single-
Safe
Atomic
Atomic
Atomic
K=M=N
Atomic
-[12, 20] [2, 4, 7, 10, 13, 15, 19] [3, 13, 17, 18, 23]
[2, 4, 7, 10, 13, 15, 19] [16, 21]

Figure

1: Two Chains of Register Constructions.
reader atomic registers. Subsequently, several solutions with polynomial complexity have
been presented [4, 10, 13, 15], including one given by us in [19]. The latter construction is
a generalization of our two-reader construction.
In this paper, we present a construction of a multiple-reader atomic register that is based
upon the solution in [19]. The presentation of this construction differs from that of [19] in
two respects. First, the solution presented here is of optimal complexity, whereas the one
given in [19] is not. (Actually, an optimal solution can be attained by combining the solution
in [19] with constructions by Lamport [12] and Peterson [16] - see [19] for details.) Second,
the correctness proof presented in this paper is more rigorous and formal (and, we hope,
easier to understand) than the proof presented in [19].
The rest of the paper is organized as follows. In Section 2, we formally define the problem
of constructing an M-reader atomic register from single-reader atomic registers. In Section
3, we present our construction. An informal description of this construction is presented in
Section 4 and a formal correctness proof is presented in Section 5; the proof makes use of
several lemmas, which are stated and proved in an appendix. Concluding remarks appear
in Section 6.
Register Construction
Register constructions can be defined in a number of different ways. Our choice of definitions
is based on simplicity and convenience.
In order to avoid confusion, we henceforth capitalize terms such as "Read"
and "Write" when they apply to the constructed register, and leave them uncapitalized when
they apply to the variables used in a construction. 2
We view the Writer (and each Reader) of a construction as a program that is invoked
by a process in order to Write (Read) a value to (from) the register. The program for the
Writer has one input parameter indicating the value to be Written; similarly, the program
for each Reader has one output parameter indicating the value Read. As an example, see
the constructions depicted in Figures 2 and 3.
Each variable of a construction is a single-reader, single-writer atomic register - this
restriction arises since our aim is to construct a multiple-reader register from single-reader
registers. We also require that all variables are bounded in size. (There is a very simple solution
if the variables are unbounded [23].) As mentioned in the introduction, each program
of a construction is "wait-free," i.e., synchronization primitives and busy-wait loops are not
allowed. (For a more formal definition of wait-freedom, refer to [1].)
Next, we define several concepts that are needed to state the correctness condition for a
multiple-reader construction. These definitions apply to a given construction.
A state is an assignment of values to the variables of the construction. (Note
that each program's ``program counter'' is considered to be a variable of the construction.)
One state is designated as the initial state. 2
An event is an execution of a statement of a program. 2
and u be any two states of a construction such that state u is the result
of executing some statement at state t. If e is the event corresponding to this statement
execution, then we say that e is enabled at state t and we write t e
!u. A history of a construction
is a sequence t 0
is the initial state. 2
precedes another event f in a history iff e occurs before f in the history.Definition: The set of events in a history corresponding to some complete program execution
is called an operation. An operation p precedes another operation q in a history iff
each event of p precedes all events of q. 2
Observe that the precedes relation is an irreflexive total order on events and an irreflexive
partial order on operations.
For the proof of correctness of a construction, it is sufficient to consider only histories
in which an initial Write operation precedes all other operations and in which there are
no incomplete program executions (i.e., operations). From now on, we deal only with such
histories. Note that by assuming that there is an initial Write operation, the value Read
by any Read operation can be matched with that Written by some Write operation. This
is equivalent to defining the initial state to be equal to that which results after the initial
Write operation. Note also that a history with incomplete operations can be extended to
one with complete operations; this is possible since all programs are required to be wait-
free. By dealing only with complete operations, the value "Read from" or "Written to" the
constructed register by an operation is well-defined.
Notation: We denote the ith operation of the Writer, where
denotes the initial Write.) 2
Following Lamport [12], we define the correctness condition for a construction as follows.
Let h be any history of a construction. h is said to be atomic iff there exists a
function OE that maps every Read operation in h to some natural number i, where W : i is a
Write operation in h, such that the following three conditions hold.
ffl Integrity: For each Read operation r in h, the value Read by r is the same as the
value Written by W : OE(r).
ffl Proximity: For each Read operation r in h, r does not precede the Write operation
and the Write operation W : (OE(r)+1) does not precede r.
ffl Precedence: For any two Read operations r and s in h, if r precedes s then OE(r) - OE(s).Definition: A register construction is correct iff all its histories are atomic. 2
3 Multi-Reader Construction
The proposed construction depicted in Figure 2 consists of a Writer program and a program
for each Reader i, where 1 Each shared variable in the construction is of the
single-reader kind. The interface between the Writer and Reader i consists of a variable
WR[i] that is written by the Writer and read by Reader i and a variable RW [i] that is
written by Reader i and read by the Writer. The interface across Readers consists of a
set of variables RR[i; j], where i - j. Variable RR[i; j] is written by Reader i and read by
Reader j. 1 An explanation of the field names appearing in the type definitions is as follows.
alt: A bit that alternates in value with each operation of the Writer.
done: A bit that distinguishes the two values written by a Write operation to variables
WR[i].
new: The "current" value of the constructed register. (valtype is the type of the constructed
register.)
old: The "previous" value of the constructed register.
1 It is possible to eliminate variables RR[i; i] from the construction. However, including these variables
simplifies the proof of correctness.
of RRtype for each i in the range 1 -
initialization
own new : valtype;
initialization
begin
0: old; new; alt := new; val; :alt;
1: for k := 1 to M do read q[k] := RW [k] od;
2: for k := 1 to M do seq[k] := q[k] \Phi 1 od;
3: for k := M to 1 do write WR[k] := (old; new; seq[1::M ]; alt; false) od;
4: for k := 1 to M do write WR[k] := (old; new; seq[1::M ]; alt; true) od
returns valtype
var
define
lag -
initialization
begin
0: read x := WR[i];
1: write RW [i] := x:seq[i];
2: for k := 1 to i do read v[k] := RR[k; i] od;
3: read y := WR[i];
4: f lag :=
5: for k := i to M do write RR[i; k] := (f lag; y:seq[i]; y:alt) od;
lag then return(y:new) else return(y:old) fi

Figure

2: Multiple-reader construction.
f lag: A bit that indicates whether a Read operation returned the old or the new value.
seq: A modulo-3 integer "sequence number." (\Phi denotes modulo-3 addition.)
Variables that are local to a program are declared in either a var or an own block. A
variable declared in an own block is assumed to retain its value across invocations of the
corresponding program. A variable declared in a var block is not assumed to retain its value
across invocations. The initialization assertions that follow the variable declarations serve
to define appropriate initial values for the variables of the construction; any state satisfying
these assertions is a suitable initial state. (However, recall that, by assumption, the initial
Write operation precedes all Read operations.)
In the programs of the construction, we use a special syntax in order to distinguish reads
and writes of shared variables from reads and writes of local variables. A program reads a
given shared variable Z by executing a statement of the form "read u := Z," where u is a
local variable of the same type as Z. A program writes a shared variable Z by executing
a statement of the form "write Z := u." If variable Z consists of m fields, then u is an
m-tuple; the ith component of u is a local variable whose value is to be stored in the ith
field of Z. We use similar names (sometimes identical) for the components of u and the
fields of Z, so the correspondence should be obvious.
The sequence numbers shared between the Writer and the Readers form the basis of our
construction. Included in every value written by the Writer is a set of sequence numbers,
one per Reader. During each Write operation, the Writer reads variable RW [k], where
to obtain the most recent sequence number of Reader k. A new sequence
number for Reader k is then obtained by incrementing that read from RW [k] using modulo-
3 addition. The Writer then writes to the Readers in two passes; in the first pass the Writer
writes to the Readers in the order from M to 1, and in the second pass this order is reversed.
The done bit distinguishes the two passes. The value that the Writer writes to each Reader
includes both the previous and current value of the constructed register, the aforementioned
set of sequence numbers, and the alt and done bits.
Each Reader i reads two values from the Writer, x and y. Between these reads, the
sequence number obtained from the first read is written back to the Writer and a value is
read from each Reader k, where k - i. The values read from the Writer and Readers are
used to compute the f lag bit, which indicates whether the old or new value from y is to be
returned. Note that f lag is assigned a value based upon the expressions These
expressions have been introduced as a shorthand, and are defined in the define section.
Before returning a value, Reader i writes a value to each Reader k, where k - i. This value
includes Reader i's f lag bit and also the sequence number for Reader i and alt bit of the
Writer obtained during Reader i's second read from WR[i].
We now calculate the space complexity of our construction by determining the number
of shared single-writer, single-reader safe bits required. The size of each shared variable in
the construction is as follows.
consists of 2M
consists of 2 bits.
consists of 4 bits.
Using the construction of [22], a single-writer, single-reader, B-bit atomic register can be
constructed using shared single-writer, single-reader safe bits. For our construction,
this yields a space complexity of 6M 2 +6MN +26M +19M (M +1)=2. It is well known that
the lower bound on space for this problem is our construction
is asymptotically optimal.
Given the correctness proof of Section 5, our construction establishes the following theorem

Theorem: It is possible to construct a single-writer, M-reader, N -bit atomic register using
shared single-writer, single-reader safe bits. 2
4 Informal Explanation
In this section, we explain the intuition behind the algorithm by discussing some of the
proof obligations that will be established in the next section and in the appendix. Before
doing so, however, we introduce some notation that will be useful in the ensuing discussion.
be an operation of program P and i be a label of a statement in P . If i
is not a for loop, then denotes the event corresponding to the execution of statement i
in operation p. Otherwise, if i is a for loop, then denotes the event corresponding to
the iteration of the loop in which the loop counter equals j. 2
For example, for a Write operation w of the construction in Figure 2, w : 1:i denotes the
event in which w reads from RW [i] and w : 4:i denotes the event in which w writes to WR[i]
for the second time. Next, we define three types of control predicates [11].
be an operation of program P in some history and let be an event
of p. Then, p at i is true at a state of the history iff the event before i is
true at a state iff the state occurs before the event after i is true at a state iff
the state occurs after the event
If n is the label of a for loop in program P , then we use p before n as a shorthand
for (8i :: p before n:i); we use p after n as a shorthand for (8i :: p after n:i); and we use
p at n as a shorthand for (9i :: p at n:i) -
Observe that if i is not a for loop, then p at i implies p before i. In particular, p at i
strengthens p before i by also requiring that p : i be enabled. On the other hand, if i is a
for loop, then it is possible to have p at i - :(p before i). This assertion holds when some
event of the loop other than the first is enabled. The following assertions are a consequence
of the preceding definition; let p and i be as given in the definition.
ffl :(p after
As examples of control predicates, observe that for any Write operation w of the construction
in

Figure
ffl w after 1:i denotes that w has read the sequence number from Reader i,
ffl w before 4 denotes that the w has not begun its second pass of writes,
ffl w after 4:i denotes that w has completed its write to Reader i in the second pass,
and
ffl w after 4 denotes that w has completed its second pass of writes.
Let A and B be two state assertions. The assertion A unless B holds iff for
every pair of consecutive states in any history, if A-:B holds in the first state, then A-B
holds in the second state. 2
Our notion of unless has been borrowed from the UNITY logic of Chandy and Misra [5].
Informally, A unless B means that once A becomes true, it remains true unless B becomes
true. In particular, if A is falsified by some event, then B either is true at the state prior to
the occurrence of that event, or is true at the state following the occurrence of that event.
There is no requirement that B eventually becomes true; however, in that case A remains
true forever.
be an operation, and z be any local variable of p. Then, p!z denotes the
final value of variable z as assigned by operation p. 2
Now, we are ready to explain the intuitive idea of the algorithm. Let us examine some
Write operation w of the Writer. Assume that w changes the value of the register from old
to new. It is possible to identify two points a and b within the execution of w such that
no Reader returns new before a and no Reader returns old after b. Let us call the interval
between a and b the uncertainty interval of w.
In establishing the correctness of a construction, the main difficulty is ensuring that
the precedence condition (in the definition of an "atomic history" given in Section 2) is
not violated during the uncertainty interval of a Write operation such as w. This amounts
to proving that new-then-old conflicts do not arise in this interval. Avoiding new-then-
old conflicts is difficult because of the fact that only single-reader registers are used in the
construction. As a result of this limitation, w must inform the Readers of the new value
being Written one at a time. Thus, during the uncertainty interval of w, there exist certain
points at which some, but not all, of the Readers have been informed by w that the value
new is currently being Written. This difficulty will be encountered in any construction of a
multiple-reader atomic register from single-reader ones.
In our solution, the uncertainty interval begins after the Writer writes to WR[1] in the
second pass and ends after the Writer writes to WR[M ] in the second pass. In other words,
the uncertainty interval exists while the predicate w at 4 - :w before 4 is true. Our
solution should therefore guarantee the following three properties.
Reads before the beginning of this interval do not return the new value.
Reads after the end of this interval do not return the old value.
Reads during this interval do not result in new-then-old conflicts.
To state these properties precisely, we define a predicate Cue that relates the values
written by a particular Write operation to the existing value of variable RR[i; j], where
Informally, predicate Cue(w; i; j) can be thought of as a cue from Reader i to Reader
j that Reader i has returned the new value of w. This predicate is defined as follows:
Cue(w; lag - RR[i;
According to the Reader program, if both values read from WR[j] by Reader j were written
by Write operation w, and if the value read from RR[i; j] satisfies the above predicate, then
Reader j will find predicate p i to be true and subsequently return the value new.
Returning to the discussion of the uncertainty interval, by property (A0), we should
ensure that Cue(w; i; j) is false before the beginning of the interval. In other words,
Control predicate w after 1:i is added as a conjunct to ensure that the value w!seq[i], which
is used in the definition of Cue(w; i; j), is available to Reader i. We prove the above property
as Lemma 4 in the appendix. Based on this lemma, Readers do not return the new value
before the beginning of the uncertainty interval and property (A0) holds.
Now, consider an operation r of Reader i and assume that both values read from WR[i]
by r were written by w. If r begins after the uncertainty interval of w, then r will find p 0
to be true; consequently, r will return the value new. Thus, Readers do not return the old
value after the end of this interval and hence property (A1) holds.
Finally, we have to ensure that property (A2) holds, i.e., that new-then-old conflicts are
avoided within the uncertainty interval. Consider successive Read operations by Reader i
and Reader j. There are two cases to consider: either i - j or j ! i. The former case is
not too difficult. If an operation of Reader i returns the value new during the uncertainty
interval of w, then, upon completing, it establishes Cue(w; i; j). If we can show that this
predicate will remain stable during the uncertainty interval then Reader j will also return
the value new and new-then-old conflicts will not arise. The stability of Cue(w; i; j) is
captured by the following property,
w at 4 - Cue(w;
which is proved as Lemma 5 in the appendix.
The latter case is more interesting, as there is no direct communication from Reader i
to Reader j if j ! i. In order to avoid new-then-old conflicts in this case, we have to rely
upon either the Writer completing its writes to Reader j or some other Reader k ! j setting
Cue(w; k; j) to true. In other words, we have to show that
w at 4 - Cue(w; l; i)
Let us examine the above assertion in detail. It states that, during the uncertainty interval
of w, if Reader i is cued by some Reader l (and hence, returns the new value) then for any
smaller j (to which Reader i does not write any values), either w has written its final values
to Reader j (in which case Reader j will return the new value) or Reader j in turn has
been cued by some Reader k (in which case, from the stability of Cue(w; k; j), Reader j will
again return the new value). This property is proved as Lemma 9 in the appendix. This
completes the last remaining obligation, (A2), of the proof that new-then-old conflicts do
not occur. Our formal proof in the next section mirrors the intuitive explanation presented
here.
5 Proof of Correctness
We prove that our construction is correct by defining a function OE for a given history, and by
showing that the defined OE meets the three conditions of integrity, proximity, and precedence
defined in Section 2. The following notational conventions and definitions are used in the
proof.
Notation: In order to avoid using too many parentheses, we define a binding order for the
symbols that we use. The following is a list of these symbols, grouped by binding power;
the groups are ordered from highest binding power to lowest.
+, \Gamma, \Phi
=, 6=, !, ?, -, OE, -
Let e and f be two events in some history. Then, e OE f j e precedes f , and
e be the event corresponding to the execution of the statement read z := Y
in an operation p, where z is a local variable and Y is a shared variable. If the value that p
reads from Y is written by operation q, then we say that operation q determines p!z. 2
Let r and s be any two operations of Reader i and Reader j respectively
such that r!y is determined by the Write operation and s!y is determined by the Write
operation precedes s and m ?
Proof:
fdefinition of determinesg
precedes sg
determines s!y and definition of determinesg
ftransitivity of OEg
operations occur sequentially in a historyg
ng
Let r be any Read operation, and suppose that Write operation
r!y. Then, OE(r) is defined as follows.
lag
otherwiseObserve that OE(r) is nonnegative. To see this, recall that the initial Write operation
by assumption, precedes all Read operations. Thus, if r!y is determined by W : 0,
then r!y:done - holds. This implies that r!f lag holds; hence,
Proof of Integrity: Let r be any Read operation, and suppose that Write operation
determines r!y. If lag is true (definition of OE) and r returns the value
r!y:new, i.e., the value Written by W : m. If lag is false (definition of
OE) and r returns the value r!y:old, i.e., the value Written by W
Proof of Proximity: Let r be an operation of Reader i, and suppose that Write operation
r!y. Because does not precede
does not precede r. Thus, if then proximity is satisfied.
In the case since r does not precede W : m, clearly r does not
1). We next show that does not precede r. From the definition of
implies that r!f lag is false. Hence, r!p 0 is also false. By the definition
of p 0 , this implies that r!y:done is false or r!x:seq[i] 6= r!y:seq[i]. If r!y:done is false, then
3:i. Thus, in either case
does not precede r. 2
Proof of Precedence: The proof of precedence is quite complicated and consists of a
somewhat lengthy case analysis, most of which has been relegated to the appendix. Here,
we make use of Lemmas 6, 10, and 11, which are proved there. These three lemmas are
based on Lemmas 4, 5, and 9 discussed in the informal description in the previous section.
Let r be any operation of Reader i, and s be any operation of Reader j such that r
precedes s. Our proof obligation is to show that OE(r) - OE(s).
Assume that Write operations determine r!y and s!y, respectively. Observe
the following.
ng
fby definition of OE,
ffrom observation proved earlier,
r precedes s
fby definition of OE,
in the appendixg
fby definition of OE,
fby definition of OE,
fby definition of OE, OE(s) - ng
fby definition of OE and f lag,
fLemmas 6 and 11 in the appendixg
true
6 Discussion
We have shown that a single-writer, M-reader, N -bit atomic register can be constructed
in a wait-free manner using single-writer, single-reader atomic registers. Our construction
requires O(M 2 +MN ) shared single-writer, single-reader safe bits, which is asymptotically
optimal.
Our definition of atomicity is equivalent to that given by Misra in [14]. His axioms for
atomicity in essence require that all read and write operations be shrunk to a point; such
a shrinking of operations is possible iff a function OE that meets the three conditions of our
definition exists. Recently, Herlihy and Wing [8] have extended the idea of atomicity to
arbitrary abstract data types by defining the concept of linearizability . Though akin to
serializability, the usual correctness criterion for concurrent execution of transactions, there
are some subtle differences between the two concepts. One important distinction is that
linearizability is a local correctness condition whereas serializability is not. We refer the
reader to [8] for further details.
In order to prove the correctness of a multiple-reader atomic register construction, a
function OE that meets the three conditions of integrity, proximity, and precedence has to be
defined for every possible history. This leads to long, and somewhat tedious proofs, mainly
because such a proof must take into account all possible ways in which Reads and Writes
can overlap. To keep the resulting case analysis in our proof to a minimum, we chose the
function OE to be very simple; it depends only on the boolean variable f lag. If our proof
appears formidable, in spite of this simplification, then it is because we have been very formal
in our reasoning, so as to leave no doubt about the validity of the proof. However, given the
length of our proof, it seems reasonable to inquire whether there exist other approaches to
constructing an M-reader register that facilitate simpler correctness arguments. We briefly
describe such an approach next.
The main idea behind this approach is to develop a construction of an M-reader (M - 2)
register from a collection of (M \Gamma 1)-reader registers. An M-reader register can then be
implemented from single-reader registers by recursively applying the construction, first to
replace all (M \Gamma 1)-reader registers by (M \Gamma 2)-reader ones, then to replace all
registers by (M \Gamma 3)-reader ones, and so on.
A simple implementation of an M-reader register from (M \Gamma1)-reader registers is depicted
in

Figure

3. In this construction, the Writer and Reader 1 are denoted as W and R,
respectively. The remaining Readers are denoted S 1 through SM Readers
execute the program called S. The construction uses two single-reader shared variables,
WR and RW , and two shared variables, WS and RS. Each variable's name
indicates those programs that read and write it, respectively. For example, WS is written by
the Writer W and is read by Readers S 1 through SM \Gamma1 . Observe that each of the Readers
shared variables. This fact is crucial and is exploited in recursive
applications of the construction. The local variables used in the construction are similar to
those used in the construction in Figure 2.
The primary advantage of the above recursive construction is that the proof of correctness
can be simplified by assuming that there are only two Readers, namely R and S. Specifically
we can ignore the possible interleavings that may arise among Readers S 1 through SM \Gamma1
when considering the proofs of integrity, proximity, and precedence. This follows quite
easily for the proofs of integrity and proximity, as these conditions relate an individual
Read operation with operations of the Writer. As for the proof of precedence, note that
the precedence condition only restricts the values returned by Read operations that are
in a strict precedence relationship with one another. Because Readers S 1 through SM \Gamma1
initialization
lag
program
own new : valtype;
begin
old; new; alt := new; val; :alt;
read q := RW ;
program R returns valtype program S returns valtype
var
begin begin
read x := WR; read x := WS ;
read y := WR; read y := WS ;
f lag := lag -
return(x:new) return(y:new)
else
return(y:old)

Figure

3: Recursive construction.
execute identical programs and write no shared variables, the only precedence relationships
that are of interest are the following: a Read operation of R precedes a Read operation of
some Read operation of R precedes another Read operation of R; a Read operation
of some S j precedes a Read operation of R; and a Read operation of some S j precedes a
Read operation of some S k . These cases are precisely those that arise in the special case
when 2. Thus, the proof of correctness for the M-reader register reduces to the much
simpler task of proving the correctness of a two-reader construction consisting of Readers
R and S.
A formal proof of correctness for the construction of Figure 3 appears in [2], where this
construction was first presented. In the remainder of this section, we informally describe how
the construction works for two Readers by comparing it to the general construction given
earlier in Figure 2. (In the general construction considered here, we assume that variables
are removed; see the footnote at the beginning of Section 3.
Hence, in the Reader program, the loop index in statement 2 is from 1 to and the loop
index in statement 5 is from i +1 to M .) We begin our comparison by considering a variant
of the two-reader version of the general construction in Figure 2. This variant is shown
in

Figure

4 (a). In this variant, some statements have been combined into larger atomic
statements, which we denote by enclosing them within angle brackets 'h' and `i'. Note also
that we have renamed the programs and variables to coincide with the names given in Figure
3. We have also moved the assignment to seq[1] so that it occurs immediately after the read
from RW . These changes to our original construction clearly do not affect the construction's
correctness. Thus, because our original construction is correct, the construction shown in

Figure

4 (a) is also correct.
Now, consider the code for W in Figure 4 (a). The fifth atomic statement of W always
assigns the value true to WR:done. Hence, the done field of WR can be removed without
affecting the construction's correctness. With this change, the W 's fifth atomic statement
can be replaced by a single write to WR.
Next, consider Reader S. The first atomic statement of S assigns the same values to local
variables x and y. Thus, in Reader S's calculation of f lag, which depends on p 0 and p 1 as
defined in Figure 2, is a tautology and can be removed. With this change,
the seq[2] fields of the construction serve no useful purpose and hence all can be removed.
Finally, the condition Reader S's computation of f lag
is also a tautology. Instead of removing it, we choose to replace it by another tautology
y. These changes, which clearly do not affect the construction's correctness, yield the
code given in Figure 4 (b). In this figure, we have not shown Reader R, as its code has not
been changed.
Note that, in the construction of Figure 4 (b), the only statement that reads or writes
multiple shared variables is the first statement of Reader S - all other such statements
have been eliminated. It turns out that with a few slight changes to the code for Reader R,
the first statement of Reader S can be broken into three separate statements. The required
program
begin
old; new; alt := new; val; :alt;
read q[1] := RW ;
hread q[2] := SW ;
hwrite WR := (old; new; seq[1]; seq[2]; alt; false);
program R returns valtype program S returns valtype
begin begin
read x := WR; hread x := WS ;
read y := WR; read v := RS;
f lag := p0 ; read y := WS
lag := p0 - p1 ;
if f lag then return(y:new) if f lag then return(y:new)
else return(y:old) fi else return(y:old) fi
(a)
program returns valtype
begin begin
read q[1] := RW ; read v := RS;
lag := y:done - lag -
lag then return(y:new)
else return(y:old) fi
(b)

Figure

4: Two intermediate constructions.
changes to Reader R are as follows: Reader R computes its f lag by f lag :=
f lag := y:done - assigns (f lag; x:seq[1]; x:alt) to RS rather
than (f lag; y:seq[1]; y:alt); and Reader R always returns x:new. With the last change, it
turns out that the Writer no longer needs to write the old value to Reader R. The resulting
construction is the same as that given in Figure 3. This completes our comparison of the
two constructions.
Although the construction of Figure 3 has a simpler correctness proof than that of

Figure

2, this simplicity comes at a price. In particular, as shown in [2], the construction
of a multiple-reader register requires a number of bits that is exponential in the number of
Readers.

Acknowledgements

We would like to thank Ted Herman and the UT Distributed Systems
Discussion Group for their comments on this paper. We would also like to thank Nancy Lynch and
the anonymous referees for their helpful comments.


Appendix

Remainder of Correctness Proof
Here we prove the lemmas that were used in the proof given in Section 5. As outlined
in the informal discussion of the algorithm in Section 4, Lemmas 4, 5, and 9 relate the
uncertainty interval of a Write operation to the values of variables RR[i; j], which are used
for communication between Readers. Lemmas 1, 2, and 3 state some elementary results that
are used in proving subsequent lemmas. Lemmas 7 and 8 are used to prove some results
that are used in the proof of Lemma 9. Lemmas 6, 10, and 11 consider the values returned
by two successive Read operations and are used in the proof of precedence presented in
Section 5.
A few words concerning the structure of the proofs are in order at this juncture. In most
of our proofs, the reasoning is based upon sequences of states or events. (In other words,
we assume a total order on all reads and writes of internal variables in the construction.)
Wherever possible, the proofs have been simplified through the introduction of invariants.
In establishing these invariants, we usually proceed by a case analysis on the order of events
that may "affect" one another. For example, consider a Write operation w and a Read
operation r of Reader i. Operation w reads a sequence number from Reader i and operation
r writes a sequence number to the Writer. So, it is possible to do a case analysis on whether
w's read of the sequence number occurs before r's write of the sequence number. On the
whole, the proofs are not difficult, but, due to the numerous interleavings of events that
may potentially occur, they are rather lengthy. The following definitions will be used in the
proofs; the first is repeated from Section 4.
Let w be a Write operation, and let 1
Cue(w; lag - RR[i;
Consider the history t 0
We say that t i is the state prior
to the event e i and t i+1 is the state following e i . Similarly, e i is the event prior to the state
t i+1 and e i+1 is the event following the state t i+1 . 2
Lemma 1: Let r be an operation of Reader i such that r!p k holds for some k - i. Let w
be the Write operation that determines r!y. Then,
holds at the state prior to the event r : 2:k.
Proof: By the program for the Writer,
3. Therefore, by transitivity, w : 1:i OE r : 3. This implies that w!q[i] is determined by either
r or some predecessor of r.
We now show that r does not determine w!q[i]. Because r!p k holds,
Because w determines r!y, Therefore, by transitivity, we have
If r determines w!q[i], then As w assigns seq[i] := q[i] \Phi 1, this implies
that contrary to (1). Therefore, r does not determine w!q[i]. Thus,
we conclude that w!q[i] is determined by a predecessor of r, i.e., w : 1:i OE r : 1.
For the second part of the proof assume that k 6= 0. Let t be the state prior to the event
2:k. Because r!p k is true and because k ? 0, the following assertion holds at state t.
RR[k; i]:f lag - RR[k;
Because k ? 0, we have, by the definition of p k ,
Because w determines r!y, this implies that w!alt. Thus,
by transitivity, the following assertion holds at state t.
RR[k; i]:f lag - RR[k;
Therefore, from the definition of Cue, Cue(w; k; i) holds at state t. 2
The following lemma relates the sequence numbers read by two consecutive operations of
the same Reader i. It states that these values do not differ by more than one. The intuition
is as follows: in order for Reader i's sequence number to be incremented by 1, it must first
be written by Reader i to RW [i], then be read by the Writer, then be incremented by the
Writer and written to WR[i], and finally be read again by Reader i. Between two reads from
WR[i] by two consecutive Read operations, this complete sequence of events can happen at
most once.
Lemma 2: Let r and s be consecutive operations by Reader i. Then,
Proof: We prove the lemma by first showing that the following assertion is an invariant.
To prove that B is an invariant, we consider the assertions B0; . ; B4 defined below and
show that B0 - is an invariant. In these assertions, we refer to the local variables
q[i] and seq[i] of the Writer and x:seq[i] of Reader i.
To see that B0 - is an invariant, observe the following.
ffl B0 is initially true, and the only statement that can possibly falsify it is the read by
the Writer from RW [i]. But, executing this statement when B0 is true establishes
B1.
ffl The only statement that can possibly falsify B1 is the assignment to seq[i] by the
Writer. But, executing this statement when B1 is true establishes B2.
ffl The only statement that can possibly falsify B2 is the first write by the Writer to
WR[i]. But, executing this statement when B2 is true establishes B3.
ffl The only statement that can possibly falsify B3 is the read by Reader i from WR[i].
But, executing this statement when B3 is true establishes B4.
ffl The only statement that can possibly falsify B4 is the write by Reader i to RW [i].
But, executing this statement when B4 is true establishes B0.
Thus, we conclude that B0- \Delta \Delta \Delta -B4 is an invariant. This also implies that B is an invariant
since
We now use invariant B to show that the lemma holds. Our proof obligation is as follows.
Let t denote the state prior to the event Because r and s are consecutive, the value of
RW [i] at state t equals r!x:seq[i], and the value of WR[i]:seq[i] at state t equals s!x:seq[i].
Since B is an invariant, either
[i] at state t, in which case
1 at state t, in which case
The following lemma relates the value written to RR[i; j] by an operation r of Reader
i to the values written by an "overlapping" or succeeding Write operation w. The proof of
this lemma makes use of Lemma 2.
Lemma 3: Let r be an operation of Reader i, and let w be a Write operation such that
be any state at which w after 1:i holds. If the value
appearing in RR[i; j] (i - j) at state t is written by r, then Cue(w; i; j) is false at t.
Proof: Let t be any state for which w after 1:i holds and i and j be indices such that i - j.
Assume that and that the value appearing in RR[i; j] at state t is written by
r. Our proof obligation is to show that Cue(w; i; j) is false at t.
We first show that r!x:seq[i] 6= w!seq[i]. Let e be the event prior to state t. Because
w after 1:i holds at t, w Therefore,
w!q[i] is determined by either r or some successor s of r. In the former case,
r!x:seq[i]. As w assigns seq[i] := q[i] \Phi 1, this implies that w!seq[i] 6= r!x:seq[i]. In the latter
Because r writes the value appearing in
RR[i; j] at state t and t is the state following event e, r and s are consecutive operations
of Reader i. Hence, by Lemma 2, w!q[i] equals r!x:seq[i] or r!x:seq[i] \Phi 1. Therefore,
w!seq[i] equals r!x:seq[i] \Phi 1 or r!x:seq[i] \Phi 2. As \Phi is modulo-3 addition, this implies that
w!seq[i] 6= r!x:seq[i]. Thus, in both cases, w!seq[i] 6= r!x:seq[i].
Because r writes the value appearing in RR[i; j] at state t,
holds at state t. Consider the two values r!y:seq[i] and w!seq[i]. If they are equal
because w!seq[i] 6= r!x:seq[i], we have r!x:seq[i] 6= r!y:seq[i] and consequently, r!f lag is
false. Therefore, by (2), RR[i; j]:f lag is false at t and hence, Cue(w; i; j) is false at t. If on
the other hand, r!y:seq[i] 6= w!seq[i] then by (2), RR[i; j]:seq 6= w!seq[i] at t and therefore,
is false at t. 2
The following lemma ensures that the new value is not returned from a Write operation
before its uncertainty interval. It states that Reader i does not cue Reader j to return the
new value unless the Writer has begun the second pass of writes to the Readers. The proof
makes use of Lemmas 1 and 3.
Lemma 4: Let w be any Write operation and i - j. Then,
Proof: We prove the lemma by induction on i. We assume the result for all indices less
than i and prove it for i. Consider the state interval over which w after 1:i - w before 4
holds. We need to show that Cue(w; i; j) is false during this interval for all j - i.
Consider a state t in the interval in question and assume that Cue(w; i; j) is false for all
at all states in the interval that occur before t. (Note that t could be the first state
in the interval.) We show that Cue(w; i; j) is also false at t for all j - i. If RR[i; j]:f lag is
false at t, then Cue(w; i; j) is clearly false at t. So, in the remainder of the proof, assume
that RR[i; j]:f lag is true at t.
Since RR[i; j]:f lag is false initially, there exists an operation r (of Reader i) that writes
the value appearing in RR[i; j] at t. Consider the events
is false at t, as required. So,
in the remainder of the proof, assume that w : 1:i OE r : 1.
Let e be the event prior to state t. By the program for Reader
Because r writes the value appearing in RR[i; j] at state t, r : 5:j - e. Because w before 4
holds at t, e OE
Therefore, r!y is determined by w or the Write operation immediately preceding w. In the
latter case, r!y:alt 6= w!alt, and therefore, Cue(w; i; j) is false at t. In the remainder of the
proof, we consider the case in which r!y is determined by w.
By therefore, r!y:done is false. Hence, by the definition of p 0 , r!p 0
is false. We now show that l ) is false as well. Because r writes the value
appearing in RR[i; j] at t, this implies that RR[i; j]:f lag is false at t and hence Cue(w;
is false at t.
Consider any l in the range From the program of the Writer, w
By assumption, w : 1:i OE r : 1. From the program for Reader 3. Thus, by
(3),
Consider the state prior to the event r : 2:l. From the above precedence assertion, w after 1:l
- w before 4 holds at this state. If l = i then Cue(w; l; i) is false at this state; this follows
from our assumption that Cue(w; i; j) is false for all j - i at all states that occur before t
in the interval over which w after 1:i - w before 4 holds. If
is false at this state by the induction hypothesis. Thus, in either case, Cue(w; l; i) is false
at this state. Since w determines r!y, by the contrapositive of Lemma 1, r!p l is false. This
establishes our remaining proof obligation. 2
The following lemma asserts the stability of Cue(w; during the uncertainty interval.
It states that once Cue(w; true during this interval, it remains true until the
interval ends. The proof makes use of Lemma 3.
Lemma 5: Let w be any Write operation and let i - j. Then,
w at 4 - Cue(w;
Proof: The stated safety property is preserved trivially by each event of the Writer and all
Readers different from Reader i. We show that it is also preserved by each event of Reader
i. Let s be any operation of Reader i. Consider the event s : 5:j. This is the only event of s
that may falsify the predicate Cue(w; t be the state prior to this event and let u
be the state following this event. Assume that w at 4 - Cue(w; holds at t. Then, our
proof obligation is to show that Cue(w; i; j) holds at u (w at 4 holds at u trivially). By the
program for Reader i, the following assertion holds at u.
Thus, to prove that Cue(w; i; j) holds at u, it suffices to prove the following.
lag -
Because Cue(w; i; j) is false initially (RR[i; j]:f lag is initially false), the value appearing in
RR[i; j] at state t is written by some operation r (of Reader i) that immediately precedes
s. Consider the events w : 1:i and r : 1. By the contrapositive of Lemma 3, :(w after 1:i)
holds at t or w : 1:i OE r : 1. But, by assumption, w at 4 holds at t. Therefore,
Now, we show that w determines r!y. By the program for Reader
Since r precedes s and w at 4 holds at t (i.e., the state prior to s : 5:j), we have r : 5:j OE
Therefore, r!y is determined by either w or the Write operation immediately preceding w.
In the latter case, r!y:alt 6= w!alt, and therefore, RR[i; j]:alt 6= w!alt at t. Consequently,
is false at t. This is contrary to our assumption. Therefore, w determines r!y.
From the program for the Writer,
Therefore, applying (6),
Therefore, w determines both s!x and s!y. The latter implies that
w!alt. This meets two out of our three proof obligations (5) and we are left with
the proof obligation that s!f lag holds. This is proved next.
Because Cue(w; holds at t, and r writes the value appearing in RR[i; j] at state
t, r!f lag holds. Since w determines r!y, this implies that Cue(w; i; i) holds at the state
following the event r : 5:i. Consequently, since r and s are consecutive operations of Reader
also holds at the state prior to the event s : 2:i. By the definition of Cue, this
implies that the following assertion holds at that state.
lag - RR[i;
By the program for Reader i, RR[i; also holds at that state. Therefore,
lag -
Because w determines both s!x and s!y (shown earlier as a consequence of (7)),
Therefore, using (8) and the definition of p i , s!p i is true. Consequently, s!f lag holds, which
was our final proof obligation. 2
The following lemma considers the case in which an operation of Reader i precedes an
operation of Reader j where i - j. This lemma formalizes the following property: if the y
variables of both Reads are determined by the same Write operation - implying that each
assigns its y variable during or after the uncertainty interval of that Write operation - and
if the first Read returns the new value, then the second Read also returns the new value.
This lemma is based on Lemmas 1, 4, and 5, and is in turn used in the proof of precedence.
Lemma r be any operation of Reader i and s be any operation of Reader j such
that precedes s. Assume that both r!y and s!y are determined by the same
Write operation. Then,
Proof: Assume that Write operation w determines both r!y and s!y and that r!p k holds
for some k - i. Our proof obligation is to show that s!p l holds for some l - j.
We first establish that w determines both s!x and s!y. Because i - j, we have
By the
program for Reader Therefore,
Because w determines s!y, by (9), w determines both s!x and s!y.
Now, consider the events first
dispose of the former case by showing that s!p 0 is true. Because w determines both s!x
and s!y, we have s!y:done is true.
Therefore, by the definition of p 0 , s!p 0 is true. In the remainder of the proof, we assume
that By (9), we have,
By assumption, r!p k holds for some k - i. Thus, by Lemma 1. From the
program for Reader 3. Therefore, by (10),
Next, we show that Cue(w; i; is true at the state prior to the event s : 2:i. Let t be the
state following the event r : 5:j. Because r!p k holds, r!f lag is true. Therefore, the following
assertion holds at state t.
lag - RR[i;
Because w determines r!y, we have w!alt. Thus, the
following assertion holds at state t.
lag - RR[i;
Hence, Cue(w; i; is true at state t. Thus, by the contrapositive of Lemma 4, :(w after 1:i)
- :(w before 4) holds at state t.
By the program for Reader i, we have r precedes s, we have r : 5:j OE
Thus, by (11),
Therefore, w after 1:i holds at state t. Consequently, :(w before 4) holds at t, i.e., w at 4
or w after 4 holds at t. But, by the above precedence assertion w after 4 does not hold at
t. Thus, w at 4 holds at t, i.e., w : 3:1 OE r : 5:j. Therefore,
Observe that w at 4 holds for all states between r : 5:j and s : 3. Thus, by Lemma 5,
holds for all states in that interval. In particular, it holds at the state prior to
Now, by the program for Reader j, RR[i; holds at the state prior to the event
This implies that the following assertion holds.
lag -
On account of (10) and the fact that s!x and s!y are both determined by
w!alt. Therefore,
lag -
Hence, by the definition of p i , s!p i is true, which is our proof obligation. 2
Because the Writer writes to higher numbered Readers first, a lemma is needed that
ensures that new-then-old conflicts do not arise in a history in which an operation of a
higher numbered Reader is followed by an operation of a lower numbered one. The required
property is given later in Lemma 9. Lemmas 7 and 8, given next, take care of subcases
arising in the proof of Lemma 9. Lemma 7 states that if Reader i has cued Reader j of
the new value during the uncertainty interval of Write operation w, then it did so either on
account of reading the final value from the Writer (i.e., w after 4:i holds) or on account of
being cued in turn by some other Reader (i.e., holds). The proof
of this lemma makes use of Lemmas 1, 3, 4 and 5.
Lemma 7: Let w be any Write operation and i - j. Then,
w at 4 - Cue(w;
Proof: Consider any Reader i and the state interval over which w at 4 holds. We need to
show that the property
holds at all states during this interval. Consider a state t in the interval in question and
assume that property (12) holds at all states in the interval that occur before t. (Note that
t could be the first state in the interval.) We show that the property also holds at state t.
Assume that Cue(w; after 4:i) holds at state t for some j - i. Our proof
obligation is to show that Cue(w; k; i) holds at state t for some k ! i.
Since RR[i; j]:f lag is false in the initial state, Cue(w; i; j) is initially false. Therefore,
assume that the value appearing in RR[i; j] at state t is written by operation r (of Reader
i). Consider the events w : 1:i and r : 1. By the contrapositive of Lemma 3, :(w after 1:i)
holds at t or w : 1:i OE r : 1. But, by assumption, w at 4 holds at t. Therefore,
By the program for Reader Because r writes the value appearing in
RR[i; j] at state t, r : 5:j - e, where e is the event prior to state t. Because :(w after 4:i)
holds at t, e OE w : 4:i. Therefore,
Therefore, r!y is determined by either w or the immediate predecessor of w - but,
the immediate predecessor of w does not determine r!y, as on account of
being true at state t. So, w determines r!y.
Because Cue(w; holds at state t, RR[i; j]:f lag also holds at t. Hence, because r
writes the value appearing in RR[i; j] at t, r!f lag holds. By the program for Reader i, this
implies that r!p k is true for some k where k - i. We now show that k ? 0. Observe that
assertion (13) implies that r : 3 OE e OE w : 4:i. Thus, because w determines r!y, r!y:done is
false, which implies that r!p 0 is false. Thus, k ? 0.
Because k - i, we have 1:i. By the program for Reader
5:j. Thus, by (13), we have
Let u denote the state prior to the event r : 2:k. Because r!p k holds and because k ?
0, by Lemma 1, Cue(w; k; i) holds at state u. Thus, by the contrapositive of Lemma 4,
:(w after 1:k) - :(w before 4) holds at u. But, by assertion (14), w after 1:k holds at u.
Consequently, :(w before 4) holds at u, i.e, w at 4 or w after 4 holds at u. But, by (14),
w after 4 does not hold at u. Thus, w at 4 holds at u, which implies that w : 3:1 OE r : 2:k.
Thus, by assertion (14), we have,
Observe that w at 4 holds for all states between r : 2:k and w : 4:i. Since Cue(w; k; i) holds
at state u, by Lemma 5, Cue(w; k; i) holds for all states in this interval. In particular, it
holds at state t (the state following event e). This establishes our proof obligation if k ! i.
In the case that holds at state u. From (15), u lies within the interval
over which w at 4 holds and u occurs before t. Consequently, from our assumption that
property (12) holds at all states prior to t in this interval, w after 4:i holds at state u or
holds at state u, for some k ! i. However, by (15), w after 4:i does not hold at
state u. Therefore, Cue(w; k; i) holds at state u, for some k ! i. Consequently, by applying
Lemma 5 as in the previous paragraph, Cue(w; k; i) also holds at state t, as desired. 2
According to the next lemma, if Reader i has cued Reader j during the uncertainty
interval of Write operation w, then it has also cued other Readers with indices between i
and j. The proof follows essentially from the fact that Reader i writes to other Readers in
the order of increasing indices. This lemma makes use of Lemmas 3, 4, and 5 and is in turn
used in the proof of Lemma 9.
Lemma 8: Let w be any Write operation and i - j. Then,
w at 4 - Cue(w;
Proof: Assume that w at 4 - Cue(w; holds at some state t. Let i - k ! j. We show
that Cue(w; holds at state t.
Because RR[i; j]:f lag is false in the initial state, Cue(w; i; j) is initially false. Therefore,
assume that the value appearing in RR[i; j] at state t is written by operation r (of Reader
i).
Let u be the state following the event r : 5:k. Since Cue(w; holds at t and since r
writes identical values to RR[i; j] and RR[i; k], Cue(w; holds at u.
Now, consider the events w : 1:i and r : 1. By the contrapositive of Lemma 3, :(w after 1:i)
holds at t or w : 1:i OE r : 1. But, by assumption, w at 4 holds at t. Therefore,
By the program for Reader Because r writes the value appearing in
RR[i; j] at state t, r : 5:j - e, where e denotes the event prior to state t. Since w at 4 holds
at t, e OE w : 4:M. Therefore,
Since w after 1:i - Cue(w; holds at state u, by Lemma 4, :w before 4 holds at
u. In other words, w at 4 or w after 4 holds at u. But, by (16), w after 4 does not hold
at state u. Thus, w at 4 holds at u. Consequently, by Lemma 5, Cue(w; holds at all
states in the interval between r : 5:k and w : 4:M and in particular at state t. This establishes
our proof obligation. 2
Lemma 9 relates the value of RR[l; i] to that of RR[k; j] where It states that
if Reader l has cued Reader i during the uncertainty interval of Write operation w, then
all Readers with indices lower than i either have been informed of the new value by the
Writer (i.e., w after 4:j holds) or they in turn have been cued by some other Reader (i.e.,
holds). The proof of this lemma makes use of Lemmas 7 and 8.
Lemma 9: Let w be any Write operation and l - i. Then,
w at 4 - Cue(w; l; i)
Proof: Assume that w at 4 - Cue(w; l; i) holds at some state t. For brevity, let P (j)
be shorthand for we have to show that
w after 4:j - P (j)) holds at state t. The proof is by induction. The inductive step is given
by the following assertion, which, as shown later, holds at state t.
w at 4 - Cue(w;
Given our assumption that w at 4 - Cue(w; l; i) holds at t, this inductive step implies
that one of the disjuncts of the consequent holds at t. If the second disjunct holds, then
the inductive step can be applied again, this time using w at 4 - Cue(w; l 1 as the
antecedent. Because the number of Readers is finite and because the Reader indices (l
appearing in the second disjunct of the consequent are smaller than the indices (l; i), this
inductive step can be applied in this way only a finite number of times. Thus, after some
finite number of applications, we eventually obtain a consequent in which the first disjunct
holds. Since the assertions P (j) are being accumulated for in the second disjunct
of each application of the inductive step, this implies that following assertion holds when
the induction terminates.
Because 4:j, we can assert the following at state t.
Combining the ranges of the two universal quantifications, we get
at state t. This implies that
holds at state t, which is the required proof obligation. The proof of the inductive step is
as follows. (All state predicates refer to state t.)
w at 4 - Cue(w; l; i)
w after 4:l -
assumption, w at 4g
w after 4:l -
w after 4:l -
fdefinition of P (j)g
w after 4:l -
assumption, w at 4 - Cue(w; l; i)g
(w after 4:l -
(w after 4:l -
fdefinition of P (j)g
(w after 4:l -
(w after 4:l -
fpredicate calculus and l - ig
(w after 4:l -
fdefinition of P (i 1 )g
(w after 4:l -
assumption, w at 4g
(w after 4:l -
The following lemma considers two successive Read operations r and s such that r,
though it precedes s, reads from a more recent Write operation than s. Because of the order
in which the Writer writes to the Readers, this situation can arise only if the index of r is
greater than that of s. The lemma ensures that r computes its f lag to be false and that s
computes its f lag to be true. This lemma is based on Lemmas 1 and 4, and is in turn used
in the proof of precedence.
Lemma 10: Let r be any operation of Reader i and s be any operation of Reader j such
that precedes s. Assume that r!y and s!y are determined by Write operations
lag is false and s!f lag is true.
By the program for Reader Because w
determines s!y and w precedes w Therefore,
Hence, r!y:done is false, s!y:done is true, and Thus, by the definition
of p 0 , r!p 0 is false and s!p 0 is true. Because s!p 0 is true, from the program of Reader j,
s!f lag is true. This meets a half of our proof obligation. In the remainder of the proof, we
show that r!p k is false for each k in the range This implies our remaining proof
obligation, namely that r!f lag is false.
Consider the two events 1. In the
former case, by the contrapositive of Lemma 1, r!p k is false for each k as desired. So, assume
that in the remainder of the proof.
Because k - i, we have By the program for Reader
3. Thus, using (17), we have
Note that w 0 after 1:k - w 0 before 4 holds at the state prior to r : 2:k. Hence, from Lemma
4, holds at that state. Therefore, by the contrapositive of Lemma 1, r!p k is
false, which is the required proof obligation. 2
The final lemma in the proof of the construction considers the case in which an operation
of Reader i precedes an operation of Reader j where i ? j. This lemma is the counterpart
of Lemma 6, which considers the case i - j. This lemma is based on Lemmas 1, 4, 5, and
9, and is in turn used in the proof of precedence.
Lemma 11: Let r be any operation of Reader i and s be any operation of Reader j such
that precedes s. Assume that both r!y and s!y are determined by the same
Write operation. Then,
Proof: Assume that Write operation w determines both r!y and s!y and that r!p k holds
for some k - i. Our proof obligation is to show that s!p l for some l - j.
Consider the two events first
dispose of the former case. Because Because r precedes s,
By the program for Reader Therefore,
Thus, since w determines s!y, s!y:done is true and Therefore, by the
definition of p 0 , s!p 0 is true, which establishes our proof obligation.
In the remainder of the proof, assume that r : 3 Because r!y is determined by
this implies that r!y:done is false. By the definition of p 0 , this implies that r!p 0 is false;
1. By the program for Reader
Therefore,
Let t denote the state prior to the event r : 2:k. We now show that w at 4 holds at t.
Because r!p k is true and because k ? 0, by Lemma 1, Cue(w; k; i) holds at state t. Hence,
by the contrapositive of Lemma 4, :(w after 1:k) - :(w before 4) holds at t. Because,
Thus, by the previous precedence assertion, we have the
following.
Therefore, w after 1:k holds at state t. Consequently, :(w before 4) holds at t, i.e, w at 4
or w after 4 holds at t. But, by the above precedence assertion, w after 4 does not hold
at t. Thus, w at 4 holds at t.
Since w at 4 - Cue(w; k; i) holds at state t and j ! i, by Lemma 9, w after 4:j holds
at t or Cue(w; m; j) holds at t for some m - j. In the former case, we have
Because r precedes s, this implies that By repeating the reasoning
following (18), this implies that s!p 0 holds, as required. In the remainder of the proof,
assume that Cue(w; m; j) holds at t.
Because Since w at 4 holds at state t, we
have 2:k. By the program for Reader Therefore,
Consider the two events first
dispose of the former case. Because r precedes s, r Hence, by (19), we have
s!y:done is true. Moreover, since
Therefore, by the definition of p 0 , s!p 0 is true, which
establishes our proof obligation.
In the remainder of the proof, assume that s : 3 Because r precedes s, r : 3 OE
3. Thus, by (19), the following assertion holds.
Therefore,
By assertion (20), w at 4 holds for all states in the interval between r : 2:k and s : 3.
Recall that Cue(w; m; j) holds at state t, i.e., the state prior to the event r : 2:k. Therefore,
by Lemma 5, Cue(w; m; holds for all states in this interval. In particular, it holds at the
state following the event s : 2:m. By the program for Reader j, RR[m;
at that state. Therefore,
lag -
Because w determines s!y, s!y, we
have s!y:alt. Therefore,
lag -
Consequently, by the definition of pm , s!p m is true, which is our proof obligation. 2



--R

The virtue of patience: concurrent programming with and without waiting
The elusive atomic register
Constructing two-writer atomic registers
Constructing multi-reader atomic values from non-atomic values
Parallel Program Design: A Foundation
Concurrent control with readers and writers
Counterexamples to a one writer multireader atomic variable construction of Burns and Peterson
Linearizability: a correctness condition for concurrent objects

Atomic multireader register
"Hoare logic"
parts I and II
How to construct wait-free variables
Axioms for memory access in asynchronous hardware systems
A protocol for wait-free
Concurrent reading while writing
Concurrent reading while writing II: the multi-writer case
On the correctness of atomic multi-writer registers
The elusive atomic register revisited
How to construct an atomic variable
Converting Lamport's regular registers to atomic registers
Concurrent reading while writing revisited
Atomic shared register access by asynchronous hardware
--TR
Axioms for memory access in asynchronous hardware systems
The elusive atomic register revisited
Constructing multi-reader atomic values from non-atomic values
A protocol for wait-free, atomic, multi-reader shared variables
Converting Lamport''s regular register to atomic register
Constructing Two-Writer Atomic Registers
Parallel program design: a foundation
Linearizability: a correctness condition for concurrent objects
Concurrent Reading While Writing
Concurrent control with MYAMPERSANDldquo;readersMYAMPERSANDrdquo; and MYAMPERSANDldquo;writersMYAMPERSANDrdquo;
Atomic Multireader Register
How to Construct an Atomic Variable (Extended Abstract)
How to Share Concurrent Asynchronous Wait-Free Varaibles (Preliminary Version)
The Virtue of Patience: Concurrent Programming with and Without Waiting
The Elusive Atomic Register

--CTR
S. Haldar , K. Vidyasankar, Constructing 1-writer multireader multivalued atomic variables from regular variables, Journal of the ACM (JACM), v.42 n.1, p.186-203, Jan. 1995
Cynthia Dwork , Orli Waarts, Simple and efficient bounded concurrent timestamping and the traceable use abstraction, Journal of the ACM (JACM), v.46 n.5, p.633-666, Sept. 1999
Alessandro Panconesi , Marina Papatriantafilou , Philippas Tsigas , Paul Vitnyi, Randomized naming using wait-free shared variables, Distributed Computing, v.11 n.3, p.113-124, August 1998
James H. Anderson , Yong-Jik Kim, Nonatomic mutual exclusion with local spinning, Proceedings of the twenty-first annual symposium on Principles of distributed computing, July 21-24, 2002, Monterey, California
Rida A. Bazzi , Gil Neiger , Gary L. Peterson, On the use of registers in achieving wait-free consensus, Distributed Computing, v.10 n.3, p.117-127, April 1997
Ming Li , John Tromp , Paul M. B. Vitnyi, How to share concurrent wait-free variables, Journal of the ACM (JACM), v.43 n.4, p.723-746, July 1996
Paul C. Attie , E. Allen Emerson, Synthesis of concurrent programs for an atomic read/write model of computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.187-242, March 2001
John Tromp , Paul Vitnyi, Randomized two-process wait-free test-and-set, Distributed Computing, v.15 n.3, p.127-135, July 2002
Yehuda Afek , David S. Greenberg , Michael Merritt , Gadi Taubenfeld, Computing with faulty shared objects, Journal of the ACM (JACM), v.42 n.6, p.1231-1274, Nov. 1995
James H. Anderson, Lamport on mutual exclusion: 27 years of planting seeds, Proceedings of the twentieth annual ACM symposium on Principles of distributed computing, p.3-12, August 2001, Newport, Rhode Island, United States
wait-free synchronization;atomic register;linearizability