Introduction

There are two specifications in this document, both of memory arrays. The memory arrays both have an ‘interference detection’ feature, for support of atomic read-modify-write operations. This feature takes the form of special forms of the read and write command. The read command outputs for each cell that is read, not only the value contained in the cell, but also the versionstamp of the cell. The version-stamp of a cell is a quantity that changes to a new value (for that cell) every time the cell is written. It may change at other times as well. The write command accepts version-stamps output by the read command for location read earlier as an extra input, with the semantics that the write changes the cell contents only if the version-stamps for the cells read earlier equal the current ones. The information flow of these two commands is summarised in the following table.

Command Operands

Read

Input  addresses to read
Output ⟨ value , version-stamp ⟩ per read address

Write Input value per written address,

version-stamp per previously read address

Output “Ok” or “Interference”

By an atomic read-modify-write operation, I mean an operation which appears to execute as follows: it reads some cells, checks preconditions as if instantaneously, and computes an assignment of new values to some possibly different cells; the assignment takes effect, in its entirity, as if in the very next instant after the precondition was checked to hold.

read ‘modify’ write
precondition  →  assignment

To obtain the effect of such a read-modify-write operation, one programs it in a loop. The body of the loop has a classical 2-phase structure:

prepare: Read the necessary cells, keeping their version-stamps. Check the precondition, and decide what to write.

commit: Issue the desired write, with the version stamps for the necessary addresses. Because of the interference detection feature, nothing will happen unless the version-stamps obtained from phase 1 and presented with the write are still current.

If the write fails because of a version stamp being non-current, then it does not mean that the precondition for the write to proceed has been falsified: that is not even apparent at the level of reads and writes. However, a precondition once checked can be falsified only by changing the value in a cell; and that can change changes only when the version stamp changes. So any interference with the precondition is detected, and the loop retried.

Before looping back, there should probably be a delay, to avoid prolonged mutual interference. A strategy with much to recommend it is randomised exponential backoff. This involves a variable local to the loop, initialised to a suitable initial 1. If this is the first time round the loop,

scale up the delay period by some factor.

2. Delay for a random time within the delay period, then restart the operation, from the beginning.

The first specification is highly idealised, the second slightly less so. The first memory never fails. The second one allows certain kinds of failure. These failures expose the fact that writes are buffered, and may in fact not reach the memory. Writes are buffered in components called clerks, which can fail (i.e. stop). In the final moments before a clerk stops, it may present a ‘false’ picture in responding to operations. The challenge for the second specification is to say what things look like when you are using a clerk that has already, so far as the outside world is concerned, stopped.

The reason for writing the first specification is to sort out some groundwork for the second. (By ‘groundwork’ I refer to several issues which seem easier, like procedure calling.) The reason for writing the second is that a fair amount of real work (even some of my own) has gone into building a part of a file system in which asynchronous conditional writing forms a central part of the design; and there are signs that intuition has not been an unerring guide in building the clerk component. The clerk has extra operations called Barrier, and Sync. Most obviously, the barrier operation needs to be made much clearer. More seriously, I was too easily satisfied that I understood the conditional writing operation, and something needs sorting out urgently.

The formulas are written using a few Z operators. Here are their definitions:

f ⊕ g  =^{Δ} [x ∈ Domain f ∪ Domain g ↦ if x ∈ Domain g then g[x] else f [x]]

A \underrightarrow{}B =^{Δ} union \{[X → B] : X ⊆ A\}
A ⊲ f =^{Δ} [x ∈ (Domain f ) ∩ A ↦ f [x]]
A − ⊲ f =^{Δ} [x ∈ (Domain f ) \A ↦ f [x]]

Procedures, memory access

The module ProcedureInterface from [?] applies to describing procedural interfaces in which there may be several concurrent activations of the same procedure. Each call or return is a change in an interface variable, with both the identity of the caller and the input or output encoded in the new interface state.

