An assertional proof for a construction of an atomic variable

The paper proves by assertional means the correctness of a construction of Haldar and Subramanian of an atomic shared variable for one writer and one reader. This construction uses four unsafe variables and four safe boolean variables. Assignment to a safe but nonatomic variable is modelled as a repetition of random assignments concluded by an actual assignment. The proof obligation consists of four invariants. These are proved using 25 auxiliary invariants. The proof has been constructed and verified with the theorem prover NQTHM.Received May 2002 Accepted in revised form March 2004 by D.J. Cooke     

Nonatomic dual bakery algorithm with bounded tokens

A simple mutual exclusion algorithm is presented that only uses nonatomic shared variables of bounded size, and that satisfies bounded overtaking. When the shared variables behave atomically, it has the first-come-first-served property (FCFS). Nonatomic access makes information vulnerable. The effects of this can be mitigated by minimizing the information and by spreading it over more variables. The design approach adopted here begins with such mitigating efforts. These resulted in an algorithm with a proof of correctness, first for atomic variables. This proof is then used as a blueprint for the simultaneous development of the algorithm for nonatomic variables and its proof. Mutual exclusion is proved by means of invariants. Bounded overtaking and liveness under weak fairness are proved with invariants and variant functions. Liveness under weak fairness is formalized and proved in a set-theoretic version of temporal logic. All these assertions are verified with the proof assistant PVS. We heavily rely on the possibility offered by a proof assistant like PVS to reuse proofs developed for one context in a different context.     

An assertional criterion for atomicity

A criterion is presented to prove atomicity of read-write objects by means of ghost variables and invariants. The criterion is applied to Bloom's construction of a two-writer atomic register from two one-writer atomic registers and to the algorithm of Vitanyi and Awerbuch for the construction of a read-write object with readers and writers, based on read-write objects for one reader and one writer. In both cases, the proof comes down to the verification of a number of invariants. The hand-written proofs of these invariants have been verified with a mechanical theorem prover. Received: 10 May 2001 / 6 December 2001     

Local proofs for global safety properties

This paper explores locality in proofs of global safety properties of concurrent programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which together imply the desired global safety property. Local proofs can be more compact than global proofs, but local reasoning is also inherently incomplete. In this paper, we present an algorithm for safety verification that combines local reasoning with gradual refinement. The algorithm gradually exposes facts about the internal state of components, until either a local proof or a real error is discovered. The refinement mechanism ensures completeness. Experiments show that local reasoning can have significantly better performance over the traditional reachability computation. Moreover, for some parameterized protocols, a local proof can be used as the basis of a correctness proof over all instances.     

A criterion for atomicity revisited

Concurrent and reactive programs are specified by their behaviours in the presence of a nondeterministic environment. In a natural way, this gives a specification (ARW) of an atomic variable in the style of Abadi and Lamport. Several implementations of atomic variables by lower level primitives are known. A few years ago, we formulated a criterion to prove the correctness of such implementations. The proof of correctness of the criterion itself was based on Lynch’s definition of atomicity by serialization points. Here, this criterion is reformulated as a specification HRW in the formal sense. Simulations from HRW to ARW and vice versa are constructed. These now serve as a constructive proof of correctness of the criterion. Eternity variables are used in the simulation from HRW to ARW. We propose so-called gliding simulations to deal with the problems that appear when occasionally the concrete implementation needs fewer steps than the abstract specification.     

Coloured Petri net refinement specification and correctness proof with Coq

In this work, we address the issue of the formal proof (using the proof assistant Coq) of refinement correctness for symmetric nets, a subclass of coloured Petri nets. We provide a formalisation of the net models, and of their type refinement in Coq. Then the Coq proof assistant is used to prove the refinement correctness lemma. An example adapted from a protocol example illustrates our work.     

Using refinement calculus techniques to prove linearizability

Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.     

Understanding and Documenting Programs

This paper reports on an experiment in trying to understand an unfamiliar program of some complexity and to record the authors' understanding of it. The goal was to simulate a practicing programmer in a program maintenance environment using the techniques of program design adapted to program understanding and documentation; that is, given a program, a specification and correctness proof were developed for the program. The approach points out the value of correctness proof ideas in guiding the discovery process. Toward this end, a variety of techniques were used: direct cognition for smaller parts, discovering and verifying loop invariants for larger program parts, and functions determined by additional analysis for larger program parts. An indeterminate bounded variable was introduced into the program documentation to summarize the effect of several program variables and simplify the proof of correctness.     

A distributed resource allocation algorithm for many processes

Resource allocation is the problem that a process may enter a critical section CS of its code only when its resource requirements are not in conflict with those of other processes in their critical sections. For each execution of CS, these requirements are given anew. In the resource requirements, levels can be distinguished, such as e.g. read access or write access. We allow unboundedly many processes that communicate by reliable asynchronous messages and have finite memory. A simple starvation-free solution is presented. Processes only wait for one another when they have conflicting resource requirements. The correctness of the solution is argued with invariants and temporal logic. It has been verified with the proof assistant PVS.     

Blackwell’s Theorem for T-related fuzzy variables

In this paper, we consider Blackwell’s Theorem in which inter-arrival times are characterized as fuzzy variables under t-norm-based fuzzy operations. We first prove that Blackwell’s Theorem for T-related fuzzy variables with respect to necessity measure holds true where T is an Archimedean t-norm. Subsequently, we provide a counter example under which Blackwell’s Theorem does not hold when T = min. Finally, we evaluate the expected value of fuzzy variable with respect to credibility measure and derive fuzzy Blackwell’s Theorem based on the expected value of fuzzy variables.     

A simple proof of the necessity of the failure detector Σ to implement an atomic register in asynchronous message-passing systems

