Cliff B Jones

Ken G Pierce

Elucidating concurrent algorithms via layers of abstraction and reification

Arguing that intricate concurrent programs satisfy their specifications can be difficult; recording understandable explanations is important for subsequent readers. Abstraction is a key tool even for sequential programs. The purpose here is to explore some abstractions that help readers (and writers) understand the design of concurrent programs. As an illustration, the paper presents a formal development of a non-trivial parallel program: Simpson's implementation of asynchronous communication mechanisms (ACMs). Although the correctness of this "4-slot algorithm" has been shown elsewhere, earlier proofs fail to offer much insight into the design. From an understandable (yet formal) design history of this one algorithm, the techniques employed in the explanation are teased out for wider application. Among these techniques is using a "fiction of atomicity" as an aid to understanding the initial steps of development. The rely-guarantee approach is, here, combined with notions of read/write frames and "phased" specifications; furthermore, the atomicity assumptions implied by the rely/guarantee conditions are achieved by clever choice of data representations.

Introduction

This paper is intended to contribute to methods of developing parallel programs; in particular it extends the repertoire of ways of "splitting (software) atoms safely". As an illustration, it explains an intricate parallel program.

The general case for developing programs from abstractions is taken as read (cf. [START_REF] Jones | Systematic Software Development using VDM[END_REF][START_REF] Pierce | The B-Book: Assigning programs to meanings[END_REF]). The VDM literature uses the terms "operation decomposition" and "data reification" for design steps of sequential programs and provides proof obligations to justify such steps. Even if -as here-what is being recorded is a rational reconstruction of a design, the resulting documentation offers clarity and captures a design history to inform subsequent modification.

Research on rely/guarantee conditions (see Section 1.2 below) extends the formal tools so as to cope with shared-variable concurrent programs. As has been repeatedly made clear in the literature, "compositionality" is essential to derive real pay off from a "posit and prove" approach.

More recently, research has looked at using a "fiction of atomicity" [START_REF] Jones | Wanted: a compositional approach to concurrency[END_REF] as an additional abstraction in the specification of parallel programs; the corresponding development notion is sometimes referred to as "splitting (software) atoms safely"; an example of this approach is the transformation rules for πoβλ as in [START_REF] Jones | Accommodating interference in the formal design of concurrent object-based programs[END_REF]. This paper uses rely/guarantee conditions in reasoning about "splitting atoms". In particular, the example illustrates the combination of rely/guarantee reasoning with data reification as outlined in [START_REF] Jones | Splitting atoms safely[END_REF].

Correspondence and offprint requests to: cliff.jones@ncl.ac.uk

The example application chosen concerns "Asynchronous Communication Methods" -specifically, the four-slot implementation of ACMs published by Hugo Simpson [START_REF] Simpson | New algorithms for asynchronous communication[END_REF] 1 -see Section 2. The algorithm is ingenious and its correctness by no means obvious. Rather than being just another proof, our hope is that this development offers insight into why Simpson's algorithm satisfies the requirements.

A comment is perhaps in order here about the use of support tools in establishing formal properties of programs. The current authors are working on such tools but consider it crucial that one's ideas are clear before using support tools. Furthermore, one should be wary of tools that constrain modes of expression so that one ends up "coding" intuition into a restricted language.

The main message of the current paper is however the (generic) approach outlined: Section 5 restates the methods used so that it is clear what the reader can take from the specific example to other specification and design challenges. Clearly not all applications will use exactly the set of ideas here: many applications will be less demanding than Simpson's intricate algorithm -doubtless, other approaches will also be invented or deployed. But the authors hope that readers can derive benefit from the collection of ideas used here.

Although this paper offers comparisons (see Section 6), it is quite specifically not competitive. The first author co-supervised Neil Henderson's PhD and encouraged the view that each of the approaches used in [START_REF] Henderson | Formal Modelling and Analysis of an Asynchronous Communication Mechanism[END_REF] threw different light on the intricate algorithm that has also been chosen for the current paper. Furthermore, this paper differs significantly from the earlier (invited) conference paper on the same topic [START_REF] Jones | Splitting atoms with rely/guarantee conditions coupled with data reification[END_REF] and Section 6.5 reviews the reasons for the changes. The remainder of this section briefly sketches state-of-the-art methods; any reader who is totally unfamiliar with any of these approaches should consult the cited publications.

Data reification

For many systems, data abstraction is key to achieving a concise and perspicuous specification. An algorithm might be easy to specify or describe in terms of tractable mathematical objects; its implementation might have to represent the abstraction in a complicated way -perhaps to achieve performance. Separation of these issues results in clearer documentation of design histories.

The preferred data reification development rule in VDM [START_REF] Jones | Systematic Software Development using VDM[END_REF] works where the chosen representation (of the abstraction) can be understood using a "retrieve function" that is a many-to-one mapping from the representation back to the abstraction. This is possible where the abstraction is free from "implementation bias". The preferred VDM reification rule basically checks that (starting with a representation state) composing the retrieve function with the post condition of an abstract operation gives the same result as composing the post condition of the operation on the representation with the retrieve function. There are restrictions to pre conditions -but here they are minimal-and an obligation to prove "adequacy" of a representation. All of this is explained in [Jon90, Chapter 8].

There are however situations where the abstraction has to record information to express potential nondeterminacy and this information is superfluous in a step of development that reduces the non-determinacy. In a sense this is intentional "bias" in the abstraction. In such situations it is necessary to use the development rule introduced by Tobias Nipkow in [START_REF] Nipkow | Non-deterministic data types: Models and implementations[END_REF][START_REF] Nipkow | Behavioural Implementation Concepts for Nondeterministic Data Types[END_REF] that expresses a general relation between the abstraction and its reification. For an exhaustive discussion of "data refinement" see [START_REF] De Roever | Data Refinement: Model-Oriented Proof Methods and Their Comparison[END_REF]; for a historical account of the development of the VDM rules see [START_REF] Jones | Data reification[END_REF].

Rely/guarantee thinking