(I suspect that there is a mistake in the definition of PendingProc. The definition does not constrain how pnd may change when there is a change to caller or rtrner which is not a call or return (for example, a change in a component .req or .ans). For example, a state variable which changes to the empty set when the value but not the bit of an interface changes would satify PendingProcs. So LegalCaller permits two Calls without an intervening Return, involving the same caller. This is surely wrong.

It does not seem to be trivial to repair the module. I believe it might have been better first to represent the calls and returns of a single thread, so that Call and Return are disjoint, and uniquely determine the value each action communicates. Then, still with a single thread, to require that it there are never two calls without an intervening return by using a history variable to count the surplus of calls over returns, and which must be zero on any (legal) call by the thread. Finally, in a multithreaded environment, to define LegalCaller so that the calls made by an individual thread are legal, and so that calls by two different threads are disjoint. These extra requirements of disjointness are ‘built-in’ to the Dagstuhl definitions. I think it would be better if they were out in the open. I am not sure what good they are. (Or even what benefit there is that a call and a return for the same thread cannot coincide.)

In terms of this we define a module MemParams. It is very similar to the module in the Dagstuhl TLA^{+} solution. A slight difference is that I do not distinguish between illegal procedure calls, and legal procedure calls with illegal parameters. The module is in figure ??.

The module MemParams conveys much the same kind of ‘syntactic’ information as is conveyed by the type-declarations in a C header file. It is convenient to deal only with the extended forms of the read and write operations: the plain forms are special cases.

The module exports all the names it defines, as well as names from the ProcedureInterface module, prefixed with Pr., and with parameters instantiated with intMem as the procedural ‘medium’, and procedure calls of the form described by LegalCall.

The module will be reused later on, in the writing the more complicated specification, which has more operators. It seems most convenient to include ‘latent support’ for this reuse, by throwing in some of the later commands. These are Synch, and Barrier, which both take a set of addresses as input operand. (I probably won’t get round to Barrier in this draft.) Both these are effectively NOOPs in the simpler specification. Another command which might make the module more reusable is a Reset command to return the memory to an initial state.

Inner memory

Importing MemParams, module InnerMemory in figure ?? adds a variable, which will be hidden, to hold the contents of the memory.

The module InnerMemory introduces a variable mem, for the memory array, and constants MemLoc, MemStamp, and MemVal, for the array index set, the set of version stamps, and the set of data values a cell might contain. In terms of these it defines the following constant operators, state functions, predicates and actions:

Cell is a constant. It is the set of values which represent states of an individual cell. Each such value is a record, with three coordinates, called κ (contents), ι (identifier), and π (past).

κ is the content of the cell, changed (perhaps) by a write operation. ι identifies the state of the cell. It is changed by a write. Not only is ι always changed by a write, it never changes twice to the same stamp in any trace of the states of this cell.

module MemParams

π is the set of version stamps so far attained by this cell. By including such a component in the state of a cell, we express the property that all changes in ι are to values that vale never before been attained. export

MemParams, Pr

parameters intMem : variable MemLoc, MemVal, MemStamp : constant

assumption ParamAssump =^{Δ} ∧ Infinite(MemStamp) ∧ MemLoc ≠ {} ∧ MemVal ≠ {}

ReadCall =^{Δ} [\begin{matrix}cmd & : & \{“Cread”\} \\ addr & : & Subset MemLoc] \end{matrix}

WriteCall =^{Δ} [\begin{matrix}cmd & : & \{“Cwrite”\} \\ data & : & MemLoc \underrightarrow{}MemVal \\ stamps & : & MemLoc \underrightarrow{}MemStamp] \end{matrix}

LegalCall =^{Δ} ReadCall ∪ WriteCall Appropriate(input) =^{Δ}

case

input ∈ ReadCall → [\begin{matrix}stamps & : & input.addr → MemStamp \\ data & : & input.addr → MemVal] \end{matrix}
input ∈ WriteCall → {“Ok”, “Interference”}

Op =^{Δ} {[input ↦ i, output ↦ o] : i ∈ LegalCall, o ∈ Appropriate(i)} include ProcedureInterface as Pr with c ← intMem, Arg ← LegalCall

Figure 1: Module characterising memory parameters.

module InnerMemory

import MemParams parameters

mem : variable

Cell =^{Δ} [κ ↦ MemVal, ι ↦ MemStamp, π ↦ Subset MemStamp] Mem =^{Δ} MemLoc → Cell Ird(X ) =^{Δ} [α ∈ X ↦ mem[α].ι] Drd(X ) =^{Δ} [α ∈ X ↦ mem[α].κ] Valid(c) =^{Δ} c = Ird(Domain c)

Write(d) =^{Δ}

∧ d ∈ MemLoc \underrightarrow{}MemVal

∧ ∃ c ∈ [Domain d → Cell] : ∧ ∀ α ∈ Domain d : ∧ c[α].π = mem[α].π ∪ {mem[α].ι} ∧ c[α].ι ∈ MemStamp \ c[α].π ∧ c[α].κ = d[α] ∧ mem′ = mem ⊕ c

Refresh =^{Δ} ∃ X ∈ Subset MemLoc : Write(Drd(X )) Invar =^{Δ} ∧ mem ∈ Mem ∧ ∀ α ∈ MemLoc : ∧ mem[α].ι ∉ mem[α].π ∧ Infinite(mem[α].π)

Execution(input, output) =^{Δ} ∨ ∧ input ∈ ReadCall ∧ output = [\begin{matrix}stamps & ↦ & Ird(input.addr) \\ data & ↦ & Drd(input.addr)] \end{matrix} ∧ unchanged mem

∨ ∧ input ∈ WriteCall ∧ Valid(input.stamps) ∧ Write(input.data) ∧ output = “Ok”

∨ ∧ input ∈ WriteCall ∧ ¬Valid(input.stamps) ∧ unchanged mem ∧ output = “Interference”

Figure 2: Inside the memory.

Mem is a constant. It is the set of values which represent states of the array.

Ird is a state function operator. For a given subset X of MemLoc, the value of the state function gives the stamp of the current state of each cell with location in X .

Drd is a state function operator. For a given subset X of MemLoc, the value of the state function gives the data content of each cell with index in X .

Valid is a predicate operator. For given partial function c ∈ MemLoc \underrightarrow{} MemStamp the predicate holds if c gives the ages of the cells with indices in its domain.

Write is an action operator. For a given partial function d ∈ MemLoc \underrightarrow{} MemVal, a a step is an occurrence of the action Write(d) if the cells with indices in Domain d receive new version stamps, and possibly new values assigned from d. Other cells must be unchanged.

Refresh is an action. It is the action of changing the version stamps of some cells, while leaving the content of all cells undisturbed.

Invar is a predicate which holds at all times.

Execute is an action operator. Given a command and a response, a step is an occurrence of such an action if the command is legal, and the response and side effect are appropriate to the command.

Cread The memory is unchanged. The response consists of two partial functions with domain equal to the read parameter. One returns the memory contents, the other the cell version stamps.

Cwrite What happens depends on whether the input stamps are still valid. If so, the memory is written with the provided data, and the response is positive. If not, the memory is unchanged, and the response is negative. Note that either of the input parameters can be empty.

Tracking calls

The module InnerSched in figure ?? is an ‘inner’ module with variables exposed to view which will ultimately be hidden. In this, it is analogous to InnerMemory; but it has a much simpler state, consisting of two sets. These sets track procedure calls which have yet to reach their execution point, and those which have yet to return control to the caller. We suppose that everything works flawlessly: once a procedure call is issued, it is never lost, before execution or after. (So we leave out loss of messages and responses.) The module InnerSched imports MemParams for the sake of LegalCall and Op.

The declarations are of variables pending for the set of pending calls (which have not yet passed their execution point), and done for the set of calls which have. Then the module says what the variables are initially, and how they change. (Or rather, it defines names for predicates and actions which will be put to that use.)

Another approach would be to model the 3 events significant for a call with actions which are not defined to be disjoint. They are mythical events anyway,

module InnerSched

import MemParams

parameters pending, done : variable

Initial =^{Δ} pending = done = {} Entry(p, c) =^{Δ} ∧ c ∈ LegalCall ∧ pending′ = pending ∪ {⟨p, c ⟩} ∧ unchanged done

Commit(p, op) =^{Δ} ∧ op ∈ Op ∧ ⟨p, op.input ⟩ ∈ pending ∧ pending′ = pending \ {⟨p, op.input ⟩} ∧ done′ = done ∪ {⟨p, op ⟩}

Return(p, op) =^{Δ} ∧ ⟨p, op ⟩ ∈ done ∧ done′ = done \ {⟨p, op ⟩} ∧ unchanged done

Figure 3: Tracking the progress of calls

so it can no more matter that they should be disjoint than it can that they should not be disjoint. If they need not be be disjoint, then it is be possible for the same state change to be both a call of a procedure and its execution. It might even be possible for all 3 events to occur in a single externally visible step. What difference would it make if they did?

Assembling first specification

The module InnerAll in figure ?? defines actions which describe how changes to the memory and scheduling state are combined. The definition of the property Liveness is the trickiest to understand:

• When any call has been issued by any process, it will eventually get done. (It will not get lost on the way there.)

• Any done call eventually returns. (It will not get lost on the way back.)

• It cannot be the case that for some particular sets of addresses w and r, there is infinitely often a write pending to the addresses in w, conditional upon version stamps for the addresses in r which allow for successful completion, yet such a pending write is never executed successfully.

This condition is bogus, as discussed below.

Unfortunately, as it stands, the liveness condition allows an implementation to frustrate all efforts processes might make to have a conditional write execute successfully. The implementation can pretend that just before accepting

module InnerAll

import MemParams parameters

mem, pending, done : variable

include InnerMemory as M include InnerSched as S m =^{Δ} ⟨intMem, mem, pending, done ⟩ Init =^{Δ} M .Invar ∧ S.Initial Entry(p) =^{Δ} ∃ c ∈ LegalCall : ∧ Pr.Call(p, c) ∧ S.Entry(p, c) ∧ unchanged mem

Do(p, in, out) =^{Δ} ∧ S.Commit(p, [input ↦ in, output ↦ out]) ∧ M .Execution(in, out)

Ret(p) =^{Δ} ∃ op ∈ Op : ∧ Pr.Return(p, op.output) ∧ S.Return(p, op) ∧ unchanged mem

Next =^{Δ} ∨ ∃ p : Entry(p) ∨ ∃ p : Ret(p) ∨ ∃ p : ∃ op ∈ Op : Do(p, op.input, op.output) ∨ M .Refresh

Safety =^{Δ} Init ∧ □[Next]_{m} Liveness =^{Δ} Bogus! See text.

∀ p : ∧ WF_{m}(Ret(p)) ∧ ∀ input ∈ LegalCall : WF_{m}(∃ out : Do(p, input, out)) ∧ WF_{m}(Ret(p)) ∧ ∀ input ∈ LegalCall : ∧ WF_{m}(∃ out : Do(p, input, out)) ∧ SF_{m}(input.cmd = “CWrite” ∧ Do(p, input, “Ok”))

Spec =^{Δ} Safety ∧ Liveness

Figure 4: Combining the two inner modules.

module Memory

import MemParams include InnerAll as I (pending, done, mem)

ComponentSpec =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ p, d, m : I (p, d, m).Spec Environment =^{Δ} Pr.LegalCaller ClosedSpec =^{Δ} Environment ∧ ComponentSpec AGSpec =^{Δ} Environment −▷^{+} ComponentSpec

Figure 5: Specification of simpler memory. any such write, it had refreshed a cell covered by the version-stamps, thereby rendering the liveness promise void. That is certainly not what is intended. It seems that something has to be added to the precondition of the Refresh action, to prevent such a step intervening between each read which obtains version stamps on a set r and any subsequent write conditional on the continued validity of r’s stamps.

A Refresh action can frustrate any attempt to accomplish the effect of an atomic read-modify-write action. What is it Refresh doing in the specification? It is there to allow for designs that base version stamps upon the addresses at which the data resides in a hidden low-level store; and to allow for occasional reorganisations of the hidden store of such a kind as to invalidate the version stamps. It is in the nature of such ‘house-keeping’ reorganisations that if a point comes after which no new data is ever successfully written, then sooner or later, there is no excuse for further house-keeping. So if there are infinitely many Refresh actions, there must also be infinitely many successfull executions of conditional writes. (This is the least one can ask for; it might be reasonable to expect that writes in one part of the address space are not automatically an excuse for refreshes in a completely different one.)

It is not hard to write a formula which rules out over-refreshing as a formula of temporal logic; but it is not so easy to accomodate it within the canonical form

∃ ∃ ∃ ∃ ∃ ∃ hidden : Init ∧ □[Next]_{⟨hidden,exposed ⟩} ∧ Fairness

in which Fairness stands for a (countable) conjunction of weak and strong fairness formulae: at least not without adding some auxiliary variables. We have to strengthen the precondition for Refresh-ing a set of addresses so that it is not always enabled. We have to make Refresh do something to bring about its eventual disablement. Something like the following seems to be required:

• a new ∃ ∃ ∃ ∃ ∃ ∃ -quantified variable, to count down towards a Refresh becoming disabled.

• a new constant for a well founded ordering, that the counting-down variable counts down through.

• a new conjunct in the subformula of Execution, which allows the new variable to assume any value in the field of the well ordering.

• a new conjunct in the definition of Refresh, which requires the new variable to be diminished.

While the strong fairness condition formulated above has no power to distinguish a bona-fide memory from a cheat which aborts all conditional writes, on the other hand the repair which I have just suggested might be made to it is in too abstract a form to characterise more than a broad family of devices, between which the differences are more interesting than the similarities.

With some systems, it may be uninteresting, if not unbelievable that an abtract logical fairness condition holds from the standpoint of eternity. It may more pertinent for practical life that the set of behaviours in which it does not hold is vanishingly unlikely, under certain messy quantitative conditions. (In this connection, I am thinking of workstations colliding over an ethernet cable, with randomised adaptive backoff.) The role of the concept of fairness in practical engineering is comparable (perhaps) to that of the concept of convergence to an ideal point (which underlies practical measurement).

Setting aside these misgivings about how satisfactory the liveness specification is, the module Memory in figure ?? defines formulae ClosedSpec and AGSpec, which describe the behaviour of the variable intMem, when

• the environment and component both behave properly.

• any misbehaviour of the component is the environment’s fault.

The more complex memory

The more complex memory has more operations, with more parameters, and a more complex state.

One of the extra parameters is something to identify the local branch or outpost of the distributed memory service you are using. The memory service itself doesn’t fail, only its various outposts, of which there are plenty. Instead of “outpost”, the terminology for the unit of local failure is “clerk”. A clerk is something that you need to use the distributed memory. You get one by asking for one; you probably get the same one as other people in the same geographical area.

The function of a clerk is to buffer the local clients from the rest of the service. This is for speed. The price is that if a clerk should suddenly halt, its buffer contents, including recently ‘written’ data, may be lost. The extra operations of the more complex memory are for limiting such loss. They are as follows:

• wait for the local copy of some data to be synchronised with the global view of the data. This operation is called “Synch”: it takes a set of locations as input, and has no significant output (just return of control).

Example: a local component using the memory service receives an external stimulus, which it interprets as a command of some kind. It fires off a number of asynchronous writes to satisfy the command, calls Synch to wait till the results have been synchronised, then responds to the stimulus.

• artificially constrain the order in which writes become globally visible. This operation is called “Barrier”. Its application is to make sure that the debris that might be left should the clerk suddenly die still satisfies the preconditions for application recovery. Its function is described below, in terms of how buffered operations may ‘overtake’ each other, between being issued and having a globally visible effect.

In intuitive terms, the rules for ‘overtaking’ between buffered operations are these:

• For a single cell, writes become visible only in order of issue. They are like beads on a wire, which cannot overtake each other.

• Sets of cells may be written atomically (as it were, with beads on different wires fused into a ‘wunner’). Through an intermediate chain of consecutively overlapping writes, two writes with no location in common may be constrained to execute in the order in which they are issued. A “Barrier” operation is like a write to the addresses in its argument set, which rewrites the same values that are already there; however, unlike a genuine write, it does not change the version stamps of the cells. The purpose of it is to introduce order constraints artificially, where they are not already implied by the natural data dependency of operations.

• Reads may be ‘pulled back’ into writes, through the use of version stamps in the condition part of a write. When a write with a non-empty conditional part executes successfully, it is as if the original values of the original reads had instead been read in the very start-state of the step in which the data is written. So such a read must appear to execute in the same atomic step as the write conditional upon the continued validity of its version stamps. For a single cell, the order of reads with respect to writes is consistent with the order in which they are issued; but reads of the same cell may be ‘pulled back’ into writes which become visible in a different order from that in which the reads are issued.

(Apology: that is as clear as mud.)

No one operation in the interface of the more complex memory has the effect as the conditional write operation of the simpler memory. Rather, the effect of that operation is the same as following a call an asynchronous conditional write operation with a Synch operation. The Synch operation waits until the real memory has caught up with the slightly futuristic view of it a clerk has been giving out. (The clerk’s local view of the future is naturally one in which it is going to play a part; but fate may already have decided otherwise.)

Description of the extra complexity needs a constant memClerk for the set of possible clerks, and variables to track them through their lives: birth, the onset of mortality (as it were, of incurable cancer of the address space), and death. In terms of these we define the syntax and semantics of operations which create new ones, or are issued to specific clerks. Also needed are variables to represent the view each clerk has of what is going to happen. Most of the time, we can pretend that it has actually happened; these variables only come into play when cancer has already taken root, but may not yet have been detected. They describe how the cancer spreads.

The parameters of the interface procedures for the more complex memory are collected into the module in figure ??. It is (in some sense) an extension of module MemParams in figure ??.

The trivial module Life in figure ?? deals with general aspects of creation and destruction. It defines two actions Birth and Death, which describe steps in which an entity comes into being, and ceases to be.

The module Mortality in figure ?? is concerned with a memory which may return bad results in response to a read command, and can lose data it said it wrote: it is permitted a degree of bad faith. There are however crucial limits on this bad faith, with which the lying must be consistent. To describe these limits, we introduce a variable liedAbout to remember the cells which have been lied about, and a variable willLose to remember the cells for which the lie was made in responding positively to a write request. export

MemParams, Pr

parameters intMem : variable MemLoc, MemVal, MemStamp, MemClerk : constant

assumption ParamAssump =^{Δ} ∧ Infinite(MemStamp) ∧ MemLoc ≠ {} ∧ MemVal ≠ {} ∧ Infinite(MemStamp) ∧ Infinite(MemClerk)

Opcode =^{Δ} {“Create”, “Cread”, “Cwrite”, “Synch”, “Barrier”} Op =^{Δ} \{\} ∪ [\begin{matrix}cmd & : & \{“Create”\} \\ h & : & MemClerk] \end{matrix} ∪ [\begin{matrix}cmd & : & \{“Cwrite”\} \\ h & : & MemClerk \\ stamps & : & MemLoc \underrightarrow{}MemStamp \\ data & : & MemLoc \underrightarrow{}MemVal \\ status & : & \{“Ok”, “Interference”, “Stopped”\}] \end{matrix} ∪ \begin{cases}r ∈ [\begin{matrix}cmd & : & \{“Cread”\} \\ h & : & MemClerk \\ addr & : & Subset MemLoc \\ stamps & : & MemLoc \underrightarrow{}MemStamp \\ data & : & MemLoc \underrightarrow{}MemVal \\ status & : & \{“Ok”, “Stopped”\}] \end{matrix} \\ : ∧ Domain (r.stamps) = Domain (r.data) ∧ Domain (r.data) ⊆ r.addr\} \end{cases} ∪ [\begin{matrix}cmd & : & \{“Synch”, “Barrier”\} \\ h & : & MemClerk \\ addr & : & Subset MemLoc \\ status & : & \{“Ok”, “Stopped”\}] \end{matrix}

