Lazy Caching for lazy readers

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

June 7, 2002

Abstract Two distributed variants of the Lazy Caching algorithm of Afek, Brown, and Merritt [2] are described and proved to be sequentially consistent. These variants are distributed in the sense that (unlike the original algorithm of [2]) they do not consider a compound action that contains several instructions as an atomic operation. Only elementary operations on registers and 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. The two variant algorithms presented here share the same higher-level part. This expresses in a formal way the similarity between the two algorithms.

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 the Lazy Caching algorithm and two distributed versions.

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. Two variants of the Lazy Caching algorithm serve this purpose of gradually introducing this framework. The first is simpler and only the second reveals the complete picture. The 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 are based on 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 (for each of the variants) has two stages. The higherlevel 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. We will see that the two proofs of the two variants share the same higher-level stage. This is an obvious advantage of our framework.

Look at the Lazy Caching algorithm in Figure 2 (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 read/write and enqueue/dequeue events are atomic. Therefore obtaining a greater degree of concurrency.

The difference between our two variants is this. In the first variant the main memory pushes data to the processes in each memory write operation. (This is the mode of the original Lazy Caching algorithm, so that the difference between that algorithm and its variant is that we take no compound actions to be atomic.) In the second variant (the Lazy Readers algorithm) the main memory only sends invalidate messages to the processes whenever a write changes the value of a block. The processes have to pull data whenever it is needed and their cached data is invalid.

Although system executions and abstract higher-level arguments for sequential consistency are used in proofs of both variants, only in the second proof our method is fully exposed. In the first, global states are still used.

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, registers, and serial memories. Then we define sequential consistency using system executions. In the second part of this introduction we illustrate with an example how histories can be transformed into system executions.

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 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 (Lamport [8]) A global-time model is a structure

S = (E; <_{S} , terminating)

where E is a set (called the set of events), <_{S} is a partial irreflexive ordering relation on E, and terminating is a unary predicate 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 the models describe those atemporal objects which are not situated in time and do not fall under the precedence relation (such as the set of possible 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.2 A system execution is a two-sorted structure S = (E, C; <_{S} , F) with sorts E and C such that (E; <_{S} , terminating) is a global-time model, C is a sort (a set) which can be further divided into subsorts, and F is a collection of functions and relations on E ∪C (among which is the predicate terminating).

A system execution is thus a structure in the sense of Tarski, it has a signature (a list of symbols) which determines its language, and a formal definition is given to explicate when a formula holds in the structure. In fact, it is a two-sorted structure, namely its universe is divided into two types of members: events (which are partially ordered with <_{S} ) and atemporal objects (mainly to represent data values). The sort of atemporal objects is often further specified into subsorts, and we then have a many-sorted structure. Although sorts can be replaced by unary predicates (in some single sort universe) there are several advantages to many-sorted structures which makes them more convenient for our purposes. For example, in a regular single sort 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 events etc.) with a noticeable gain of clarity in formulas.

We will be particularly interested in set-theoretical system executions. In these structures one of the sorts represents sets, finite sets which are used to express functions, numbers, sequences etc. Section 2.5 contains details on these structures.

The correctness of an algorithm is expressed by a sentence and the requirement that it holds in each system execution that describes an execution of the algorithm. It is often the case that the correctness sentence describes higherlevel events and so we introduce them into our system executions (see section 6.3.1).

2.2 Specifications of queues and serial memory accesses

In this subsection we use system executions to give an abstract definition of queues and then of serial registers. This will specify our requirements from queue operations and serial registers which are used by our algorithms.

We first define a signature L_{queue} which is a list of symbols that define a first order language. Any language for system executions contains a binary relation symbol < to denote the temporal precedence (partial) ordering on the events, and a predicate terminating, to denote those events that are terminating. In addition to these standard symbols, L_{queue} contains the following.

Sorts: There are two sorts. Events and Data (Data contains the atemporal objects). (Events = Event. Sometimes we say e is in the sort of Events, and sometimes e is an Event.)

Unary predicates: Producer, Consumer, enqueue, dequeue, and peek. These are defined on the sort of events.

Functions: There are two functions. Val, and γ, defined on the events. Val returns Data values, and γ returns events.

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 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 L_{queue}. A system execution that satisfies these properties is said to comply to the queue specifications.

Given any system execution S that interprets the L_{queue} signature, and given any dequeue or peek event e in S, we say that Consumer is “cautious” at e in S 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). In section 2.7 we will give a formal argument in favor of these specifications by proving that they must hold in any system execution of a traditional queue transition diagram.

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.

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.

Serial read/write operations

The memory and cache locations which our processes access are serial registers. Our aim now is to specify these registers. The operations supported by a register are read (which returns a data value) and write (which requires a data parameter). The specification of these operations is simple. Let R be any register. Two predicates are needed: read_{R}(x) says that x is a read event, and write_{R}(x) that x is a write event. When the identity of the register is clear, we write read(x) and write(x). These read/write events are assumed to be terminating, and Val(x) is the Data value read or written by x. In addition, it is convenient to have a “return” function ω defined on the read events. Two axioms suffice to characterize our requirements from such read/write events:

1. The set of read/write events is serially ordered by the temporal precedence relation <. The set of read events is disjoint to the set of write events.

Every read/write event is terminating.

2. For every read event r,

(a) ω(r) < r, ω(r) is a write event, and Val(r) = Val(ω(r)).

(b) There is no write event w such that ω(r) < w < r.

It follows from this that the first event is a write event (if it were a read event r, then ω(r) < r is a contradiction).

2.3 Serial memory

When there is a large number of registers it is not convenient to have read_{R}/write_{R} predicates for each register R, and it is preferable to have just read/write predicates and a function that assigns to each read/write event the name or address of its register. A serial memory is a collection of serial registers, each with its own address. To specify serial memories we add the addresses to the specification language, and require that read/write events to any address (or memory location as we say) comply to the seriality requirements.

To be more specific, define L_{serial} as the language that contains (in addition to the temporal precedence relation <, and the terminating predicate which are always present) the following:

1. The sort of atemporal objects is now divided into two subsorts: Addresses and Data. Then there is of course the sort of Events.

2. Unary predicates Read and Write defined on Events. (We use here the predicates Read and Write, rather than read and write, to match the corresponding names in our algorithm.)

3. Functions Val : Events → Data, and address : Events → Addresses.

4. A function ω from the Read events into the Write events.

Two seriality axioms specify serial memories:

1. The set of Read/Write events is serially ordered by the temporal precedence relation <. The set of Read events is disjoint to the set of Write events. The events are terminating.

2. For every Read event r,

(a) address(r) = address(ω(r)) and Val(r) = Val(ω(r)).

(b) ω(r) < r.

(c) There is no Write event w such that ω(r) < w < r and address(w) = address(r).

2.4 Sequential consistency

To define sequential consistency, we extend L_{serial} by adding N unary predicates P_{1}, …, P_{N} defined on the events. If P_{i}(e) then we say that e is an event in process P_{i}. Let L = L_{serial}^{P_{1},...,P_{N}} be the language thus obtained.

Sequential consistency is a second-order property in the sense that its definition involves an existential quantification over all possible serial orderings of events. Let S be a system execution that interprets the language L defined above. We say that S is sequentially consistent iff

1. Every Read/Write event e is in some unique P_{i} (i.e. P_{i}(e) holds but ¬P_{j}(e) for j ≠ i).

2. There exists a serial ordering <^{∗} of the set of (Read and Write) events in S such that: If S^{∗} is the structure obtained from S by replacing its temporal precedence relation <_{S} with <^{∗}, then:

(a) S^{∗} is a system execution that satisfies the serial memory requirements.

(b) For every process index i, for all Read/Write events x, y in P_{i}, x <_{S} y iff x <^{∗} y.

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}.

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.

2.5 Set-theoretic systems

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 ∈ ω 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] and W. Hodges [5], we shall see that it is convenient to develop set theory with urelements in order to specify concurrent systems. Urelements are things in our universe that have no members and yet are not the empty set. We use them to represent atomic events and 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. ^{1}

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 ∈ ω}.

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 of sets, and a single predicate the membership relation ∈. (Besides equality which is automatically included in any signature.)

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. We define a signature σ_{0} which contains a specific sort named Set and a membership predicate ∈. Let M_{0} = (C_{1}, …, C_{n}; F) be any structure that interprets σ_{0}. It is a many-sorted structure with universe consisting of n sorts C_{1}, …, C_{n}, and with a collection F of constants, functions, and predicates on V = ⋃_{1≤i≤n} C_{i}. Suppose for definiteness that C_{n} = Set^{M_{0}} is the sort of sets in M_{0}. And let U = C_{1} ∪ ⋯ ∪ C_{n−1} be the union of all sorts in M_{0} that are not sets. We say that M_{0} has a standard set theoretical interpretation if the sets in Set^{M_{0}} represent the collection of all hereditarily finite set constructed over U as urelements. Formally we require that for some set A of urelements the structures (U, Set^{M_{0}}; ∈^{M_{0}}) and HF(A) are isomorphic. That is, there exists a function

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].

Event type  Allowed if  Action
Enq(d)  true  q.Enq(d)

Deq(d) q is non-empty and d is the value at head of q.

q.Deq()

peek(d) q is non-empty and d is the value at head of q.

no action

isEmpty(t) q is non-empty and t is false, or q is empty and t is true.

no action

Initially: q is an empty queue.

Figure 1: A transition diagram M_{q} for a queue, with four Event types.

i : V → HF(A), one-to-one and onto, such that for every a ∈ V a ∈ U iff i(a) ∈ A, and for every x, y in V, x ∈^{M} y iff i(x) ∈ i(y).

Usually, we fix a standard set-theoretical interpretation M_{0} of σ_{0}, which is called here the “base” structure. Then we define a signature σ that extends σ_{0} (obtained by adding function and relation symbols) and a specification sentence φ is expressed in σ. Then we define M as the collection of all models M of φ that are expansions of M_{0}. That is such that M_{0} is a reduct of M. (The reduct of a structure M to a sub-signature σ_{0} is a structure N obtained by taking the interpretations of M to the sorts, functions, predicates, and constants of σ_{0}.)

In particular, a set-theoretic system execution is a system execution as defined in Section 2.1 that has the form S = (E, C, Set; <_{S} , ∈, F) and that has a standard set theoretical interpretation.

2.6 States and histories

Given a collection Var of variables with a set Type_{v} of possible values for each v ∈ Var, a state over Var is a function S defined on Var (or a subset of Var) and such that S(v) is in Type_{v} for every v in the domain of S. A state is an instantaneous description of the system. Usually a certain subset of states is defined to be the initial states.

When the system contains several processes and Var includes all local variables of the processes as well as all communication variables (queues, channels, interprocess registers etc.) then the state is called a global state. If a state is defined only on the local variables of some process P_{i}, but not over its communication variables, then we say that the state is local.

A pair of states (S_{1}, S_{2}) is called a transition: it represents an atomic change from state S_{1} to S_{2}. Transitions can be described by a transition diagram, and we illustrate this with the example of Figure 1. Transition diagram M_{q} assumes a single variable q which represents a FIFO queue. The set of possible values of q is the collection of all finite sequences of Data elements. Thus for every state S, S(q) is a (possibly empty) sequence (d_{0}, …, d_{k−1}), where k is the length of S(q) (k = 0 if the sequence is empty). As initial state we take the state S_{init} with an empty queue. That is S_{init}(q) = ∅.

In fact, any sequence s is a data structure and it supports the basic queue actions with the well-known semantics. If s is non-empty and its value is the sequence (d_{0}, …, d_{k−1}) then s.Deq() is the dequeue operation on s, returning the head value d_{0} and changing s to be the tail sequence (d_{1}, …, d_{k−1}) (which may be empty). If s is non-empty then s.peek() returns the head value s_{0} but does not change s. And for any Data value d the enqueue action s.Enq(d) changes s to be (d_{0}, …, d_{k−1}, d).

There are four classes of types of transitions in our example M_{q}.

1. An Enq(d) transition is a pair of states (S_{1}, S_{2}) such that S_{2}(q) = (S_{1}(q)).Enq(d). Namely the queue value at S_{2} is obtained from that of S_{1} by executing an enqueue operation of value d.

2. A Deq(d) transition is pair of states (S_{1}, S_{2}) such that S_{1}(q) = (d_{0}, …, d_{k−1}) is non-empty, d = d_{0}, and S_{2}(q) is the tail sequence (d_{1}, …, d_{k−1}) obtained by removing d from the head of S_{1}(q).

3. A peek(d) transition is a pair of states (S_{1}, S_{2}) such that S_{1}(q) is nonempty, d is the head value of S_{1}(q), and S_{2}(q) = S_{1}(q).

4. An isEmpty(t) transition (where t is a boolean value) is a pair of states (S_{1}, S_{2}) such that either S_{1}(q) is empty and t = true or else S_{1}(q) is non-empty and t = false. In any case, S_{2}(q) = S_{1}(q).

Observe that a pair of states (S_{1}, S_{2}) can be both a peek transition and an isEmpty transition. To remedy this, we attach to each transition its type. An occurrence of a transition in a history (together with its specific type) is called a step.

A history of M_{q} is an infinite sequence of steps H = (t_{i} | i ∈ ω) and corresponding sequence of Event types (Q_{i} | i ∈ ω). Where t_{i} is an occurrence of transition (S_{1}(t_{i}), S_{2}(t_{i})). (So S_{1}(t_{i}) and S_{2}(t_{i}) are the two states of the step.) Such that:

1. S_{1}(t_{0}) is the initial state S_{init} of empty queue.

2. For every index i, S_{2}(t_{i}) = S_{1}(t_{i+1}).

3. Every step t_{i} in H has Event type Q_{i} (of M_{q}). For example, if Q_{i} is Enq(d) for some d ∈ Data, then t_{i} being the transition consisting of pair of states

(S_{1}(t_{i}), S_{2}(t_{i})) = (A, B)

satisfies the requirement that B(q) = A(q).Enq(q).

The steps in any history are linearly ordered: t_{i} < t_{j} iff i < j.

2.7 Histories as structures

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 capable 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.)

A detailed discussion of the procedure for transforming a history into a structure can be found in [1]; here we take a somewhat different approach in which histories are directly construed as structures, using set theoretical concepts. This approach is exemplified in defining the history structures that correspond to the transition diagram M_{q} of Figure 1.

To define histories of M_{q} as structures we first define the following “base” structure M_{0} and define its signature σ_{0} consisting of sorts, functions, and predicates as follows. We require that M_{0} has a standard set theoretical interpretation.

M_{0} contains the following.

1. Sort Data is interpreted in M_{0} as some set of unspecified data values. (These are the value that that appear in the queue operations.)

2. Sort Boolean with its two values, true and false. (It is possible to have this as a subsort of Data.)

3. Sort Var contains all the variables: in our case just a single state variable, q, which represents the queue. In general, states will be functions defined on this sort Var.

4. Sort EventType contains for each d ∈ Data, the objects Enq(d), Deq(d), peek(d). And for each boolean value t an object isEmpty(t). We need a function Val which assigns to each object t ∈ EventType its value Val(t). For example, if t is Enq(d) then Val(t) = d. So the functions Enq, Deq, and peek are from Data into EventType, the function isEmpty is from sort boolean into EventType, and the function Val, is from EventType back into the appropriate values. That is, Val(Enq(d)) = d etc. These are functions of the structure M_{0}.

5. Sort Set and the membership relation ∈ are in M_{0}. The class of natural numbers ω is identifiable as a subsort of Set.

6. A sort Step will be used to represent the step of the history. We assume in M_{0} a one-to-one function t from ω onto Step, enumerating the steps in increasing order {t_{i} | i ∈ ω}. This induces a linear ordering < of the steps. Namely t_{i} < t_{j} iff i < j. (Here t_{i} is t(i), an application of function t to i.)

7. We assume that M_{0} has a standard set theoretical interpretation. That is, Set is (or is isomorphic to) the collection of sets in HF(U) where U is the union of all sorts of M_{0} except Set itself (and ω which is a subsort of Set).

In a short while we shall enlarge σ_{0} to a signature σ obtained by the addition of three function symbols Q, S_{1} and S_{2}. We shall write a sentence φ in σ, and then the collection of all structures M that expand M_{0} by interpreting these three functions so that φ holds will be defined to be the collection of history structures of M_{q}.

First we define a formula DataSequence(s) which says about set variable s that it is a sequence of Data values, namely a function from some initial set 0, …, n − 1 of natural numbers into Data. In writing this formula we are allowed to use all the machinery of Set Theory which shows how functions are to be defined as sets. For convenience we may now add this formula as a set predicate to our language.

Then we can define the notion of states in M_{0}. We do it just as before, yet now the definition is completely formal. Namely we define a formula state(s) with a single free variable s (varying over sets) which expresses the fact that s is a state. In this formula we use the notion of functions and DataSequence previously specified.

Transitions can be defined formally in M_{0}. We can also define a relation between a transition s and EventType p saying that s is of type p (see the definitions of the four classes of types of transitions in section 2.6).

Next we extend our signature with three functions: Q, S_{1} and S_{2}. These are defined on sort Step. For every Step s, Q(s) ∈ EventType is “its type”, and ⟨S_{1}(s), S_{2}(s)⟩ is the transition corresponding to s. Let σ be the resulting extended signature.

A history structure is defined to be any expansion of M_{0} obtained by interpreting Q, S_{1}, and S_{2} in which the following Transition Properties holds:

