A framework for semantic reasoning about Byzantine quorum systems.
We have defined a class of shared variables called TS-variables that includes those implemented by the various Byzantine quorum system constructions of Malkhi and Reiter, and developed a number of definitions and theorems enabling us to reason about these variables abstractly. Using these tools, we have reduced the problem of Lamport's atomic semantics for such variables to the simpler problem of regular semantics. We discuss the fact that both these problems have remained stubbornly difficult to solve for some types of Byzantine quorum system variables (notably masking quorum system variables) by showing that they are not solvable by traditional approaches in an asynchronous environment. Finally, for such variables we define the notion of pseudoregular and pseudoatomic semantics, and state briefly that a similar reduction holds for these concepts.
Introduction
Byzantine quorum systems [MR98a] are a promising approach to the problem of e-ciently implementing
Byzantine fault-tolerant data services. There are several variations on this approach [Baz97, MRWr97,
MRW97, MR98a], but the basic concept is the same for all of them: data are maintained simultaneously
at multiple sites, and each read or write operation is processed at a subset (called a quorum) of those
sites. Quorums are dened in such a way that the intersection of any two quorums contains enough servers
to allow a query to determine and return accurate and up-to-date information even in the presence of a
limited set of arbitrarily faulty servers. Furthermore, because only a subset of the servers is concerned with
any given operation, such a system can also remain available in spite of limited server crashes or network
partitions. Finally, the fact that the service is designed to tolerate out-of-date servers (e.g., those which
were not part of the most recent write quorum) greatly simplies the task of recovering from failures; as
long as a quorum of servers is up to date, others may be brought back online without any need to recover
their most recent state.
Analyzing the semantics of shared variables implemented by these quorum systems can be quite chal-
lenging. Heretofore, such analysis has been limited to individual protocols; there has been no framework for
reasoning about the semantics of quorum variables as a family. For example, while there exist compelling
arguments to the eect that fully serializable operations have been achieved for some types of quorum
systems (notably the dissemination quorum systems of [MR98b]) and remain an open problem for others
(e.g., masking quorum systems, [MR98a]), these arguments do not tell us why these discrepancies exist, or
the degree to which individual solutions can be generalized.
One of the primary contributions of this paper is to address this need. We present a set of denitions
and theorems that allow us to reason about the class of shared variables implemented by quorum systems,
including the various Byzantine quorum systems; we call such variables TS-variables because of the important
role of timestamps in their protocols. 1 Further, we give an adapted version of Lamport's formal
denitions of the concepts of safe, regular, and atomic semantics [Lam86]. These concepts have traditionally
been used to describe the semantics of Byzantine quorum systems, but their use has necessarily had
to be somewhat informal, as Lamport's formal denitions and theorems were based on the assumption
that variable writes were never concurrent with one another. Our adaptation is not dependent on this
assumption, and so can be applied directly to the variables of interest in a fully calculational proof style.
As far as we know, this is the rst paper to apply calculational proofs to quorum system variables.
We use these formalisms to prove that the atomicity result of [MR98b] generalizes to an important
theorem about TS-variables: the writeback mechanism used in that particular protocol in fact reduces the
problem of atomic variable semantics for any TS-variable to the simpler problem of regular semantics. The
correctness of the atomic protocol of [MR98b] can in fact be viewed as a corollary of this result, as the
cryptographic framework of dissemination quorum systems (sans writeback) enforces regular semantics.
As a follow-up, we show why the problem of atomic semantics (fully serializable operations) has been
straightforwardly solved for some types of quorum system while remaining unsolved for others. Specically,
we show that for a signicant subclass of TS-variables, traditional approaches to protocol design will always
have some danger of failed read queries (aborted, retried or incorrect) in an asynchronous environment.
(In fact, the masking quorum systems of [MR98a], for which atomic semantics have proved stubbornly
elusive, fall into this category.) Finally, we propose and brie
y discuss the somewhat weaker notions of
pseudoregular and pseudoatomic semantics for such systems.
The structure of this paper is as follows. In Section 2, we dene TS-variables and a number of related
concepts and theorems, including our adapted version of Lamport's semantic categories. In Section 3 we use
In fact, our denition of TS-variables is not specic to quorum system variables; it simply captures those properties that
are common to such variables and are relevant to our analysis. Our theorems therefore also hold for any other variable types
that may share these properties.
these formalisms to give a fully calculational proof that any regular read/write protocol that satises the
denition of a TS-variable protocol can be used to implement a corresponding atomic read/write protocol.
In Section 4 we show that for an important class of possible protocols, traditional approaches to protocol
design always result in a danger of unresolvable queries in an asynchronous system; we then dene the
weaker notions of pseudoregular and pseudoatomic semantics, which can be implemented in spite of such
queries. We conclude in Section 5. (An example of a pseudoregular protocol for masking quorum systems
is included in the appendix.)
Preliminaries
2.1 Formalizing masking quorum system variables: TS-variables
In order to reason formally about Byzantine quorum system variables as a class, we need an abstraction
that denes the important features of such variables independently of operational details. To this end, in
this section we introduce the concept of TS-variables. We begin by dening the more general concept of
\timestamped variables" as well as a number of useful functions on such variables:
Denition 1 A timestamped variable is a variable of any type whose value is read and updated in conjunction
with an associated timestamp, where timestamps are drawn from some unbounded totally ordered
set.
Let RW be a set of read and write operations on some timestamped variable with a given read/write
protocol; let R  RW be the set of reads, and let W  RW be the set of writes. Then the following
function denitions hold (R and B represent the set of reals and the set of booleans, respectively):
value: For op 2 RW , if op is a read, then value(op) is the value returned by the read; if op is a write, then
value(op) is the value written.
ts: For op 2 RW , if op is a read, then ts(op) is the timestamp of the value returned by the read; if op is a
write, then ts(op) is the timestamp assigned to the value written.
readsfrom: For r 2 R, w reads the result of write w. For timestamped
variables, we dene this to be equivalent to:
readsfrom
For the purposes of the next two functions, we postulate a real-valued global \clock" (e.g., the age of the
universe in milliseconds) that provides an absolute timescale for system events. As the systems we discuss
are asynchronous, individual processes do not have access to global clock values or to these functions,
which are used only for reasoning purposes.
start: The start time of the operation in global time.
end: The end time of the operation in global time.
The purpose of these functions is to give us a convenient shorthand for reasoning about the possibility
of concurrency between operations without being specic about the actual (nondeterministic, in an
asynchronous environment) order in which servers process requests. Essentially, if
then op2 is not concurrent with op1, whereas if
such concurrency may exist and thus needs to be resolved in any proposed serialization of op1 and op2.
For simplicity, we will therefore treat the latter expression as our denition of concurrency hereafter. 2
In keeping with their hypothetical meaning, we stipulate that the start and end functions meet the
following restriction:
2.1.1 TS-variables
A variable consists of a type, a memory address, and a specication of the operations that may be performed
on it, including at least read and write. 3 We refer to such a specication as a variable protocol. Read and
write activity on a variable is described in terms of a run of its protocol:
Denition 2 A run of a variable v is a set of operations performed on v, all of which meet the specication
of v's protocol. We call a run RW complete if, for all read operations r 2 RW , there exists a write operation
RW such that readsfrom (r; w).
It is useful to have a separate term for the run consisting of all operations performed on a variable during
its lifetime:
Denition 3 The history of a variable is the run consisting of all operations performed on that variable
during its lifetime.
In this chapter we will continue to use the label RW to represent a variable run; subscripts will be used
to distinguish between runs when the context is not otherwise clear. The projection of a run RW onto its
read operations will be denoted R; the corresponding projection onto write operations will be denoted W .
Although some researchers use the terms \run" and \execution" interchangeably, in this work we nd
it useful to follow the example of [Lam86], which gives them distinct technical meanings. Specically, an
execution associates a run with a precedence relation on the operations of that run, i.e.:
Denition 4 An execution of a variable v is a pair hRW; - i, where RW is a run of v and - is a
precedence relation (irre
exive partial order) on the operations in RW .
We now dene two specic types of execution that are of special importance to this work:
Denition 5 An execution hRW; - i is said to be real-time consistent if
Denition 6 An execution hRW; - i is said to be write-ordered if it satises the following:
1.
2. hW; - i is real-time consistent.
2 A more literal denition would be that two operations are concurrent if and only if there exist two servers that process
them in dierent order. However, it will be readily seen that if end(op1) < start(op2), then every server processes op1 before
hence they are not concurrent.
3 We do not concern ourselves with read-only variables in the context of this work.
In other words, (1) in a write-ordered execution, the write operations are totally ordered by - , and (2)
the order is consistent with the partial order of write operations in real time.
Denition 7 For all runs RW of a timestamped variable v, the relation ts - is dened by:
1. 8op 2 RW;8w ts - w  ts(op) < ts(w)
2. 8w 2 W;8r ts - r  ts(w)  ts(r)
3. 8r a ; r b
ts
It is easy to see that ts - is irre
exive, antisymmetric and transitive. It is therefore an irre
exive partial
order. (Note that operations with identical timestamps are not necessarily ordered by ts - .)
We now dene TS-variables as follows:
Denition 8 A TS-variable is a timestamped variable v such that, for all histories RW of v, hRW; ts - i
is write-ordered.
Note that Denitions 7 and 8 imply that TS-variable writes are uniquely identied by timestamp; thus
for any given read, there is at most one write with the same timestamp. We can therefore make the
following observation, which provides a simplied form of the denition of readsfrom() for TS-variables:
Observation 1 For any read operation r and write operation w of a complete TS-variable run,
2.2 Formalizing data semantics for TS-variables
We now dene what it means for a write-ordered execution to be safe, regular or atomic. The denitions
of safe and regular are based on the idea that once a write to a variable has completed, previous values of
that variable should not be read. This concept is expressed in [Lam86] in terms of the set of writes that
a given read \sees": 4
Denition 9 For a write-ordered execution hRW; - i, let w be the ordered list of write operations
from RW as dened by - . Furthermore, for a given read operation r, let i be the index of the last write
that precedes r, i.e., start(r)g. Then we say that r sees W 0  W , where:
We express this relationship in predicate form as
Thus the values that a read sees are those that might be legitimately returned by that read, i.e., the
value of the most recently completed write w i and the values of any concurrent writes.
The above denition is di-cult to use directly. Fortunately, the fact that hRW; - i is write-ordered
implies that all writes seen by r fall within a well-dened range { no such write is earlier than the last
(in terms of the write order) to precede r or later than the last write that is concurrent with r:
4 [Lam86] dened this concept for a single-writer register, whose write operations are thus necessarily serial. We relax this
requirement, dening our version of \sees" in terms of serializable, rather than serial, writes. Thus our denition can be
applied to variables with multiple writers.
Observation 2 For a given read r, let i be dened as in Denition 9, and let
Then: 5
We are now ready to give our denitions of safe, regular, and atomic executions.
2.2.1 Safe executions
In informal terms, an execution is safe if any read that sees only one write returns the value of that write.
Operationally, this means that a read that is concurrent with no writes returns the result of the \most
recent" write according to the serialization dened by the write-ordering. Formally, continuing to use w
to denote the i th write in the order dened by - we say:
Denition
it is write-ordered, and
2.2.2 Regular executions
A write-ordered execution is regular if every read returns some value that it sees, i.e., the result of the
most recently completed write or a concurrent one. Formally:
Denition 11 An execution hRW; - i is regular if:
it is write-ordered, and
Note that a regular execution is necessarily safe.
For TS-variables, this denition has a useful consequence: the timestamp of any given read is at least the
timestamp of the most recently completed write. Formally:
ts - i be regular. Then
A calculational proof of this lemma is given in Figure 1; it consists of showing that any arbitrary write
that precedes a given read has a timestamp less than or equal to that of the read.
5 Note that the reverse is not true. It is possible for a write to fall within the given range without being seen if the \invisible"
occurs after read r, but concurrently with w j .

Figure

1: Proof of Lemma 1
2.2.3 Atomic executions
Finally, we dene an atomic execution as an execution that behaves as though the operations were totally
ordered in a real-time consistent way, i.e., (A) they are totally ordered, (B) they behave as though performed
serially in that order, and (C) the order is consistent with the partial order of the operations in real time:
Denition 12 An execution hRW; - i is atomic if:
- is a total order on RW ,
Note that the second and third bullets of the denition above imply that any atomic execution is also
regular, while the reverse is not necessarily true.
The safeness, regularity or atomicity of a variable protocol is a property of the set of possible histories (see
Denition of a variable implemented with that protocol:
Denition 13 A variable protocol is safe (regular, atomic) with respect to a precedence relation - if,
for all possible histories RW consistent with the protocol, the execution hRW; - i is safe (regular, atomic).
A protocol is safe (regular, atomic) if it is safe (regular, atomic) with respect to some precedence relation.
A variable is safe (regular, atomic) if its protocol is safe (regular, atomic).
Observation 3 Denitions 11 and 12 (specically, the second bullet of each) imply that every read in a
regular or atomic execution reads from some write; thus all possible histories of a regular or atomic variable
are complete runs.
3 Reducing the Atomic Semantics Problem
In the previous section, we developed tools for reasoning about TS-variables, a class of shared variables
that includes those implemented by various types of benign and Byzantine quorum systems. We now
demonstrate the power of these tools by using them to prove that the writeback mechanism of [MR98b]
does not apply only to dissemination quorum systems; it can be used to promote a regular protocol to an
atomic one for any type of TS-variable. Specically, we show how to construct a protocol for a TS-variable
atom given a protocol for a regular TS-variable v reg , and prove that the result is atomic. We accomplish
this by means of the following steps:
1. Add a new operation to the protocol for v reg , dene the operations of v atom in terms of this expanded
regular protocol, and show that the resulting v atom is a TS-variable.
2. Dene a total order ts 0
- on operations of v atom that extends ts - , i.e., op a
ts - op b ) op a
ts 0
3. Use Denition 13 to prove that v atom is atomic with respect to ts 0
- .
3.1 Dening the atomic protocol
Let v reg be a regular TS-variable. We expand the protocol of v reg by dening a third operation in addition
to read and write: writeback. The writeback operation is similar to the write operation of v reg except that
whereas write operations calculate their own timestamps, a writeback takes its timestamp as an argument;
thus writebacks are not necessarily ordered by ts - . We stipulate, however, that all runs RW exp of the
expanded protocol continue to satisfy Lemma 1, as well as the following additional property: 6
Property 1 For all read operations r, write operations w and writeback operations b in RW exp ,
We now dene our proposed atomic variable protocol v atom as follows, where read reg and write reg are
the read and write protocols of v reg , and val, ts are the value and timestamp respectively of the read reg
operation:
In other words, a write operation of v atom consists of a single write operation of v reg , while a read operation
of v atom consists of a read operation of v reg followed by a writeback of the resulting value and timestamp.
The timestamp of each Read atom or Write atom operation is identical to the timestamp of the underlying
read reg or write reg operation. Because each write operation of v atom consists exactly of one write operation
of v reg , it follows that v atom is also a TS-variable. (For clarity, we will hereafter follow the convention that
operations of v atom are represented in boldface, while operations of v reg are represented in italics.)
6 In masking quorum systems, as in dissemination quorum systems, both Lemma 1 and Property 1 are implemented by
having a write/writeback perform a null operation at any server whose current timestamp for the variable is higher than that
of the write/writeback; thus monotonicity of timestamps is enforced at each server.
3.2 A total order over operations on v atom
In preparation for proving v atom atomic, we specify a precedence relation that totally orders all runs
RW atom of v atom . The ts - relation that we have already dened is not su-cient, as it does not order read
operations that share the same timestamp. We therefore propose to dene an extension ts 0
- of ts - using
the following additional function that maps all operations of any run RW to some totally ordered set:
gtf: An arbitrary function with the following three properties:
Uniqueness: 8op a ; op b 2 RW , gtf (op a
An example of such a function is a mapping from op 2 RW to the pair (time(op); id), where id is a unique
real-valued operation identier, and
The purpose of the gtf function is to act as a supplement to timestamps when we dene a serialization
of the operations. Sequentiality ensures that the order imposed by gtf is compatible with the partial
order of the operations in real-time, Uniqueness ensures that the function can act as a \tie-breaker" for
operations with the same timestamp, and Read Promotion ensures that each read operation has a higher
gtf than any write that might aect it. 7
We now dene ts 0
- as follows: for any given run RW atom of v atom , 8op a ; op b 2 RW atom :
op a
ts 0
In other words, ts 0
- is the lexicographic ordering on the pair (ts(op); gtf (op)). It is therefore a total order by
virtue of the Uniqueness property of gtf() and the fact that ts() and gtf() have totally ordered codomains.
As a consequence of this denition, we have the following lemma and corollary, which allow us to use
Denition 12 to prove atomicity:
ts - op b ) op a
ts 0
Corollary 1 All executions hRW atom ; ts 0
- i of v atom are write-ordered.
ts 0
ts - r
The proofs of this lemma and corollaries are straightforward, and are omitted for reasons of space.
3.3 Proving v atom atomic
Our remaining goal is to prove that hRW atom ; ts 0
- i is atomic for all runs RW atom of v atom , thus proving
that v atom is an atomic variable:
Theorem 1 For all possible histories RW atom of v atom , the execution hRW atom ; ts 0
- i is atomic.
As we have already shown that ts 0
totally orders RW atom , our remaining obligations are to prove:
7 In fact, these properties are su-cient to allow us to dene a total order strictly in terms of gtf . However, gtf alone
does not specify the behavior of timestamps, and so does not allow us to reason directly about the behavior of reads via the
readsfrom function. We will therefore will use gtf as indicated above.

Figure

2: Proof that readsfrom(r; w
ts 0
ts 0
hRW; ts 0
- i is real-time consistent.
The proofs appear in Figures 2 and 3. In the latter case, our obligation is to prove that:
ts 0
We prove this separately for each of the four possible cases: two writes, a write followed by a read, a read
followed by a write, and two reads. For simplicity, we will use the convention that r and w (with possible
subscripts) refer to operations of RW atom , while r, w, and b denote the corresponding read, write and
writeback operations of the expanded regular protocol (Figure 3).
Thus we have reduced the problem of atomic semantics for all TS-variables to that of regular semantics.
In the next section we show that, while the latter problem is readily solvable for some types of TS-variables
(e.g., dissemination quorum systems), there is a signicant class of TS-variables (including, unfortunately,
masking quorum systems) for which regular semantics cannot be achieved in an asynchronous environment
using the type of approach that has heretofore been standard. At the end of the section we brie
y discuss
how regular and atomic semantics may be approximated for such variables.
On Regular and Pseudoregular Semantics
With a few exceptions (e.g., [Baz97]), most Byzantine quorum system protocols have been designed for
asynchronous systems with few restrictions. Typically:
Any client may send a write request to a quorum of servers at any time, using its choice of timestamp;
i.e., writes are always enabled.
No ordering or scheduling is imposed on read and write requests.
Read and write requests are processed by servers in the order received.
8 According to the convention we adopted earlier, Ratom is the set of read operations from RWatom .

Figure

3: Proof that hRW; ts 0
- i is real-time consistent
Hereafter, we describe a system with these characteristics as a nonrestricted system.
Although there are several variations on quorum system protocols, most or all of those currently in the
literature share the following characteristics:
1. Each server maintains a single version of the variable image at any given time.
2. A read generates a single query, and returns a non-? value only if some appropriately dened voucher
set of servers responds to its query with identical images; otherwise it returns ? for both value and
timestamp. (In this context, ? is the signal for an aborted operation, and is never written to the
3. The processing of a write request with a su-ciently high timestamp changes the state of the variable
image at the server, and the processing of a read request consists simply of returning the requested
data.
For the remainder of this discussion, we refer to such a protocol as a classic quorum protocol. More
specically, if the smallest voucher set accepted by the protocol is of size m, we refer to it as a classic m-set
quorum protocol.
In this section, we show that, for m > 1, any classic m-set quorum protocol in a nonrestricted system
may return ? in response to a given query. For a read r that returns this value, there exists no write w
such that readsfrom(r; w); thus any history that contains such a read is not regular (cf. Observation 3).
In short:
Theorem 2 For m > 1, no classic m-set protocol is regular in a nonrestricted system.
We prove this theorem by showing that certain possible server responses to a read query in such a
system are unresolvable for m > 1, and results in a read value of ?. As a corollary to the theorem, we
also show that the same is true even if each server maintains a bounded list of the variable images it has
received.
4.1 Denitions
We begin with a number of useful denitions. Let P be a classic m-set quorum protocol, and let r and w
be operations under P such that r is a read operation and w is the most recently completed (as determined
by timestamp) write operation as of the beginning of r. Let Q r and Qw be the quorums on which r and w
respectively are performed. Let F  Q r be the set of servers that return faulty responses during read r.
Denition 14 The informed set for r is the set Q r \ Qw n F .
Note that if there are no writes concurrent with r, so that no servers in Q r \ Qw have been overwritten
since w, then the informed set for r is the voucher set for r. In any case, all servers in the informed set
return the results of writes that r sees (Denition 9), and in the worst case these are the only servers that
do so. We can therefore observe:
Observation 4 Protocol P is regular i all possible sets of responses to a read by informed sets contain
identical responses from at least one voucher set.
4.2 Nonregularity argument: the smallest informed set
Let Q be a quorum system with classic m-set quorum protocol P. Let mininf be the size of the smallest
possible informed set for Q. 9
The smallest informed set represents the worst-case scenario for a successful read. Suppose that for a
given history RW under P, every read operation is concurrent with at most k write operations. Then:
Theorem 3 RW is regular i:
Proof: For an arbitrary read operation r let I be the partitioning of the informed set such
that I 0 contains the servers that return the result of the most recently completed write operation and each
I i contains the servers that return the result of the i th write that is concurrent with r. In a nonrestricted
system, any or all of the sets I i may be nonempty, depending on the order in which concurrent operation
requests are received at individual servers. We prove the \if" and \only if" portions of the theorem
separately.
9 as every quorum system is based on well-dened set of possible failure scenarios, this value is well-dened.
If: If dmininf =(k then for any read r, some I i 2 I r contains a voucher set by the Extended
Pigeonhole Principle, which states that at least one member of a partition contains at least the average
number of elements for the partition.
Only if: Suppose dmininf =(k r be a read operation with an informed set of size mininf,
and suppose that r is concurrent with exactly k writes. Furthermore, let I r be an even partition, i.e., a
partition in which every set contains either the ceiling or the
oor of the average number of elements. I r
does not contain a voucher set, so r returns ?, implying that RW is not regular. Since this history is
possible in a system such as that described above, the protocol is not regular.2
Since by denition a nonrestricted system allows arbitrary values of k, we have:
Lemma 3 A classic m-set protocol P is regular in a nonrestricted system
Theorem 3 follows directly from this result.
Thus, if m > 1 for a classic m-set read protocol, i.e., the protocol requires agreement between multiple
servers in order to determine a correct result, then it is not regular in an unrestricted system. While
this category includes the masking quorum systems of [MR98a], it is worth noting that ordinary quorum
systems and dissemination quorum systems, which are classic m-set protocols for are already
known to be regular for their appropriate failure models (benign, Byzantine-limited-by-authenticated-data
respectively).
4.2.1 Non-regularity of classic protocols with bounded image list
We dene a classic m-set protocol with bounded image list as an enhanced m-set protocol with the following
characteristics:
1. Each server maintains a bounded list of the images it has received for a given variable, i.e., a list of
the last hsize images written to the server.
2. Again, a read returns a non-? value only if it receives identical images from at least b
for a specied b > 0.
Even if each server responds to every query with its entire list of hsize images, it remains possible for a
read query to be unresolvable in a nonrestricted system, i.e.:
Lemma 4 For m > 1, no classic m-set quorum protocol with bounded image list is regular in a nonre-
stricted system.
Proof: In a nonrestricted system, any given read operation may be concurrent with an unbounded
number of writes. Suppose some read operation r is concurrent with hsizes write operations, where hsize
is the size of the bounded image list and s is the size of the informed set for r. For 1  i  s, server S i
may receive the rst hsizei write requests before receiving the request for r. Then the image list of S 1
will contain the images of the rst hsize writes, the image list of S 2 will contain the images of the next
hsize writes (which displace the rst hsize because the list is bounded), and so forth. In response to its
query, r therefore receives hsizes dierent variable images, each from exactly one server. It is therefore
unable to resolve the query.2
4.3 Ignoring aborts: pseudoregular semantics
Certain applications, however, may be able to tolerate occasional aborted reads. For such applications it
is worthwhile to reason about a somewhat weaker version of regular (and atomic) semantics for variables,
which we will refer to as pseudoregular (respectively pseudoatomic) semantics. We dene these concepts in
terms of variable pseudohistories, as follows:
Denition 15 The pseudohistory of a variable is the run consisting of all writes in the variable history
and all reads that do not return ? (i.e., the set of all non-aborted operations).
We now dene our new semantic concepts as follows:
Denition variable protocol is pseudoregular (pseudoatomic) with respect to a precedence relation
- if, for all possible pseudohistories RW consistent with the protocol, the execution hRW; - i is regular
(atomic). A protocol is pseudoregular (pseudoatomic) if it is pseudoregular (pseudoatomic) with respect to
some precedence relation.
4.3.1 Reducing pseudoatomicity to pseudoregularity
Suppose we have a pseudoregular protocol for a TS-variable. (An example of such a protocol for masking
quorum systems appears in the appendix to this paper, and was initially sketched in [AMPRW00].) For
any possible pseudohistory RW , the execution hRW; ts - i satises Denition 11, so RW is a complete run.
Therefore the arguments of Section 3 apply to these pseudohistories as well. The same writeback mechanism
we demonstrated before can thus be used to produce a pseudoatomic protocol from the pseudoregular one.
5 Conclusion
In this paper we have presented a set of denitions and theorems that allow us to reason about the semantics
of shared variables implemented by various types of quorum systems, including the often-problematic
Byzantine quorum systems. This framework allows us to develop theorems about such variables (which
we call TS-variables) as a class, without reference to the details of individual implementations. We have
also used the resulting tools to prove that any regular protocol for a TS-variable can be straightforwardly
enhanced into an atomic protocol.
As a subsidiary result, we showed that there is a signicant subclass of TS-variables (including masking
quorum systems) for which traditional design approaches cannot produce a regular protocol for an
asynchronous environment. For such variables, we introduce the idea of pseudoregular and pseudoatomic
semantics, which are similar to the original concept except in that they allow occasonal aborted operations.

Acknowledgements

We would like to express our sincere thanks to Dahlia Malkhi and Michael Reiter
for numerous thought-provoking discussions, and to Jennifer Welch, HyunYoung Lee, Pete Manolios and
Phoebe Weidmann for their helpful comments on earlier drafts of this paper.



--R

Dynamic Byzantine Quorum Systems.
Synchronous Byzantine quorum systems.

Atomic Multireader Register.
On Interprocess Communications.
Quorum systems.
Byzantine Quorum Systems.
Secure and Scalable Replication in Phalanx.
Optimal Byzantine Quorum Systems.
Probabilistic Quorum Systems
Extensions of the UNITY Methodology
The Elusive Atomic Register.
--TR
Dynamic Byzantine Quorum Systems
Secure and Scalable Replication in Phalanx

--CTR
Ittai Abraham , Gregory Chockler , Idit Keidar , Dahlia Malkhi, Wait-free regular storage from Byzantine components, Information Processing Letters, v.101 n.2, p.60-65, January, 2007
distributed data services;atomic variable semantics;byzantine fault tolerance;quorum systems