Memory Access Semantics for a Multiprocessor Instruction Set

Mike Gordon  ??? ??? ???
Computer Laboratory  ??? ??? ???
New Museums Site  ??? ??? ???
Pembroke Street  ??? ??? ???
Cambridge CB2 3QG  ??? ??? ???

Contents

1 Introduction 1 2 Summary of set theory and logic 1 3 A simple generic instruction set 2

3.1 Load instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 3.2 Store instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3.3 Barrier instruction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3.4 Branch instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.5 Local instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

4 General semantics of the instruction set 5 5 General semantics of programs 6 6 Uniprocessor semantics of programs 7 7 Shared memory model 8 8 Relationships between the two semantics 11 9 Acknowledgements 13 References 13

1 Introduction

Multiprocessor architectures, such as Digital’s Alpha [4] and Sun’s SPARC [1], consist of a number of processors that read and write a shared global memory. The documents that define them usually specify the behaviour of the shared memory via constraints on the sets of reads and writes. Formalisms such as process algebra or temporal logic, that are popular in the verification community, are not used. There is thus a ‘gap’ between the models found in architecture manuals and those underlying standard verification technologies. The work presented here is a start at bridging this gap. A semantics for machine instructions is formulated in terms of constraints on sets of memory references. This is then related to standard state machine models. It is hoped that this will enable state-of-the-art techniques for reasoning about object code (e.g. [5]) to be applied to programs running on multiprocessor architectures.

Although the work described here started out as specifically targeted at Digital’s Alpha architecture, the various simplifications that have been made make the results more widely applicable. For example, the generic machine instructions used, although very simple, have as instances instructions found in other processors.

2 Summary of set theory and logic

The application of a function f to an argument x will be written as f x. If f is ‘curried’ then its application to n arguments x_{1}, …, x_{n} is written f x_{1} … x_{n}. An application of the form f (x_{1}, …, x_{n}) is regarded as the application of f to a single tuple argument (x_{1}, …, x_{n}).

Predicates are regarded as functions that return the truth-values T and F. For example, the set membership predicate ∈ is defined by: u ∈ S = T if u is a member of S and u ∈ S = F if u is not a member of S; ∈ is regarded as a function taking two arguments and returning a truth value (following convention, it is written infixed).

Sets will normally be written in a slanted font. For example, num, bool and string denote the sets of truth values, natural numbers and strings, respectively. Finite S means S is finite. The empty set is denoted by { }. If S_{1} and S_{2} are sets, then S_{1} × S_{2} denotes the Cartesian product of S_{1} and S_{2} (i.e. the set of all pairs (x_{1}, x_{2}), where x_{1} ∈ S_{1} and x_{2} ∈ S_{2}) and (S_{1} → S_{2}) denotes the set of all total functions from S_{1} to S_{2}. The union of S_{1} and S_{2} is S_{1} ∪ S_{2}.

The lambda-notation λx. E[x] denotes the function (which is sometimes written as x ↦ E[x]) that mape x to E[x]. For example, λx. 1 is a function that returns 1 on all arguments and λx. x + 1 adds 1 to its argument.

The Hilbert epsilon notation εx. P[x] (where P[x] is a truth-valued term) denotes an arbitrarily chosen value a such that P[a] holds. If P[x] = F for all values of x, then a is chosen arbitrarily.

Functions and predicates can be applied to other functions and predicates and return them as results (i.e. higher order predicate calculus is used).

The symbols used for the logical operators are: ¬ (negation – “not), ∧ (conjunction – “and”), ∨ (disjunction – “or”), ⇒ (implication – “implies”), ∀ (universal quantification – “for all”) and ∃ (existential quantificatioEn – “there exists”). Quantifications may be restricted to a set S using the notations ∀x ∈ S and ∃x ∈ S. The notation (b ⟶ x | y) means “if b then x else y”.

A definition of c has the form c x_{1} … x_{n} =^{def} E, where E is some expression involving x_{1}, …, x_{n}. The notation ⊢ F means that F follows from the definitions that precede it. No proofs are given is this paper, but all theorems have been proved with the HOL system [3].

3 A simple generic instruction set