Definition 2.3 (Transition Properties:) 1. For S = S_{1}(t_{0}) which is the initial state we require that S(q) = ∅. That is, the queue is empty in the initial state.

2. For every index i, S_{2}(t_{i}) = S_{1}(t_{i+1}). That is, the resulting state of step t_{i} is the starting state of the following step.

3. For every step s ∈ Step exactly one of the following four alternatives hold:

(a) Q(s) = Enq(d) for some d ∈ Data. In this case S_{2}(s)(q) = (S_{1}(s)(q))^{⌢}⟨d⟩. That is, the state of the queue after an enqueue event s is obtained by concatenating its state S_{1}(s)(q) just before executing s with the one-element sequence ⟨d⟩.

(b) Q(s) = Deq(d) for some d ∈ Data. Then S_{1}(s)(q) is non-empty and has the form ⟨d, d_{1}, …, d_{k−1}⟩, and S_{2}(s)(q) is ⟨d_{1}, …, d_{k−1}⟩.

(c) Q(s) = peek(d) for some d ∈ Data. In this case S_{1}(s)(q) is nonempty, d = (S_{1}(s)(q))(0), and S_{1}(s) = S_{2}(s).

(d) Q(s) = isEmpty(t) where t is either true or false. Then t = true if and only if S_{1}(s)(q) is empty. In any case S_{1}(s) = S_{2}(s).

Let M be a history structure, as defined above. For later use, we add predicates and functions as follows to M.

1. Unary predicates are defined below on the steps, in accordance with their types: dequeue, enqueue, peek, and checkingEmptiness. The Data valued function Val is defined on the steps. Let s be a step (some t_{i}) and consider Event type Q(s).

(a) If s is an Enq(d) step (that is if Q(s) is Enq(d)), then we define enqueue(s) and Val(s) = d (its Data value). Intuitively, this says that step s with its transition (S_{1}(s), S_{2}(s)) represents an enqueue event of value d.

(b) If s is a Deq(d) step, then we define dequeue(s), and Val(s) = d.

(c) If s is a peek(d) step, then we define peek(s) and Val(s) = d.

(d) If s is an isEmpty(true) or isEmpty(false) step, then we define checkingEmptiness(s), and Val(s) = true in the first case and = false in the second.

The role of checkingEmptiness(s) is to say that step s checks whether the queue is empty or not, and Val(s) is the boolean answer. (We can define Boolean as a subsort of Data and then Val is into Data.)

2. A predicate “terminating” is defined on the steps. All steps in M are terminating.

We can use the transition properties listed above in Definition 2.3, and prove by induction assertions about M. Any such assertion is bound to hold in any history structure M for M_{q}. This resembles the assertional method, but the range of possible assertions is greater than the state-assertions of the classical approach because the language of M is richer.

For example, referring to the queue specification in 2.2.1, we can prove that Consumer is cautious in M and that the queue specifications hold in M. This proof can be seen as a formal justification of the specifications of 2.2.1. For this we must define the function γ from the dequeue and peek events to the enqueue events. Intuitively, γ takes the nth dequeue event to the nth enqueue event. We will show how to define the formula e = γ(d), and we will outline the proof that γ satisfies its specifications. Recall that our structure M contains all finite sequences of its elements. Let ϕ_{1}(r) be the formula which says that

“r is an enumeration, in increasing order, of an initial segment of enqueue events”.

More formally, using i and j as variables of members of ω and e as variable over steps:

r is a sequence of steps and ∀i < length(r)

1. enqueue(r(i)) and

2. ∀j such that i < j < length(r), r(i) < r(j) and

3. ∀e [enqueue(e) ∧ ∃k < length(r) (e < r(k)) ⟹

∃k < length(r)(e = r(k))] In a similar fashion we define ϕ_{2}(t) which says that t is an enumeration, in

increasing order, of an initial segment of dequeue events.

Next we define a formula enq(n, e) which says that n ∈ ω and e is the nth enqueue event. Namely, for some r such that ϕ_{1}(r), e = r(n). In a similar fashion we define deq(n, d) which says that d is the nth dequeue step.

We define now a formula γ(d, e) for two variables d and e (which are steps). It is a disjunction:

1. dequeue(d) and for some n ∈ ω, deq(n, d) and enq(n, e). Or

2. peek(d), and e is the first enqueue event not in the set

{e′ | for some dequeue event d′ < d γ(d′, e′)}.

Having defined the relation γ(d, e), we shall prove that for every dequeue and peek event d there exists an enqueue e < d such that γ(d, e). The uniqueness of this enqueue step e is obvious from the definition of γ. Namely, if d is the nth dequeue step, then the nth enqueue step (once we prove that it exists) is uniquely determined. In case d is a peek step, then there are no two steps e that can satisfy γ(d, e) because e is the first step that satisfies the requirement in 2. This justifies our subsequent functional form of writing e = γ(d). We shall also prove that Val(d) = Val(γ(d)) for every dequeue or peek step d..

Then it will follow directly from the definition that γ is one-to-one and order preserving on dequeue events. Namely, if d_{1} < d_{2} are dequeue events, then γ(d_{1}) < γ(d_{2}). (For if d_{1} it the nth dequeue step and d_{1} < d_{2}, then d_{2} is the mth dequeue step for m > n.)

It will also follow that Consumer is cautious. Namely for every dequeue or peek step d there exists an enqueue event u (which is γ(d)) such that u < d and u is not in {γ(x) | x < d, x is a dequeue}.

For the proof, we formulate an assertion α(s) on steps s and prove it by induction on s. That is, prove that α(t_{i}) holds for every i ∈ ω by induction on i, where {t_{i} | i ∈ ω} is the assumed enumeration of Step in increasing order. The induced ω ordering < on Step is also used.

It is convenient to define for every step s two sets R(s) and S(s) consisting of enqueue events that precede s.

e ∈ R(s) iff e < s ∧ enqueue(e)∧

∃(d < s)(dequeue(d) ∧ γ(d, e)). (2)

e ∈ S(s) iff e < s ∧ enqueue(e) ∧ e ∉ R(s).

It follows from the definition of γ that R(s) is an initial segment of enqueue events, and S(s) is a final segment of enqueue events that precede s. Intuitively, if we restrict our attention to those steps that precede s, then R(s) is the set of those enqueue steps that were already dequeued, and S(s) is the set of those remaining enqueue steps that were not yet dequeued. Now we formulate our assertion α(s) which will be proved to hold for every step s..

1. For every dequeue or peek step, d < s, S(d) ≠ ∅ and γ(d, e) where e is the first step of S(d). In this case Val(d) = Val(e). thus it follows that e = γ(d) is defined for every d < s that is a dequeue or peek step.

2. the value, S_{1}(s)(q), of the queue just before step s is equal to the sequence of values of all enqueue steps e ∈ S(s) enumerated in order. That is, if we define the sequence u so that u(0) < ⋯ < u(m − 1) is the enumeration in increasing order of S(s) (which may well be empty), then

S_{1}(s)(q) = Val(u(0)), …, Val(u(m − 1)).

(A short set-theoretical argument is needed to prove that such a sequence u exists.)

We give a partial outline for the inductive proof that α(t_{i}) holds for all i ∈ ω. Since S_{1}(t_{0})(q) is the empty sequence, α(t_{0}) is obvious.

Assume that α(t_{k}) holds. Relying on item 3 of Definition 2.3 (Transition Properties), there are four possibilities for the type of s = t_{k}, and the proof that α(t_{k+1}) holds is by considering them all: Enq(d), Deq(d), peek(d), and isEmpty(t). As an example, we give the details for the first case. So assume that enqueue(t_{k}), and let v = Val(s). Item 1 of α(t_{k+1}) is obvious: since t_{k} is an enqueue step, for any dequeue or peek step d < t_{k+1}, d < t_{k}, and induction can be applied. For item 2 of α(t_{k+1}) we use items 2 and 3(a) of Definition 2.3:

S_{1}(t_{k+1})(q) = S_{2}(t_{k})(q) = (S_{1}(t_{k})(q))^{⌢}⟨v⟩.

This entails α(t_{k+1}).

We shall later need the following lemma which is easy to prove.

Lemma 2.4 Suppose that for some steps k_{1} < k_{2} we have

1. S_{1}(k_{1})(q) = ⟨v_{0}, …, v_{n−1}⟩ is non-empty, and v_{0} is its head value.

2. There is no step m such that k_{1} ≤ m < k_{2} and m is a dequeue step.

If k_{2} is a peek or a dequeue event, then γ(k_{2}) < k_{1} and Val(k_{2}) = v_{0}.

Every history structure is a system execution (a set theoretical system execution) with Step as sort of Events, and < is the precedence relation. A lesson that can be drawn from this section is that one can freely use the queue specification of section 2.2.1. Although it is possible to give a direct justification for this specification and to argue that the properties of γ express our understanding of what a queue should do, the specification of 2.2.1 may appear strange at first, because the values of the queue are not represented. Namely, sequences of Data do not figure in that specification. The proof given in the present section that the properties of γ are deducible from the traditional specification of queues (which use a transition diagram such as M_{q}) should convince our reader that those properties hide no surprises and can safely be assumed.

3 Properties entailing Sequential Consistency

In the first part of this section we define a first-order language L_{SC}, by listing its vocabulary. This language extends the language L of section 2.4 by which sequential consistency was explicated. Then we write down a series of properties, called SC Axioms, which suffice to prove sequential consistency of the Read/Write events. In the second part (3.2) another set of axioms, called Caching Axioms, is described and proved to imply the SC axioms. In our correctness proofs we will actually prove that executions of the algorithms satisfy the Caching Axioms.

We start by defining the formal vocabulary of the SC language and the corresponding informal English expressions that are used in an informal discourse.

sorts: There are four sorts: Events, Data, Indices, and Addresses. Constant d_{0} in Data is the initial value.

predicates: P_{1}, …, P_{N} are unary predicates over sort Events (N is the number of processes). If P_{i}(e) holds then we say that event e is by process P_{i}. Unary predicates Write and Read are defined over the events. If Read(x) then x is said to be a Read event, and similarly x is a Write event if Write(x). We say that x is external if Read(x) ∨ Write(x).

Unary predicate, MemoryWrite, is defined on the events. If MemoryWrite(x) then x is said to be a Memory Write event (it is also called an internal memory write event, to distinguish it from the external Write events).

There are binary relation symbols on sort Events: <_{i} for i = 1, …, N, and ≺. (The role of each <_{i} is to serially order the external events of P_{i}, and ≺ is the serial ordering of the Memory Write events.)

Also < is used to represent the temporal precedence relation on the events. A unary predicate terminating is used.

functions: The unary function Val is defined over the events, and it gives Data values. If Val(e) = d then we say that d is the data value of e (“written” by e if e is a Write or Memory Write event, and “returned” by e if e is a Read event). Another unary function is address: for any Read, Write, or Memory Write event x, address(x) ∈ Addresses is the address read or written by x. We say that Read or Write event x “accesses” its address address(x).

For every event e, index(e) ∈ Indices = {1, …, N} is the index of e. A function of major importance is μ defined on the Read/Write events and it returns Memory Write events. If μ(x) = m then Memory Write event m is said to “correspond” to the Read/Write event x. Intuitively, Write(e) and m = μ(e) say that e is a write event and the its request to write Val(e) on memory location address(e) is executed by Memory Write event m. Similarly, Read(e) and m = μ(e) say that the value obtained by the read e was written on memory by m.

A system execution S is an interpretation of this L_{SC} language if its universe consists of four sorts: E for the Events, D for the Data, I for the Indices, and A for the Addresses. It interprets the temporal relation ordering < and the terminating predicate in such a way that (E; <_{S}, terminating) forms a globaltime model, and it interprets each of the predicates and function symbols of L_{SC}.

3.1 SC Axioms

The following list of properties (called SC Axioms) specifies a collection of system executions: those which 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.

1. For indices i ≠ j, the events in P_{i} are disjoint to those in P_{j}, and disjoint to the MemoryWrite events. For every event x, external(x) iff Read(x) ∨ Write(x). No event can fall under two predicates from: Read, Write, MemoryWrite. Every external event is in some P_{i}. We have already said that MemoryWrite events are not in any P_{i}. (At this moment we have only Read, Write, and Memory Write events, but in the following subsection Cache Update events will also be added to the processes. So the present specification does not exclude the possibility that P_{i} contains additional events beyond the Read/Write.)

2. For i = 1, …, N, <_{i} is the restriction of the precedence relation < to the Read/Write events in P_{i}. Though < is a partial ordering, <_{i} is a linear ordering of the external events in P_{i}. The relation, ≺ is a linear ordering of MemoryWrite. (We write M_{1} ⪯ M_{2} for M_{1} ≺ M_{2} ∨ M_{1} = M_{2}.)

3. The restriction of the function μ to the Write events establishes a oneto-one correspondence between the Write events and the Memory Write events. However, different Read events may correspond to the same Memory Write event.

4. For every external event x, Val(x) = Val(μ(x)) and

address(x) = address(μ(x)).

That is Read/Write events have the same data value and the same address as their corresponding Memory Write events.

5. For every Read/Write event x, P_{i}(x) iff index(x) = i. If x is a Write event in P_{i} and M = μ(x) is the associated MemoryWrite event, then index(M) = i.

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

7. 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).

8. If R is a Read by P_{i} of address a, M a Memory Write on a such that μ(R) ≺ M, then, for every P_{i} event U (Read or Write) such that U <_{i} R, μ(U) ≺ M holds.

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. 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 external 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, property 8 exclude this possibility.

Formally, we first define for each Read/Write event U, in P_{i}, a Memory Write event denoted χ(U) by the formula

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

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 ≺.

The ordering <^{∗} can now be defined. For every external events (that is Read or Write) 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 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 and define a return function ω as required by 2.4. 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.1 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 (3). This also proves the additional claim, namely that χ(e) ≺ χ(W).

Well, if e is a Read event, this follows from property 7 in the list of axioms, and if e is a Write event then this follows from 6. 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 the Memory Write events. In this case, it cannot be that both A and B are Write events, because this would implies that μ(A) ≠ μ(B) (by 3) 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 <^{∗}. 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. For every Read event R let ω(R) be that unique Write event W such that μ(W) = μ(R). (Existence and uniqueness of W is a consequence of item 3). 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 Memory Write event). Item 4 implies that W and M, and similarly R and M address the same memory location a and have the same 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.

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 item 8 of the SC axioms! (Where M = μ(V).)

3.2 Caching Axioms

The SC axioms give the fundamental reason for the correctness of the Lazy Caching algorithms, but we need more detailed axioms in order to prove the correctness of these algorithms. In particular, since the algorithms use Cache Update events, we need a description of their basic properties which is given by the list of Caching Axioms described in this section. We extend the SC language by adding a predicate CacheUpdate defined on the sort of events. The functions index, Val, and μ are defined on all CacheUpdate events as well (giving Indices, Data, and MemoryWrite events respectively). The following list of properties is called Caching Axioms. Essentially, the SC axioms 1–7 are repeated, but instead of Axiom 8, five Caching Axioms L1–L5 are introduced, which are then shown to imply that axiom.

The changes in the first seven axioms result from the addition of CacheUpdate events. Observe that for every Cache Update event x, P_{i}(x) iff index(x) = i, and that CacheUpdate events in P_{i} are serially ordered under <, but the possibility that a Cache Update event in P_{i} is concurrent with a Read/Write event in P_{i} is not excluded.

1. For indices i ≠ j, the events in P_{i} are disjoint to those in P_{j}, and to the MemoryWrite events. For every event x, external(x) iff Read(x) ∨ Write(x). No event can fall under two predicates from: Read, Write, MemoryWrite, CacheUpdate. If P_{i}(x) then Read(x)∨Write(x)∨CacheUpdate(x). Any Read, Write, or CacheUpdate event x is in some P_{i} (for i = index(x)).

2. For i = 1, …, N, <_{i} is the restriction of the precedence relation < to the events in P_{i}. The restriction of < to the Read/Write events in P_{i} is linear. The restriction of < to the CacheUpdate events in P_{i} is also linear. The relation ≺ is a linear ordering of MemoryWrite.

3. The function μ is defined on the Read/Write events and on the Cache-Update events. The restriction of the function μ to the Write events establishes a one-to-one correspondence between the Write events and the Memory Write events. However, μ is not generally one-to-one.

4. For every Read/Write or CacheUpdate event x, Val(x) = Val(μ(x)) and

address(x) = address(μ(x)).

5. For every Read/Write or CacheUpdate event x, P_{i}(x) iff index(x) = i. Thus every such event is in some (unique) P_{i}. If x is a Write event in P_{i} and M = μ(x) is the associated MemoryWrite event, then index(M) = i.

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

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

L1 If W <_{i} R, W a Write and R a Read events in P_{i}, if address(W) = address(R), then μ(W) ⪯ μ(R).

L2 If R_{0} <_{i} R_{1} are two Reads by P_{i} of the same address, then μ(R_{0}) ⪯ μ(R_{1}).

L3 Let M_{0} be a MemoryWrite event and C a CacheUpdate event 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}).

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

L5 Suppose that C <_{i} end(R) are a CacheUpdate and Read events in P_{i} such that R and μ(C) have the same address. Then μ(C) ⪯ μ(R).

Theorem 3.2 The Caching Axioms imply the SC axioms, and hence imply sequential consistency.

