Bilateral Proofs of Safety and Progress Properties of Concurrent Programs

TL;DR

This paper introduces a bilateral compositional proof system for verifying safety and progress properties of concurrent programs, enabling modular verification and specification composition even with unavailable source code.

Contribution

It develops a novel bilateral proof technique and composition rules for concurrent program specifications, facilitating modular verification and integration.

Findings

Proof techniques for verification of concurrent programs

Composition rules for deriving program specifications

Applicable to cross-vendor program integration

Abstract

This paper suggests a theomisra@utexas.edury of composable specification of concurrent programs that permits: (1) verification of program code for a given specification, and (2) composition of the specifications of the components to yield the specification of a program. The specification consists of both terminal properties that hold at the end of a program execution (if the execution terminates) and perpetual properties that hold throughout an execution. We devise (1) proof techniques for verification, and (2) composition rules to derive the specification of a program from those of its components. We employ terminal properties of components to derive perpetual properties of a program and conversely. Hence, this proof strategy is called bilateral. The compositional aspect of the theory is important in assembling a program out of components some of whose source code may not be available, as is increasingly the case with cross-vendor program integration.

Tables

Table 1. Table 1: Proofs of (S3), (S4) and (S5)

		$\alpha$	$\beta$	$\gamma$
(S3)	$cs\Rightarrow try$	post: $\neg cs$	post: $try$	post: $\neg cs$
(S4)	$try\Rightarrow turn$	post: $turn$	unaff.: $try,turn$	post: $\neg try$
(S5)	$cs\wedge tr{y}^{\prime }\Rightarrow tur{n}^{\prime }$	post: $\neg cs$	see text	post: $\neg cs$

Full text

Keywords: Program specification, concurrent programming, verification, composition, safety and progress properties.

1 Introduction

Four decades of intensive research has failed to yield a scalable solution to the problem of concurrent program design and verification. While there have been vast improvements in our understanding, the theory and practice in this area lag considerably behind what has been achieved for sequential programs. Very small programs, say for synchronization, are proved manually, though the proof methods are mostly unscalable. Larger programs of practical significance, say cache coherence protocols, are typically proved using model checking, which imposes size limitations. Programs from different vendors are rarely assembled to run concurrently.

We believe that the problem stems from the lack of a theory of composable specification for concurrent programs. Sequential imperative programs enjoy such a theory, introduced by Hoare [7], in which a program is specified by a pair of predicates, called its pre- and postcondition. The theory successfully permits: (1) verification of program code for a given specification, and (2) composition of the specifications of the components to yield the specification of a program. A fundamental concept is invariant that holds at specific program points, though invariant is not typically part of the program specification. Termination of a program is proved separately.

A specification of a concurrent program typically includes not just the pre- and postconditions but properties that hold of an entire execution, similar to invariants. A typical specification of a thread that requests a resource, for example, may state that: (1) once it requests a resource the thread waits until the resource is granted, and (2) once the resource is granted the thread will eventually release it. The first property is an instance of a safety property and the second of a progress property, see Lamport [10] and Owicki and Lamport [14].

Call the postcondition of a program for a given precondition to be a terminal property. And a property that holds throughout an execution a perpetual property. Terminal properties compose only for sequential programs, though not for concurrent programs, and they constitute the essence of the assertional proof method of Hoare. Safety and progress are typical perpetual properties.

This paper suggests a theory of composable specification of concurrent programs with similar goals as for sequential programs. The specification consists of both terminal and perpetual properties. We devise (1) proof techniques to verify that program code meets a given specification, and (2) composition rules to derive the specification of a program from those of its components. We employ terminal properties of components to derive perpetual properties of a program and conversely. Hence, this proof strategy is called bilateral. The compositional aspect of the theory is important in assembling a program out of components some of whose source code may not be available, as is increasingly the case with cross-vendor program integration.

The Hoare-proof theory for sequential programs is known to be sound and relatively-complete. A sound and relatively-complete proof theory for concurrent programs that use a very limited set of program constructs, known as Unity, appears in Chandy and Misra [2] and Misra [11]. This paper combines both approaches to yield a theory applicable to concurrent programs written in conventional languages. (The soundness and relatively-completeness of this theory has not been proved yet.)

We treat three examples of varying complexity in detail in this paper. First, a program that implements a distributed counter is used to illustrate the various concepts of the theory in stages through out the paper. Appendix B includes a proof of a mutual exclusion program, a system of tightly-coupled components. Unlike traditional proofs, it is based on composing the specifications of the components. Appendix C includes proof of a recursively-defined concurrent program, where code of one component is only implicit, again using composable specifications. We know of no other proof technique that can be used to prove this example program.

2 Program and Execution Model

2.1 Program Structure

The syntax for programs and its components is given below.

[TABLE]

An action has a guard, which is a predicate, and a body which is a piece of code. Execution of the body in a state in which the guard holds is guaranteed to terminate; we assume that this guarantee is independently available. Details of execution semantics is given Section 2.2. A guard that is true is often dropped. An action without a guard is non-blocking and a guarded action blocking.

A structured component is either: (1) a join of the form $f\ [\!\,]\ g$ where $f$ and $g$ are its direct subcomponents, or (2) seq$(f_{0},\ f_{1},\cdots f_{n})$ where the direct subcomponents, $f_{i}$, are combined using some sequential language construct. A join models concurrent execution, as we describe in Section 2.2. And seq denotes any sequential language construct for which proof rules are available. Thus, the typical constructs of sequencing, if-then-else and do-while are seq constructs. A subcomponent of any component is either its direct subcomponent or a subcomponent of some direct subcomponent. Note that a component is never empty.

Join construct is commutative and associative. The syntax permits arbitrary nesting of sequential and concurrency constructs, so, “(f\ [\!\,]\ g)\ \mbox{\boldmath{;}}\ (f^{\prime}\ [\!\,]\ g^{\prime})” is a program with $f,\ f^{\prime},\ g$ and $g^{\prime}$ as components.

A program is a component that is meant to be executed alone.

Access rights to variables

A variable named in a component is accessible to it. Variable $x$ is local to $f$ if $f$ has exclusive write-access to $x$ during any of its executions. Therefore, any accessible variable of a component in a sequential program is local to it. However, a local variable of $f\ [\!\,]\ g$ may not be local to either $f$ or $g$. An accessible non-local variable $x$ of $f$ is shared; $x$ is shared with $g$ if $x$ is also accessible to $g$. Note that $x$ is local to $f$ and shared in $g$ if $f$ has exclusive write-access to $x$ and $g$ can only read $x$.

A program is executed alone, so, all its accessible variables are local to it.

A local predicate of $f$ is a predicate in which every variable is a local variable of $f$. Therefore, true and false are local to all components. It follows that the value of a local predicate of $f$ remains unchanged in any execution as long as $f$ does not take a step.

2.2 Program execution

A step is an instance of the execution of an action. A step of action $b\!\rightarrow\!\alpha$ is executed as follows: evaluate $b$ without preemption and if it is true, immediately execute $\alpha$ to completion, again without preemption —this is called an effective execution of the action— else the program state (and its control point) are unaltered —this is called an ineffective execution. Thus, in an effective execution of $b\!\rightarrow\!\alpha$, $b$ holds when the execution of $\alpha$ begins. Ineffective execution models busy-waiting whereby the action execution is retried at some future moment.

Execution of a join starts simultaneously for all its direct subcomponents, and terminates when they all do. At any moment during the execution, the program control may reside simultaneously in many of its subcomponents. Execution rules for a seq are the traditional ones from sequential programming, which ensures that the program control is within one direct subcomponent at any moment. The subcomponent itself may be a join which may have multiple control points of its own.