For simplicity, it is assumed that each location in shared memory is represented by a string (think of this as its symbolic name) and that the value of each location is a natural number. Thus a shared memory state is a function of in the set (string → num). These particular representations are somewhat arbitrary and the results in this paper do not really depend on them. In actual implementations locations might, for example, be restricted to be strings of 0s and 1s of length 64, and values might be restricted to be numbers mod 2^{64}.

The local state of each processor contains a program counter pc, which is represented by a natural number, and a register file rg, which is assumed to be a member of a given set registers. For example, if there were 64 quadword registers (as in Alpha) then members of registers could be 64-tuples of 64-bit words; however for most of this paper registers can be left arbitrary.

Example 1: A model of registers that will be used in examples is registers = (string → num) (i.e. register names are represented by strings and their values by numbers).

Note that the state of the shared memory is also represented by a function that maps locations to values. However, in this example the string arguments of the functions represent register names, but when a function represents a state of the shared memory the string argument represents a location. End of Example 1.

First the instruction set is given, then each instruction is explained in detail. Note that the instructions are parameterized on various functions and relations.

Instruction  Meaning
Load x lrel  Read x; use resulting value and lrel to determine new values of registers
Store x sfn  Apply sfn to registers; store result in x
Barrier  Constrain order of memory accesses
Branch pred sfn If pred is true of registers then branch to result of applying sfn
Local rel  Modify registers to satisfy rel

3.1 Load instructions

The Load instruction takes two arguments: (i) a location x from which to read a value in shared memory, and (ii) a relation lrel ∈ (value → (registers → (registers → bool))) that specifies what to do with the resulting value. More specifically, if the value of x in shared memory is a and the state of the registers is rg, then executing Load x lrel results in a new register state rg′ such that lrel a rg rg′ = T.

Example 2: Suppose that registers are modelled as in Example 1 by functions from string to num. The instruction LD x r that reads location x in shared memory and stores the result in register r is defined by:

LD x r =^{def} Load x (λa regs regs′. regs′ = Update r a regs)

where Update is a function that updates a given register in a register bank; it is defined by:

Update r a regs =^{def} λr′. (r = r′ ⟶ a | regs r′)

End of Example 2.

Note that Load x lrel may be nondeterministic, but this generality is not used here. However, it might be useful to consider cases in which there is no successor state for some read values, i.e. for some values of a and rg to use an lrel such that lrel a rg rg′ = F for all values of rg′ (i.e. the processor halts).

Example 3: Assume registers as in Example 1. The instruction LDHALT x pred that reads location x in shared memory and then halts if the resulting value satisfies pred is defined by:

LDHALT x pred =^{def} Load x (λa regs regs′. ¬(pred a))

End of Example 3.

3.2 Store instructions

The Store instruction takes two arguments: (i) a location x in shared memory to write to, and (ii) a function sfn ∈ (registers → num) that specifies what value to write. If the state of the registers is rg, then executing Store x sfun writes sfun rg to location x; the registers are unchanged.

Example 4: The instruction ST x a that writes location x in shared memory with value a is defined by:

ST x a =^{def} Store x (λregs. a)

End of Example 4.

Example 5: Suppose that registers are modelled as in Example 1. The instruction STR x r that writes location x in shared memory with the value of register r is defined by:

STR x a =^{def} Store x (λregs. regs r)

End of Example 5.

3.3 Barrier instruction

The Barrier instruction forces all read/write accesses issued before it to take place before any read/write accesses issued after it.

Example 6: Let x and y be different locations. Consider the sequence:

                                     LD x R Barrier ST y a

The Barrier instruction forces the read from shared memory generated by LDxR to be before the write generated by ST y a. Without the Barrier these two memory accesses could be performed in arbitrary order. End of Example 6.

3.4 Branch instructions

The Branch instruction takes two arguments: (i) a predicate pred ∈ (registers → bool) to determine whether to jump, and (ii) a function sfn ∈ (registers → num) to determine where to jump to if pred is true. If the register state is rg then executing Branch pred sfun has no effect if rg = F; however if pred rg = T then the program counter is set to sfun rg.

Example 7: The instruction JMP n that causes an unconditional jump to the nth instruction is defined by:

JMP n =^{def} Branch (λregs. T) (λregs. n)

End of Example 7.

3.5 Local instructions

The Local instruction takes one argument: a relation rel ∈ (registers → (registers → bool)) that specifies a change to the contents of the registers. If the state of the registers is rg, then executing Local rel results in a new register state rg′ such that rel rg rg′ = T.

Example 8: Suppose that registers are modelled as in Example 1. The instruction ADD r_{1} r_{2} r that adds the contents of registers r_{1} and r_{2} and puts the result in register r is defined by:

ADD r_{1} r_{2} r =^{def} Local (λregs regs′. regs′ = Update r (regs r_{1} + regs r_{2}) regs)

End of Example 8.

Example 9: The instruction HALT that halts the processor is defined by:

HALT =^{def} Local (λregs regs′. F)

End of Example 9.

Example 10: The following two-processor example is based on a suggestion by Jim Saxe:

Program for Processor 1 (P1) Program for Processor 2 (P2)

           ST x v  ST flag 0
           Barrier                        LD flag R1
           ST flag 1  Barrier
                                          LD x R2

The program running on P1 stores v in location x of the shared memory; it then executes an Barrier and then it stores 1 into location flag. The memory barrier instruction Barrier ensures that the write generated by ST x v is performed before the write generated by ST flag 1.

The program running on P2 first stores 0 into location flag, then loads the value of flag into its local register R1. (Note that the value read is not necessarily the 0 just written, because the write generated by ST flag 1 on P1 might be executed after the write generated by ST flag 0 on P2.) Next a memory barrier is executed on P2 and finally the value in location x of shared memory is loaded into P2’s register R2. Because of the preceding Barrier, the read generated by this load is constrained by the architecture to happen after the references generated by the two instructions preceding the Barrier.

If P1 and P2 start up running the two programs in parallel, then the results are not completely predictable. However, the following must hold (assuming no other processors are accessing the shared memory):

If the value in P2’s register R1 in the final state is 1, then the value in P2’s register R2 in the final state must be v.

End of Example 10.

4 General semantics of the instruction set

As each processor executes a program it issues a sequence of memory references consisting of:

(i) Reads: R p n x a ;

(ii) Writes: W p n x a;

(iii) Memory barriers: MB p n

where R, W and MB are functions that construct references. They take as arguments a natural number p representing a processor, and a natural number n specifying the order in which the reference is issued. Reads and writes also take a location x in shared memory (a string) and a value read or written a (a natural number).

The execution of an individual instruction is specified by a relation InstructionStep, such that InstructionStep p i refs s s′ = T iff executing instruction i on processor p with local state s results in a new local state s′ and generates the set refs of memory references. The set refs will be empty if i is a barrier, branch or local instruction; it will be of the form {R p n x a} if i is a load and of the form {W p n x a} if i is a store.

In order to specify the numbers defining the order in which references are generated (i.e. the issue sequence), the local state of each processor will be augmented with a ‘reference count’ component. Thus the local state of a processor will be a triple (pc, ic, rg) where pc is the program counter (a natural number), ic is the reference count (a natural number) and rg is the register state (a member of registers).

InstructionStep is defined by cases on the five kinds of instructions so as to satisfy:

InstructionStep p (Load x lrel) refs (pc, ic, rg) (pc′, ic′, rg′) = ∃a. refs = {R p ic x a} ∧ (pc′ = pc + 1) ∧ (ic′ = ic + 1) ∧ lrel a rg rg′

InstructionStep p (Store x sfn) refs (pc, ic, rg) (pc′, ic′, rg′) = refs = {W p ic x (sfn rg)} ∧ (pc′ = pc + 1) ∧ (ic′ = ic + 1) ∧ (rg′ = rg)

InstructionStep p Barrier refs (pc, ic, rg) (pc′, ic′, rg′) = refs = {MB p ic} ∧ (pc′ = pc + 1) ∧ (ic′ = ic + 1) ∧ (rg′ = rg)

InstructionStep p (Branch pred sfn) refs (pc, ic, rg) (pc′, ic′, rg′) = refs = { } ∧ (pc′ = (pred rg ⟶ sfn rg | pc + 1)) ∧ (ic′ = ic) ∧ (rg′ = rg)

InstructionStep p (Local rel) refs (pc, ic, rg) (pc′, ic′, rg′) = refs = { } ∧ (pc′ = pc + 1) ∧ (ic′ = ic) ∧ rel rg rg′