InputField(op) =^{Δ} case

op.cmd = “Create”  → {}
op.cmd ∈ {“Cread”, “Synch”, “Barrier”} → {“h”, “addr”}
op.cmd = “Cwrite”  → {“h”, “stamps”, “data”}

Input(op) =^{Δ} InputField(op) ⊲ op Output(op) =^{Δ} InputField(op) − ⊲ op include ProcedureInterface as Pr with c ← intMem, Arg ← LegalCall

Figure 6: Parameter module for asynchronous memory

module Life

parameters Entity : constant born, dead : variable

Invar =^{Δ} dead ⊆ born ⊆ Entity Initial =^{Δ} dead = born = {} Birth(c) =^{Δ} ∧ c ∈ Entity \ born ∧ born′ = born ∪ {c} ∧ unchanged dead

Live =^{Δ} (born \ dead) Death(c) =^{Δ} ∧ c ∈ Live ∧ dead′ = dead ∪ {c} ∧ unchanged born

Being =^{Δ} ⟨born, dead ⟩

Figure 7: Birth, life, and death

module Mortality

import MemParams parameters

liedAbout, willLose : variable

Fibs =^{Δ} ⟨liedAbout, willLose ⟩ Invar =^{Δ} willLose ⊆ liedAbout ⊆ MemLoc Fits(r, w) =^{Δ} ∧ r, w ⊆ MemLoc ∧ w ∩ liedAbout = {} ∧ r ∩ willLose = {}

Spread(r, w) =^{Δ} ∧ liedAbout′ = liedAbout ∪ r ∪ w ∧ willLose′ = willLose ∪ w

Figure 8: How loss and lies spread.

module InnerMemory2

import MemParams2

parameters view : variable lies, loss : variable born, dead : variable

TheLot =^{Δ} ⟨mem, view, bad, born, dead ⟩ include InnerMemory as V (c) with view ← view[c] include Life as Clerk with Entity ← MemClerk include Mortality as M (c) with liedAbout ← lies[c] willLose ← loss[c]

Invar =^{Δ} ∧ Clerk.Invar ∧ ∀ c ∈ Clerk.Live : M (c).Invar ∧ V (c).Invar ∧ ∀ c_{1}, c_{2} ∈ Clerk.Live a ∈ MemLoc \ (loss[c_{1}] ∪ loss[c_{2}]) : view[c_{1}, a] = view[c_{2}, a]

Correct(c) =^{Δ} lies[c] − ⊲ view[c] GoodWrite(op) =^{Δ} ∧ unchanged Clerk.Being ∧ op.h ∈ Clerk.Live ∧ M (op.h).Fits(Domain (op.data), Domain (op.stamps)) ∧ V (op.h).Valid(op.stamps) ∧ V (op.h).Write(op.data) ∧ ∀ c ∈ Clerk.Live : if M (c).Fits(Domain (op.data), Domain (op.stamps)) then ∧ unchanged M (c).Fibs ∧ view′[c] = view[c] ⊕ (Domain (op.data) ⊲ view[op.h]) else ∧ M (c).Spread(Domain (op.data), Domain (op.stamps)) ∧ unchanged view[c]

SynchOk(c, as) =^{Δ} ∧ c ∈ Clerk.Live ∧ as ⊆ MemLoc \ bad[c].lies

BadClerk(c, as) =^{Δ} ∧ as ∩ bad[c] ≠ {} ∧ Clerk.Death(clerk) ∧ unchanged ⟨mem, view, bad, born ⟩

Figure 9: Inside the more complicated memory … ReadPart(input) =^{Δ} let c =^{Δ} input.par.stamps; d =^{Δ} input.par.data in Domain c \ Domain d

WritePart(input) =^{Δ} let c =^{Δ} input.par.stamps; d =^{Δ} input.par.data in Domain d \ Domain c

ModifyPart(input) =^{Δ} let c =^{Δ} input.par.stamps; d =^{Δ} input.par.data in Domain c ∩ Domain d

Affected(input) =^{Δ} ReadPart(input) ∪ WritePart(input) ∪ ModifyPart(input) CwriteDo(clerk, input, output) =^{Δ}

∧ VMem(clerk).Execute(input, output)

∧ if bad[clerk] ∩ Affected(input) ≠ {} then ∧ bad′ = [bad except ![clerk] = @ ∪ WritePart(input)] ∧ unchanged mem else ∧ unchanged bad ∧ mem′ = mem ⊕ (WritePart(input) ⊲ view′[clerk])

CreadDo(clerk, input, output) =^{Δ}

∧ VMem(clerk).Execute(input, output) Dispatch(clerk, input, output) =^{Δ}

∧ input.opc = “Synch” ⇒ SynchDo(clerk, input) ∧ input.opc = “Cwrite” ⇒ CWriteDo(clerk, input) ∧ input.opc = “Cread” ⇒ CReadDo(clerk, input) ∧ …

Execute(input, output) =^{Δ} ∧ input ∈ LegalCalls ∧ if input.opc = “Create” then ∃ c ∈ MemClerk : ∧ Clerk.Birth(c) ∧ view′ = [view except ![c] = mem] ∧ bad′ = [bad except ![c] = {} ∧ unchanged memoutput = c else if Clerk.Live(input.par.clerk) then Dispatch(input.par.clerk, C 2S(input), output) else unchanged TheLot ∧ output = “No such clerk”

…

Figure 10: … Inside the more complicated memory.

References

[1] The Dagstuhl Problem–TLA^{+} Solution, Martín Abadi, Leslie Lamport, and Stephen Merz, Tue 23 Aug 1994 [12:12]