Initially the program control is at the entry point of the program. In any given state the program takes a step by choosing a control point before an action and executing, effectively or ineffectively, the action. If there is no such control point, the program has terminated. The choice of control point for a step is arbitrary, but subject to the following fairness constraint: every control point is chosen eventually for execution, so that no component is ignored forever. This is the same constraint advocated by Dijkstra [5] in his classic paper. In contrast to a terminated execution a deadlocked execution attempts executions of certain actions ineffectively forever, and the control resides permanently at the points preceding each of these actions.

An execution is a sequence of steps that can not be extended. Infinite executions do not have an end state. A finite execution either terminates or is deadlocked, and it has an end state. It simplifies the proof theory considerably to imagine that every execution is infinite, by extending each finite execution by an infinite number of stutter steps that repeat the end state forever.

2.3 Example: Distributed counter

We consider an abstraction of a distributed counter protocol in Blumofe [1]. The proof in this paper is based on a proof by Rajeev Joshi and the one given in Chapter 6 of Misra [11].

The protocol $f$ that implements counter $ctr$ is the join of a finite number of threads, $f_{j}$, given below. Each $f_{j}$ has local variables $old_{j}$ and $new_{j}$. Below, each assignment statement and guarded statement is an action. The following form of the if statement was introduced by Dijkstra [4]; in each execution of the statement an alternative whose guard holds is executed without preemption.

[TABLE]

It is required to show that $ctr$ behaves as a counter, that is: (1) $ctr$ never decreases and it increases only by 1, and (2) $ctr$ increases eventually. Both of these are perpetual properties. There is no terminal property of interest since the program never terminates.

3 Introduction to the proof theory

3.1 Specification

A specification of component $f$ is of the form $\{r\}\ f\ \{Q\ \;\,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}}\;\,\ s\}$ where $r$ and $s$ are the pre- and postconditions, and $Q$ is a set of perpetual properties. The meaning of such a specification is as follows. For any execution of $f$ starting in an $r$-state,

if the execution terminates, the end state is an $s$-state, and 2. 2.

every property in $Q$ holds for the execution.

We give proof rules for pre- and postconditions in the following section. Proof rules for perpetual properties appear in subsequent sections, for safety properties in Section 4 and for progress properties in Section 5.

Terminology

Write $\{r\}\ f\ \{s\}$ when $Q$ is irrelevant in the discussion, and $\{r\}\ f\ \{Q\ \;\,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}}\;\,\ \}$ when $s$ is irrelevant. Further for $q\in Q$, write “$q\ \mbox{in}\ f$” when $r$ is understood from the context, and just “$q$” when both $f$ and $r$ are understood. An inference rule without explicit mention of $f$ or $r$ denotes that the rule applies for any $f$ and $r$.

Variables named in properties

A property of component $f$ includes predicates that name accessible variables of $f$, and other variables, called free variables. A property is implicitly universally quantified over its free variables. Any inaccessible variable named in a property denotes a free variable, and, being a bound variable, may be renamed.

3.2 Local Annotation

Local Annotation of component $f$ associates assertions with program points such that each assertion holds whenever program control reaches the associated point in every execution of any program in which $f$ is a component. Thus, a local annotation yields precondition for the execution of each action of $f$, and valid pre- and postcondition of $f$ in any environment. Since the execution environment of $f$ is arbitrary, only the predicates that are local to $f$ are unaffected by executions of other components. Therefore, a local annotation associates predicates local to each point of $f$, as explained below.

Local annotation is defined by the program structure. First, the proof rule for an action is as follows:

\frac{\raisebox{2.0pt}{\normalsize{p\land b}\ \alpha\ {q}}}{\raisebox{-2.0pt}{\normalsize{p}\ b!\rightarrow!\alpha\ {q}}}\\

To construct a local annotation of f=\seq$(f_{0},\ f_{1},\cdots f_{n})$, construct local annotation of each $f_{i}$ using only the local variables of $f_{i}$ as well as those of $f$. Then construct an annotation of $f$ using the proof rules for seq from the sequential program proof theory. Observe that the local variables of $f$ are local to each $f_{i}$ because in a sequential execution among the direct subcomponents of $f$ each $f_{i}$ has exclusive write-access to these variables during its execution.

To construct a local annotation of $f=g\ [\!\,]\ h$, construct local annotations of each of $g$ and $h$ using only their local variables. Then construct an annotation of $f$ using the proof rule given below. Note that the proof rule is valid only because the assertions in $g$ and $h$ are local to those components.

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}{r}\ g\ {s}\ {r^{\prime}}\ h\ {s^{\prime}}\end{array}}}{\raisebox{-2.0pt}{\normalsize{r\land r^{\prime}}\ g\ [!,]\ h\ {s\land s^{\prime}}}}\\

Observe that a local variable of $f$ is not necessarily local to $g$ or $h$ unless they have exclusive write-access to it. Henceforth, all annotations in this paper are local annotations.

A shortcoming of local annotation is that a variable that is local to $f\ [\!\,]\ g$ but shared by both $f$ and $g$ can not appear in a local annotation by the application of these rules alone. The invariance meta-rule, given in Section 3.4, overcomes this problem.

3.3 Example: Distributed Counter, contd.

Construct a local annotation of $f_{j}$ for the example of Section 2.3. Below, we have labeled the actions to refer to them in subsequent proofs.

[TABLE]

3.4 Meta-rules

The following general rules apply for specifications.

• •

(lhs strengthening; rhs weakening)

 \frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}{r}\ f\ {Q\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s}\ r^{\prime}\Rightarrow r,\ s\Rightarrow s^{\prime},\ Q^{\prime}\subseteq Q,\ \ r^{\prime}\ \mbox{and $s^{\prime}$ are local to $f$}\end{array}}}{\raisebox{-2.0pt}{\normalsize{r^{\prime}}\ f\ {Q^{\prime}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s^{\prime}}}}

• •

(Conjunction; Disjunction)

 \frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}{r}\ f\ {Q\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s}\ {r^{\prime}}\ f\ {Q^{\prime}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s^{\prime}}\end{array}}}{\raisebox{-2.0pt}{\normalsize\begin{array}[]{ccc}{r\land r^{\prime}}\ f\ {Q\cup Q^{\prime}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s\land s^{\prime}}\ {r\lor r^{\prime}}\ f\ {Q\cap Q^{\prime}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s\lor s^{\prime}}\end{array}}}

Justifications for the meta-rules

The lhs strengthening and rhs weakening rules are inspired by similar rules for Hoare-triples. Additionally, since the properties in $Q$ are independent, any number of them may be removed.

For the conjunction rule, let the set of executions of $f$ starting in $r$-state be $r$-executions, and, similarly $r^{\prime}$-executions. The $r\land r^{\prime}$-executions is the intersection of $r$-executions and $r^{\prime}$-executions. Therefore, the postcondition of any execution in $r\land r^{\prime}$-executions satisfies $s\land s^{\prime}$ and every property in $Q$ or $Q^{\prime}$, justifying the conjunction rule. The arguments for the disjunction rule are similar.

4 Safety Properties

A safety property is perpetual. We develop a safety property, co, and its special cases, taken from Misra [11]. Safety properties are derived from local annotations and/or safety properties of the subcomponents of a component.

4.1 Safety Property co

Write $p\mbox{\ {\bf co}\ }q$ in component $f$, for predicates $p$ and $q$ that may not be local to $f$, to mean that effective execution of any action of $f$ in a $p$-state establishes a $q$-state. Observe that an ineffective execution preserves $p$. Thus, given $p\mbox{\ {\bf co}\ }q$: (1) in any execution of $f$ once $p$ holds it continues to hold until $q$ is established, though $q$ may never be established, and (2) as a composition rule, $p\mbox{\ {\bf co}\ }q$ holds in component iff it holds in every subcomponent of it.