Proof. Axioms 1–7 from the SC list appear in the Caching list as well (in a slightly stronger form which includes Cache Update events). We must prove Axiom 8.

So let R be Read of address a in P_{i}, and M be a MemoryWrite of address a such that

μ(R) ≺ M  (4)

For every Read/Write event U in P_{i} such that U <_{i} R, we prove that μ(U) ≺ M.

Assume first that U and R have the same address a. Then μ(U) ⪯ μ(R): if U is a Read, use L2, and if U is a Write use L1. Hence we can suppose that address(U) ≠ a.

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 2: Transition system M_{distr} of the Lazy Caching algorithm.

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 by L4 some CacheUpdate event C_{1} in P_{i} such that C_{1} <_{i} end(R) and μ(C_{1}) = M_{1}.

As M ≺ M_{1}, there exists by L3 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} end(R) implies that C_{0} <_{i} end(R) and since R and M = μ(C_{0}) have the same address a, L5 implies μ(C_{0}) ⪯ μ(R). That is, M ⪯ μ(R), which contradicts (4). Q.E.D.

4 The Lazy Caching algorithm and its distributed variant

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 2 (with minor changes).

There is a main memory Mem, and for every address a 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 Addresses, but it is possible that C_{i}[a] =⊥, which indicates that the value at address a is not presently in cache 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 ∈ Addresses 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 ∈ Addresses, and queue In_{i} can also contain triples of the form (d, a, ∗) where ∗ is a special symbol. However, we are not going to represent these sequences as values of the queues. Rather, we shall use a function , γ, which assigns to every dequeue its corresponding enqueue step, and assume the specifications of section 2.2.1 (see also section 2.7).

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 3 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 2), 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 2) 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 first 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 distributed version of the Lazy Caching algorithm is described by a transition diagram (Figure 3), which we call M_{distributed}. In presenting M_{distributed}, we are still within the accepted framework of global states, transitions, and histories. However, our histories are structures capable of supporting first-order sentences, rather than plain sequences of transitions. The correctness proof will not be a traditional invariant-based proof. Every history H will be a system execution and we will prove sequential consistency of H. This proof consists in defining higher-level events in H and showing that they satisfy the abstract Caching Axioms of section 3.2.

We shall define history structures of M_{distributed} with standard set interpretation. First a base structure M_{0} and its signature σ_{0} are defined. Two sorts, Data and Addresses are assumed to be given. The states of the system are defined with respect to the following collection Var of variables which contains the queues In_{i} and Out_{i} of the different processes, the central memory Mem, the local caches C_{i}, the control variables PC_{i} for 1 ≤ i ≤ N, which control the P_{i} processes, and the control variable PC_{S} for the system. Mem and C_{i} are functions from Addresses into Data ∪ {⊥}, where ⊥ is a special value not in Data (a sort apart) used as an “undefined” value.

We next describe the sort ControlVal of all possible values of the control variables PC_{i} and PC_{S}.

The possible values of PC_{i} are R, W, CU[1], and CU(d, a)[2] where d is a Data value and a in Addresses. It will soon be clear why we add these parameters to CU. The value PC_{i} = R indicates that P_{i} is ready to execute a Read event, the value PC_{i} = W is for a Write event, and the values CU[1] and CU(d, a)[2] are for the first and second instructions in the Cache Update program.

The values assumed by control variable PC_{S} are

1. MR, to indicate that a Memory Read operation is enabled,

2. CI, to indicate a Cache Invalidate operation,

3. MW[1], to indicate that the system is ready to execute the first instruction of a Memory Write operation. Then MW_{i}(d, a)[2] and MW_{i}(d, a)[3] for the second and third instructions.

4. For every non-empty X ⊂ {1, …, N} that does not include i, MW_{i}(d, a)[X] is also a possible value for PC_{S}. The intention is that if PC_{S} = MW_{i}(d, a)[X], then for every k ∈ X the system can execute the In_{k}.Enq(d, a) instruction.

The first column of Figure 3 defines a sort of EventType, with corresponding functions and predicates. For example, for every index i, Data d and address a, R_{i}(d, a) ∈ EventType. Another example: for Data d, Addresses a, and indices 1 ≤ i, k ≤ N, where i ≠ k, MW_{i}(d, a)[4, k] ∈ EventType. We assume that these EventType values are pairwise different. If v is a value in EventType, then predicates (and functions into Data and Addresses) are assumed to tell if v is an R_{i}(d, a), event, a W_{i}(d, a) event etc.

Two additional sorts are needed: Step and Set. Step is countable, and as the set of natural numbers ω is definable in Set (with the membership relation ∈) we also assume a one-to-one map t from ω onto Step. So that Step = {t(n) | n ∈ ω}.

Sorts Data, Addresses, Var, ControlVal, EventType, and Step form the collection of urelements U, and Set is supposed to be HF(U). Let σ_{0} be the signature thus defined and let M_{0} be the interpretation of σ_{0} that we described (with an assumed standard set interpretation). Since all needed set-theoretical definitions can be made in M_{0} we can freely use simple notions such as pairs and finite sequences in our definitions. Thus states can be defined (with respect to sort Var defined above), and then transitions (pairs of states) that correspond to diagram M_{distributed} are defined as follows. Each of these definitions is a formula in the σ_{0} language.

Definition 4.1 (Transition Definition) 1. An R_{i}(d, a) transition is a pair of states (S_{1}, S_{2}) such that S_{1}(PC_{i}) = R, queue Out_{i} is empty in state S_{1}, queue In_{i} is starless in S_{1}, and d = S_{1}(C_{i})[a]. (The value S_{1}(C_{i}) of cache C_{i} in state S_{1} is a function defined on Addresses and S_{1}(C_{i})[a] is its value at address a.) The only difference between S_{1} and S_{2} is possibly in the value of PC_{i}, where S_{2}(PC_{i}) must be an initial value. Namely one of

Event type  Allowed if  Action

R_{i}(d, a) PC_{i} = R, Out_{i}.isEmpty, In_{i} is starless, and C_{i}[a] = d.

initialize PC_{i}

W_{i}(d, a)  PC_{i} = W  Out_{i}.Enq((d, a));

initialize PC_{i}

CU_{i}(d, a)[1] PC_{i} = CU[1], and In_{i}.peek() is either (d, a) or (d, a, ∗)

In_{i}.Deq(); PC_{i} := CU(d, a)[2]

CU_{i}(d, a)[2]  PC_{i} = CU(d, a)[2]  C_{i}[a] := d;

initialize PC_{i}

MW_{i}(d, a)[1] PC_{S} = MW[1] and Out_{i}.peek() = (d, a)

{PC_{S} := MW_{i}(d, a)[2] ; \atop Mem[a] := d}

MW_{i}(d, a)[2] {PC_{S} = \atop MW_{i}(d, a)[2]} PC_{S} := MW_{i}(d, a)[3]; In_{i}.Enq((d, a, ∗))

MW_{i}(d, a)[3] {PC_{S} = \atop MW_{i}(d, a)[3]} X := {1, …, N} \ {i};

PC_{S} := MW_{i}(d, a)[X]; Out_{i}.Deq()

MW_{i}(d, a)[4, k] {PC_{S} = MW_{i}(d, a)[X] \atop and k ∈ X} In_{k}.Enq((d, a));

X := X \ {k}; if X = ∅ then initialize PC_{S}

MR_{i}(d, a)

{PC_{S} = MR \atop Mem[a] = d} In_{i}.Enq((d, a)); initialize PC_{S}

CI_{i}(a) PC_{S} = CI C_{i}[a] :=⊥; initialize PC_{S}

All queues are initially empty. All cache locations C_{i}[a] are initially ⊥ (undefined). Instead of assuming that Mem[a] = d_{0} at the initial state, we assume initial events: W_{i}(d_{0}, a) events for all a ∈ Addresses, followed by MW_{i}(d_{0}, a) events (for some i for all addresses a). So every MR_{j}(d, a) event is preceded by some MW_{i}(d, a) event. Action “initialize PC_{i}” means: assign to PC_{i} a value in {R, W, CU[1]}. Action “initialize PC_{S} means: assign to PC_{S} a value in {MR, CI, MW[1]}. In the initial state the control variables are assumed to have an initial value.

Figure 3: Transition system M_{distributed} for the first variant of the Lazy Caching algorithm.

{R, W, CU[1]}. (A queue is starless if it contains no items of the form (v, m, ∗).)

We have in fact defined here a formula ρ(S_{1}, S_{2}, i, d, a) in the σ_{0} language, and we say (informally) that (S_{1}, S_{2}) is an R_{i}(d, a) transition instead of writing ρ(S_{1}, S_{2}, i, d, a).

2. A W_{i}(d, a) transition is a pair of states (S_{1}, S_{2}) such that S_{1}(PC_{i}) = W and S_{1} and S_{2} agree at all variables except that the value of queue Out_{i} at S_{2} is obtained from that of S_{1} by enqueuing the pair (d, a), and that the value of S_{2}(PC_{i}) is a (possibly different) initial value.

3. Transitions CU_{i}(d, a)[1] and CU_{i}(d, a)[2] are two transitions that correspond to the single, atomic transition CU(d, a) of transition system M_{distr}.

A CU_{i}(d, a)[1] transition is a pair of states (S_{1}, S_{2}) such that

(a) S_{1}(PC_{i}) = CU[1], and S_{1}(In_{i}) = ⟨v_{0}⟩^{⌢}\overline{v}, where v_{0} (head value) is either (d, a) or (d, a, ∗), and

(b) S_{2} is obtained from S_{1} by changing S_{2}(In_{i}) to \overline{v}, and setting S_{2}(PC_{i}) = CU(d, a)[2]. All other variables remain in S_{2} as in S_{1}.

A CU_{i}(d, a)[2] transition is a pair of states (S_{1}, S_{2}) such that S_{1}(PC_{i}) = CU(d, a)[2], S_{2}(PC_{i}) is an initial value of PC_{i}, and S_{2}(C_{i})[a] = d.

4. The double horizontal line in M_{distributed} splits the system into transitions that correspond to control variable PC_{i}, which are described above the line, and those that correspond to control variable PC_{S} which are below the line.

Four types of MW transitions are described instead of the single atomic MW(d, a) action of M_{distr}.

An MW_{i}(d, a)[1] transition is a pair of states (S_{1}, S_{2}) such that system control variable PC_{S} at S_{1} is MW[1], and queue Out_{i} is non-empty with its head having value (d, a). At state S_{2}, the control variable acquires value MW_{i}(d, a)[2] (indicating both the process index i, the data value d, and the address a of the operation). In addition S_{2}(Mem[a]) = d.

5. If PC_{S} is MW_{i}(d, a)[2] in a state, then a MW_{i}(d, a)[2] transition is enabled, and S_{2} is obtained by advancing PC_{S} to MW_{i}(d, a)[3] and enqueuing the triple (d, a, ∗) to In_{i}. Then (S_{1}, S_{2}) is an MW_{i}(d, a)[2] transition.

6. A MW_{i}(d, a)[3] transition is a pair of states (S_{1}, S_{2}) such that PC_{S} in S_{1} is MW_{i}(d, a)[3], and the only changes that lead to S_{2} are

(a) queue Out_{i} of S_{2} is obtained by dequeuing its S_{1} value, and

(b) PC_{S} acquires value MW_{i}(d, a)[X] in S_{2}, where X is the set of all process indices except i itself.

An MW_{i}(d, a)[4, k] transition is a pair of states (S_{2}, S_{2}) such that S_{1}(PC_{S}) = MW_{i}(d, a)[X] and k ∈ X, and the pair (d, a) is enqueued to S_{1}(In_{i}) to produce S_{2}(In_{i}). There are two possibilities: if X = {k}, then S_{2}(PC_{S}) is an initial value, but otherwise it is MW_{i}(d, a)[X \ {k}].

7. The role of value MW_{i}(d, a)[X] for control variable PC_{S} (where X is a non-empty set of indices), is to indicate that for every index k ∈ X the action of enqueuing the pair (d, a) into In_{k} is enabled. The total effect of actions MW_{i}(d, a)[4, k] is to enqueue (d, a) on all queues In_{k} for k ≠ i in any order, and to reset PC_{S} to an initial value when this is done.

8. Memory Read transitions, and Cache Invalidate transitions are defined similarly.

We thus have defined a formula τ(S_{1}, S_{2}, E) saying about states S_{1} and _{2} and about EventType E that transition S_{1}, S_{2}) is an E transition. If S is any state, we say that E ∈ EventType is “enabled” at S iff there exists a state S′ such that τ(S, S′, E).

Now three functions are added to σ_{0} to form σ: S_{1}, S_{2}, and Q. For every step s S_{1}(s) and S_{2}(s) are states, and Q(s) is in EventType. If s = t_{i}, then r = ⟨S_{1}(s), S_{2}(s)⟩ is the transition corresponding to s, and Q(s) in EventType is the type of r. A history of M = M_{distributed} is defined to be any expansion of M_{0} to σ (obtained by interpreting S_{1}, S_{2}, and Q) in which the following hold.

1. The first state S_{1}(t_{0}) is an initial state. Namely all queues are empty, the value of all Mem[a] addresses is d_{0}, and the value of all cache locations is ⊥. Instead of making this initial state assumption, a simpler correctness proof is obtained by asking that the first steps in the history are MW_{j}(d_{0}, a) events which write the initial value.

2. For every index i ∈ ω, S_{2}(t_{i}) = S_{1}(t_{i+1}).

3. For every index i ∈ ω, transition ⟨S_{1}(t_{i}), S_{2}(t_{i})⟩ is of type Q(t_{i}). (The formula specifying when a transition ⟨S_{1}, S_{2}⟩ is of type T ∈ EventType was specified in the Transition Definition 4.1 listed above.

4. The fairness requirement is that (with the possible exception of CI events) no EventType E can be enabled continuously (i.e., for some k, enabled in every S_{1}(t_{i}) for i ≥ k) without being taken (i.e. such that no transition t_{i} for i ≥ k is of type E).

The resulting histories are in fact system executions. In any history H, sort Step is the sort of events (all are terminating) and the precedence ordering is defined by t_{i} < t_{j} iff i < j. These events of H are said to be “lowerlevel” events to distinguish them from higher-level events introduced below in subsection 4.0.1.

Signature σ is extended, and further predicates and functions are defined on these lower-level events of H as follows. In general, if t is a step and Q(t) = E is the corresponding event type, then we say that t is an E step. (In definition 4.1 we defined when a transition is an E transition. Now we speak about transition occurrences, namely steps, and make the corresponding definition.)

1. If t is an event (a step) in our history H and Q(t) = R_{i}(d, a), then we say that t is an R_{i}(d, a) event and we define the following predicates and functions: read_{C_{i}[a]}(t) (viewing t as a lower-level read of cache location C_{i}[a]), P_{i}(t) (which says that t is in the ith process), Val(t) = d, and address(t) = a.

2. For every W_{i}(d, a) event t in history H (namely Q(t) = W_{i}(d, a)), the predicates and functions are defined naturally in a similar fashion as above: enqueue_{Out_{i}}(t), P_{i}(t), and Val(t) = (d, a).

3. Predicates and functions are defined on Cache Update lower-level events in a history. If t is a CU_{i}(d, a)[1] event in H (namely Q(t) = CU_{i}(d, a)[1]) then we define dequeue_{In_{i}}(t), and Val(t) = (d, a) or Val(t) = (d, a, ∗) in accordance with the value dequeued. If t is a CU_{i}(d, a)[2] event, we define write_{C_{i}[a]}(t), viewing t as a write event on location C_{i}[a] (with Val(t) = d).

4. If t is an MW_{i}(d, a)[1] event in a history, then t is a lower-level write event on location Mem[a] and so we define write_{Mem}(t) address(t) = a, and Val(t) = d (to indicate that t is a write on memory location Mem[a] with value d). We also write index(t) = i to show on behalf of which process this operation is executed (but t is not a P_{i} event).

5. If t is an MW_{i}(d, a)[2] step in a history H, then predicates and functions are defined on t as above. In particular, we define enqueue_{In_{i}}(t) in order to say that t is an enqueue event on In_{i} (of value Val(t) = (d, a, ∗)). Remark: in order to have fewer predicates, it is possible to have a predicate enqueue_{In}(t), to say that t is an enqueue event on some In queue, and then define index(t) = i to determine the queue.

6. If t is an MW_{i}(d, a)[3] step in H, then we define dequeue_{Out_{i}}(t) to say that t is a dequeue event, and Val(t) = (d, a) is the head value of S_{1}(Out_{i}).

7. Each MR_{i}(d, a) event is an enqueue event, and each CI_{i}(a) event is a write event, with values Val(t) defined appropriately..

To sum-up we have the following lower-level events:

List 4.2 (Lower-Level events) 1. write events: An execution of CU_{i}(d, a)[2] is a write event, on cache location C_{i}[a] and of value d.

An execution of MW_{i}(d, a)[1] is a write event, on memory location Mem[a] and of value d.

And an execution of CI_{i}(a) is a write event, on cache location C_{i}[a] and of value ⊥.

2. read events: An execution of R_{i}(d, a) is a read event of cache location C_{i}[a] of value d.

3. enqueue events: An execution of a W_{i}(d, a) event is an enqueue event, on queue Out_{i} of the pair (d, a).

An execution of a MW_{i}(d, a)[2] in an enqueue event, on queue In_{i} of value (d, a, ∗).

An execution of MW_{i}(d, a)[4, k] is an enqueue event, on queue In_{k} of value (d, a).

And an execution of MR_{i}(d, a) is an enqueue event, on queue In_{i} of value (d, a).

4. dequeue events: An execution of CU_{i}(d, a)[1] is a dequeue of In_{i}, obtaining (d, a) or (d, a, ∗).

And an execution of MW_{i}(d, a)[3] is a dequeue of Out_{i}, necessarily obtaining (d, a).

Every lower-level event appears in this list, and is either a read/write or an enqueue/dequeue event. This list is exhaustive in the sense that it lists all event types of H. It can be used to deduce for example that every write on Mem[a] is an MW_{i}(d, a) event for some d and i, or that every dequeue of Out_{i} is an MW_{i}(d, a)[3] event for some d and a. Notice however that there are three event types that are enqueues of In_{i}: MW_{i}(d, a)[2], MW_{j}(d, a)[4, i], and MR_{i}(d, a).

As in sections 2.2.1 and 2.3, functions Val, γ, and ω are used to describe the behavior of queues and registers (each of the memory and cache locations is a serial register). We add these (definable) functions to our history structures.

4.0.1 Higher-level view of the distributed Lazy Caching algorithm

If T is any system execution, and E is its sort of events, a higher-level event is a non-empty subset of E. The structure T can be extended by adding a new sort HL of higher-level events. So every X ∈ HL is a non-empty subset of E, and a membership predicate e ∈ X is added to the signature of T to express the relationship between events (lower-level events, namely members of E) and higher-level events.

When T contains each of its finite subsets (which is the case for our HF(U) structures), some higher-level events correspond to finite subsets of E, yet in many cases infinite higher-level events are also required (for representation of non-terminating events). In this case the infinite sets are not sets of HF(M), of course, but are special urelements that represent non-terminating events.

The temporal relation <_{T} on E is extended on HL events and the following definitions are made. For every higher-level events X and Y

X < Y iff ∀x ∈ X ∀y ∈ Y (x <_{T} y)  (5)

For every lower-level event e we also define

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

We add functions and predicates on higher-level events (see below), and the resulting structure is called a higher-level view (and we still denote it with T). Not all subsets of E are taken as higher-level events, only those that serve the correctness proof. In fact, the higher-level events that are added are definable in T. Namely, there exists a formula ϕ(x, y) that defines an equivalence relation on the sort of events in T, or on a subset of events, and the higher-level events are the resulting equivalence classes. These classes are pairwise disjoint, and any lower-level event x belongs to a unique higher-level event denoted [x].

Leaving the general discussion, let H be a history structure of M_{distributed}. Our aim is to add higher-level events to H (the resulting structure is still denoted H.) Consider a MemoryWrite operation execution. It consists of N + 2 events: an MW_{i}(d, a)[1] event followed by MW_{i}(d, a)[2], MW_{i}(d, a)[3], and then by N −1 MW_{i}(d, a)[4, k] events for k ≠ i. Whereas in executions of M_{distr} an MW event is a single atomic event, here the N + 2 sub-events are arbitrarily interleaved with events from other processes. The simplicity afforded by atomicity of the events is lost here, but it is counterbalanced by formation of compound, higher-level events. We assemble these dispersed N + 2 events into a single entity, called a higher-level MW_{i}(d, a) event, and we investigate abstract properties of these events in the resulting system execution.

Formally, define a relation ∼_{MW} on Memory Write sub-events in H: a ∼_{MW} b iff both a and b are MW_{i}(d, a)[p] events for some i, d, and parameter p ∈ {1, 2, 3, (4, k)}, and there is no MW_{i′}(d′, a′)[1] event e such that (in case a <_{H} b) a <_{H} e ≤_{H} b. In simpler words, a ∼_{MW} b iff a and b belong to the same execution of an MW operation (there is no beginning of another operation in between). Clearly a ∼_{MW} b is an equivalence relation on its domain. All equivalence classes of this relation are assembled to form higher-level MW events.

In a similar vein CU(d, a) (CacheUpdate) events are formed, consisting each of two lower-level events. It may seem trivial, but we also form higher-level events that are singletons. For example if r is an R_{i}(d, a) event, then we form R = {r} as a higher-level Read event. This is done for uniformity, so that at a later stage of the proof it will be simpler to collect all higher-level events and to prove that they satisfy the Caching Axioms. Similarly, we define Write, MemoryRead, and CacheInvalidate higher-level events. The resulting structure is still denoted H. Every higher-level event in H is a non-empty set of lower-level events, and different higher-level events are disjoint subsets. Every lower-level event x belongs to a unique higher-level event X and we write X = [x] (for the appropriate equivalence class of x).

The following lists six types of higher-level events that are added to H, and associated additional functions and predicates defined over them.

List 4.3 (Types of Higher-Level Events) 1. If X is a higher-level R_{i}(d, a) event then X is a singleton of the form X = {r} where r is a lowerlevel R_{i}(d, a) event (this r is denoted r_{X}). We define the following additional predicates: Read(X), P_{i}(X), and the functions: index(X) = i, Val(X) = d, and address(X) = a.

2. If X is a higher-level W_{i}(d, a) event then X is a singleton of the form X = {e_{X}} where e_{X} is a lower-level W_{i}(d, a) event. We have also defined enqueue_{Out_{i}}(e_{X}) to say that e_{X} is an enqueue event of queue Out_{i}. We can also write enqueue(e_{X}) and say that e_{X} is an enqueue on Out_{i} event, in an informal discussion. Additional predicates are defined: Write(X) and P_{i}(X), and functions: index(X) = i, Val(X) = d ∈ Data, and address(X) = a. We say that X is a W_{i} event if it is a W_{i}(d, a) event for some d and a.

3. If X is a CU_{i}(d, a) higher-level event (and we also say then that it is a CU event) then it has the form X = {d_{X}, w_{X}} where d_{X} <_{H} w_{X} are its two lower-level elements, a dequeue of In_{i} and a write of d on C_{i}[a]. We define CacheUpdate(X), P_{i}(X), and functions index(X) = i, Val(X) = d, and address(X) = a.

4. If X is an MW_{i}(d, a) higher-level event (and we say then that it is a MW event) then it has the form X = {w_{X}, e_{X}^{∗}, d_{X}} ∪ {e_{X}^{k} | k ≠ i}, where w_{X} <_{H} e_{X}^{∗} <_{H} d_{X} <_{H} e_{X}^{k} are (respectively) a write on Mem[a] of d, an enqueue of (d, a, ∗) on In_{i}, a dequeue of Out_{i}, and a series of enqueue events of value (d, a) on the In_{k} queues for every k ≠ i.

We define the predicate MemoryWrite(X), and the functions index(X) = i, Val(X) = d, and address(X) = a. Note that although index(X) = i, X is not in P_{i}. It is a Memory Write event done on behalf of a Write in P_{i}.

5. If X is a higher-level MR_{i}(d, a) event (and we say then that it is a MR event) then it is a singleton X = {e_{X}} where e_{X} is a lower-level enqueue event on In_{i} of value (d, a). We define MemoryRead(X), index(X) = i, Val(X) = d, and address(X) = a.

6. If X is a CI_{i}(a) higher-level event then it is a singleton X = {w_{X}} where w_{X} is a write on C_{i}[a] of value ⊥. We define CacheInvalidate(X), index(X) = i, and address(X) = a.

Note that the higher-level events in P_{i} (Read, Write, and CacheUpdate) are linearly ordered under <. We also denote the restriction of < to P_{i} by <_{i}. The higher-level system events in H (Memory Write, Memory Read, and Cache Invalidate) are linearly ordered under <, and we also use the symbol ≺, as in M_{0} ≺ M_{1} instead of M_{0} < M_{1}, for Memory Write events. The reason for this linearity is the behavior of the control variables. For example, if PC_{S} indicates that a Memory Write event is executing, then no MR or CI can begin. Yet events by P_{i} can interleave with events by P_{j} (for i ≠ j) and with system events. Some simple properties will be useful in our proof. They are all derived from list 4.2 of Lower-Level events.

List 4.4 (Simple Properties) 1. Every enqueue event on Out_{i} belongs to some higher-level W_{i} event.

2. Every write on Mem belongs to some MW event.

3. Every enqueue on In_{i} belongs either to some MW event or to some MR_{i} event.

4. Every dequeue event of Out_{i} belongs to some MW_{i} event.

5. Every dequeue event of In_{i}, and every Data write on a C_{i} location belong to some CU_{i} event. Writes on a C_{i} location of ⊥ belong to CI_{i} events.

The Lazy Caching algorithm has conditions that enable actions. Following Definition 4.1, we have defined what it means that a transition is enabled at state S. For example, an R_{i}(d, a) transition is allowed at state S only if state S satisfies the “Allowed if” pre-condition: Out_{i} is empty, In_{i} is starless, and C_{i}[a] = d. Here, we move from states to events with properties, and hence the pre-conditions are translated into statements about executions.

List 4.5 (“Allowed if” conditions on higher-level events) 1. If X is a R_{i}(d, a) event, then

(a) For every enqueue event e on Out_{i} such that e < X, there exists a dequeue event d on Out_{i} such that γ(d) = e and d < X.

(b) For every enqueue event e on In_{i} of a star triple (d, a, ∗) such that e < X, there exists a dequeue event dq such that γ(dq) = e and dq < X.

2. Recall that we assumed initial write events in H. So, if X is a MR_{i} event on address a, then it is preceded by some (initial) MemoryWrite event MW_{j} on address a (which contains a write on Mem[a]). The pre-condition Mem[a] = d that enables any MR_{i}(d, a) event translates into the demand that if X is a MR_{i}(d, a) event and if we define w as the <-last write on Mem[a] such that w < X, then Val(w) = d.

3. If M is a MemoryWrite event of index i, if w_{M} < d_{M} are its write and its dequeue of Out_{i} events, then γ(d_{M}) < w_{M}.

We prove item 3 as an example. Let M be a MemoryWrite event of index i, and let w_{M} and d_{M} be the write and dequeue events in M. Then for some parameters (d, a), w_{M} is an MW_{i}(d, a)[1] event and d_{M} is the subsequent MW_{i}(d, a)[3] event. Let S = S_{1}(w_{M}) be the first state of w_{M} in history H. Then Out_{i} is non-empty in S and its head value is the pair (d, a) (check item 4 in Definition 4.1 where this transition type is defined). Since every dequeue of Out_{i} is in some MW_{i} event, d_{M} is the earliest dequeue_{Out_{i}} transition after S_{j}. It follows from Lemma 2.4 that γ(d_{M}) is an enqueue transition that precedes w_{M}. Fairness Property. For every enqueue event e on Out_{i} there exists a dequeue event d_{M} (in some MW_{i} event M) such that γ(d_{M}) = e. Since d_{M} is a dequeue of Out_{i}, it follows that index(M) = i.

This property is a restriction on the system in the ways that it invokes the Memory Write operations: it must attend every Out_{i} queue. Seriality Property. Every P_{i} is serial. That is any two higher-level Read, Write, or CacheUpdate events are < comparable. Similarly, system is serial. That is any two Memory-Write, MemoryRead, and CacheInvalidate events are < comparable.

The next step in the definition of the higher-level view H consists in defining a function μ which associates to every higher-level Write, MemoryRead, CacheUpdate, and Read event X a MemoryWrite event μ(X).

First, let W be any Write event. Suppose that predicate W_{i}(d, a) applies to W. Then W = {e_{W} }, where e_{W} is an enqueue event on Out_{i} of the pair (d, a). By the Fairness Property, there exists a dequeue event d_{M} such that e_{W} = γ(d_{M}) where M (the higher-level event containing d_{M}, namely [d_{M}]) is some MW_{i}(d, a) event. We define μ(W) = M. Clearly Val(M) = Val(W), address(M) = address(W), and index(M) = index(W).

We claim that if M = μ(W) then

e_{W} < w_{M},  (7)

where w_{M} is the write on Mem in M. Indeed, by property 3 of the Allowed if conditions 4.5, γ(d_{M}) < w_{M}. But γ(d_{M}) = e_{W} and hence e_{W} < w_{M} < d_{M} follows.

Now let X be some MemoryRead event of index i. That is, predicate MR_{i}(d, a) holds for X for some d and a. Then, by condition 2 of 4.5, the rightmost write w on Mem[a] such that w < X exists and has value d. As any write on Mem[a], w belongs to some (uniquely determined) MemoryWrite event M, and we define μ(X) = M. Clearly

M = μ(X) < X,  (8)

because Seriality Property implies that the alternative is X ≤ M which contradicts w < X.

Next, let C = {d_{C}, w_{C}} be a CacheUpdate event of index i. Then d_{C} is a dequeue of In_{i} of either a pair (d, a) or a triple (d, a, ∗). Let γ(d_{C}) be the corresponding enqueue on In_{i}. According to item 3 in the list of Simple Properties 4.4 there are two possibilities:

1. γ(d_{C}) belongs to some uniquely determined MemoryWrite event M, and we define μ(C) = M.

2. γ(d_{C}) belongs to some MR_{i} event X, and we define μ(C) = μ(X).

In any case w_{M} < C (where w_{M} is the write on Mem in μ(C)). Clearly, C and μ(C) have the same value and address.

Before defining μ on Read events, we define an auxiliary function cu on Read events which returns Cache Update events. Let R = {r} be some R_{i}(d, a) event.

Then r is a read and ω(r) is the corresponding write on cache location C_{i}[a], both of value d ∈ Data. For any Data write on C_{i}[a], and hence for ω(r), there exists a CacheUpdate event C such that ω(r) ∈ C. Since distinct higher-level events are disjoint, C is uniquely defined and we define C = cu(R). Since ω(r) < r and as C = {d_{C}, ω(r)} (where ω(r) = w_{C} so that d_{C} < ω(r)),

cu(R) < R.  (9)

Now for every Read event R we can define μ(R) = μ(cu(R)). It follows that if M = μ(R), then

w_{M} < R.  (10)

4.1 Correctness of the distributed Lazy Caching algorithm

Theorem 4.6 Let H be a history of M_{distributed} and augmented with higherlevel events, predicates and functions as above. Then the higher-level events satisfy all Caching Axioms of 3.2 and hence the sequential consistency property.

The proof is given in this section. Axioms 1 to 5 of the Caching list of 3.2 are very easy to prove. Axiom 6 is also an easy consequence of the order-preserving property of γ. If V <_{i} W are Write events in P_{i}, then e_{V} < e_{W} are both enqueue on Out_{i}. So if d_{1} and d_{2} are the dequeue events such that γ(d_{1}) = e_{V} and γ(d_{2}) = e_{W}, then d_{1} < d_{2}. It follows now immediately that μ(V) < μ(W).

We prove item 7 of the Caching Axioms:

Lemma 4.7 If R is a Read and W = {e_{W} } a Write events, both are in P_{i} and R <_{i} W, then μ(R) ≺ μ(W).

Proof. Let M = μ(R), N = μ(W). Then w_{M} < R was concluded above in (10).

Since N = μ(W), e_{W} < w_{N} as concluded in (7). Hence w_{M} < e_{W} < w_{N}. So w_{M} < w_{N}, and hence M < N. Q.E.D.

Lemma 4.8 If C_{1} <_{i} C_{2} are Cache Updates in P_{i} of the same address a, then μ(C_{1}) ⪯ μ(C_{2}).

Proof. Let d_{1} ∈ C_{1} and d_{2} ∈ C_{2} be the dequeues of In_{i}. Then d_{1} < d_{2}, and hence γ(d_{1}) < γ(d_{2}) (by remark 2 in 2.2.1. There are four possibilities concerning the definitions of M = μ(C_{1}) and N = μ(C_{2}):

1. Both γ(d_{1}) and γ(d_{2}) belong to Memory Write events M = μ(C_{1}) and N = μ(C_{2}) respectively. Then M ≺ N is easily inferred from the order preservation of γ.

2. Both γ(d_{1}) and γ(d_{2}) belong to MemoryRead events Mr_{1} and Mr_{2} respectively. Then Mr_{1} < Mr_{2}. Since M = μ(Mr_{1}) and N = μ(Mr_{2}) a short argument yields that μ(C_{1}) ⪯ μ(C_{2}).

3. Suppose that γ(d_{1}) belongs to MemoryWrite M = μ(C_{1}), and γ(d_{2}) belongs to some MR_{i} event Mr. Then M < Mr (by Seriality Property of the system, which includes Memory Read and Memory Write events). If w_{M} is the write on Mem[a] in M, then w_{M} < Mr, and thus M ⪯ μ(Mr) is concluded. (Recall that in defining μ(Mr), we looked for the rightmost write w on Mem[a] such that w < Mr, and so w_{M} ≤ w implies our conclusion.) But μ(C_{2}) = μ(Mr) by definition of μ(C_{2}).

4. Suppose that γ(d_{1}) belongs to some MR_{i} event Mr, and γ(d_{2}) ∈ N. Then Mr < N. But μ(Mr) < Mr (by 8), and hence M < N.

Q.E.D.

Next we prove property L5.

Lemma 4.9 If C <_{i} R are a CacheUpdate and a Read in P_{i}, and the address of R is the address of C, then μ(C) ⪯ μ(R). (Remark that in our protocol C <_{i} R and C <_{i} end(R) are equivalent.)

Proof. Let w_{C} be the write on C_{i}[a] in a CU_{i}(d, a) event C, and let r ∈ R be the read of C_{i}[a] in R, where C <_{i} R. Then w_{C} < r implies that w_{C} ≤ ω(r). Hence C ≤ cu(R). By the previous lemma, μ(C) ⪯ μ(cu(R)). That is, μ(C) ⪯ μ(R), as required. Q.E.D.

Next we prove property L2.

Lemma 4.10 If R_{0} <_{i} R_{1} are Reads in P_{i} of the same address, then μ(R_{0}) ⪯ μ(R_{1}).

Proof. If R_{0} <_{i} R_{1} are Reads in P_{i} of address a, then cu(R_{0}) ≤_{i} cu(R_{1}) (is easily obtained) and by Lemma 4.8 μ(cu(R_{0})) ⪯ μ(cu(R_{1})), namely μ(R_{0}) ⪯ μ(R_{1}). Q.E.D.

The following proves L3:

Lemma 4.11 If M_{0} is a MemoryWrite event and C a CacheUpdate event and M_{0} ≺ μ(C), then there exists a CacheUpdate event C_{0} <_{i} C such that μ(C_{0}) = M_{0}.

Proof. Suppose that M_{0} ≺ μ(C) = M_{1}. There are two possibilities in the definition of μ(C).

1. γ(d_{C}) ∈ M_{1}. Let e_{0} ∈ M_{0} be the enqueue on In_{i}. Then e_{0} < γ(d_{C}) (since M_{0} ≺ M_{1}). Since the range of γ is an initial segment of enqueue events (item 3 of section 2.2.1) it follows that e_{0} = γ(d_{0}) for some dequeue d_{0} < d_{C} of In_{i}. It follows from the list of lower-level events 4.2 that dequeues of In_{i} are only in CU_{i} events, and so the lemma can be concluded in this case.

2. γ(d_{C}) belongs to some MR_{i}(d, a) event Mr. In this case, if w < Mr is the rightmost write on Mem[a] that precedes Mr then w has value d and w ∈ μ(C) = μ(Mr), by definition of μ, and μ(Mr) < Mr by (8). Since M_{0} ≺ μ(C), M_{0} < Mr. Hence, if e ∈ M_{0} is the enqueue on In_{i} there, then e = γ(d_{0}) for some dequeue event d_{0} < d_{C}. Since dequeues of In_{i} are in Cache Update events by P_{i}, d_{0} ∈ C_{0} for some CacheUpdate event C_{0} <_{i} C. Thus μ(C_{0}) = M_{0} is as required. Q.E.D.

The following is L4.

Lemma 4.12 If U ∈ P_{i} is a Read/Write event and R a Read event in P_{i} such that U <_{i} R, then there exists a CacheUpdate event C in P_{i} such that C <_{i} R and μ(C) = μ(U).

Proof. If U is a Read, then C = cu(U) < U is the required CU_{i} event such that μ(C) = μ(U) and C < R (see equation 9).

If U is a Write let e_{U} ∈ U be the enqueue event on Out_{i}. Then e_{U} < R and Allowed if condition 4.5 1(a) gives a dequeue event d on Out_{i} such that d < R and γ(d) = e_{U}. Dequeues of Out_{i} are in MW_{i} events, and so there exists a MemoryWrite events M such that d ∈ M. If follows that M = μ(U). Let e_{M}^{∗} ∈ M be the enqueue on In_{i} of triple (d, a, ∗) (where M is an MW_{i}(d, a) event). Then e_{M}^{∗} < d_{M} = d < R. So Allowed if condition 1(b) applies to e_{M}^{∗} < R, and there exists a dequeue event dq (on In_{i}) such that γ(dq) = e_{M}^{∗} and dq < R. All dequeue events on In_{i} belong to CU_{i} events, and so there exists a CU_{i} event C with dq ∈ C. As C is in P_{i}, seriality of P_{i} implies that C < R. Since γ(dq) = e_{M}^{∗}, μ(C) = M follows the definition of μ. So C is as required. Q.E.D.

Now L1 can also be concluded. If W <_{i} R are a Write and a Read in P_{i}, both of address a, then the previous lemma implies that there exists a CacheUpdate event C in P_{i} such that C <_{i} R and μ(C) = μ(W). But C <_{i} R and Lemma 4.9 imply that μ(C) ⪯ μ(R), and hence μ(W) ⪯ μ(R) as required. Q.E.D.

This concludes the proof of the Caching Axioms and hence of sequential consistency for the Lazy Caching algorithm. We observe that it is possible that no R_{i} event is ever enabled in some history of M_{distributed} (if W_{i} events continuously fill-up Out_{i}). In the following algorithm it will be clearer that whenever a Read is requested by P_{i}, Writes by P_{i} are prevented and then Memory Read and Cache Update operations finally enable the Read.

5 Lazy Readers

This section describes the second variant of the Lazy Caching algorithm, called Lazy Readers algorithm (see figures 4 and 5).

The Lazy Caching algorithm pushes data values to the local processes P_{i}, making them available when needed. In our second variant Lazy readers pull data from main memory to their caches only when needed. Though this change makes sense when data values are very large, it is not claimed that it is an improvement, since each of the algorithms has its advantages. It is interesting though to see how the two variants share the same higher-level properties, and how these properties enable in a very formal way to express the similarity of these two algorithms. algorithm: Lazy Readers

concurrently do

P_{1}, …, L_{N}, MemoryWriter, CacheInvalidator.

Figure 4: General form of the Lazy Readers algorithm.

5.1 The Lazy Readers algorithm

The Lazy Readers algorithm is not described by a transition diagram but by a program that concurrently activates N + 2 processes: P_{i} for i = 1, …, N, and two “system” processes MemoryWriter, and CacheInvalidator (see Figure 4.)

The algorithm is presented in Figure 5 by seven small programs which we describe informally first. A program that corresponds to one of the independent N + 2 processes is called here a “procedure”, and a sub-procedure is a program that is invoked by procedure P_{i}.

1. Each P_{i} repeatedly cycles the following operations. It decides the value of r ∈ {R, W, CU}, a variable which tells whether the next operation is a Read (if r = R), a Write (if r = W), or a cache Update (if r = CU). It also decides the data value d and address a that are used by the Write operation and the Read (which uses a and may return any data value). Formally, decide(r, d, a) is just some external operation that determines the values of r, d, and a. For simplicity we assume that it is always terminating (expressing the situation in which the client of P_{i} accesses infinitely often Read and Write operations). If r = R, then sub-procedure Read with parameter a is executed by P_{i}. If r = W then Write is executed with parameters d and a.

Notice that higher-level events Read, Write, and CacheUpdate invoked by P_{i} are serially ordered. This follows from the form of P_{i} which invokes its sub-procedures serially.

2. Sub-procedure Read(a), where a is an address begins with two “wait” operations.

(a) wait-for-empty-Out is some externally supplied operation. That is, we assume its existence (without writing its text), but we shall specify its behavior formally. It suffices to say now that it may be nonterminating, and that, intuitively, termination indicates that Out (necessarily Out_{i}, if executed by P_{i}) is empty.

(b) Then sub-procedure wait-for-starless-In is invoked. (See item 7 below for more details on this procedure.) If and when that procedure returns, P_{i} can be sure that In_{i} contains no ∗. (A more accurate description is given later.) 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. sub-procedure Read(a) (by P_{i})

1. wait-for-empty-Out;

2. wait-for-starless-In;

3. c := C_{i}[a];

4. if c =⊥ c := Mem[a]; In_{i}.Enq(∗); C_{i}[a] := c;

sub-procedure Write(d, a) (by P_{i})

1. Out_{i}.Enq((d, a));

2. C_{i}[a] := d. procedure MemoryWriter repeat forever

1. decide(i);

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

3. Mem[a] := d;

4. In_{i}.Enq(∗);

5. Out_{i}.Deq();

6. forall k ≠ i In_{k}.Enq(a);

sub-procedure CacheUpdate (by P_{i})

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

2. if x ∈ Addresses C_{i}[x] :=⊥. procedure CacheInvalidator

concurrently  for i ∈ {1, …, N}

repeat forever 1. decide_{i}(a);

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

sub-procedure wait-for-starless-In ( by P_{i} )

1. k := number-of-asterisks-in-In_{i};

2. repeat

CacheUpdate until (k asterisks were dequeued)

Initially all queues are empty, and all C_{i}[a] locations are ⊥. For some initial Data value d_{0}, we assume an initial MemoryWrite event which is an execution of the following code: forall a ∈ Addresses Mem[a] := d_{0}.

Figure 5: Lazy Readers algorithm.

We say that the executions of wait-for-empty-Out and wait-for-starless-In of a Read event R “prepare” R. Then the Read checks the content c of C_{i}[a]. If it is a Data value, then this is the value of the Read operation, but otherwise (if it is ⊥) memory location Mem[a] is read directly into variable c, an asterisk is enqueued into In_{i}, and then value c obtained from Mem[a] is copied into C_{i}[a]. The value of the Read operation is defined in this case to be the value that was read from Mem[a].

We shall prove that the executions of the wait operations connected to lines 1 and 2 always terminate. It then follows that a Read always terminates since read/write events on every memory and cache locations terminate and since enqueue events always terminate. The Read is a “hit” if value c obtained in executing line 1 (reading C_{i}[a]) is a Data value, or a “miss” if that value is ⊥ and then the read continues and reads its value from Mem[a].

In case a Read execution R is a hit, the read of C_{i}[a] in R (returning a data value) is said to be the decisive read, but otherwise it is the read of Mem[a] that is called the decisive read.

3. Procedure Write (by P_{i}) needs two parameters, Data d, and Addresses a. It enqueues the pair (d, a) into Out_{i}, and it then writes d into local cache C_{i} at address a. A Write operation execution is always terminating.

4. MemoryWriter executes for-ever Memory Write operations. Each such operation consists of the following instructions executed in order.

(a) Decide which index to use. An execution of decide(i) can be nonterminating (if all Out_{k} queues are permanently empty). In this case the MemoryWrite operation is said to be non-terminating. If decide(i) returns, then the value of variable i is such that Out_{i} is non-empty. This value of i is called the “index decided” by the Memory Write execution.

(b) Hence Out_{i}.peek() returns a pair, which is assigned to (d, a).

(c) Then d is written to main memory, at location Mem[a].

(d) Asterisk is enqueued into In_{i} (same i decided in (a)).

(e) Only now Out_{i} is dequeued and (d, a) removed.

(f) Finally, address a is enqueued into In_{k} for every k ≠ i (in any order).

There is also an initial MemoryWrite operation which is not connected with any particular P_{i}. In this operation an initial Data value d_{0} is assigned to all memory locations Mem[a]. This initialization event is assumed to occur before any other event.

5. Sub-procedure CacheUpdate is invoked directly by P_{i} (when r = CU is decided) and also indirectly by the wait-for-starless-In procedure of P_{i} which precedes every Read by P_{i}. It is necessary that Cache Updater is cautious, namely that whenever CacheUpdate is invoked (directly or indirectly) queue In_{i} is non-empty, and hence instruction x := In_{i}.Deq() returns a value. This value can either be an address or ∗. If it is an address a, then cache location C_{i}[a] is invalidated.

6. For every index i procedure CacheInvalidator executes Cache Invalidate operations repeatedly. Each such operation consists of:

(a) A call to procedure decide_{i}(a) which returns (if it terminates) with some address a for cache C_{i}, and then

(b) cache C_{i} at address a is invalidated.

For every index i, we think of CacheInvalidator operations with index i as being local to P_{i} (since they invalidate only C_{i} locations). By writing the CacheInvalidator as a separate procedure, we emphasize that Cache Invalidate operations on C_{i} are allowed to be concurrent with Read/Write and Cache Update events on different locations. Allowed, but not forced to. This flexibility is sometimes mistaken to be a burden on the implementor who has to build a separate, concurrently working, process. The truth is that implementors are not obliged to build CacheInvalidator as a separate process; they can incorporated it with each P_{i}. If this is done, then P_{i} decides four values for r in its decide(r, d, a) operation, namely the possibility r = CI is added.

7. Sub-procedure wait-for-starless-In is invoked by P_{i}. The first step records in k the number of asterisks that are present in queue In_{i} (k can be 0). If k > 0, then CacheUpdate operations are executed repeatedly, each one dequeuing one item from In_{i}, until all k asterisks were dequeued (along with addresses that had to be dequeued as well by the FIFO regime). It is possible that by the time procedure wait-for-starless-In has terminated, additional asterisks were enqueued in In_{i} (which is a concurrent queue). However, it must terminate, and it must dequeue all k asterisks that were present beforehand in In_{i}.

Observe that we have no MemoryReader procedure here. This is for simplicity and since Memory Read operations are not strictly necessary for our algorithm. Indeed a Read operation that is a miss accesses main memory directly. A Memory Read operation could be introduced, but not much new would then be learned and the shorter algorithm suits our needs.

Now we spell out concurrency limitations that are required for the correctness of the algorithm.

List 5.1 (Concurrency Limitations)

1. For every address a accesses to location Mem[a] are required to be mutually exclusive and to satisfy the requirements for read/write seriality (see section 2.2). These accesses are present in line 2 of Read, and in line 3 of MemoryWriter. Distinct memory addresses can be accessed concurrently.

2. For every address a, and index i, accesses to cache location C_{i}[a] are required to be mutually exclusive and to satisfy the requirements for read/write seriality. These accesses are present in lines 1 and 2 of Read, line 2 of Write, line 2 of CacheUpdate, and line 2 of CacheInvalidator.

3. The operations on each of the queues are required to satisfy the queue specifications (see section 2.2). Implicitly, these specifications imply that the queues are initially empty (because for every dequeue event d, γ(d) is the corresponding enqueue, there are no dequeues whose justification is some initial value). Observe that queue In_{i} is accessed for Enq operations both by the Read and by the MemoryWrite procedures. We assume some mutual-exclusion mechanism to ensure that these accesses are serially ordered.

There are no other concurrency limitations and there is no need to further synchronize the processes. For example, P_{i} can read its cache C_{i} while a Memory Write operation access In_{i} and some P_{j} executes a Write operation.

For fairness, we assume that each of the N + 2 processes executes an infinite number of instructions, unless it halts because of some nonterminating operation. But we will prove that all operation executions (excepting Cache invalidates) are terminating. We will also formulate a fairness requirement to ensure that every enqueue on Out_{i} (by some Write operation) is finally dequeued (by some MemoryWrite operation).

We shall prove that the distributed Lazy Readers algorithm satisfies the Caching axioms of section 3.2, and is thence sequentially consistent. However there is some preparation before we can access the actual proof. First the semantics of our algorithm is defined in Section 6, and only then the correctness proof is given in section 7.

6 Semantics of distributed algorithms

Our plan is to define the semantics of the Lazy Readers algorithm with system executions replacing global states and histories. This follows a rather general approach described in Chapter 3 of [1], and here we apply it to our algorithm as an example. Describing the semantics consists of three main steps: defining flowcharts, defining unrestricted semantics, and finally incorporating the specification of the communication devices and completing the definition. After that last stage we will be ready to prove the correctness of our algorithm.

6.1 Flowcharts

A flowchart is a directed graph, the nodes of which represent primitive instructions, and its edges (or “arrows”) represent transitions. It is a transition diagram, but for a single serial process. When K processes acts concurrently, K flowcharts describe the activity of each process and a system execution combines these activities (as we shall see) with the specification of the communication devices. The flowchart of the P_{i} program is described in Figure 6. It is selfexplanatory and we only say a few remarks (more is said when the transitions will be described). There are two types of nodes:

1. instruction-tagged nodes (rectangular nodes here) such as the initial node n_{1}^{p} tagged with the decide(r, d, a) instruction. A single arrow leaves an instruction node to the next node.

2. Conditional nodes containing a condition that determines the arrow through which the computation continues. For example, node n_{2}^{p} checks the value of variable r and chooses the arrow (R, W, or CU) of its value to lead to the next instruction.

Notice that node n_{4}^{p} (tagged with “wait-for-starless-In_{i}”) is in fact an invocation of this procedure, and it should be completed by an appropriate flowchart (which involves a repeat-until instruction).

The Lazy Readers algorithm is composed of N + 2 flowcharts: N flowcharts for processes P_{1}, …, P_{N}, and two additional flowcharts, one for MemoryWriter and the second for CacheInvalidator. The reader will easily complete the remaining flowcharts (for MemoryWriter, and CacheInvalidator), and expand the wait-for-starless-In node into its flowchart.

Flowcharts are graphical representations of a “machine language” translation of the program, and nodes correspond to unique primitive instructions. The role of a serial flowchart is to determine the transitions (by which the semantics of the process is described), and its nodes serve as values for the “location variable”. In general, line numbers of an algorithm (of Figure 5 for example) cannot serve for this purpose, because a single line can relate to several primitive instructions (e.g. a conditional if-else instruction). However, in informal discussions it may be convenient to use the line numbers instead of the corresponding flowchart nodes.

6.2 States and transitions

Let X be one of the N + 2 serial flowcharts defined for our processes. Let V(X) be the set of local variables of X, that is those that appear on the nodes of X. For example, if X is the flowchart of P_{i} of Figure 6 then V(X) = {r, d, a, c, x}. Each variable has its type. Here, r ∈ {R, W, CU}, d ∈ Data, a ∈ Addresses, c ∈ Data ∪ {⊥}, x ∈ Addresses ∪ {∗}. Observe that communication devices and shared variables are not in V(X). So Out_{i}, In_{i}, C_{i}, C_{i}[a], Mem, Mem[a] are not local variables. Yet every communication device and shared variable has its type, and it supports operations with that type. Thus a read of cache location c := C_{i}[a] on n_{5}^{p} requires a parameter a in Addresses and a variable c to receive values in Data ∪ {⊥}. A write on cache has the form C_{i}[a] := v where a ∈ Addresses and v is a term with value in Data ∪ {⊥}. Mem locations require Data values. So a read has the form f := Mem[a] where f is a variable of type Data (or a larger type) and a ∈ Addresses. A write has the form Mem[a] := v where a ∈ Addresses, and v is a Data term. Operations on queue also have their

[figure: wait-for-empty-; Out_{i}; decide(r, d, a); Out_{i}.Enq(d, a); C_{i}[a] := d; T; F; T; c := C_{i}[a]; n_{1}^{p}; F; x ∈; CU; r =; n_{14}^{p}; .; wait-for-starless-; In_{i}; n_{13}^{p}; n_{11}^{p}; n_{12}^{p}; Addresses; x := In_{i}.Deq(); n_{8}^{p}; c ∈ Data; c := Mem[a]; C_{i}[x] :=⊥; n_{3}^{p}; n_{4}^{p}; n_{5}^{p}; n_{6}^{p}; n_{7}^{p}; W; P_{1}; C_{i}[a] := c; n_{9}^{p}; n_{2}^{p}; n_{10}^{p}; R; In_{i}.Enq(∗); .]

Figure 6: Flowchart of p = P_{i}, incorporating the Read and Write flowcharts, but not the wait-for-starless-In flowchart.

types. The type of Enq and Deq on In_{i} is Addresses∪{∗}. There is an operation denoted number-of-asterisks-in-In_{i} that returns natural numbers. Enq, Deq, and peek operations on Out_{i} have type (Data, Addresses). For example, an execution of (d, a) := Out_{i}.peek() is a transition that assigns to variables d and a values in Data and Addresses respectively.

Let locations(X) be the set of nodes of X. For X the P_{i} flowchart,

locations(X) = {n_{1}^{p}, …, n_{14}^{p}}

where p is P_{i}. Let C_{X} be a “location variable” for X. We assume that C_{X} ∉ V(X). C_{X} varies over locations(X).

A regular state over X is a function S that assigns to each variable v ∈ V(X) a value S(v) in the type of v, and to C_{X} some node in X (that is S(C_{X}) ∈ locations(X)). Besides regular states, we define “unreachable” states as functions S that are defined only on C_{X}, with values in locations(X).

A regular state S over X represents the situation when the instruction on S(C_{X}) is about to be executed, with the values of all variables of X 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 X 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(C_{X}).

A relation =_{C}, “equality except for control variable”, is defined on the states: if S_{0} and S_{1} are regular X states then we write

S_{0} =_{C} S_{1} iff for every variable v ∈ V(X), S_{0}(v) = S_{1}(v) (it is possible that S_{0}(C_{X}) ≠ S_{1}(C_{X})).

Certain regular states are defined to be initial states. If S is an initial state then S(C_{X}) is the initial node of X. (In figure 6 the initial node is marked with an isolated arrow leading to it.)

We have only local states, that is states of serial processes corresponding to one of the serial flowcharts. Global states shall not be defined. Global states are appropriate for an interleaving semantics, which is not what we discuss here.

Now we define transitions over X, which represent executions of instructions of X. A pair of states over X, t = (S_{0}, S_{1}), is a transition if ⟨S_{0}(C_{X}), S_{1}(C_{X})⟩ is a directed edge of X and the transition represents an execution of the instruction tagged at node S_{0}(C_{X}). State S_{0} must be a regular state. If S_{1} is also regular then the transition t is said to be terminating, but if S_{1} is unreachable then t is said to be non-terminating. For example, for X the flowchart of P_{i}, we have the following transitions. Let t = (S_{0}, S_{1}) be a pair of states over X.

1. t is said to be a transition (by P_{i}) that decides r, d, a if the following holds. S_{0}(C_{X}) = n_{1}^{p}, S_{1}(C_{X}) = n_{2}^{p} (where p is P_{i}), and S_{1} is a regular state. The value Val(t) of this transition is the triple: S_{1}(r) ∈ {R, W, CU}, S_{1}(d) ∈ Data, S_{1}(a) ∈ Addresses.

2. t is a conditional transition corresponding to n_{2}^{p} if it is terminating, S_{0}(C_{X}) = n_{2}^{p} and there are three possibilities.

(a) S_{0}(r) is R and S_{1}(C_{X}) = n_{3}^{p}.

(b) S_{0}(r) is W and S_{1}(C_{X}) = n_{10}^{p}.

(c) S_{0}(r) is CU and S_{1}(C_{X}) = n_{12}^{p}.

In any case, S_{0} =_{C} S_{1}.

3. If S_{0}(C_{X}) = n_{3}^{p} and S_{1}(C_{X}) = n_{4}^{p} then t is a wait-for-empty-Out_{i} transition, and it can be of two kinds:

(a) t is terminating if S_{1} is a terminating state, and S_{0} =_{C} S_{1}.

(b) t is non-terminating (S_{1} is an unreachable state).

Recall that Out_{i} is not a variable in V(X); no global queue or communication device is a variable in our local flowcharts, and the states have no “access” to these devices.

4. A transition t is a wait-for-starless-In_{i} transition if S_{0}(C_{X}) = n_{4}^{p}, S_{1}(C_{X}) = n_{5}^{p}, and (if S_{1} is terminating) S_{0} =_{C} S_{1}. When this node is replaced by the flowchart for procedure wait-for-starless-In, then appropriate transitions are further defined.

5. Transition t is said to be a reading transition of cache C_{i} from address S_{0}(a) if t is terminating, S_{0}(C_{X}) = n_{5}^{p}, S_{1}(C_{X}) = n_{6}^{p}, and S_{0}(x) = S_{1}(x) for every variable x ∈ V(X) except possibly for x = c.

The value Val(t) of this read is defined to be S_{1}(c) and it can be either a Data value or ⊥. Again, C_{i}[a] is not a variable in V(X), and it does not restrict the possible outcomes of the reads which can be ⊥ or any Data value.

6. Conditional transitions corresponding to node n_{6}^{p} are defined naturally. S_{0}(C_{X}) = n_{6}^{p}, S_{1} is a regular state, S_{0} =_{C} S_{1} and there are two possibilities. If S_{0}(c) ∈ Data, then C_{1}(C_{X}) = n_{1}^{p}. If S_{0}(c) =⊥, then C_{1}(C_{X}) = n_{7}^{p}.

7. Reading transitions of Mem[a] corresponding to n_{7}^{p} are defined as above in item 5. S_{0}(C_{x}) = n_{7}^{p}, S_{1}(C_{X}) = n_{8}^{p}, S_{1}(c) ∈ Data (any Data value), and S_{0}(x) = S_{1}(x) for any other variable. The value Val(t) of this read is defined to be S_{1}(c).

8. Enqueuing transitions corresponding to node n_{8}^{p} are defined by the following requirements. S_{0}(C_{X}) = n_{8}^{p}, S_{1}(C_{X}) = n_{9}^{p}, t is terminating, and S_{0} =_{C} S_{1}. The value Val(t) of this transition is defined to be ∗, but In_{i} is not a variable in V(X) and the enqueue operation is not recorded in some state change.

9. t is a write transition corresponding to n_{9}^{p} if it is terminating, S_{0}(C_{X}) = n_{9}^{p}, S_{1}(C_{X}) = n_{1}^{p}, and S_{0} =_{C} S_{1}. The value, Val(t), of this transition is S_{0}(c). Again, C_{i}[a] is not a variable in V(X), and t does not change it.

10. t is an enqueue transition corresponding to n_{10}^{p} if it is a terminating transition such that S_{0}(C_{X}) = n_{10}^{p}, S_{1}(C_{X}) = n_{11}^{p}, and S_{0} =_{C} S_{1}. The value Val(t) of this transition is defined to be the pair ⟨S_{0}(d), S_{0}(a)⟩ of data and address.

11. The write transition corresponding to n_{11}^{p} is defined as the one corresponding to n_{9}^{p}.

12. The remaining transitions are defined in a similar fashion.

We leave it to the reader to complete the definitions of the states and transitions for the MemoryWriter and CacheInvalidator flowcharts. We shall have it handy to have an initialization transition in the MemoryWriter flowchart. This transition is a pair of states (S_{0}, S_{1}) such that for some initial Data value d_{0}, S_{1}(Mem)[a] = d_{0} for all a ∈ Addresses.

We see that transitions of serial flowcharts are really trivial. They do not express any properties of queues or atomic read/write operations. They are just local steps that reflect the structure of the flowchart and the possible moves along its directed edges.

6.3 Histories and unrestricted semantics

A history for a serial flowchart X is a sequence of steps over X, H = ⟨t_{i} | i ∈ I⟩, where the set of indices I is either all of ω (the set of natural numbers) or a finite initial segment of ω, I = {0, …, k − 1} of length k. Each step t = t_{i} corresponds to a transition, a pair of states, ⟨S_{1}(t), S_{2}(t)⟩. These transitions satisfy four demands:

1. They are transitions over X.

2. For each i such that i + 1 ∈ I, S_{2}(t_{i}) = S_{1}(t_{i+1}).

3. S_{1}(t_{0}) is an initial state.

4. All states S_{1}(t_{i}) for i ∈ I are regular, and if I is finite, the last state S_{2}(t_{k−1}) is unreachable.

The definition given here to histories is similar to the usual one, but notice the possible existence of unreachable states and the fact that all states are local.

We are going to redefine H. As in section 2.7, we shall define our histories as Tarskian structures, containing urelements and closed under formation of finite subsets. It is in this set-theoretical environment that the diverse definitions leading to histories are formally made. Let X be one of the flowcharts. First, the base structure M_{0} containing sorts, predicates, and functions that are later used is defined.

For example, M_{0} contains sorts Data and Addresses, and a special sort, X, to describe its flowchart. Members of X are the nodes of the flowchart (namely its locations). Then diverse functions (with possible additional sorts) are needed for the description of X. For example, a tag function gives to each node in X its instruction. A sort of variables consisting of V(X) and the locations variable C_{X} is also needed. A sort of events (or steps) Step (= Step_{X}) is in M_{0}. M_{0} contains also a sort Set (and an ∈ relation) and the set ω of natural number (with the ordering relation <, and arithmetical functions) is definable. There is in M_{0} a correspondence t which enumerate Step. Step = {t_{i} | i ∈ I}, where I is either ω or a finite initial segment of ω. In any case, a linear ordering < is defined on the events by t_{i} < t_{j} iff i < j.

We assume that M_{0} has a standard set interpretation. The definitions of states and transitions over X can be formally made in M_{0}.

Then the signature σ_{0} of M_{0} is extended by adding S_{1} and S_{2} as functions taking events in Step into states over X. Let σ be the resulting signature. The four demands formulated above are written as a sentence φ in σ. Then a history of X is an expansion H of M_{0} to signature σ that satisfies φ.

There is no need for a function Q as in section 2.7, since this information is definable and obtained from the value of the location variable. That is, the location in X can serve as EventType: for every step t = t_{j} we can define Q(t) = S_{1}(t)(C_{X}). (Here S = S_{1}(t) is the state prior to the execution of t, and S(C_{x}) is the node of X containing the instruction that t is about to execute.) This correspondence allows definitions of predicates and functions in H. Suppose for example that X is the flowchart of P_{i}. If t is a step of type wait-for-empty-Out_{i}, namely if Q(t) = n_{3}^{p}, then (viewing this instruction as a predicate on steps) define wait-for-empty-Out(t_{j}), and define P_{i}(t_{j}). Similarly, if Q(t) = n_{10}^{p}, then define enqueue(t) (here enqueue is a predicate, not an instruction), and define Val(t) as the pair of data and address (S(d), S(a)) where S = S_{1}(t).

For another example, suppose that t is a step such that Q(t) = n_{12}^{p}. Then the following predicates apply to t: dequeue_{In_{i}}(t) (to say that t is a dequeue of In_{i}), and Val(t) = S(x) where S = S_{2}(t).

Histories, as defined here for a single process with its flowchart X, are rather trivial, and they do not reveal the complexity of the algorithm. They are, however, a stage in the definition of the unrestricted semantics. Very simple properties that are still useful can be derived from these unrestricted histories. We give an example related to the flowchart of P_{i} and CacheInvalidator (although, for simplicity we refer to the text of the algorithm and to the line numbers rather than to the flowchart locations).

By “cache write” we mean a lower-level event that is an execution of an instruction of the form C_{i}[a] := v where v is a term. Cache write steps can be found in histories of the flowcharts of P_{i} and in histories of the flowchart of CacheInvalidator. The cache write events are divided into two types: those of Data values and those of ⊥.

1. The only cache write events of Data values are at the executions of line 2 in Read, and line 2 of Write.

2. There are two places where ⊥ is written on C_{i}. Line 2 of CacheUpdate and line 2 of CacheInvalidator.

Histories structures are defined for the MemoryWriter and CacheInvalidator flowcharts in a similar fashion. For any flowchart X we let H(X) denote the collection of all history structures of X.

6.3.1 Higher level events

Let H be a history structure of one of our flowcharts, and let E be the set of events of H (namely its Step sort). We further expand H by adding a new sort of “higher level” events. These represent complete executions of operations. For example if H is a history of flowchart X of P_{i}, then there are three types of higher level events: Read, Write, and CacheUpdate. Any higher level event is a set of lower level events (that is events from E). We have a membership relation ∈ in H which relates lower-level events to higher-level events that contain them.

A Write event W is a set W = {e, w} where e (denoted e_{W}, the “enqueue of W ”) is an enqueue event in E corresponding to node n_{10}^{p}, and w (denoted w_{W}, the “write of W ”) is the following write event corresponding to node n_{11}^{p}. The value Val(W) and the address address(W) of this higher level event are defined to be the corresponding values of the enqueue step e.

A higher-level Read event consists of an execution of sub-procedure Read(a) by some P_{i}. We shall prove that under the required specifications, all wait-for-empty-Out and wait-for-starless-In events are terminating, and hence all Read events are terminating. There are two categories of Reads, those that return their value “from cache” and are called “hit”, and those that return their value “from main memory” and are called “miss”. Somewhat more formally, if R is a Read event, let e be its cache read step corresponding to node n_{5}^{p}. If the value Val(e), of this read (namely S_{2}(e)(c)) is a Data value then R is said to be a hit and e is called the decisive read in R. In this case we define Val(R) = Val(e). If, however, Val(e) =⊥, then R contains another read event, corresponding to n_{7}^{p}, and then R is called a miss. If R is a miss, then the read in R corresponding to n_{7}^{p} is called the decisive read in R and its value is define to be Val(R). In any case, Val(R) is a Data value.

Recall that <, is the step ordering on the lower-level events of H defined by t_{i} < t_{j} iff i < j. In case H is a history for the flowchart of P_{i}, we can write <_{i} instead of < if we want to emphasize that the events are by process P_{i}. Now we extend this ordering relation on the higher-level events, and define for two higher-level events X and Y that

X <_{i} Y iff ∀x ∈ X ∀y ∈ Y (x <_{i} y).

It turns out that this is a linear ordering of the higher-level events in H, since they form disjoint (convex) intervals.

We also extend and define e <_{i} X and X <_{i} e for a lower-level event e and a higher-level event X when ∀x ∈ X e <_{i} x and respectively ∀x ∈ X x <_{i} e. Now, it is not the case that every lower-level and higher-level events are comparable. Indeed a higher-level event is not comparable with any of its elements.

We continue to denote with H(X) the collection of all (unrestricted) history structures for X with the additional higher-level events.

6.3.2 Unrestricted and restricted executions of the algorithm

Let \overline{X} = X_{1}, …, X_{N+2} be the collection of all flowcharts of our algorithm (N processes P_{i}, a central MemoryWriter and a CacheInvalidator). We intend to define structures H that are histories for each of the flowcharts X_{k}. Such a structure is called an “unrestricted” execution of the protocol. We shall let H = H(\overline{X}) denote the collection of all unrestricted executions.

We define H(\overline{X}) as the collection of all structures H obtained by taking all sequences of history structures H_{i} ∈ H(X_{i}) and forming their union H = H_{1} ∪ ⋯ H_{N+1} as follows.

1. Certain sorts, such as Data are common to all processes and appear uniformly in every H_{j}. Such sorts appear as a single entity in the union H. Other sorts, like that of the flowcharts, are specific to each process, and they appear as separate sorts. For example, the flowcharts X are specified as X_{P_{1}} etc, and taken as separate, disjoint sorts. Likewise, States are defined in H and are divided (or predicated) as “states of P_{i}” “states of MemoryWriter” and “states of CacheInvalidator”. Also events are specific to each H_{i} and they appear separately in H, as the following item says.

2. The events of H are obtained as a (disjoint) union of the events of all structures H_{i}. That is

E^{H} = Step^{H} = ⋃_{1≤i≤N+2} Step^{H_{i}}.

There are thus lower-level events and higher-level events in H partitioned by the following predicates: P_{i} events, MemoryWriter, and CacheInvalidator events.

3. For each P_{i}, <_{i} is the serial ordering of the lower-level events and also the induced serial ordering of the higher-level events of P_{i}. For i ≠ j there is no comparison between P_{i} and a P_{j} events. Similarly all MemoryWrite events in H are serially ordered, but we use the symbol ≺ (or ≺_{H}) to denote this ordering. For the CacheInvalidator events, we use <. Then <_{H} denotes the union of these orderings. So events that came from different H_{i}’s are unrelated in <_{H}. For example P_{i} and P_{j} events for i ≠ j are incomparable in <_{H}.

There are two main reasons why H is different from the history structures defined before (in Section 2.7 for example).

1. H does not represent an interleaving history of the processes. Each process is totally unrelated to the other processes. For example, it is possible that a read event c := Mem[a] in some Read event obtains a value for c that was never written in H in any of its Write events on Mem[a]. In this sense H is a totally “unrestricted execution” of the algorithm. If you want, it can be though of as representing an execution in which all communications are broken. The values returned by reads or dequeued are supposed to be in the appropriate type, but have no relation with any writes or enqueues. If any statement φ is true for every H ∈ H, then φ is true by virtue of the local structures of the algorithm even if the devices are totally malfunctioning. An example of such a statement is that in any higher level Write event W by P_{i}, of value v and address a, there exists a lower-level write w ∈ W on C_{i}[a] of value v.

2. Since events by different processes in H are incomparable in <_{H}, the relation <_{H} does not satisfy the finiteness requirement of Lamport (see Definition 2.1): any event in P_{i} has infinitely many events (in P_{j} when P_{j} is infinite) that do not follow it.

We define now restricted executions as system executions that define properly working runs of the Lazy Readers algorithm.

Definition 6.1 Let H ∈ H(\overline{X}) be any unrestricted execution. A system execution S is said to be a restricted extension of H (or a restricted execution based on H) if the following holds.

1. S is an expansion of H, namely H is the reduct of S to the signature of H, but S can have additional sorts, relations, and functions.

2. In particular, it follows from the item above that S and H have the same events, Step^{S} = Step^{H}. Since S is a system execution <_{S} (the temporal precedence relation of S) satisfies the requirements of Section 2.1. We further require that <_{S} extends <_{H}. That is, e_{1} <_{H} e_{2} implies that e_{1} <_{S} e_{2} for any two events. Namely, <_{S} respects the local linear ordering of each process.

3. For every queue q, the events in S pertaining to q satisfy in S the queue requirements. So S contains a function γ with which these requirements are expressed. (See section 2.2.1.)

4. The read and write events of every memory and cache locations comply to the atomicity requirements in S. So S contains a return function ω with which these requirements are expressed. (See section 2.3).

5. The external operations used by the algorithm (see the following subsection) satisfy their specifications in S.

A note concerning initial events is made. Histories are usually defined so that their first state is an initial global state. Here we prefer initial events (that precede any other events). The advantage of this assumption is that it enable a uniform definition of functions that return events. For example, without such an assumption the definition of the function that assigns MemoryWrite events to read events would be in two parts: if the read is preceded by a MemoryWrite event, then one form of the definition is applied, but otherwise it is a case of a read that returns “an initial value of the initial state”. So we assume that H contains initial MemoryWrite events.

6.3.3 Properties of external operations

In the state/history approach, the “Allowed if” conditions of a transition diagram determine which operations are enabled at each state. Here we have no such state provisions and the aim of this section is to replace them with system execution statements concerning the external operations. The external operations are those supplied by the system. Besides the read/write and the queue operations (enqueue/dequeue/peek), our algorithm uses the following external operations: decide(r, d, a) invoked by P_{i}, wait-for-empty-Out by the Read of P_{i}, decide(i) by the MemoryWriter, decide_{i}(a) by CacheInvalidator, and number-of-asterisks-in-In_{i} by wait-for-starless-In. Referring to system execution S the following specifies these operations.

List 6.2 (External Operations) 1. Every decide(r, d, a) event is terminating and it determines the values of its variables in their ranges: r ∈ {R, W, CU}, d ∈ Data, a ∈ Addresses. Formally it is possible to express this in our first-order language as a requirement on the structure S. We assume that there are in S three functions Val_{r}, Val_{d}, Val_{a} such that if D is a decide event (namely decide(D)) then Val_{r}(D) is defined and it is one of the constants R, W, CU, etc.

If D is a decide(r, d, a) event by P_{i} that determines r = CU, then there exists an enqueue event e on In_{i} that is not in {γ(x) | x <_{S} D, x is a dequeue event}.

In plain words, this condition restricts the system by allowing it to decide on a Cache Update operation by P_{i} only when In_{i} is non-empty. (But here In_{i} is not a variable, and this requirement is formulated in terms of γ.)

2. If t is a wait-for-empty-Out by P_{i}, then t is terminating iff every enqueue event q on Out_{i} such that q <_{S} t is in the range of γ restricted to the dequeue events. In case t is terminating, for every enqueue event q on Out_{i} such that q <_{S} t there is a dequeue event d on Out_{i} such that γ(d) = q and d <_{S} end(t).

3. For every index i, CacheInvalidator uses decide_{i}(a) to determine which address in C_{i} to invalidate. decide_{i}(a) may be non-terminating, but if it terminates it determines a ∈ Addresses. From the point of view of sequential consistency it is not important which policy is used in deciding this address.

4. If M is a number-of-asterisks-in-In_{i} event then M is terminating and it returns a natural number k (= Val(M)) that is the number of enqueue events q of value ∗ on In_{i} such that q <_{S} M and q ∉ {γ(d) | d <_{S} M is a dequeue}. (It is possible that by the time M terminates additional asterisks are enqueued.)

5. For every decide(i) event D by MemoryWriter, D is terminating iff there exists a process index k and an enqueue event e on Out_{k} that is not in {γ(d) | d <_{S} D}. If D terminates and it decides the value of variable i to be k, then there exists an enqueue event e on Out_{k} not in {γ(d) | d <_{S} D} and such that e <_{S} end(D).

6. The fairness requirement says that the following situation is impossible. That there is an enqueue event q on Out_{k} that is never dequeued, and there is an infinite number of decide(i) events, and yet only a finite number of decide(i) events decide i = k.

We continue with some consequences of this list of external operation properties which will be used in our correctness proof.

Lemma 6.3 It follows from this list of properties that each dequeue of In_{i} is cautious. Namely it is preceded by a check that the queue is non-empty. Hence all dequeue events x of In_{i} are terminating and γ(x) < x (by item 3 of 2.2.1 and the ensuing third remark). It also follows that all CacheUpdate and waitfor-starless-In events are terminating.

Proof. Since a CacheUpdate event contains a dequeue event of In_{i} followed by a possible write, once we prove that every dequeue of In_{i} is terminating, we obtain immediately that all CacheUpdate operations are terminating.

Observe that all dequeue events of In_{i} are in P_{i} and are hence linearly ordered in <_{S} (there are no peek events on In_{i}). Indeed an inspection of the flowcharts (or the programs of Figure 5) reveals that only CacheUpdate (for P_{i}) contains an In_{i}.Deq() instruction. The flowchart of CacheUpdate appears, in fact, twice within the flowchart of P_{i}, and there are two nodes with this dequeue instruction. One is n_{12}^{P_{i}} (within a direct invocation of CacheUpdate), and the second is within the expansion of node n_{4}^{P_{i}} into the flowchart of waitfor-starless-In. So In_{i} queues are dequeued only by Cache Update events, and we shall prove that these dequeues are all cautious. There are two cases:

1. For CacheUpdate events that are invoked by procedure P_{i} the lemma follows from item 1 in List 6.2 above which specifies that before CacheUpdate is invoked by P_{i}, decide(r, d, a) ensures that the execution of In_{i}.Deq() is cautious.

2. For CacheUpdate events that are (repeatedly) invoked by procedure waitfor-starless-In the lemma is based on item 4 of this list. The argument, which also shows that this procedure is terminating, follows.

Consider an execution s of procedure wait-for-starless-In by P_{i}. Its first instruction M is terminating (by item 4 of our list) and it determines the number k of those enqueue events of value ∗ on In_{i} that precede M and are not in {γ(d) | d <_{S} M}. Let U be the set of these k enqueue events. If k = 0, then the repeat loop of s is empty. Otherwise, let e be the last event in U. The repeat loop of s is executed and it contains only dequeue events d′ such that γ(d′) ≤_{S} e until a dequeue d′ such that e = γ(d′) is reached (because if e = γ(d′), then the condition “k asterisks were dequeued” holds after d′ and the loop stops. So s contains no further dequeue events after this last d′.) It follows that all dequeue events in s are cautious and hence terminating. Indeed if d′ is any dequeue in s then e shows that d′ is cautious. Namely, e <_{S} M <_{S} d′, and e is not of the form γ(d) for d <_{S} d′ (since such d would be the last event in s). So all dequeues in s are terminating.

Since the number of enqueue events on In_{i} that precede e is finite, the loop of CacheUpdate events in s must be terminating, and s itself is terminating. Briefly, the point is that each execution of In_{i}.Deq() is terminating as long as e has not yet been dequeued.

Q.E.D.

Included in the proof is the following corollary which we formulate for future use.

Corollary 6.4 Suppose that s is an execution of wait-for-starless-In by P_{i}, and e <_{S} s is an enqueue event of ∗ on In_{i}. Then there exists a dequeue event d on In_{i} such that γ(d) = e and d <_{S} end(s).

(Indeed, if e <_{S} s then either e = γ(d) for some d <_{S} M, or else e is in U.)

The following lemma uses both global properties of the queues Out_{k}, as formulated in section 2.2.1, and local properties of our serial flowcharts.

Lemma 6.5 1. Every dequeue or peek event on Out_{i} is terminating. Every MemoryWrite event is terminating.

2. For every enqueue event q on Out_{k} there exists a dequeue event d such that γ(d) = q.

Proof. Out_{i} queues are peeked and dequeued only by Memory Write events. The first item of the lemma follows from item 5 in List 6.2 which specifies that whenever decide(i) terminates and decides the value of i, it ensures that the following peek and dequeue of Out_{i} are cautious and hence terminating. Since all enqueue events are terminating, it follows that any MemoryWrite event is terminating.

Suppose that the second item of our lemma is false and q is an enqueue event on Out_{k} that is never dequeued. Namely, it is not in the range of γ restricted to the dequeue events. Since this range is an initial segment of enqueue events (see Item 3 of the Queue specifications 2.2.1), it follows that γ(d) < q for every dequeue event d of Out_{k}. Hence as γ is one-to-one on the dequeue events, there is only a finite number of dequeues of Out_{k} (as there is only a finite number of events that precede q, by the Finiteness condition). We will derive now a contradiction thereby proving the lemma.

Item 5 of the External Operations list 6.2 implies that every decide(i) event D is terminating. Indeed, enqueue event q is not in the range of γ, and is certainly not in {γ(d) | d <_{S} D}. It follows that every MemoryWrite event M is terminating, since each of its instructions is terminating. Indeed we proved that all peek and dequeue events are terminating, and we assume that writes on memory locations and enqueue operations are always terminating.

Since the program of MemoryWriter is a repeat forever loop of terminating executions, it follows that there is an infinite number of MemoryWrite events, and hence an infinite number of decide(i) events. Since, q is never dequeued, item 6 of 6.2 (the fairness requirement) implies that there must be an infinite number of Memory Write events that decide an index i = k. This yields an infinite number of dequeue events of Out_{k}. This contradiction proves the lemma. Q.E.D.

Lemma 6.6 Every executions of wait-for-empty-Out is terminating.

Proof. Let t be an execution of wait-for-empty-Out event by P_{i}. Every enqueue event q on Out_{i} such that q <_{S} t is in the range of γ restricted to the dequeue events (by the previous lemma 6.5). Hence item 2 of our list of properties implies that t is terminating.

The phrase “let S be an execution of the Lazy Readers algorithm” will be used to say that S is a restricted execution based on some history structure T of the algorithm.

7 Correctness of the Lazy Readers algorithm

Our aim in this section is to prove the following theorem.

Theorem 7.1 Every execution of the Lazy Readers algorithm is sequentially consistent.

Let S be an execution of the Lazy Readers algorithm fixed throughout this section. Our aim is to define in S a function μ and to prove that the Caching Axioms of section 3.2 hold in S. This will prove that S is sequentially consistent. We first define μ on all higher-level Write events. Let W be a Write event in S, and let q be the enqueue event in W (corresponding to line 1) of the pair (d, a) on Out_{i}. As q is in the range of γ (by Lemma 6.5) let d be that (unique) dequeue event such that γ(d) = q. Then d belongs to a unique MemoryWrite operation execution M and we define μ(W) = M.

It is clear that if W is a Write event then Val(W) = Val(μ(W)). (Val is defined in section 6.3.1. Val(W) = d.)

We can prove now axiom 6 of the Caching Axioms list 3.2.

Lemma 7.2 Suppose that in S, V <_{i} W where V and W are Write events in P_{i}. Then μ(V) ≺ μ(W).

Proof. Let e_{V} and e_{W} be the enqueue events in V and W. Since V <_{i} W, e_{V} <_{i} e_{W}. There exists dequeue events d_{V} and d_{W} such that e_{V} = γ(d_{V}) and e_{W} = γ(d_{W}). Since γ restricted to the dequeue events is order preserving d_{V} <_{S} d_{W}. Thus μ(V) <_{S} μ(W) which is the same as μ(V) ≺ μ(W)). Q.E.D.

We next define μ on the Read events. We also define a function ρ on Read events that are a hit. This will help us in later lemmas.

Let R be a Read by P_{i} of address a. R consists of terminating wait-for-empty-Out, wait-for-starless-In, and an execution of lines 3 and 4 of sub-procedure Read(a). Suppose first that R is a miss, namely that the value obtained in reading C_{i}[a] in line 3 of Read(a) is ⊥. Then R contains a read r of Mem[a]. This r was called the decisive read in R. Let ω(r) <_{S} r be the write on Mem[a] corresponding to r, and let M be the unique MemoryWrite event containing ω(r). Define μ(R) = M. (We have used here the assumption that an initial MemoryWrite event precede all other events. This ensures that every read of Mem[a] is preceded by some write on that register.)

Now suppose that R is a hit, and let r be the read in R of C_{i}[a]. This r was called the decisive read in R. Then the value of r is in Data and ω(r) is a Data write on cache C_{i}. Since the only writes of Data values on C_{i}[a] are in Reads that are miss and in Writes operation executions (all by P_{i}), there are two cases:

1. If ω(r) is an execution of instruction C_{i}[a] := c in line 4 in a Read event R^{∗}, then R^{∗} is a miss, and hence μ(R^{∗}) is defined. Then we define μ(R) = μ(R^{∗}). Observe that R^{∗} <_{S} R and R^{∗} is in P_{i}.

If this case holds, then we say that R is “a hit that reads from a miss,” and we define in this case ρ(R) = R^{∗}.

2. If ω(r) is an execution of instruction C_{i}[a] := d at line 2 of a Write event, then there is a unique Write event W (necessarily by P_{i}) such that ω(r) ∈ W. Clearly W <_{S} R. If this case holds, then we way that R is a “hit that reads from a Write,” and we define ρ(R) = W. We also define μ(R) = μ(ρ(R)).

This defines μ and ρ, and we continue the analysis in case R is a hit that reads from a Write. Consider W = ρ(R) as defined in item 2 above.

Let e_{W} ∈ W be the enqueue event on Out_{i}. Let t ∈ R be the wait-for-empty-Out event. As W <_{S} R, e_{W} <_{i} t follows. Item 2 of List 6.2 implies now that there exists a dequeue event d such that d <_{S} end(t) and γ(d) = e_{W}. By definition, W = μ(R). Let M be the unique MemoryWrite event containing d. So we write d_{M} for d. Let w_{M} ∈ M be the Mem[a] write in M (corresponding to line 3). Then we have

w_{M} <_{S} d_{M} <_{S} end(t) <_{S} r

and hence

w_{M} <_{S} r.  (11)

That is, the decisive read in R is after the relevant write in μ(R), although there is no direct connection between ω(r) and w_{M}.

Observe that ρ(R) <_{S} R for every Read R that is a hit, and ρ(R) is either a miss or a Write.

Lemma 7.3 For every Read event R, if M = μ(R) is the associated MemoryWrite event then M > |_{S} R. In fact, if w_{M} ∈ M is the write onto Mem[a] in μ(R) (execution of line 3 or an initial write) and if r ∈ R is the decisive read of address a in R, then w_{M} <_{S} r.

Proof. The proof is by considering the different cases in the definition of μ(R). The only interesting case is when R is a hit and the decisive read r ∈ R (of cache C_{i}[a]) is such that ω(r) belongs to a Write event W. We already gave the argument for this case in equation (11) above.

Lemma 7.4 For every Write event W, if M = μ(W) is the corresponding MemoryWrite event, if w_{M} ∈ M is the write onto Mem[a] in M, if e_{W} ∈ W is the enqueue event in W, then e_{W} <_{S} w_{M}. Hence W > |_{S} μ(W).

Proof. Let W be a Write event in P_{i}. Recall how μ(W) is defined: let e_{W} ∈ W be the enqueue event on Out_{i}, and let d be that dequeue event such that γ(d) = e_{W}, Then d belongs to a unique Memory Write event M, and we defined μ(W) = M. Since M is a Memory Write operation execution, it contains a peek event p ∈ W such that p <_{S} w_{M} <_{S} d (as p is an execution of line 2 and d of line 5). But necessarily γ(p) = γ(d) = e_{W}, and so e_{W} <_{S} p follows. Hence e_{W} <_{S} w_{M}. Q.E.D.

The following is axiom 7 from the list of Caching Axioms.

Corollary 7.5 Suppose that, in S, R <_{i} W, R is a Read and W a Write, both in P_{i}. Then μ(R) ≺ μ(W).

Proof. Say M_{1} = μ(R) and M_{2} = μ(W) are the corresponding Memory Write events. Let w_{1} ∈ M_{1} and w_{2} ∈ M_{2} be the lower-level writes onto Mem (we do not preclude the possibility that M_{1} = M_{2} and w_{1} = w_{2}). Let e_{W} ∈ W be its enqueue event. Then e_{W} <_{S} w_{2} by Lemma 7.4. If r ∈ R is its decisive read, then w_{1} <_{S} r by Lemma 7.3. But r <_{i} e_{W} (since R <_{i} W) and hence w_{1} <_{S} w_{2}. This yields M_{1} ≺ M_{2}. Q.E.D.

The following establishes L1 in the Caching Axioms list.

Lemma 7.6 Suppose that W and R are a Write and a Read events in P_{i} such that W <_{i} R. Then

M = μ(W) > |_{S} R.

In fact, if d_{M} ∈ M is the dequeue event in M (execution of line 5 in the Memory Write event) and t ∈ R is the wait-for-empty-Out event that prepare R, then d <_{S} end(t).

If, in addition, W and R have the same address, then μ(W) ⪯ μ(R)

Proof. Let e_{W} ∈ W be its enqueue of Out_{i} execution (corresponding to line 1 of Write). Let t ∈ R be the wait-for-empty-Out event that prepares R. Since t is terminating and as e_{W} <_{i} t, e_{W} = γ(d) for some dequeue event d such that d <_{S} end(t). Then d belongs to some uniquely defined Memory Write event M, and we defined M = μ(W). (By item 2 of List 6.2 of External Operations.) This proves the first part of the lemma.

Now we assume that W and R as above have the same address a. Let m ∈ M be the write in M onto Mem[a] (corresponding to line 3). Our aim is to prove that M ⪯ μ(R).

If R is a miss and r ∈ R its decisive read of Mem[a] then

m <_{S} d <_{S} end(t) <_{S} r

implies that m <_{S} r and hence m ≤_{S} ω(r), which shows that M ⪯ μ(R).

So we may assume now that R is a hit. Suppose first that R reads from a miss, and compare that miss ρ(R) (which is in P_{i}) with W. If W <_{i} ρ(R), then (as ρ(R) is a miss) μ(W) ⪯ μ(ρ(R)) is concluded, as in the previous paragraph, and (since μ(R) = μ(ρ(R))) μ(W) ⪯ μ(R). But ρ(R) ≺ W is impossible since W contains a write onto C_{i}[a] (an execution of line 2) and so the definition of ρ(R) excludes ρ(R) ≺ W ≺ R.

Assume next that R is a hit that reads from a Write, and compare that Write ρ(R) with W. Since W <_{i} R and W contains a write onto C_{i}[a], W ≤_{i} ρ(R). Hence Lemma 7.2 implies that μ(W) ⪯ μ(ρ(R)), namely μ(W) ⪯ μ(R) as required. Q.E.D.

Lemma 7.7 Let R in P_{i} be a Read of address a, and let r ∈ R be its decisive read. Suppose that R is a hit.

1. If R is a hit that reads from a miss, and ρ(R) <_{i} R is that miss, then for every Read R_{0} of address a in P_{i} such that

ρ(R) <_{i} R_{0} <_{i} R,

R_{0} is also a hit that reads from a miss, ρ(R_{0}) = ρ(R) and consequently μ(R_{0}) = μ(R).

2. If R is a hit that reads from a Write, and ρ(R) is that Write, then ρ(R) <_{i} R and for every Read R_{0} of address a in P_{i} such that

ρ(R) <_{i} R_{0} <_{i} R

R_{0} is also a hit that reads from a Write, ρ(R_{0}) = ρ(R) and consequently μ(R_{0}) = μ(R).

Proof. Assume first that R is a Read and a hit that reads from a miss. Say R is in P_{i} and its address is a. Let r ∈ R be its decisive read, which in this case is a read of C_{i}[a] such that ω(r) belongs to some Read event denoted ρ(R). Since ω(r) is a write of a Data value on C_{i}[a], ρ(R) is necessarily a miss (only Reads that are misses write back to their caches).

Now let R_{0} be any Read event in P_{i} such that R_{0} reads address a and ρ(R) <_{i} R_{0} <_{i} R. Let s ∈ R_{0} be the read of C_{i}[a] corresponding to line 3 of its program. Then we have

ω(r) <_{i} s <_{i} r.

It clearly follows from the seriality of C_{i}[a] that

ω(r) = ω(s).  (12)

(Because the alternatives ω(r) <_{i} ω(s) and ω(s) <_{i} ω(r) lead to immediate contradictions.) Thus ρ(R_{0}) = ρ(R)). Since μ(R_{0}) is defined by μ(R_{0}) = μ(ρ(R_{0})), we obtain μ(R_{0}) = μ(R).