5 General semantics of programs

A program will be represented by a list of instructions. The list of length n+1 containing the elements x_{0}, …, x_{n} will be written as [x_{0}; x_{1}; …; x_{n}]. El i l is the (i+1)th element of l, thus El i [x_{0}; x_{1}; …; x_{n}] = x_{i}. The length of a list l is denoted by Length l.

If prog is a list of instructions and pc a number, then FetchInstruction prog pc denotes the instruction pointed to by pc, or HALT (see Example 9) if pc doesn’t point to an instruction in prog.

FetchInstruction prog pc =^{def} (pc > (Length prog) ⟶ HALT | El pc prog)

Define ProgSteps so that ProgSteps p prog refs (pc, ic, rg) (pc′, ic′, rg′) is true iff whenever program prog is executed on processor p with initial local state (pc, ic, rg), then there is a sequence of steps to state (pc′, ic′, rg′), each of which satisfies InstructionStep, and that generates the set refs of references.

Intuitively, ProgSteps is a kind of transitive closure of InstructionStep that ‘accumulates’ memory references. Formally ProgSteps is the least relation satisfying the following two conditions:

InstructionStep p (FetchInstruction prog pc) refs (pc, ic, rg) (pc′, ic′, rg′)

⇒

ProgSteps p prog refs (pc, ic, rg) (pc′, ic′, rg′)

ProgSteps p prog refs_{1} (pc, ic, rg) (pc′, ic′, rg′) ∧

InstructionStep p (FetchInstruction prog pc′) refs_{2} (pc′, ic′, rg′) (pc′′, ic′′, rg′′) ⇒ ProgSteps p prog (refs_{1} ∪ refs_{2}) (pc, ic, rg) (pc′′, ic′′, rg′′)

Example 11: Consider the programs discussed in Example 10:

Prog_{0}(v) =^{def} [ST x v; Barrier; ST flag 1]

                Prog_{1}  =^{def} [ST flag 0; LD flag R1; Barrier; LD x R2]

It can be shown that:

⊢ ProgSteps 0 (Prog_{0} v) refs_{0} (0, 0, rg_{0}) (3, 3, rg′_{0}) =
(refs_{0} = {W 0 0 x v, MB 0 1, W 0 2 flag 1}) ∧
(rg′_{0} = rg_{0})
⊢ ProgSteps 1 Prog_{1} refs_{1} (0, 0, rg_{1}) (4, 4, rg′_{1}) =
∃a1 a2. (refs_{1} = {W 1 0 flag 0, R 1 1 flag a1, MB 1 2, R 1 3 x a2}) ∧

(rg′_{1} = Update R2 a2 (Update R1 a1 rg_{1}))

End of Example 11.

6 Uniprocessor semantics of programs

In the general semantics of the previous section, the effect of loads and stores was to issue memory accesses. The fact that writes may effect later reads was only specified indirectly via the definition of the before-ordering on the set of all memory references (see Section 7). There is no explicit updating of the shared memory in the semantics.

Although this semantics can be used to reason about programs, it is rather cumbersome (see Example 12 on page 10). An important special case is when there is no communication between processors. When this holds, each processor can be treated as though it were a uniprocessor and much simpler models can be used. In particular, the highly developed technology for reasoning about object code developed by Boyer and Yu [5] is applicable.

In this section a uniprocessor semantics for the instruction set of Section 3 is presented. Its relationship to the general semantics is then considered.

The uniprocessor semantics is a straightforward state-machine. Each step corresponds to the exection of a single instruction. The state consists of the program counter, registers and the shared memory (note that in the uniprocessor case the memory is not really shared as there is only one processor). The effect of a store is to explicity update the shared memory and the value read by a load is obtained by ‘looking up’ the value of the location in shared memory.

The execution of individual instructions on a uniprocecssor is specified by UniInstructionStep, which is the relation such that UniInstructionStep i (pc, rg, mem) (pc′, rg′, mem′) = T iff executing instruction i when the program counter is pc, the register state is rg and the shared memory is mem results in a new state with program counter pc′, register state rg′ and shared memory state mem′.

The definition of UniInstructionStep is by cases on the five kinds of instructions. Note that since the shared memory has the same representation as the register model of Example 1, the function Update defined in Example 2 can be used.