For an annotated component, co is defined by the following proof rule.

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}{r}\ f\ {s}\ \ \mbox{For every action}\ b!\rightarrow!\alpha\ \mbox{with precondition}\ pre\ \mbox{in the annotation}:\ {pre\land b\land p}\ \alpha\ {q}\end{array}}}{\raisebox{-2.0pt}{\normalsize{r}\ f\ {p\mbox{\ {\bf co}\ }q\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s}}}

As an example, the statement “every change in integer variable $ctr$ can only increment its value” may be formalized as $ctr=m\mbox{\ {\bf co}\ }ctr=m\ \lor\ ctr=m+1$, for all integer $m$.

4.2 Special cases of co

Define special cases of co for component $f$: stable, constant and invariant. Given predicate $p$ and expression $e$, in any execution of $f$: (1) $\mbox{{\bf stable}\ }p$ means that $p$ remains true once it becomes true, (2) $\mbox{{\bf constant}\ }e$ that the value of $e$ never changes, and (3) $\mbox{{\bf invariant}\ }p$ that $p$ is always true, including after termination, if the program terminates. Formally, in $f$

[TABLE]

Observe that invariant true (hence, stable true) and stable false are properties of every component. A variable for which $f$ has no write-access is constant in $f$, and so is any expression constructed out of such variables.

Derived rules for co and some of its special cases, which are heavily used in actual proofs, are given in Appendix A.1. It follows from the derived rules that a safety property of a program is a property of all its components, and conversely, as given by the inheritance rule below.

4.3 Meta-rules

(Inheritance) If any safety property (co or any of its special cases) holds in all subcomponents of $f$ then it holds in $f$. More formally, for safety properties $\sigma$,

Given:  \frac{\raisebox{2.0pt}{\normalsize(\forall i::\ {r_{i}}\ f_{i}\ {s_{i}})}}{\raisebox{-2.0pt}{\normalsize{r}\ f\ {s}}}

Assert: \frac{\raisebox{2.0pt}{\normalsize(\forall i::\ {r_{i}}\ f_{i}\ {\mathit{\sigma}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s_{i}})}}{\raisebox{-2.0pt}{\normalsize{r}\ f\ {\mathit{\sigma}\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s}}} 2. 2.

(Invariance) A local invariant of a component, i.e., a local predicate that is invariant in the component, can be substituted for true, and vice versa, in any predicate in an annotation or property of the component. In particular, for a program all variables are local, so any invariant can be conjoined to an assertion including the postcondition.

Justifications for the meta-rules

Inheritance rule is based on the fact that if a safety property holds for all components of $f$ it holds for $f$ as well. Given the proof rule at left the inheritance proof rule at right can be asserted for any set of safety properties $\mathit{\sigma}$.

The invariance rule is from Chandy and Misra [2] where it is called the “substitution axiom”. One consequence of the rule is that a local invariant of $f\ [\!\,]\ g$, that may not be a local predicate of either $f$ or $g$, could be conjoined to predicates in an annotation of $f\ [\!\,]\ g$. Additionally, all variables in a program are local; so, any invariant can be substituted for true in a program.

4.4 Example: Distributed Counter, contd.

For the example of Section 2.3 we prove that $ctr$ behaves as a counter in that its value can only be incremented, i.e., $ctr=m\mbox{\ {\bf co}\ }ctr=m\lor ctr=m+1$ in $f$. Using the inheritance rule, it is sufficient to prove this property in every component $f_{j}$. In $f_{j}$, only $\beta_{j}$ may change the value of $ctr$; so we need only show the following whose proof is immediate:

[TABLE]

5 Progress Properties

We are mostly interested in progress properties of the form “if predicate $p$ holds at any point during the execution of a component, predicate $q$ holds eventually”. Here “eventually” includes the current and all future moments in the execution. This property, called leads-to, is defined in Section 5.3 (page 5.3). First, we introduce two simpler progress properties, transient and ensures. Transient is a fundamental progress property, the counterpart of the safety property stable. It is introduced because its proof rules are easy to justify and it can be used to define ensures. However, it is rarely used in program specification because ensures is far more useful in practice. Ensures is used to define leads-to.

5.1 Progress Property: transient

In contrast to a stable predicate that remains true once it becomes true, a transient predicate is guaranteed to be falsified eventually. That is, predicate $p$ is transient in component $f$ implies that if $p$ holds at any point during an execution of $f$, $\lnot p$ holds then or eventually in that execution. In temporal logic notation $p$ is transient is written as $\Box\Diamond\lnot p$. Note that $\lnot p$ may not continue to hold after $p$ has been falsified. Predicate false is transient because $\mbox{\em false}\Rightarrow\mbox{\em true}$, and, hence $\lnot\mbox{\em false}$ holds whenever false holds. Note that given $p$ transient in $f$, $\lnot p$ holds at the termination point of $f$ because, otherwise, $f$ can take no further steps to falsify $p$.

The proof rules are given in Figure 1. Below, $\mathit{post_{f}}$ is a local predicate of $f$ that is initially false and becomes true only on the termination of $f$. Such a predicate always exists, say, by encoding the termination control point into it. For a non-terminating program, $\mathit{post_{f}}$ is false. Proof of $\mathit{post_{f}}$ is a safety proof.

Justifications

The formal justification is based on induction on the program structure: show that the basis rule is justified and then inductively prove the remaining rules. We give informal justifications below.

In the basis rule the hypotheses guarantee that each action of $f$ is effectively executed whenever $p$ holds, and that the execution establishes $\lnot p$. If no action can be executed effectively, because precondition of no action holds, the program has terminated and $\mathit{post_{f}}$ holds. Hence, $\lnot p\lor\mathit{post_{f}}$, i.e.$\lnot(p\land\lnot\mathit{post_{f}})$, hold eventually in all cases. Note that if $pre\Rightarrow\lnot p$ then $pre\land p$ is false and the hypotheses are vacuously satisfied. If $f$ never terminates, $\lnot\mathit{post_{f}}$ always holds and $\lnot p$ is guaranteed eventually.

The next two rules, for sequential and concurrent composition, have weaker hypotheses. The sequencing rule is based on an observation about a sequence of actions, $\alpha;\ \beta$. To prove $\mbox{{\bf transient}\ }p$ it is sufficient that $\alpha$ establish $\lnot p$ or that it execute effectively, thus establishing $post_{\alpha}$, and that $\beta$ establish $\lnot p$. The sequencing rule generalizes this observation to components. Being a local predicate, $\mathit{post_{f}}$ can not be falsified by any concurrently executing component, so it holds as long as the control remains at the termination point of $f$.

In the concurrency rule, as a tautology $g$ either establishes $\lnot p$ eventually, thus guaranteeing the desired result, or preserves $p$ forever. In the latter case, $f$ establishes $\lnot p$ since $\mbox{{\bf transient}\ }p$ holds in $f$.

The inheritance rule applies to a program with multiple components. It asserts that if the property holds in each component $f_{i}$ then it holds in program $f$. To see this consider two cases: $f$ is seq or join, and argue by induction on the program structure.

For seq $f$: if $p$ holds at some point before termination of $f$ it is within exactly one direct subcomponent $f_{i}$, or will do so without changing any variable value. For example, if control precedes execution of “ifb  then $f_{0}$ else $f_{1}$” then it will move to a point preceding $f_{0}$ or $f_{1}$ after evaluation of $b$ without changing the state. Note that $f_{i}$ may be a join, so there may be multiple program points within it where control may reside simultaneously, but all controls reside within one direct subcomponent of seq $f$ at any moment. From the hypothesis, that component, and hence, the program establishes $\lnot p$ eventually.

For a join, say $f\ [\!\,]\ g$: Consider an execution in which, say, $f$ has not terminated when $p$ holds. From the arguments for the concurrency rule, using that $\mbox{{\bf transient}\ }p$ in $f$, eventually $\lnot p$ is established in that execution. Similar remarks apply for all executions in which $g$ has not terminated. And, if both $f$ and $g$ have terminated, then $\lnot p$ holds from the definition of transient  for each component. $\Box$

