Concurrencey without global states: a case study

Uri Abraham Depatments of Mathematics and Computer Science, Ben Gurion University, Be’er Sheva, Israel

December 25, 2002

Abstract

A distributed variant of the Lazy Caching algorithm of Afek, Brown, and Merritt [2] is described and proved to be sequentially consistent. This variant is distributed in the sense that (unlike the original algorithm of [2]) it does not consider a compound action that contains several instructions as an atomic operation. Only elementary operations on queues are atomic. The correctness proof exemplifies a new approach to concurrency in which there are no global states, and part of the proof (the higher-level part) is an abstract reasoning about system executions.

1 Preface

Volume 12 of Distributed Computing (1999) comprises six articles which are all devoted to the Lazy Caching algorithm of Afek, Brown, and Merritt [2], proving that it is sequentially consistent. In addition it contains a short introduction by R. Gerth [4] defining the Lazy Caching algorithm and the notion of sequential consistency. (We suggest to view Gerth’s paper as an introduction to our paper as well, though we intend to repeat the basic definitions.) As noted by M. Merritt in the editorial introduction to that volume, the problem of proving the correctness of the lazy caching algorithm became a “favorite challenge problem”, and now it is probably a canonical problem for verification formalisms.

In [1] a “behavioral” approach to concurrency is developed in which the notion of a global state has lost its importance and replaced by system executions and first-order specifications of behaviors. The aim of this paper is to expose this approach by explaining how it treats a variant of the Lazy Caching algorithm.

There is a common framework which is accepted by all six articles mentioned above, namely that concurrent executions are described by global states and histories. A global state is a function that assigns values to all system variables, both local variables of the participating processes and communication variables, namely registers, queues, and channels that are used for inter-process communication. Each of the participating processes is serial. It executes its actions one after the other, and actions by different processes are arbitrarily interleaved to form a history. Any correctness proof of an algorithm is basically an analysis of all possible resulting histories.

This framework has a well-known drawback: the state explosion problem is the difficulty of analyzing histories when the number of possible global states is unmanageably big. In our correctness proof we avoid this problem simply by not having global states. Queues and registers are not variables to which values are assigned. Instead, system executions and first-order theories that specify registers and queues are employed.

The paper is quite long. Since our aim here is to introduce the model theoretic framework of [1], it is necessary to proceed slowly and to gradually develop the semantics of the algorithm and the tools used it its analysis. The following introduction explains some basic notions. Sequential consistency is defined in terms of structures (in the sense of Tarski). These are of basic importance in our exposition and we spend some time in their definition. The particular structures that are used here are system executions, and they are defined in Section 2.1 (they generalize Lamport’s well known definition, for example in [8]). To each concurrent algorithm we attach a class of structures (called its executions) and a correctness condition which is expressed by a statement in the language of the structures. The correctness proof of the algorithm amounts to proving that all its structures satisfy this correctness condition.

The correctness proof has two stages. The higher-level stage is not directly connected to any algorithm. It is a first-order proof that some “axioms” entail sequential consistency. This is done in Section 3. Then the lower-level stage of the proof shows that these axioms hold in each of the executions (structures) of the algorithm.

Look at the Lazy Caching algorithm in Figure 1 (it will be explained in details later) and observe that is has, in its six rows, six types of events. Each such event is atomic: its execution is not interleaved with other events. In particular, the MW_{i}(d, a) action is an atomic event consisting of a write followed by N +1 enqueue/dequeue instructions (N is the number of user processes). It is an aim of our paper to investigate the possibility of Lazy Caching algorithms in which compound operations are not executed atomically, and where only lowerlevel read/write and enqueue/dequeue events are atomic. Therefore obtaining a greater degree of concurrency.

2 Introduction

To say it in one sentence, our approach consists in replacing histories (sequences of states) by system executions. So we begin by defining these structures. We continue with specifications of queues, and serial memories.

We shall use here two elementary notions: signature and interpretation. A “signature” is a (finite) collection of names of sorts, function symbols, and predicate with prescribed arity for each symbol. (Equality is automatically included in any signature.) An “interpretation” is a structure M with universe A = |M| which gives meaning to each item in the signature. So if T is a sort, then T ⊂ A (we can use T also as a predicate over A). If S is a predicate or function symbol of arity n then S^{M} (also written S_{M}) is a relation, S^{M} ⊆ A^{n}, or a function S^{M} : A^{n} → A.

If M is an interpretation of some signature σ and and σ_{0} is a subsignature of σ, then the “reduct” of M to σ_{0} is the interpretation of σ_{0} obtained from M by restricting M to σ_{0}.

The structures used here are “many-sorted” structures. This means that the universe A of the structure M is a union of finitely many sorts (and each sort has a name). For example, structures with two sorts, Event and Data, will be used. Although sorts can be replaced by unary predicates (in some singlesort universe) there are several advantages to many-sorted structures which make them more convenient for our purposes. For example, in a regular singlesort structure all functions must be defined on all the universe and predicates applicable to all tuples of elements from the universe. But here we can specify functions from some sort to another, or predicates defined on tuples of specific sorts. Another advantage is the possibility of specifying for each sort a set of specific variables (d for Data variables, e for Event variables etc.) with a noticeable gain of clarity in formulas.

2.1 System Executions

System executions were introduced and used by Lamport [7], [8], and a similar notion appears in Pratt [11]. The particular form of definitions given here (emphasizing that system executions are structures in the model theoretic sense) is taken from [1].

An irreflexive and transitive relation R on E is called an interval-ordering iff for all a, b, c, d ∈ E

a R b ∧ ¬(c R b) ∧ c R d ⟹ a R d  (1)

We say then that R satisfies the Russell–Wiener property. It is easy to prove that if a = (a_{1}, a_{2}), b = (b_{1}, b_{2}) etc. are intervals of some linear ordering ≤, and R is defined by (a_{1}, a_{2}) R (b_{1}, b_{2}) iff a_{2} ≤ b_{1}, then (1) holds. Wiener [12] proved that any interval ordering can be represented by intervals of a linear ordering. This is the justification for the choice of interval orderings to model the temporal precedence relation of system executions. If a < b then we say that a precedes b. If neither a < b nor b < a then a and b are said to be concurrent.

Definition 2.1 The common signature of system executions comprises of:

1. A sort called Event,

2. A binary predicate < on Event,

3. A unary predicate “terminating”.

Definition 2.2 (Lamport [8]) A global-time model is an interpretation S of the common signature of system executions of the form

S = (Event^{S}; <_{S} , terminating^{S})

where E = Event is a set (called the set of events), <_{S} is a partial irreflexive ordering relation on E, and terminating^{S} is a unary relation on E such that the following holds, where > |_{S} is defined on E by a > |_{S} b iff ¬(b <_{S} a):

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

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

2. For any a ∈ E, if terminating(a) then {x ∈ E | x > |_{S} a} is finite. (Lamport’s Finiteness condition)

3. If a is a non-terminating event (that is ¬terminating(a)) then there is no event y such that a <_{S} y. There is only a finite number of non-terminating events.

Sometimes we use the expression a < end(b) to mean that terminating(a), terminating(b) and

∀e ∈ E (b < e ⟹ a < e).

Global-time models only give the precedence relations among the events but not any other useful information. Nor do they describe those atemporal objects which are not situated in time and do not fall under the precedence relation (such as the set of possible data values). For this reason the definition of “system execution” given here involves not only events with their temporal ordering, but also atemporal objects, relations, and functions. This shows the need for many-sorted structures containing sorts for different types of objects other than events.

Definition 2.3 A system execution is a many-sorted structure M that interprets a signature Sig that contains the standard signature of system executions, and such that the reduct of M to this standard signature is global-time model.

In other words, a many-sorted structure M is a system execution if it has a sort Event^{M}, a binary relation <_{M} on that sort, and a unary relation terminating^{M}, such that (Event^{M}, <_{M}, terminating^{M}) (namely the reduct of M to the common signature of system executions) is a global-time model.

Usually, a system execution is a two-sorted structure, and its universe is divided into two sorts: Event (partially ordered with <_{S} ) and a sort of atemporal objects (mainly to represent data values). The sort of atemporal objects is often further specified into subsorts.

2.1.1 System executions with higher-level events.

An advantage of system executions is the capability of dealing with both lowerlevel and higher-level events in the same structure. Higher-level events and their orderings were introduced and employed by Lamport (e. g. [8]) and we generalize this concept as follows.

Definition 2.4 Let M be a system execution. We say that M is a system execution with higher-level events iff its signature contains an additional predicate ∈ defined on sort Event such that the properties following hold:

1. Define the set of higher-level events by the formula

Event(e) ∧ ∃x(Event(x) wedge x ∈ e).

That is, an event e in M is a higher-level event if it has some member. An event devoid of any member is a “lower-level” event. although it is conceivable that higher-level events can be grouped into even higher-level events, we have her just two layers. If e is an event and x ∈ e, then x is always a lower-level event.

2. Extensionality holds for higher-level events. If X ≠ Y are two higher-level events, then there exists some x such that x ∈ X and x ∉ Y or x ∈ Y and x ∉ X. (Clearly extensionality does not hold for lower-level events.)

3. A higher-level event e in M is terminating iff the set of its elements (that is those x’s such that x ∈ e holds in M) is finite and every element of e is terminating. Thus the terminating predicate of M restricted to the lower-level events determine the terminating predicate on all higher-level events.

4. The precedence ordering < on Event is also determined by its restriction to the lower-level events, in accordance with the following formulas. For every higher-level events X and Y

X < Y iff ∀x ∈ X ∀y ∈ Y (x < y)  (2)

For every lower-level event e we also require

\begin{matrix}e < Y iff ∀y ∈ Y (e < y) \\ and \\ X < e iff ∀x ∈ X (x < e) \end{matrix}  (3)

2.2 Specifications of queues and serial memory accesses

In this subsection we use system executions to give an abstract definition of queues.

We first define a signature L_{queue} which extends the standard signature of system executions. The following items define the L_{queue} signature.

Sorts: There are two sorts. Event and Data (Data contains the atemporal objects).

Predicates: In addition to the common predicates < and terminating defined on Event, L_{queue} contains the following unary predicates: Producer, Consumer, enqueue, dequeue, and peek, defined on sort Event.

Functions: There are two functions,

Val : Event → Data

and γ : Event → Event.

The intended meaning is that there are two (sequential) processes: Producer that loads the queue and Consumer that unloads it. If e is any event then either Consumer(e) or Producer(e). For any event e exactly one of enqueue(e), dequeue(e), and peek(e) can hold. All enqueue events are in Producer, peek and dequeue events in Consumer. Every enqueue event is terminating (we assume for simplicity queues with unbounded capacity). If enqueue(e) then Val(e) is the Data value enqueued by e. A dequeue or peek event may be non-terminating, in which case it has no data value. For a terminating dequeue/peek event e, Val(e) ∈ Data is the data value of e.

The fact that Val(e) is defined only on terminating events explains why we tend to accept partially defined functions in our structures. It is reasonable to assume that all our structures contain a special constant ⊥, and then Val(e) =⊥ is our way to say that Val is undefined on e, retaining the advantage of having functions completely defined (on their sorts).

The function γ gives for every terminating dequeue or peek event x the enqueue event γ(x) that deposited the value unloaded or peeked by x. A formal and non-ambiguous specification of this is given next as a list of properties written in (the first-order language of) L_{queue}.

An interpretation of L_{queue} is a structure S with universe Event^{S} ∪ Data^{S}, a disjoint union of the interpretations of the two sorts, such that every symbol X in L_{queue} (a function or relation symbol) has an appropriate interpretation X^{S} (sometimes written X_{S}). For example, <_{S} is a binary relation of Event^{S}, terminating^{S} ⊆ Event^{S}, Val^{S} : Event → Data^{S} etc. An interpretation S of L_{queue} is a system-execution iff (Event^{S}; <_{S} , terminating^{S}) is a global-time model.

Definition 2.5 Given any system execution S that interprets the L_{queue} signature, and given any event e in S, we say that Consumer is “cautious” at e in S (or simply that “the queue is non-empty” at e) iff there exists an enqueue event u such that u <_{S} e and u is not in {γ(d) | d <_{S} e, d is a dequeue}. We say that Consumer is cautious if it is cautious at every dequeue and peek event.

That is, Consumer is cautious in a system execution if no dequeue or peek event begins unless it is preceded by some enqueue that is not yet dequeued.

In practice, this means that Consumer can call a procedure isEmpty which returns a boolean value. Consumer will not execute a dequeue or peek event unless a previous call to isEmpty returned true. In this specification we do not introduce events of type isEmpty, but define a property, “cautious Consumer”, which indicates that such a function has been used. Under this assumption of cautious usage, all consumer events are terminating and are in the domain of γ.

2.2.1 Queue specification

The specification of queues is given here by four sentences written in L_{queue}. It seems to me that these specifications are “self-evident”: the basic idea is that the function γ assigns to the nth dequeue event the corresponding nth enqueue event (yet there is no need to mention numbers in this specification).

1. Each of the (disjoint) processes Producer and Consumer is serial, that is linearly ordered by <. (Producer and Consumer are predicates, but here we refer to them as sets. So “Producer is serial” means that the restriction of the precedence relation < to the collection of all events e such that Producer(e) is a linear ordering of this set.) enqueue events are in Producer. But peek and dequeue events are in Consumer.

2. γ is defined on terminating dequeue and terminating peek events. When γ(e) is defined, enqueue(γ(e)), Val(e) = Val(γ(e)), and γ(e) < end(e) hold.

3. For every terminating dequeue or peek event x, γ(x) is the <-first enqueue event y that is not of the form γ(d) where d < x is a dequeue event. In words, γ(d) is the first enqueue event that is not yet dequeued, namely that is not dequeued by previous dequeue events.

4. All enqueue events are terminating. (This reflects our assumption that queues have unbounded capacity.) If e is any peek or dequeue event and Consumer is cautious at e, then e is terminating. So if Consumer is cautious then all events are terminating.

We make some remarks on this specification.

1. Though each process is serial, events from different processes can overlap. For example, any two dequeue events are < comparable, but a dequeue and an enqueue can be concurrent (<-comparable).

2. It follows from item 3 that the restriction of γ to dequeue is order preserving and one-to-one. That is if e_{1} < e_{2} are terminating dequeue events, then γ(e_{1}) < γ(e_{2}). (This implies that γ is one-to-one on the dequeue events since Consumer is serial.)

It also follows that the range of γ is an initial segment of enqueue events. That is if a < γ(e) and enqueue(a), then a = γ(e′) for some dequeue event e′ (such that e′ < e).

3. If Consumer is cautious then actually γ(e) < e for every dequeue and peek event e. (Because in this case, there exists an enqueue event u < e not of the form γ(d) for a dequeue event d < e. By item (3), γ(e) is the first such u and hence γ(e) < e.)

4. These specifications imply that every dequeue obtains a corresponding value that was previously enqueued. Thus they correspond to the notion of a queue that is initially empty.

5. We say in item 2 that γ is defined on terminating events. This means (if we want γ to be defined on all of Event) that for a non-terminating event e γ(e) =⊥.

The following is easy to prove.

Lemma 2.6 Assuming the queue specifications, suppose that p < d, p is a peek and d a dequeue events. If d is the first dequeue after p, then γ(p) = γ(d).

2.2.2 Statements about queues.

We define a formula “the queue is empty at(e)” by

terminating(e)∧ ∀y(y < e ∧ enqueue(y) ⟹ ∃x(dequeue(x) ∧ γ(x) = y ∧ x < end(e)). (4)

Thus, “the queue is empty at(e)” says that e is a terminating event and every enqueue events preceding e has been dequeued by some event that ends before e does.

2.3 Sequential consistency

We define sequential consistency with the signature L_{serial} that extends the common signature of system executions and contains the following items:

1. There are three sorts: Event, Data, and Address.

2. Unary predicates P_{1}, …, P_{N} are defined on Event. (If P_{i}(e) then we say that e is an event in process P_{i}.) There are two additional unary predicates defined on Event: Read and Write.

3. The binary predicate < (temporal ordering) on Event, and the unary predicate terminating are included (although we shall assume that all events are terminating, and thus this relation is not strictly necessary for sequential consistency).

4. The functions Val : Event → Data, and address : Event → Address are in L_{serial}.

Sequential consistency is a second-order property in the sense that its definition involves an existential quantification over all possible serial orderings of events.

Definition 2.7 Let S be a system execution that interprets the signature L_{serial} defined above (or possibly a larger signature). We say that S is sequentially consistent iff

1. Every Read/Write event e is a terminating event and is in some unique P_{i} (i.e. P_{i}(e) holds but ¬P_{j}(e) for j ≠ i). Every P_{i} is sequential, that is linearly ordered by <.

2. There exists a serial ordering <^{∗} of the set of (Read and Write) events in S such that

(a) For every 1 ≤ i ≤ N, <^{∗} extends the restriction of < to P_{i}.

(b) If Read(r) then there exists some w such that Write(w), address(w) = address(r), Val(w) = Val(r), w <^{∗} r, and there is no event e such that w <^{∗} e <^{∗} r and address(e) = address(r). In plain words, the value of every read of address d is the value of the <^{∗} last write on address d that <^{∗} preceded r.

The difference between our definition here of sequential consistency and that of Gerth [4] (both follow the original definition of Lamport [6]) is that Gerth uses histories while we use system executions. But intuitively the two definitions say the same, namely that there exists a serial ordering of the read/write events which does not change the given ordering < restricted to the Read/Write events in each process P_{i}, and such that the value of every read is the value of the last write on its address that preceded the read.

As remarked, sequential consistency is a second-order property, but in proving sequential consistency for an algorithm we will actually find a (first-order) definable relation <^{∗} that satisfies the required conditions. That is, we will find a formula ϕ(x, y) and define x <^{∗} y iff ϕ(x, y) holds.

3 Properties entailing Sequential Consistency

In this section we define a signature L_{SC} which extends the signature L_{serial} of section 2.3 by which sequential consistency was explicated. Then we write down a series of properties, called SC Axioms, which entails sequential consistency of the Read/Write events. The correctness proof of the distributed Lazy Caching algorithm, given later in this paper, will prove that executions of the algorithm satisfy the SC Axioms.

We start by defining the L_{SC} signature.

sorts: There are four sorts: Event, Data, Index, and Address. predicates: For some natural number N ≥ 1, P_{1}, …, P_{N}, P_{N+1} are unary

predicates over sort Event. We write P_{MM} instead of P_{N+1} (that is MM = N + 1).

Additional unary predicates over Event are Write, Read, CacheUpdate, MemoryWrite, and, the common predicate, terminating.

There are the following binary predicates on sort Event: <_{i} for i = 1, …, N, ≺, and the binary predicate from the common signature of system executions: <. (So the standard system execution signature is included in L_{SC}.)

functions: The following functions are in L_{SC}.

Val : Event → Data,

address : Event → Address,

index : Event → Index = {1, …, N, N + 1}, μ : Event → MemoryWrite,

constants: 1, …, N + 1 constituting Index.

A few words on the intended meaning of these symbols. Processes P_{1}, …, P_{N} are the users of the system, and P_{N+1} = P_{MM} is the main memory process. The function index(x) tells the process in which x is: P_{i}(x) iff i = index(x). For 1 ≤ i ≤ N, P_{i} executes Read/Write, and CacheUpdate operations. And P_{MM} executes MemoryWrite operations. A Read r in P_{i} is executed from the cache of P_{i}, and then Val(r) in Data is the value obtained at address(r) ∈ Address. CacheUpdate operations are needed either for updating the cache or because the cache location has been evacuated. Instead of an initial value, we assume that every Read in P_{i} is preceded by a CacheUpdate in P_{i} on the same address. Write events also have Val and address attribute. Every MemoryWrite event e is responsible for a specific Write event w, that is, e executes the write on main memory requested by w. We express this relationship by e = μ(w). Although the function μ is formally defined on all Event, we are only interested in its restriction to the Read/ Write/ CacheUpdate events. If Read(r), then μ(r) is the MemoryWrite event that determines the value of r. Each <_{i} is a linear ordering of P_{i} for 1 ≤ i ≤ N. The linear ordering ≺ of P_{MM} has a special symbol because of its importance: it determines the linear ordering required for sequential consistency. The meaning of these symbols will be much clearer after a strudy of the protocol, but there is an advantage of approaching the L_{SC} signature and the following axioms and consequences beforehand: it will be clear and evident that the results are proved abstractly from the axioms without relying on any prior knowledge and intuition.

3.1 SC Axioms

The following list of properties (called SC Axioms) specifies a collection of system executions: those which interpret the L_{SC} signature and satisfy the SC axioms. The axioms are written in (mathematical) English, but it should be obvious that they can easily be formulated as first order L_{SC} statements. In particular, we often treat unary predicates as though they were subsets, and we speak, for example, about an event e being in P_{i} instead of the more formal P_{i}(e). The axioms are listed in two groups, A1—A6, and L1—L4.

A1 For indices i ≠ j in {1, …, N + 1}, the events in P_{i} are disjoint to those in P_{j}. Every event x is in P_{i} for i = index(x). If MemoryWrite(x) then index(x) = N + 1. If x is in Read, Write, or CacheUpdate, then 1 ≤ index(x) ≤ N. No event can fall under two predicates from: Read, Write, CacheUpdate, MemoryWrite. All these events are terminating.

A2 For i = 1, …, N, <_{i} is the restriction of < to P_{i}. P_{i} is linearly ordered by <_{i}.

The relation, ≺ is a linear ordering of MemoryWrite. (We write M_{1} ⪯ M_{2} for M_{1} ≺ M_{2} ∨ M_{1} = M_{2}.)

A3 The function μ is defined on the Read/Write events and on the CacheUpdate events. The restriction of μ to the Write events establishes a one-to-one correspondence from the Write events and onto the Memory Write events. (Different Read or CacheUpdate events may correspond to the same Memory Write event.)

A4 For every Read/Write or CacheUpdate event E, Val(E) = Val(μ(E)) and

address(E) = address(μ(E)).

A5 Let W and V be Write events by P_{i} (possibly to different addresses). If V <_{i} W then μ(V) ≺ μ(W).

A6 Let R be a Read event and W a Write event in P_{i}. If R <_{i} W then μ(R) ≺ μ(W) (R and W can access different addresses).

L1 If C_{0} <_{i} C_{1} are two CacheUpdate events by P_{i} of the same address, then μ(C_{0}) ⪯ μ(C_{1}).

L2 Let M_{0} be a MemoryWrite event and C a CacheUpdate event in P_{i} such that M_{0} ≺ μ(C). Then there exists a CacheUpdate event C_{0} in P_{i} such that C_{0} <_{i} C and M_{0} = μ(C_{0}).

L3 Let R be a Read event in P_{i}, and W <_{i} R be any Write event in P_{i} that precedes R. Then there exists a CacheUpdate event C in P_{i} such that W <_{i} C <_{i} R and μ(C) = μ(W).

L4 For every Read event R in P_{i} with a = address(R) there exists a Cache-Update event C in P_{i} such that C <_{i} R and address(C) = a. If C is the rightmost CacheUpdate event in P_{i} such that C <_{i} R and address(C) = a, then μ(R) = μ(C).

Lemma 3.1 If U <_{i} R, U a Read, Write, or CacheUpdate in P_{i}, and R a Read event in P_{i}, if address(U) = address(R), then μ(U) ⪯ μ(R).

Proof. Assume first that U is a CacheUpdate event. There exists by L4 a CacheUpdate event C in P_{i} such that C <_{i} R, address(C) = address(R). We take C to be the rightmost such CacheUpdate event, so that μ(R) = μ(C). Hence U ≤_{i} C, and L1 gives μ(U) ⪯ μ(C). Hence μ(U) ⪯ μ(R). The two remaining cases are easily reduced to the first case.

• If U is a Read event, then μ(U) = μ(C) for some CacheUpdate event C with address(C) = address(U) and such that C <_{i} U (by L4). Apply the first case of the lemma to C <_{i} R and obtain μ(C) ⪯ μ(R), which yields μ(U) ⪯ μ(R).

• If U is a Write event, apply L3 to U <_{i} R and get a CacheUpdate event C such that C <_{i} R and μ(C) = μ(U). It follows from A4 that address(C) = address(U). Then the first case of the lemma yields μ(C) ⪯ μ(R) and hence μ(U) ⪯ μ(R).

Q.E.D.

Lemma 3.2 The following is a consequence of the SC axioms. If R is a Read by P_{i} of address a, M a Memory Write on a such that

μ(R) ≺ M,  (5)

then, for every P_{i} event U (Read, Write, or CacheUpdate) such that U <_{i} R, μ(U) ≺ M holds.

Proof. Suppose that U is a Read or Write and R is a Read such that U <_{i} R and address(U) ≠ address(R). The lemma does not exclude the possibility that μ(R) ≺ μ(U), but it doesn’t allow a Memory Write event M with the same address of R and such that μ(R) ≺ M ⪯ μ(U).

Assume first that U and R have the same address a. Then μ(U) ⪯ μ(R) by Lemma 3.1. Hence we can suppose that address(U) ≠ a.

Set M_{1} = μ(U). We want to prove that M_{1} ≺ M. Assume for the sake of a contradiction that this is not so and hence that

M ≺ M_{1}.

(Equality is impossible because the addresses are different.) Since U <_{i} R, there is some CacheUpdate event C_{1} in P_{i} such that C_{1} <_{i} R and μ(C_{1}) = M_{1}. If U is a Read, this follows from L4, and if U is a Write, then this follows from L3. (If U is a CacheUpdate, then this is trivial.)

As M ≺ M_{1}, there exists by L2 some CacheUpdate C_{0} in P_{i} such that C_{0} <_{i} C_{1} and μ(C_{0}) = M.

Now C_{0} <_{i} C_{1} <_{i} R implies that C_{0} <_{i} R and since R and M = μ(C_{0}) have the same address a, Lemma 3.1 implies μ(C_{0}) ⪯ μ(R). That is, M ⪯ μ(R), which contradicts (5). Q.E.D.

Our aim is to prove that the SC axioms entail sequential consistency. Therefore we shall define a linear ordering <^{∗} on the Read/Write events, prove that it extends each <_{i}, and prove that it satisfies the seriality requirement of Definition 2.7. The idea is to use the Memory Write events to guide the definition of <^{∗}. Although the Memory Write events themselves are not part of the required ordering (of the Read/Write events), it is useful intuitively to think of them as left end-points of intervals which determine the ordering <^{∗}.

The idea in defining <^{∗} is to put every Write event W in the place of μ(W), and every Read event R of address a somewhere between μ(R) and the next MemoryWrite event M on address a (if there exists such an M). The problem in this case could be that for some P_{i} event U with U <_{i} R, M ⪯ μ(U). Fortunately, Lemma 3.2 exclude this possibility.

Theorem 3.3 If S is any system execution that interprets the L_{SC} signature and satisfies the SC Axioms, then S is sequentially consistent. (See Definition 2.7.)

Proof. We shall use the shorthand external(x) for Read(x) ∨ Write(x). We first define for each external event U, in P_{i}, a MemoryWrite event denoted χ(U) by the formula

χ(U) = max in ≺ of {μ(e) | external(e) ∧ e ≤_{i} U}.  (6)

In words: apply μ to e = U and to all external events e in P_{i} that precede U and choose the maximal Memory Write event μ(e) in the linear ordering ≺. Since the set considered is finite, it has a maximal value in the linear ordering ≺. (Recall that S is a system execution and hence the set of <-predecessors of U is finite, and it includes the set of <_{i}-predecessors of U.)

The ordering <^{∗} can now be defined. For every external events A and B define A <^{∗} B iff χ(A) ≺ χ(B), or else χ(A) = χ(B) and one of the following three alternatives hold:

1. A is a Write event, but B is a Read.

2. A and B are both Read events in the same process, P_{i}, and A <_{i} B.

3. A is a Read event in P_{i}, B is a Read event in P_{j} and i < j.

We shall prove that <^{∗} is a linear ordering as required by Definition 2.7. Since the orderings <_{i} and ≺ are all irreflexive, and as the processes are pairwise disjoint, it is clear that <^{∗} is also irreflexive, that is, A <^{∗} A never holds. Similarly, if A <^{∗} B holds, then B <^{∗} A does not. We next need a lemma.

Lemma 3.4 For every Write event W, χ(W) = μ(W). Moreover, if e <_{i} W (e a Read or Write event) then χ(e) ≺ χ(W).

Proof. Suppose that W is a Write event in P_{i}. We prove below that if e <_{i} W is an external event, then μ(e) ≺ μ(W), namely μ(W) is the largest value and hence χ(W) = μ(W) follows (6). This also proves the additional claim, namely that χ(e) ≺ χ(W).

Well, if e is a Read event, this follows from property A6 in the list of axioms, and if e is a Write event then this follows from A5. Q.E.D.

Now we can prove that for every two (different) external events A and B either A <^{∗} B or B <^{∗} A. If χ(A) ≺ χ(B) or χ(B) ≺ χ(A), this is clear. Otherwise, χ(A) = χ(B), since ≺ is a linear ordering of MemoryWrite. In this case, it cannot be that both A and B are Write events, because this would implies that μ(A) ≠ μ(B) (by A3) and hence that χ(A) ≠ χ(B) by our lemma. So at most one of A and B is a Write event. In case one of A and B is a Write event, that write <^{∗}-precedes the other event. In case both A and B are Read events, there are two possibilities. Either they are both in one process, say P_{i}, and then they are <_{i} comparable and subsequently <^{∗} comparable. Or else they belong to different processes and then their indices decide on their <^{∗} ordering.

Transitivity of <^{∗} can easily be proved by checking all possibilities of A <^{∗} B <^{∗} C.

It is also clear that <^{∗} extends every <_{i}. Indeed, if A <_{i} B, then

{e | e ≤_{i} A} ⊂ {e | e ≤_{i} B},

and hence the maximum for χ(B) is taken over a larger set than that for χ(A). Thus χ(A) ⪯ χ(B). If χ(A) ≺ χ(B), then A <^{∗} B follows. So we assume that χ(A) = χ(B). Consider now the following possibilities.

1. B is a Write event. This is impossible since in that case χ(A) ≺ χ(B), by our lemma.

2. A is a Write event. In this case A <^{∗} B by the definition of <^{∗}.

3. A and B are both Read events. Then A <_{i} B implies that A <^{∗} B again by the definition of <^{∗}.

The main point is to prove that <^{∗} and μ describe a serial memory (item 2(b) in Definition 2.7). By A3, every MemoryWrite event M is μ(W) for some unique Write W. So for every Read event R we define ω(R) as that unique Write event W such that μ(W) = μ(R). We prove the following two required properties for every Read event R of memory address a.

1. ω(R) <^{∗} R is a Write event on address a, and

Val(R) = Val(ω(R)).

Proof. Say W = ω(R). That is μ(W) = μ(R) = M (M is a MemoryWrite event). Item A4 implies that W and M, and similarly R and M have the same address a and the same Data value. Our lemma implies that χ(W) = μ(W) = M. Since M = μ(R) is one of the values in the definition of χ(R), M ⪯ χ(R) follows. If M ≺ χ(R), then W <^{∗} R by definition, but otherwise, χ(W) = χ(R) and then again W <^{∗} R since W is a Write event and R a Read event.

Event type  Allowed if  Action

R_{i}(d, a) Out_{i}.isEmpty, In_{i} is

starless, and C_{i}[a] = d.

W_{i}(d, a)  true  Out_{i}.Enq((d, a))

MW_{i}(d, a) Out_{i}.peek() = (d, a)

Mem[a] := d;
Out_{i}.Deq();
∀k ≠ i
In_{k}.Enq((d, a));
In_{i}.Enq((d, a, ∗)).

CU_{i}(d, a) In_{i}.peek() is either (d, a) or

(d, a, ∗)

{In_{i}.Deq(); \atop C_{i}[a] := d.}

MR_{i}(d, a) Mem[a] = d  In_{i}.Enq((d, a))
CI_{i}(a)  true  C_{i}[a] :=⊥

Initially: ∀a Mem[a] = d_{0}, ∀a C_{i}[a] =⊥, all queues are empty. Legend: MW–Memory Write, MR–Memory Read, CU–Cache Update, CI–Cache Invalidate. Variable d is in Data, and a in Address. ⊥ is the “undefined” value (not in Data). Fairness: No action other than CI_{i} can be always enabled but never taken.

Figure 1: Transition system M_{distr} of the Lazy Caching algorithm.

2. There is no Write event V on address a such that ω(R) <^{∗} V <^{∗} R.

Proof. Assume on the contrary that such a V exists, and W = ω(R). Then W <^{∗} V implies that χ(W) ≺ χ(V) and hence (by the lemma which equates μ with χ in case of Write events) that μ(W) ≺ μ(V). And as μ(W) = μ(R), by the definition of W, μ(R) ≺ μ(V). Since V <^{∗} R, χ(V) ⪯ χ(R) follows (or else χ(R) ≺ χ(V) and then R <^{∗} V). So

μ(R) ≺ μ(V) = χ(V) ⪯ χ(R).

Thus μ(R) ≺ χ(R). Hence (by definition of χ) for some event e in P_{i} (the process of R) such that e <_{i} R, χ(R) = μ(e). But then μ(R) ≺ μ(V) ⪯ μ(e) contradicts Lemma 3.2! (Where M = μ(V).) Q.E.D.

4 The Lazy Caching algorithm

The Lazy Caching algorithm of Afek, Brown, and Merritt [2] is described in Gerth [4] by a transition diagram M_{distr} which is reproduced in Figure 1 (with minor changes).

There is a main memory Mem, and, for every address a ∈ Address, Mem[a] is a variable of type Data. For every 1 ≤ i ≤ N, process P_{i} possesses a local cache C_{i}. Each cache C_{i} is a local, partial, and not always punctual copy of main memory Mem. Each C_{i} has the same space of addresses as Mem, namely Address, but it is possible that C_{i}[a] =⊥, which indicates that the value at address a is not presently in cache C_{i} and has to be brought from main memory. Here ⊥ is a special “undefined” value, supposed not to be in Data. A history in which there are no Cache Invalidate events and in which C_{i}[a] is a Data value for all a ∈ Address is legitimate, even though not very realistic. We expect that Cache Invalidate events ensure that the set of cache locations that carry Data values (i.e. not ⊥) is bounded by the capacity of the cache. This expectation and the replacement schemes that can implement it are not relevant to the question of sequential consistency, and for the sake of clarity are disregarded.

Each process P_{i} is associated with two FIFO queues Out_{i} and In_{i}. These queues contain finite sequences of pairs (d, a) with d ∈ Data and a ∈ Address, and queue In_{i} can also contain triples of the form (d, a, ∗) where ∗ is a special symbol.

4.1 Global states and histories

A global state of a system is a description of an instant. It is obtained by describing the values of all variables, including the communication variables (the In and Out queues in our example). The set of variables V for M_{distr} is defined by

V = {Mem[a] | a ∈ Address} ∪ {C_{i}[a] | a ∈ Address & 1 ≤ i ≤ N}∪

{In_{i} | 1 ≤ i ≤ N} ∪ {Out_{i} | 1 ≤ i ≤ N}. (7)

Every variable v ∈ V has a range of possible values, denoted type(v). For every a ∈ Address, type(Mem[a]) = Data, and type(C_{i}[a]) = Data ∪ {⊥} for every 1 ≤ i ≤ N. To express the type of the different queues we introduce the notation Seq(X) which denotes the set of all finite sequences of elements from the set X. For every 1 ≤ i ≤ N

type(In_{i}) = Seq(Data × Address ∪ Data × Address × {∗}),

type(Out_{i}) = Seq(Data × Address).

A “global state” is a function S defined on V such that S(v) ∈ type(v) for every v ∈ V. Fixing an initial data value d_{0} ∈ Data, the initial state S_{init} is the function S such that for all a ∈ Address S(Mem[a]) = d_{0}, S(C_{i}[a]) = d_{0}, and S(In_{i}) = S(Out_{i}) = ∅ for all 1 ≤ i ≤ N.

4.1.1 Steps

A pair of states (S_{0}, S_{1}) is called an M_{distr} step iff it expresses an action that is allowed by the transition diagram. To define this more formally, we need some notation. If q is any sequence of length ℓ (namely a function defined on {0, …, ℓ − 1}, where ℓ is a natural number and q = ∅ iff ℓ = 0) then q.Enq(x) is the sequence r obtained from q by enqueueing x, that is the length of r is ℓ + 1 and r(i) = q(i) for 0 ≤ i < ℓ, and r(ℓ) = x. Let s = (S_{0}, S_{1}) be a pair of states over V.

1. s is an R_{i}(d, a) step iff

(a) S_{0}(Out_{i}) = ∅,

(b) q = S_{0}(In_{i}) is starless, which means that for every i ∈ dom(q) q(i) ∈ Data × Address, and

(c) S_{0}(C_{i}[a]) = d,

(d) S_{1} = S_{0}

2. s is a W_{i}(d, a) step iff S_{1}(Out_{i}) is the concatenation of S_{0}(Out_{i}) with the pair (d, a), and for every variable v ∈ V \ {Out_{i}}, S_{1}(v) = S_{0}(v),

3. s is an MW_{i}(d, a) step iff the length of q = S_{0}(Out_{i}) is ℓ > 0, q(ℓ − 1) = (d, a), and the value of S_{1} is as follows:

(a) S_{1}(Mem[a]) = d,

(b) for every k ≠ i, 1 ≤ k ≤ N, S_{1}(In_{k}) is the concatenation of S_{0}(In_{k}) with the pair (d, a), and S_{1}(In_{i}) is the concatenation of S_{0}(In_{k}) with the triple (d, a, ∗).

(c) for all variables v ∈ V \ {Mem[a], Out_{i}, In_{1}, …, In_{N}}, V_{1}(v) = V_{0}(v).

4. CU_{i}(d, a), MR_{i}(d, a), and CI_{i}(a) steps are defined in a similar fashion.

A “history” of M_{distr} is a sequence ⟨S_{i} | i ∈ ω⟩, where ω is the set of natural numbers, such that

1. each S_{i} is a state, and S_{0} is the initial state defined above,

2. for every i the pair (S_{i}, S_{i+1}) is a step.

A history is thus a description of a run (or execution) of a protocol. The steps by the different processes are interleaved arbitrarily in a history, and the manifold of all histories is the description of the system of concurrently executing processes.

4.2 A critique

We are going to explain now a shortcoming (from our point of view) of the M_{distr} algorithm, and why we want to change it and deal with the variant of Figure 2 instead. As gathered from the corresponding row in M_{distr}, an MW_{i}(d, a) transition is a pair of states (S_{1}, S_{2}) such that queue Out_{i} is not empty in S_{1}, and, if (d, a) is its head value, then the following actions are taken to produce S_{2}. S_{2}(Mem[a]) = d (but all other values of Mem remain unchanged of course), the head value is dequeued out of Out_{i} and the value obtained (d, a) is enqueued to all In_{k} queues for k a process index different from i. Finally, the triple (d, a, ∗) is enqueued into In_{i}. The fact that these operations produce the subsequent state S_{2} indicates that they are executed “atomically” in our model.

This MW_{i}(d, a) transition is called a Memory Write event type, of value d at address a.

Since an MW_{i}(d, a) operation execution is represented in M_{distr} by a single (atomic) transition, it follows that the ordering of the inner actions of MW_{i}(d, a) is totally irrelevant for M_{distr}, and if the algorithm is sequentially consistent under some inner ordering then it is sequentially consistent under any inner ordering of its MW actions. Yet, if we view this operation as a non-atomic, complex event which can be interleaved with other events, then the inner ordering is of crucial importance, as we are going to discover now .

Consider the Lazy Caching algorithm (Figure 1), and suppose that the Memory Write action MW_{i}(d, a) is not executed atomically, as it is supposed to be, but instruction by instruction, interleaved with other actions executed by other processes. Now consider the following scenario. The queues are empty and the memory and cache addresses are with the initial value d_{0}. A W_{i}(d_{1}, a) event enqueues (d_{1}, a) on Out_{i} (where d_{1} ≠ d_{0}). Then a Memory Write operation, M, begins to execute. It writes Mem[a] := d_{1} and dequeues (d_{1}, a) from Out_{i}. At this moment M halts for a while, and P_{i} begins a Read of address a operation. It finds that Out_{i} is empty (since it was already dequeued) and it also finds the In_{i} queue to be empty, since M has not yet enqueued its ∗ triple. Therefore the Read event accesses C_{i}[a] and reads the old value d_{0} that was initially there.

Thus the Read operation follows a Write by its own process, and yet gets the old value. This clearly shows that the algorithm, under this distributed implementation, is wrong.

Suppose an engineer who wants to implement the Lazy Caching algorithm in the form presented by Gerth [4]. Following the M_{distr} transition system (Figure 1) he will have in fact to build a centralized and completely synchronized system. He will probably use semaphores (or other means) to coordinate the processes and to ensure for example that every Memory Write event is executed atomically—not interleaved with other operations. If he will not do this then, as we have shown, some of the algorithm’s executions may turn out to be incorrect. Fortunately, there is a better solution which our engineer can adopt: to change the ordering of the inner actions of MW_{i}(d, a) and to replace the original ordering by

1. Mem[a] := d;
2, In_{i}.Enq((d, a, ∗));
3. Out_{i}.Deq();
4. ∀k ≠ i
In_{k}.Enq((d, a)).

Notice how the dequeue of Out_{i} is executed only after the enqueue of the stared triple to In_{i}. The resulting algorithm is our variant, which we call the distributed Lazy Caching algorithm. As we explained, it is different from the original algorithm of [2] on two counts: the ordering of the inner MW operations, and the interpretation of the MW operation and the CU operation as non-atomic events.

The problem with histories, as defined above, is that they are not structures in the sense of Tarski (a universe, consisting of sorts, with predicates and functions). The advantage of structures in modeling is that they are capaalgorithm: Lazy Readers

concurrently do

P_{1}, …, L_{N}, P_{MM}

Figure 2: General form of the DLC algorithm.

ble of assigning truth values to first-order formulas, and thus enable a formal definition of intuitive statements concerning the behavior of systems. Regular histories (sequences of transitions) also support sentences and truth valuation, but for temporal logic (see for example [9]). It seems to me that the greater flexibility afforded by first-order sentences justifies the additional effort needed in defining histories as structures. (This point of view is not self evident of course, and it is a main purpose of our paper to support it.)

5 A distributed Lazy Caching algorithm

We think of the system as being composed of a central “memory system” process which takes care of main memory (we call this process P_{MM} ), and N “user” processes which are the different P_{i} for 1 ≤ i ≤ N. The Distributed version of the Lazy Caching algorithm (called DLC) algorithm is not described by a single transition diagram, but by N + 1 protocols. The protocol of process P_{i} is in Figure 3, and the protocol of P_{MM} is in Figure 4. The general form of the algorithm is in Figure 2. We see that N +1 processes are activated concurrently, each with its own protocol which we describe informally next.

5.0.1 Description of the protocol.

The protocol for P_{i} (Figure 3) is a repeat forever loop. The first instruction in its body, in line 1, is decide(r, d, a). It may be non-terminating (when P_{i} has nothing to do), but when it terminates it determines the value of variable r to be one of the constants {R, W, CU, CI} (which refer to 3, 4, 5, and 7) and it determines d and a as values in Data and Address respectively. Line 2 checks the value of r, and then the appropriate sub-procedure is activated. After each execution of a sub-procedure, control returns to line 1 for another execution of the decide operation.

1. If r is R, then line 3 is executed, P_{i} reads its cache C_{i}[a] and returns the Data value found there (so parameter d is not used). We assume that when the decide operation sets r = R it checks beforehand that queue Out_{i} is empty, In_{i} is starless, and C_{i}[a] ∈ Data. We do not describe the mechanism by which these conditions are ensured, the inner structure of decide is not revealed, only its properties will be formally stated (in 6.3.1). After executing the Read(a) procedure, process P_{i} returns to line 1 again.

2. If r is W then procedure Write(d, a) is executed, that is the enqueue operation at line 4. Enqueue operations are assumed to always terminate. procedure P_{i}

repeat forever

1. decide(r, d, a)

2. if r = R then Read(a); else if r = W thenWrite(d, a) else if r = CU then CacheUpdate else if r = CI then CacheInvalidate(a). sub-procedure Read(a)

3. return C_{i}[a].

sub-procedure Write(d, a)

4. Out_{i}.Enq((d, a)); sub-procedure CacheUpdate

5. x := In_{i}.Deq();

6. C_{i}[π_{1}(x)] := π_{0}(x). This means that if x = (d′, a′) or x = (d′, a′, ∗) then C_{i}[a′] := d′.

procedure CacheInvalidate(a)

7. C_{i}[a] :=⊥.

Figure 3: The DLC Protocol of P_{i}.

procedure P_{MM}

repeat forever

1. decide(r, i, a);

2. if r = MR then MemoryRead(i, a); else if r = MW then MemoryWrite(i, a); sub-procedure MemoryRead(i, a)

3. In_{i}.Enq((Mem[a], a)).

sub-procedure MemoryWrite(i)

4. (d, a) := Out_{i}.peek();

5. Mem[a] := d;

6. In_{i}.Enq((d, a, ∗));

7. Out_{i}.Deq();

8. forall k ≠ i such that 1 ≤ k ≤ N do In_{k}.Enq((d, a)).

Figure 4: The DLC Protocol of P_{MM} .

3. If r = CU, then a CacheUpdate operation is executed. We assume that if decide sets r to be CU then it ensures that queue In_{i} is non-empty, and hence the dequeue action in line 5 is terminating. The value x obtained in this action is either a pair or a triple. We use here the notation that for any sequence x, π_{k}(x) = x(k). That is, π_{0}(x) = x(0) is the first member of x, π_{1}(x) the second etc. So if x has the form (d′, a′) or (d′, a′, ∗) then π_{1}(x) = a′ and π_{0}(x) = d′. (In this case parameters d and a are irrelevant.)

4. If r = CI, then line 7 is executed in the CacheInvalidate(a) procedure. This sets C_{i}[a] to be the undefined value ⊥.

The protocol of P_{MM} is also a repeat forever loop. If it terminates, the decide(r, i, a) operation at line 1 of P_{MM} determines r ∈ {MR, MW} where MR is (line) 3, and MW is 4. Variables 1 ≤ i ≤ N and a ∈ Address are also determined by decide(r, i, a).

1. It r is MR then procedure MemoryRead(i, a) is executed. It consists of enqueueing into queue In_{i} the pair (Mem[a], a) (in Data × Address).

2. If r is MW, operation MemoryWrite is executed. It consists of 5 instructions. We assume that when decide(r, i, a) sets r = MW, it ensures that the peek() action at line 4 returns a value which can be assigned to (d, a) (i. e. Out_{i} is non-empty). The instruction at line 8 is a forall loop that consists of N −1 enqueue instructions. These can be executed in any order (and in fact, concurrently).

To prove the correctness of the DLC algorithm we will define a family of structures (called history structures) that represent all executions of the protocol and prove that the SC Axioms of section 3.1 hold in these structures, thereby proving the sequential consistency of the algorithm.

6 History structures of the DLC algorithm

In this section we describe a family of system executions (of a special form called history structure) that represent both lower-level and higher-level views of executions of the DLC algorithm. The description involves several concepts that are introduced gradually in accordance with the following plan.

6.0.3 Unrestricted and restricted semantics. A preliminary discussion of these notions.

6.1 Set-theoretic system executions facilitate standard definitions, such as functions and numbers, that are set-theoretical.

6.2 Unrestricted system executions. These are our history structures The states are local, and queues are not represented.

6.3 Restricted system executions impose the correct behaviour on the queues.

6.3.1 Properties required from the decide operations. Using the function γ with which the semantics of queues is described the “Allowed if” conditions of the DLC algorithm can be phrased.

6.4 A correctness proof of the DLC algorithm can finally be given.

6.0.2 Unrestricted and restricted semantics.

The realization that the semantics of concurrency has two distinct aspects: unrestricted (or internal) and restricted (or external) is an important feature of [1], and the following description is taken from that book (Chapter 3).

There are two aspects to semantics, which we call unrestricted and restricted, that should be discussed before getting on to the technical issues. Usually these aspects are intertwined, but here they are separated and hence understanding the difference is a key issue.

By unrestricted semantics we mean analyzing the forms of programs and relating these forms to meaning, without considering the external world and the communication devices. For example, it is part of unrestricted semantics to define that the execution of a sequence of two instructions p_{1}; p_{2} is done by first executing p_{1} and then (if it terminates) executing p_{2} in such a way that its starting state is the state in which p_{1} has terminated. The notion of state is of prime importance here, but only local states influence the internal semantics. The term “unrestricted semantics” is used because the communication devices are not restricted to operate properly: a dequeue for example may obtain any value (within its range) even if that value has never been enqueued.

By restricted (or external) semantics we mean the specification of communication devices and the relationship of the programs with the external environment. The semantics of registers, queues, or channels, for example, do not depend on the programs that use them, and ought to be described separately from the programs’ semantics. In describing the semantics of communication devices and how it affects the programs, system executions are of prime importance. The term “restricted semantics” is used to convey the idea that the communication devices operate properly.

There seems to be a consensus among computer scientists to describe concurrent systems by means of states and transitions (steps). According to this model of concurrency a concurrent execution of sequential procedures P_{1}…. , P_{n} is obtained as an arbitrary interleaving of atomic steps of the processes. Each step “taken” by some P_{i} changes the global state in accordance with well defined rules, and the manifold of all possible sequences of states thus obtained is the semantics of the concurrent procedures. It seems to me that this interleaving view is inadequate for very complex environments in which the programs are embedded. In antithesis to this state/transition approach we use no global states here; only local states to describe the unrestricted semantics, and then system executions to describe the external semantics (the environment and its interrelation with the program).

6.1 Set-theoretic system executions

Some notions are so standard and prevalent that it makes no sense to redefine them whenever they are needed. These are usually basic set theoretical notion, such as sequences, pairs, union of two sets etc. For example, a sequence of length n (a natural number) is a function defined on {0, …, n − 1}. In many applications only finite sets are needed, and then the universe of hereditarily finite sets suffices. Following J. Barwise [3], W. Hodges [5], and Y. Moschovakis [10] we shall see that it is convenient to develop set theory with urelements (atoms). ^{1} “Urelements” are things in our universe that have no members and yet are not the empty set. We use them here to represent unspecified data points. The hereditarily finite sets are those that can be formed by applying finitely many times the operation of forming finite subsets, starting with the collection of all urelements. In details this construction is explained in the following paragraph, but the reader may want to consult [10] in which set theory with urelements (called “atoms”) is developed.

Let A be a collection of urelements. Define by induction on n ∈ ω the sets HF_{n}(A). For n = 0, HF_{0}(A) = A. Then HF_{n+1}(A) is the union of HF_{n}(A) with the collection of all finite subsets of HF_{n}(A). Finally,

HF(A) = ⋃{HF_{n}(A) | n ∈ ω}.

1“We have followed Zermelo in allowing atoms (without demanding them), primarily because this makes the theory more naturally applicable to general mathematics and science”, p. 30 in [10].

That is, X ∈ HF(A) iff X ∈ HF_{n}(A) for some n ∈ ω. The requirement on A is that if u ∈ A then there is no x ∈ HF(A) such that x ∈ u. Namely, urelements have no members in HF(A). We view HF(A) not only as a set, but also as a two-sorted structure: (A, HF(A)\A; ∈) with sort A of urelements, sort HF(A) \ A, called Set, and a single predicate the membership relation ∈. (The reason Set does not include A is that urelements are not sets. But they appear as members of sets.)

Set Theory develops the notions of pair, function, ordinal, etc. and it is very convenient to employ this arsenal of definitions (we need only finite ordinals, namely the natural numbers, finite functions etc). The collection HF = HF(∅) (a subcollection of HF(A)) contains each natural number. That is ω ⊂ HF.

In applications, we use set-theoretical structures in the following form, designed to represent protocol executions. We define a signature Sig_{0} which has a fixed interpretation A with universe A, and we extend Sig_{0} by adding the following items;

1. A sort Set.

2. A binary predicate ∈ (the membership relation)

3. Unary predicates I_{1}, …, I_{K} and functions H_{1}, …, H_{K} (I_{j} is the domain of H_{j}).

4. Additional function symbols and predicates are possible.

A standard interpretation of Sig is an interpretation M of Sig that extends A such that:

1. Signature Sig_{0} is interpreted in M as A.

2. Set is interpreted as HF(A)\A. ∈ is interpreted as the membership relation on HF(A).

3. Each I_{j} is interpreted as ω×{j}. That is, I_{j} is a copy of ω. dom(H_{j}) = I_{j}.

A standard interpretation of Sig is an unrestricted history structure iff each H_{j} is interpreted as a function defined on I_{j} such that, for every n ∈ I_{j}, H_{j}(n) is a state of P_{j} and the sequence ⟨H_{j}(n) | n ∈ I_{j}⟩ defines an unrestricted execution of the program of P_{j}. We shall give more details below.

6.2 Unrestricted history structures of the DLC algorithm

We assume that two fixed sets Address and Data are given. We assume that both sets are finite. We view them as urelements (that is undefined objects). We will take these two sets as fundamental sorts in the structure that we define here.

The sort V of variables is defined now as the union of local variables of all processes. The set of variables of P_{i} is denoted V_{i}:

V_{i} = {PC_{i}, r_{i}, d_{i}, a_{i}, x_{i}} ∪ {C_{i}[a] | a ∈ Address}.

The set of variables of P_{MM} is denoted V_{MM} :

V_{MM} = {PC_{MM} , r_{MM} , i_{MM} , d_{MM} , a_{MM} , X_{MM} } ∪ {Mem[a] | a ∈ Address}.

The indices for variables with the same names but at different processes indicates that these local variables are distinct. So the variables of distinct processes are pairwise disjoint.

Variables PC_{i} and PC_{MM} are the “program counters” of P_{i} and P_{MM} . Variable X does not appear in the text of procedure P_{MM} , and we will use it to determine the execution of the forall loop at line 8 of that procedure. The exact roles of these variables will be defined below.

The set of variables V is the union of the sets of variables defined above:

V = V_{1} ∪ V_{2} ∪ ⋯ ∪ V_{N} ∪ V_{MM} .

The set of urelements A is defined to be the (disjoint) union of the three sorts:

A = Address ∪ Data ∪ V

.

We view A as the universe of a very simple structure A with three sorts (namely Address, Data, and V), with constants for each of the variables (PC_{i} etc.) and with predicates V_{i} and V_{MM} . The signature of A is denoted Sig_{0}.

Definition 6.1 The signature, Sig, of history structures of the DLC algorithm is defined as follows:

1. Sig_{0} is a subsignature of Sig. So Address, Data, and V are sorts of Sign, and there is an additional sort: Set. Additional items of Sig are the following.

2. A binary predicate ∈, unary predicates I_{1}, …, I_{N}, I_{N+1} (we may write I_{MM} instead of I_{N+1}), and unary function symbols H_{1}, …, H_{N+1} (again H_{MM} can be written instead of H_{N+1}).

Definition 6.2 A “standard interpretation of Sig” is a structure M that interprets our signature Sig such that the following holds:

1. Sig_{0} is interpreted in M as A.

2. HF(A) is formed, the ∈ relation of Sig is interpreted as ∈ of HF(A), and Set = HF(A) \ A.

3. Each I_{j} is interpreted as a copy of ω. Specifically I_{j} = ω × {j}. Each H_{j} is a function with dom(H_{j}) = I_{j}.

Thus there is some freedom in interpreting the functions H_{j}, and we will define unrestricted history structures of the DLC algorithm as standard interpretations of Sig in which these functions represent (unrestricted) executions of the protocol. To make a formal definition we must first define states and steps.

6.2.1 Definition of type(v) for v ∈ V.

For every variable v ∈ V we define its range of possible values type(v). This definition is carried out in the language of Sig. For 1 ≤ i ≤ N we make the following definitions.

1. PC_{i} is the “program counter” of P_{i}. type(P_{i}) = {1, …, 7}. (The value k of PC_{i} indicates that P_{i} is ready to execute line k.)

2. For variable r_{i} we define type(r) = {3, 4, 5, 7}. Constant R denotes 3, constant W denotes 4, constant CU denotes 5, and constant CI denotes 7.

3. type(d_{i}) = Data.

4. For variable a_{i} we define type(a_{i}) = Address.

5. type(x_{i}) = (Data × Address) ∪ (Data × Address × {∗}). (Here ∗ is some special value, for example the number 1.)

6. For every a ∈ Address, type(C_{i}[a]) = Data ∪ {⊥}. (Here ⊥ is some object no in Data.

The types of the variables of P_{MM} are similarly defined:

1. type(PC_{MM} ) = {1, …, 8}.

2. type(r_{MM} ) = {3, 4}. (We have two constants, MR = 3 and MW = 4.)

3. type(i_{MM} ) = {1, …, N}.

4. type(d_{MM} ) = Data, and type(a_{MM} ) = Address.

5. type(X) = P({1, …, N}). That is, X ⊆ {1, …, N}. The role of X will be clarified when we discuss the steps of P_{MM} .

6.2.2 Regular and unreachable states

We shall define now the (local) states of the DLC algorithm. Each P_{i} has its set of states for 1 ≤ i ≤ N + 1. We have two sorts of states: regular and unreachable.

A regular state of P_{i} is any function S from V_{i} and such that S(v) ∈ type(v) for every v ∈ V_{i}. Since functions can be defined in the ∈-language, this definition can be carried in Sig and as the three basic sorts (Data, Address, and V) are finite, the set of all regular states is finite and is thus represented in HF(A).

An initial state of P_{i} is a regular state S such that S(PC_{i}) = 1. That is, a state in which P_{i} is ready to execute the first instruction.

An unreachable state of P_{i} is a function U defined just on PC_{i} with values in type(PC_{i}). The role of these states will be clarified later on; they will be used to characterize non-terminating steps. A regular state S represents the situation when the instruction on S(PC_{i}) is about to be executed, with the values of all variables of V_{i} as they are assigned by S. An unreachable state is not a state in that sense, no computation can proceed from such a state. An unreachable state represents the situation of process P_{i} when the operation that it is executing is non-terminating (and will never terminate) and the node it would arrive to (if it were terminating) is S(PC_{i}).

Observe (again) that these states are local, and the queues do not appear in them. Global states are appropriate for an interleaving semantics, which is not what we discuss here.

A step is a pair of states (S_{1}, S_{2}) in one of the processes that represent an execution of a line of the protocol of that processes. A regular (or terminating) step is one in which both S_{1} and S_{2} are regular states. A non-terminating step is one in which S_{1} is a regular state but S_{2} is unreachable. An oblivion step is such that S_{1} = S_{2} are both unreachable. We shall define the steps of the different processes, and define also a function line on the steps saying which line in the protocol of P_{i} is being executed by that step. In addition, we shall define three partial functions on the steps: DataVal, address, and Val.

6.2.3 Steps of P_{i}.

Let s = (S_{1}, S_{2}) be a pair of P_{i} states for some 1 ≤ i ≤ N. S_{1} is a regular state, but S_{2} may be unreachable. In the following, each formal definition of a step is preceded by an informal introduction. We refer to the protocol of Figure 3.

1. An execution of line 1 decides the value of variable r and hence determines which procedure is invoked: Read, Write, CacheUpdate, or CacheInvalidate. This step also determines the values of data d and address a which are used by some of the procedures. The values of cache locations do not change of course in executing line 1. We allow a non-terminating decide operation. In such a case P_{i} will have only a finite number of operation executions.

We define line(s) = 1 iff S_{1}(PC_{i}) = 1, S_{2}(PC_{i}) = 2, and one of the following two possibilities hold.

(a) S_{2} is also a regular state, and for every variable, v ∉ {PC_{i}, r_{i}, d_{i}, a_{i}}, S_{1}(v) = S_{2}(v). (In this case we think of S_{2}(r_{i}), S_{2}(d_{i}), and S_{2}(a_{i}) as the values “decided by s” for these three variables.)

(b) S_{2} is an unreachable state. (In this case s is a non-terminating decide step.)

If line(s) = 1 and terminating(s) then we define DataVal(s) = S_{2}(d_{i}) and address(s) = S_{2}(a_{i}).

2. An execution of line 2 just transfers control variable PC_{i} to the line number determined by r. This must be a terminating event.

We define line(s) = 2 iff S_{1}(PC_{i}) = 2, S_{2}(PC_{2}) = S_{1}(r). For all variables v other than PC_{i}, S_{2}(v) = S_{1}(v).

3. An execution of line 3 just reads the value of C_{i}[a] and then returns for another execution of line 1. Formally, this step just changes the value of PC_{i}, so that the “reading” of C_{i}[a] is not manifest. However, we define DataVal(s) as the value of variable C_{i}[a]. Since read/write operations are assumed to be terminating, an execution of line 3 is always terminating.

We define line(s) = 3 iff S_{1}(PC_{i}) = 3, S_{2} is a regular state, S_{2}(PC_{i}) = 1, and for any variable v other than PC_{i} S_{2}(v) = S_{1}(v) holds.

If line(s) = 3 then we define DataVal(s) = S_{1}(C_{i}[S_{1}(a_{i})]), and address(s) = S_{1}(a_{i}). (Since S_{1} and S_{2} agree on these variables, it is possible to replace S_{1} by S_{2} in these definitions. However, conceptually, it seems that S_{1} is more meaningful here.)

4. An execution of line 4 is an enqueue of the pair (d, a) on the Out_{i} queue. Yet Out_{i} is not a variable in V_{i} and hence, as a local step, this execution just changes the value of PC_{i}. Enqueue operations are always terminating.

We define line(s) = 4 iff S_{1}(PC_{i}) = 4, S_{2} is a regular state, S_{2}(PC_{i}) = 1 and for any variable v other than PC_{i}, V_{2}(v) = V_{1}(v).

If line(s) = 4, we define DataVal(s) = S_{1}(d_{i}), and address(s) = S_{1}(a_{i}). We also define Val(s) = ⟨DataVal(s), address(s)⟩. (This is the value “enqueued” on Out_{i}.)

5. An execution of line 5 is a dequeue operation which may be non-terminating (in case the queue is empty). We have to prove that in executions of the protocol these operations always terminate, but we cannot assume this.

We define line(s) = 5 iff S_{1}(PC_{i}) = 5, S_{2}(PC_{i}) = 6, and one of the following two possibilities hold.

(a) S_{2} is a regular state, and for every variable v, other than PC_{i} and x_{i}, S_{2}(v) = S_{1}(v). So there is no restriction on the value S_{2}(x_{i}) (dequeued from In_{i}) and any value can be obtained. This is what we mean by unrestricted semantics—that dequeues can obtain any values, even values that were never deposited.

(b) S_{2} is an unreachable state.

If line(s) = 5 and terminating(s), we define Val(s) = S_{2}(x_{i}), DataVal(s) = π_{0}(Val(s)), and address(s) = π_{1}(Val(s)). (Recall that π_{k}(v) = v(k).)

6. An execution of line 6 is an assignment C_{i}[a′] := d′ where x is either (d′, a′) or (d′, a′, ∗). Any assignment is a terminating operation.

We define line(s) = 6 iff S_{1}(PC_{i}) = 6, S_{2} is a terminating state, S_{2}(PC_{i}) = 1, and S_{2}(C_{i}[π_{1}(S_{1}(x_{i}))]) = π_{0}(S_{1}(x_{i})).

Suppose that S_{1}(x_{i}) = (d′, a′) (or (d′, a′, ∗)), then π_{1}(S_{1}(x_{i})) = a′ and π_{0}(S_{1}(x_{i})) = d′, so that the condition above is S_{2}(C_{i}[a′]) = d′.

If line(s) = 6, we define DataVal(s) = π_{0}(S_{1}(x_{i})), and address(s) = π_{1}(S_{1}(x_{i})). It follows that S_{2}(C_{i}[address(s)]) = DataVal(s).

7. An execution of line 7 just determines the value of C_{i}[a] to be “undefined”. It is always terminating.

We define line(s) = 7 iff S_{1}(PC_{i}) = 7, S_{2} is a terminating state, S_{2}(PC_{i}) = 1, and S_{2}(C_{i}[S_{1}(a_{i})]) =⊥. For any variable v other than PC_{i} or C_{i}[S_{1}(a_{i})], S_{2}(v) = S_{1}(v).

If line(s) = 7, we define DataVal(s) =⊥ (which is not in Data) and address(s) = S_{1}(a_{i}).

We also define “oblivion steps” as pairs of the form (S, S) where S is an unreachable state of P_{i}.

6.2.4 Steps of P_{MM}

Let s = (S_{1}, S_{2}) be a pair of P_{MM} states. S_{1} is a regular state, but S_{2} may be unreachable. We define as follows the steps of procedure P_{MM} as well as the function line on them and the partial functions DataVal and address. An additional partial function Qindex(s) give the index k of queue Out_{k} or In_{k} approached by s. The protocol of P_{MM} is in Figure 4.

1. Operation decide(i) is not necessarily terminating. We will require however that main memory is attentive to the processes so that each Write request is finally taken care of.

We define line(s) = 1 iff S_{1}(PC_{MM} ) = 1, S_{2}(PC_{MM} ) = 2, and one of the following two cases holds.

(a) S_{2} is a terminating state, and for every variable v ∈ V_{MM} , not in {PC_{MM} , r_{MM} , i_{MM} , a_{MM} }, S_{2}(v) = S_{1}(v).

(b) S_{2} is an unreachable state.

2. An execution of line 2 just switch PC_{MM} to the appropriate line. This is a terminating operation.

We define line(s) = 2 iff S_{1}(PC_{MM} ) = 2, S_{2} is a regular state, S_{2}(PC_{MM} ) = S_{1}(r), and no variable except PC_{MM} is changed.

3. An execution of line 3 just changes PC_{MM} from 3 to 1. It is always terminating.

We define line(s) = 3 iff S_{1}(PC_{MM} ) = 3, S_{2} is a regular state, S_{2}(PC_{MM} ) = 1, and the two states agree on all other variables. In case line(s) = 3 we define DataVal(s) = S_{1}(Mem[S_{1}(a_{MM} )]), address(s) = S_{1}(a_{MM} ), and

Val(s)⟨DataVal(s), address(s)⟩.  (8)

In this case we also define Qindex(s) = S_{1}(i_{MM} ).

4. An execution of line 4 is a peek operation which may be non-terminating (when the queue is empty). Again, since Out_{i} is not a variable in V_{MM} , the steps that represent peek operations can return any possible values.

We define line(s) = 4 iff S_{1}(PC_{MM} ) = 4, S_{2}(PC_{MM} ) = 5 and one of the following two cases holds.

(a) S_{2} is a regular state and in this case S_{2}(v) = S_{1}(v) for every variable v ∈ V_{MM} \ {PC_{MM} , d_{MM} , a_{MM} }.

(b) S_{2} is an unreachable state.

In case line(s) = 4 and terminating(s) we define DataVal(s) = S_{2}(d_{MM} ), address(s) = S_{2}(a_{MM} ), and Val(s) as in (8).

5. An execution of line 5 is a write which is always terminating.

We define line(s) = 5 iff S_{1}(P_{MM} ) = 5, S_{2} is a regular state, S_{2}(P_{MM} ) = 6, and

S_{2}(Mem[S_{1}(a_{MM} )]) = S_{1}(d_{MM} ).

On every variables other than P_{MM} and Mem[S_{1}(a_{MM} )] S_{1} and S_{2} agree.

In case line(s) = 5, define DataVal(s) = S_{1}(d_{MM} ) and address(s) = S_{1}(a_{MM} ).

6. An execution of line 6 is an enqueue of the triple (S_{1}(d_{MM} ), S_{1}(a_{MM} ), ∗) on queue In_{i}. It is always terminating. However, since this queue is not a variable in V_{MM} , a step that represents this operation does not change any of its variables except the program counter.

We define line(s) = 6 iff S_{1}(P_{MM} ) = 6, S_{2} is a terminating state, S_{2}(P_{MM} ) = 7, and S_{2}(v) = S_{1}(v) for any other variable.

In case line(s) = 6, define DataVal(s) = S_{1}(d_{MM} ), address(s) = S_{1}(a_{MM} ), and Val(s) = ⟨DataVal(s), address(s), ∗⟩. We also define in this case Qindex(s) = S_{1}(i_{MM} ).

7. An execution of line 7 is a dequeue event which can be non-terminating (in case Out_{i} is empty). Since Out_{i} is not a variable in V_{MM} the pair of local states (S_{1}, S_{2}) that represents this step do not reflect the change in the queue.

We define line(s) = 7 iff S_{1}(PC_{MM} ) = 7, S_{2}(PC_{MM} ) = 8, and one of the following two possibilities holds.

(a) S_{2} is a regular state, and then S_{2}(X) = {1, …, N} \ {S_{1}(i_{MM} )}, and S_{2}(v) = S_{1}(v) for every variable v ∉ {PC_{MM} , X}. This step prepares X to be in its initial value suitable for executing line 8 (see below).

(b) S_{2} is an unreachable state.

We do not define the DataVal and address function on these steps, but we define Qindex(s) = S_{1}(i_{MM} ).

8. An execution of line 8 is a sequence of N − 1 enqueue operations to queue In_{k}, where 1 ≤ k ≤ N and k ≠ i, executed in any order. This execution is represented by N − 1 steps, and variable X serves for that purpose by recording the set of indices for which this enqueue operation has not yet been executed. We use pairs 8.k where 1 ≤ k ≤ N to denote “lines” of steps in which In_{k} is about to be enqueued.

We define line(s) = 8.k iff S_{1}(PC_{MM} ) = 8, k ∈ S_{1}(X), S_{2} is a regular state, S_{2}(X) = S_{1}(X) \ {k}, S_{2}(PC_{MM} ) remains 8, and for all other variables S_{2} and S_{1} agree.

In case line(s) = 8.k define DataVal(s) = S_{1}(d_{MM} ), address(s) = S_{1}(a_{MM} ), and Val(s) as in (8). Then Qindex(s) = k.

We define line(s) = 8 iff S_{1}(PC_{MM} ) = 8, S_{1}(X) = ∅, S_{2} is a regular state, S_{2}(PC_{MM} ) = 1, and all other variables are left unchanged.

Again, we define “oblivion steps” as pairs of the form (S, S) where S is an unreachable state of P_{MM} .

Definition 6.3 A pair of states s = (S_{1}, S_{2}) is a step iff it is either a P_{i} step for some 1 ≤ i ≤ N or a P_{MM} step, as defined in 6.2.3 and 6.2.4. Let Step(x) be the formula saying that x is a step. We shall refer to Step also as a set and write s is in Step etc.

6.2.5 Unrestricted history structures.

Let i be an index either in {1, …, N} (referring to P_{i}) or i = N + 1 (referring to P_{MM} ). Recall that I_{i} is canonically interpreted as ω × {i}, a copy of ω, and we shall write k_{i} for ⟨k, i⟩ (the copy of k).

Definition 6.4 A canonical interpretation of the Sig signature in which each H_{i} for 1 ≤ i ≤ N + 1 satisfies the “history requirement” (stated below) is called an unrestricted history structure of the DLC algorithm. The hisotry requirement is the following sentence.

H_{i} is defined over I_{i} and is such that H_{i}(0_{i}) is an initial state of P_{i} and for every n ∈ ω the pair ⟨H_{i}(n_{i}), H_{i}(n + 1_{i})⟩ is a step of P_{i}.

Let M denote an unrestricted history structure of the DLC algorithm. Since M is fixed and there is no place for confusion, we shall write I_{i} and H_{i} instead of I_{i}^{M} and H_{i}^{M} for these interpretations. So H_{i} is a sequence of states that represent an execution of the protocol (of P_{i} or P_{MM} ). However, the values obtained in dequeue steps in M are not necessarily related to the values enqueued. This is why M is called “unrestricted”. The only restriction imposed on M is that for each process alone its events are regulated by the protocol of that process. Every k_{i} ∈ I_{i} represents the step (H_{i}(k_{i}), H_{i}(k + 1_{i})). Observe that if some step (H_{i}(n_{i}), H_{i}(n + 1_{i})) is non-terminating, namely if H_{i}(n + 1_{i}) is an unreachable state, then, for every k > n, H_{i}(k_{i}) is unreachable. This is so because only oblivion steps begin with an unreachable state.

6.2.6 Definable predicates and functions.

A definable predicate is a new predicate symbol, P, of arity n connected to a defining formula φ_{P} (x_{1}, …, x_{n}) with an axiom that introduces it by

∀\overline{x}(P (\overline{x}) ↔ φ_{P} (\overline{x})).

A definable function is a new function symbol, F, of arity n connected to a defining formula φ_{F} (x_{1}, …, x_{n}, y) and the axiom

F (\overline{x}) = y ↔ φ_{F} (\overline{x}, y).

In this subsection and in the following one (6.2.7) we define predicates and functions which are added to the Sig signature and form the extended Sig^{+} signature. We define the following predicates in the language of Sig.

1. The formula Step has been define (Definition 6.3), and we define here a function step on ⋃_{1≤i≤N+1} I_{i}. For every k ∈ ω and 1 ≤ i ≤ N + 1 define

step(k_{i}) = (H_{i}(k_{i}), H_{i}(k + 1_{i})).

This function gives the k-th step in H_{i}. Define Event(e) iff e = k_{i}, for some k and i, and s = step(e) is not an oblivion step. That is, s = (S_{1}, S_{2}) where S_{1} is a regular state. If Event(e), define terminating(e) iff step(e) = s is a terminating step. That is, s = (S_{1}, S_{2}) where S_{2} is a regular state. Define Index = {1, …, N + 1}. The numbers 1, …, N + 1 are constants. We can write MM for N + 1. The function line defined on the steps is naturally extended over Event by the definition line(e) = line(step(e)). So if e = k_{i} is an event, then line(e) = ℓ indicates that e represents an execution of (the instruction at) line ℓ by P_{i}. Similarly, the partial functions DataVal and address can be (partially) defined on Event by DataVal(e) = DataVal(step(e)) and address(e) = address(step(e)).

2. We are going to define the processes P_{i}, for 1 ≤ i ≤ N, and the process P_{MM} . We shall also define a function index on the events. The aim of index(e) = i is to indicate that P_{i}(e) holds. For 1 ≤ i ≤ N + 1 define P_{i}(e) iff Event(e) and e = k_{i} for some k ∈ ω. In this case define index(e) = i. Thus, P_{MM} (e) iff Event(e) and e = k_{N+1} for some k ∈ ω. We define <_{i}, for every 1 ≤ i ≤ N + 1, as the natural ordering on P_{i}. That is, j_{i} <_{i} k_{i} is defined for j_{i}, k_{i} ∈ Event iff j < k. In other words, <_{i} is the natural ordering on I_{i} restricted to the set of events (which can be all of I_{i} or an initial segment). Instead of <_{N+1} we write ≺. Although a <_{i} b implies that both a and b are in P_{i} we shall often repeat this fact for emphasis.

3. For events e that correspond to execution of some operation on a queue (Out_{i} or In_{i}), we define the function Qindex(e) = k to say that the queue approached has index k. Thus if step(e) = s = (S_{1}, S_{2}) we define Qindex(e) = k iff 1 ≤ k ≤ N, Event(e), and one of the following holds:

(a) P_{k}(e) and line(s) ∈ {4, 5}. (Process P_{k} approaches only Out_{k} and In_{k}.)

(b) P_{MM} (e), line(s) ∈ {3, 4, 6} and k = S_{1}(i_{MM} ). (The value of variable i_{MM} being k tells P_{MM} to approach In_{k} in line 3, Out_{k} in line 4, and In_{k} in line 6.)

(c) P_{MM} (e), and line(s) = 8.k. (Item 8 of 6.2.4 explains that line(s) = 8.k indicates that step s is viewed as an enqueue on In_{k}.)

4. We shall define for queues Out_{i} the formulas enqueueOut_{i}, dequeueOut_{i}, peekOut_{i}, and similarly the corresponding formulas for queues In_{i}, for every 1 ≤ i ≤ N. The idea is that if Q is one of these queues, then enqueueQ(e) says that e is an enqueue event of Q. In this case Val(e) is the value of the item enqueued. Similarly, dequeueQ(e) says that e is a dequeue event, and in case terminating(e) then Val(e) is the value dequeued. We give below just two examples of these formulas, since the definitions of the other formulas follow similar lines.

Define enqueueOut_{k}(e) iff 1 ≤ k ≤ N, Event(e), P_{k}(e), and line(e) = 4. (This definition was obtained by observing that Out_{k} is approached for enqueues only be executions of line 4 of the DLC algorithm of P_{i} where i = k.)

Define enqueueIn_{k}(e) iff Event(e), P_{MM} (e), and one of the following holds, where step(e) = s = (S_{1}, S_{2}).

1. line(e) = 3 and Qindex(e) = k. In simple words, e is an execution of line 3 in MemoryRead procedure, enqueueing In_{k}. In this case define

Val(e) = (DataVal(e), address(e)).

DataVal(e) and address(e) were defined above by:

DataVal(e) = S_{1}(Mem[S_{1}(a_{MM} )]),
address(e) = S_{1}(a_{MM} ),

2. line(e) = 6 and Qindex(e) = k. Namely, e is the execution of line 6 in MemoryWrite: In_{i}.Enq(d, a, ∗); where S_{1}(i_{MM} ) = k. In this case define

Val(e) = (DataVal(e), address(e), ∗).

Recall that we have defined above:

DataVal(e) = S_{1}(d_{MM} ),
address(e) = S_{1}(a_{MM} ),

3. line(e) = 8 and Qindex(step(e)) = k. Namely, e is one of the N − 1 events executing line 8 of MemoryWrite, and e approaches In_{k}. In this case, DataVal(e) and address(e) are defined as above, but Val(e) = (DataVal(e), address(e)) has no asterisk.

6.2.7 Higher-level events.

A higher-level event is a (definable) finite subset of Event that represents a compound operation. Recall that every finite subset of HF(A) is an element of HF(A). We shall define here the following higher-level events (they correspond to executions of the procedures with the same names).

1. Higher-level events by P_{i} (for 1 ≤ i ≤ N) are: decide, Read, Write, CacheUpdate, and CacheInvalidate.

2. Higher-level events by P_{MM} are: decide, MemoryRead, and MemoryWrite.

Higher-level events by P_{i}. In the following definitions D, R, W, I, and U denote finite subsets of P_{i} for some 1 ≤ i ≤ N (see item 2 in 6.2.6 or the definition of P_{i}). We also define the functions Val and address on the Read, Write, and CacheUpdate events.

1. Define Read(R) iff R = {e} is a singleton such that line(e) = 3. In this case s = step(e) is terminating, s = (S_{1}, S_{2}) and we define Val(R) = DataVal(e), and address(R) = address(e).

2. Define Write(W) iff W = {e} is a singleton such that line(e) = 4. Define Val(W) = DataVal(e), and address(W) = address(e).

3. Define CacheUpdate(U) iff for some k ∈ ω line(k_{i}) = 5 and one of the following two possibilities holds:

(a) not terminating(k_{i}) and then U = {k_{i}} (is a non-terminating Cache-Update event), or

(b) k_{i} is terminating and U = {k_{i}, k + 1_{i}}, In this case define Val(U) = DataVal(k_{i}), and address(U) = address(k_{i}).

4. Define CacheInvalidate(I) iff I = {e} is a singleton and line(e) = 7.

Higher-level events by P_{MM} . In the following definition D, R, and W denote finite subsets of P_{MM} . The functions Val and address are defined on the MemoryRead and MemoryWrite events.

1. Define MemoryRead(R) iff R = {e} where line(e) = 3. In this case define Val(R) = DataVal(e)), and address(R) = address(e).

2. Define MemoryWrite(MW) iff for some k ∈ ω MW = {k_{N}, k+1_{N}, … (k+ 2 + N)_{N}} and line(k_{N}) = 4. In plain words, MW is a set of N + 3 consecutive events from P_{MM} , that constitute an execution of the MemoryWrite procedure. Here, k_{N} is the peek event corresponding to line 4, and we define:

Val(MW) = DataVal(k_{N}),

and

address(MW) = address(k_{N}).

Finally we define HL(X) iff X is a higher-level event as defined above. If HL(X) then for some i, 1 ≤ i ≤ N + 1, X ⊂ P_{i} and we define i = index(X).

6.2.8 Simple properties of unrestricted history structures.

Properties of unrestricted history structures are dubbed “simple” because no concurrency is involved in these structures. Every process has its own history function (H_{j}) and there is no relationship between the different processes. Therefore any property that we derive is a simple property of a sequential process. Usually these properties refer to the local states of each process, and we can prove them by induction.

S1 Suppose that C <_{i} R, where C and R are both in P_{i}, CacheUpdate(C), Read(R), and address(C) = address(R). If there is no CacheUpdate or CacheInvalidate event U such that C <_{i} U <_{i} R and address(U) = address(R), then Val(R) = Val(C).

To prove this, observe that only CacheUpdate and CacheInvalidate events can change the value of C_{i}[a].

S2 If dq is a dequeue event of Out_{k}, then there exists a unique MemoryWrite higher-level event containing dq.

S3 The only higher-level events that contain an enqueue operation on In_{i} are MemoryWrite and MemoryRead events.

S4 Suppose that MemoryWrite(MW), MemoryRead(MR), MW ≺ MR, and address(MR) = address(MW). If there is no MemoryWrite event M such that MW ≺ M ≺ MR and address(M) = address(R), then Val(MR) = Val(MW).

The reason for this is that only MemoryWrite events can change the value of Mem[a].

S5 If X and Y are higher-level events in P_{i}, then either X <_{i} Y (which means that x <_{i} y for all x ∈ X and y ∈ Y) or X = Y or Y <_{i} X. Hence if x <_{i} y for some x ∈ X and y ∈ Y, then X <_{i} Y.

6.3 Restricted executions

The unrestricted history structures defined in the previous subsection are unrestricted on two accounts. Firstly there is no temporal relation that relates events from different processes. The ordering <_{i} is a serial ordering of P_{i} (for 1 ≤ i ≤ N +1) but there is no < partial ordering as required from system executions. Thus unrestricted history structures are not system executions. Secondly, the enqueue and dequeue events are not required to operate properly.

Recall that the definition of unrestricted history structures (Definition 6.4) required them to be canonical interpretations of signature Sig (Definition 6.1) in which each H_{i} satisfies the history requirement (6.2.5). Recall also that we defined relations and functions in 6.2.6 and 6.2.7.

We expand the Sig and define a larger signature Sig^{+} by adding the following items.

1. All definable predicates and functions that were defined in 6.2.6 and 6.2.7. In particular, we view the definable classes Event and HL as sorts of Sig^{+}.

2. A new binary predicate < defined on Event, and new (unary) function symbols γ_{Out_{i}} and γ_{In_{i}} for 1 ≤ i ≤ N.

Definition 6.5 If M is an unrestricted history structure of the DLC algorithm then an “expansion” of M to Sig^{+} is obtained by adding to M interpretations of < and of the γ functions.

A “restricted system execution of the DLC algorithm” is an expansion M′ to Sig^{+} of an unrestricted history structure of the DLC algorithm such that the following holds.

1. The symbols of Sig^{+} that were definable in M are interpreted in M′ in accordance with their definitions.

2. The expansion is a system execution. That is the interpretation of < as a relation on Event, together with predicate terminating, form a globaltime model. When the higher-level events are also considered, with the ordering < and the terminating relation defined as in Definition 2.1.1 (in subsection 2.1.1), then M′ is a system execution with higher-level events.

3. The restriction of < to P_{i} is <_{i} (for every 1 ≤ i ≤ N + 1).

4. For every queue Q (In_{i} or Out_{i}) the function γ_{Q}, the enqueue/dequeue/peek events on Q, and the Val function defined over them satisfy the queue specifications of section 2.2.

Not every every unrestricted history structure of the DLC algorithm is expandable into a restricted system execution, but those which are not do not interest us since they do not represent orderly executions of the algorithm. We want to prove the correctness of the algorithm by considering the restricted executions, and proving that they satisfy the correctness requirements. Not every restricted execution of the DLC algorithm is sequentially consistent. The problem is that we did not specify the conditions that should hold before each operation is invoked. Only now we can do this, since this specification relates to the precedence ordering and the γ functions of the queues. We do this in the following subsection.

6.3.1 Required properties of the decide operations.

A key element of the presentation of the DLC algorithm is still missing: the specification of the two decide functions–that of P_{i} and that of P_{MM} . The corresponding part of the Lazy Caching algorithm was easy to formulate: the “Allowed if” column of transition system M_{distr} (Figure 1) shows clearly when different steps can be taken. A read step R_{i}(d, a), for example, can be taken for some d in Data whenever:

1. Out_{i} is empty,

2. In_{i} is starless, and

3. C_{i}[a] ≠⊥.

We cannot phrase such simple specifications for our decide functions because we have only local states, in which the queues do not appear. Hence our specifications of the decide operations involve the γ functions of the different queues.

It is possible to write programs for the decide operations which show how they operate, but this will be a futile overspecification of the caching algorithm. Instead, we define higher-level properties to which these operations must comply. Still, in order to explain these higher-level properties, we describe very informally a possible policy of the decide operations.

The main point is that before any Read by P_{i} (for 1 ≤ i ≤ N) the decide operations must ensure that the three conditions stated above are met. This raizes the following wrinkle, a problem which exists also for the implementor of the Lazy Caching algorithm of M_{distr}. It is conceivable that after a check that the thre conditions hold for P_{i}, but before the ensuing Read operation begins, process P_{MM} enqueues a starred item into In_{i}, thereby spoiling the required condition. It is in order to overcome this difficulty that the ordering of the Lazy Caching instructions in the MemoryWrite operation was changed, and the dequeue of Out_{i} is executed after the enqueue of (d, a, ∗). (See lines 6 and 7 in Figure 4.)

The policy of decide that we describe is that before any decision on a Read execution the following are executed (in the prescribed order):

1. Wait until Out_{i} is empty. At this stage, assuming that the wait has been successful, P_{i} can be sure of the following fact. If W is the last Write operation by P_{i} so far (assuming there is one), and e ∈ W is the corresponding enqueue on Out_{i}, then there exists a dequeue event d such that γ_{Out_{i}}(d) = e (since e has been dequeued). But all dequeues of Out_{i} belong to MemoryWrite events, and hence d is an execution of line 7 at some MemoryWrite event MW. Let en ∈ MW be the execution of line 6, namely the enqueue of (d, a, ∗) into In_{i}. Then en precedes d, and en is the last enqueue of a starred item at this stage. And even at later times, as long as P_{i} does not execute another Write operation.

2. P_{i} ensures that enough CacheUpdate operations are executed, and with them dequeues of In_{i}, until some dequeue event q with γ_{In_{i}}(q) = en is executed. That is, P_{i} can read how deep is the deepset starred item in I_{i}, and if k ≥ 0 is that depth, then it executes k times CacheUpdate operations, the last of which will dequeue en.

We return to the more formal discussion now and write down the assumptions that we make on the decide events. Assumptions on decide by P_{MM} :

1. Suppose that dc is a decide operation that determines a MemoryRead event (by setting r = MR), let step(dc) = (S_{1}, S_{2}) be the corresponding step and a = S_{2}(a_{MM} ) be the address decided by dc. Then there exists some MemoryWrite event MW such that MW < dc and address(MW) = a. Hence if MW_{0} is the rightmost MemoryWrite event such that MW < dc and address(MW) = a, then Val(MW_{0}) = S_{2}(Mem[s]).

2. If dc is a decide operation that determines a MemoryWrite event (by setting r = MW) then Out_{i} is non-empty at dc. (See Definition 2.5.) This implies that P_{MM} , being the Consumer of queue Out_{i}, is cautious. So, all peek and dequeue events in MemoryWrite events are terminating.

3. A liveness assumption is that any item enqueued at Out_{i} is finally dequed by some MemoryWrite(i) operation. So the function γ_{Out_{i}} is onto the class of enqueue events.

Assumptions on decide by P_{i}:

1. If dc is a decide operation by P_{i} which sets the value of variable r_{i} to CU (namely dc is the decide operation that precedes a CacheUpdate operation) then In_{i} is non-empty at dc. It follows that all dequeue events of In_{i} are terminating.

2. If dc is a decide operation by P_{i} which sets the values of variables r_{i} to R, and variable a_{i} to a, then there is a write on C_{i}[a] that precedes dc and the last such write is of a Data value (that is, it is a write by a CacheUpdate event rather than a CacheInvalidate event).

3. If dc is a decide operation by P_{i} which sets the values of variable r_{i} ro R, and if there is a Write event that precedes dc, then the following requirement holds for any Write event, W, that precedes dc. Let e ∈ W be the enqueue event there (an execution of line 4). There exists a dequeue event, dq, of Out_{i} such that γ_{Out_{i}}(dq) = e and the following holds. Since all dequeue events of Out_{i} are in MemoryWrite events, there exists a MemoryWrite event MW such that the value of i_{MM} in MW is i, and dq ∈ MW. Now dq is an execution of line 7, and there exists in MW an enqueue event, en, on In_{i} which is the execution of line 6 in MW. The requirement is that there exists a CacheUpdate event CU in P_{i} such that CU < dc, and such that γ_{In_{i}}(deq) = en, where deq is the dequeue event in CU (the execution of line 8).

6.4 Correctness proof

We have now all the ingredients for the correctness proof.

Theorem 6.6 Let N be a restricted system execution of the DLC algorithm in which the decide events satisfy the assumptions on decide by P_{MM} and P_{i} for every i (listed in 6.3.1). Then N is sequentially consistent.

Proof. Recall first that sequential consistency was defined in Definition 2.7 by reference to the signature L_{serial} defined in section 2.3. We view N as an interpretation of L_{serial} by viewing sort HL as the sort of events (Event). (All other elements of L_{serial} appear in Sig^{+}, the signature of N, so that indeed N interprets L_{serial} and the theorem is meaningful.) Recall Theorem 3.3 which states that every system execution that satisfies the SC Axioms of section 3.1 is sequentially consistent. These axioms are formulated in the L_{SC} signature defined in section 3. Except for the function μ : Event → MemoryWrite, all other members of L_{SC} are also in Sig^{+}. So we plan to define this function μ in N, and then to prove that the reduct of N to the L_{SC} signature satisfies the SC Axioms and is thence sequentially consistent. It is necessary to take a reduct, because N does not satisfy, as it is, the SC Axioms. For example, A1 states that all events are terminating, yet the decide events can be non-terminating. It is only by interpreting sort Event as HL, the sort of higher-level events of N, that we can prove all events to be terminating.

6.4.1 Definition of μ

We defined the function μ over Write, MemoryRead, CacheUpdate, and Read events, with values in MemoryWrite events.

So let W be a Write higher-level event by P_{i}. According to item 3 in 6.2.7 W is a singleton of one event, W = {e} where P_{i}(e) and line(e) = 3. So e is an enqueue event on Out_{i} (that is enqueueOut_{i}(e) holds, by the definition of item 4 of 6.2.6). Since γ_{Out_{k}} is required by assumption number 2 made on the decide operation by P_{MM} to be onto the enqueue events on Out_{k}, there exists some dequeue event dq of Out_{k} such that

γ_{Out_{k}}(dq) = e.

Since γ_{Out_{k}} is one-to-one oon the dequeue events of Out_{i}, dq is uniquely determined by e. There exists a unique MemoryWrite event M such that dq ∈ M (this is a simple property, S2). We define

μ(W) = M.

Clearly, Val(M) = Val(W).

Now let MR be a MemoryRead event by P_{MM} . Then MR = {e} where e is a terminating enqueue event on some In_{i} queue. Say Val(e) = ⟨d, a⟩. It follows from

item 1 of the Assumptions on decide by P_{MM} (in 6.3.1) that there exists a MemoryWrite event MW such that MW < MR and address(MW) = a, and then that Val(MR) = Val(MW_{0}) for the rightmost such MemoryWrite event MW_{0}. We define

μ(MR) = MW_{0}.

Now let U be a CacheUpdate event by P_{k}. By definition there exists some n ∈ ω such that line(n_{k}) = 5 and [n_{k}] = U (namely U is the unique HL event containing n_{k}). We claim that n_{k} is a terminating dequeue of In_{k}. This termination follows from the first assuption on decide by P_{k} made in 6.3.1. Hence γ_{In_{k}}(n_{k}) = e is defined. It is an enqueue on In_{k} and we consider [e], the unique higher-level P_{MM} event containing e. A simple property is that [e] is either a MemoryWrite event or a MemoryRead event. In the first case we define μ(U) = [e] and in the second case μ(U) = μ([e]). In both cases Val(U) = Val(μ(U)) and address(U) = address(μ(U)).

Finally, let R be a Read event by some P_{i} (1 ≤ i ≤ N). It follows by item 2 of the assumptions on decide by P_{i} (6.3.1) that there exists a CacheUpdate event CU in P_{i} such that address(CU) = address(R) and CU < R. If we let CU be the last such CacheUpdate event, then we define

μ(R) = μ(CU).

Clearly, Val(CU) = Val(R)

The definition of μ has the following consequences.

Lemma 6.7 If V <_{i} W then μ(V) ≤ μ(W).

Proof. This follows from the fact that γ_{Out_{i}} is order preserving on the dequeue events.

Lemma 6.8 1. If W is a Write, then W < μ(W).

2. If C is a CacheUpdate event then μ(C) > | C. Hence if R is a Read then μ(R) > | C.

3. If R <_{i} W are a Read and a Write, then μ(R) < μ(W).

Another useful observation is the following.

Lemma 6.9 If C_{0} <_{i} C_{1} are CacheUpdate events, of the same address, then μ(C_{0}) ≤ μ(C_{1}).

6.4.2 The AC Axioms hold.

Let N_{SC} denote the reduction of N to the SC signature, where Event is interpreted as HL, and μ as the function defined above. We have to check the axioms of section 3.1, one by one, and prove that they hold in N_{SC}. Many of these properties are simple, that is, they hold in every unrestricted execution of the protocol and have nothing to do with concurrency. For example, the statement in A1 that for i ≠ j there is no event both in P_{i} and in P_{j}. An event of P_{i} is a non-empty subset of I_{i} = ω × {i}, and this claim is trivial. We will not give the details of the proofs of the simple properties since they follow easily from the relevant defintions.

The first non-simple property is that each HL event is terminating. By 2.1.1, a higher-level event is terminating iff it is a finite set of terminating (lower-level) events. Since HL events are finite subsets of Event and since only peek and dequeue events can be non-terminating members of HL events, we must prove that every peek or dequeue events are terminating. It is one of the roles of the decide events—to ensure that if they determine executions of peek or dequeue events then these are terminating. For processes P_{i}, the only such events are the dequeue events of In_{i} executed in CacheUpdate operateions. Property 1 of the Assumptions on decideby P_{i} (in 6.3.1) says directly that these dequeues are all terminating. Process P_{MM} has peek and dequeue events in MemoryWrite operations. Property 2 in the list of Assumptions made on decide by P_{MM} ensures that the peek and dequeue events associated with lines 6 and 7 are terminating.

Property A2 is obvious. The fact that < extends each <_{i} is item 3 in Definition 6.5, and the linearity of <_{i} is a simple property (namely that (I_{i}, <_{i}) is isomorphic to (ω, <)).

The main point of A3 is that μ is a one-to-one correspondance between the Write and the MemoryWrite events. The claim that μ is one-to-one follows directly from the definition of μ and the fact that γ_{Out_{i}} is one-to-one. Indeed suppose W_{0} ≠ W_{1} are two Write events with W_{0} = {e_{0}} and W_{1} = {e_{1}}. Suppose that μ(W_{0}) = μ(W_{1}) = M. Let dq ∈ M be the (unique) dequeue event in M. It follows from the definition of μ that μ(dq) = e_{0} and μ(dq) = e_{1}, which is a contradiction.

Item A4 states that Val(E) = Val(μ(E)) and address(E) = address(μ(E)), and this was observed already when μ was defined.

Item A5 was proved in Lemma 6.7.

Item A6 was proved in Lemma 6.8.

Item L1 was proved in Lemma 6.9.

Item L2 is proved by considering the defintion of μ(C) for a CacheUpdate event C ∈ P_{i} such that M_{0} ≺ μ(C) (recall that ≺ is < restricted to P_{MM} ). Say C = {dq} where dq is a terminating dequeue of In_{i}. Then γ_{In_{i}}(dq) = e is defined, and the definition of μ(C) was such that μ(C) ⪯ [e]. Hence M_{0} ≺ [e]. But M_{0}, a MemoryWrite, contains also an enqueue event e_{0} on In_{i} (it contains enqueue events on all In_{k} for 1 ≤ k ≤ N). So e_{0} < e = γ_{In_{i}}(dq) implies that e_{0} = γ_{In_{i}}(dq_{0}) for some dq_{0} < dq.

Item L3 follows,rather directly, from item 3 of the Assumptions on decide by P_{i} (in 6.3.1).

Item L4 is actually a repeatition of the definition of μ(R) is case Read(R). This ends the proof of the SC Axioms and hence the proof of Theorem

6.6 which says that the DLC algorithm establish sequential consistencey if the decide operations satisfy their requirements.

7 Conclusion

A distributed version of the Lazy Caching algorithm of Afek, Brown, and Merritt [2] is described here—the DLCalgorithm. This version is “distributed” in the sense that we do not assume atomicity of complex operations. A correctness proof is given to this variant in which the notion of a global state does not appear. Our approach can deal with higher-level operations in the same framework in which it deals with lower-level events. Complexity becomes manageable because properties of higher-level operations can be stated with the aid of functions and predicates.

Part of the correctness proof is an abstract derivation (such as sequential consistency from SC Axioms) which is then applicable to more than one algorithm. By finding the common, higher-level properties of seemingly different algorithms we facilitate the proofs and increase the range of applicability of existing correctness proofs.

In several cases I found that a greater understanding of a protocol is obtained by finding what is common to a family of variants of that protocol. Not only from a practical point of view, but also scientifically it is desirable to classify variants of the Lazy Caching algorithm and to find out in what sense algorithms that appear to be similar are indeed similar. The answer given here is clear: similarity can be expressed by higher-level properties. For example, the list of SC Axioms is common to all variants, and in fact it defines a family of variant algorithms—namely those that satisfy the axioms. The properties are “higherlevel” in the sense that they speak about operation executions rather than about lower-level events (or transitions), and abstract in the sense that a first-order language is used to formulate them.

We have outlined here an approach to concurrency in which only local states are used to define unrestricted semantics, and system executions with abstract specifications of communication devices are used to complete the definition. A separation of concerns is a characteristic of our approach. The unrestricted semantics disregards the interprocess communication devices, and the restricted semantics is based on abstract definitions (of queues for example as in Section 2.2) which disregard the programs that use them. A detailed development of this approach with more applications is given in [1].

There is still much work to do before an engineering product along the direction roughly outlined here will be fabricated. It is clear however, even at this stage, that any such tools to check proofs or help proving the correctness of distributed programs should be flexible enough to handle any mathematical statements written in a first-order language: temporal logic is not sufficient to derive sequential consistency, for example, from the axioms of Section 3.1).

References

[1] U. Abraham, Models for Concurrency. Gordon and Breach 1999 [2] Y. Afek, G. Brown, and M. Merritt, Lazy caching. ACM Transactions on

Programming Languages and Systems 15(1):182-205 (1993)

[3] J. Barwise, Admissible Sets and Structures. Springer 1975.

[4] R. Gerth, Sequential consistency and the lazy caching algorithm. Distributed Computing 12:57-59 (1999)

[5] W. Hodges, The meaning of specifications II: Set-theoretical specification. Pages 43–68 in Semantics of Programming Languages and Model Theory, edited by M. Droste and Y. Gurevich. Gordon and Breach 1993.

[6] L. Lamport, How to make a multiprocessor that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28:690–691, 1979

[7] L. Lamport, A new approach to proving the correctness of multiprocess programs. ACM Trans. on Prog. Lang. and Systems 1: 84-97 (1979)

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

[9] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer 1991.

[10] Y. N. Moschovakis, Notes on Set Theory. Springer 1994.

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

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