An Operational Model for Multiprocessors with Caches

Salil Joshi^{⋆} and Sanjiva Prasad^{⋆⋆}

Indian Institute of Technology Delhi

Abstract. Modern multiprocessors are equipped with local caches, to enhance program performance. However, the presence of caches can lead to the violation of sequential consistency [7] assumptions regarding program order and write atomicity. With respect to such relaxed memory models [1], we provide an operational description of program execution (in the style of [4]) that accounts for cache effects. In particular, we provide an operational characterization of cache invalidation and update policies and an abstract characterization of cache consistency. The programming model consists of a simple imperative language extended with common synchronization primitives such as locks or barrier instructions. The main results show that by precluding certain data races or by placing certain synchronization constraints, sequentially consistent behavior can be obtained for multiprocessor execution even in the presence of local caches.

1 Introduction

While shared memory multiprocessor systems are becoming increasingly common today, writing correct concurrent programs for such systems remains a challenge. Program behavior is determined by a memory model. Programmers commonly assume a model of memory that is sequentially consistent [7], i.e., all memory accesses appear to occur atomically in some total order, and those issued by any given processor occur as specified by the program order.

One feature for improving performance, found in all modern processors, is a cache. The presence of caches in a multiprocessor system can lead to violations of program order and write atomicity assumptions [1]. The goal of this work is to understand the effect of caches on concurrent program execution with respect to a weaker memory model where these assumptions are relaxed [2], and to discover constraints under which sequentially consistent behavior is guaranteed.

We follow the approach of Boudol and Petri [4] in presenting an operational model of memory and describe the execution of programs written in a simple imperative language with respect to a sequentially consistent model (“the specification”), and then with respect to a relaxed model (“the implementation”). We then consider some synchronization primitives (called “safety nets” in [1]) supported by the model; these are instructions used to temporarily force program

⋆ salil.ssj@gmail.com ⋆⋆ sanjiva@cse.iitd.ac.in

order or write atomicity in order to make the program behavior more manageable. In particular, we show that for locks a well synchronizedness condition (equivalent to data-race-freedom), and for barrier instructions, a multiple-race-free barrier condition, are sufficient to ensure sequentially consistent behavior in an otherwise non-sequentially consistent system.

Technically, this is done by establishing precise correspondences (e.g., “bisimilarity”) between the specification and implementation behaviors. The consequence of these results is that for programs satisfying these constraints (which are stated at the specification level), the programmer need only consider the more intuitive set of sequentially consistent executions rather than all possible executions, when reasoning about program behavior.

A novel contribution in this paper is an abstract operational characterization of a memory model, general enough to express multiprocessor memory with local caches as a particular instance, in terms of a small set of operational properties. The theorems are thus proven for any memory model exhibiting these properties. We believe that our implementation semantics closely resemble actual processor architectures (with caches). At the same time, the semantics abstract over processor specific details like cache replacement policies, cache consistency protocols etc. Thus our models (and hence our theorems) should hold for a wide variety of multiprocessor systems. We give an example of a cache-based system which exhibits the required properties, and which allows the following relaxations with respect to the classification of relaxed memory models in [1]:

1. W → R: Reordering of a write with a following read to a different variable.

2. W → W: Reordering of a write with a following write to a different variable.

3. Read other’s write early: This violates write atomicity.

4. Read own write early: This violates both write atomicity and program order.

Our approach differs from that of Boudol and Petri [4] in several ways: (i) while they present a higher-order language with ML-style imperative features, dynamic thread creation and scoped locks, we prefer a simple imperative language that we believe has greater applicability; (ii) in addition to locks, we consider synchronization primitives such as barrier or fence instructions; (iii) while Boudol et al consider write buffers, we believe we consider a more general multiprocessor model with caches, while being able to deal with a variety of cache management policies (update, invalidation). Furthermore our operational characterization is presented in terms of abstract properties.

The rest of this paper is organised as follows. §2 presents the language and the specification semantics. The abstract characterization of the implementation semantics is given in §3 as a collection of properties on the operational relation. §4 introduces scoped locks as a synchronization primitive and shows sequential consistency can be ensured by data race freedom; similarly a barrier condition is shown to achieve this when using barrier instructions (§5). In §6, we present an intuitive model of caches which satisfies the abstract properties of §3.2. §7 concludes the paper with some directions for future work. Proofs of lemmas and theorems are omitted in this paper but can be found in [6].

2 The Language

We employ a simple imperative language, which will later be extended with two different synchronization primitives.

⟨e⟩ ::= ⟨int⟩ ; | ⟨e⟩ ⊕ ⟨e⟩ ; | ⟨var⟩ ⟨b⟩ ::= true | false | ¬ ⟨b⟩ | ⟨b⟩ ∧ ⟨b⟩ | ⟨e⟩ ≤ ⟨e⟩

⟨C ⟩ ::= ⟨var⟩ := ⟨e⟩
| ⟨C ⟩; ⟨C ⟩
| if ⟨b⟩ then ⟨C ⟩ else ⟨C ⟩
| while ⟨b⟩ do ⟨C ⟩

All variables are integer valued, boolean values are used only for tests and the ⊕ operator is any one of +, ∗, … We also have a runtime marker, (), which is ‘returned’ when a command is executed. It is used only to make the operational semantics easier to formulate.