UniInstructionStep (Load x lrel) (pc, rg, mem) (pc′, rg′, mem′) = (pc = pc + 1) ∧ lrel (mem x) rg rg′ ∧ (mem′ = mem)

UniInstructionStep (Store x sfn) (pc, rg, mem) (pc′, rg′, mem′) = (pc′ = pc + 1) ∧ (rg′ = rg) ∧ (mem′ = Update x (sfn rg) mem)

UniInstructionStep Barrier (pc, rg, mem) (pc′, rg′, mem′) = (pc′ = pc + 1) ∧ (rg′ = rg) ∧ (mem′ = mem)

UniInstructionStep (Branch pred sfn) (pc, rg, mem) (pc′, rg′, mem′) = (pc′ = (pred rg ⟶ sfn rg | pc + 1)) ∧ (rg′ = rg) ∧ (mem′ = mem)

UniInstructionStep (Local rel) (pc, rg, mem) (pc′, rg′, mem′) = (pc′ = pc + 1) ∧ rel rg rg′ ∧ (mem′ = mem)

Define UniProgSteps so that UniProgSteps prog (pc, rg, mem) (pc′, rg′, mem′) is true iff whenever program prog is executed with initial state (pc, rg, mem), then there is a sequence of steps to state (pc′, rg′, mem′), each of which satisfies UniInstructionStep.

UniInstructionStep (FetchInstruction prog pc) (pc, rg, mem) (pc′, rg′, mem′)

⇒

UniProgSteps prog (pc, rg, mem) (pc′, rg′, mem′)

UniProgSteps prog (pc, rg, mem) (pc′, rg′, mem′) ∧

UniInstructionStep (FetchInstruction prog pc′) (pc′, rg′, mem′) (pc′′, rg′′, mem′′) ⇒ UniProgSteps prog (pc, rg, mem) (pc′′, rg′′, mem′′)

7 Shared memory model

The memory model used here is motivated and described in detail in a companion paper [2]. To make this paper self-contained it is summarized below.

A number of auxiliary functions for manipulating references are used.

The components of references can be extracted with the functions Proc, Seq, Var and Val, which are defined so as to satisfy the following equations:

Proc(R p n x a) = p,  Proc(W p n x a) = p,  Proc(MB p n) = p,
Seq(R p n x a) = n, Seq(W p n x a) = n, Seq(MB p n) = n,
Var(R p n x a) = x, Var(W p n x a) = x,
Val(R p n x a) = a, Val(W p n x a) = a.

The predicates IsR, IsW and IsMB are defined so as to satisfy:

IsR(R p n x a) = T,  IsR(W p n x a) = F,  IsR(MB p n) = F,
IsW(R p n x a) = F,  IsW(W p n x a) = T, IsW(MB p n) = F,
IsMB(R p n x a) = F,  IsMB(W p n x a) = F,  IsMB(MB p n) = T.

Reference u precedes v in the processor issue order if they are issued by the same processor, the sequence number of u is less than the sequence number of v and either u or v is a memory barrier or they are both read/write accesses to the same variable:

IssueOrder u v =^{def} (Proc u = Proc v) ∧ (Seq u < Seq v) ∧ (IsMB u ∨ IsMB v ∨ (Var u = Var v))

The restriction of IssueOrder to a set refs will be needed. Define:

Restrict refs ord u v =^{def} u ∈ refs ∧ v ∈ refs ∧ ord u v

then the restricted issue order is Restrict IssueOrder refs.

The processor issue order only orders references from the same processor. A second ordering, the location access order, orders references to a given location in shared memory from any processor.

Location access order is only partially specified. It is required to satisfy three properties:

1. Any two accesses to the same location, one of which is a write, must be ordered.

2. Storage:

(a) If a read u to a location x follows a write v to x, and there is no other intervening write to x with a different value, then the value read in v must be the value written in u.

(b) If a read u to a location x follows a write v to x and the value read in v is different from the value written in u, then there must exist an intervening write w to x with the value read by v.

3. If u and v are two accesses to the same location, one of which is a write, and u precedes v in the issue order, then u precedes v in the location access order.

To formalize these, first define the auxiliary predicate AtLeastOneWrite by:

AtLeastOneWrite u v =^{def} ¬(u = v) ∧ (Var u = Var v) ∧ ((IsR u ∧ IsW v) ∨ (IsW u ∧ IsR v) ∨ (IsW u ∧ IsW v))

The first condition, 1, is then formalized by Linearity refs ord, where:

Linearity refs ord =^{def} ∀u v ∈ refs. AtLeastOneWrite u v ⇒ (ord u v ∨ ord v u)

Part (a) of the second condition, 2, is formalized by ReadGetsLastWrite refs ord, where:

ReadGetsLastWrite refs ord =^{def}

∀u v ∈ refs.

IsW u ∧ IsR v ∧ (Var u = Var v) ∧ ord u v ∧

¬(∃w ∈ refs. IsW w ∧ (Var w = Var u) ∧ ¬(Val u = Val w) ∧ ord u w ∧ ord w v)

⇒ (Val u = Val v)

Part (b) is formalized by ReadRequiresWrite refs ord, where:

ReadRequiresWrite refs ord =^{def}

∀u v ∈ refs.

IsW u ∧ IsR v ∧ (Var u = Var v) ∧ ord u v ∧ ¬(Val u = Val v)

⇒ ∃w ∈ refs. IsW w ∧ (Var w = Var u) ∧ (Val v = Val w) ∧ ord u w ∧ ord w v

The second condition, 2, is the combination of (a) and (b) and is formalized by Storage refs ord, where:

Storage refs ord =^{def} ReadGetsLastWrite refs ord ∧ ReadRequiresWrite refs ord

The third condition, 3, is formalized by IssueAccess refs ord, where:

IssueAccess refs ord =^{def} ∀u v ∈ refs. AtLeastOneWrite u v ∧ IssueOrder u v ⇒ ord u v

The conditions for an order ord to be an access order on a set of references refs are thus:

IsAccessOrder refs ord =^{def} Linearity refs ord ∧ Storage refs ord ∧ IssueAccess refs ord

An ordering ord on a set refs of references is a possible before-ordering iff there is an access order, access order say, such that:

(i) ord is the transitive closure of the union of the issue order restricted to refs and access order;

(ii) if u and v are references, then at most one of ord u v and ord v u is true.

If R_{1} and R_{2} are binary relations, then the transitive closure of the union of R_{1} and R_{2} is the least transitive relation including R_{1} and R_{2}.

This is the relation Closure R_{1} R_{2} characterized by the four properties:

∀u v. R_{1} u v ⇒ Closure R_{1} R_{2} u v
∀u v. R_{2} u v ⇒ Closure R_{1} R_{2} u v
∀u v. (∃w. Closure R_{1} R_{2} u w ∧ Closure R_{1} R_{2} w v) ⇒ Closure R_{1} R_{2} u v
∀P. (∀u v. R_{1} u v ⇒ P u v) ∧

(∀u v. R_{2} u v ⇒ P u v) ∧

(∀u v. (∃w. P u w ∧ P w v) ⇒ P u v)

⇒ (∀u v. Closure R_{1} R_{2} u v ⇒ P u v)

A relation is formally defined to be a ‘before relation’ on refs by:

IsBefore refs ord =^{def}

∃access order. IsAccessOrder refs access order ∧ (ord = Closure (Restrict IssueOrder refs) access order) ∧ ¬(∃u v ∈ refs. ord u v ∧ ord v u)

Theorem 1: If Trans ord means that ord is transitive, then:

⊢ ∀refs ord. Finite refs ⇒ (IsBefore refs ord =

IsAccessOrder refs ord ∧

Trans (Restrict ord refs) ∧

¬(∃u v ∈ refs. ord u v ∧ ord v u))

Because it does not use Closure, this characterization of IsBefore is sometimes easier to work with than the definition given above.

Example 12: Recall Example 11 concerning the programs:

Prog_{0}(v) =^{def} [ST x v; Barrier; ST flag 1]

                Prog_{1}  =^{def} [ST flag 0; LD flag R1; Barrier; LD x R2]

It follows that:

