Waitfree linearization of data objects was introduced by Herlihy in 1991. The present article proposes an algorithm for waitfree linearization of a possibly nondeterministic data object in bounded memory, together with a complete proof of correctness supported by the proof assistant PVS. The project is exceptional in that the proofs of 70 invariants are recorded systematically, and that waitfree progress is quantified in waitfree complexity and is formally proved.

An example is given of a software algorithm that implements its specification in linear time temporal logic (LTL), but not in branching time temporal logic (CTL). In LTL, a prophecy of future behaviour is needed to prove the simulation. Eternity variables are used for this purpose. The final phase of the proof is a refinement mapping in which two threads exchange roles. The example is a software implementation of trylock in a variation of the fast mutual exclusion algorithm of Lamport (1987). It has been used fruitfully for the construction of software algorithms for high performance mutual exclusion.

Abstract UNITY is a model for concurrent specifications with a complete logic for proving progress properties of the form “ P leads to Q ”. UNITY is generalized to U-specifications by giving more freedom to specify the steps that are to be taken infinitely often. In particular, these steps can correspond to non-total relations. The generalization keeps the logic sound and complete. The paper exploits the generalization in two ways. Firstly, the logic remains sound when the specification is extended with hypotheses of the form “ F leads to G ”. As the paper shows, this can make the logic incomplete. The generalization is used to show that the logic remains complete, if the added hypotheses “ F leads to G ” satisfy “ F unless G ”. The main result extends the applicability and completeness of UNITY logic to proofs that a given concurrent program satisfies any given formula of LTL, linear temporal logic, without the next-operator which is omitted because it is sensitive to stuttering. For this purpose, the program, written as a UNITY program, is extended with a number of boolean variables. The proof method relies on implementing the LTL formula, i.e., restricting the specification in such a way that only those runs remain that satisfy the formula. This result is a variation of the classical construction of a Büchi automatonfor a given LTL formula that accepts precisely those runs that satisfy the formula.

Summary This paper presents new starvation‐free hardware‐assisted and software‐only algorithms for the N‐thread mutual‐exclusion problem. The hardware‐assisted versions use a single atomic‐CAS instruction and no fences. The software‐only algorithms simulate the CAS instruction using a variation of Burns‐Lamport (1 fence) or Lamport's fast algorithm (3 fences). The algorithms are based on Attiya et al, where every thread in the critical section chooses its successor (if one is available). While Attiya et al use a binary tree for this purpose, it can also be done with a linear search. Surprisingly, all software‐only algorithms perform equally well under maximal contention on three different computer architectures; the hardware‐assisted versions perform better under minimal contention. The new algorithms are between −5% to 50% slower for maximal contention than the starvation‐free first‐come first‐served hardware‐assisted MCS algorithm, which uses two atomic instructions (fetch‐store and CAS); they are between 10% to 50% slower than MCS for minimal contention.

Summary This paper presents a newstarvation‐freesoftware algorithm for theN‐thread mutual‐exclusion problem. In the absence of contention, the algorithm requires only eight write and four read operations to enter and leave the critical section; to the best of our knowledge, this is optimal. For algorithmswith starvation, five write and two read read operations are optimal. In the presence of contention, the algorithm has excellent performance comparable to the best‐known software solutions using only atomic load and store and to a hardware‐assisted lock (MCS) using stronger atomic primitives and used within the Linux kernel. It is rare for software‐only algorithms for mutual exclusion to perform well for both minimal and maximal contention workloads, making the new algorithm largely self‐tuning when exposed to swings in access patterns.

Abstract Given a mutual exclusion algorithm MXd for d ≥ 2 threads, a mutual exclusion algorithm for N > d threads can be built in a tree of degree d with N leaves, with the critical section at the root of the tree. This tournament solution seems obviously correct and efficient. The present note proves the correctness, and formalizes the efficiency in terms of concurrent complexity by means of Bounded Unity. If the tree is balanced, the throughput is logarithmic in N . If moreover MXd satisfies FCFS (first-come first-served), the worst case individual delay of the tournament algorithm is of order N . This is optimal.

Summary Dekker's algorithm was thought to be safe in an environment without atomic reads or writes where bits flicker or scramble during simultaneous operations. A counter‐example is presented showing Dekker's algorithm is unsafe without atomic read. A modification to the original algorithm is presented making it RW‐safe, allowing threaded systems to be built on low cost/power hardware without atomic read/write. Correctness is verified by means of invariants and UNITY logic. A performance comparison is made for several two‐thread software mutual‐exclusion algorithms to see if the RW‐safe Dekker is competitive. A subset of the two‐thread solutions are then compared in two N‐thread tournament algorithms. The performance results show that the additional checks in the RW‐safe Dekker do not disadvantage the algorithm in comparison with other two‐thread algorithms. The RW‐safe N‐thread tournament algorithms are competitive with the hardware‐assisted Mellor‐Crummey and Scott algorithm. Copyright © 2015 John Wiley & Sons, Ltd.