Just as pre conditions simplify a designer's task by limiting the starting states in which the specified object is to be deployed, rely conditions indicate assumptions that a developer is allowed to make about the expected interference to a (shared-variable) concurrent program. Similarly, guarantee conditions can be compared to post conditions in that both are constraints on the behaviour of the created program.

VDM's operation decomposition rules for sequential programs have always used post conditions that relate the final state to the initial state (this is in contrast to the many approaches that try to get by with predicates of the final state). Both rely and guarantee conditions are also relations between two states.

The general idea of documenting and reasoning about interference has many embodiments; some of the 1 The authors are grateful to the reviewer who pointed out earlier relevant work -see Section 6.

references are [START_REF] Jones | Development Methods for Computer Programs including a Notion of Interference[END_REF][START_REF] Jones | Specification and design of (parallel) programs[END_REF][START_REF] Jones | Tentative steps toward a development method for interfering programs[END_REF][START_REF] Jones | Accommodating interference in the formal design of concurrent object-based programs[END_REF] but a number of other theses have extended the basic idea.2 As the title of this section suggests, the approach is seen as a general way of thinking and reasoning about the design of concurrent systems rather than being limited to a specific set of rules. (In fact, the general approach can also be applied to communication-based concurrency.) Rules for introducing parallel program constructs are similar to those for sequential programming; examples are presented in [START_REF] Coleman | A structural proof of the soundness of rely/guarantee rules[END_REF] and [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF] discusses why there are more choices to be made for concurrent -rather than the sequential-rules. Interestingly, no rule for the introduction of concurrent constructs is needed in the development below because concurrency is present in the initial specification. Once again, de Roever provides an encyclopaedic treatment in [dR01]; a particularly valuable contribution is the clear identification of the fact that rely/guarantee thinking achieves "compositionality". A further aspect of this is studied in [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF] which makes clear that "auxiliary variables" can be used in ways that can damage compositionality.

Atomicity refinement

A more recent development is the link made in [START_REF] Jones | Splitting atoms safely[END_REF], between the achievement of a rely/guarantee specification and the designer's ability to find an appropriate data representation. This observation throws light on several older developments and is crucial to the design step in Section 4 below. Essentially, an abstraction is used that could be said to be using the "fiction of atomicity". The splitting of operations that have to be atomic on the abstraction is made possible by judicious choice of representation. So, for example, a variable whose monotonic reduction would imply locking can be represented by an expression involving the minimum of two values each of which can only be updated by one of two parallel processes. This topic is discussed in more detail in [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF].

ACMs and their specification

The abstraction and development ideas are first illustrated (in this section and Sections 3, 4) on a specific example and then refreshed in Section 5.

Asynchronous Communication Methods (ACMs) address an extremely interesting application scenario. Consider two processes that are independently timed in the sense that they are not synchronised in any way (thus "asynchronous"); furthermore, suppose that one process produces values that are to be "communicated" to the other (one writes and the other reads); the key requirement is that communication must be achieved with no delay to either process. Thus it is not, for example, possible to use a conventional shared variable -access to which is controlled by some device such as semaphores-since this can delay a process waiting for a lock to be released. To sharpen the issues, it might be useful to think of Values below as being large -something that certainly can't be assigned in one machine cycle ("atomically"). ACMs are used in important high speed communication situations such as passing values from sensors to flight control software.

Sections 3 and 4 present a formal development of a well-known -and extremely ingenious-implementation of ACMs but it is clearly necessary to offer a formal starting point for such a development. The aim here is to provide a way of specifying ACM behaviour with which a user can feel comfortable.

It would fit the "splitting atoms" programme nicely if it were possible to present a specification using a simple (atomic) variable. Such a simple model would show that successive reads can see the same written value. This is because there is no synchronization between the process writing and that reading and two reads can occur without an intervening write.

Unfortunately, the highly asynchronous nature of ACMs brings further complications that mean a single simple variable is not an appropriate abstraction because it does not show all potential behaviours of an ACM. It is necessary to consider, even in the specification, the question of what behaviours are allowed when reading and writing overlap in time. The obvious case of new behaviour comes when a read action starts but a complete write executes before the read finishes. In such a case, the read is allowed to return either the value at the start of the read or that at the end. This can be extended to the case where multiple writes "overtake" a read. The specification below splits read actions into start-Read and end -Read sub-actions in order to show this behaviour. This is done in a way that makes an essential limitation on the behaviour: two successive reads must not be able to return first a "newer" value followed in time by an "older" value.

A number of non-obvious consequences follow from the asynchronous essence of ACMs. The simplest is that it is certainly valid for the reader to see the same value multiple times if it cycles faster than the writer. Specifying ACMs in an understandable way is itself non-trivial. (See Section 6 for alternative specifications.) Sections 2.1 and 2.2 attempt to offer intuition before the actual specification is given in Section 2.3.

Intuition from pseudo-code

Consider the following pseudo-code:

INIT ; Ñ while true do Write(v : Value) < data-w ← data-w [v ] > od || while true do Read ()r : Value < r ← data-w (len data-w ) > od é
This would allow observable behaviours like (v going into Write; r coming out of Read ): in: [x , y, z ] out: [x , x , z , z ] These are (two) important aspects of asynchronous communication: the same value can be read more than once and written values might never be read. 3"Atomic brackets" (< • • • >) are used in this pseudo-code because of multiple references to shared variables. (Note that no assumption about assignment statements being executed atomically is made herecf. [START_REF] Coleman | A structural proof of the soundness of rely/guarantee rules[END_REF].) Ultimately, we seek an algorithm whose only atomicity assumption is that single bit indicators can be set atomically (think of this as a signal on a single wire). There is a technique here that is familiar from the database world: that is the split of making change (to data-w ) then committing it (by update to fresh-w ).

So far, so good, but the pseudo-code above does not give us a way of discussing the issue of the Read and Write overlapping which is another important facet of asynchronous behaviour. What for example are the permitted behaviours of Read s and Writes overlapping? More behaviours can be discussed if we split both Read and Write into two phases. With states:4 Σ a :: data-w :

Value * fresh-w : N 1 hold -r : N 1 inv (mk -Σ a (d -w , fr -w , ho-r )) 1 ≤ ho-r ≤ fr -w ≤ len d -w init mk -Σ a ([x], 1, 1)
It is obviously necessary to initialise the state. Most authors who give formal presentations do this by assuming that a value, say, x has been written and read once. This can be shown as in init-Σ a .

The observable behaviour (permissible outputs) comes from the pseudo-code in Figure 1. We use a "fiction of atomicity" -but split Write and Read each into two parts. The division of the write action (into start-Write and commit-Write) is not strictly necessary as far as admitting extra behaviours but it is a convenient way of discussing the overlap between read and write operations: remembering that the values being passed might be large in the sense that they might not be changed by a machine in one atomic action, it is useful to think about readying the data before it is committed. 5The idea here is that data-w retains all values written; start-Write first stores a new value but only commit-Write releases it for access by updating fresh-w . Conversely, start-Read notes the index of values that must be regarded as "fresh" and end -Read makes a non-deterministic choice of an index between the hold -r and the value of fresh-w at the time of completion of the read. (The suffixes of the variable names The sub-actions can be characterised by the pseudo-code shown in Figure 1. Although end -Read might not select the newest item in the sequence, a value only becomes old when a newer item is returned. Since start-Read sets hold -r to the value of fresh-w before the choice is made and hold -r is never greater than fresh-w , the read process cannot return an "old" value (though the same value may be returned more than once).

while true do start-Write(v : Value) < data-w ← data-w [v ] > ; commit-Write() fresh-w ← len data-w od || while true do start-Read () hold -r ← fresh-w ; end -Read ()r : Value r ← data-w (hold -r ) od Fig. 1. Pseudo-code description of ACM start-Write(y) .. mk -Σ a ([x, y], 1, 1) commit-Write() .. mk -Σ a ([x, y], 2, 1) start-Read () .. mk -Σ a ([x, y], 2, 2) end -Read () .. r = y Fig. 2. Sequential case start-Write(y) .. mk -Σ a ([x, y], 1, 1) start-Read () .. mk -Σ a ([x, y], 1, 1) end -Read () .. r = x commit-Write() .. mk -Σ a ([x, y], 2, 1) Fig. 3. Interleaved case start-Read () .. mk -Σ a ([x], 1, 1) start-Write(y) .. mk -Σ a ([x, y], 1, 1) commit-Write() .. mk -Σ a ([x, y], 2, 1) start-Write(z) .. mk -Σ a ([x, y, z], 2, 1) commit-Write() .. mk -Σ a ([x, y, z], 3, 1) end -Read () .. r ∈ {x, y, z} start-Read () .. mk -Σ a ([x, y, z], 3, 3) end -Read () .. r = z
The continued use of atomic brackets around changes to data-w is an indication of development work still required (see Section 2.5).

Intuition from selected test cases

Figures 2, 3 and 4 give possible executions of the pseudo-code (giving the operation name and corresponding final sate). Figure 2 is a simple sequential write and read: y is added to data-w , marked as fresh and subsequently read. In Figure 3, the read begins before the write ends and the read yields x.

The more complex case in Figure 4 shows the non-determinism of the read operation. By the time end -Read is ready to return a result, three possible values are available and one will be selected nondeterministically. Note however that a subsequent read can return neither x nor y because hold -r is updated to the value of fresh-w at the start of the read.

Write(v : Value) owns wr data-w , fresh-w start-Write(v : Value) wr data-w guar {1..fresh-w } ¡ data-w = {1..fresh-w } ¡ ---- data-w post data-w = ---- data-w [v ] commit-Write()
wr fresh-w rd data-w guar ---fresh-w ≤ fresh-w post fresh-w = len data-w Read ()r : Value owns wr hold -r start-Read ()

wr hold -r rd fresh-w guar ---- fresh-w ≤ fresh-w post hold -r ∈ ˚ fresh-w end -Read ()r : Value rd data-w , hold -r rely data-w (hold -r ) = ---- data-w (hold -r ) post r = data-w (hold -r )

A specification

The pseudo-code in Figure 1 is brief and offers the intuition of what can happen 6 but for the development that follows, this needs to be presented as formal (VDM) specifications of the four operations. Furthermore, the specification has to cover interference. This is exactly the role of rely/guarantee conditions (cf. Section 1.2). Figure 5 uses VDM's rd/wr markings; in addition, it employs owns wr to indicate that no parallel process is allowed to write into these variables. This simplifies the rely conditions. Note that there are no variables changed by both Read and Write. 7 The efficacy of these markings is addressed in the thesis of the second author [START_REF] Pierce | Enhancing the Useability of Rely-Guaranteee Conditions for Atomicity Refinement[END_REF]. "Phasing" shows start-Write and commit-Write can't interfere with each other (nor can start-Read and end -Read ). This reduces the complexity of the rely/guarantee conditions, it avoids the need for (auxiliary vars, and) implications and it simplifies the subsequent proofs.

A new notation (since the formulation in [START_REF] Jones | Splitting atoms with rely/guarantee conditions coupled with data reification[END_REF]) is the use of Û x for any "possible values" that can occur during the execution of the operation. Notice that it is possible for { ---fresh-w , fresh-w } ⊂ ˚ fresh-w ; in fact, there could be an arbitrary number of changes to the variable fresh-w if the Write process cycles faster than Read . The concept of "any possible values" is intuitive and it seems reasonable to grace it with a formal expression. We could actually avoid the need to write ˚ fresh-w at this point because the range of indices {hold -r ..fresh-w } offers a form of auxiliary variable -but such fortuitous auxiliary variables are not always to hand and [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF] presents reservations about adding auxiliary variables. Finally, the use of ˚ fresh-w in Section 3.2 cannot be avoided without a specially contrived auxiliary variable.

An astute reader might be worried that massive assumptions are being made here about what can be changed atomically. Such assumptions have to be eliminated in subsequent development. What is achieved 6 For those who feel queasy about the use of sequentially composed sub-operations in a specification, Section 6 discusses alternatives. Furthermore, the approach of the current section can be proved to give the same behaviours as attempts at more "implicit" specifications. 7 The suffixes of names such as fresh-w , hold-r provide a useful reminder of which process can write to the variable.

here is to show that the "fiction of atomicity" idea can provide an intuitive understanding of extremely delicate code.

The details of the rely and guarantee operations are, here, made much simpler to write because of the way that the sub-operations are ordered (by semicolon). Were one to try to record specifications of the entire Read and Write operations, they would be festooned with implications. The structure of the program (e.g. that Write cannot interfere with Write) simplifies the specifications of the sub-operations.

Proofs

Even on a specification, there are proof obligations: notably involving inv -Σ a . Initial state satisfies invariant: inv -Σ a (σ a 0 ) is immediate Preservation of inv -Σ a by each operation:

The argument needs a form of "dynamic invariant":

dinv -Σ a : Σ a × Σ a → B dinv -Σ a (mk -Σ a (d -w , fr -w , ho-r ), mk -Σ a (d -w , fr -w , ho-r ))
fr -w ≤ fr -w

We need to prove that each operation preserves the invariant; we simultaneously cover the dynamic invariant.

∀ - σ a ∈ Σ a • post-start-Write a ( - σ a , in, σ a ) ⇒ dinv -Σ a ( - σ a , σ a ) ∧ σ a ∈ Σ a is immediate. ∀ - σ a ∈ Σ a • post-commit-Write a ( - σ a , σ a ) ⇒ dinv -Σ a ( - σ a , σ a ) ∧ σ a ∈ Σ a
needs information from the invariant to establish the dynamic invariant.

∀ - σ a ∈ Σ a • post-start-Read a ( - σ a , σ a ) ⇒ dinv -Σ a ( - σ a , σ a ) ∧ σ a ∈ Σ a is immediate. ∀ - σ a ∈ Σ a • post-end -Read a ( - σ a , σ a ) ⇒ dinv -Σ a ( - σ a , σ a ) ∧ σ a ∈ Σ a is trivial since σ a = - σ a .

Taking stock

This section has established a clear specification in Figure 5; the non-determinism allowed is important in that it reflects details of timing. The rely/guarantee conditions are an essential aspect of the specification because they ensure mutual exclusion. That having been said, all of the development work remains to be done. In particular, it is clear that the atomicity considerations have to be relaxed -it is our claim that the key to splitting the atomicity constraints is data reification. In fact, finding a more economical representation is the next task.

Reusing cells without clashing

It should be obvious that the behaviour of the algorithm does not depend on retaining all of the values in data-w . This step of development introduces a potential reduction in the number of Values retained by storing them in a mapping indexed by an arbitrary set X . The essence of this step is to show "ownership" of the indices (in X ); in particular, that an element of data-w whose index could be used by Read is not overwritten. Essentially, a careful data reification step is bringing in some of the design decisions without going all the way to Simpson's code. Rely/guarantee conditions are again used to investigate the requirements.

The state used throughout this section is:

Σ i :: data-w : X m -→ Value fresh-w : X hold -r : X hold -w : X inv (mk -Σ i (d -w , fr -w , ho-r , ho-w )) {fr -w , ho-r , ho-w } ⊆ dom d -w init mk -Σ i ({α → x}, α, α, α)
Note that hold -w is strictly local (not even accessed by Read ). We did consider using a special notation for local hold -w but it actually saves little.

Intuition from pseudo-code

It is again possible to use pseudo-code to convey the intuition of what has to be given below as a formal specification -this is presented in Figure 6. Notice that the Write process now needs to access hold -r : essentially, this means that the Read process can communicate the fact that a certain cell must not be destroyed or corrupted.

Specifications of the sub-operations on Σ i

The specifications of the four sub-operations are shown in Figure 7. There is masses of non-determinism here -in fact, one valid implementation is to have X = N 1 and retain the whole sequence as in Section 2 -but it is shown below that card X must be at least 3 (cf. start-Write) -we return to this point in Section 3.4.

The Write process in Section 2.3 avoided destroying (or even worse, corrupting) any Value required by Read by concatenating new values to the end of data-w (and only exposing them in commit-Write) -we now need to be more explicit about setting hold -w (R/G to the rescue).

The post condition of start-Write clearly shows that we need at least three slots in order to avoid "race conditions" on individual Values.

The property in rely-start-Write (mirrored in guar -Start-Read ) ensures that there are only two possible values during any single execution of start-Write.

Notice that -in contrast to the situation with ˚ fresh-w in Section 2.3-here, we can only talk about the possible values of fresh-w in start-Read by use of the new notation (or by adding auxiliary variables).

Write(v : Value) owns wr data-w , fresh-w , hold -w start-Write(v : Value) wr data-w , hold -w rd hold -r , fresh-w

rely hold -r = --- hold -r ⇒ hold -r = fresh-w guar ḣold -r ¡ data-w = ḣold -r ¡ ---- data-w post hold -w / ∈ { --- hold -r , fresh-w } ∧ data-w = ---- data-w † {hold -w → v } commit-Write()
wr fresh-w rd hold -w post fresh-w = hold -w

Read ()r : Value owns wr hold -r start-Read () wr hold -r rd fresh-w guar hold -r = --hold -r ⇒ hold -r = fresh-w post hold -r ∈ ˚ fresh-w end -Read ()r : Value rd data-w , hold -r rely data-w (hold -r ) = ---data-w (hold -r ) post r = data-w (hold -r ) Fig. 7. Rely/guarantee specifications on Σ i

Proofs

The initial state satisfies invariant: inv -Σ i (σ i 0 ) is immediate Preservation of inv -Σ i by each operation:

∀ - σ i ∈ Σ i • post-start-Write i ( - σ i , v , σ i ) ⇒ σ i ∈ Σ i
First, start-Write cannot reduce dom data-w (so both fresh-w and hold -r will be in the domain of the resulting data-w ); furthermore hold -w is of type X and is clearly in

dom ( ---- data-w † {hold -w } → v ). ∀ - σ i ∈ Σ i • post-commit-Write i ( - σ i , σ i ) ⇒ σ i ∈ Σ i
is immediate because hold -w was already in dom data-w .

∀ - σ i ∈ Σ i • post-start-Read i ( - σ i , σ i ) ⇒ σ i ∈ Σ i
is immediate because fresh-w was already in dom data-w .

∀ - σ i ∈ Σ i • post-end -Read i ( - σ i , σ i ) ⇒ σ i ∈ Σ i is trivial since σ i = - σ i .

Respecting rely-conditions (by pairs of operations):

The obvious case is to show that rely-end -Read is OK: this follows immediately from guar -start-Write.

In fact, the more interesting case is rely-start-Write: (end -Read does not change any of the relevant variables, so) guar -start-Read has to imply rely-start-Write which is immediate from their texts and the fact that fresh-w cannot change during the execution of start-Write.

Reification:

This is a classic situation where the standard VDM "homomorphic" data reification rule does not suffice and Nipkow's version (cf. Section 1.1) is needed to show that the data absent in the representation was not actually essential in the specification. 8The key here is to show that any required Values are contained in the smaller data-w i ; this is done by checking that a mapping m exists between the available X indices and the N 1 indices to the full list in data-w a . So:

rel : Σ a × Σ i → B rel (mk -Σ a (d -w a , fr -w a , ho-r a ), mk -Σ i (d -w i , fr -w i , ho-r i , ho-w i )) ∃m ∈ (X m ←→ N 1 ) • d -w i ⊆ m • d -w a ∧ m(fr -w i ) = fr -w a ∧ m(ho-r i ) = ho-r a
The initial states relate:

rel (σ a 0 , σ i 0 ) is immediate with m = {α → 1}
It is then necessary to show that each pair of operations preserve this relation. It is often a disadvantage of "Nipkow's rule" that it requires an existential proof; in general, such existence proofs can be troublesome but in this case the Σ a operations are simple enough (two are deterministic) that it is easy to spot the witness for σ a 2 .

The pair of start-Write operations preserve the relation:

The only one where the existence of the new mapping m requires work is:

rel (σ a 1 , σ i 1 ) ∧ post-start-Write i (σ i 1 , v , σ i 2 ) ⇒ ∃σ a 2 ∈ Σ a • post-start-Write a (σ a 1 , v , σ a 2 ) ∧ rel (σ a 2 , σ i 2 ) From rel (σ a 1 , σ i 1 ) we have: ∃m 1 ∈ (X m ←→ N 1 ) • d -w i 1 ⊆ m 1 • d -w a 1 ∧ m 1 (fr -w i 1 ) = fr -w a 1 ∧ m 1 (ho-r i 1 ) = ho-r a 1 Then (as mentioned) post-start-Write a (σ a 1 , v , σ a 2 ) determines σ a 2 to have: data-w a 2 = data-w a 1 [v ]
Then rel (σ a 2 , σ i 2 ) follows from: m 2 = m 1 † {ho-w i → len data-w a 2 } because the type of ho-w ∈ X gives the first property; the pairing ho-w → len data-w a 2 ensures d -w i 2 ⊆ m 2 • d -w a 2 ; and ho-w i 2 / ∈ {fr -w i 1 , ho-r i 1 } (from post-start-Write i ) shows the last two requirements on m are satisfied.

The pair of commit-Write operations preserve the relation:

rel (σ a 1 , σ i 1 ) ∧ post-commit-Write i (σ i 1 , σ i 2 ) ⇒ ∃σ a 2 ∈ Σ a • post-commit-Write a (σ a 1 , σ a 2 ) ∧ rel (σ a 2 , σ i 2 )
Here, m 2 = m 1 .

The pair of start-Read operations preserve the relation:

rel (σ a 1 , σ i 1 ) ∧ post-start-Read i (σ i 1 , σ i 2 ) ⇒ ∃σ a 2 ∈ Σ a • post-start-Read a (σ a 1 , σ a 2 ) ∧ rel (σ a 2 , σ i
2 ) is immediate with m 2 = m 1 and the post-conditions both copying fresh-w into hold -r .

The pair of end -Read operations preserve the relation:

rel (σ a 1 , σ i 1 ) ∧ post-end -Read i (σ i 1 , σ i 2 , v ) ⇒ ∃σ a 2 ∈ Σ a • post-end -Read a (σ a 1 , σ a 2 , v ) ∧ rel (σ a 2 , σ i
2 ) again is immediate with m 2 = m 1 ; in fact, the only interest here is to see that the result v is the same in each case.

Taking stock again

This section has made progress in that the specification in Figure 7 offers a way to retain only a small number of Values in data-w i ; but in resolving the atomicity of data-w , we have actually introduced new atomicity problems! Recall that in Section 2 it was made clear that -in the final implementation-atomicity is only to be assumed at the level of single bit operations (not even a pair of bits can be accessed and changed atomically).

To be precise, the only requirement taken forward is that card X ≥ 3 -but Section 4 shows that Simpson needs four slots precisely to facilitate communication. We need a way of communicating hold -r without assuming that we can assign values of type X atomically otherwise we might have a problem as big as the initial transfer of Values. Again, choosing the right representation is the key to achieving the guarantee conditions.

The four-slot representation

Section 3 reduces the number of Values that have to be retained. More importantly, it reduces the atomicity requirements providing the fields of data-w can be separately accessible. This leaves the issue of atomic operations on the shared variables fresh-w and hold -r (hold -w is not shared). Essentially, this section shows how to encode the "ownership" from the Σ i level without atomicity assumptions on hold -r and fresh-w . There is, in fact, a clue to how this can be done in that so far we have only established the need for three distinct places in data-w -maybe a couple of bits suffice. But it is part of the atomicity objective of the whole design process that one cannot even "lock" two bits: even this could delay the sibling process.

Simpson's contribution is not, in fact, realising a minimal number of slots but in finding a way to communicate between Read and Write assuming only single bit operations avoid corruption.

The code

The state of the implementation can be defined as in Figure 8. Although they play no real part in this development, Simpson's terms "pair" and "slot" are used here. This final state introduces local variables for slot and pair information: in the Write process these are wp-w and ws-w ; in Read , pair -r and rs-r . All but pair -r are strictly local (not even visible to the other process).9 Notice that viewing pair/slot as the model of X gives card X = 4. (Also, anywhere in the proofs, we can use, for a field any of type P or S , card ãny ≤ 2.)

The code for Simpson's algorithm is given in Figure 9. For convenience of comparison with earlier papers [START_REF] Simpson | New algorithms for asynchronous communication[END_REF][START_REF] Henderson | Formal Modelling and Analysis of an Asynchronous Communication Mechanism[END_REF], comments are added to the code.

Two pairs of statements (in commit-Write and start-Read ) are marked as being executed atomically for now: this requirement is lifted in Section 4.3. The reason for the temporary assumption is that -in Figure 7the behaviour of fresh-w i is clearly atomic whereas its representation here as a P /S pair could introduce new behaviours. As becomes clear below, these are avoided by a standard concurrent programming technique. : S inv (mk -Σ r (data-w , pair -w , pair -r , slot-w , wp-w , ws-w , rs-r ))

card dom data-w = 4 ∧ card dom slot-w = 2 init let data-w = {(p 0 , s 0 ) → x, (p 0 , s 1 ) → nil, (p 1 , s 0 ) → nil, (p 1 , s 1 ) → nil} pair -w = p 0 pair -r = p 0 slot-w = {p 0 → s 0 , p 1 → s 0 } wp-w = p 0 ws-w = s 0 rs-r = s 0 in mk -Σ r (data-w , pair -w , pair -r , slot-w , wp-w , ws-w , rs-r )
Where (card P = card S = 2): Code (with atomicity) satisfies specs of Section 3.2 10 There is a small issue here which different authors circumvent in various ways: several authors put the initial x value in all four slots; we prefer to view data-w i = data-w r -£ {nil}.

P , S = token-set
Preservation of inv -Σ r : With the interpretation:

fresh-w = (pair -w , slot-w (pair -w )) hold -r = (pair -r , rs-r ) hold -w = (wp-w , ws-w )

Re post-start-Write There are essentially three clauses: 1) hold -w = fresh-w even if pair -r = pair -w , ws-w = ρ(slot-w (pair -w )) ensures (wp-w , ws-w ) = (pair -w , slot-w (pair -w )) note that all variables with names α-w cannot change by interference.