Notes

The basis rule by itself is sufficient to define an elementary form of transient. However, the transient predicate then has to be extremely elaborate, typically encoding control point of the program, so that it is falsified by every action of the component. The other rules permit simpler predicates to be proven transient. 2. 2.

Basis rule is the only rule that needs program code for its application, others are derived from properties of the components, and hence, permit specification composition. 3. 3.

It is possible that $p$ is eventually falsified in every execution of a component though there is no proof for $\mbox{{\bf transient}\ }p$. To see this consider the program $f\ [\!\,]\ g$ in which every action of $f$ falsifies $p$ only if for some predicate $q$, $p\land q$ holds as a precondition, and every action of $g$ falsifies $p$ only if $p\land\lnot q$ holds as a precondition, and neither component modifies $q$. Clearly, $p$ will be falsified eventually, but this fact can not be proved as a transient property; only $p\land q$ and $p\land\lnot q$ can be shown transient. As we show later, $p\ \mbox{\em leads-to}\ \lnot p$.

5.2 Progress Property: ensures

Property ensures for component $f$, written as $p\mbox{\ {\bf en}\ }q$ with predicates $p$ and $q$, says that if $p$ holds at any moment in an execution of $f$ then it continues to hold until $q$ holds, and $q$ holds eventually. This claim applies even if $p$ holds after the termination of $f$. For initial state predicate $r$, it is written formally as $\{r\}\ f\ \{p\mbox{\ {\bf en}\ }q\ \;\,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}}\;\,\ \}$ and defined as follows:

\displaystyle\frac{\begin{array}[]{@{}c@{}}\{r\}\ f\ \{p\land\lnot q\ \mbox{\ {\bf co}\ }\ p\lor q,\ \mbox{{\bf transient}\ }p\land\lnot q\ \;\,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}}\;\,\ \}\end{array}}{\begin{array}[]{@{}c@{}}\{r\}\ f\ \{p\mbox{\ {\bf en}\ }q\ \;\,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}}\;\,\ \}\end{array}}

We see from the safety property in the hypothesis that once $p$ holds it continues until $q$ holds, and from the transient property that eventually $q$ holds.

Corresponding to each proof rule for transient, there is a similar rule for ensures. These rules and additional derived rules for en are given in Appendix A.3 (page A.3).

Example: Distributed counter, contd.

We prove a progress property of the annotated program from Section 3.3, reproduced below.

[TABLE]

Our ultimate goal is to prove that for any integer $m$ if $ctr=m$ at some point during an execution of $f$, eventually $ctr>m$. To this end let auxiliary variable $nb$ be the number of threads $f_{j}$ for which $ctr\neq old_{j}$. We prove the following ensures property, (E), that says that every step of $f$ either increases $ctr$ or decreases $nb$ while preserving $ctr$’s value. Proof uses the inheritance rule from Appendix A.3 (page A.3). For every $f_{j}$ and any $m$ and $N$:

[TABLE]

We use the rules for en given in Appendix A.3 (page A.3). First, to prove (E) in $g;\ h$, for any $g$ and $h$, it is sufficient to show that $g$ terminates and (E) in $h$. Hence, it is sufficient to show that (E) holds only for the loop in $f_{j}$, because initialization always terminates. Next, using the inheritance rule, it is sufficient to show that (E) holds only for the body of the loop in $f_{j}$. Further, since $\alpha_{j}$ always terminates, (E) needs to be shown only for the if statement. Using inheritance, prove (E) for $\beta_{j}$ and $\gamma_{j}$. In each case, assume the precondition $ctr=m\land nb=N$ of if and the preconditions of $\beta_{j}$ and $\gamma_{j}$. The postcondition $ctr=m\land nb<N\lor ctr>m$ is easy to see in each of the following cases:

[TABLE]

5.3 Progress Property: Leads-to

The informal meaning of $p\ {\boldmath\mapsto}\ q$ (read: $p$ leads-to $q$) is “if $p$ holds at any point during an execution, $q$ holds eventually”. Unlike en, $p$ is not required to hold until $q$ holds.

Leads-to is defined by the following three rules, taken from Chandy and Misra [2]. The rules are easy to justify intuitively.

• •

(basis) \frac{\raisebox{2.0pt}{\normalsizep\ \mbox{\ {\bf en}\ }\ q}}{\raisebox{-2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q}}

• •

(transitivity) \frac{\raisebox{2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q\ ,\ q\ \ {\boldmath\mapsto}\ \ r}}{\raisebox{-2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ r}}

• •

(disjunction) For any (finite or infinite) set of predicates S\

\frac{\raisebox{2.0pt}{\normalsize(\forall p:\ p\in S:\ p\ \ {\boldmath\mapsto}\ \ q)}}{\raisebox{-2.0pt}{\normalsize(\lor p:\ p\in S:\ p)\ \ {\boldmath\mapsto}\ \ q}}

Derived rules for \ {\boldmath\mapsto}\ are given in Appendix A.4 (page A.4). leads-to is not conjunctive, nor does it obey the inheritance rule, so even if $p\ {\boldmath\mapsto}\ q$ holds in both $f$ and $g$ it may not hold in $f\ [\!\,]\ g$.

Example: Distributed counter, contd.

We show that for the example of Section 2.3 the counter $ctr$ increases without bound. The proof is actually quite simple. We use the induction rule for leads-to given in Appendix Section A.4.2.

The goal is to show that for any integer $C$, $\mbox{\em true}\ {\boldmath\mapsto}\ ctr>C$. Below, all properties are in $f$.

[TABLE]

6 Related Work

The earliest proof method for concurrent programs appears in Owicki and Gries [13]. The method works well for small programs, but does not scale up for large ones. Further it is limited to proving safety properties only. There is no notion of component specification and their composition. Lamport [10] first identified leads-to for concurrent programs as the appropriate generalization of termination for sequential programs (“progress” is called liveness in that paper). Owicki and Lamport [14] is a pioneering paper.

The first method to suggest proof rules in the style of Hoare [7], and thus a specification technique, is due to Jones [8, 9]. Each component is annotated assuming that its environment preserves certain predicates. Then the assumptions are discharged using the annotations of the various components. The method though is restricted to safety properties only. A similar technique for message communicating programs was proposed in Misra and Chandy [12].

The approaches above are all based on specifying allowed interface behaviors using compositional temporal logics. Since 2000, a number of proposals[6, 3] have instead used traditional Hoare triples and resource/object invariants, but extending state predicates to include permissions describing how locations can be used, and suitably generalizing the Hoare rule for disjoint parallel composition. However, these proposals typically address only global safety and local termination properties, not global progress properties (as this paper does).

A completely different approach is suggested in the UNITY theory of Chandy and Misra [2], and extended in Misra [11]. A restricted language for describing programs is prescribed. There is no notion of associating assertions with program points. Instead, the safety and progress specification of each component is given by a set of properties that are proved directly. The specifications of components of a program can be composed to derive program properties. The current paper extends this approach by removing the syntactic constraints on programs, though the safety and progress properties of UNITY are the ones used in this paper.

One of the essential questions in these proof methods is to propose the appropriate preconditions for actions. In Owicki and Gries [13] theory it is postulated and proved. In UNITY the programmer supplies the preconditions, which are often easily available for event-driven systems. Here, we derive preconditions that remain valid in any environment; so there can be no assertion about shared variables. The theory separates local precondition (obtained through annotation) from global properties that may mention shared variables.

The proof strategy described in the paper is bilateral in the following sense. An invariant, a perpetual property, may be used to strengthen a postcondition, a terminal property, using the invariance rule. Conversely, a terminal property, postcondition $post_{f}$ of $f$, may be employed to deduce a transient predicate, a perpetual property.

Separation logic [16] has been effective in reasonong about concurrently accessed data structures. We are studying its relationship to the work described here.

Acknowledgment

I am truly grateful to Ernie Cohen of Amazon and José Meseguer of the Univ. of Illinois at Urbana, for reading the manuscript thoroughly and several times, endless discussions and substantive comments that have shaped the paper. Presenting this work at the IFIPS Working Group 2.3 and the Programming Languages lunch at the University of Texas at Austin has sharpened my understanding; I am grateful to the students and the other attendees, in particular to Dhananjay Raju.

Appendix A Appendix: Derived Rules

A.1 Derived Rules for co and its special

cases

The derived rules for co are given in Figure 2 and for the special cases in Figure 3. The rules are easy to derive; see Chapter 5 of Misra [11].

The top two rules in Figure 2 are simple properties of Hoare triples. The conjunction and disjunction rules follow from the conjunctivity, disjunctivity and monotonicity properties of the weakest precondition, see Dijkstra [4] and of logical implication. These rules generalize in the obvious manner to any set —finite or infinite— of co-properties, because weakest precondition and logical implication are universally conjunctive and disjunctive.

The following rules for the special cases are easy to derive from the definition of stable , invariant  and constant . Special Cases of co

A.2 Derived Rules for transient

• •

transient false.

• •

(Strengthening) Given $\mbox{{\bf transient}\ }p$, $\mbox{{\bf transient}\ }p\land q$ for any $q$.

To prove transient false use the basis rule. The proof of the strengthening rule uses induction on the number of applications of the proof rules in deriving $\mbox{{\bf transient}\ }p$. The proof is a template for proofs of many derived rules for ensures and leads-to. Consider the different ways by which $\mbox{{\bf transient}\ }p$ can be proved in a component. Basis rule gives the base case of induction.

(Basis) In component $f$, $p$ is of the form $p^{\prime}\land\lnot\mathit{post_{f}}$ for some $p^{\prime}$. Then in some annotation of $f$ where action $b\!\rightarrow\!\alpha$ has the precondition $pre$:

(1) $pre\land p^{\prime}\ \Rightarrow\ b$, and (2) $\{pre\land p^{\prime}\}\ \alpha\ \{\lnot p^{\prime}\}$.

(1’) From predicate calculus $pre\land p^{\prime}\land q\ \Rightarrow\ b$, and

(2’) from Hoare logic $\{pre\land p^{\prime}\land q\}\ \alpha\ \{\lnot p^{\prime}\}$. Applying the basis rule, $\mbox{{\bf transient}\ }p^{\prime}\land q\land\lnot\mathit{post_{f}}$, i.e., $\mbox{{\bf transient}\ }p\land q$. 2. 2.

(Sequencing) In f\ \mbox{\boldmath{;}}\ g, $\mbox{{\bf transient}\ }p\land\lnot\mathit{post_{f}}$ in $f$ and $\mbox{{\bf transient}\ }p$ in $g$. Inductively, $\mbox{{\bf transient}\ }p\land q\land\lnot\mathit{post_{f}}$ in $f$ and $\mbox{{\bf transient}\ }p\land q$ in $g$. Applying the sequencing rule, $\mbox{{\bf transient}\ }p\land q$. 3. 3.

(Concurrency, Inheritance) Similar proofs.

A.3 Derived Rules for en

A.3.1 Counterparts of rules for transient

This set of derived rules correspond to the similar rules for transient. Their proofs are straight-forward using the definition of en.

• •

(Basis)

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}{r}\ f\ {s}\ \ \mbox{For every action}\ b!\rightarrow!\alpha\ \mbox{with precondition}\ pre\ \mbox{in the annotation}:\ pre\land p\land\lnot q\ \Rightarrow\ b\ {pre\land p\land\lnot q}\ \alpha\ {q}\end{array}}}{\raisebox{-2.0pt}{\normalsize{r}\ f\ {p\mbox{\ {\bf en}\ }p\land s\lor q\ ;,{\mbox{\rule[-2.27621pt]{1.0812pt}{10.243pt}}};,\ s}}}

• •

(Sequencing)

[TABLE]

• •

(Concurrency)

[TABLE]

• •

(Inheritance) Assuming the proof rule at left the inheritance proof rule at right can be asserted.

[TABLE]

A.3.2 Additional derived rules

The following rules are easy to verify by expanding each ensures property by its definition, and using the derived rules for transient and co. We show one such proof, for the PSP rule. Observe that ensures is only partially conjunctive and not disjunctive, unlike co.

(implication)  \frac{\raisebox{2.0pt}{\normalsizep\Rightarrow q}}{\raisebox{-2.0pt}{\normalsizep\mbox{\ {\bf en}\ }q}}

Consequently, $\mbox{\em false}\mbox{\ {\bf en}\ }q$ and $p\mbox{\ {\bf en}\ }\mbox{\em true}$ for any $p$ and $q$. 2. 2.

(rhs weakening)   \frac{\raisebox{2.0pt}{\normalsizep\ \mbox{\ {\bf en}\ }\ q}}{\raisebox{-2.0pt}{\normalsizep\ \mbox{\ {\bf en}\ }\ q\lor q^{\prime}}} 3. 3.

(partial conjunction)  \frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{lll}p\ \mbox{\ {\bf en}\ }\ q\ p^{\prime}\ \mbox{\ {\bf en}\ }\ q\end{array}}}{\raisebox{-2.0pt}{\normalsizep\land p^{\prime}\ \mbox{\ {\bf en}\ }\ q}} 4. 4.

(lhs manipulation)   \frac{\raisebox{2.0pt}{\normalsizep\land\lnot q\ \Rightarrow\ p^{\prime}\ \Rightarrow\ p\lor q}}{\raisebox{-2.0pt}{\normalsizep\ \mbox{\ {\bf en}\ }\ q\ \equiv\ p^{\prime}\ \mbox{\ {\bf en}\ }\ q}}

Observe that $p\land\lnot q\ \equiv\ p^{\prime}\land\lnot q$ and $p\lor q\ \equiv\ p^{\prime}\lor q$. So, $p$ and $q$ are interchangeable in all the proof rules. As special cases, $p\land\lnot q\ \mbox{\ {\bf en}\ }\ q\ \equiv\ p\ \mbox{\ {\bf en}\ }\ q\equiv\ p\lor q\ \mbox{\ {\bf en}\ }\ q$. 5. 5.

(PSP) The general rule is at left, and a special case at right using $\mbox{{\bf stable}\ }r$ as $r\mbox{\ {\bf co}\ }r$.

[TABLE] 6. 6.

(Special case of Concurrency)

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}p\mbox{\ {\bf en}\ }q\ \mbox{in}\ f\ \mbox{{\bf stable}\ }p\ \mbox{in}\ g\end{array}}}{\raisebox{-2.0pt}{\normalsizep\mbox{\ {\bf en}\ }q\ \mbox{in}\ f\ [!,]\ g}} $\Box$

Proof of (PSP): From the hypotheses:

[TABLE]

We have to show:

[TABLE]

First, simplify the term on the rhs of (4) and lhs of (5) to $p\land r\land\lnot q\land s$. Proof of (4) is then immediate, as a strengthening of (1). For the proof of (5), apply conjunction to (2) and (3) to get:

[TABLE]

A.4 Derived Rules for leads-to

The rules are taken from Misra [11] where the proofs are given. The rules are divided into two classes, lightweight and heavyweight. The former includes rules whose validity are easily established; the latter rules are not entirely obvious. Each application of a heavyweight rule goes a long way toward completing a progress proof.

A.4.1 Lightweight rules