2.1 Specification Semantics

A configuration ℂ is a pair (S, P), where S is the store (main memory) that is shared across the system, and P is a list of processes. Each process runs on its own processor. The store is common to all, and is a simple mapping from variable names to integers. For convenience, we will use ℂ.S and ℂ.P to refer to the store and program respectively of a specific configuration ℂ.

Transitions involve reducing a redex in an evaluation context [10]. An evaluation context consists of a number i (indicating that the process P_{i} is being executed), and a one-hole context. We use P_{i}[E[]] to denote the hole E[] in the i^{th} process in P.

The redexes and one-hole contexts (E[]) are as follows:

⟨bval⟩ ::= true | false ⟨redex⟩ ::= ⟨int⟩ ⊕ ⟨int⟩ | ⟨int⟩ ≤ ⟨int⟩ | ¬ ⟨bval⟩ | ⟨bval⟩ ∧ ⟨bval⟩ | ⟨var⟩ | ⟨var⟩ := ⟨int⟩ | if ⟨bval⟩ then ⟨C ⟩ else ⟨C ⟩ | while ⟨b⟩ do ⟨C ⟩ | ();⟨C ⟩ ⟨E⟩ ::= [] | E ⊕ ⟨e⟩ | ⟨int⟩ ⊕ E | E ≤ ⟨e⟩ | ⟨int⟩ ≤ E | ¬ E | E ∧ ⟨b⟩ | ⟨bval⟩ ∧ E | ⟨var⟩ := E| E;⟨C ⟩ | if E then ⟨C ⟩ else ⟨C ⟩

The operational semantics are given in Figure 1. We have left out the obvious transitions such as those for the arithmetic and boolean operators.

Transitions are decorated as: ⟶^{(a,i)}. Here i is used to indicate that the transition is for process P_{i}, and a denotes the action being carried out. The possible actions are: τ (reduction which does not involve the store), rd_{x}^{v} (the value v is read from variable x) and wr_{x}^{v} (the value v is written to the variable x). For reads and writes we will use rd_{x} and wr_{x} when we do not care what value was read/written. Concurrent, conflicting transitions are said to form a race:

Definition 1. In a sequence of transitions ℂ_{0} ⟶^{(a_{0},i_{0})} ⋯ ⟶^{(a_{n},i_{n})} ℂ_{n+1}, two

transitions ⟶^{(a_{j},i_{j})} and ⟶^{(a_{k},i_{k})} are said to form a race if i_{j} ≠ i_{k} and a_{j}, a_{k} ∈ {rd_{x}, wr_{x}} and at least one is wr_{x}.

(S, P_{i}[E[x]]) ⟶^{(rd_{x}^{v},i)} (S, P_{i}[E[v]]) where S(x) = v

(S, P_{i}[E[x:=v]]) ⟶^{(wr_{x}^{v},i)} (S[x ← v], P_{i}[E[()]])

(S, P_{i}[E[(); C]]) ⟶^{(τ,i)} (S, P_{i}[E[C]])