2) hold -w = hold -r Since wp-w = ρ(pair -r ), it follows that (wp-w , ws-w ) = (pair -r , rs-r ) 3) Finally,

data-w = ---- data-w † {hold -w → v } is immediate.
Re guar -start-Write The code only changes data-w (hold -w ) rely-start-Write gives ḣold -r = { --hold -r , fresh-w } by the same argument as above, hold -w / ∈ { --hold -r , fresh-w } Re post-commit-Write hold -w = (wp-w , ws-w ) and fresh-w = (pair -w , slot-w (pair -w )) so the result is immediate (but splitting the atoms is discussed in Section 4.3).

Re post-start-Read fresh-w = (pair -w , slot-w (pair -w )) and hold -r = (pair -r , rs-r ) give the exact result (but again splitting the atoms has to be discussed in Section 4.3).

Re guar -start-Read is essentially the same argument.

Re post-end -Read follows immediately from hold -r = (pair -r , rs-r )

Final atomicity refinement

The code in Figure 9 has atomic brackets around two pairs of statements: as far as start-Read is concerned, while these pairs of statements are linked, there are only two possible behaviours: either hold -r = ---fresh-w or hold -r = fresh-w . Allowing the steps of the atomic statements in commit-Write and start-Read to interleave admits no new behaviours. But it is crucial that the slot-w and pair -r are set (read) in commit-Write (start-Read ) in the reverse order: this gives the impression of "atomicity". This is, of course, a standard technique from database locking [WV01, §4] (for an attempt to link views of different communities about "atomicity", see [START_REF] Jones | The atomic manifesto[END_REF]).

Many authors choose to present the code of Figure 9 above with an additional variable wp-r and write start-Read is to write rp-r ← pair -w ; pair -r ← rp-r instead of pair -r ← pair -w ; This is not done here since we do not assume assignment statements are executed atomically. But, if they did execute atomically, the use of the extra wp-r admits more behaviours. This observation just goes to emphasise the extreme interference/interleaving being considered in ACM implementation.

It is worth emphasising that the residual assumptions on "atomicity" are only at the bit level: any assignment has only one shared variable and affects only a single bit. For a discussion of "meta-stability" at the bit level, see [START_REF] Paynter | Ramifications of meta-stability in bit variables explored via Simpson's 4-slot mechanism[END_REF].

Generality of the techniques

This section pulls out the ideas which -in various subsets/combinations-should be useful in other developments.

In the ACM example, the ideal of the "fiction of atomicity" would be to abstract from all of the details by using a single atomically accessed variable as an abstraction but this does not describe all of the possible behaviours and one has to think harder to obtain a starting specification. The choice here is to make a minimal split of the two parallel processes each into two sub-operations whose behaviour is composed sequentially ("by semicolon"). This "phasing" is of course algorithmic detail in a specification but is claimed to offer a reasonably intuitive description of the permissable behaviours of an ACM. The general suggestion of tasteful use of algorithmic operators in specifications is a useful message.

The same phasing idea pays off handsomely when the move is made to specifications with rely and guarantee conditions: if the same essential properties were to be presented for the whole of say Write in the ACM example, there would have to be ghost variables to track the phase and implications to present the information about the separate phases as a single predicate. The current authors believe that phasing is a useful specification idea that is explored further in the second author's PhD thesis [START_REF] Pierce | Enhancing the Useability of Rely-Guaranteee Conditions for Atomicity Refinement[END_REF].

In Section 2, the rely and guarantee conditions themselves are fairly standard. Checking that they are consistent between the two parallel threads is made almost trivial by judicious choice of frame markings. Such frame markings are another useful technique familiar from writings on VDM but with additional payoff in concurrency.

The notation for "possible values" is new in this paper and warrants further exploration and exploitation. This links with how mutual exclusion is handled in Section 3 at the abstract level (Σ i ); this is in contrast to the auxiliary variable argument in [START_REF] Pierce | Enhancing the Useability of Rely-Guaranteee Conditions for Atomicity Refinement[END_REF]. This issue is discussed further in [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF].

The justification of the data reification from Σ a to Σ i cannot be done using the simpler of the two rules in the VDM literature but the rule from Nipkow's thesis covers the (possible) reduction in the size of the state space and this rule is included in VDM: e.g. [Jon90, §9.3]. The use in Section 3 is technically interesting; in fact, its availability makes possible the choice of development from Σ a to Σ r via Σ i . Such careful choice of design strategy is essential but is perhaps the hardest of the techniques to reduce to general rules.

Another key point only sees its completion in Section 4 and that is the use even at this step of rather bold atomicity assumptions. Without Simpson's clever data representation it might be impossible to achieve atomic update (on a reasonable machine architecture) without locking and it is made clear in Section 2 that this is not allowed in ACMs. Such roadblocks (leading to backtracking) cannot be ruled out by any method whether formal or informal. The general observation that data reification has a key role to play in "atomicity refinement" is made in Section 1.3.

There is a danger when presenting such a development that a reader will conclude that a claim is being made that the "method" can never lead down false paths. This is certainly not the claim of the current authors. For example, without the clever choice of data representation, the guarantee conditions on Σ i cannot be met within the atomicity assumptions. What is claimed here is (only) that the design decisions can be seen more clearly in a reification process than by staring at the final code.

Discussion

This section offers brief descriptions of some other recent justifications of Simpson's algorithm. In making such comparisons, the current authors are not trying to be competitive but to use this intricate algorithm to indicate what insight can be given by various approaches. No attempt is made here to trace the full history of the algorithm that we -in common with most authors-have referred to as "Simpson's algorithm". The interested reader could start at [START_REF] Gary | Concurrent reading while writing[END_REF][START_REF] Gary | A new solution to lamport's concurrent programming problem using small shared variables[END_REF] and certainly read some of Leslie Lamport's many contributions such as [START_REF] Lamport | The mutual exclusion problem: part i-a theory of interprocess communication[END_REF].

Henderson's development

Henderson's research (in particular, his thesis [Hen04]11 ) has been a key information source. Interestingly, he uses broadly the same set of technical tools as in the current paper. In spite of this, the presentation here looks very different.

First, Henderson's specification attempts to retain a minimal list of Values that could potentially be returned by a Read . A cost for this is a pair of "ghost variables" that inform the Read operation in which phase the Write operation is executing (and vice versa). These variables can be eliminated in reification because Henderson also uses "Nipkow's rule". The current authors hold the (biased) view that the specification here is clearer but there would be little difficulty in proving they describe the same behaviour and the choice can be left to the "customer".

A more pervasive difference results in part from the recent development (cf. [START_REF] Jones | Splitting atoms safely[END_REF]) of the link between atomicity refinement and data reification. In Section 4 of the current paper, the preceding interference specifications are achieved by capitalising on Simpson's four-slot representation.

Event decomposition

Jean-Raymond Abrial's extension of his "B" approach [START_REF] Pierce | The B-Book: Assigning programs to meanings[END_REF] to "Event-B" is described in [START_REF] Abrial | Formal construction of a non-blocking concurrent queue algorithm[END_REF]. Guarded events are assumed to be executed atomically; selection as to which event can be executed is non-deterministic if multiple guards evaluate to true. As such, this approach is completely different from that of rely/guarantee thinking. The approach in [START_REF] Abrial | Formal construction of a non-blocking concurrent queue algorithm[END_REF] to increasing concurrency (or "splitting atoms") is to decompose events. When one "splits" an event into sub-events it has to be shown that all but one "refines skip". There are a number of elegant examples of the use of this approach.

Abrial and Cansell have also tackled the "4-slot" implementation of ACMs and have been kind enough to let us see their development as supported by the RODIN tools [START_REF] Rodin | Rodin tools can be downloaded from SourceForge[END_REF]. They start from a specification in terms of the traces of reading and writing. It is inherent in the ACM problem -rather than a criticism of their specification-that pinning down the exact behaviour is somewhat messy: in essence, they have to reflect the points at which operations start and end. It would be possible to relate the initial specification in Section 2.3 to their specification and prove that the same invariants are satisfied. This then leaves the user to decide which is the most intuitive way of understanding ACM behaviour.

The "event decomposition" method is extremely interesting: Abrial and Cansell avoid the need for rely and guarantee conditions by preserving the atomicity of events at any level of development. This achieves a considerable economy of rules. The use of pseudo instruction counters is vividly illustrated in Abrial's event refinement approach. In those situations where the correctness depends on a constrained order, since the order of execution of the events with true guards in a given set is non-deterministic, pseudo instruction counters are tested in guards and set in the corresponding events. 12The current authors do also wonder whether the interesting development of Simpson's algorithm in [START_REF] Abrial | Development of a concurrent program[END_REF] indicates that the atomicity constraint might require a series of difficult-to-invent steps. But their forthcoming publication will admit wider comparison (and by people unbiased by being authors of either approach).

Comparison with "Separation Logic"

Another exciting avenue in research on concurrent code has been the recent developments around "concurrent separation logic" [Rey02, O'H07, Bro07, OYR09, PB05]. At this time, researchers in Newcastle, London and Cambridge are discussing ways of combining the best features of both separation logic and rely/guarantee reasoning. For example, the second author's thesis builds the bridge with the read/write frames here. There is not space here to do this research full justice; but an excellent recent reference (from which other citations can be found) is [START_REF] Vafeiadis | Modular fine-grained concurrency verification[END_REF].

During the writing of this paper, Richard Bornat sent us his current work on Simpson's algorithm using separation logic. The title of [START_REF] Bornat | Inter-process buffers in separation logic with rely-guarantee[END_REF] alone should indicate why this is exciting. Again, the availability of this in published form will admit proper unbiased comparison. There is a sense in which the dynamic ownership (by the two processes) of the indices of data-w i ought be made for reasoning with concurrent separation logic. As far as the current authors can determine, no paper has fully exploited this observation. In contrast, the approach here is to show this as a representation of a carefully thought out abstraction. This distinction goes to the heart of John Reynold's comment at MFPS (Birmingham, OK, 2005) that "separation logic lets one show avoidance of races and rely/guarantee facilitates reasoning about races" (this is only an approximate quote -sadly, John has not put it in a published paper). This aspect is the subject of on-going discussions between the first author and Matt Parkinson.

Model checking

Between the initial submission to this journal and the final revision of the paper, its first author has discussed the specific application with Bill Roscoe. His [START_REF] Roscoe | Understanding Concurrent Systems[END_REF] and the earlier [START_REF] Rushby | Model checking Simpson's four-slot fully asynchronous communication mechanism[END_REF] certainly provide insight into aspects of Simpson's algorithm. In particular, the conditions under which one can even relax the atomicity constraints on the control bits are interesting. Although the current authors prefer a developmental presentation, it is clear that:

• this algorithm uses (basically) finite data structures and lends itself to model checking • model checking is a good tool to investigate code • this is another example of diverse formal approaches providing different insight

Our own path

The current paper is an extensive revision of [START_REF] Jones | Splitting atoms with rely/guarantee conditions coupled with data reification[END_REF]. Already in that paper the role of the intermediate abstraction (Σ i ) is clear. There was however an error in the description at that level of abstraction that is corrected here by the use of the new notation for "possible values".

More importantly, the step from Σ i to Σ r is completely different here making much more use of the results at the Σ i level than in [START_REF] Jones | Splitting atoms with rely/guarantee conditions coupled with data reification[END_REF]. The second author's thesis [START_REF] Pierce | Enhancing the Useability of Rely-Guaranteee Conditions for Atomicity Refinement[END_REF] illustrates an approach to showing mutual exclusion on data-w r using auxiliary variables. The difference between Pierce's solo argument and that here reflects Jones' strong preference for arguing via abstraction rather than backwards from code.

Another interesting insight into the evolution of Jones' thinking is that the paper [START_REF] Jones | The role of auxiliary variables in the formal development of concurrent programs[END_REF] was written between [START_REF] Jones | Splitting atoms with rely/guarantee conditions coupled with data reification[END_REF] and the current paper.

Conclusions

As made clear at the outset, ACMs are complex; Simpson's algorithm is ingenious; and its correctness requires delicate reasoning. The development in Figures 5, 7 and 9 is key to providing an intuitive grasp of the correctness. The authors hope that the reader finds this a clear design rationale. (The material in Figures 1 and6 is really there to provide intuition about the behaviour.)

The intention, however, was not just to add yet another correctness argument of one specific algorithm but instead to use this example to illustrate how a number of ideas can be used in concert to move from a "fiction of atomicity" using a development approach that can be called "splitting (software) atoms safely". The notes in Section 5 can be summarised as:

• The authors present an understandable and tractable reworking of the "4-slot" algorithm, with a clear design history. • The "fiction of atomicity" is a good place to begin.

• Rely/guarantee reasoning is greatly simplified by the use of frames and phasing arguments.

• While rely/guarantee conditions allow us to reason about the interference, a clever data reification is required (which Simpson gives us).

Fig. 4 .

 4 Fig. 4. Non-deterministic case

Fig. 5 .

 5 Fig. 5. Specification of sub-operations on Σ a with rely/guarantee

Fig. 6 .

 6 Fig. 6. Intermediate pseudo-code

Σ

  r :: data-w : P × S m -→ [Value] pair -w : P pair -r : P slot-w : P m -→ S wp-w : P ws-w : S rs-r

Fig. 8 .Fig. 9 .

 89 Fig. 8. The final state: Σ r

February 2010. Version C

See an on-line attempt to keep track of the literature at: http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/rg-hist.pdf

Notice that this shows that a "circular buffer" is not a model of the required behaviour.

Remember that types in VDM are restricted by invariants; so, for example, quantifying over Σ a only considers records that satisfy its invariant.

As an aside: It would be reasonable to assume that a Read operation will run in less time than a Write -in this case it would be impossible for multiple Writes to complete within the time of a Read -such an assumption can slightly simplify solutions. This assumption is not made here (nor in most other papers).

Note that no adequacy proof is required.

This fits with the locality of hold-w in Σ a .

The reader is also referred to[START_REF] Henderson | The formal classification and verification of Simpson's 4-slot asynchronous communication mechanism[END_REF] and[START_REF] Paynter | Ramifications of meta-stability in bit variables explored via Simpson's 4-slot mechanism[END_REF]; the second of these addresses the delicate issue of "meta-stability" of the control bits.

This is reminiscent of the proof of the Boehm/Jacopini theorem that "goto" statements can be avoided.

Acknowledgements

The authors are grateful to Jean-Raymond Abrial and Dominique Cansell for sharing their ongoing work in this area. Similarly, the preview of the paper by Richard Bornat and Hasan Amjad is gratefully acknowledged. Thanks also go to Peter O'Hearn, Hongseok Yang, Viktor Vafeiadis, Mike Dodds and Matt Parkinson for general and ongoing discussions on development methods for concurrency. These exchanges have been amplified by the London concurrency meeting in January 2009, its Northern edition in the same format in November 2009 and are to be continued in Cambridge.

The authors are grateful for the reviewers comments obtained anonymously by the journal. Of course, our original inspiration of the specific algorithm comes from Hugo Simpson. Neil Henderson and Steve Paynter made us aware of the challenge of this tiny but intriguing problem.

Our research is supported by the EPSRC Platform Grant on "Trustworthy Ambient Systems" and the EU FP7 "DEPLOY project".