The proof of the second part of the lemma is very similar. Now L2 can be derived.

Corollary 7.8 If R_{0} <_{i} R_{1} are two Read events by P_{i} both of address a, then μ(R_{0}) ⪯ μ(R_{1}).

Proof. The finiteness condition (Definition 2.1 in Section 2.1) implies that for every event e there exists only a finite number of events x such that x <_{S} e. Hence, if the lemma is false, there is a (minimal) counterexample R_{1} such that for every R′_{1} <_{i} R_{1} the lemma for R′_{1} is valid. Consider this minimal counterexample R_{1} and let R_{0} <_{i} R_{1} be a Read of the same address a We shall analyze the definition of μ(R_{1}) and obtain the lemma in every case.

The simplest case is when R_{1} is a miss. Let r_{1} ∈ R_{1} be the decisive read in R_{1} and let r_{0} ∈ R_{0} be its decisive read. Let m ∈ μ(R_{0}) be the write on Mem[a]. Then m <_{S} r_{0}, by Lemma 7.3. Since R_{0} <_{S} R_{1} implies that r_{0} <_{i} r_{1}, it follows that m <_{S} r_{1}. As m is a write and r_{1} a read of the same memory location Mem[a], m ≤_{S} ω(r_{1}) follows, and μ(R_{0}) ⪯ μ(R_{1}) is concluded.

Now suppose that R_{1} is a hit. Then ρ(R_{1}) is defined and μ(R_{1}) = μ(ρ(R_{1})). There are two cases. Suppose first that R_{1} reads from a miss. That is ρ(R_{1}) is a Read in P_{i} that is a miss. We compare ρ(R_{1}) and R_{0}. If ρ(R_{1}) <_{i} R_{0} then Lemma 7.7 and R_{0} <_{i} R_{1} imply that R_{0} is also a hit that reads from a miss and ρ(R_{0}) = ρ(R_{1}). Thus μ(R_{0}) = μ(R_{1}).

If ρ(R_{1}) = R_{0} then μ(R_{1}) = μ(ρ(R_{1})) = μ(R_{0}). So R_{0} <_{i} ρ(R_{1}) remains to be considered. Since both R_{0} and ρ(R_{1}) are Reads in P_{i} of address a, we may by the inductive assumption conclude that μ(R_{0}) ⪯ μ(ρ(R_{1})) = μ(R_{1}).

Now suppose that R_{1} is a hit that reads from a Write. Again we compare that Write ρ(R_{1}) with R_{0} <_{i} R_{1}. If ρ(R_{1}) <_{i} R_{0}, then Lemma 7.7(2) implies that R_{0} is also a hit that reads from ρ(R_{1}) and μ(R_{0}) = μ(R_{1}) follows. Thus R_{0} ≤_{i} ρ(R_{1}). Equality is impossible since R_{0} is a Read and ρ(R_{1}) a Write. So the last possibility is R_{0} <_{i} ρ(R_{1}). Now Corollary 7.5 applies and gives μ(R_{0}) ≺ μ(ρ(R_{1})) = μ(R_{1})). Q.E.D.

We discuss now CacheUpdate operations and extend the definition of μ on them. Given any CacheUpdate event C by P_{i} consider its dequeue event d_{C} of In_{i} (execution of line 1). Then γ(d_{C}) = e is the corresponding enqueue event. Checking the algorithm, it is evident that only MemoryWrite events and Reads by P_{i} that are a miss contain enqueue events on In_{i}. So e is in some higher-level event X, which is a uniquely determined MemoryWrite or Read. In the first case we define μ(C) = X, and in the latter μ(C) = μ(X). Whenever μ(C) = M, we say that “C is the updating of cache C_{i} done for M” (even though C may include no write at all, in case the value dequeued is ∗).

Lemma 7.9 Let C be a CacheUpdate event in P_{i}, and M = μ(C) be the associated MemoryWrite event. Let d_{C} ∈ C be the dequeue event, and w_{M} ∈ M the write on Mem[a] corresponding to line 3. Then w_{M} <_{S} d_{C} and thus μ(C) > |_{S} C.

Proof. Consider the definition of μ(C). Let e = γ(d_{C}) be the associated enqueue event on In_{i}. Then e <_{S} d_{C}. This follows remark 3 in section 2.2.1, since by Lemma 6.3 each dequeue of In_{i} is cautious.

1. If e ∈ M. Then e corresponds either to line 4 (enqueuing ∗) or to line 6 (enqueuing a Data value). In any case w_{M} <_{S} e, and the lemma follows.

