This is a preprint of a paper that will appear in the Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004), Chennai, India, December 16, 2004 \begin{matrix}c \\ ◯ \end{matrix}Springer-Verlag.

Toward a Grainless Semantics for Shared-Variable Concurrency ^{⋆}

John C. Reynolds

Carnegie Mellon University and Edinburgh University

                   john.reynolds@cs.cmu.edu

Abstract. Conventional semantics for shared-variable concurrency suffers from the “grain of time” problem, i.e., the necessity of specifying a default level of atomicity. We propose a semantics that avoids any such choice by regarding all interference that is not controlled by explicit critical regions as catastrophic. It is based on three principles:

– Operations have duration and can overlap one another during execution.

– If two overlapping operations touch the same location, the meaning of the program execution is “wrong”.

– If, from a given starting state, execution of a program can give “wrong”, then no other possibilities need be considered.

1 Introduction

Ever since the early 1970’s, when researchers began to propose programming languages in which concurrent processes interact via shared variables, the problem of default atomicity, which Dijkstra called the “grain of time” phenomenon, has plagued the design and definition of such languages. Basically, if two concurrent processes access the same variable, without any explicit description of atomicity or mutual exclusion, the variety of outcomes will depend on a default choice of the level of atomicity, increasing as the atomicity becomes more fine-grained.

For example, consider the concurrent execution of two assignments to the same variable:

x := x × x ∥ x := x + 1 .

1. If each of these assignment commands is an atomic action, then there are two possible interleavings of the actions, which lead to two distinct possible outcomes.