(S, P_{i}[E[if true then C_{t} else C_{f}]) ⟶^{(τ,i)} (S, P_{i}[E[C_{t}]]) (S, P_{i}[E[if false then C_{t} else C_{f}]) ⟶^{(τ,i)} (S, P_{i}[E[C_{f}]]) (S, P_{i}[E[while b do C]]) ⟶^{(τ,i)} (S, P_{i}[E[if b then {C; while b do C} else ()]])

Fig. 1. Specification Semantics

(M, P_{i}[E[x]]) ⟶^{(rd_{x}^{v},i)} (M′, P_{i}[E[v]]) where M_{i}[x] = (M′, v) (M, P_{i}[E[x:=v]]) ⟶^{(wr_{x}^{v},i)} (M′, P_{i}[E[()]]) where M_{i}[x ← v] = M′

Fig. 2. Implementation Semantics

Specification semantics correspond to a programmer’s intuitive view of interleaving execution (i.e. a sequentially consistent memory model). Here, processes execute one at a time (conceptually) albeit in a non-deterministic order, program order is respected and writes are atomic. Storage features such as caches and write buffers can violate these guarantees in a multiprocessor setting [1].

3 Implementation Semantics

In the implementation semantics, we replace the store S with a more general abstraction for memory, denoted as M. Each processor has a different view of the memory; processor i sees the value of x as M_{i}[x] and in general M_{i}[x] and M_{j}[x] need not be equal. We will use M to model a memory hierarchy where each processor has a local cache. Our semantic account abstracts from the internal structure of M. We place purely operational constraints on M in order to prove sequential consistency theorems and later show that common cache based architectures satisfy these constraints. Thus while our focus is on the effects of caches, the framework presented here is more general.

In Figure 2 we present the significant changes to the operational rules. We omit the rules of Figure 1 that do not involve memory.

Both wr_{x}^{v} and rd_{x}^{v} transitions access the memory, and potentially alter it. Writing a variable (denoted M_{i}[x ← v]) returns the modified memory M′. Reading a variable from memory (denoted M_{i}[x]) returns a pair (M′, v) where v is the value read, and M′ is the possibly modified memory (e.g. an altered cache). For convenience, we write M_{i}[x].val = v when M_{i}[x] = (M′, v). The next section imposes some restrictions on the permissible changes in M′.

In addition, we have some more transitions called the ‘system’ transitions, denoted by ⟶. These are used by the system to manage the internal structure of the memory. We will use → moves later e.g. to model cache consistency and cache replacement protocols. These transitions can fire non-deterministically at any time. Moreover, the program does not constrain which system transitions can occur, or when. We abstractly characterize the system transitions in §3.2 by a series of properties which we use in the sequel. In particular the model described in §6 implements M as a cache based system satisfying these properties.

The transitions introduced in Figures 1 and 2 are now called ‘program’ transitions (since they fire as a direct result of some piece of code). We will use ℂ →_{I}^{∗} ℂ′ to denote that ℂ′ is reachable from ℂ by the implementation semantics (program and system transitions), and similarly ℂ →_{S}^{∗} ℂ′′ for the specification semantics. Note that we will use ⟶^{∗} to denote 0 or more system transitions, whereas →_{I}^{∗} means 0 or more system and program transitions.

3.1 Coherence and Consistency

Let us call a configuration ℂ “→-normal” if it cannot make any ⟶ moves (i.e. system transitions). In order to relate implementation semantics to specification semantics, we need the following definition:

Definition 2. An implementation configuration ℂ_{I} is said to reduce to a specification configuration ℂ_{S} (written ℂ_{I} ⇓ ℂ_{S}) if ∃ℂ′_{I} : ℂ_{I} ⟶^{∗} ℂ′_{I}, ℂ′_{I} is →-normal, and ∀i∀x ℂ′_{I}.M_{i}[x].val = ℂ_{S}.S[x]. ℂ_{S} is called a reduct of ℂ_{I}.

In the next subsection we impose conditions that ensure the existence of reducts.

Definition 3. ℂ is coherent for x if ∃v : ∀ℂ_{S} : ℂ ⇓ ℂ_{S}, ℂ_{S}.S(x) = v.

A configuration is coherent if it is coherent for all x. It follows that a coherent configuration has a unique reduct. We use ^{⌜}ℂ^{⌝} to refer to the unique reduct of a coherent configuration ℂ.

Definition 4. ℂ is consistent for x if (a) it is coherent for x, (b) ∀i, j, ℂ.M_{i}[x].val = ℂ.M_{j}[x].val, (c) ∀ℂ_{S}, ℂ ⇓ ℂ_{S} ⇒ ∀i, ℂ.M_{i}[x].val = ℂ_{S}.S(x) and (d) ∀i, w if ℂ′ is the same as ℂ except that ℂ′.M = ℂ.M_{i}[x ← w], then ℂ′ is coherent for x.

Condition (a) ensures that a consistent configuration is coherent, and (d) that it remains coherent after any single write. Thus there are no pending writes to x in a configuration that is consistent for x. Condition (b) ensures that all views of x coincide and (c) that it agrees on x with its reducts. ℂ is consistent if it is consistent for all x. A consistent configurations is in some sense identifiable with its reduct.

3.2 Constraints on the Memory Model

We now present the properties that the memory structure and its system transitions should satisfy. The theorems in the following sections hold for any system which has these properties.

Property 1 If ℂ → ℂ′, then ℂ.P = ℂ′.P

System transitions have no effect on the program.

Property 2 An →-normal configuration is consistent.

Property 2 ensures that system transitions are adequate to ensure consistency. For example, it prevents pathological cache architectures where the contents of only one designated cache are copied to the rest. In this pathological system, in the absence of a cached entry in the designated cache, inconsistent →-normal configurations are possible.

Property 3 Every configuration reachable from a consistent configuration has at least one →-normal configuration under ⟶^{∗}.

We restrict this condition to configurations reachable from a consistent configuration because we always begin with a consistent configuration in practice. The above two properties together mean that such a configuration has at least one reduct. They also imply that any such configuration can always become consistent, which is important for the synchronization primitives of the sequel.

Property 4 Consider ℂ_{I} ⟶^{∗}⟶^{(a,i)} ℂ′_{I}. For any ℂ′_{S} such that ℂ′_{I} ⇓ ℂ′_{S}, ∃ℂ_{S} : ℂ_{I} ⇓ ℂ_{S} which is identical to ℂ′_{S} except in the position of the redex in P_{i}, unless ℂ′_{S}.S(x) = v and a = wr_{x}^{v} in which case ℂ_{S}, ℂ′_{S} may also differ on S(x).

Property 4 states that only writes may make a fundamental change in M, and only to a single variable. Reads are allowed to change M, but the change is superficial in this sense (and usually done solely for performance reasons).

Property 5 If ℂ is coherent (resp. consistent) for x and ℂ → ℂ′, then ℂ′ is also coherent (resp. consistent) for x.

Property 5 states that system transitions preserve coherence and consistency.

Property 6 Let ℂ be consistent for x and consider the sequence ℂ ⟶^{∗}⟶^{(a_{0},i_{0})}

… ⟶^{∗}⟶^{(a_{n},i_{n})} ℂ′. If there is at most one processor i such that (a_{k}, i_{k}) = (wr_{x}, i) in this sequence then ℂ′ is coherent for x.

Property 6 says if there is no conflicting write then coherence is maintained.

Property 7 If ℂ is consistent, ℂ →_{I}^{∗} ℂ′ then for any i, if ℂ′.M_{i}[x].val = v then either ℂ.M_{i}[x].val = v or there is a wr_{x}^{v} on some processor in ℂ →_{I}^{∗} ℂ′.

Property 7 states that a value is either set by some write or is preserved.

Property 8 Let ℂ be consistent for x, ℂ →_{I}^{∗} ℂ_{I} ⟶^{(a,i)} ℂ′_{I}, and ℂ′_{I} ⇓ ℂ′_{S}. If a ∈ {wr_{x}^{v}, rd_{x}^{v}} and ℂ′_{S}.S(x) = w ≠ v then there exists a transition (wr_{x}^{w}, j) with j ≠ i in ℂ →_{I}^{∗} ℂ_{I}.

Property 8 means that the last write cannot be ignored and the last read cannot read the wrong value, unless they form a race with some earlier transition. System transitions must ensure that the effects of a write can propagate.

3.3 Derived Properties

The following lemmas can be derived from the above constraints.

Lemma 1. If ℂ is coherent for x, ℂ ⟶^{(a,i)} ℂ′ and a ≠ wr_{x} then ℂ′ is coherent for x.

Any transition not involving a write on x will maintain coherence for x.

Lemma 2. Let ℂ be reachable from a consistent configuration. If ℂ is consistent

for x, ℂ →_{I}^{∗} ℂ_{I} ⟶^{(a,i)} ℂ′_{I}, ℂ_{I} is coherent and ℂ_{I} ⇓ ℂ_{S}, then ∃ℂ′_{s} such that following diagram commutes:

\xymatrix{ℂ_{I} \ar[r]^{(a,i)} \ar@{=>}[d] & ℂ′_{I} \ar@{=>}[d] \\ ℂ_{S} \ar[r]^{(a,i)} & ℂ′_{S}}

where either a is not a memory access or if a accesses x then in ℂ →_{I}^{∗} ℂ_{I} there is a wr_{x} transition only on i.

By Properties 2, 3, 4 and 8. This lemma means that a write-free sequence of transitions exactly implements the specification semantics.

The following is a useful special case of this lemma:

Lemma 3. If ℂ_{I} is a consistent configuration then ∃ℂ′_{S} which makes the following diagram commutes:

\xymatrix{ℂ_{I} \ar[r]^{(a,i)} \ar@{=>}[d] & ℂ′_{I} \ar@{=>}[d] \\ ^{⌜}ℂ_{I}^{⌝} \ar[r]^{(a,i)} & ℂ′_{S}}

We are now ready to consider two synchronization primitives in turn, and give sufficient conditions for sequential consistency for each.

4 Locks

We extend our language with a locking construct, with l do ⟨C⟩ following the approach of [4].

⟨C ⟩ ::= … | with l do ⟨C ⟩ ⟨E⟩ ::= … | holding l do ⟨E⟩

⟨redex⟩ ::= … | with l do ⟨C ⟩ | holding l do ()

Additionally we have a construct holding l do ⟨C ⟩ which is a runtime construct. It is used when a lock is held, and ⟨C ⟩ is being executed. In the following subsection, we assume that the initial configuration we consider is written in the source language, and thus has no runtime constructs.

The configurations also change, becoming (S, L, P) (specification) and (M, L, P) (implementation) where L is the set of locks that are currently held. L remains

(S, L, P_{i}[E[with l do C]]) ⟶^{(l̂,i)} (S, L ∪ {l}, P_{i}[E[holding l do C]]) where l ∉ L (S, L, P_{i}[E[holding l do()]]) ⟶^{(ľ,i)} (S, L − {l}, P_{i}[E[()]])

Fig. 3. Locks: Specification Semantics

(M, L, P_{i}[E[with l do C]]) ⟶^{(l̂,i)} (M, L ∪ {l}, P_{i}[E[holding l do C]]) where l ∉ L (M, L, P_{i}[E[holding l do ()]]) ⟶^{(ľ,i)} (M, L − {l}, P_{i}[E[()]]) configuration is consistent

Fig. 4. Locks: Implementation Semantics

unaffected by all the transitions given so far, appearing unchanged on both sides. We introduce two new transitions for locking, with the decorations: l̂ (acquire lock l) and ľ (release lock l). The specification and implementation semantics for locks are given in Figures 3 and 4 respectively.

A lock l can only be acquired by a process if no other process holds l. Also, in the implementation semantics a lock can only be released when the configuration is consistent. Recall that Properties 2 and 3 ensure that this can happen.

4.1 Sequential Consistency

A sufficient condition to ensure sequential consistency even in the implementation semantics, is that the initial configuration must be Data Race Free (DRF):

Definition 5. A consistent configuration ℂ involves a data race if it has two redexes P_{i}[E[r]] and P_{j}[E[r′]]], i ≠ j, r and r′ are both accesses to the same variable and at least one is a write. ℂ is data race free (DRF) iff no configurations specification reachable from ^{⌜}ℂ^{⌝} involve a data race.

The following definition for well synchronizedness is often taken to be synonymous with DRF, and we treat it as such. Boudol and Petri’s proof [4] of their equivalence applies to our model nearly unchanged since the proof is at the specification level, and our specification semantics are essentially the same as their ‘strong’ semantics. The full proof can be found in [6].

Definition 6. A consistent configuration ℂ is said to be well-synchronized (WS),

iff in any valid sequence of specification transitions^{⌜}ℂ^{⌝} = ℂ_{0} ⟶^{(a_{0},i_{0})} … ⟶^{(a_{n−1},i_{n−1})} ℂ_{n} if there exists n_{1} and n_{2} (with n_{1} < n_{2}) such that (a_{n_{1}}, i_{n_{1}}) and (a_{n_{2}}, i_{n_{2}}) form a race, then ∃n_{3} : n_{1} < n_{3} < n_{2} ∧ i_{n_{3}} = i_{n_{1}} ∧ a_{n_{3}} = ľ.

For proofs, we will use this characterization rather than Definition 5. Informally, this property means that there must exist an unlocking operation between every pair of transitions forming a race (in every sequence of specification transitions). Note that we need only analyze sequentially consistent executions of a program in order to determine whether it is WS.

There is one last definition that is required in order to prove that the implementation and specification semantics coincide for WS programs.

Definition 7. For any given consistent configuration ℂ, define R(ℂ) as: (ℂ_{I}, ℂ_{S}) ∈ R(ℂ) if and only if there exists a sequence of implementation transitions

ℂ = ℂ_{0} ⟶^{∗}⟶^{(a_{0},i_{0})} ℂ_{1} ⋯ ⟶^{∗}⟶^{(a_{n},i_{n})} ℂ_{n} = ℂ_{I}

such that

⌜ℂ^{⌝} = ℂ′_{0} ⟶^{(a_{0},i_{0})} ℂ′_{1} ⋯ ⟶^{(a_{n},i_{n})} ℂ′_{n} = ℂ_{S}

is a valid sequence of specification transitions, with ℂ_{j} ⇓ ℂ′_{j} for all j.

We show that if ℂ is WS then the relation R(ℂ) is a bisimulation (and thus the specification and implementation semantics are essentially the same).

In one direction, the simulation holds whether or not ℂ is WS.

Theorem 1. If (ℂ_{I}, ℂ_{S}) ∈ R(ℂ) and ℂ_{S} ⟶^{(a,i)} \overline{ℂ}_{S} then there exists \overline{ℂ}_{I} with

ℂ_{I} ⟶^{∗}⟶^{(a,i)} \overline{ℂ}_{I} such that (\overline{ℂ}_{I}, \overline{ℂ}_{S}) ∈ R(ℂ).

The other direction also holds when the configuration is WS. Further, coherence is maintained.

Theorem 2. If (ℂ_{I}, ℂ_{S}) ∈ R(ℂ) (with WS ℂ), ℂ_{I} is coherent and ℂ_{I} ⟶^{∗}⟶^{(a,i)}

\overline{ℂ}_{I} then \overline{ℂ}_{I} is coherent and there exists \overline{ℂ}_{S} such that ℂ_{S} ⟶^{(a,i)} \overline{ℂ}_{S} with (\overline{ℂ}_{I}, \overline{ℂ}_{S}) ∈ R(ℂ).

5 Barriers

Barriers or fences are a common safety net in various processors with a relaxed memory model [1] and have also been used in other contexts [3]. Their role is to prevent instruction re-ordering across the barrier (hence the name). Unlike locks, they cannot entirely prevent data races but they can still guarantee sequential consistency (at least with the semantics that we present below).

We extend our language with a bar command, and a new expression for barred reads:

⟨e⟩ ::= … | !⟨var⟩  ⟨C ⟩ ::= … | bar  ⟨redex⟩ ::= … | bar | !⟨var⟩

The one-hole contexts remain unchanged. We introduce a barrier transition, decorated with bar. In the specification semantics, this is a no-op. In the implementation, it is a way of waiting for pending writes to complete. Figures 5 and 6 give the specification and implementation semantics respectively. The new read is only a way of introducing a barrier in the middle of an expression. The actual read is still handled by the usual rd_{x}^{v} actions.

Note that our barrier semantics enforces a global constraint. Hardware implementations today often provide barriers whose effects are in some way local to the current processor (e.g. x86 mFence) but as noted in [9], this is insufficient to ensure sequential consistency.

(S, P_{i}[E[bar]]) ⟶^{(bar,i)} (S, P_{i}[E[()]]) i.e. do nothing (S, P_{i}[E[!x]]) ⟶^{(bar,i)} (S, P_{i}[E[x]]) i.e. do nothing

Fig. 5. Barriers: Specification Semantics

(M, P_{i}[E[bar]]) ⟶^{(bar,i)} (M, P_{i}[E[()]]) configuration is consistent (M, P_{i}[E[!x]]) ⟶^{(bar,i)} (M, P_{i}[E[x]]) configuration is consistent

Fig. 6. Barriers: Implementation Semantics

5.1 Sequential Consistency

An important difference between this and the lock model is that in general, it is not possible to place bars in the program in a way that ensures that there is a bar between every pair of actions forming a race in every sequentially consistent execution. Instead, we achieve sequential consistency by preventing multiple races involving the same processor from appearing between a pair of bars.

Definition 8. A sequence of transitions ℂ →_{I}^{∗} ℂ′ (resp. ℂ →_{S}^{∗} ℂ′) is called multiple race free iff for every k such that (a_{k}, i_{k}) forms a race with some transition in the sequence, if ∃j : j ≠ k ∧ i_{j} = i_{k} then (a_{j}, i_{j}) does not form a race with any transition in the sequence.

Definition 9. A consistent configuration ℂ is said to satisfy the barrier con-

dition iff in any valid sequence of specification transitions ^{⌜}ℂ^{⌝} = ℂ_{0} ⟶^{(a_{0},i_{0})}

ℂ_{1} … ℂ_{n} ⟶^{(a_{n},i_{n})} ℂ_{n+1}, if there are bar transitions at {k_{1}, k_{2}, …, k_{m}} then taking k_{0} = 0 and k_{m+1} = n+1, each subsequence in {ℂ_{k_{i}} →_{S}^{∗} ℂ_{k_{i+1}}|0 ≤ i < n+1} is multiple race free.

As in the case for WS, we need only analyze sequentially consistent executions of a program to verify that it satisfies the barrier condition.

To prove the equivalence of the two semantics under this condition, we show that for every specification-reachable configuration there is an implementationreachable configuration, and vice-versa. One direction is quite trivial, and the barrier condition is not required:

Theorem 3. For any consistent configuration ℂ, for every specification configuration ^{⌜}ℂ^{⌝} →_{S}^{∗} ℂ_{S}, there exists an implementation configuration ℂ_{I} such that ℂ →_{I}^{∗} ℂ_{I} and ℂ_{I} ⇓ ℂ_{S}.

Theorem 4. For any consistent configuration ℂ which satisfies the barrier condition, for every implementation configuration ℂ_{I} such that ℂ →_{I}^{∗} ℂ_{I} and every specification configuration ℂ_{S} such that ℂ_{I} ⇓ ℂ_{S}, ^{⌜}ℂ^{⌝} →_{S}^{∗} ℂ_{S}.

In order to prove this theorem, we need the following lemmas:

(S, C, P_{i}[E[x]]) ⟶^{(rd1_{x}^{v},i)} (S, C, P_{i}[E[v]]) where x ∈ dom(C_{i}) ∧ C_{i}[x].val = v

(S, C, P_{i}[E[x]]) ⟶^{(rd2_{x}^{v},i)} (S, C, P_{i}[E[v]]) where x ∉ dom(C_{i}) ∧ S(x) = v

(S, C, P_{i}[E[x]]) ⟶^{(rd3_{x}^{v},i)} (S, C_{i}[x ← (v, clean)], P_{i}[E[v]]) where x ∉ dom(C_{i}) ∧ S(x) = v (S, C, P_{i}[E[x:=v]]) ⟶^{(wr_{x}^{v},i)} (S, C_{i}[x ← (v, dirty)], P_{i}[E[()]])

Fig. 7. Implementation Semantics

Lemma 4. Consider a consistent configuration ℂ, and a configuration ℂ_{I} such

that ℂ ⟶^{∗}⟶^{(a_{0},i_{0})} ⋯ ⟶^{∗}⟶^{(a_{n},i_{n})} ℂ_{I}. If this sequence is multiple race free, then for

every ℂ_{S} such that ℂ_{I} ⇓ ℂ_{S} there exists a sequence ^{⌜}ℂ^{⌝} ⟶^{(b_{0},j_{0})} ⋯ ⟶^{(b_{n},j_{n})} ℂ_{S}. Furthermore, the sequence of pairs {(b_{k}, j_{k})} is a permutation of the sequence {(a_{k}, i_{k})}.

Lemma 5. For any consistent configuration ℂ which satisfies the barrier condition, for every implementation configuration ℂ_{I} such that ℂ →_{I}^{∗} ℂ_{I} and every specification configuration ℂ_{S} such that ℂ_{I} ⇓ ℂ_{S}, the following hold:

1. The sequence ℂ →_{I}^{∗} ℂ_{I} is multiple race free between bars.

2. ^{⌜}ℂ^{⌝} →_{S}^{∗} ℂ_{S}.

3. The sequence ^{⌜}ℂ^{⌝} →_{S}^{∗} ℂ_{S} is a barrier-bounded permutation of (the program transitions in) ℂ →_{I}^{∗} ℂ_{I}.

6 Modeling Multiprocessors with Caches

This section gives examples of how a multiprocessor system with local caches can be modeled in our framework. The memory M now becomes a tuple (S, C), where S is a store (as in the specification semantics) and C is a set of |P | caches. The caches contain a local copy of a subset of the store. When a variable is written to, the write is to the cache. System transitions are used to update the store and the other caches asynchronously at some later time. A read may also pull a variable into the cache.

If x ∈ dom(C_{n}) then this means the n^{th} processor has x in its cache. Its value C_{n}[x] is given by a pair (val, state), where val is the ordinary integer value of the variable and state may be either clean or dirty. A variable is clean either if it has not been written to by this processor, or if its changed value has been written through to the store. Otherwise it is dirty. However note that in general, C_{n}(x) = (v, clean) ⇏ S(x) = v. The system may allow the store to contain a different value if some other processor has updated the store but this cache has not yet been notified. As a notational convenience, we shall write C_{i}[x].val = v and C_{i}[x].state = s when C_{i}[x] = (v, s).

Figure 7 gives the semantics for M_{i}[x] and M_{i}[x ← v]. We express all the possibilities as separate transitions to make it easier to read. There are three transitions for reading a variable but they merely represent the different cases possible for the same label rd_{x}^{v}. Note also that there are two transitions for

(S, C, P) ⟶_{i↾}^{x} (S, C_{i} ↑ x, P) C_{i}[x] = (v, clean)

(S, C, P) ⟶_{i→j}^{x} (S, C_{j}[x ← (v, clean)], P)

x ∈ dom(C_{j}) ∧ C_{j}[x]≠(v, clean)∧C_{i}[x]=(v, dirty)

(S, C, P) ⟶_{i→S}^{x} (S[x ← v], C_{i}[x ← (v, clean)], P)

∀j:j ≠i∧x∈dom(C_{j}), C_{j}[x]=(v, clean)∧C_{i}[x]=(v, dirty)

Fig. 8. System Transitions: Update

rd_{x}^{v} when x ∉ dom(C_{i}), corresponding to whether or not x is pulled into the cache. This decision is made non-deterministically, which (along with another transition for eviction to be introduced later) makes the model independent of the cache-replacement policy used by the actual implementation.

The system transitions are used to propagate writes to other caches and the store. In practice this is usually done either with an update-based protocol (where cached copies are updated with the new value) or with an invalidationbased protocol (where cached copies are invalidated, effectively removing them from the cache)[5]. We give two sets of system transitions, one for each type of protocol.

This model allows for W → R reordering, since a read may be serviced while a previous write (to the cache) has not yet been propagated. W → W reorderings are possible because there is no guarantee that writes will be propagated in the order in which they appear. Thus the behaviors described in Fig 5 (a) and (b) in [1] will be exhibited by this model. Further, a processor may see its own writes before any other processor, simply because updates/invalidates haven’t occurred yet. Similarly, other processors may see the write at different times, since the updates/invalidates on other caches need not happen all at once.

In [6] we show that this model with an update-based protocol satisfies the constraints in §3.2. This means that the abstract operational description presented earlier is general enough to at least allow these four relaxations.

6.1 Coherence and Consistency

For both protocols, we reformulate the definitions of coherence and consistency. We will show that these structural definitions are equivalent to the operational definitions given earlier.

Definition 10. A configuration ℂ is said to be coherent for x if ∃v : ∀i : x ∈ dom(C_{i}) ∧ C_{i}[x].state = dirty ⇒ C_{i}[x].val = v.

Definition 11. A configuration (S, C, P) is said to be consistent for x if and only if ∀i : x ∈ dom(C_{i}), C_{i}[x] = (S(x), clean).

6.2 Modeling Update-based Protocols

Figure 8 gives the system transitions used in the update-based model. The transitions are as follows:

1. Eviction ⟶_{i↾}^{x}: Evict x from C_{i}. This is only used for the cache replacement

policy. We do not need it to achieve a consistent configuration in this model.

2. Cache update ⟶_{i→j}^{x}: Update x in C_{j} from C_{i}. This is used to update other

caches when a variable is written to in a cache. It can be applied anytime there is some cache whose entry for the variable differs from the “correct” one.

3. Store update ⟶_{i→S}^{x}: Update x in S from C_{i}. The condition for its application ensures that a store update only happens after all caches have been updated and agree on the value of the variable.

As an example of how these transitions work, suppose a write occurs on a processor, and this is the only processor where that variable is dirty. An update-based system would execute the cache update transition multiple times to update the value in the other caches, and then a store update to put that value in the store. The →-normal configurations are those that have empty caches.

If ℂ is coherent for x by the structural definition, then we can see that any ⟶_{i→S}^{x} will set S(x) to the same value. Conversely, if ∃i, j : C_{i}[x].state =

C_{j}[x].state = dirty ∧ C_{i}[x].val ≠ C_{j}[x].val then depending on whether ⟶_{i→j}^{x} or

⟶_{j→i}^{x} occurs (one of the two must occur), two distinct store updates are possible.

Thus the structural and operational definitions for coherence are equivalent.

Similarly, it is easy to see that if ℂ is consistent by the structural definition, it is consistent by the operational definition. Conversely, for ℂ to be consistent for x, ∀i : x ∈ dom(C_{i}), C_{i}[x].val = S(x) due to (b) and (c) of Definition 4. Further, if ∃i : C_{i}[x] = (v, dirty) then for any w ≠ v ∧ j ≠ i, ℂ′ is not coherent for x where ℂ′.M = ℂ.M_{j}[x ← w], thus violating condition (d) of Definition 4.

This model satisfies all the constraints in §3.2 [6]. We additionally prove that it is possible to achieve a consistent configuration without the use of the eviction transition. This models the intended semantics of an update based protocol.

Lemma 6. For any configuration ℂ reachable from a consistent configuration, there exists a sequence of system transitions ⟶^{∗} not involving evictions such that ℂ ⟶^{∗} ℂ′ and ℂ′ is a consistent configuration.

6.3 Relaxing the Unlocking condition

The following lemma holds in the update based model:

Lemma 7. If ℂ is consistent for x and ℂ →_{I}^{∗} ℂ_{I} where ℂ_{I} is such that ∀i, C_{i}[x].state = clean, then ℂ_{I} is also consistent for x (i.e. ∀i, ℂ_{I}.C_{i}[x].val = S(x))

Using this lemma, we can relax the condition for an ľ operation and still ensure that the implementation and specification semantics coincide for WS configurations. Currently, an unlock can only happen if the configuration is consistent, but we can replace the “configuration is consistent” condition with the following:

∀x ∈ dom(C_{i}), C_{i}[x].state = clean

(S, C, P) ⟶_{i↾}^{x} (S, C_{i} ↑ x, P) C_{i}[x] = (v, clean)

(S, C, P) ⟶_{i→S}^{x} (S[x ← v], C_{i}[x ← (v, clean)], P) C_{i}[x] = (v, dirty)

Fig. 9. System Transitions: Invalidation

i.e. there are no dirty entries in the current cache. This is a purely local condition (i.e. local to the current processor) on the unlock similar to the semantics of the unlock instruction on x86 processors [8].

In a system where Lemma 7 holds, this condition ensures that the configuration is consistent for x after the last unlock ľ in a WS sequence, as used in the proof of Theorem 2. We can modify the abstract semantics to allow local semantics for unlocking ľ by introducing an abstract predicate on M, safe_{i}^{x} with the conditions that only a (wr_{x}, i) destroys safe_{i}^{x}, and ∀i safe_{i}^{x} ⇒ consistent for x. An ľ can then happen only when ∀x safe_{i}^{x}. Then in the cache model safe_{i}^{x} is definable as C_{i}[x].state = clean.

Note that with the global semantics for locks it may be possible to simulate barriers with locks, but with these local semantics that is no longer true.

6.4 Modeling Invalidation-based Protocols

Figure 9 gives the system transitions required to model an invalidation based cache consistency protocol. The transitions are as follows:

1. Eviction ⟶_{i↾}^{x}: This is now used for both cache replacement and cache con-

sistency.

2. Store update ⟶_{i→S}^{x}: This can now happen before other caches have been notified about a write.

As an example of how these work, suppose a write occurs on a processor, and this is the only processor where that variable is dirty. An invalidation-based system would execute ⟶_{j↾}^{x} on all other caches, and ⟶_{i→S}^{x} on this cache (with no

restrictions on the order in which these are carried out).

The proof that this model satisfies the constraints in §3.2 is nearly the same as that for the update model. Lemma 7 does not hold in this model, so the relaxed unlock condition cannot be used. The reason this lemma does not hold is that the last store update can happen before all caches have been invalidated. Thus some cache may hold a clean entry which nevertheless has a wrong value, simply because it has not yet been evicted.

7 Related and Future Work

Our work is complementary to the seminal work of Adve et al [1] wherein they present a classification of memory models (from a systems perspective rather than a programming perspective) that examine permissible reorderings of instructions. The notions of Data Race Freedom and weak orderings are also extensively explored by Adve et al [2].

Owens et al [8] have considered the x86 memory model and shown the correspondence between an axiomatic characterization of the model and an operational one. It would be interesting to relate our work to such concrete instances.

There are several strands of work that we identify for the future. First, the conditions we give are certainly sufficient to ensure sequential consistency, but it is not clear whether they are necessary. We also plan to investigate other synchronization primitives in a similar manner, in particular atomic compareand-swap instructions for synchronization which are preferred over locks in many processors.

An interesting direction is the development of program analysis tools that will help analyze whether a program satisfies the condition that guarantees sequentially consistent behavior. Finally, we are formalizing the results presented here using the proof assistant Coq.

References

1. Sarita V. Adve and Kourosh Gharachorloo. Shared Memory Consistency Models: A Tutorial. Computer, 29(12):66–76, 1996.

2. Sarita V. Adve and Mark D. Hill. Weak Ordering—A new definition. SIGARCH Comput. Archit. News, 18(3a):2–14, 1990.

3. N. N. Arvind, J.-W. Maessen, R. S. Nikhil, and J. E. Stoy. A Lambda Calculus with Letrecs and Barriers. In Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 19–36, London, UK, 1996. Springer-Verlag.

4. Gérard Boudol and Gustavo Petri. Relaxed Memory Models: An Operational Approach. In POPL ’09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pages 392–403, New York, NY, USA, 2009. ACM.

5. Jim Handy. The Cache Memory Book. Academic Press Professional, Inc., San Diego, CA, USA, 1993.

6. Salil Joshi and Sanjiva Prasad. An Operational Model for Multiprocessors with Caches. Technical report, Indian Institute of Technology Delhi, 2010. http://cse.

iitd.ac.in/~sanjiva/OpCache.pdf.

7. Leslie Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computers, 100(28):690–691, 1979.

8. Scott Owens, Susmit Sarkar, and Peter Sewell. A Better x86 Memory Model: x86-TSO. In TPHOLs ’09: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pages 391–407, Berlin, Heidelberg, 2009. Springer-Verlag.

9. S. Sarkar, P. Sewell, F.Z. Nardelli, S. Owens, T. Ridge, T. Braibant, M.O. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. ACM SIGPLAN Notices, 44(1):379–391, 2009.

10. Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115:38–94, 1992.