This paper presents a simple proof that shows that the quorum failure detector class (denoted Σ) is the weakest failure detector class required to implement an atomic read/write register in an asynchronous message-passing system prone to an arbitrary number of process crashes. This proof is based on a new reduction algorithm in which all the variables are bounded.     

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.     

A simple proof technique for priority-scheduled systems

A simple proof method is presented for proving invariance properties of concurrent programs in priority-scheduled systems. This method is illustrated by using it to establish the correctness of a simple wait-free consensus algorithm for priority-scheduled uniprocessor systems. This consensus algorithm is of interest in its own right because is shows that atomic read and write operations are universal in priority-scheduled uniprocessor systems, i.e., they can be used to implement any shared object in such a system in a wait-free manner. This stands in contrast to fully asynchronous systems, where strong synchronization primitives such as compare-and-swap are needed for universality.     

Mechanized proofs of opacity: a comparison of two techniques

Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called opacity, which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.     

Generating all polynomial invariants in simple loops

This paper presents a method for automatically generating all polynomial invariants in simple loops. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Based on this connection, a fixpoint procedure using operations on ideals and Gröbner basis constructions is proposed for finding all polynomial invariants. Most importantly, it is proved that the procedure terminates in at most m+1$m+1$ iterations, where m$m$ is the number of program variables. The proof relies on showing that the irreducible components of the varieties associated with the ideals generated by the procedure either remain the same or increase their dimension at every iteration of the fixpoint procedure. This yields a correct and complete algorithm for inferring conjunctions of polynomial equalities as invariants. The method has been implemented in Maple using the Groebner package. The implementation has been used to automatically discover non-trivial invariants for several examples to illustrate the power of the technique.     

The correctness proof of Ben-Or’s randomized consensus algorithm

In a ground-breaking paper that appeared in 1983, Ben-Or presented the first randomized algorithm to solve consensus in an asynchronous message-passing system where processes can fail by crashing. Although more efficient randomized algorithms were subsequently proposed, Ben-Or’s algorithm is still the simplest and most elegant one. For this reason, it is often taught in distributed computing courses and it appears in several textbooks. Even though Ben-Or’s algorithm is widely known and it is very simple, surprisingly a proof of correctness of the algorithm has not yet appeared: previously published proofs make some simplifying assumptions—specifically, they either assume that f < n/3 (n is the total number of processes and f is maximum number of processes that may crash) or that the adversary is weak, that is, it cannot see the process states or the content of the messages. In this paper, we present a correctness proof for Ben-Or’s randomized consensus algorithm for the case that f < n/2 process crashes and the adversary is strong (i.e., it can see the process states and message contents, and schedule the process steps and message receipts accordingly). To the best of our knowledge, this is the first full proof of this classical algorithm. We also demonstrate a counterintuitive problem that may occur if one uses the well-known abstraction of a “global coin” to modularize and speed up randomized consensus algorithms, such as Ben-Or’s algorithm. Specifically, we show that contrary to common belief, the use of a global coin can sometimes be deleterious rather than beneficial: instead of speeding up Ben-Or’s algorithm, the use of a global coin in this algorithm may actually prevent termination.     

A hoare-like proof system for analysing the computation time of programs

Versions of Hoare logic have been introduced to prove partial and total correctness properties of programs. In this paper it is shown how a Hoare-like proof system for while programs may be extended to prove properties of the computation time as well. It should be stressed that the system does not require the programs to be modified by inserting explicit operations upon a clock variable. We generalize the notions of arithmetically sound and complete and show that the proof system satisfies these. Also we derive formal rules corresponding to the informal rules for determining the computation time of while programs. The applicability of the proof system is illustrated by an example, the bubble sorting algorithm.     

A general lock-free algorithm using compare-and-swap

The compare-and-swap register (CAS) is a synchronization primitive for lock-free algorithms. Most uses of it, however, suffer from the so-called ABA problem. The simplest and most efficient solution to the ABA problem is to include a tag with the memory location such that the tag is incremented with each update of the target location. This solution, however, is theoretically unsound and has limited applicability. This paper presents a general lock-free pattern that is based on the synchronization primitive CAS without causing ABA problem or problems with wrap around. It can be used to provide lock-free functionality for any data type. Our algorithm is a CAS variation of Herlihy’s LL/SC methodology for lock-free transformation. The basis of our techniques is to poll different locations on reading and writing objects in such a way that the consistency of an object can be checked by its location instead of its tag. It consists of simple code that can be easily implemented using C-like languages. A true problem of lock-free algorithms is that they are hard to design correctly, which even holds for apparently straightforward algorithms. We therefore develop a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on Lamport’s refinement mappings, and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and formulate without considering the internal structure of the final implementation.     

Correctness of programs with Pascal-like procedures without global variables

We study a programming language L_Pas consisting of blockstructured programs with a Pascal-like procedure concept which allows procedures as parameters. Due to Clarke (1979) there cannot be any sound and relatively complete Hoare-like system proving partial correctness for the full language L_Pas. However, in Langmaack and Olderog (1980) it has been conjectured that such a system exists once global variables are disallowed.In this paper we prove a slightly weaker version of this conjecture by presenting a Hoare-like system which is sound and g-complete for all programs in L_Pas without global variables; g-completeness means completeness modulo a special second-order theory and an appropriate notion of expressiveness. The proof system provides new methods of dealing with procedures which are formalized in the Rule of Separation for procedure calls. The completeness proof for the system is carried out in a transparent way using modified formal computation trees. An example shows how to apply the proposed methods.     

Probabilistic guarded commands mechanized in HOL

The probabilistic guarded-command language (pGCL) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-)valued functions.We present a mechanization of the quantitative logic for pGCL using the HOL theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL.The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm.