

The purpose of this paper is to address some of the challenges of formally specifying components of shared-memory concurrent programs. The focus is to provide an abstract specification of a component that is suitable for use both by clients of the component and as a starting point for refinement to an implementation of the component. We present some approaches to devising specifications, investigating different forms suitable for different contexts. We examine handling atomicity of access to data structures, blocking operations and progress properties, and transactional operations that may fail and need to be retried.

Introduction
============

The objective of this paper is to address challenges to do with specifying concurrent program components in order to promote discussion about alternative approaches. Our main foci are atomicity, blocking operations and transactional operations in the context of rely/guarantee specifications @Jones83a [@Jones83b]. Our aim is to present the ideas rather than a fully formal development. Specifications play an important role in decoupling the use of a component from its detailed implementation. Often the role of specifications as a starting point for refinement to an implementation is emphasised but here we would like to balance that with their role of being used by other components. Hence we focus on a top-down approach to concurrent program specification, rather than a bottom-up approach.

#### Sequential programs.

For sequential programs conventional, Floyd/Hoare-style specifications @Floyd67 [@Hoare69a] in terms of *preconditions* and *postconditions* form the basis of component specifications, however, pre and post conditions alone are inadequate for specifying concurrent operations because they do not handle interference between the operations.

#### Shared variable concurrency.

First, to state the obvious, variables that are local to a thread are not subject to interference and hence can be treated in a manner similar to their use in a sequential program. For variables shared between parallel threads, interference becomes an issue. An important consideration is whether access (e.g. read or write) to variables is *atomic* or not. At the lowest level, atomicity is determined by the machine hardware and properties like its atomic access "word" size. A further complication at the hardware level is that, due to caches and write buffers, the order of write/read accesses to shared memory may not respect the sequential order of instruction execution. But perhaps we get a bit ahead of ourselves if we worry about these issues when considering specifications.

A thread that needs to perform multiple atomic accesses can be subject to *data races* where variables are updated in parallel by concurrent threads and the thread may see inconsistent data. At a more abstract level, operations may be required to be atomic with respect to a shared data structure. The implementation of such operations may require locks to ensure sequentialisation of access to the data structure or it may use more sophisticated non-blocking algorithms that achieve the effect of operation atomicity by utilising hardware-level atomicity @Scott13.

A concept commonly used to show an implementation is valid is *linearizability* @HW90, whereby parallel execution of a set of operations on a shared data structure is considered valid if it is equivalent to some linear (sequential) execution of the same operations (subject to certain requirements).

#### Verifying concurrent programs.

Early rules for reasoning about parallel programs by Hoare @Hoare75 utilised preconditions and postconditions but had strict disjointness requirements on program variables occurring in parallel threads, which effectively ruled out interference between parallel threads. The approach of Owicki and Gries @Owicki75 [@OwickiGries76; @OwickiGries-CACM-76] treats parallel components like sequential programs with intermediate assertions between each atomic step but then requires an extensive interference-freedom proof. Concurrent separation logic @BrookesSepLogic07 [@OHearn07] also leverages disjointness but does so in a more fine-grained and dynamic manner because it handles assertions over objects in the heap.

An early compositional approach to handle interleaved interference on shared variables was the rely/guarantee approach of Jones @Jones81d [@Jones83a; @Jones83b]. Jones extended pre/post specifications with a *rely* condition, a binary relation between program states expressing an assumption about the tolerable interference that any step of the environment of the thread can impose on the shared variables. To constrain the interference generated by a thread, Jones uses a *guarantee* condition, also a binary relation on states limiting the changes a program step of a thread can make to the shared variables. The guarantee is required to be reflexive (i.e. it contains the identity relation) so that the program may make stuttering steps that do not change the observable variables. The rely of each thread must be implied by the guarantees of all threads that run in parallel with it. The rely/guarantee approach does not dictate any particular granularity of atomicity, however, it does require all steps of a thread to satisfy its guarantee as long as all steps of the thread's environment satisfy its rely.

#### Blocking.

Operations may block waiting for "communication" from another thread. For example, an operation wanting to read a message from a communication channel may need to wait for a message to be written to the channel by another thread. Specifications of such operations need to be able to express such *waiting* criteria. This affects the termination behaviour of the operation. For example, if a message is never written to a channel, a read from the channel will never terminate (block forever). We consider two approaches to specifying such operations.

-   Using an explicit ${{\mathop{\mathbf{await}}}}$ construct that allows both nonterminating behaviour if the ${{\mathop{\mathbf{await}}}}$ blocks forever and terminating behaviour if it becomes unblocked.

-   An implicit approach that specifies under what conditions an operation is guaranteed to terminate as well as its behaviour when it does terminate, e.g. a read on a message channel is guaranteed to terminate if the channel is non-empty.

These forms can give equivalent specifications, for which the explicit form may be more useful for refining the operation, while the implicit form makes it easier to reason about using the operation. Another source of blocking is at the implementation level where atomicity constraints on operations may lead to the use of locks that lead to an implementation blocking awaiting a lock.

#### Transactional operations.

Utilising locks can generate bottlenecks because operations requiring the locks are sequentialised, and on multi-processor architectures they also generate more costly memory synchronisation primitives. One approach to avoiding (or minimising) locks is to implement operations that do most of their work locally and then perform a final atomic commit step that may fail if another operation has committed while the first operation was executing based on the old data @Scott13. Such implementations may suffer from starvation where they can repeatedly try and fail, potentially forever if there is continual interference from competing parallel operations. Note that in these situations, one of the competing threads may succeed but an individual thread may be pre-empted every time and never succeed. Fair scheduling is assumed, i.e. every thread is executed eventually, but that does not prevent an operation that a thread is attempting to execute from failing due to interference and needing to be retried.

Specifying such operations has to allow for the case in which an operation is continually thwarted and may never terminate, while guaranteeing termination if the interference on the data structure eventually quiesces. Using ${c^{\omega}}$ to represent the execution of a command $c$ zero or more times, including possibly infinitely many times, such specifications have the general form $${fail^{\omega}} {\mathbin{\mathbin{;}}}succeed$$ where $fail$ represents the operation failing due to interference (and not changing the state) and $succeed$ represents the operation successfully completing (and updating the state once). The iteration ${fail^{\omega}}$ may execute $fail$ infinitely many times representing the continual thwarting by interference from parallel operations. Arguments about termination usually need to resort to either

-   arguments that interference eventually quiesces altogether,

-   timing arguments based on minimal separation between operations in any single thread leading to a situation in which interference will eventually quiesce for long enough for the operation to succeed, and

-   arguments based on probabilities of two (or more) operations overlapping and competing.

Note that probability bounds can be derived from timing bounds. The probability can be sensitive to load, i.e. the more threads competing, the lower the probability of success of any single operation. And probabilities can also be sensitive to the execution time of an operation: the longer it executes, the more likely it is to overlap with a competing operation. Of course, such timing and probability arguments depend on the context of the use of the data structure and can be tricky in practice.

Implicit specifications can also be used for such operations by specifying the conditions under which they are guaranteed to terminate.

#### Overview.

Sect. \[S-atomicity\] addresses specifying atomic operations on a shared data structure (or resource). It examines the use of Hoare's ${{\mathop{\mathbf{with}}}}$ statement @Hoare71g and how it interacts with rely and guarantee conditions. Sect. \[S-blocking\] examines blocking operations giving both explicit waiting conditions and more implicit specifications using a temporal logic formula under which an operation terminates. Sect. \[S-transactional\] looks at transactional operations that may either succeed, or try and fail, possibly indefinitely. Both explicit waiting and implicit temporal logic specifications are considered.

Specifying atomicity {#S-atomicity}
====================

As an example, consider a message queue with operations to enqueue and dequeue messages. If there are separate concurrent threads enqueuing and dequeuing, each operation needs to (appear to be) be atomic, i.e. other operations cannot observe the state part way through the operation. If the queue were used in a purely sequential program, the ${write}$ and ${read}$ operations can be specified by Morgan-style specification commands @TSS [@Morgan94] as follows. $$\begin{aligned}
  {write}(v : Val) & {\mathrel{\widehat{=}}}& \Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]} \\
  {read}() res : Val & {\mathrel{\widehat{=}}}& {\{qu \neq [~]\}} {\mathbin{\mathbin{;}}}\Spec{res,qu}{}{qu = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}qu'}\end{aligned}$$ The ${write}$ operation takes a value $v$ to append to the queue. Its postcondition is $qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]$, in which $qu'$ stands for the final value of the queue, $qu$ stands for the initial value, "${\mathbin{\raise 0.8ex\hbox{$\frown$}}}$" is sequence concatenation, and $[v]$ is the singleton sequence containing $v$. The ${write}$ operation modifies only the queue and hence it has a frame of $qu$ (before the colon). The ${read}$ operation returns a value $res$ that is the head of the queue and removes it from the queue in the process. It has a precondition that the queue is non-empty, which is written as an assertion command (in braces).

To extend the operation specification to handle concurrency, as presented in Fig. \[F-queue\], the operations need to be augmented with rely and guarantee conditions and the atomicity of the operations needs to be handled. In Fig. \[F-queue\] the relies and guarantees are represented as rely and guarantee commands @DaSMfaWSLwC [@FM2016atomicSteps; @FMJournalAtomicSteps]. The guarantee command $({{\mathop{{\mathop{\mathbf{guar}}}}}~g})$ restricts every atomic program step of the thread to satisfy $g$. The rely command $({{{{\mathop{\mathbf{rely}}}}}~r})$ represents an assumption that every environment step satisfies $r$; if an execution trace performs an environment step not satisfying $r$, any behaviour whatsoever is allowed from that point (i.e. it aborts in a manner similar to the precondition command ${\{p\}}$ aborting if the initial state does not satisfy $p$). The rely and guarantee commands are combined with the remainder of the specification using the weak conjunction operator "${\mathbin{\Cap}}$" @HayesJonesColvin14TR [@AFfGRGRACP]. The weak conjunction $c_0 {\mathbin{\Cap}}c_1$ performs steps allowed by both $c_0$ and $c_1$ unless either $c_0$ or $c_1$ aborts at some point, in which case their weak conjunction aborts from that point. Weak conjunction is a specification operator, rather than a programming operator.

For the message queue we assume there is a single writer thread performing ${write}$ operations and a single reader thread performing ${read}$ operations. A suitable rely condition for ${write}$ is that elements are only ever removed from the front of the queue, i.e. the queue after any interference is a suffix of the queue before. The rely condition for ${read}$ is that the interference only ever adds elements to the end of the queue and hence the queue before the interference is a prefix of the queue after. Note that the precondition of ${read}$ is stable under its rely condition @Wickerson10-TR [@DBLP:conf/esop/WickersonDP10], i.e. $qu \neq [~] \land qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu' {\mathrel{\Rrightarrow}}qu' \neq [~]$. The guarantees of each operation match the rely of the other operation. This version requires that there is just one reader thread and one writer thread because the rely condition of ${read}$ assumes the queue can only be extended and hence it is not concurrently being dequeued by another thread, and the rely condition of ${write}$ assumes the queue can only become a suffix of its previous state and hence it is not concurrently being enqueued by another thread.

For sequential programs and in the original rely/guarantee approach the postconditions of operations are considered end-to-end, i.e. they must hold between the states at the start and end of an operation invocation. Such a postcondition is problematic in the context of a parallel thread modifying the queue, for example, after an ${write}$ operation is initiated but before it can complete (or lock the data structure), the reader thread may ${read}$ a value. If the writer then completes the ${write}$ without further interference, the end-to-end effect is that of both the ${read}$ and the ${write}$, not just the ${write}$. An end-to-end postcondition is not suitable in this case. The alternative is a specification whereby the postcondition holds for some "atomic" step between the start and end of the operation and the operation makes no changes to the queue before or after that step, although other threads may. Atomicity can be handled by using resources (see Sect. \[S-resources\]). The environment may also interfere with operation preconditions. For example, if multiple readers were allowed on a queue, a precondition that the queue is non-empty may be invalidated by a parallel ${read}$ operation that reads the last value from the queue thus making it empty.

Resources {#S-resources}
---------

------------------------------------------------------------------------

$$\begin{array}{l}
  {{\mathop{\mathbf{resource}}}}qu : {{\mathop{\mathbf{seq}}}}Val~~{{\mathop{\mathbf{initially}}}}qu = [~] \\[1ex]
  {write}(v : Val) {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    ({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}~~~{~~~~\mbox{\color{darkgreen}-- implies single writer}} \\
    ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies the rely of {read}}}  \\
    {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  \end{array} \\[4ex]
  {read}() res : Val {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    ({{{{\mathop{\mathbf{rely}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}~~~{~~~~\mbox{\color{darkgreen}-- implies single reader}} \\
    ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}~{~~~~\mbox{\color{darkgreen}-- implies the rely of {write}}} \\
    {\{qu \neq [~]\}} {\mathbin{\mathbin{;}}}{~~~~\mbox{\color{darkgreen}-- stable under the rely condition}} \\
    {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu,res}{}{qu = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}qu'}\,{{{\mathop{\mathbf{od}}}}}}
  \end{array}
 \end{array}$$

------------------------------------------------------------------------

Early work of Hoare @Hoare71g introduced the idea of a resource and a ${{\mathop{\mathbf{with}}}}$ statement that provides access to the resource. A *resource* represents a shared data structure that is only accessible to a thread within a command of the form, $$\begin{aligned}
  {{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,c\,{{{\mathop{\mathbf{od}}}}}}\end{aligned}$$ that ensures the resource $d$ is not modified by the environment while the thread is executing $c$. A data structure $d$ is declared as a resource by a declaration of the form ${{\mathop{\mathbf{resource}}}}d$ and, within the scope of the resource declaration, all uses of $d$ must be within a ${{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,...\,{{{\mathop{\mathbf{od}}}}}}$ statement.[^1] It is required that the data structure of the resource is only accessed within ${{\mathop{\mathbf{with}}}}$ statements; this may be checked syntactically. The implementation is responsible for ensuring the data structure is not modified by the environment while executing within the ${{\mathop{\mathbf{with}}}}$ statement. The ${{\mathop{\mathbf{with}}}}$ statement allows any number of stuttering steps before the body and finite stuttering after the body of the ${{\mathop{\mathbf{with}}}}$ is executed. As entry to a ${{\mathop{\mathbf{with}}}}$ statement by one thread may block other threads wishing to gain access to the same resource, it is prudent to require that the bodies of ${{\mathop{\mathbf{with}}}}$ statements terminate; that is required within this paper. The data structure of the resource also often has a data-type invariant associated with it that is established by its initialisation and maintained by each operation (see the example in Section \[S-blocking\]).

An operation whose body consists of a single ${{\mathop{\mathbf{with}}}}$ statement executes the ${{\mathop{\mathbf{with}}}}$ statement atomically at some point of time between its invocation and completion. Hence multiple operations that overlap in time will have their bodies executed in some sequence (i.e. their execution is linearized @HW90) and hence they will appear to behave equivalently to some sequential execution of the same operations, i.e. their execution is sequentially consistent.

Rely/guarantee laws for resource access
---------------------------------------

The concept of a resource may be combined with the rely/guarantee approach. When a thread enters the body of a ${{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,c\,{{{\mathop{\mathbf{od}}}}}}$ statement, the rely can be strengthened for the duration of $c$ with $d\,' = d$ and the guarantee weakened so that $d$ only need satisfy the guarantee over the complete operation, not over every step. The initial step of the refinement of operations specified via a ${{\mathop{\mathbf{with}}}}$ statement needs to "move" the rely and guarantee conditions into the body of the ${{\mathop{\mathbf{with}}}}$ but in the process the rely and guarantee conditions are transformed.

\[rely-with\]\[law-rely-with\] $
  ~~~~({{{{\mathop{\mathbf{rely}}}}}~r}) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,c\,{{{\mathop{\mathbf{od}}}}}} ~{\mathrel{\sqsubseteq}}~ {{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{{{\mathop{\mathbf{rely}}}}}~r \land d\,'=d}) {\mathbin{\Cap}}c\,{{{\mathop{\mathbf{od}}}}}}
$

For the ${write}$ operation above (ignoring the guarantee for the moment) this law can be applied as follows. $$\begin{array}{l}
  ({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}{\mathrel{\sqsubseteq}}\@ifnextchar*{\@ChainRelCommment}{}}}*[by \Law{rely-with}]
  {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu \land qu' = qu}) {\mathbin{\Cap}}\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}=
  \@ifnextchar*{\@ChainRelCommment}{}}}*[as $qu' = qu ~{\mathrel{\Rrightarrow}}~ qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu$]
  {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{{{\mathop{\mathbf{rely}}}}}~qu' = qu}) {\mathbin{\Cap}}\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
 \end{array}$$

A guarantee condition surrounding a ${{\mathop{\mathbf{with}}}}$ may be weakened so that it only has to apply for the resource data structure over the body of the ${{\mathop{\mathbf{with}}}}$ command. It is assumed that the guarantee is of the form $g_d \land g_x$, where $d$ is the only shared variable $g_d$ refers to, and $g_x$ does not refer to $d$. The weakened guarantee $g_x$ is retained to handle references to variables other than $d$ within the guarantee. The specification $\Spec{}{}{g_d}$ requires $g_d$ to hold end-to-end over the body of the ${{\mathop{\mathbf{with}}}}$. The lack of a frame allows any variables to be modified but when it is combined with $c$, any frame of $c$ will apply to their weak conjunction.

\[guar-with\]\[law-guar-with\] $
  ~~~~({{\mathop{{\mathop{\mathbf{guar}}}}}~g_d \land g_x}) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,c\,{{{\mathop{\mathbf{od}}}}}} ~{\mathrel{\sqsubseteq}}~ 
      {{{\mathop{\mathbf{with}}}}\,d\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{\mathop{{\mathop{\mathbf{guar}}}}}~g_x}) {\mathbin{\Cap}}\Spec{}{}{g_d} {\mathbin{\Cap}}c\,{{{\mathop{\mathbf{od}}}}}}
$

For the ${write}$ operation above (ignoring the rely for the moment) this law can be applied as follows. $$\begin{array}{l}
  ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}{\mathrel{\sqsubseteq}}\@ifnextchar*{\@ChainRelCommment}{}}}*[by \Law{guar-with} with $g_d {\mathrel{\widehat{=}}}qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'$ and $g_x {\mathrel{\widehat{=}}}{{\mathsf{true}}}$]
  {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{\mathop{{\mathop{\mathbf{guar}}}}}~{{\mathsf{true}}}}) {\mathbin{\Cap}}\Spec{}{}{qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'} {\mathbin{\Cap}}\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}=
  \@ifnextchar*{\@ChainRelCommment}{}}}*[as $({{\mathop{{\mathop{\mathbf{guar}}}}}~{{\mathsf{true}}}})$ requires no guarantee and $\Spec{}{}{q_1} {\mathbin{\Cap}}\Spec{x}{}{q_2} = \Spec{x}{}{q_1 \land q_2}$]
  {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu' \land qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
  {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}=
  \@ifnextchar*{\@ChainRelCommment}{}}}*[as {$qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v] ~{\mathrel{\Rrightarrow}}~ qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'$}]
  {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
 \end{array}$$ Combining the above applications of and , the following refinement of the ${write}$ operation holds. $$\begin{array}{l}
    ({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}({{\mathop{{\mathop{\mathbf{guar}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
   {{\crcr \noalign{\penalty\interdisplaylinepenalty}
  \hspace*{-1em}{\mathrel{\sqsubseteq}}\@ifnextchar*{\@ChainRelCommment}{}}}*[using \Law{guar-with} and \Law{rely-with}]
    {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,({{{{\mathop{\mathbf{rely}}}}}~qu' = qu}) {\mathbin{\Cap}}\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
 \end{array}$$ Note that in the body of the ${{\mathop{\mathbf{with}}}}$ there is no explicit guarantee and the rely condition assumes that $qu$ is not modified by the environment and hence the refinement of the body of the ${{\mathop{\mathbf{with}}}}$ is effectively a sequential refinement (as one would expect).

Specifying operations that may block {#S-blocking}
====================================

------------------------------------------------------------------------

$$\begin{array}{l}
  {{\mathop{\mathbf{resource}}}}qu : {{\mathop{\mathbf{seq}}}}Val~~{{\mathop{\mathbf{invariant}}}}~\# qu \leq N~~{{\mathop{\mathbf{initially}}}}qu = [~] \\[1ex]
  {write}(v : Val) {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    ({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies single writer}} \\
    ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies the rely of {read}}} \\
    {{{\mathop{\mathbf{with}}}}\,qu\,{{\mathop{\mathbf{await}}}}\,\# qu < N\,{\mathop{{\mathop{\mathbf{do}}}}}\,{~~~~\mbox{\color{darkgreen}-- stable under the rely condition}} \\~~~
      {\{\# qu < N\}} {\mathbin{\mathbin{;}}}\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}
    \,{{{\mathop{\mathbf{od}}}}}}
  \end{array} \\[5ex]
  {read}() res : Val {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    ({{{{\mathop{\mathbf{rely}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies single reader}} \\
    ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies the rely of {write}}} \\
    {{{\mathop{\mathbf{with}}}}\,qu\,{{\mathop{\mathbf{await}}}}\,qu \neq [~]\,{\mathop{{\mathop{\mathbf{do}}}}}\,{~~~~\mbox{\color{darkgreen}-- stable under the rely condition}} \\~~~
      {\{qu \neq [~]\}} {\mathbin{\mathbin{;}}}\Spec{qu,res}{}{qu = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}qu'}
    \,{{{\mathop{\mathbf{od}}}}}}
  \end{array}
 \end{array}$$

------------------------------------------------------------------------

Blocking using an explicit await condition {#S-blocking-await}
------------------------------------------

Consider the example in Fig. \[F-blocking-queue\] of a message queue with a bounded capacity of $N$ messages. It has a ${write}$ operation that waits until the queue is not full and appends a value to the tail of the queue, and a ${read}$ operation that waits until there is a message in the queue and returns the head of the queue, removing it in the process. The queue has a data-type invariant that its size is bounded by $N$. The initialisation establishes the invariant (assuming $N$ is a positive integer) and each operation on the queue can assume the invariant when it starts and must be re-establish the invariant when it terminates.

A common approach to specifying potentially blocking operations is to use an ${{\mathop{\mathbf{await}}}}$ statement. The form used here is combined with a ${{\mathop{\mathbf{with}}}}$ statement. The statement ${{{\mathop{\mathbf{with}}}}\,d\,{{\mathop{\mathbf{await}}}}\,b\,{\mathop{{\mathop{\mathbf{do}}}}}\,c\,{{{\mathop{\mathbf{od}}}}}}$ waits until condition $b$ holds and then executes $c$. The resource $d$ is attained each time $b$ is evaluated, and retained for the execution of $c$ if $b$ is true; if $b$ is false the resource is released and the await retries. For both the ${write}$ and ${read}$ operations the await conditions are stable under the rely condition, i.e. if the await condition $b$ holds before a step that satisfies the rely condition $r$, then $b$ holds after the step. Hence once the operations are enabled, they remain enabled until they occur.

Blocking using temporal logic termination conditions {#S-blocking-assume}
----------------------------------------------------

------------------------------------------------------------------------

$$\begin{array}{l}
  {{\mathop{\mathbf{resource}}}}qu : {{\mathop{\mathbf{seq}}}}Val~~{{\mathop{\mathbf{invariant}}}}~\# qu \leq N~~{{\mathop{\mathbf{initially}}}}qu = [~] \\[1ex]
  {write}(v : Val) {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    {{\mathop{\mathbf{terminate}}}}{\mathop{\Diamond}}(\# qu < N) {\mathbin{\Cap}}{}\\~~~
     \begin{array}{l}
      ({{{{\mathop{\mathbf{rely}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies single writer}} \\
      ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies the rely of {read}}} \\
      {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu}{}{qu' = qu {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[v]}\,{{{\mathop{\mathbf{od}}}}}}
    \end{array}
  \end{array} \\[5ex]
  {read}() res : Val {\mathrel{\widehat{=}}}\\~~~
  \begin{array}{l}
    {{\mathop{\mathbf{terminate}}}}{\mathop{\Diamond}}(qu \neq [~]) {\mathbin{\Cap}}{}\\~~~
     \begin{array}{l}
      ({{{{\mathop{\mathbf{rely}}}}}~qu {\mathrel{{\mathop{\mathbf{prefixof}}}}}qu'}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies single reader}} \\
      ({{\mathop{{\mathop{\mathbf{guar}}}}}~qu' {\mathrel{{\mathop{\mathbf{suffixof}}}}}qu}) {\mathbin{\Cap}}{~~~~\mbox{\color{darkgreen}-- implies the rely of {write}}} \\
      {{{\mathop{\mathbf{with}}}}\,qu\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{qu,res}{}{qu = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}qu'}\,{{{\mathop{\mathbf{od}}}}}}
    \end{array}
  \end{array}
 \end{array}$$

------------------------------------------------------------------------

The specifications of ${read}$ and ${write}$ in Fig. \[F-blocking-queue\], by including ${{\mathop{\mathbf{await}}}}$ statements, allow non-terminating behaviour in the cases where the await condition never becomes true, e.g. a ${read}$ will wait forever if the queue remains empty because no writes are performed. However, ${read}$ terminates if the queue is eventually non-empty and ${write}$ terminates if the queue is eventually non-full. That leads to an alternative specification using temporal logic termination conditions in Fig. \[F-assume-queue\]. To accommodate the termination conditions, a command of the form, $$\begin{aligned}
  {{\mathop{\mathbf{terminate}}}}t  & {\mathrel{\widehat{=}}}& {{\mathop{\mathbf{term}}}}{\mathbin{\sqcap}}({{\mathop{\mathbf{encode}}}}\lnot t)\end{aligned}$$ is introduced, in which the command ${{\mathop{\mathbf{term}}}}$ only allows any terminating behaviour and for a temporal logic formula $t$, the command ${{\mathop{\mathbf{encode}}}}t$ allows just those traces that satisfy $t$.[^2] If the temporal logic formula $t$ holds, ${{\mathop{\mathbf{terminate}}}}t$ must terminate, but if $t$ does not hold termination is not required, but is allowed. Neither of the specifications of ${write}$ and ${read}$ in Fig. \[F-assume-queue\], contain the explicit ${{\mathop{\mathbf{await}}}}$s used in Fig. \[F-blocking-queue\]. The postcondition of the ${read}$ is unsatisfiable if the queue always remains empty because $$\begin{aligned}
[~] = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}qu' & \equiv & {{\mathsf{false}}}~.\end{aligned}$$ However, if the condition ${\mathop{\Diamond}}(qu \neq [~])$ holds (i.e. the queue is eventually non-empty), the postcondition eventually becomes feasible from the state in which the queue is non-empty. Note that $qu \neq [~]$ is stable under the rely condition and so it will not be falsified by the environment and hence the termination condition is equivalent to ${\mathop{\Diamond}}{\mathop{\Box}}(qu \neq [~])$ in this case.

For the ${read}$ operation, the negation of ${\mathop{\Diamond}}(qu \neq [~])$ is ${\mathop{\Box}}(qu = [~])$, i.e. the queue is always empty. If ${\mathop{\Box}}(qu = [~])$ the ${read}$ operation is not required to terminate. In addition, if in every state $qu = [~]$, the postcondition of ${read}$ is unsatisfiable because $[~] = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}[~]$ is false, and hence the terminating behaviour of ${read}$ is infeasible, and therefore the only possible behaviour if ${read}$ is to not terminate.

More subtly, any finite prefix of a trace of a ${read}$ operation for which $qu = [~]$ in every state cannot have satisfied the postcondition of ${read}$ and hence cannot have terminated. However, it is still possible that another thread may execute a ${write}$ at some later time establishing $qu \neq [~]$ and allowing the ${read}$ to terminate. For the finite prefix of the trace, the behaviour of the ${read}$ must correspond to the stuttering allowed by the ${{\mathop{\mathbf{with}}}}$ statement before it enters its body. Hence for every finite prefix of a trace of ${read}$ in which $qu = [~]$ in every state, the operation performs only finite stuttering steps and, further, nontermination is allowed if ${\mathop{\Box}}(qu = [~])$. Hence the behaviours allowed by the specifications in Fig. \[F-assume-queue\] are actually equivalent to those of the specifications in Fig. \[F-blocking-queue\].

For the queue example, if multiple readers and writers are allowed, the specifications need to be adapted. Firstly, the rely conditions of the ${write}$ and ${read}$ operations need to be removed because the rely of ${write}$ is broken by a concurrent thread also performing ${write}$s, and similarly for the rely of ${read}$ if there are concurrent readers. Secondly, the termination conditions need to be strengthened. There are two strengthenings that correspond to weakly and strongly fair interpretations of the await in specifications using ${{\mathop{\mathbf{await}}}}$.

For weak fairness the termination condition of ${read}$ is strengthened to ${\mathop{\Diamond}}{\mathop{\Box}}(qu \neq [~])$, that is, eventually the queue remains non-empty, which implies that concurrent threads are not making the queue empty through ${read}$ operations. For the equivalent specification using an ${{\mathop{\mathbf{await}}}}$ rather than a ${{\mathop{\mathbf{terminate}}}}$, the ${{\mathop{\mathbf{await}}}}$ can be given a weakly fair interpretation, i.e. if the guard of the await for ${read}$, $qu \neq [~]$, is eventually continually enabled, the ${{\mathop{\mathbf{await}}}}$ will succeed. The termination condition for ${write}$ is similar.

For strong fairness the termination condition of ${read}$ is the weaker ${\mathop{\Box}}{\mathop{\Diamond}}(qu \neq [~])$, that is, it is always the case that eventually the queue is non-empty, which implies that concurrent threads can repeatedly make the queue empty through ${read}$ operations but if the queue becomes empty there must then be one of more ${write}$ operations that make it non-empty. Because the termination condition is weaker, this version of ${read}$ must terminate for a wider range of behaviours of its environment and hence requires a stronger implementation, e.g. one that strictly sequences access to the queue, perhaps using a ticket lock.

For the equivalent specification using an ${{\mathop{\mathbf{await}}}}$ rather than a ${{\mathop{\mathbf{terminate}}}}$, the ${{\mathop{\mathbf{await}}}}$ can be given a strongly fair interpretation, i.e. if the guard of the await for ${read}$, $qu \neq [~]$, is always eventually enabled (but the queue may alternate between empty and non-empty), the ${{\mathop{\mathbf{await}}}}$ will succeed.

An advantage of the specifications using ${{\mathop{\mathbf{terminate}}}}$ clauses is that the condition under which an operation is guaranteed to terminate is made explicit, unlike specifications using await statements where the semantics of the await needs to be changed. This makes it clearer what a programmer using a component can rely on. It also avoids the complication of having different interpretations of await guards as used by Liang and Feng @LiangFengPOPL18.

Transactional operations {#S-transactional}
========================

Some implementations of operations are optimistic in that they complete most of the operation locally within a thread and then have a final commit phase that may fail if another operation has committed. Such operations consist of a repeated failure behaviour (that does not change the shared data structure) in the presence of interference followed by a successful commit phase. Of course, in the presence of repeated interference the successful commit may never occur. There are many examples of lock-free algorithms that exhibit the above behaviour @Scott13 but to make the discussion concrete, we make use of Treiber's well-known concurrent stack data structure @Treiber86.

Specification using explicit failure {#S-transactional-explicit}
------------------------------------

------------------------------------------------------------------------

$$\begin{array}{l}
  {{\mathop{\mathbf{resource}}}}s : {{\mathop{\mathbf{seq}}}}Val~~{{\mathop{\mathbf{initially}}}}s = [~] \\[2ex]
  push(v : Val) {\mathrel{\widehat{=}}}{\{v \neq {\mathsf{null}}\}} {\mathbin{\mathbin{;}}}{push\_fail^{\omega}} {\mathbin{\mathbin{;}}}push\_success(v) \\[0ex]
  {{\mathop{\mathbf{where}}}}\begin{array}[t]{l}
    push\_fail {\mathrel{\widehat{=}}}{\epsilon{\langles' \neq s\rangle}} \\
    push\_success(v : Val) {\mathrel{\widehat{=}}}{{{\mathop{\mathbf{with}}}}\,s\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{s}{}{s' = [v] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}s}\,{{{\mathop{\mathbf{od}}}}}} {\mathbin{\Cap}}{{\mathop{\mathbf{term}}}}\end{array}\\[4ex]
  pop() res : Val {\mathrel{\widehat{=}}}{pop\_fail^{\omega}} {\mathbin{\mathbin{;}}}res:= pop\_success() \\[0ex]
  {{\mathop{\mathbf{where}}}}\begin{array}[t]{l}
    pop\_fail {\mathrel{\widehat{=}}}{\epsilon{\langles' \neq s\rangle}} \\
    pop\_success() res : Val {\mathrel{\widehat{=}}}{{{\mathop{\mathbf{with}}}}\,s\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{s,res}{}{(s \neq [~] {\mathrel{\Rightarrow}}s = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}s') \land \\(s = [~] {\mathrel{\Rightarrow}}res' = {\mathsf{null}}}\,{{{\mathop{\mathbf{od}}}}}} {\mathbin{\Cap}}{{\mathop{\mathbf{term}}}}\end{array}
 \end{array}$$

------------------------------------------------------------------------

Treiber @Treiber86 provided a non-blocking lock-free implementation of a stack in which the push and pop operations may be concurrently executed by many threads. However, an attempt to push or pop a value may fail due to interference from parallel stack operations, and hence it may need to be retried until it succeeds. In the worse case, if every time an operation is tried it fails due to interference, that invocation of operation may never terminate.

Fig. \[F-stack\] gives a specification of a stack with $push$ and $pop$ operations that may fail and need to retry, possibly indefinitely. If the stack is empty, $pop$ returns the special value ${\mathsf{null}}$, which may not be pushed onto the stack.[^3] The $push\_fail$ operation may be executed any number of times but each time it is executed the environment makes a step that changes the stack $s$. If from some point of time the environment never changes $s$, then the $push\_fail$ becomes infeasible and the operation must perform $push\_success$ which pushes the value on the stack and terminates; the command ${{\mathop{\mathbf{term}}}}$ only allows any terminating computation and hence when conjoined with a specification restricts it to just its terminating behaviours. The command ${\epsilon{\langles' \neq s\rangle}}$ corresponds to the environment performing a step that modifies $s$; it may also perform a finite number of stuttering program steps (i.e. steps that do not change observable variables). If the environment performs a step modifying $s$, ${\epsilon{\langles' \neq s\rangle}}$ terminates but if not, it becomes infeasible and termination of the iteration is forced, so that the $push\_success$ alternative is taken. The definition of $pop$ is similar.

Specification using temporal logic termination conditions {#S-transactional-assume}
---------------------------------------------------------

Note that if the stack $s$ is never changed by the environment, the behaviour of the $push$ (or $pop$) operation reduces to just its successful behaviour. More subtly, if the environment eventually stops changing $s$, then there can only be a finite number of failure iterations before the operation succeeds. This latter condition can be converted into a temporal logic termination condition ${\mathop{\Diamond}}{\mathop{\Box}}_{\epsilon}(s' = s)$, i.e. eventually all environment steps do not change the value of the stack, which leads to the specification given in Fig. \[F-stack-assume\]. An extended form of temporal logic is used here that distinguishes program and environment steps and allows one to specify a constraint on a step in the form of a relation, in this case $s'=s$. If parallel activity on the stack eventually quiesces, Treiber's push and pop operations are guaranteed to terminate, and hence the specifications with the quiescence termination conditions do not need to include the failure possibilities.

------------------------------------------------------------------------

$$\begin{array}{l}
  {{\mathop{\mathbf{resource}}}}s : {{\mathop{\mathbf{seq}}}}Val~~{{\mathop{\mathbf{initially}}}}s = [~] \\[2ex]
  push(v : Val) {\mathrel{\widehat{=}}}{\{v \neq {\mathsf{null}}\}} {\mathbin{\mathbin{;}}}{{\mathop{\mathbf{terminate}}}}{\mathop{\Diamond}}{\mathop{\Box}}_\epsilon(s' = s) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,s\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{s}{}{s' = [v] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}s}\,{{{\mathop{\mathbf{od}}}}}} \\[2ex]
  pop() res : Val {\mathrel{\widehat{=}}}{{\mathop{\mathbf{terminate}}}}{\mathop{\Diamond}}{\mathop{\Box}}_\epsilon(s' = s) {\mathbin{\Cap}}{{{\mathop{\mathbf{with}}}}\,s\,{\mathop{{\mathop{\mathbf{do}}}}}\,\Spec{s,res}{}{(s \neq [~] {\mathrel{\Rightarrow}}s = [res'] {\mathbin{\raise 0.8ex\hbox{$\frown$}}}s') \land \\(s = [~] {\mathrel{\Rightarrow}}res' = {\mathsf{null}}}\,{{{\mathop{\mathbf{od}}}}}}
 \end{array}$$

------------------------------------------------------------------------

The negation of the termination condition is ${\mathop{\Box}}{\mathop{\Diamond}}_\epsilon(s' \neq s)$, i.e. from every state there is eventually an environment step that modifies $s$. However –unlike for the blocking queue– that does not make the postcondition of either operation unsatisfiable and hence if the negation of the termination condition holds, each operation may either terminate satisfying its postcondition or never terminate. In a similar manner to the blocking queue, for a finite trace for which an operation has not yet satisfied its postcondition, it is still possible to extend the trace so that the postcondition is satisfied, and hence the only allowable behaviour of the operation for a finite trace that has not yet satisfied its postcondition is finite stuttering. Hence if the termination condition is not satisfied an operation may either terminate successfully satisfying its postcondition or fail to terminate but only ever perform stuttering steps, i.e. it never modifies $s$. Hence the specifications in Fig. \[F-stack-assume\] are equivalent to those in Fig. \[F-stack\].

If the termination conditions on the stack operations are replaced by $true$, the operations must always terminate, even under interference from other threads performing $push$ and $pop$ operations. That gives strictly stronger specifications because their termination conditions are weaker. An implementation might then be required to make use of a lock that sequentialises access to the stack in the order in which the lock is requested (such as a ticket lock) in order to ensure termination.

Conclusions {#S-conclusions}
===========

To specify concurrent program components one needs to be able to address issues such as operation atomicity, operations blocking on conditions or locks, and transactional operations that may fail and need to be retried. Hoare's resource concept provides a notion of atomicity with respect to a resource. A contribution of this paper is to examine its interaction with rely and guarantee conditions in order to enable the initial refinement step of Hoare's ${{\mathop{\mathbf{with}}}}$ statements to code. Brookes @BrookesSepLogic07 also makes use of the concept of a resource in concurrent separation logic. He generalises Hoare's concept to handle the heap as well as variables.

The specifications of operations using ${{\mathop{\mathbf{with}}}}$ statements do not dictate whether they are refined to implementations using locks or to non-blocking implementations or even a programming language that supports ${{\mathop{\mathbf{with}}}}$ statements. One issue not addressed here is that operations requiring multiple resources, e.g. an operation that needs to perform operations on two separate resources and needs to be considered atomic as a whole. In this case the ${{\mathop{\mathbf{with}}}}$ statement needs to allow for multiple resources, and if locking is used in the implementation of the operations, to avoid deadlock, the locking has to ensure that resources are locked in the same order. Note that ${{\mathop{\mathbf{with}}}}$ statements may be nested but they do not allow the complete flexibility of locks. For example, algorithms that lock one node in a list and then lock the next node before releasing the first node do not match a nesting structure.

Operations that block waiting for some condition have the potential for non-terminating behaviour. That has been addressed via two ways of specifying such operations: a form that makes use of an ${{\mathop{\mathbf{await}}}}$ construct that blocks until its guard holds, and an implicit form that includes a condition under which termination is required.

Non-blocking algorithms can provide more efficient solutions for managing shared data structures than using locks, but some algorithms have the issue that, under interference, they may fail and need to be retried. In the worst case an operation may be continually thwarted and never get a chance to complete and hence its specification needs to either allow for that possible behaviour or provide conditions under which it will terminate successfully, e.g. that the interference quiesces so that it can complete.

The approach taken in this paper is to indicate some directions for devising specifications for concurrent program components. In doing so we have shown that specifications with explicit await clauses can be expressed in a more abstract form with a temporal logic formula giving the condition under which termination is guaranteed. Such specifications have greater expressive power than those using explicit await constructs because temporal logic formulae allow termination conditions that cannot be expressed as await conditions, for example, if the blocking queue allows multiple readers and hence its await condition was no longer stable, an alternative termination condition of ${\mathop{\Box}}{\mathop{\Diamond}}(qu \neq [~])$ would require an implementation to guarantee the termination of each <span>read</span> operation under interference from other <span>read</span>s, provided a writer was also actively appending values to the queue. An implementation of ${read}$ might, for example, use a lock that sequentialises access in the order in which the lock is requested (such as a ticket lock) in order to ensure termination.

Liang and Feng @LiangFengPOPL18 have addressed handling progress conditions for blocking operations (which they refer to as partial methods). Their approach makes use of await statements but they give four different semantic interpretations to await statements depending on whether one requires the operations to be starvation free or deadlock free, and depending on whether the enabling conditions are treated as weakly or strongly fair. The weakly and strongly fair interpretations correspond to different termination conditions for operations. The explicit use of a temporal logic termination condition differentiates these two cases while avoiding the issues involved with giving different semantic interpretations to the await construct.

At this stage our treatment has not been fully formalised and further work is required to support refinement of such specifications to code.

#### Acknowledgements.

Thanks are due to Robert Colvin, Cliff Jones, Larissa Meinicke, Patrick Meiring, and Kirsten Winter, and the anonymous reviewers for feedback on the ideas presented here. This research was supported Australian Research Council Discovery Grant DP130102901.

[^1]: A more general resource construct would allow a resource to encompass a set of variables but for the examples here a resource will correspond to a single variable, so we identify the resource with the variable to simplify the presentation.

[^2]: Such a command can be straightforwardly defined in the semantics for rely/guarantee concurrency presented in @DaSMfaWSLwC.

[^3]: In the context of concurrent stack operations, the $pop$ operation must well defined when the stack is empty; note that even if an $is\_empty$ operation returned false, concurrent interference may empty the stack before a subsequent $pop$ operation.

{'source': 'arXiv_out/1810'}