⊢ ∀v rg_{0} rg_{1} rg′_{0} rg′_{1} refs_{0} refs_{‘} ord.
ProgSteps 0 (Prog_{0} v) refs_{0} (0, 0, rg_{0}) (3, 3, rg′_{0}) ∧
ProgSteps 1 Prog_{1} refs_{1} (0, 0, rg_{1}) (4, 4, rg′_{1})
⇒
refs_{0} ∪ refs_{1} = {W 0 0 x v,  W 1 0 flag 0, MB 0 1,  R 1 1 flag a1, W 0 2 flag 1, MB 1 2, R 1 3 x a2}

This can be used to prove that if Prog_{0} v and Prog_{1} are executed with a shared memory, and if there is a before-ordering on the resultant set of references, i.e. a before-ordering on the set:

{W 0 0 x v,  W 1 0 flag 0,
MB 0 1,  R 1 1 flag a1,
W 0 2 flag 1, MB 1 2,
R 1 3 x a2}

then if the final value of P2’s register R1 is 1 then the final value of its register R2 must be v.

⊢ ∀v rg_{0} rg_{1} rg′_{0} rg′_{1} refs_{0} refs_{‘} ord. ProgSteps 0 (Prog_{0} v) refs_{0} (0, 0, rg_{0}) (3, 3, rg′_{0}) ∧ ProgSteps 1 Prog_{1} refs_{1} (0, 0, rg_{1}) (4, 4, rg′_{1}) ∧ IsBefore (refs_{0} ∪ refs_{1}) ord ⇒ (rg′_{1} R1 = 1) ⇒ (rg′_{1} R2 = v)

This is a safety property. The corresponding liveness property is that there always does exist a before-ordering in which the final value of P2’s register R1 is 1. Formally:

⊢ ∀v rg_{0} rg_{1}.
∃rg′_{0} rg′_{1} refs_{0} refs_{1} ord.
ProgSteps 0 (Prog_{0} v) refs_{0} (0, 0, rg_{0}) (3, 3, rg′_{0}) ∧
ProgSteps 1 Prog_{1} refs_{1} (0, 0, rg_{1}) (4, 4, rg′_{1}) ∧
IsBefore (refs_{0} ∪ refs_{1}) ord ∧
(rg′_{1} R1 = 1)

End of Example 12.

A set refs of references is initialized with respect to a memory state init and an ordering ord iff every read in refs can be ‘explained’ by init or by a preceding write in refs.

More precisely: for every read u in refs, if u reads from location x, then the value a that is read is either the value of x in init or the value written by some write to x in refs that precedes the read in the ordering ord.

Init init refs ord =^{def}

∀u ∈ refs. IsR u ⇒ (Val u = init(Var u)) ∨ ∃v ∈ refs. IsW v ∧ (Var v = Var u) ∧ (Val v = Val u) ∧ ord v u

8 Relationships between the two semantics

In the general semantics of section 4 the state of the shared memory is not explicit, but is implicit in the history of reads and writes that have occurred. If refs is a set of references, ord a beforeordering on refs and init an initial state, then the final state determined by refs, ord and init is denoted by Final refs ord init.

The function Final is defined using four auxiliary predicates: IsLast, IsLastWrite, IsFinalLocVal and IsFinal.

IsLast refs p ord u is true iff u is the last (with respect to ord) member of the set refs satisfying the predicate p.

IsLast refs p ord u =^{def} u ∈ refs ∧ p u ∧ ∀v ∈ refs. p v ⇒ ((v = u) ∨ ord v u)

IsLastWrite refs ord x u is true iff u is the last (with respect to ord) write access to x in refs.

IsLastWrite refs ord x u =^{def} IsLast refs (λu. IsW u ∧ (Var u = x)) ord u

IsFinalLocVal refs ord s x a is true iff a is the last value (with respect to the ordering ord) written to x by a write in refs. If there is no write to x in refs, then a is the initial value of x, i.e. init x

IsFinalLocVal refs ord init x a =^{def} ((∃w ∈ refs. IsW w ∧ (Var w = x)) ⟶ ∃w ∈ refs. IsLastWrite refs ord x w ∧ (a = Val w) | (a = init x))

IsFinal refs ord s s′ is true iff s′ is the memory state resulting from performing the memory accesses in refs on the state s. More precisely, the value of every location in s′ is the last value written to the location by a reference in refs.

IsFinal refs ord s s′ =^{def} ∀x. IsFinalLocVal refs ord s x (s′ x)