Abstract Lamport’s Bakery Algorithm (Commun ACM 17:453–455, 1974 ) implements mutual exclusion for a fixed number of threads with the first-come first-served property. It has the disadvantage, however, that it uses integer communication variables that can become arbitrarily large. Taubenfeld’s Black-White Bakery Algorithm (Proceedings of the DISC. LNCS, vol 3274, pp 56–70, 2004 ) keeps the integers bounded, and is adaptive in the sense that the time complexity only depends on the number of competing threads, say N . The present paper offers an assertional proof of correctness and shows that the concurrent complexity for throughput is linear in N , and for individual progress is quadratic in N . This is proved with a bounded version of UNITY, i.e., by assertional means.

Summary Software solutions for mutual exclusion developed over a 30‐year period, starting with complex ad hoc algorithms and progressing to simpler formal ones. While it is easy to dismiss software solutions for mutual exclusion, as this family of algorithms is antiquated and most platforms support atomic hardware instructions, there is still a need for these algorithms in threaded, embedded systems running on low‐cost processors lacking atomic instructions. WhileN‐thread solutions are usually short (10–25 lines of code), each is ingenious with exceptionally subtle aspects, often making it difficult to prove correctness or construct an implementation. This work examines correctness and performance of the implementations. An extensive survey of existing algorithms is presented, with explanations of the intuition behind the algorithms and how they work. Several errors were found and corrections made, as well as a few small improvements, in the existing algorithms; two new high‐performance algorithms were developed. Finally, a worst‐case high‐contention performance experiment is performed to compare the algorithms and contrast them with three common locks based on hardware atomic instructions. The results show our two new algorithms are highly competitive with an equivalent hardware lock (Mellor‐Crummey and Scott) over a range of 1–32 processors. Hence, threading is a viable alternative to event‐driven programming for complex embedded systems without atomic instructions. Copyright © 2014 John Wiley & Sons, Ltd.

Abstract The standard implementation of mutual exclusion by means of a semaphore allows starvation of processes. Between 1979 and 1986, three algorithms were proposed that preclude starvation. These algorithms use a special kind of semaphore. We model this so-called buffered semaphore rigorously and provide mechanized proofs of the algorithms. We prove that the algorithms are three implementations of one abstract algorithm in which every competing process is overtaken not more than once by any other process. We also consider a so-called polite semaphore, which is weaker than the buffered one and is strong enough for one of the three algorithms. Refinement techniques are used to compare the algorithms and the semaphores.

Abstract An abstract file system is defined here as a partial function from (absolute) paths to data. Such a file system determines the set of valid paths. It allows the file system to be read and written at a valid path, and it allows the system to be modified by the Unix operations for creation, removal, and moving of files and directories. We present abstract definitions (axioms) for these operations. This specification is refined towards a pointer implementation. The challenge is to have a natural abstraction function from the implementation to the specification, to define operations on the concrete store that behave exactly in the same way as the corresponding functions on the abstract store, and to prove these facts. To mitigate the problems attached to partial functions, we do this in two steps: first a refinement towards a pointer implementation with total functions, followed by one that allows partial functions. These two refinements are proved correct by means of a number of invariants. Indeed, the insights gained consist, on the one hand, of the invariants of the pointer implementation that are needed for the refinement functions, and on the other hand of the precise enabling conditions of the operations on the different levels of abstraction. Each of the three specification levels is enriched with a permission system for reading, writing, or executing, and the refinement relations between these permission systems are explored. Files and directories are distinguished from the outset, but this rarely affects our part of the specifications. All results have been verified with the proof assistant PVS, in particular, that the invariants are preserved by the operations, and that, where the invariants hold, the operations commute with the refinement functions.

Abstract A context-free grammar corresponds to a system of equations in languages. The language generated by the grammar is the smallest solution of the system. We give a necessary and sufficient condition for an arbitrary solution to be the smallest one. We revive an old criterion to decide that a grammar has a unique solution. All this fits in an approach to search for a grammar for an arbitrary language that is given by other means. The approach is illustrated by the derivation of a grammar for a certain set of bit strings. The approach is used to give an elegant derivation of the grammar for a language accepted by a pushdown automaton.

On shared memory multiprocessors, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. By avoiding locks, the significant benefit of lock (or wait)-freedom for real-time systems is that the potentials for deadlock and priority inversion are avoided. The lock-free algorithms often require the use of special atomic processor primitives such as CAS (compare and swap) or LL /SC (load linked/store conditional). However, many machine architectures support either CAS or LL /SC , but not both. In this paper, we present a lock-free implementation of the ideal semantics of LL /SC using only pointer-size CAS , and show how to use refinement mapping to prove the correctness of the algorithm.

A general algorithm for computing Euclidean skeletons of 2D and 3D data sets in linear time is presented. These skeletons are defined in terms of a new concept, called the integer medial axis (IMA) transform. We prove a number of fundamental properties of the IMA skeleton, and compare these with properties of the CMD (centers of maximal disks) skeleton. Several pruning methods for IMA skeletons are introduced (constant, linear and square-root pruning) and their properties studied. The algorithm for computing the IMA skeleton is based upon the feature transform, using a modification of a linear-time algorithm for Euclidean distance transforms. The skeletonization algorithm has a time complexity which is linear in the number of input points, and can be easily parallelized. We present experimental results for several data sets, looking at skeleton quality, memory usage and computation time, both for 2D images and 3D volumes.

Morphological attribute filters have not previously been parallelized, mainly because they are both global and non-separable. We propose a parallel algorithm that achieves efficient parallelism for a large class of attribute filters, including attribute openings, closings, thinnings and thickenings, based on Salembier's Max-Trees and Min-trees. The image or volume is first partitioned in multiple slices. We then compute the Max-trees of each slice using any sequential Max-Tree algorithm. Subsequently, the Max-trees of the slices can be merged to obtain the Max-tree of the image. A C-implementation yielded good speed-ups on both a 16-processor MIPS 14000 parallel machine, and a dual-core Opteron-based machine. It is shown that the speed-up of the parallel algorithm is a direct measure of the gain with respect to the sequential algorithm used. Furthermore, the concurrent algorithm shows a speed gain of up to 72 percent on a single-core processor, due to reduced cache thrashing.

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.

The Euclidean distance transform of a binary image is the function that assigns to every pixel the Euclidean distance to the background. The Euclidean feature transform is the function that assigns to every pixel the set of background pixels with this distance. We present an algorithm to compute the exact Euclidean feature transform sets in linear time. The algorithm is applicable in arbitrary dimensions.

Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and only if there is a simulation from the first one to the second one that satisfies a certain condition. By adding stutterings, the formalism allows that the concrete behaviors take more (or possibly less) steps than the abstract ones.Eternity variables are introduced as a more powerful alternative for prophecy variables and backward simulations. This formalism is semantically complete: every simulation that preserves quiescence is a composition of a forward simulation, an extension with eternity variables, and a refinement mapping. This result does not need finite invisible nondeterminism and machine closure as in the Abadi--Lamport Theorem. The requirement of internal continuity is weakened to preservation of quiescence.Almost all concepts are illustrated by tiny examples or counter-examples.

Summary form only given. In multiprogrammed systems, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. Wait-free and lock-free algorithms can do without locking mechanisms, and therefore do not suffer from these problems. We present an efficient almost wait-free algorithm for parallel accessible hashtables, which promises more robust performance and reliability than conventional lock-based implementations. Our solution is as efficient as sequential hashtables. It can easily be implemented using C-like languages and requires on average only constant time for insertion, deletion or accessing of elements. The algorithm allows the hashtables to grow and shrink when needed. A true problem of wait-free and lock-free algorithms is that they are hard to design correctly, even when apparently straightforward. The reason for this is that processes can execute all statements in every conceivable order. Since our algorithm is quite large and rather complex, we turned to the interactive theorem prover PVS to prove safety of our algorithm, which we could not have done reliably by hand. To our knowledge no algorithms of comparable complexity have ever been mechanically verified. Wait-freedom is shown informally.

Abstract. 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.

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 $m$ readers and writers, based on $m^2$ 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.

Abstract. The paper announces an incremental mechanically–verified design of the algorithm of Gallager, Humblet, and Spira for the distributed determination of the minimum-weight spanning tree in a graph of processes. The processes communicate by means of asynchronous messages with their neighbours in the graph. Messages over one link may pass each other. The proof of the algorithm is based on ghost variables, invariants, and a decreasing variant function. The verification is mechanized by means of the theorem prover Nqthm of Boyer and Moore. This extended abstract is an introduction to the full paper that can be obtained by ftp (http://link.springer.de/link/service/journals/00165/).

Abstract. The weakest precondition semantics of recursive procedures with local variables are developed for an imperative language with demonic and angelic operators for unbounded nondeterminate choice. This does not require stacking of local variables. The formalism serves as a foundation for a proof rule for total correctness of (mutually) recursive procedures with local variables. This rule is illustrated by a simple example. Its soundness is proved for arbitrary well-founded variant functions.

Abstract We describe the construction of a distributed algorithm with asynchronous communication together with a mechanically verified proof of correctness. For this purpose we treat Segall's PIF algorithm (propagation of information with feedback). The proofs are based on invariants, and variant functions for termination. The theorem prover NQTHM is used to deal with the many case distinctions due to asynchronous distributed computation. Emphasis is on the modelling assumptions, the treatment of nondeterminacy, the forms of termination detection, and the proof obligations for a complete mechanical proof. Finally, a comparison is made with (the proof of) the minimum spanning tree algorithm of Gallager, Humblet, and Spira, for which the technique was developed.

Abstract For convenient application of a first-order theorem prover to verification of imperative programs, it is important to encapsulate the operational semantics in generic theories. The possibility to do so is illustrated by two theories for the Boyer-Moore theorem prover Nqthm. The first theory is an Nqthm version of the classical while-theorem. Here the main interest is to show how one can use Nqthm's facilities to constrain and to functionally instantiate for the development and application of a generic theory. The theory is illustrated by a linear search program. The second theory is a finitary approach to progress for shared-memory concurrent programs. It is illustrated by Peterson's algorithm for mutual exclusion of two processes. The proof of progress for Peterson's algorithm is new. The assertion of bounded fairness is slightly stronger than the conventional notion of weak fairness. This new concept may have other applications.

Abstract Temporal weakest precondions are introduced for calculational reasoning about the states encountered during execution of not-necessarily terminating recursive procedures. The formalism can distinguish error from useful nontermination. The precondition functions are constructed in a new and more elegant way. Healthiness laws are discussed briefly. Proof rules are introduced that enable calculational proofs of various safety and progress properties. The construction of the precondition functions is justified in an Appendix that provides the operational semantics.

Abstract Four proof rules for recursive procedures in a Pascal-like language are presented. The main rule deals with total correctness and is based on results of Gries and Martin. The rule is easier to apply than Martin's. It is introduced as an extension of a specification format for Pascal-procedures, with its associated correctness and invocation rules. It uses well-founded recursion and is proved under the postulate that a procedure is semantically equal to its body. This rule for total correctness is compared with Hoare's rule for partial correctness of recursive procedures, in which no well-founded relation is needed. Both rules serve to prove correctness, i.e. sufficiency of certain preconditions. There are also two rules for proving necessity of preconditions. These rules can be used to give formal proofs of nontermination and refinement. They seem to be completely new.

Abstract Dijkstra's language of guarded commands is extended with recursion and transformed into algebra. The semantics is expressed in terms of weakest preconditions and weakest liberal preconditions. Extreme fixed points are used to deal with recursion. Unbounded nondeterminacy is allowed. The algebraic setting enables us to develop efficient transformation rules for recursive procedures. The main result is an algebraic version of the rule of computational induction. In this version, certain parts of the programs are restricted to finite nondeterminacy. It is shown that without this restriction the rule would not be valid. Some applications of the rule are presented. In particular, we prove the correctness of an iterative stack implementation of a class of simple recursive procedures.

Abstract Girard's recent system of linear logic is presented in a way that avoids the two-level structure of formulae and sequents, and that minimises the number of primitive function symbols. A deduction theorem is proved concerning the classical implication as embedded in linear logic. The Hilbert-style axiomatisation is proved to be equivalent to the sequent formalism. The axiomatisation leads to a complete class of algebraic models. Various models are exhibited. On the meta-level we use Dijkstra's method of explicit equational proofs.

The theory of abstract data types is generalized to the case of nondeterministic operations (set-valuedfunctions). Since the nondeterminism of operations may be coupled, signatures are extended so that operations can have results in Cartesian products. Input/output behavior is used to characterize implementation of one model by another. It is described by means of accumulated arrows, which form a generalization of the term algebra. Morphisms of nondeterministic models are introduced. Both innovations prove to be powerful tools in the analysis of input/output behavior. Extraction equivalence and observable equivalence of values are investigated. Quotient models for such equivalence relations are constructed. The equivalence relations are compared with each other, with separation of values by means of experiments, and with the separation property that characterizes a terminal model. Examples are given to show that the four concepts are different. In deterministic models the concepts coincide.