Abstract The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns and allows different theorem provers to be used interchangeably. However, generating verification conditions is still a difficult undertaking and the use of more “high-level” intermediate verification languages has become commonplace. In particular, Boogie provides a widely used and understood intermediate verification language. A common difficulty is the potential for an impedance mismatch between the source language and the intermediate verification language. In this paper, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We provide a comprehensive account of translating Whiley to Boogie which demonstrates that it is possible to model most aspects of the Whiley language. Key challenges posed by the Whiley language included: the encoding of Whiley’s expressive type system and support for flow typing and generics; the implicit assumption that expressions in specifications are well defined; the ability to invoke methods from within expressions; the ability to return multiple values from a function or method; the presence of unrestricted lambda functions; and the limited syntax for framing. We demonstrate that the resulting verification tool can verify significantly more programs than the native Whiley verifier which was custom-built for Whiley verification. Furthermore, our work provides evidence that Boogie is (for the most part) sufficiently general to act as an intermediate language for a wide range of source languages.

Path dependent types have long served as an expressive component of the Scala programming language. They allow for the modelling of both bounded polymorphism and a degree of nominal subtyping. Nominality in turn provides the ability to capture first class modules. Thus a single language feature gives rise to a rich array of expressiveness. Recent work has proven path dependent types sound in the presence of both intersection and recursive types, but unfortunately typing remains undecidable, posing problems for programmers who rely on the results of type checkers. The Wyvern programming language is an object oriented language with path dependent types, recursive types and first class modules. In this paper we define two variants of Wyvern that feature decidable typing, along with machine checked proofs of decidability. Despite the restrictions, our approaches retain the ability to encode the parameteric polymorphism of Java generics along with many idioms of the Scala module system.

Network devices rely on forwarding rules to forward packets. With the latest OpenFlow standard (the de-facto software defined network standard), the rules that make up a forwarding set may be expressed in the form of a single table or multiple linked tables. This raises the question of how to reconcile the forwarding behaviour of different flow tables? In this paper we propose two approaches to convert various forwarding sets into a canonical form called equivalent forwarding set and formalise the process of evaluating equivalence between two forwarding sets in terms of networking function.

Software Defined Networking (SDN) enables a centralised entity - the controller - to monitor the network's status by collecting traffic statistics such as packets, bytes, etc. Each statistic is associated with a forwarding table entry (FTE) in a switch whose structure and format is specified by the OpenFlow standard (de-facto SDN standard). For a flow with a FTE, its statistic is easily acquired by an inquiry from a controller to the switch on this flow's corresponding FTE. If a flow has no matching FTE, its statistic is not known until a new FTE is installed for the purpose of monitoring it. However, the time to install these FTEs and the potential conflicts between them and the existing FTEs jeopardise the feasibility of this approach. To avoid these drawbacks, this paper proposes a traffic estimation approach based on the existing FTE's statistics. With the help of boolean algebra, the deterministic confidence interval of any given flowset can be estimated. This approach avoids the FTE installation time and also saves the FTE storage space.

Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures. We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.

Traditionally, formal semantic models of Java-like languages use an explicit model of the store which mimics pointers and ram. These low level models hamper understanding of the semantics, and development of proofs about ownerships and other encapsulation properties, since the real (graph) structure of the data is obscured by the encoding. Such models are also inadequate for didactic purposes since they rely on run-time structures that do not exist in the source program --- in order to understand the meaning of an expression in the middle of the execution one is required to visualize the memory structure which is hard to relate to the abstract program state.