(implication) \frac{\raisebox{2.0pt}{\normalsizep\ \Rightarrow\ q}}{\raisebox{-2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q}} 2. 2.

(lhs strengthening, rhs weakening)

 \frac{\raisebox{2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q}}{\raisebox{-2.0pt}{\normalsize\begin{array}[]{lll}p^{\prime}\land p\ \ {\boldmath\mapsto}\ \ q\ p\ \ {\boldmath\mapsto}\ \ q\lor q^{\prime}\end{array}}} 3. 3.

(disjunction) \frac{\raisebox{2.0pt}{\normalsize(\forall i::\ p_{i}\ \ {\boldmath\mapsto}\ \ q_{i})}}{\raisebox{-2.0pt}{\normalsize(\forall i::\ p_{i})\ \ {\boldmath\mapsto}\ \ (\forall i::\ q_{i})}}

where $i$ is quantified over an arbitrary finite or infinite index set, and $p_{i},q_{i}$ are predicates. 4. 4.

(cancellation) \frac{\raisebox{2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q\lor r\ ,\ r\ \ {\boldmath\mapsto}\ \ s}}{\raisebox{-2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ q\lor s}}

A.4.2 Heavyweight rules

(impossibility) \frac{\raisebox{2.0pt}{\normalsizep\ \ {\boldmath\mapsto}\ \ \mbox{\em false}}}{\raisebox{-2.0pt}{\normalsize\lnot p}} 2. 2.

(PSP) The general rule is at left, and a special case at right using $\mbox{{\bf stable}\ }r$ as $r\mbox{\ {\bf co}\ }r$.

[TABLE] 3. 3.

(induction) Let $M$ be a total function from program states to a well-founded set ($W,\prec$). Variable $m$ in the following premise ranges over $W$. Predicates $p$ and $q$ do not contain free occurrences of variable $m$.

[TABLE] 4. 4.

(completion) Let $p_{i}$ and $q_{i}$ be predicates where $i$ ranges over a finite set.

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{lll}(\forall i::\ \quad p_{i}\ \ {\boldmath\mapsto}\ \ q_{i}\lor b\ \quad q_{i}\ \mbox{\ {\bf co}\ }\ q_{i}\lor b\ )\end{array}}}{\raisebox{-2.0pt}{\normalsize(\forall i::\ p_{i})\ \ {\boldmath\mapsto}\ \ (\forall i::\ q_{i})\ \lor\ b}}

A.4.3 Lifting Rule

This rule permits lifting a leads-to property of $f$ to $f\ [\!\,]\ g$ with some modifications. Let $x$ be a tuple of some accessible variables of $f$ that includes all variables that $f$ shares with $g$. Below, $X$ is a free variable, therefore universally quantified. Predicates $p$ and $q$ name accessible variables of $f$ and $g$. Clearly, any local variable of $g$ named in $p$ or $q$ is treated as a constant in $f$.

(L)

\frac{\raisebox{2.0pt}{\normalsize\begin{array}[]{ccc}p\ {\boldmath\mapsto}\ q\ \mbox{in}\ f\ r\land x=X\mbox{\ {\bf co}\ }x=X\lor\lnot r\ \mbox{in}\ g\end{array}}}{\raisebox{-2.0pt}{\normalsizep\ {\boldmath\mapsto}\ q\lor\lnot r\ \mbox{in}\ f\ [!,]\ g}}\\

An informal justification of this rule is as follows. Any $p$-state in which $\lnot r$ holds, $q\lor\lnot r$ holds. We show that in any execution of $f\ [\!\,]\ g$ starting in a $(p\land r)$-state $q$ or $\lnot r$ holds eventually. If $r$ is falsified by a step of $f$ then $\lnot r$ holds. Therefore, assume that every step of $f$ preserves $r$. Now if any step of $g$ changes the value of $x$ then it falsifies $r$ from the antecedent, i.e., $\lnot r$ holds. So, assume that no step of $g$ modifies $x$. Then $g$ does not modify any accessible variable of $f$; so, $f$ is oblivious to the presence of $g$, and it establishes $q$.

As a special case, we can show

(L’)

\frac{\raisebox{2.0pt}{\normalsizep\ {\boldmath\mapsto}\ q\ \mbox{in}\ f}}{\raisebox{-2.0pt}{\normalsizep\land x=M\ {\boldmath\mapsto}\ q\lor x\neq M\ \mbox{in}\ f\ [!,]\ g}}\\

The formal proof of (L) is by induction on the structure of the proof of $p\ {\boldmath\mapsto}\ q\ \mbox{in}\ f$. See

http://www.cs.utexas.edu/users/psp/unity/notes/UnionLiftingRule.pdf

for details.

Appendix B Example: Mutual exclusion

We prove a coarse-grained version of a 2-process mutual exclusion program due to Peterson [15]. The given program has a finite number of states, so it is amenable to model-checking. In fact, model-checking is a simpler alternative to an axiomatic proof. We consider this example primarily because this is an instance of a tightly-coupled system where the codes of all the components are typically considered together to construct a proof. In contrast, we construct a composable specification of each component and combine the specifications to derive a proof.

B.1 Program

The program has two processes $M$ and $M^{\prime}$. Process $M$ has two local boolean variables, $try$ and $cs$ where $try$ remains true as long as $M$ is attempting to enter the critical section or in it and $cs$ is true as long as it is in the critical section; $M^{\prime}$ has $try^{\prime}$ and $cs^{\prime}$. They both have access to a shared boolean variable $turn$. It simplifies coding and proof to postulate an additional boolean variable $turn^{\prime}$ that is the complement of $turn$, i.e., $turn^{\prime}\equiv\lnot turn$.

The global initialization and the code for $M$, along with a local annotation, is given below. The code of $M^{\prime}$ is the dual of $M$, obtained by replacing each variable in $M$ by its primed counterpart. Henceforth, the primed and the unprimed versions of the same variable re duals of each other.

The “unrelated computation” below refers to computation preceding the attempt to enter the critical section that does not access any of the relevant variables. This computation may or may not terminate in any iteration.

[TABLE]

Given that $M^{\prime}$ is the dual of $M$, from any property of $M$ obtain its dual as a property of $M^{\prime}$. And, for any property of $M\ [\!\,]\ M^{\prime}$ its dual is a property of $M^{\prime}\ [\!\,]\ M$, i.e., $M\ [\!\,]\ M^{\prime}$, thus reducing the proof length by around half.

Remarks on the program

The given program is based on a simplification of an algorithm in Peterson [15]. In the original version the assignment in $\alpha$ may be decoupled to the sequence $try:=\mbox{\em true};\ turn:=\mbox{\em true}$. The tests in $\beta$ may be made separately for each disjunct in arbitrary order. Action $\gamma$ may be written in sequential order $try:=\mbox{\em false};\ cs:=\mbox{\em false}$. These changes can be easily accommodated within our proof theory by introducing auxiliary variables to record the program control.

B.2 Safety and progress properties

It is required to show in $M\ [\!\,]\ M^{\prime}$ (1) the safety property: both $M$ and $M^{\prime}$ are never simultaneously within their critical sections, i.e., $\mbox{{\bf invariant}\ }\lnot(cs\land cs^{\prime})$, and (2) the progress property: any process attempting to enter its critical section will succeed eventually, i.e., $try\ {\boldmath\mapsto}\ cs$ and $try^{\prime}\ {\boldmath\mapsto}\ cs^{\prime}$; we prove just $try\ {\boldmath\mapsto}\ cs$ since its dual also holds.

B.2.1 Safety proof: $\mbox{{\bf invariant}\ }\lnot(cs\land cs^{\prime})$

We prove below:

[TABLE]

Mutual exclusion is immediate from (S1) and (S2), as follows.

[TABLE]

Proofs of (S1) and (S2)

First, we show the following stable properties of $M$, which constitute its safety specification, from which (S1) and (S2) follow.

