Rely-guarantee (RG) reasoning is useful for modular Hoare-style proofs of concurrent programs. However, RG requires that assertions be proved stable under the actions of the environment. We cast stability analysis as a model checking problem and show how this may be of use in interactive and automatic verification.
Multi-core and multi-processor computing systems are now mainstream. Consequently, concurrent programs are the focus of much recent research on automatically proving safety, correctness and liveness properties. Often, the assertions we would like to prove are not amenable to existing automatic analyses. This paper studies one such scenario, and shows how existing automatic techniques can nonetheless help the proof process. The demonstration is expected to be the first step towards a fully automatic method.
Shared-memory concurrency, where multiple threads have read/write access to the same memory addresses, is commonplace. The main challenge in proving properties of such programs, and indeed in their design, is dealing with interference, i.e., the possibility that threads may concurrently make changes to the same memory address.
The concurrent programming community has evolved several synchronisation
schemes to avoid interference. Most rely on some form of access denial, such as
locks. Whereas locks make it easy to reason about the correctness, they may
also cause loss of efficiency as threads wait to acquire locks on needed resources.
Locking schemes have thus become increasingly fine-grained, attempting to deny
access to the smallest possible size of resource, to minimise waiting and maximise
concurrency. The ultimate form of such fine-grained concurrency are programs
that manage without any synchronisation at all [
The finer the concurrency, the more involved the logic for avoiding interference. This logic must implicitly or explicitly take the actions of other threads into account. This is a problem for program proofs where we strive for modularity, i.e., we wish to be able to reason about a piece of code in isolation from the various environments it could execute in.
Rely-guarantee reasoning [
The next section gives brief relevant background. We then describe our
method, and comment on shortcomings and possible developments. We assume
some familiarity with program proofs using Hoare logic [
Rely-guarantee (RG) is a compositional verification method for shared memory
concurrency introduced by Jones [
Our command language will be the one used by Jones [
Program variables will range over B and N. It may seem odd to have program variables range over infinite types. In practice however, reasoning about numbers with the aid of abstraction, has been found to be more tractable than reasoning about finite but huge state spaces over words or bit-vectors, which are harder to abstract due to fiddly problems with overflow and underflow.
RG can be seen as a compositional version of the Owicki-Gries method [
R and G summarise the properties of the individual atomic actions invoked by the environment and the thread respectively. An action is given as a binary relation on the shared state, and is written P Q. This notation indicates that the action updates the part of shared state that satisfies P (at the moment the action executes), so that it satisfies Q.
For example, the action corresponding to the command x := x + 1, that increments a shared integer x, might be written as x = N
x = N + 1 where the implicitly existentially quantified N serves to relate the state before and after the execution. Such logical variables are required for describing actions using single-state assertions. We shall denote them using N, M, . . . and assume they are existentially quantified with scope limited to the action.
G is the relation given by the reflexive and transitive closure of all actions of the thread being specified. The actions are given by manual annotation, as in general, automatic action discovery is non-trivial. R is calculated in an identical manner from the actions of the environment. Typically, the actions comprising R are just the G actions of all the other threads.
An assertion P on a single state is considered stable under interference from a binary relation R if (P ; R) ⇒ P , i.e., if P (s) and (s, s0) ∈ R, then P (s0). More specifically, if P is the pre-condition for some command C, then it must continue to hold after any environment action, before the execution of C. For our purpose, we do not need to pin down the level of atomicity of execution.
Jones gives a full proof system for the satisfaction relation, but we will not need it for this work. However, we reproduce the two critical rules here, to make our assumptions about RG concrete. The first rule is parallel composition, where || is the interleaving parallel composition operator.
(P1, R ∨ G2, G1, Q1)
C1 (P2, R ∨ G1, G2, Q2)
C2 (P1 ∧ P2, R, G1 ∨ G2, Q1 ∧ Q2)
C1||C2 The second rule tells us what it means for a command to be atomic. (P, id, true, Q ∧ G) (P, R, G, Q)
C
P stable under R atomic(C)
Note one departure from standard RG: the post-condition of the very last line of code is not checked for stability. It is instantaneously true immediately after execution of that line. At this point, either the thread terminates, so that we do not care whether the environment interferes with the post-condition, or, the thread resumes execution from some command the pre-condition of which will be the same as this post-condition, and thus will be checked for stability. 2.2
Let V be the set of program variables (or state variables) used in a program (with appropriate scope management, which we ignore without loss of generality). Each v ∈ V ranges over a non-empty set of values Dv. The state space S of the program is given by Qv∈V Dv. A single state of the program is then a value assignment to each v ∈ V .
Suppose AP is the set of all those atomic propositions over V that we might use in the specification of a program. Then we can turn the program into a state machine (technically, a Kripke structure) M represented as a tuple (S, S0, T, L) where S is the set of states, S0 ⊆ S is the set of initial states, T ⊆ S × S is the transition relation, and L : S → 2AP labels each state with the subset of AP that is true in that state.
A temporal logic augments propositional logic with modal and fix-point operators. The semantics of a temporal logic formula in which the atomic propositions range over AP can be expressed in terms of sets of states and/or sequences of states of M . If we turn a program into a state machine, we can use temporal logics to express time-dependent properties of the program.
The most common such property is the global invariant, i.e., a property that holds in all states of a state machine, or equivalently, always holds during the execution of a program.
Global invariants can be checked automatically using proof procedures known as model checkers, subject only to time and space constraints. More importantly, if the proof attempt fails, the model checker can return a counterexample, which is an execution path (sequence of states) leading from an initial state to a state in which the invariant is not satisfied.
The problem of model checking global invariants is in general undecidable
when the state space is infinite. However, the ability to produce counterexamples
has led to the development of counterexample guided abstraction refinement
(CEGAR) [
We do not need to describe model checking or CEGAR in more depth,
particularly as there are many different abstraction schemes and CEGAR techniques.
Further details may be found in [
If the assertion permits, stability can be checked syntactically and unstable assertions can be automatically stabilised by a fix-point computation that disjunctively adds state until stability is achieved. More precisely, given an assertion satisfying a set of states s, we compute the fix-point by until sn+1 = sn, i.e, performing n environment transitions. If the domain of any program variable is infinite, this fix-point computation might not terminate. In such cases, automatic stabilisation techniques rely on abstract interpretation to simplify the domain.
As a simple example, consider the assertion x = 10 that is clearly unstable under the environment action x = N x = N + 1. To stabilise, we would proceed s0 = (x = 10) s1 = (x = 10 ∨ x = 11) s2 = (x = 10 ∨ x = 11 ∨ x = 12) . .
. so automatic stabilisation will not terminate. To fix it, we could use the boolean abstraction α(x) ⇐⇒ x ≥ 10. Under this abstraction the action above becomes the identity action in all cases except when x = 9, but in that case x = 10 does not hold anyway, so we have stability immediately, and the assertion is stabilised to x ≥ 10.
In general, if the abstraction is too weak, it may throw away so much information that the proof becomes impossible (e.g., we can trivially stabilise any assertion by replacing it with true). But if the abstraction is too strong, the fix-point computation may not terminate, or may run out of time or space resources.
Current techniques therefore use hand-crafted abstraction heuristics that are
found to work in practice, for the underlying variable domains [
We have seen in §2.2 that this problem of finding exactly the right level of abstraction also occurs in model checking. It is our hope that the model checking solution can be applied to stability analysis as well. If so, the vast amount of model checking research on this topic can be brought to bear on the problem. We now present the first step towards this goal, by representing stability analysis as a model checking problem.
Rather than representing R and G as the reflexive transitive closures of their constituent actions, we consider them as state machines over the shared state. In addition, the state machine also has state variables for the program counters of the constituent threads. Tracking program counters allows us to easily encode the flow control of actions in the state machine.
The state machine for the guarantee condition Gt for a thread t, is Mt = (St, S0t, t, Lt) and is constructed as follows. Let Vt be the set of all shared program variables used in t as well as the t program counter pct : N. Then St is constructed like S in §2.2. S0t is those states of St in which pct = 0 and in which any other v ∈ Vt are assigned their initial values if any. Let al be the (possibly empty) set of actions associated with the primitive command on line l of the thread code (this is for easy specification: in reality a single atomic statement can only have a single associated action, so the analysis simply conjoins them). Then t((s, pct), (s0, pc0t)) = _ l pct = l ∧ pc0t = next(s, l) ∧ ^ a(s, s0)
! a∈al where the next function encodes the control flow of thread t. Finally, Lt(s) = {p ∈ AP | p(s) = true}. The state machine for R, MR = (SR, S0R, TR, LR) over variables VR, is constructed analogously, though of course it is more complicated since it encompasses the actions of all the other threads.
Now suppose that we wish to stabilise an assertion P that is the pre-condition of a command at program line l in a thread t. The first step is to check whether the assertion is already stable. To do this we augment MR with fresh1 variables corresponding to any thread-local variables that occur in P , and also add identity actions over these variables to TR so that their values never change. This represents our intuition that when checking the stability under the environment of an assertion in thread t, t itself is not executing.
We can now model check the augmented state machine M R0 for the global
invariant P . Note that here we can use standard model checking abstraction
construction techniques [
At this point we have already improved on existing stabilisation methods by not being reliant on having a syntactic check for stability. However, we still have to handle the case where the stability check fails.
In this situation, we have at hand a counterexample trace π showing a sequence of environment actions that falsified P , and also the particular abstraction function α being used by the model checker when the stability check failed. These two pieces of information can be used to weaken P and then repeat the stability check, and iterate until P is stable. 1 So that there is no name clash with any v ∈ VR.
For example, if we are using predicate abstraction techniques, then for our running example where we are checking stability of P ≡ x = 10, we may have α(x) ⇐⇒ x = 10 and π ≡ x = 10 where k uniquely identifies the action responsible. This information suggests generalising P to x ≥ 10, and then the stability check succeeds.
This is as far as we have come. The new weakened assertion must be found
manually for now, using the point-of-failure α and π as guides, as in the example
above. Of course, we could simply use the existing method of repeated disjunctive
addition of the resultant state of the involved actions (which in this
cherrypicked example fails to terminate). However, the model checking approach gives
us extra information (point-of-failure π and α) which should hopefully allow
us to do better. We plan to develop an automatic method that uses symbolic
simulation driven by the counterexample traces, perhaps in combination with
heuristics, to weaken P in a useful manner. Here, we expect to use existing model
checking research on automatic abstraction construction [
In fact, at the moment our in-development tool (effectively a translation layer
on top of the NuSMV model checker [
In standard RG, the rely is represented as the reflexive transitive closure of all actions that the environment can execute. This can also be thought of as a state machine, albeit a not very informative one in which any transition (action) can execute from any state. Thus, our representation of R and G as state machines of actions can be seen as a refinement of the standard RG representation. The latter can be thought of as the state machine consisting of all states reachable from any state via all possible interleavings of the underlying actions, regardless of whether these interleavings will ever actually occur. Our refinement proceeds by adding control flow information, thus ruling out certain interleavings.
Thus it is possible for us to prove the stability of stronger assertions than is possible in standard RG. Since the stability check is orthogonal to the RG proof system, this means that we automatically obtain a stronger proof system.
Indeed, we can parameterise the RG proof system by the level of refinement of R and G. We have experimented along these lines by adding some G actions to R, or by selectively exposing the thread-local state of the environment, both of which rule out some class of impossible action sequences. In each case we have been able to prove properties that are stronger, and often more intuitive to specify.
There is a trade-off here, since adding more information to R and G will almost certainly make the underlying model checking problem harder, affecting scalability. Nonetheless, increasing the refinement level is attractive not only because it permits stronger properties to be proved, but also because the stabilised assertion may be syntactically smaller and thus more readable. This latter consideration is important if these methods are used as part of a larger interactive proof framework, such as a theorem prover. 4
We do not know of any other work that uses model checking for stability analysis
in Hoare-style RG proofs. There is work underway at MSR Cambridge [
It is well known [
Apart from the unfinished aspect, this approach has other shortcomings. An
important one is that refining R and G quickly makes the underlying model
checking problem more resource intensive. The same refinement (specifically,
the need to track program counters) also prevents the results from scaling up
to arbitrary numbers of threads for free, unlike in standard RG. We expect
that model checking techniques like paramatric verification [
We are also considering the use of separation logic in this framework, to
frame out irrelevant state and thus alleviate our model checking woes. RG and
separation logic have already been combined [
Acknowledgement The first author would like to thank Viktor Vafeiades for permission to copy from the description of RG in his Ph.D. thesis.