Abstract Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving that they are. In this paper, we present TMS1 (Transactional Memory Specification 1), a precise specification of correct behaviour of a TM runtime library. TMS1 targets TM runtimes used to implement transactional features in an unmanaged programming language such as C or C++. In such contexts, even transactions that ultimately abort must observe consistent states of memory; otherwise, unrecoverable errors such as divide-by-zero may occur before a transaction aborts, even in a correct program in which the error would not be possible if transactions were executed atomically. We specify TMS1 precisely using an I/O automaton (IOA). This approach enables us to also model TM implementations using IOAs and to construct fully formal and machine-checked correctness proofs for them using well established proof techniques and tools. We outline key requirements for a TM system. To avoid precluding any implementation that satisfies these requirements, we specify TMS1 to be as general as we can, consistent with these requirements. The cost of such generality is that the condition does not map closely to intuition about common TM implementation techniques, and thus it is difficult to prove that such implementations satisfy the condition. To address this concern, we present TMS2, a more restrictive condition that more closely reflects intuition about common TM implementation techniques. We present a simulation proof that TMS2 implements TMS1, thus showing that to prove that an implementation satisfies TMS1, it suffices to prove that it satisfies TMS2. We have formalised and verified this proof using the PVS specification and verification system.

We develop a mechanized proof of Featherweight Java with Assignment and Immutability in the Coq proof assistant. This is a step towards more machine-checked proofs of a non-trivial type system. We used object immutability close to that of IGJ [9]. We describe the challenges of the mechanisation and the encoding we used inside of Coq.

Large, unwieldy classes are a significant maintenance problem. Programmers dislike them because the fundamental logic is often obscured, making them hard to understand and modify. This paper proposes a solution - a semi-automatic technique for splitting large classes into smaller, more cohesive ones. The core of the technique is the use of betweenness clustering to identify the best way of partitioning a class. This turned a tedious manual process into a quick and simple semi-automated one in roughly one third of the cases we examined.

Abstract We show how a sophisticated, lock-free concurrent stack implementation can be derived from an abstract specification in a series of verifiable steps. The algorithm is based on the scalable stack algorithm of Hendler et al. (Proceedings of the sixteenth annual ACM symposium on parallel algorithms, 27–30 June 2004, Barcelona, Spain, pp 206–215), which allows push and pop operations to be paired off and eliminated without affecting the central stack, thus reducing contention on the stack, and allowing multiple pairs of push and pop operations to be performed in parallel. Our algorithm uses a simpler data structure than Hendler, Shavit and Yerushalmi’s, and avoids an ABA problem. We first derive a simple lock-free stack algorithm using a linked-list implementation, and discuss issues related to memory management and the ABA problem. We then add an abstract model of the elimination process, from which we derive our elimination algorithm. This allows the basic algorithmic ideas to be separated from implementation details, and provides a basis for explaining and comparing different variants of the algorithm. We show that the elimination stack algorithm is linearisable by showing that any execution of the implementation can be transformed into an equivalent execution of an abstract model of a linearisable stack. Each step in the derivation is either a data refinement which preserves the level of atomicity, an operational refinement which may alter the level of atomicity, or a refactoring step which alters the structure of the system resulting from the preceding derivation. We verify our refinements using an extension of Lipton’s reduction method, allowing concurrent and non-concurrent aspects to be considered separately.

The dramatic expansion of semistructured data has led to the development of database systems for manipulating the data. Despite its huge potential, there is still a lack of formality and verification support in the design of good semistructured databases. Like traditional database systems, developed semistructured database systems should contain minimal redundancies and update anomalies, in order to store and manage the data effectively. Several normalization algorithms have been proposed to satisfy these needs, by transforming the schema of the semistructured data into a better form. It is essential to ensure that the normalized schema remains semantically equivalent to its original form. In this paper, we present tool support for reasoning about the correctness of semistructured data normalization. The proposed approach uses the ORA-SS data modeling notation and defines its correctness criteria and rules in the PVS formal language. It further utilizes the PVS theorem prover to perform automated checking on the normalized schema, checking that functional dependencies are preserved, no data is lost and no spurious data is created. In summary, our approach not only investigates the characteristics of semistructured data normalization, but also provides a scalable and automated first step towards reasoning about the correctness of normalization algorithms on semistructured data.