Theorem 2: If ord is a before-ordering on refs then if a final state exists, it is unique:

⊢ ∀refs ord. IsBefore refs ord ⇒ ∀init s_{1} s_{2}. IsFinal refs ord init s_{1} ∧ IsFinal refs ord init s_{1} ⇒ (s_{1} = s_{2})

If, in addition, refs is finite and is initialized with respect to ord and init, then a final state always exists.

Theorem 3:

⊢ ∀init refs ord. Init init refs ord ∧ IsBefore refs ord ∧ Finite refs ⇒ ∃s. IsFinal refs ord init s

The function Final can now be defined by:

Final refs ord init =^{def} εs. IsFinal refs ord init s

Theorem 4: If there is only one processor, then the general semantics is equivalent to the uniprocessor semantics in the following sense:

⊢ ∀p prog pc ic rg pc′ rg′ mem mem′.

(∃refs. (∃ic′. ProgSteps p prog refs (pc, ic, rg) (pc′, ic′, rg′)) ∧

(∃ord. Init mem refs ord ∧ IsBefore refs ord ∧ (mem′ = Final refs ord mem))

= UniProgSteps prog (pc, rg, mem) (pc′, rg′, mem′)

This result is, perhaps, of limited utility as it assumes that there is only one processor. Its main significance is that it reassures us that the apparently rather ad hoc collection of properties constituting the definition of IsBefore are sound and complete.

A second result, that promises to be more useful, establishes that a set of programs running on a true multiprocessor can be ‘factored’ into a conjunction of uniprocessors if the programs access disjoint sets of references. For simplicity, this will only be stated for the case of two processors.

Theorem 5: Let DisjointLocs prog_{0} prog_{1} be true if and only if prog_{0} and prog_{1} access disjoint sets of locations. Then:

⊢ ∀mem p_{0} prog_{0} pc_{0} ic_{0} rg_{0} pc′_{0} rg′_{0} mem′_{0} p_{1} prog_{1} pc_{1} ic_{1} rg_{1} pc′_{1} rg′_{1} mem′_{1}.
DisjointLocs proc_{0} proc_{1} ∧ ¬(p_{0} = p_{1})
⇒
((∃refs_{0} refs_{1}. (∃ic′_{0}. ProgSteps p_{0} prog_{0} refs_{0} (pc_{0}, ic_{0}, rg_{0}) (pc′_{0}, ic′_{0}, rg′_{0})) ∧
(∃ic′_{1}. ProgSteps p_{1} prog_{1} refs_{1} (pc_{1}, ic_{1}, rg_{1}) (pc′_{1}, ic′_{1}, rg′_{1})) ∧
(∃ord. Init mem (refs_{0} ∪ refs_{1}) ord ∧

IsBefore (refs_{0} ∪ refs_{1}) ord ∧

(mem′_{0} = Final refs_{0} (Restrict ord refs_{0}) mem) ∧ (mem′_{1} = Final refs_{1} (Restrict ord refs_{1}) mem)))

=

UniProgSteps prog_{0} (pc_{0}, rg_{0}, mem_{0}) (pc′_{0}, rg′_{0}, mem′_{0}) ∧ UniProgSteps prog_{1} (pc_{1}, rg_{1}, mem_{1}) (pc′_{1}, rg′_{1}, mem′_{1}))

9 Acknowledgements

The work reported here started during a four week visit I made to DEC’s Systems Research Center in March/April, 1993. The main ideas were worked out then through a combination of conversations with Martin Abadi, Jim Horning, Jim Saxe and Yuan Yu.

I am particularly grateful to Yuan Yu for many hours of help and discussions, to Martin Abadi for hosting my visit to SRC and to Digital for supporting it.

References

[1] The SPARC Architecture Manual. Prentice Hall, 1992.

[2] M. J. C. Gordon and ??? A formalization of a simplified subset of the Alpha shared memory model. 1993.

[3] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.

[4] Richard L. Sites, editor. Alpha Architecture Reference Manual. Digital Press, 1992.

[5] Yuan Yu. Automated Proofs of Object Code for a Widely Used Microprocessor. PhD thesis, The University of Texas at Austin, yuanyu@com.dec.src, 1992.