How to formally explain a (cache coherence) protocol

Uri Abraham

Departments of Mathematics and Computer Science, Ben-Gurion University, Be’er-Sheva, Israel

October 29, 2003

Abstract

Formal specification writers and researchers whose main interest is mathematical correctness proofs do not usually explain their protocols. Engineers and system builders are usually not very interested in the formal details involved in a correctness proof, although they surely want the readers to understand the subtleties of their constructions. We want to narrow this gap by suggesting that a mathematical investigation of higher-level properties of protocols can contribute to the process of learning and understanding them. To exemplify our approach, a cache coherence protocol is described and explained informally. Part of this explanation is an abstract, higher-level proof that the desirable properties of the protocol (cache coherence) follow from some basic properties (Called here axioms).

1 Introduction

It is a common experience that by reading a well-written mathematical proof one is not only convinced that the theorem is correct, but also gains a deeper understanding of the subject studied. We shall argue in this paper that explaining and understanding a concurrent protocol ameliorate by following a formal proof of its higher level properties. This may seem at first counter-intuitive since the two terms, formal proof and explanation may seem contradictory: explanation is intuitive, often inaccurate on purpose, while formalization is detailed and often hard to read and understand. So the natural and most efficient way to learn a subject is first to understand its broad outlines informally and only then to plunge into the details and formality of a mathematical proof. It is not our intension here to reverse this order, but to point to the advantage of having a formal proof as part of the understanding process, at a reasonably early stage, and to suggest that this formal proof should concentrate on the higher-level properties of the protocol. Concurrent protocols are often very intricate texts with many details that are hard to understand. In many subjects of study it is a good strategy to present a reduced model, a simplified version, of the “real” object studied. Protocols are not an exception and whenever a short protocol can represent an idea that a larger protocol encompasses, it is advisable to explain the short protocol first. Yet even tiny protocols are hard to understand because concurrency amplifies their complexity. So the question remains for short protocols that cannot be further reduced: how to explain them? Our answer is to study them abstractly by considering their higher level properties.

Examples are necessary to support this answer and to show its advantages, and this paper consists of such an example: a formal explanation of a cache coherence protocol.

The protocol investigated here is motivated by the protocol that appears in the Wildfire Verification Challenge described in [5] and in TLA documents by L. Lamport that can be obtained through the web^{1}. The Wildfire is not an easy protocol, and in order to understand one of its ideas (concerning cache coherence) we reduced and simplified the protocol to the smallest elements in which this idea still appears. The resulting protocol is the Cache Coherence protocol described and explained (informally) here.

2 The protocol: an informal description

The processes involved in the protocol are the following.

1. There are N user processes Proc = {P_{1}, …, P_{N}} which share a collection of objects. Each user process requests load and store operations on objects (a load is a read of an object, and a store is a write).

2. There are N “cache administrators”, CAP_{1}, …, CAP_{N}. The role of CAP_{i} is to cater to the requests of P_{i} and to monitor the cache C_{i} of that process.

1in URL http://research.microsoft.com/users/lamport/tla/wildfire-challenge.html

3. The central directory is a process that dynamically maintains a list of owners and objects and their secondary copy holders.

Each object has its own address, and the space of all addresses is called Address. An address of an object is used as its name, so that we say “the object a” instead of “the object at address a”. At each moment every object has a (unique) “owner” which is that user process that has the “primary” copy of the object. Other processes may have “secondary” copies of it (these are the readers of the object). This distribution of copies among processes changes in time, as processes dynamically request to be writers or readers of objects, and thus the ownership and readership of an object vary.

1. If process P_{i} has a primary copy of an object a and no other process has a copy of a, then we say that P_{i} has a primary exclusive copy of a.

2. If P_{i} has a primary copy of a but some other processes have secondary copies, then P_{i} is said to have a primary shared copy of a.

Every process P_{i} has a cache (a local memory) C_{i} in which it keeps its copies and additional information. (There is no central memory.) For every a ∈ Address, C_{i}[a] is a record (called cache line) with three fields:

                    {state, data, activated}.

If C = C_{i}[a] is the cache line of address a, then

1. C.state ∈ {PrimaryExclusive, PrimaryShared, Secondary, Invalid}.

2. C.data ∈ Data ∪ {InvalidData}.

3. C.activated is Boolean,

We describe the role of these fields intuitively.

1. C.state = PrimaryExclusive when P_{i} has an exclusive copy of a (no other process has a copy), and then P_{i} may write (and certainly read) a.

2. If C.state = PrimaryShared, then P_{i} can read a, but is not allowed to change it since there are processes with a secondary copy of a, and changing a will leave them with a stale copy. P_{i} must regain an exclusive copy of a before it may write and change it.

3. In the first two cases P_{i} has a primary copy of the object. If C.state = Secondary, then P_{i} can only load (read) the object.

4. The value C_{i}[a].state = Invalid indicates that P_{i} has no copy of a, and it must gain one for any operation on a.

5. Data is the type of our objects, and whenever C.state ≠ Invalid, C.data is the copy of a in C_{i}[a]. InvalidData is a non-data constant, and C.data = InvalidDataindicates that P_{i} has no copy of a.

6. The third field, activated, indicates that P_{i} is waiting for a fill message from some process or for a message from the directory. Its role is explained in details later.

The user processes issue Load/Store requests to the system which administrate their requests. The requests of each process are issued in a serial order. At each moment there may be several outstanding requests (requests of a user that the system has not yet completely treated). The system itself comprises of the caches C_{i} and a central “directory” process. The directory maintains an array Mem with entries indexed by Address. For every a ∈ Address, Mem[a] is a record with two fields: Writer and Readers. If M = Mem[a], then M.Writer ∈ Proc (recall that Proc = {P_{1}, …, P_{N}}) and M.Readers ⊆ Proc. If M.Writer = P_{i}, we say that P_{i} is the owner of a and it has the primary copy. There are two cases:

1. If M.Writer = P_{i} and M.Readers = ∅, then we say that P_{i} has a primary exclusive copy of a.

2. If M.Writer = P_{i} and M.Readers ≠ ∅, then we say that P_{i} has a primary shared copy of a, and each P_{j} ∈ M.Readers has a secondary copy.

The directory does not contain copies of objects—these reside solely with the users’ caches. As a consequence, the owner of an object cannot evict it, and the primary copy of an object always circulates among the users. (It is easy to add a central memory which holds copies of objects while they have no owner, but we prefer to keep the protocol as simple as possible and hence we have no central memory).

P_{i} issues its load/store requests to the cache administrator process of P_{i}, called CAP_{i}, which checks if the request can be executed immediately (from the cache of P_{i}) or else the help of the directory is required. A preliminary description of these procedures is as follows.

1. A load of a is immediate if C_{i}[a].state ≠ Invalid. In this case the load is executed immediately from C_{i}[a].data. If, however, C_{i}[a].state = Invalid, CAP_{i} sends a GetShared message to the directory (with a as a parameter), The directory has no copies of objects, but it knows which process is the owner of a and it sends a ForwardedGet message to that owner. Then the owner sends a copy of a to CAP_{i} (which becomes a secondary copy) and finally (when this copy arrives) C_{i}[a] can be updated with the new value.

2. A store request on a is immediate for P_{i} if C_{i}[a].state = PrimaryExclusive. In this case the writing on C_{i}[a].data is done immediately. In any other case, CAP_{i} first sends an appropriate message to the directory, and P_{i} must wait until it possesses an exclusive copy of a. There are two basic cases when C_{i}[a].state ≠ PrimaryExclusive.

(a) If C_{i}[a].state ≠ Invalid, then C_{i}[a].state is either PrimaryShared or Secondary. In both cases CAP_{i} sends a ChangeToExclusive message to the directory. The directory checks that P_{i} has a valid copy of a (namely that either P_{i} = Mem[a].Writer or P_{i} ∈ Mem[a].Readers). If it does, then the directory sends Inval messages to the processes that would no longer have a valid copy (since P_{i} is going to change it), and sends a positive ChangeToExclusiveAck message to CAP_{i} which now has a primary exclusive copy of a.

(b) If C_{i}[a].state = Invalid, then CAP_{i} sends a GetExclusive message to the directory (always with a as a parameter). The directory then sends a ForwardedGet message to the owner of a and Inval messages to its readers. When the owner of a receives this message it sends its primary copy of a directly to CAP_{i} (as a fill message) and thus C_{i}[a] becomes the primary exclusive copy of a.

[figure: P_{i}; P_{j}; reqQ_{i}; resQ_{i}; CaDr_{i}; CAP_{i}; C_{i}; DIRECTORY; SYSTEM; DrCaQ_{i}; fillQ_{{}j, i}]

Figure 1: Architecture of the system.

This short description leaves out many details, but it shows the necessity of communication channels (called here queues) between the users, the cache administrators, and the directory. These queues are described as follows.

2.0.1 System architecture.

By system architecture we mean a description of the queues that connect the different processes. The architecture is described in Figure 1. A queue is a data structure connecting two processes: the sender sends (or enqueues) messages and the receiver removes (or dequeues) them. The receiver can also just read the incoming messages without removing them. Each message sent arrives (in order) and each message received was sent. We say that message a precedes message b on a queue if a was enqueued before b. In this case it also arrives to the receiver’s end before b. However the queues are not necessarily FIFO, and the receiver can dequeue messages in any order. The protocol maintains five kinds of queues, each with a specified type of messages. The queues are: DrCaQ_{i}, CaDrQ_{i}, reqQ_{i}, resQ_{i}, and the fill queues fillQ_{i,j}.

We have the following types of messages:

Load, Store, MemoryBarrier, Responses, GetShared, GetExclusive,

ChangeToExclusive, FillMarker, ForwardedGet, ChangeToExclusiveAck,

Inval, Fill.

1. The request queues. reqQ_{i} is a queue of requests enqueued by the user process P_{i}, and then serviced and dequeued by its system process CAP_{i}. The elements of reqQ_{i} are of the form (Load, a), (Store, v, a), and MB. Here, Load, Store, and MB are constants, v ∈ Data, and a ∈ Address.

2. The response queues. resQ_{i} is a queue of Responses that are sent by the system’s cache administrator process CAP_{i} to the user process. MB and Store requests need no response. The response to a Load request at address a is pair (v, a) of value v ∈ Data and address a.

3. The cache to directory queues. CaDrQ_{i} is a queue of messages that travel from CAP_{i} to the directory Dr. The elements of CaDrQ_{i} are of type GetShared, GetExclusive, and ChangeToExclusive. The directory alway responds to these messages: GetShared and GetExclusivemessages are responded by a FillMarker message, and ChangeToExclusive messages are responded by ChangeToExclusiveAck messages.

4. The directory to cache queues. DrCaQ_{i} is a queue of messages that travel from the directory to processor CAP_{i}. The messages are of type FillMarker, ChangeToExclusiveAck, Inval, and ForwardedGet.

This queue is assumed to be FIFO: it is always the last (oldest) message that is dequeued.

5. The fill queues form a complete connection between all the CAP processes. These queues carry data messages (as opposed to the previous control messages). Process CAP_{i} sends a Fill to process CAP_{j} via the fillQ_{i,j} queue. If F is a Fill message, then F has two fields: F.data ∈ Data, F.address ∈ Address.