Reduction methods developed by Lipton, Lamport, Cohen, and others, allow one to reason about concurrent programs at various levels of atomicity. An action which is considered to be atomic at one level may be implemented by more complex code at the next level. We can show that certain properties of the program are preserved by first showing that the property holds when the expanded code is executed sequentially, and then showing that any execution in which this code is executed concurrently with other processes is equivalent to an execution in which the expanded code is executed without interruption. Existing reduction methods are aimed at traditional approaches to concurrency which prevent interference between concurrent processes using mechanisms such as locks or semaphores. In this paper, we show that these reduction methods can be adapted to reason about nonblocking algorithms, which are designed to operate correctly in the presence of interference, rather than to avoid interference. These algorithms typically use strong synchronisation primitives, such as Load Linked/Store Conditional or Compare and Swap, to detect that interference has occurred and in that case retry their operations. We show that reduction can be used with such algorithms, and illustrate this approach with examples based on shared counters and stacks.

The design of efficient software supporting concurrent access to shared data is a challenging task. Often such programs will have at their core algorithms which utilise conceptual locks to restrict access to the data, and which are significantly more complex than their sequential (non-concurrent) counterparts. Lock-free algorithms, which have been developed to avoid problems such as priority inversion and deadlock, are more complex still due to the larger scope for interference between processes. These algorithms become even more complex when further mechanisms are added to achieve good performance under a wide range of workloads. In this paper we present a lock-free algorithm that efficiently manages interference on a shared stack, by allowing complementary stack operations to be eliminated without altering the stack. The algorithm we present is based on a published algorithm due to Hendler, Shavit and Yerushalmi (2004), and incorporates simplifications and improvements that we discovered while attempting to verify the original algorithm. We present a high-level view of the formal verification of our algorithm, which was machine-checked using the PVS theorem prover.

We describe an array-based nonblocking implementation of a concurrent bounded queue, due to Shann, Huang and Chen (2000), and explain how we detected errors in the algorithm while attempting a formal verification. We explain how we first corrected the errors, and then modified the algorithm to obtain nonblocking behaviour in the boundary cases. Both the corrected and modified versions of the algorithm were verified using the PVS theorem proven. We describe the verification of the modified algorithm, which subsumes the proof of the corrected version.

Despite years of research, the design of efficient nonblocking algorithms remains difficult. A key reason is that current shared-memory multiprocessor architectures support only single-location synchronisation primitives such as compare-and-swap (CAS) and load-linked/store-conditional (LL/SC). Recently researchers have investigated the utility of double-compare-and-swap (DCAS)--a generalisation of CAS that supports atomic access to two memory locations -- in overcoming these problems. We summarise recent research in this direction and present a detailed case study concerning a previously published nonblocking DCAS-based double-ended queue implementation. Our summary and case study clearly show that DCAS does not provide a silver bullet for nonblocking synchronisation. That is, it does not make the design and verification of even mundane nonblocking data structures with desirable properties easy. Therefore, our position is that while slightly more powerful synchronisation primitives can ave a profound effect on ease of algorithm design and verification, DCAS does not provide sufficient additional power over CAS to justify supporting it in hardware.

This paper presents a systematic approach to implementing certain kinds of program modifications, in which (conceptually at least) the modification is implemented as a separate program and then integrated with the original program using semantically based transformations. This approach allows us to ensure that the required modification is implemented correctly and also allows us to explore different ways of implementing a given modification. The approach is illustrated informally using an example where the modification can be implemented in two distinct ways, and then formalised within the refinement calculus by defining a program conjunction operator whose properties justify the transformations required in the example.

Although program refinement is usually presented as a top-down process, real programs are usually constructed by extending, adapting and combining existing programs. We show how this kind of program development can be performed within the refinement calculus using editable refinement scripts, which can be extended, adapted and combined in this way. Our approach is illustrated by a sequence of examples, beginning with a list insertion algorithm and culminating in a stable sorting algorithm.