[TABLE]

The proofs of (S3), (S4) and (S5) are entirely straight-forward, but each property has to be shown stable for each action. We show the proofs in Table 1, where each row refers to one of the predicates in (S3 – S5) and each column to an action. An entry in the table is either: (1) “post: $p$” claiming that since $p$ is a postcondition of this action the given predicate is stable, or (2) “unaff.” meaning that the variables in the given predicate are unaffected by this action execution. The only entry that is left out is for the case that $\beta$ preserves (S5): $cs\land try^{\prime}\Rightarrow turn^{\prime}$; this is shown as follows. The guard of $\beta$ can be written as $try^{\prime}\Rightarrow turn^{\prime}$ and execution of $\beta$ affects neither $try^{\prime}$ nor $turn^{\prime}$, so $try^{\prime}\Rightarrow turn^{\prime}$ is a postcondition, and so is $cs\land try^{\prime}\Rightarrow turn^{\prime}$.

Now we are ready to prove (S1) and (S2). The predicates in (S1) and (S2) hold initially because $\mbox{{\bf initially}\ }cs,cs^{\prime}=\mbox{\em false},\mbox{\em false}$. Next, we show these predicates to be stable. The proof is compositional, by proving each predicate to be stable in both $M$ and $M^{\prime}$. The proof is simplified by duality of the codes.

$\bullet$ (S1) $\mbox{{\bf stable}\ }cs\Rightarrow try$ in $M\ [\!\,]\ M^{\prime}$:

[TABLE]

$\bullet$ (S2) $\mbox{{\bf stable}\ }cs^{\prime}\land try\Rightarrow turn$ in $M\ [\!\,]\ M^{\prime}$:

[TABLE]

B.2.2 Progress proof: $try\ {\boldmath\mapsto}\ cs$ in $M\ [\!\,]\ M^{\prime}$

First, we prove a safety property:

[TABLE]

To prove (S6) first prove $try\land\lnot cs\mbox{\ {\bf co}\ }try\lor cs$ in $M$, which is entirely straight-forward. Now variables $try$ and $cs$ are local to $M$, therefore $\mbox{{\bf stable}\ }try\land\lnot cs$ in $M^{\prime}$, and through rhs weakening, $try\land\lnot cs\mbox{\ {\bf co}\ }try\lor cs$ in $M^{\prime}$. Using inheritance (S6) follows. $\Box$

Next we prove a progress property:

[TABLE]

First, prove $try\land(\lnot try^{\prime}\lor turn^{\prime})\mbox{\ {\bf en}\ }\lnot try$ in $M$, using the sequencing rule for  en ; intuitively, in a $try\land(\lnot try^{\prime}\lor turn^{\prime})$-state the program control is never at $\alpha$, execution of $\beta$ terminates while preserving $try\land(\lnot try^{\prime}\lor turn^{\prime})$, and execution of $\gamma$ establishes $\lnot try$.

Using duality on (S4) get $\mbox{{\bf stable}\ }try^{\prime}\Rightarrow turn^{\prime}$ in $M^{\prime}$, i.e., $\mbox{{\bf stable}\ }\lnot try^{\prime}\lor turn^{\prime}$ in $M^{\prime}$. And $try$ is local to $M$, so $\mbox{{\bf stable}\ }try$ in $M^{\prime}$. Conjoining these two properties, $\mbox{{\bf stable}\ }try\land(\lnot try^{\prime}\lor turn^{\prime})$ in $M^{\prime}$. Apply the concurrency rule for  en  with $\mbox{{\bf stable}\ }try\land(\lnot try^{\prime}\lor turn^{\prime})$ in $M^{\prime}$ and $try\land(\lnot try^{\prime}\lor turn^{\prime})\mbox{\ {\bf en}\ }\lnot try$ in $M$ to conclude that $try\land(\lnot try^{\prime}\lor turn^{\prime})\ \mbox{\ {\bf en}\ }\ \lnot try$ in $M\ [\!\,]\ M^{\prime}$.

Now apply the basis rule for \ {\boldmath\mapsto}\ to conclude the proof of (P). $\Box$

Proof of $try\ {\boldmath\mapsto}\ cs$ in $M\ [\!\,]\ M^{\prime}$:

All the properties below are in $M\ [\!\,]\ M^{\prime}$.

Conclude from (P), using lhs strengthening,

[TABLE]

The main proof:

[TABLE]

Appendix C Example: Associative, Commutative fold

We consider a recursively defined program $f$ where the code of $f_{1}$ is given and $f_{k+1}$ is defined to be $f_{1}\ [\!\,]\ f_{k}$. This structure dictates that the specification $s_{k}$ of $f_{k}$ must permit proof of (1) $s_{1}$ from the code of $f_{1}$, and (2) $s_{k+1}$ from $s_{1}$ and $s_{k}$, using induction on $k$. This example illustrates the usefulness of the various composition rules for the perpetual properties. The program is not easy to understand intuitively; it does need a formal proof.

C.1 Informal Problem Description

Given is a bag $u$ on which $\oplus$ is a commutative and associative binary operation. Define $\Sigma u$, fold of $u$, to be the result of applying $\oplus$ repeatedly to all pairs of elements of $u$ until there is a single element. It is required to replace all the elements of $u$ by $\Sigma u$. Program $f_{k}$, for $k\geq 1$, decreases the size of $u$ by $k$ while preserving its fold. That is, $f_{k}$ transforms the original bag $u^{\prime}$ to $u$ such that: (1) $\Sigma u=\Sigma u^{\prime}$, and (2) $|u|+k=|u^{\prime}|$, provided $|u^{\prime}|>k$, where $|u|$ is the size of $u$. Therefore, execution of $f_{n-1}$, where $n$ is the size of $u^{\prime}$ and $n>1$, computes a single value in $u$ that is the fold of the initial bag.

Below, $get(x)$ removes an item from $u$ and assigns its value to variable $x$. This operation can be completed only if $u$ has an item. And $put(x\oplus y)$, a non-blocking action, stores $x\oplus y$ in $u$. The formal semantics of $get$ and $put$ are given by the following assertions where $u^{\prime}$ is constant:

[TABLE]

The fold program $f_{k}$ for all $k$, $k\geq 1$, is given by:

[TABLE]

Specification and proof of safety properties appear in Section C.2, next, and progress properties in Section C.3. Observe that

C.2 Terminal property

The relevant safety property of $f_{k}$, for all $k$, $k\geq 1$, is a terminal property:

[TABLE]

This property can not be proved from a local annotation alone because it names the shared variable $u$ in its pre- and postconditions. We suggest an enhanced safety property using certain auxiliary variables.

Auxiliary variables

The following auxiliary variables of $f_{k}$ are local to it:

$w_{k}$: the bag of items removed from $u$ that are, as yet, unfolded. That is, every $get$ from $u$ puts a copy of the item in $w_{k}$, and $put(x\oplus y)$ removes $x$ and $y$ from $w_{k}$. Initially $w_{k}=\{\}$. 2. 2.

$nh_{k}$: the number of halted threads where a thread halts after completing a $put$. A $get$ does not affect $nh_{k}$ and a $put$ increments it. Initially $nh_{k}=0$.

Introduction of any auxiliary variable $aux_{k}$ for $f_{k}$ follows a pattern: (1) specify the initial value of $aux_{k}$, (2) define $aux_{1}$ by modifying the code of $f_{1}$, corresponding to the basis of a recursive definition, and (3) define $aux_{k+1}$ in terms of $aux_{1}$ and $aux_{k}$.