Process CAP_{i} serves a request in reqQ_{i} and either executes it immediately (in case of a hit) or else begins an execution that involves several processes (in case of a miss). In both cases the request is finally dequeued from reqQ_{i} by CAP_{i}. The rules for serving a request are the following:

1. Process CAP_{i} can serve a request r for a Load/Store instruction in reqQ_{i} if all of the following occur:

(a) r refers to address a and C_{i}[a].activated is false. (This indicates that r has not yet been served.)

(b) r is not preceded by a memory barrier request present in reqQ_{i}.

(c) r is not preceded by a request with the same address present in reqQ_{i}.

2. CAP_{i} can serve and immediately dequeue a memory barrier request mb from reqQ_{i} queue, if all of the following holds:

(a) mb is not preceded by another memory barrier request. Namely, mb is the latest request on reqQ_{i}.

(b) The ackPending counter of CAP_{i} is zero. This counter records the number of messages CAP_{i} has sent to the directory minus the number of responses received.

2.0.2 Immediate executions.

1. Suppose CAP_{i} serves a ⟨Load, a⟩ request in reqQ_{i} and C_{i}[a].state ≠ Invalid. Then this request is said to be a “hit”. In this case CAP_{i} dequeues the request, and enqueues on resQ_{i} the response ⟨C_{i}[a].data, a⟩.

2. Suppose CAP_{i} serves a ⟨Store, v, a⟩ request in reqQ_{i} when C_{i}[a].state = PrimaryExclusive. Then this request is said to be a “hit”. In this case CAP_{i} assigns C_{i}[a] := v, and dequeues the request.

In case CAP_{i} serves a Load/Store request that is not a hit, we say that the request is a miss. Then CAP_{i} begins an indirect execution which we describe by the following possible “scenarios”. We use the term scenario to describe a chain of events by several processes. In a formal presentation we would have to write a program, a protocol text, but here we remain at an informal stage of explaining how the protocol works, and for this aim scenarios are quite useful.

3 Scenarios of the protocol

We present in this section the possible scenarios that describe what CAP_{i} does when a miss occurs.

1. Suppose CAP_{i} serves a ⟨Store, v, a⟩ request in reqQ_{i} that is a miss. Consider first the case that C_{i}[a].state = Invalid. Then CAP_{i} sends to the directory a GetExclusive message ⟨GE, a⟩ (via the CaDrQ_{i} queue). CAP_{i} also sets field activated of C_{i}[a] to true. (This will prevent P_{i} from resending a GetExclusive message to the directory.) The GetExclusive message reaches the directory which checks M = Mem[a]. If M.Writer = P_{j}, then P_{j} is the current primary holder of address a. The directory sends to CAP_{j} a ForwardedGet message ⟨FG, P_{i}, a, “exclusive′′⟩. This message contains the name of the requesting processor (namely P_{i}), the address requested (a) and an “exclusive” state flag. When CAP_{j} receives the ForwardedGet message, it sends a Fill message ⟨C_{j}[a].data, a⟩, to CAP_{i} and invalidates its own cached copy. The Fill is sent via fillQ_{j,i}.

The directory also sends each reader of a processor an Inval message containing the address, asking them to invalidate their copy (since now the requesting processor has exclusive access to that address and it may change it). The directory sets M.Readers := ∅. The directory marks P_{i} as the primary holder of address a. In addition, the directory sends a FillMarker acknowledgment message ⟨FM, a⟩ to CAP_{i}.

When CAP_{i} receives the FillMarker message, it decreases a ackPending counter. (This counter is increased at every message sent to the directory: GetShared, GetExclusive, and ChangeToExclusive.) When the Fill sent by CAP_{j} arrives, CAP_{i} does the following:

(a) It sets the data, activated, and state fields of C_{i}[a] as follows. The datafield is as obtained by the fill, the activated field is set to false, and the state field is PrimaryExclusive.