⋆ Research was partially supported by National Science Foundation Grant CCR-0204242, by an EPSRC Visiting Fellowship at Edinburgh University, and by the Basic Research in Computer Science (http://www.brics.dk/) Centre of the Danish National Research Foundation. A more preliminary version of this material was presented at POPL 2004 [1].

2. If the evaluation of expressions and the storing of a value in a variable are atomic, then there are more interleavings and more possible outcomes.

3. If each load and store of a variable is atomic, there are still more interleavings and outcomes.

4. In the extreme case, say if x is a double-precision floating-point number, the atomic actions might be loads and stores of parts of the number representation, so that the possible outcomes would depend upon details of the machine representation of numbers.

In practice, at most the first of these interpretations would be useful to a programmer, while efficient implementation would be possible only at levels 3 or 4, where hardware-implemented mutual exclusion of memory references would suffice to guarantee atomicity.

The fact that there is no default level of atomicity that is natural for both user and implementor led researchers such as Hoare [2] and Brinch-Hansen [3] to propose that interfering concurrent commands such as x := x × x ∥ x := x + 1 should be prohibited syntactically, so that, whenever interference is possible, the programmer must indicate atomicity explicitly by means of critical regions, e.g.,

with lock do x := x × x ∥ with lock do x := x + 1 .

Unfortunately, this proposal floundered when applied to languages that permit a flexible usage of pointers (which is why, for instance, the approach was not followed in ADA, even though it was mandated in the early requirements specifications of that language). For example, consider the concurrent composition of two indirect assignments:

[x] := [x] × [x] ∥ [y] := [y] + 1

(where [x] denotes the contents of the pointer that is the value of x). This command should be prohibited just when x = y — but in general this kind of condition cannot be determined by a compiler.

Our answer to this dilemma is that, when x = y, the semantics of the above program is simply “wrong”. To provide any further information would make no sense at any level of abstraction above the machine-language implementation, and would unnecessarily restrict the ways in which the program could be implemented.

More precisely, we propose a compositional semantics of shared-variable concurrency that avoids the “grain of time” phenomenon by employing three principles:

– All operations, except locking and unlocking, have duration, and can overlap one another during execution.

– If two overlapping operations lookup or set the same location, which may be either a variable or a pointer, then the meaning of program execution is wrong.

– If, from a given starting state, execution of a program can give wrong, then no other possibilities need be considered.

It must be emphasized that there is no intention of implementing wrong as a run-time error stop, which would be extremely inefficient and, in view of the nondeterminacy of concurrent computation, of little use. Instead, when the semantics of a program execution is wrong, there are no constraints on how it may be implemented.

Thus it is the programmer’s obligation to make a convincing argument that his program will not go wrong. We can define what that means, and we should be able to provide a logic in which such arguments can be made rigorous. But the development of programming languages over the past thirty years makes it clear that this concept of wrongness cannot be decided automatically without restricting the programming language in ways that are unacceptable for many applications.

Our hope of providing an appropriate logic lies in the development of separation logic [4], and, more particularly, in its extension to shared-variable concurrency [5]. The soundness of this extension is very delicate, however, and thus must be demonstrated rigorously with respect to a compelling semantics of the concurrent programming language. Although we will not discuss separation logic further in this paper, we believe that the work described herein can provide such a semantics.

Recently, Steve Brookes proposed a novel semantics for shared-variable concurrency and used it to establish the soundness of separation logic [6]. There are considerable similarities between this work and ours: The starting point of both is a form of transition-trace semantics developed earlier by Brookes [7] (and based on still earlier ideas of Park [8]), in which traces are sequences of startfinish pairs of states. In Brookes’s current semantics, these pairs are replaced by “actions”, the actions of concurrent processes are interleaved, and uncontrolled interference is mirrored by interference between adjacent actions.

In contrast, our semantics captures duration directly by regarding start and finish as separate actions, between which the actions of other processes may intervene. (Although these two approaches are conceptually quite distinct, each has had significant influence on the other.)

2 Some Examples

The meaning of a command is a set of traces, each of which is a finite or infinite sequence of actions. Except for critical regions, the relevant actions are states labelled “start” or “fin”.

For example, the meaning of the operation x:=x×x, which we write [[x:=x×x]] is the set of traces of the form

start[ x: n] fin[ x: n × n] ,

for all integers n. Notice that the states in the start and finish actions have the same domain, which is the footprint of the operation, i.e., the exact set of locations that are examined or set by the operation.

If x := x × x runs by itself, without other processes running concurrently, its behavior is determined by executing the traces in its meaning. For example, starting in the state [ x: 3 | t: 22 ], the trace start[ x: 3 ] fin[ x: 9 ] has the execution

[ x: 3 | t: 22 ]

↓  start[ x: 3 ]

[ t: 22 ]

↓  fin[ x: 9 ]

[ x: 9 | t: 22 ] .

In essence, the effect of the start action is to check that x = 3 and then mark x “busy” by removing [ x: 3 ] from the current state. Then the effect of the finish action is to return x to the current state with a new value.

On the other hand, when started in a state with a different value of x, the trace start[ x: 3 ] fin[ x: 9 ] is irrelevant and has no execution. But an execution will be provided by another trace, such as start[ x: 4 ] fin[ x: 16 ], in [[x := x × x]].

A third possibility arises when x does not occur in the domain of the starting state. In this case the execution goes wrong:

[ t: 22 ]

↓ start[ x: 3 ]

wrong .

When a command assigns indirectly to a pointer, its footprint is more complex. For example, the meaning [[[x] := [x] × [x]]] is the set of traces

start[ x: n_{1} | n_{1}: n_{2} ] fin[ x: n_{1} | n_{1}: n_{2} × n_{2} ] ,

for all integers n_{1} and n_{2}. Here the footprint contains both x and its value n_{1}, which is a pointer. (We regard pointers as integers, in order to permit unrestricted pointer arithmetic.) Similarly, the meaning [[[y] := [y] + 1]] is the set of traces

start[ y: n_{3} | n_{3}: n_{4} ] fin[ y: n_{3} | n_{3}: n_{4} + 1 ] ,

for all integers n_{3} and n_{4}.

Now consider the concurrent execution of these two indirect assignments. The meaning

[[[x] := [x] × [x] ∥ [y] := [y] + 1]]

is the set of interleavings of the traces of each subcommand. This set includes traces of the form

start[ x: n_{1} | n_{1}: n_{2} ] start[ y: n_{3} | n_{3}: n_{4} ]
fin[ y: n_{3} | n_{3}: n_{4} + 1 ] fin[ x: n_{1} | n_{1}: n_{2} × n_{2} ] ,

in which the two assignment operations overlap.

When n_{1} ≠ n_{3}, such a trace executes without interference:

[ x: n_{1} | n_{1}: n_{2} | y: n_{3} | n_{3}: n_{4} ]

↓ start[ x: n_{1} | n_{1}: n_{2} ]

[ y: n_{3} | n_{3}: n_{4} ]

↓ start[ y: n_{3} | n_{3}: n_{4} ]

[ ]

↓ fin[ y: n_{3} | n_{3}: n_{4} + 1 ]

[ y: n_{3} | n_{3}: n_{4} + 1 ]

↓ fin[ x: n_{1} | n_{1}: n_{2} × n_{2} ]

[ y: n_{3} | n_{3}: n_{4} + 1 | x: n_{1} | n_{1}: n_{2} × n_{2} ] .

On the other hand, when n_{1} = n_{3} and n_{2} = n_{4}, the two assignments interfere:

[ x: n_{1} | n_{1}: n_{2} | y: n_{1} ]
↓  start[ x: n_{1} | n_{1}: n_{2} ]
[ y: n_{1} ]
↓  start[ y: n_{1} | n_{1}: n_{2} ]
wrong .

Our treatment of critical regions follows the recent work of Brookes [6]. Three actions are involved, each of which names a lock or semaphore:

try(k) : Try to acquire k, but find it is already locked.
acq(k) : Succeed in acquiring k, and lock it.
rel(k) : Unlock k (or signal “impossible” if it is already unlocked).

For example, the meaning of the critical region with k do x := x × x is the set of traces (for all integers n):

acq(k) start[ x: n] fin[ x: n × n] rel(k),

try(k) acq(k) start[ x: n] fin[ x: n × n] rel(k),

try(k) try(k) acq(k) start[ x: n] fin[ x: n × n] rel(k),

⋮

try(k) try(k) try(k) · · · .

To execute these new actions, we augment the current state of the computation with a set κ of “closed” locks. When k ∉ κ (and n is 3), a trace of the first form has an execution:

κ, [ x: 3 | t: 22 ]
↓  acq(k)
κ ∪ {k}, [ x: 3 | t: 22 ]
↓  start[ x: 3 ]
κ ∪ {k}, [ t: 22 ]
↓  fin[ x: 9 ]
κ ∪ {k}, [ x: 9 | t: 22 ]
↓  rel(k)
κ, [ x: 9 | t: 22 ] .

On the other hand, when k ^{∈} κ, the last trace has a nonterminating execution that represents deadlock:

κ, [ x: 3 | t: 22 ]
↓  try(k)
κ, [ x: 3 | t: 22 ]
↓  try(k)
⋮

The remaining traces in [[with k do x := x × x]] can only execute successfully after being interleaved with other traces that affect the same lock. For example, one possible interleaving of

try(k) try(k) acq(k) start[ x: 3 ] fin[ x: 9 ] rel(k)

with

acq(k) start[ x: 2 ] fin[ x: 3 ] rel(k)

(which is a trace in the meaning of with k do x := x + 1) is

acq(k) start[ x: 2 ] try(k) fin[ x: 3 ] try(k)

rel(k) acq(k) start[ x: 3 ] fin[ x: 9 ] rel(k) ,

which executes as follows when k ∉ κ:

κ, [ x: 2 ]
↓  acq(k)
κ ∪ {k}, [ x: 2 ]
↓  start[ x: 2 ]
κ ∪ {k}, [ ]
↓  try(k)
κ ∪ {k}, [ ]
↓  fin[ x: 3 ]
κ ∪ {k}, [ x: 3 ]
↓  try(k)
⋮

κ ∪ {k}, [ x: 3 ]
↓  rel(k)
κ, [ x: 3 ]
↓  acq(k)
κ ∪ {k}, [ x: 3 ]
↓  start[ x: 3 ]
κ ∪ {k}, [ ]
↓  fin[ x: 9 ]
κ ∪ {k}, [ x: 9 ]
↓  rel(k)
κ, [ x: 9 ] .

3 Syntax, States, and the Semantics of Expressions

The programing language we will use throughout this paper is an extension of the simple imperative language:

⟨exp⟩ ::= ⟨var⟩ | ⟨constant⟩ | ⟨exp⟩ + ⟨exp⟩ | ⋯
⟨boolexp⟩ ::= ⟨exp⟩ = ⟨exp⟩ | ⋯ | ⟨boolexp⟩ ∧ ⟨boolexp⟩ | ⋯
⟨comm⟩ ::= ⟨var⟩:= ⟨exp⟩ | skip | ⟨comm⟩; ⟨comm⟩
| if ⟨boolexp⟩ then ⟨comm⟩ else ⟨comm⟩
| while ⟨boolexp⟩ do ⟨comm⟩

with operations for looking up and mutating the contents of addresses:

⟨exp⟩ ::= [⟨exp⟩]
⟨comm⟩ ::= [⟨exp⟩] := ⟨exp⟩

concurrent composition:

⟨comm⟩ ::= ⟨comm⟩ ∥ ⟨comm⟩

and critical regions:

⟨comm⟩ ::= with ⟨lock⟩ do ⟨comm⟩ | with ⟨lock⟩ when ⟨boolexp⟩ do ⟨comm⟩

(In fact, the unconditional critical region with k do c can be regarded as an abbreviation for the conditional critical region with k when true do c. We treat it as a separate form for expository reasons.)

We assume that constants are integers, and that variables and locks are unstructured syntactic names (which are not integers). We also identify addresses with integers. Then we define a location to be either a variable or an address, and a state to be a mapping from a finite set of locations to integers:

Addresses = Integers
Locations = ⟨var⟩ ⊎ Addresses
States = ⋃{ δ → Integers | δ ⊆^{fin} Locations } .

We will use the following metavariables (with occasional decorations) to range over specific sets:

v : ⟨var⟩ (Variables)
e : ⟨exp⟩ (Expressions)
b : ⟨boolexp⟩ (Boolean Expressions)
c : ⟨comm⟩ (Commands)
n : Integers
t : Truth Values
ℓ : Locations

δ : Finite Sets of Locations
σ : States
k : ⟨lock⟩ (Locks)
κ : Finite Sets of Locks
τ : Traces
T : Sets of Traces
Φ : Configurations

(Traces and configurations will be defined later.)

We will also need some concepts and notations for states. We say that σ and σ′ are compatible, written σ ⌣ σ′, iff σ ∪ σ′ is a function, or equivalently, σ and σ′ agree on the intersection of their domains. We also write δ ⊥ δ′ when the sets δ and δ′ are disjoint, and σ ⊥ σ′ when dom σ ⊥ dom σ′.

When ℓ_{1}, …, ℓ_{m} are distinct, we write [ ℓ_{1}: n_{1} | … | ℓ_{m}: n_{m}] for the state with domain {ℓ_{1}, …, ℓ_{m}} that maps each ℓ_{i} into n_{i}. We also write [ σ | ℓ: n] for the state such that

dom[ σ | ℓ: n] = dom σ ∪ {ℓ}
[ σ | ℓ: n](ℓ) = n
[ σ | ℓ: n](ℓ′) = σ(ℓ′) when ℓ ≠ ℓ′ .

(Note that [ σ | ℓ: n] may either be an extension of σ or a possibly altered function with the same domain as σ.)

The meaning [[e]] of an expression (or boolean expression) e is a set of pairs ⟨σ, n⟩ in which n is the value obtained by evaluating e in any state that is an extension of σ, and in which the domain of σ is the footprint of the evaluation, i.e., the set of locations that are actually examined during the evaluation.

For example,

[[x − x]] = { ⟨[ x: m], 0⟩ | m ^{∈} Integers }
[[x + [y]]] = { ⟨[ x: m | y: n | n: n′], m + n′⟩ | m, n, m′ ^{∈} Integers } .

The relevant semantics equations are

[[⟨exp⟩]] ⊆ States × Integers
[[n]] = {⟨[ ], n⟩}
[[v]] = { ⟨[ v: n], n⟩ | n ^{∈} Integers }
[[e + e′]] = { ⟨σ ∪ σ′, n + n′⟩ | ⟨σ, n⟩ ^{∈} [[e]], ⟨σ′, n′⟩ ^{∈} [[e′]], and σ ⌣ σ′ }
[[[e]]] = { ⟨σ ∪ [ n: n′], n′⟩ | ⟨σ, n⟩ ^{∈} [[e]], n′ ^{∈} Integers, and σ ⌣ [ n: n′] }
[[⟨boolexp⟩]] ⊆ States × Bool
[[e = e′]] = { ⟨σ ∪ σ′, n = n′⟩ | ⟨σ, n⟩ ^{∈} [[e]], ⟨σ′, n′⟩ ^{∈} [[e′]], and σ ⌣ σ′ }
[[b ∧ b′]] = { ⟨σ, false⟩ | ⟨σ, false⟩ ^{∈} [[b]] }
∪ { ⟨σ ∪ σ′, t′⟩ | ⟨σ, true⟩ ^{∈} [[b]], ⟨σ′, t′⟩ ^{∈} [[b′]], and σ ⌣ σ′ } .

(Note that the final equation describes short-circuit evaluation of conjunction.)

Since expression evaluation in our programming language happens to be deterministic (though this is not required by the nature of our semantics), the meaning of an expression will be a function, but because its domain contains only states whose domains are footprints, this function will be a restriction of the meaning in a conventional denotational semantics.

Nevertheless, one can show an appropriate property of totality: For all e and σ, there are σ′ and n such that σ ⌣ σ′ and ⟨σ′, n⟩ ^{∈} [[e]]. A similar property holds for boolean expressions.

4 Traces and the Semantics of Commands

Actions can be defined grammatically:

⟨action⟩ ::= start(⟨state⟩) | fin(⟨state⟩) | try(⟨lock⟩) | acq(⟨lock⟩) | rel(⟨lock⟩)

Then a trace is a finite or infinite sequence of actions, or a finite sequence of actions followed by either wrong or ⊥.

We use “;” to denote the following concatenation of traces:

τ_{1} ; τ_{2} = \{ \begin{matrix}τ_{1} & if τ_{1} is infinite, or ends in wrong or ⊥, \\ τ_{1} τ_{2} & otherwise. \end{matrix}

Then we can define the concatenation and exponentiation of trace sets in a standard way:

\begin{aligned}T ; T′ & = & \{ τ ; τ′ | τ ^{∈} T, τ′ ^{∈} T′ \} \\ T^{0} & = & \{ϵ\} \\ T^{n+1} & = & T ; T^{n} \\ T^{∗} & = & ⋃_{n=0}^{∞} T^{n} \\ T^{ω} & = & \{ τ_{0} ; τ_{1} ; ⋯ | ∀i ≥ 0. τ_{i} ^{∈} T \} . \end{aligned}

We will also need the concept of a filter to describe the use of boolean expressions to determine control flow:

filter(⟨boolexp⟩) ⊆ Traces
filter(b) = { start(σ) fin(σ) | ⟨σ, true⟩ ^{∈} [[b]] } .

From the totality property of boolean expressions, one can obtain a totality condition for filters: For all b and σ, there is a σ′ such that σ ⌣ σ′ and

start(σ′) fin(σ′) ^{∈} filter(b) ∪ filter(¬ b) .

With these preliminaries, we can give semantic equations that determine the sets of traces that are meanings of sequential commands:

[[⟨comm⟩]] ⊆ Traces
[[v := e]] = { start(σ ∪ [ v: n_{old} ]) fin([ σ | v: n]) |
⟨σ, n⟩ ^{∈} [[e]], σ ⌣ [ v: n_{old} ] }
[[[e] := e′]] = { start(σ ∪ σ′ ∪ [ n: n_{old} ]) fin([ σ ∪ σ′ | n: n′]) |

⟨σ, n⟩ ^{∈} [[e]], ⟨σ′, n′⟩ ^{∈} [[e′]], σ ⌣ σ′, (σ ∪ σ′) ⌣ [ n: n_{old} ] }

[[skip]] = {start[ ] fin[ ]}
[[c_{1} ; c_{2}]] = [[c_{1}]] ; [[c_{2}]]
[[if b then c_{1} else c_{2}]] = (filter(b) ; [[c_{1}]]) ∪ (filter(¬ b) ; [[c_{2}]])
[[while b do c]] = ((filter(b) ; [[c]])^{∗} ; filter(¬ b)) ∪ (filter(b) ; [[c]])^{ω} .

For example

[[[x] := [y] + 1]] =

{ start[ x: m | m: m′ | y: n | n: n′] fin[ x: m | m: n′ + 1 | y: n | n: n′]
| m, m′, n, n′ ^{∈} Integers and m ≠ n }

∪ { start[ x: n | y: n | n: n′] fin[ x: n | y: n | n: n′ + 1 ] | n, n′ ^{∈} Integers } .

To define concurrent composition, we must first introduce the concept of a fair merge of the traces τ_{1} and τ_{2}, which is an merge (or interleaving) that contains every occurrence of actions in τ_{1} and τ_{2} (even when τ_{1} or τ_{2} is infinite).

To make this concept precise, we regard a trace as a function whose domain is the finite or infinite set of nonnegative numbers less than the length of the trace. Then τ is a fair merge of τ_{1} and τ_{2} iff there are functions ϕ_{1} and ϕ_{2} such that

dom ϕ_{1} = dom τ_{1} and dom ϕ_{2} = dom τ_{2}.

ϕ_{1} and ϕ_{2} are strictly monotone.

The ranges of ϕ_{1} and ϕ_{2} are a partition of dom τ.

For all i ^{∈} dom τ_{1}, τ_{1}(i) = τ(ϕ_{1}(i)).

For all i ^{∈} dom τ_{2}, τ_{2}(i) = τ(ϕ_{2}(i)).

Next, we define

τ_{1} ∥ τ_{2} = { truncate(τ) | τ is a fair merge of τ_{1} and τ_{2} } ,

where truncate is a function that captures the fact that wrong and ⊥ always terminate traces: When τ does not contain wrong or ⊥,

truncate(τ) = τ
truncate(τ wrong τ′) = τ wrong
truncate(τ ⊥ τ′) = τ ⊥ .

Finally, the meaning of the concurrent composition c_{1} ∥ c_{2} is the set of truncated fair merges of traces in the meaning of c_{1} with traces in the meaning of c_{2}:

[[c_{1} ∥ c_{2}]] = ⋃{ τ_{1} ∥ τ_{2} | τ_{1} ^{∈} [[c_{1}]], τ_{2} ^{∈} [[c_{2}]] } .

Our semantics of critical regions follows closely that of Brookes [6]:

[[with k do c]] = ({try(k)}^{∗} ; {acq(k)}; [[c]] ; {rel(k)}) ∪ {try(k)}^{ω}

[[with k when b do c]] =

(wait^{∗} ; {try(k)}^{∗} ; {acq(k)}; filter(b) ; [[c]] ; {rel(k)}) ∪ wait^{ω} ,

where

wait = ({try(k)}^{∗} ; {acq(k)}; filter(¬ b) ; {rel(k)}) ∪ {try(k)}^{ω} .

Notice that with k when b do c will fail to terminate if either it fails to ever acquire the lock k, or if it acquires k, but never when b is true.

There is a concept of totality that is appropriate to sets of traces: A set T of traces is said to be total whenever, if

τ start(σ_{0}) τ′ ^{∈} T ,

holds for some state σ_{0}, then for every state σ there is a trace

τ start(σ′) τ′′ ^{∈} T ,

such that σ ⌣ σ′.

There is also a somewhat analogous concept related to locks: A set T of traces is lock-total whenever, if

τ acq(k) τ′ ^{∈} T ,

then there is a trace

τ try(k) τ′′ ^{∈} T .

It can be shown that, for all commands c, [[c]] is total and lock-total.

5 Executing Traces

The execution of traces is described by a small-step operational semantics. A configuration Φ consists of a trace to be executed, coupled with the currently available state and a finite set of closed locks, or it is one of three special configurations that indicate abnormal termination or explicit nontermination:

Configurations =

Finite Sets of Locks × States × Traces ∪ {wrong, impossible, ⊥} .

A configuration is nonterminal if it contains a nonempty trace; otherwise it is terminal. (For readability, we omit empty traces from terminal configuations.)

Informally, the special terminal configurations have the following meanings:

– “wrong” indicates that a start operation has tried to access a location that is not in the domain of the currently available state.

– “impossible” indicates that a fin operation has tried to extend the current state at a location that is already in its domain, or that a rel has tried to open a lock that is not closed.

– ⊥ indicates that the trace will execute forever without performing further actions.

Transitions go from nonterminal configurations to configurations that are either nonterminal or terminal. They are described by the relation

→ ⊆ Nonterminal Configurations × Configurations that is the least relation satisfying:

κ, σ, start(σ′) τ → \{ \begin{matrix}κ, σ − σ′, τ & if σ′ ⊆ σ \\ wrong & if σ ⌣ σ′ and σ′ ⊈ σ \\ no transition & if σ ⌣̸ σ′ \end{matrix}

κ, σ, fin(σ′) τ → \{ \begin{matrix}κ, σ ∪ σ′, τ & if σ′ ⊥ σ \\ impossible & otherwise \end{matrix}

κ, σ, try(k) τ → \{ \begin{matrix}κ, σ, τ & if k ^{∈} κ \\ no transition & if k ∉ κ \end{matrix}

κ, σ, acq(k) τ → \{ \begin{matrix}κ ∪ \{k\}, σ, τ & if k ∉ κ \\ no transition & if k ^{∈} κ \end{matrix}

κ, σ, rel(k) τ → \{ \begin{matrix}κ − \{k\}, σ, τ & if k ^{∈} κ \\ impossible & if k ∉ κ \end{matrix}

κ, σ, wrong → wrong
κ, σ, ⊥ → ⊥ .

It is easy to see that → is a partial, but not total function.

A sequence of configurations that begins with the nonterminal Φ = κ, σ, τ, and in which each configuration is related to the next, is called an execution of τ in κ, σ. If there is such an execution that is finite and ends with Φ′, we write Φ →^{∗} Φ′; if there is such an execution that is infinite, we say that Φ diverges.

Since → is a partial function, if Φ diverges, then there is no terminal Φ′ such that Φ →^{∗} Φ′, while if Φ does not diverge, then there is at most one Φ′ such that Φ →^{∗} Φ′. In other words, the execution of a trace is always determinate.

On the other hand, since → is not a total function, there are nonterminal Φ = κ, σ, τ such that Φ does not diverge and there is no terminal Φ′ such that Φ →^{∗} Φ′. In this case, there is no execution of τ in κ, σ, and we say that τ is irrelevant to κ, σ.

Another property of trace execution stems from from the fact that in any trace of any command in our programming language, the actions acq and rel, and also start and fin, are balanced, in much the same sense as with parentheses. Specifically, in any prefix of any trace of any command, the number of occurrences of rel(k) for a particular lock k will never exceed the number of occurrences of acq(k) for the same lock, and the number of occurrences of fin(σ) for which a particular variable occurs in dom σ will never exceed the number of occurrences of start(σ′) for which the same variable occurs in dom σ′.

Because of this property (which might not hold for a lower-level programming language), one can show that the abnormal termination “impossible” never arises: For all commands c, traces τ ^{∈} [[c]], lock sets κ, and states σ:

κ, σ, τ ↛^{∗} impossible .

Finally, we define the execution of a set of traces T, in κ, σ:

Exec(κ, σ, T) = { ⟨κ′, σ′⟩ | ∃τ ^{∈} T. κ, σ, τ →^{∗} κ′, σ′ }
∪ if ∃τ ^{∈} T. κ, σ, τ →^{∗} wrong then Wrong else {}
∪ if ∃τ ^{∈} T. κ, σ, τ diverges then {⊥} else {} ,

where Wrong is the set of all terminal configurations, including “wrong”. Since

Wrong ∪ S = Wrong ,

for all sets S of terminal configurations, this captures the principle that Wrong overrides other possible outcomes. It also captures the notion that Wrong can be implemented arbitrarily.

In contrast to the execution of a particular trace, the execution of a trace set that is the meaning of a command can be nondeterminate. On the other hand, since command meanings are total and lock-total, Exec(κ, σ, [[c]]) contains at least one terminal configuration for every command c, state σ, and finite lock set κ.

6 Future Directions

Our trace semantics leads to a broader notion of observational equivalence than the conventional semantics of shared-variable concurrency. For example, in a conventional semantics the commands

x := x + 1 ; x := x + 2  and  x := x + 3

are distinguishable when run concurrently with, say, x:=1. But in our semantics, these commands are observationally equivalent: They would both go wrong if run concurrently with any command that assigns to or evaluates x; otherwise they would both increase x by three.

As suggested by this example, the broader notion of observational equivalence should provide greater scope for the development of code optimization. Unfortunately, however, our trace semantics is far from fully abstract; for example, the above commands denote distinct trace sets.

We intend to study equivalences on trace sets that at least approach observational equivalence. For example, we conjecture that every command without critical regions has a meaning that is equivalent to a set of traces whose members each have one of the forms:

start(σ) fin(σ′) where dom σ = dom σ′

start(σ) ⊥

start(σ) wrong .

I hope to report more on this topic in my talk.

We also hope to extend the programming language described by our semantics to include declarations of variables and locks. This should be a straightforward adaptation of the approach used by Brookes for transition traces [7]. It would also be useful to introduce operations for storage allocation and deallocation, perhaps similar to the cons and dispose operations of separation logic.

Another important direction would be permit passivity, i.e., to relax the assumption that overlapping operations on the same location go wrong, in order to allow the overlapping of read-only operations.

Finally, we hope to use our grainless semantics to model concurrent separation logic [5], and to relate the semantics to Brookes’s model [6].

Acknowledgement

The author wishes to thank Stephen D. Brookes for numerous helpful discussions.

References

1. Reynolds, J.C.: Towards a grainless semantics for shared variable concurrency (abstract only). In: Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, ACM Press (2004)

2. Hoare, C.A.R.: Towards a theory of parallel programming. In Hoare, C.A.R., Perrott, R.H., eds.: Operating Systems Techniques. Volume 9 of A.P.I.C. Studies in Data Processing, London, Academic Press (1972) 61–71

3. Brinch Hansen, P.: Structured multiprogramming. Communications of the ACM 15 (1972) 574–578

4. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, California, IEEE Computer Society (2002) 55–74

5. O’Hearn, P.W.: Resources, concurrency and local reasoning. In: CONCUR 2004 — Concurrency Theory, Proceedings of the 15th International Conference. Volume 3170 of Lecture Notes in Computer Science, Berlin, Springer-Verlag (2004) 49–67

6. Brookes, S.D.: A semantics for concurrent separation logic. In: CONCUR 2004 — Concurrency Theory, Proceedings of the 15th International Conference. Volume 3170 of Lecture Notes in Computer Science, Berlin, Springer-Verlag (2004) 16–34

7. Brookes, S.D.: Full abstraction for a shared-variable parallel language. Information and Computation 127 (1996) 145–163

8. Park, D.M.R.: On the semantics of fair parallelism. In Bjørner, D., ed.: Abstract Software Specifications. Volume 86 of Lecture Notes in Computer Science, Berlin, Springer-Verlag (1980) 504–526