We adopt this pattern for defining $w_{k}$ and $nh_{k}$ for all $k$, $k\geq 1$. First, the initial values of $w_{k}$ and $nh_{k}$ are $\{\}$ and [math], respectively. Second, $w_{1}$ and $nh_{1}$ are defined below in $f_{1}$. Third, $w_{k+1}=w_{1}\cup w_{k}$ and $nh_{k+1}=nh_{1}+nh_{k}$, for all $k$. The modified program for $f_{1}$ is as follows where $\langle\cdots\rangle$ is an action.

[TABLE]

Note: The definition of auxiliary variables is problematic for $nh_{2}$, for instance; by definition, $nh_{2}=nh_{1}+nh_{1}$. However, these are two different instances of $nh_{1}$ referring to the local variables of the two instances of $f_{1}$ in $f_{2}$. This is not a problem in the forthcoming proofs because the proofs always refer to indices $1$, $k$ and $k+1$, and, $nh_{k}$ is treated as being different from $nh_{1}$.

Specification of safety property

The safety specification of $f_{k}$, for all $k$, $k\geq 1$, is given by:

[TABLE]

$\bullet$ Proof of (S) for $f_{1}$: Construct the following local annotation of $f_{1}$.

[TABLE]

The perpetual and terminal properties of $f_{1}$ in (S) are easily shown using this annotation and employing the semantics of $get$ and $put$.

$\bullet$ Proof of (S) for $f_{k+1}$: by induction on $k$. Use the following abbreviations in the proof.

[TABLE]

[TABLE]

The terminal property $\{u=u^{\prime}\}\ f_{k}\ \{\Sigma u=\Sigma u^{\prime},\ |u|+k=|u^{\prime}|\}$ follows from (S) as follows. The initial values of $\Sigma(u\cup w_{k})$ and $|u|+|w_{k}|+nh_{k}$ are, respectively, $\Sigma u^{\prime}$ and $|u^{\prime}|$, so deduce that $\mbox{{\bf invariant}\ }\Sigma(u\cup w_{k})=\Sigma u^{\prime}$ and also $\mbox{{\bf invariant}\ }|u|+|w_{k}|+nh_{k}=|u^{\prime}|$. Given that $f_{k}$ is a program whose terminal properties are being proved, we may apply the invariance rule of Section 4.3 with these invariants. So, deduce $\Sigma u=\Sigma u^{\prime},\ |u|+k=|u^{\prime}|$ as a postcondition of $f_{k}$ with the given precondition.

C.3 Specification and proof of progress property

The relevant progress property is that if $u$ has more than $k$ elements initially, $f_{k}$ terminates eventually. That is, $|u^{\prime}|>k\ {\boldmath\mapsto}\ nh_{k}=k$ in $f_{k}$. Initially $|u^{\prime}|=|u|+|w_{k}|+nh_{k}$, so it is enough to prove $|u|+|w_{k}|+nh_{k}>k\ {\boldmath\mapsto}\ nh_{k}=k$. Abbreviate $|u|+|w_{k}|+nh_{k}>k$ by $p_{k}$ and $nh_{k}=k$ by $q_{k}$ so that for all $k$, $k\geq 1$, the required progress property is:

[TABLE]

The proof of (P) is by induction on $k$, as shown in Sections C.3.1 and  C.3.2.

C.3.1 Progress proof, $p_{1}\ {\boldmath\mapsto}\ q_{1}$ in

$f_{1}$

We show that $p_{1}\mbox{\ {\bf en}\ }q_{1}$, from which $p_{1}\ {\boldmath\mapsto}\ q_{1}$ follows by applying the basis rule of leads-to. We reproduce the annotation of $f_{1}$ for easy reference.

[TABLE]

Next, prove $p_{1}\mbox{\ {\bf en}\ }q_{1}$ using the sequencing rule of en, from Section A.3.1. It amounts to showing that if $p_{1}$ holds before any action then the action is effectively executed and $q_{1}$ holds on completion of $f_{1}$. As shown in Section C.2 $p_{1}$ is stable, and from the annotation $q_{1}$ holds on completion of $f_{1}$. Therefore, it suffices to show that if $p_{1}$ holds initially then every action is effectively executed. The $put$ action is always effectively executed. Using the given annotation, the verification conditions for the two $get$ actions are shown below in full:

[TABLE]

These are easily proved.

C.3.2 Progress proof, $p_{k+1}\ {\boldmath\mapsto}\ q_{k+1}$ in $f_{k+1}$

The main part of the proof uses the observation that every action, $put$ and $get$, reduces a well-founded metric. The metric is the pair $(|u|+|w_{k}|,|u|)$ and the order relation is lexicographic. Clearly, the metric is bounded from below because each set size is at least [math]. The crux of the proof is to show that if program $f_{k}$ is not terminated there is some action that can be executed, i.e., there is no deadlock. Henceforth, abbreviate $(|u|+|w_{k}|,|u|)$ by $z_{k}$ and any pair of non-negative integers by $n$.

First, observe that $z_{k}$ can only decrease or remain the same in $f_{k}$, that is, $\mbox{{\bf stable}\ }z_{k}\preceq n$ in $f_{k}$, where $\preceq$ is the lexicographic ordering. The proof is by induction on $k$ and it follows the same pattern as all other safety proofs. In $f_{1}$, informally, every effective $get$ preserves $|u|+|w_{1}|$ and decreases $|u|$, and a $put$ decreases $|u|+|w_{1}|$. For the proof in $f_{k+1}$: from above, $\mbox{{\bf stable}\ }z_{1}\preceq n$ in $f_{1}$, and inductively $\mbox{{\bf stable}\ }z_{k}\preceq n$ in $f_{k}$. Since $\mbox{{\bf constant}\ }w_{k}$ in $f_{1}$ and $\mbox{{\bf constant}\ }w_{1}$ in $f_{k}$, $\mbox{{\bf stable}\ }z_{k+1}\preceq n$ in both $f_{1}$ and $f_{k}$. Apply the inheritance rule to conclude that $\mbox{{\bf stable}\ }z_{k+1}\preceq n$ in $f_{k+1}$.

The progress proof of $p_{k+1}\ {\boldmath\mapsto}\ q_{k+1}$ in $f_{k+1}$ is based on two simpler progress results, (P1) and (P2). (P1) says that any execution starting from $p_{k+1}$ results in the termination of either $f_{1}$ or $f_{k}$. And, (P2) says that once either $f_{1}$ or $f_{k}$ terminates the other component also terminates. The desired result, $p_{k+1}\ {\boldmath\mapsto}\ q_{k+1}$, follows by using transitivity on (P1) and (P2).

[TABLE]

The proofs mostly use the derived rules of leads-to from Section A.4. Note that $z_{k+1}$ includes all the shared variables between $f_{1}$ and $f_{k}$, namely $u$, so that the lifting rule can be used with $z_{k+1}$. Also note that

$p_{k+1}\Rightarrow(p_{1}\lor p_{k})$, $p_{k+1}\land q_{1}\Rightarrow p_{k}$, $p_{k+1}\land q_{k}\Rightarrow p_{1}$ and $q_{1}\land q_{k}\Rightarrow q_{k+1}$. As shown in Section C.2 $p_{k}$ is constant, hence stable, and $q_{k}$ is also stable in $f_{k}$.

Proof of (P1)

$p_{k+1}\ {\boldmath\mapsto}\ p_{k+1}\land(q_{1}\lor q_{k})$ in $f_{k+1}$: Below all properties are in $f_{k+1}$. Lifting rule refers to rule (L’) of Section A.4.3. We have already shown $p_{1}\ {\boldmath\mapsto}\ q_{1}$ and, inductively, $p_{k}\ {\boldmath\mapsto}\ q_{k}$.

[TABLE]

Proof of (P2)

$p_{k+1}\land(q_{1}\lor q_{k})\ {\boldmath\mapsto}\ q_{k+1}$ in $f_{k+1}$: Below all properties are in $f_{k+1}$.

[TABLE]

Appendix D References