(b) It dequeue the (Store, a⟩ request.

Processor can perform these operations as soon as the Fill is received, even in case that the FillMarker message has not been received yet.

2. Suppose, again, that CAP_{i} serves a ⟨Store, v, a⟩ request that is a miss, but this time C_{i}[a].state ∈ {PrimaryShared, Secondary}. Then CAP_{i} sends a ChangeToExclusive message ⟨CtE, a⟩ to the directory. In addition, CAP_{i} sets C_{i}[a].activated to true. When the directory obtains this message, it checks M = Mem[a]. There are two cases.

(a) If CAP_{i} is not in M.Readers ∪ {M.Writer}, then the request is denied. The directory sends P_{i} a ChangeToExclusiveAck message ⟨CtEAck, a, false⟩ with field success set to false. This situation can happen when another process has asked for an exclusive copy or for a change to exclusive, and this request was granted. In this case an invalidation for address a is in DrCaQ_{i} which has not yet been dequeued by CAP_{i}, and CAP_{i} has asked for a ChangeToExclusive without knowing this fact. Another possibility is that CAP_{i} had a PrimaryShared copy of address a and a ForwardedGet message has not yet reached it when it asked for a ChangeToExclusive. In any case, since the DrCaQ_{i} is FIFO, when CAP_{i} receives this negative acknowledgment, it has already received the message from the directory which invalidates the cached copy and its cache line has an invalid state. Then P_{i} just updates field activated to be false. Later on, when P_{i} tries again to perform the same store, it finds the state of this cache line Invalid, and it will act as stated in item 1.

(b) If P_{i} appears on the readers list or is the current writer of M, then the request is granted. The directory sends Inval messages to each CAP_{k}, for k ≠ i in M.Readers∪{M.W riter}. The directory sets M.W riter := P_{i} and MReaders := ∅. The directory sends CAP_{i} a ChangeToExclusiveAck message for address a with a success field set to true. When P_{i} receives this acknowledgment, it upgrades the state of the cached copy to PrimaryExclusive. Now CAP_{i} can execute the store instruction: it dequeues the request from reqQ_{i}, it writes on cache line C_{i}[a] the value requested to be stored, and it enqueues a response in resQ_{i} by which the store operation terminates.

3. If CAP_{i} serves a ⟨Load, a⟩ instruction that is a miss (namely C_{i}[a].state = Invalid), then it sends a GetShared message ⟨GS, a⟩ to the directory. CAP_{i} also sets field activated of C_{i}[a] to true. When the directory receives the message, it checks the contents of M = Mem[a]. Suppose that j is the index such that M.Writer = P_{j}. Then j ≠ i. The directory adds P_{i} to the readers list of M, and acts as follows.

(a) The directory sends a ForwardedGet message ⟨FG, P_{i}, a, “shared′′⟩, to CAP_{j} via the DrCaQ_{j} queue. This message has a “shared” state flag. When CAP_{j} receives the ForwardedGet message, it sends a Fill message with a copy of C_{j}[a].data to CAP_{i}, and changes its own state to PrimaryShared. (CAP_{j} knows that the request is for a shared copy, and hence it doesn’t invalidate its cache line.)

(b) The directory also sends a FillMarker acknowledgment message to CAP_{i}.

As soon as CAP_{i} receives the Fill from CAP_{j} it updates the state of its cache line C_{i}[a] to Secondary, it dequeues the Load request from reqQ_{i}, and it enqueues a response with the data and address on the resQ_{i} queue.

When CAP_{i} receives the FillMarker from the directory, it decreases its ackPending counter.

4 Higher level events, functions, and relations

The protocol that we described informally in the previous section is designed to achieve a specific aim—it has to meet a certain set of requirements—which is its correctness condition. When we prove the correctness of the protocol, we prove that each of its executions satisfies this correctness condition. The formulation of this correctness condition is in terms of the resulting higherlevel operation executions, and therefor we must first define these higher-level events. A higher-level event is a set of lower-level events that forms a certain task. We define three types of high-level events: MemoryAccess (which is divided into Load and Store), MemoryBarrier, and Commit.

A MemoryAccess higher-level event by P_{i} represents a complete execution of a Load/Store memory access initiated by a request made by P_{i}.

A Load event begins with the enqueue by P_{i} of the (Load, a) request on reqQ_{i}, and ends with the dequeue of that item by CAP_{i} which enqueues the return value on the resQ[P_{i}] immediately. The Load event also contains all the intermediate events executed by CAP_{i}, and (in case of a miss) the directory, and the owner of a which sent the copy.

A Store higher level event begins with the enqueue of the (Store, v, a) request on reqQ_{i}, and ends with the dequeue of that request by CAP_{i}. In case the execution is immediate (a hit) that high level event contains just these events. But in case the request is a miss, there are further sub-events beginning with CAP_{i} serving (reading) the request and sending the GetExclusive or ChangeToExclusive request to the directory.

A MemoryBarrier higher-level event by P_{i} is a set of just two lower-level events: the enqueue by P_{i} on reqQ_{i} of the MB request, and the dequeue of that request by the system process CAP_{i}.

We also introduce directory events into the collection of higher-level events. A higher-level Commit event is a singleton containing an execution by the directory of a request from one of the CAP_{i} processes connected with a Load/Store memory request. This request can be for a copy (GetShared or GetExclusive) or for an upgrade for an already cached value (ChangeToExclusive).

It may seem strange that we form singletons and take {r} as a Commit event instead of just r. This is done for uniformity’s sake so that we can define higher-level events as those events that have elements.

There are also initial higher-level events, which are not executions of requests but determine the initial values of the objects and the state of Mem.

4.1 Functions and relations

There are several higher-level functions and relations that we define here, that is functions and relations defined on the higher-level events. The Value function is defined on every higher-level Load and Store event L, with Value(L) ∈ Data. For a Load it is the value returned on the resQ queue, and for a Store it is the value requested to be written (namely the value on reqQ).

The most basic relation on the events is the temporal precedence relation <. For any events A and B, A < B iff A terminates before B begins. Since A and B can be incomparable, namely A ≮ B and B ≮ A, < is a partial ordering.

Relation <_{i} is the issue sequence order for P_{i}. It is the ordering of the higher-level events (Load, Store, and MB) as determined by the linear ordering of the corresponding request that were enqueued on reqQ_{i}. Namely, X_{1} <_{i} X_{2} iff X_{1} and X_{2} are higher-level (Store, Load, or MemoryBarrier) events by P_{i} with lower-level enqueues e_{1} ∈ X_{1} and e_{2} ∈ X_{2} on reqQ_{i} such that e_{1} was enqueued before e_{2} (that is e_{1} < e_{2}).

Since the directory is a serial process, the Commit events are linearly ordered, and <_{Dir} is the temporal precedence relation on the the Commit events. That is, for any Commit events c_{1} and c_{2}, c_{1}<_{Dir}c_{2} iff c_{1} < c_{2}.

The μ function is defined as follows on the Store/Load events which it maps into Commit events. Intuitively, if A is a memory access to address a by P_{i} then μ(A) is that Commit event in which the directory gave to P_{i} the right to access that location. There are two basic cases in the definition of μ(A).

Suppose first that A is a miss. Then CAP_{i} sends a request to the directory which is finally granted. (It is possible that a ChangeToExclusive request is denied, but then a following GetExclusive request is handled successfully.) Anyhow, the successful Commit event related to this request is defined to be μ(A). Observe that if A is a miss, then μ(A) is temporally included in A. Namely the temporal interval that represents μ(A) is a subinterval of the interval that represents A.

Now suppose that A is a hit. That is, A is a Store to a cache line for which the state is already PrimaryExclusive, or is a Load from a cache line that is not Invalid. In this case, there must exist a previous memory access by P_{i} to the same address, and for the latest such event A′, μ(A′) is already defined. So we define μ(A) = μ(A′). In this case, μ(A) < A, namely μ(A) temporally precedes A.

So μ is not necessarily one-to-one, but if μ(A_{0}) = μ(A_{2}) then A_{1} and A_{2} are P_{i} events for the same i and have the same address.

We make some easy but useful observations on μ and the possibility of inversion.

1. First observation is that if e_{1}, e_{2} are memory requests by P_{i} and e_{1} <_{i} e_{2}, if address(e_{1}) = address(e_{2}), then μ(e_{1})≤_{Dirctory}μ(e_{2}). The main point is that when CAP_{i} serves e_{2} and reads its reqQ_{i} request, the queue does not contain any request with address(e_{2}) that precedes e_{2}. So, e_{1} has been dequeued at that moment.

2. The second observation is that if m is a memory barrier event in P_{i} and a <_{i} m is a preceding memory access, then μ(a) < endμ(m). This is so since m can be retired from reqQ_{i} only when the ackPending counter of P_{i} is zero. Thus the directory message on DrCaQ_{i} associated with μ(a) has already been removed when m is retired.

3. A consequence of this is that if m is a memory barrier in P_{i} and a <_{i} m <_{i} b are two accesses issued before and after m, if b is a miss then μ(a)<_{Dir}μ(b).

5 Cache Coherence

The correctness condition of the protocol, called cache coherence, is a statement about higher-level events and we can now formulate it. It says that there exists a linear ordering called beforeOrder and denoted ⇐ of all Load, Store, and MemoryBarrier, instruction executions so that the following three conditions are met.

1. For every Load event R of address a there exists a Store event W, also of address a, such that:

(a) the value returned by R is the value of W,

(b) W ⇐R and there is no Store event W′ on address a such that W ⇐W′⇐R.

2. For every Store/Load events E_{1} and E_{2} issued by user process P_{i}, if E_{1} and E_{2} have the same address and the request for E_{1} is issued before the request for E_{2}, then E_{1}⇐E_{2}.

3. For every events E_{1} and E_{2} issued by P_{i}, if (at least one) of E_{1} and E_{2} is a MemoryBarrier event, then the issuing ordering is preserved. That is, if E_{1} is issued before E_{2} then E_{1}⇐E_{2}.

These conditions say that the system is allowed to execute the user’s requests in any order, and not necessarily in the issue ordering (in which they were inserted into their reqQ queue) provided it respects the ordering on events that have the same address and it does not change the ordering on events by P_{i} that have a MemoryBarrier event issued by P_{i} in between. We now understand the role of the MemoryBarrier events: to enforce a respect for the issuing ordering. A sequence of instructions issued in the ordering A, MB, B, ensure that A is executed before B.

6 Motivating χ and the Before Ordering

How shall we obtain the linear ordering ⇐ that satisfies the Cache Coherence requirements? It should be obvious that the directory with its serially ordered Commit events plays a central role in this definition. Using the function μ, defined above, we may try to define A⇐B iff μ(A)<_{Dir}μ(B) or else μ(A) = μ(B) and A <_{i} B (where P_{i} is the process of A and B, which is the same process if μ(A) = μ(B)). This, however, will not work as the following example demonstrates. Suppose that A is a Load event by P_{i} of address a. Then B is a Load of address b ≠ a by P_{i}, and A <_{i} B and μ(A)<_{Dir}μ(B). So A⇐B. Now let M be a MemoryBarrier event by P_{i} that follows B. Suppose that, after M, P_{i} has yet another Load of address a denoted C, and assume that when CAP_{i} executes C it finds address a to be valid in its Cache C_{i}[a] (by virtue of A). This implies that μ(C) = μ(A), and as μ(C)<_{Dir}μ(B) follows, we have that C⇐B. But B <_{i} M <_{i} C imply (by property 3) that B⇐M⇐C, and hence B⇐C which contradicts the assumption that ⇐ is an irreflexive ordering.

The function χ defined next correct this problem and provides the right definition of ⇐.

6.1 χ and the Before Ordering

We now define the χ function on the Store/Load events. It definition is based on μ.

Definition 6.1 χ: {h: Store(h) ∨ Load(h)} → Commit is defined as follows Let h be an arbitrary Load/Store event by P_{i}. Define the following set X of P_{i} events first.

X = {h} ∪ {x ∈ P_{i} | (Store(x) ∨ Load(x) and ∃m ∈ MB x <_{i} m <_{i} h }

Then define

χ(h) = {max \atop <_{Dir}}\{μ(x) | x ∈ X\}

For every Load/Store memory access h, χ(h) is properly defined since the set on which the maximum is taken is always a non-empty and finite subset of the linear ordering of Commit events. Note also that the statement μ(h)≤_{Dirctory} χ(h) is always true since h ∈ X.

Definition 6.2 For every Store/Load events h_{1} and h_{2} in MemoryAccess we define,

h_{1}⇐h_{2}iff ((χ(h_{1}) <_{Dir} χ(h_{2})) ∨ (χ(h_{1}) = χ(h_{2}) ∧ h_{1} < h_{2})).

Note that the relation ⇐, just defined, is a serial order of memory accesses. For every two memory access events, h_{1} and h_{2}, that belong to different processor χ(h_{1}) ≠ χ(h_{2}), and for every two events h_{1} and h_{2} that belong to the same processor h_{1} < h_{2} or h_{2} < h_{1}.

Definition 6.3 Let h be a Store/Load memory access: h is called an inversion iff μ(h)<_{Dir} χ(h).

If h is an inversion then h is a hit, since otherwise it is a miss and, as we have observed, mu(x)<_{Dir}μ(h) whenever x <_{i} m <_{i} h for some memory barrier m in P_{i}.

6.1.1 The source function

We define a function, denoted source, on the high-level Load events h: If h is a Load. Intuitively, the source of h is the Store that determined the value returned by h. So let h be any Load event of address a = address(h). Let μ(h) be the associated Commit event. There exists a Commit event c to address a such that c≤_{Dirctory}μ(h) and such that c = μ(h′) for some Store event h′. (For example, the initial Commit on a.) Let c_{0} be the latest such Commit in the ≤_{Dirctory} ordering. The set of Store events h′ such that μ(h′) = c_{0} is a non-empty subset of some P_{j}, and as P_{j} is linearly ordered by <_{j}, we can defined source(h) = h′ for the last Store h′ in that set.

In order to obtain a better understanding we describe different possibilities for the definition of source for a Load event h on address a by P_{i}.

1. Suppose that when CAP_{i} executes h, the state of the cache line at address a is PrimaryExclusive or PrimaryShared. Then there exists in P_{i} a Store event w such that w <_{i} h and μ(w) = μ(h). In fact, it is possible that there are several such Store events: the first one is a miss (or is the initializing Store event on address a), and the following stores are hit events. In any case, they are all in P_{i} and the last Store w such that μ(w) = μ(h) is defined to be source(h).

2. Suppose that when h is executed the state of C_{i}[a] is Secondary(so h is a hit Load). Then some previous Load in P_{i} has already obtained this status, and μ(h) is defined to be μ(e) where e <_{i} h is the <_{i} last Load of address(h) preceding h. We define source(h) = source(e).

3. Suppose that when h executes CAP_{i} finds the state of address a to be Invalid (so h is a miss). Then CAP_{i} sends a GetShared message to the directory which forms a commit event t = μ(h). In the Commit the directory consults M = Mem[a] and finds M.Writer = P_{j} for some j ≠ i. (The directory sends a ForwardedGet message to CAP_{j}, and finally P_{i} obtains a secondary copy of a.) In order to define source(h), we trace what caused the directory to set this value M.Writer = P_{j}. There has been a commit event c (and we take the last one preceding t) which set M.Writer = P_{j}. Then there exists a Store event s in P_{j} such that μ(s) = c. In fact, it is possible that there are several such Store events, and we define source(h) as the <_{j} last such Store.

6.2 The inversion lemmas

The following two lemmas are of prime importance for understanding how the protocol works.

Lemma 6.4 Let h be a Store memory access that is an inversion. Then there does not exist a commit event c such that

μ(h)<_{Dir} c <_{Dir} χ(h) and address(c) = address(h).

Lemma 6.5 Let h be any Load that is an inversion. Then there does not exist a Store memory access event h′ such that

μ(h)<_{Dir} μ(h′) <_{Dir} χ(h) and address(h′) = address(h).

7 The higher-level part of the correctness proof

This is the main section of our paper. We have been quite informal so far: we described the protocol by listing some of its possible scenarios. A more careful treatment would be to give a program in some computer language with a well-defined semantics that describes the protocol completely. We described the higher-level events but this too was done quite informally, and we defined the correctness condition (in Section 5). This definition was, again, informal (see the discussion below for what characterizes a formal definition and proof). All this informality suits best our intention which is to demonstrate that an informal, intuitive description of a protocol can benefit from a formal discussion of its higher-level events. So far we had the informal and intuitive description, and now it’s time for the formal part.

To carry a formal definition and proof we need first of all a formal language. Such a language can be a temporal logic language (for example the one used in [4]), but we prefer to use a predicate calculus language (first or second order) which is more common in ordinary mathematical discourse. To define a formal language one must give a list of its elements (predicates, function symbols, and constants) and rely on precise rules about the formation of expressions and formulas. Secondly, we need a mathematical definition of the class of structures (or interpretations) for the language defined, and we must define (or rely on a well-known definition of) the satisfaction relation “M satisfies ϕ” which holds for a structure M and sentence ϕ whenever ϕ is true in M (if ϕ is a formula with variables, then an assignment is also needed, which gives to each variable its value in M).

We define in this section a predicate calculus language, DCC, followed by a list of properties (“axioms”) and then prove that the desired cache coherence properties follow from the axioms.

7.1 Higher-level signature

The higher-level events are described in a language called DCC (for Directory Cache Coherence). The signature of this language is the following. There are three sorts, HL (for higher-level events), Address for the address space (set of all memory locations), and Data for the type of objects loaded and stored. We have the following predicates defined on the events HL.

1. Unary predicates: MemoryAccess, MemoryBarrier, Commit.

2. Unary predicates Load and Store.

3. Unary predicates P_{i} for i ∈ {1, …, N}.

4. Binary predicates <_{i} for i ∈ {1, …, N}. And binary predicate <_{Dir}.

5. Unary function Value is from the HL events into Data.

6. Unary functions μ and χ are from HL into HL.

7. Unary function source is from HL to HL.

8. unary function address from HL to Address.

7.1.1 Higher-level axioms

We have the following axioms (or properties) formulated in DCC.

Events: The set of events defined by the predicates MemoryAccess, MemoryBarrier, and Commit are pairwise disjoint. The sets Load and Store are disjoint. For every x, MemoryAccess(x) iff Load(x) ∨ Store(x). The events P_{0}, …, P_{N} are pairwise disjoint. Each MemoryAccess and MemoryBarrier is in some P_{i}. If P_{i}(x) then MemoryAccess(x) ∨ MemoryBarrier(x).

Orderings: Each <_{i} is a linear ordering of P_{i}. Every event e in P_{i} has only a finite number of events a in P_{i} such that a <_{i} e. Relation <_{Dir} is a linear ordering of the set of MemoryBarrier events. Again, each MemoryBarrier event e has only a finite number of MemoryBarrier events a such that a<_{Dir}e.

μ properties: The function μ is defined on the MemoryAccess events. For every event m such that MemoryAccess(m), Commit(μ(m)). For every MemoryAccess event m, address(m) = address(μ(m)) and Value(m) = Value(μ(m)). If μ(m_{1}) = μ(m_{1}), then m_{1} and m_{2} belong to the same process. That is, for some i P_{i}(m_{1}) and P_{i}(m_{2}).

For every MemoryAccess events m_{1} and m_{2} in P_{i}, if m_{1} <_{i} m_{2} and address(m_{1}) = address(m_{2}), then μ(m_{1})≤_{Dirctory}μ(m_{2}).

χ and ⇐: For every Load/Store event h by P_{i}:

χ(h) = max<_{Dir} ({μ(h)} ∪ {μ(h′) : Store(h′) ∨ Load(h′) and ∃mb ∈ MemoryBarrier h′ <_{i} mb <_{i} h})

For every events h_{1} and h_{2} that are MemoryAccess events we define:

h_{1}⇐h_{2} iff χ(h_{1})<_{Dir} χ(h_{2}) ∨ (χ(h_{1}) = χ(h_{2}) ∧ ∃i h_{1} <_{i} h_{2}).

Source: Let h be any Load event in P_{i}. There exists a Commit event c with address(c) = address(h) such that c ≤_{Dirctory} μ(h) and there is a Store event h′ such that μ(h′) = c. Moreover, let c_{0} denote the latest such Commit in the ≤_{Dirctory} ordering. Then either c_{0}<_{Dir}μ(h) or else c_{0} = μ(h) and then there exists a Store event h′ in P_{i} such that h′ <_{i} h and μ(h′) = c_{0}. Accordingly, there are two cases in the definition of source(h). In both cases source(h) is a maximal Store to have some stated properties.

1. In the first case c_{0} <_{Dir} μ(h), and source(h) = s where s is a Store event such that μ(s) = c_{0} and s′ <_{j} s for any other Store event s′in P_{j} (the process of s) such that μ(s′) = c_{0}.

2. In the second case c_{0} = μ(h), and then source(h) = s for the <_{i} latest Store event s such that s <_{i} h and μ(s) = c_{0}.

Value: If h is a Load event then Value(h) = Value(source(h)).

Inversion: Let h be a Store/Load event. h is called an inversion iff

μ(h)<_{Dir} χ(h).

1. Let h be a Store memory access, such that h is an inversion. Then there does not exist a commit event c such that μ(h)<_{Dir} c <_{Dir} χ(h) and address(c) = address(h).

2. Let h be a memory access such that h is an inversion. Then there does not exist a Store memory access event w, such that μ(h)<_{Dir} μ(w) <_{Dir} χ(h) and address(w) = address(h).

7.1.2 Correctness conditions

We must prove the following.

1. The beforeOrder relation ⇐ is a linear ordering on the Store/Load events.

2. If a <_{i} b and a, b access the same address, then a⇐b.

3. If a and b are Store/Load events in P_{i} and there exists a memory barrier event mb such that a <_{i} mb <_{i} b, then a⇐b.

4. For every Load event e:

(a) source(e) is a Store event. address(e) = address(source(e)) and Value(e) = Value(source(e)).

(b) source(e)⇐e.

(c) There is no Store event w with address(w) = address(e) such that source(e)⇐w⇐e.

Theorem 7.1 The axioms of 7.1.1 imply the correctness conditions 7.1.2.

We need the following lemma for the proof of the theorem.

Lemma 7.2 If S_{1}, S_{2} are memory accesses to the same address, and S_{1} <_{i} S_{2}, then χ(S_{1})≤_{Dirctory}χ(S_{2}).

Proof. By the μ properties, μ(S_{1})≤_{Dirctory}μ(S_{2}). Suppose for contradiction that χ(S_{2})<_{Dir}χ(S_{1}). Then μ(S_{1})≤_{Dirctory}μ(S_{2})≤_{Dirctory}χ(S_{2})<_{Dir}χ(S_{1}) shows that S_{1} is an inversion. The definition of χ(S_{1}) gives some Store event h′ and a memory barrier mb such that h′ <_{i} mb <_{i} S_{1} and χ(S_{1}) = μ(h′). But then, the same h′ also determines that μ(h′) ≤_{i} χ(S_{2}) which is a contradiction. ⊣

We prove 4(c) (all other items are very easy to prove). Suppose, for the sake of a contradiction, that there exists a Load event e by P_{i} on address a such that source(e)⇐w⇐e for some Store event w on address a. Let s = source(e) and P_{j} be the process of s.

We structure the proof in three cases:

Case 1: μ(w) = μ(e). Then w is in P_{i} and w <_{i} e (since w⇐e). The maximality of s = source(e) implies μ(s) = μ(e) and w <_{i} s. But then w⇐s, which is not the case.

Case 2: μ(s)≤_{Dirctory}μ(w). If μ(s) = μ(w), then the maximality of the source s implies that w <_{i} s and hence, again, w⇐s, which is not the case. If, however, μ(s)<_{Dir}μ(w), then μ(w)<_{Dir}μ(e) is excluded by the maximality of s, and μ(w) = μ(e) is excluded in Case 1. So we assume that μ(e)<_{Dir}μ(w). Since w⇐e, χ(w)≤_{Dirctory}χ(e). So

μ(e)<_{Dir}μ(w)≤_{Dirctory}χ(w)≤_{Dirctory}χ(e).  (1)

Thus e is an inversion. We cannot have μ(w)<_{Dir}χ(e) because in this case μ(e)<_{Dir}μ(w)<_{Dir}χ(e) contradicts Inversion.. Thus μ(w) = χ(w) = χ(e). Since w⇐e, χ(w) = χ(e) implies w <_{i} e. But then μ(w)≤_{Dirctory}μ(e) follows lemma 7.2 and contradicts (1). Since the Commit events are serially ordered, the following case remains.

Case 3: μ(w)<_{Dir}μ(s). We compare χ(w) with χ(s) and obtain a contradiction in each case.

(a) If χ(s)<_{Dir}χ(w) then

μ(w)<_{Dir}μ(s)≤_{Dirctory}χ(s)<_{Dir}χ(w)

implies μ(w)<_{Dir}μ(s)<_{Dir}χ(w) and contradicts Inversion.

(b) If χ(s) = χ(w), then s and w are both in P_{j}, and w <_{j} s (since otherwise s ≤_{j} w implies μ(s)≤_{Dirctory}μ(w) which contradicts our assumption μ(w)<_{Dir}μ(s)). Thus w⇐s, which is not the case.

(c) If χ(w)<_{Dir}χ(s) then w⇐s again.

8 Discussion and Conclusion

When the cache coherence protocol described here is studied, a natural question to ask concerns the role of the FillMarker messages sent by the directory to the CAP_{i} processes. All other messages seem quite natural and necessary, but the FillMarker messages seem to be redundant since the data flow directly through the fillQ that connect the CAP processes. A related question concerns the role of the ackPending counter maintained by each CAP_{i}. That process increases the counter on each message it sends to the directory, and decreases the counter whenever a FillMarker or a ChangeToExclusiveAck message is dequeued from DrCaQ_{i}. The counter is used whenever a memory barrier message is dequeued from the request queue reqQ_{i}: the counter has to be zero in order for this dequeue to be enabled.

The first answer to these question is through examples that show what could go wrong if the FillMarker messages are omitted. Here is an example.

Suppose in P_{i} a Store events, s, on address a, followed by a Store, t, on address b, followed by a MemoryBarrier event mb, followed by a Load, u, of address a again. So s <_{i} t <_{i}<_{i} mb <_{i} a. We also assume a Store, w, by another process P_{j}, on address a, such that μ(s)<_{Dir}μ(w)<_{Dir}μ(t) and μ(s) = μ(u), as shown in Figure 2.

When the directory received the GetExclusive message from CAP_{j} (on behalf of w) it found that P_{i} is the owner of address a and sent a ForwardedGet message M to P_{i}, which however was not received immediately. The directory then received the GetShared message on behalf of t,

[figure: s; t; mb; u; w; mu(w); mu(s); mu(t)]

Figure 2: A bad scenario of what could happen if the FillMarker messages are eliminated.

and sent to the owner of b a ForwardedGet message, which caused a fill to be sent to CAP_{i}. We assume that the fill was received before the memory barrier event MB. Since message M has not yet arrived when u has executed, CAP_{i} executed u immediately on the local copy of a, and returned the value written by s. Since χ(u) = μ(t), w⇐u. Now we have the following situation: s⇐w⇐u but u returned the value of s instead of that of w.

The ackPending counter prevents this situation, since it ensures that the FillMarker sent by μ(t) is dequeued before the memory barrier request is dequeued. Since the CaDrQ is FIFO, the ForwardedGet message M must also be dequeued before, and hence CAP_{i} has invalidated its copy of a. Thus when u executes it is unsuccessful. This scenario is just one of several bad ones that may occur if the FillMarker messages are omitted. The general proof that the algorithm is correct need the two lemmas, and the explanation of why these lemmas suffice is given in fact by the proof in Section 7.

Example are certainly useful for the understanding process, but deeper answers are provided by general considerations and mathematical proofs. Our answer to the questions concerning the role of the FillMarker messages and the ackPending counters is given in section 7 which is in a way the main section of the paper. Namely, the FillMarker messages and the counters ensure that lemmas hold, and thus enable the proof of correctness (mainly the proof of ).

The higher-level proof that is given in section 7 is useful not only to enhance

There is a vast literature on formalization of correctness proofs of algorithms, and much research is published on the question of specifying and proving correct concurrently operating protocols. Although explaining and understanding concurrent protocols is a major endeavor of many, this part of our activity has remained an art left to the individual talent of researchers and students. One can argue that “formal explanation” is a contradiction in terms: an explanation is general, pictorial, and informal. It should not be confused with the formal mathematical proof that one must give to a protocol in order to show its correctness. We have argued in this paper that a formal correctness proof can be incorporated in the learning process, and we suggested the higher level properties rather than the minute details of the protocol text as the vehicle for understanding.

The correctness conditions of concurrent protocols are often stated by reference to higher-level events (those events that are obtained as collections of lower-level events). Our experience is that the correctness proofs of many protocols can be presented in a two tier fashion. The lower-level part deals directly with the protocol’s text and proves that whenever the protocol is executed and its lower-level events are collected into higher-level events, then these events satisfy some simple, abstract properties which we call “higherlevel axioms”. The higher-level part of the correctness proof is proving that the axioms logically imply the correctness conditions which the protocol has to fulfill. The thesis offered in this paper is that the second part of the proof, the one that deals with higher-level events and their properties, can serve as a formal explanation of the protocol.

References

[1] U. Abraham, Models for Concurrency, Gordon and Breach, 1999.

[2] Concurrency without global states: a case study. In preparation.

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

[4] L. Lamport. Specifying concurrent systems with TLA^{+}. In Manfred Broy and Ralf Steinbrüggen, editors, Calculational system Design, pages 183-247, Amsterdam, 1999. IOS Press.

[5] L. Lamport, M. Sharma, M. Tuttle, and Y. Yu. The Wildfire Challenge Problem. 2001.