2. If e is in some Read event R, then R is in P_{i}, and M = μ(R) by definition. Clearly R <_{i} C since every two higher-level P_{i} events are comparable, and C <_{i} R contradicts e <_{S} d_{C}. Necessarily, R is a miss, since only misses have enqueue events on In_{i}. Let r ∈ R be its decisive read. Then w_{M} = ω(r), by definition of M = μ(R). Thus

w_{M} <_{S} r <_{S} e <_{S} d_{C}

and again w_{M} <_{S} d_{C}.

Lemma 7.10 Let C be a CacheUpdate event by P_{i}, and suppose that W is in P_{i} a Write event (of any address). If C <_{i} W, then

μ(C) ≺ μ(W).

Hence if W and C are a Write and CacheUpdate events both by P_{i}, and if μ(W) ⪯ μ(C), then W <_{i} C.

Proof. If w ∈ μ(C) is the write on its memory location, and d_{C} ∈ C is the dequeue event of In_{i}, then w <_{S} d_{C} by the previous lemma.

On the other hand, if M_{1} = μ(W), e_{W} ∈ W is the enqueue event on Out_{i}, and w_{1} ∈ M_{1} is the write there on its memory location, then e_{W} <_{S} w_{1} by Lemma 7.4.

Since C <_{i} W, d_{C} <_{S} e_{W}, w <_{S} w_{1} follows. Hence μ(C) ≺ μ(W).

The second part of the lemma is deduced immediately since if W <_{i} C does not hold, then C <_{i} W by the seriality of P_{i}, and hence the first part of the lemma yields a contradiction: μ(C) ≺ μ(W). Q.E.D.

The following lemma shows that the updates of local cache C_{i} are done in order. This is axiom L3.

Lemma 7.11 Suppose that M_{0} is a MemoryWrite event, and C a CacheUpdate event such that M_{0} ≺ μ(C). Then M_{0} = μ(C_{0}) for some CacheUpdate C_{0} in P_{i} such that C_{0} <_{i} C.

Proof. There are two cases in the definition of μ(C), and accordingly the proof is divided in two. Let d_{C} ∈ C be its dequeue of In_{i} event. Suppose first that e = γ(d_{C}) is in M = μ(C). Consider M_{0} ≺ M and let e_{0} ∈ M_{0} be the enqueue event on In_{i} there (either of ∗ or of some address). Then e_{0} <_{S} e. Hence, by the 2.2.1 properties of γ, e_{0} = γ(d_{0}) for some dequeue event of In_{i} such that d_{0} <_{S} d_{C}. But only CacheUpdate events by P_{i} contain dequeues of In_{i}, and hence e_{0} ∈ C_{0} for some C_{0} <_{i} C which is as required.

The second case is when e = γ(d_{C}) is in some miss R, and then M = μ(C) is defined by M = μ(R). Let m ∈ M be its write on Mem[a]. In Lemma 7.3 we concluded that m <_{S} r, where r is the decisive read in R. As r <_{S} e, m <_{S} e = γ(d_{C}). If e_{0} ∈ M_{0} is the enqueue event there on In_{i} then M_{0} ≺ M implies that e_{0} <_{S} m, and hence e_{0} <_{S} γ(d_{C}). Again, we obtain some dequeue event of In_{i}, d_{0} <_{S} d_{C}, such that e_{0} = γ(d_{0}), and this yields as above that M_{0} = μ(C_{0}) for some CacheUpdate C_{0} <_{i} C. Q.E.D.

Our next lemma proves that axiom L4 holds in S.

Lemma 7.12 Suppose that R is a Read in P_{i} and U is a Read or a Write event in P_{i} such that U <_{i} R. Let M = μ(U) be the MemoryWrite event associated with U. Then there exists a CacheUpdate event C in P_{i} such that C <_{i} end(R) and M = μ(C).

Proof. Suppose first that U is a miss by P_{i}. Since U <_{i} R, the wait-for-starless-In event v that prepares R satisfies U <_{S} v <_{S} R. As it is a miss, U contains an enqueue event e_{U} of ∗ on In_{i}. So e_{U} <_{S} v and (Lemma 6.4) there is a CacheUpdate event C with its dequeue event d_{C} ∈ C satisfying C <_{S} end(v) and γ(d_{C}) = e_{C}. By definition, γ(C) = M. Clearly C <_{S} R (as v <_{S} R).

Now suppose that U is a Write by P_{i}. Then U contains an enqueue event e on Out_{i}, and M = μ(U) contains a dequeue event d of Out_{i} such that γ(d) = e. Let t and v (with t <_{S} v) be the wait-for-empty-Out and wait-for-empty-starless-In events in P_{i} that prepare R. Then U <_{S} t <_{S} v <_{S} R. So e <_{S} t and hence d <_{S} end(t) (by List 6.2). In M, the dequeue of Out_{i} comes after the enqueue e_{M}^{∗} of ∗ into In_{i}. Thus, e_{M}^{∗} <_{S} end(t) and hence e_{M}^{∗} <_{S} v. By Lemma 6.4 there exists a dequeue of In_{i} event d′ such that γ(d′) = e_{M}^{∗} and d′ <_{S} end(v). There exists a CacheUpdate event C by P_{i} such that d′ ∈ C, and then μ(C) = M and C <_{i} R follows.

Finally, suppose that U is a Read that is a hit. Then ρ(U) <_{i} U is defined; ρ(U) is a miss or a Write and hence the lemma holds for ρ(U). Yet μ(ρ(U)) = μ(U), and hence the lemma holds for U as well. Q.E.D.

The following lemma is Axiom L5.

Lemma 7.13 Let C and R be a CacheUpdate and Read events in P_{i} such that C <_{i} R, and such that R and M = μ(C) have the same address a. Then M ⪯ μ(R).

Proof. Intuitively, the lemma says that if C is a local update of M in cache C_{i}, and if R comes after that update, then the Memory Write associated with R cannot be older than M.

If w_{M} ∈ M is the write on Mem[a], and d_{C} ∈ C is the dequeue of In_{i}, then w_{M} <_{S} d_{C} by Lemma 7.9. An easy argument shows in case R is a miss that M ⪯ μ(R). So we assume that R is a hit.

There are two case in the definition of M = μ(C). Assume first that e = γ(d_{C}) is in some miss R_{0} <_{i} C in P_{i}, and M = μ(R_{0}). Then R_{0} <_{i} R and both are Reads of address a. Hence μ(R_{0}) ⪯ μ(R) by Corollary 7.8.

Thus we may assume the second case, namely that e = γ(d_{C}) is in M. Let W be that Write event such that μ(W) = M. There are two possibilities

1. Assume first that W is in P_{j} for j ≠ i. Then Val(e) ∈ Data, and it follows that C contains a write, w, of ⊥ on location C_{i}[a]. This entails that C <_{i} ρ(R).

(a) If ρ(R) is a Write event then Lemma 7.10 yields μ(C) ≺ μ(ρ(R)) = μ(R).

(b) If ρ(R) is a miss, then (by our lemma which is already proven for misses) μ(C) ⪯ μ(ρ(R)) = μ(R).

2. Next assume that W ∈ P_{i}. Then W <_{i} C by the last sentence of Lemma 7.10 (since μ(W) = μ(C)). Thus W <_{i} R and they have the same address a, so by Lemma 7.6 μ(W) = μ(R).

8 Conclusion

Two distributed versions of the Lazy Caching algorithm of Afek, Brown, and Merritt [2] were described here. These versions are “distributed” in the sense that we do not assume atomicity of complex operations. Correctness proofs were given to these variants in which the notion of a global state does not appear. For fear of “state explosion”, the generally accepted paradigm of state-history shuns multiplicity of states and seeks ways to reduce their numbers, at the price of reducing concurrency. 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, even though the notion of a global state is no longer available (and is not needed) for higher-level events.

Part of the correctness proof is an abstract derivation (such as sequential consistency from Caching 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 Caching 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 “higher-level” 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 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)