Saturday, January 29, 2011
Austin, Texas, USA
Co-located with POPL 2011
Paul McKenney, IBM
The advent of low-cost readily available multicore hardware has brought new urgency to the question of validating parallel software. The traditional validation approaches leverage linearizability, commutativity, lock freedom, and wait freedom, each of which has attractive theoretical properties, but which collectively suffer from the minor shortcoming of being unable to address some common parallel-programming techniques that are used in practice. This talk will discuss what might be done to bridge this researcher-practitioner divide from the viewpoint of a practitioner with 20 years of parallel-programming experience.
Martin Rinard, MIT
Commuting operations play a critical role in many parallel computing systems. We present a new technique for verifying commutativity conditions, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not identical) data structure states in different execution orders. We have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList). This effort involved the specification and verification of 765 commutativity conditions. Many speculative parallel systems need to undo the effects of speculatively executed operations. Inverse operations, which undo these effects, are often more efficient than alternate approaches (such as saving and restoring data structure state). We present a new technique for verifying such inverse operations. We have specified and verified, for all of our linked data structure implementations, an inverse operation for every operation that changes the data structure state. Together, the commutativity conditions and inverse operations provide a key resource that language designers and system developers can draw on to build parallel languages and systems with strong correctness guarantees.
Milind Kulkarni, Purdue
Speculative execution is a promising approach for exploiting parallelism in many programs, but it requires efficient schemes for detecting conflicts between concurrently executing threads. Prior work has argued that checking semantic commutativity of method invocations is the right way to detect conflicts for complex data structures such as kd-trees. Several ad hoc ways of checking commutativity have been proposed in the literature, but there is no systematic approach for producing implementations.
In this paper, we describe a novel framework for reasoning about commutativity conditions: the commutativity lattice. We show how commutativity specifications from this lattice can be systematically implemented in one of three different schemes: abstract locking, forward gatekeeping and general gatekeeping. We also discuss a disciplined approach to exploiting the lattice to find different implementations that trade off precision in conflict detection for performance. Finally, we show that our novel conflict detection schemes are practical and can deliver speedup on three real-world applications.
Victor Luchangco, Oracle
In a transactional memory system, a programmer can designate a block of code to be executed as a transaction. The system guarantees that transactions appear to execute in isolation, so that no transaction can see internal transitions of other transactions. This greatly simplifies reasoning about concurrent programs because transactions only interact at their boundaries. Verification of programs using transactional memory consists of two parts: verification of the program given a specification of the transactional memory and verification that the transactional memory system correctly implements its specification. Unfortunately, although transactional memory has been the subject of active research for several years now, work on both these parts is sadly lacking. First, there is no consensus on exactly what transactional memory should guarantee, and indeed, it seems likely that different guarantees are appropriate for different systems. Second, no real transactional memory system has been carefully verified. Rather, all that exists are informal arguments that these systems satisfy some properties, which themselves are sometimes poorly defined.
In this talk, I will point out some of the challenges of specifying and verifying transactional memory systems, and I'll describe our nascent work on formally encoding transactional memory specifications and algorithms, and verifying that the latter satisfy the former using the PVS system. This work builds on our earlier work on verifying lock-free concurrent data structures using PVS.
Matthew Parkinson, Microsoft
In recent years, separation logic has brought great advances in the world of verification. However, there is a disturbing trend for each new library or concurrency primitive to require a new separation logic. In this talk, I will discuss recent advances in separation logic that have allowed concurrency primitives to abstract from their low-level implementation. So instead of producing new logics for each concurrency construct, we can use a single logic and verify the construct meets an abstract specification.
This is talk is based on joint work with Mike Dodds, Thomas Dinsdale-Young, Xinyu Feng, Philippa Gardner and Viktor Vafeiadis.
Marc Shapiro, INRIA
Replicating shared data is a fundamental mechanism in large-scale distributed systems, but suffers from a fundamental tension between scalability and data consistency. Eventual consistency sidesteps the (foreground) synchronisation bottleneck, but remains ad-hoc, error-prone, and difficult to prove correct.
We present a promising new approach that is simple, scales almost indefinitely, and provably ensures eventual consistency: A CRDT is a data type that demonstrates some simple properties, viz. that its concurrent operations commute, or that its states form a semi-lattice. Any CRDT provably converges, provided all replicas eventually receive all operations. A CRDT requires no synchronisation: an update can execute immediately, irrespective of network latency, faults, or disconnection; it is highly scalable and fault-tolerant.
The approach is necessarily limited since any task requiring consensus is out of reach. Nonetheless, many interesting and useful data types can be designed as a CRDT. We previously published the Treedoc CRDT, a sequence data type suited to concurrent editing tasks (as in a p2p wiki). This talk presents a portfolio of generally-useful, non-trivial, composable CRDTs, including variations on counters, registers, sets, maps (key-value stores), graphs and sequences. This research is part of a systematic and principled study of CRDTs, to discover their power and limitations, and to better understand the underlying mechanisms and requirements. The challenges ahead include scaling garbage collection and integrating occasional non-commuting operations.
This is joint work with Marek Zawirski of LIP6, Nuno Preguiça of Universidade Nova de Lisboa, and Carlos Baquero, of Universidade do Minho. The research is supported by ANR grant ConcoRDanT (ANR-10-BLAN-0208), a Google Research Award 2009, and a Google European Doctoral Fellowship 2010.
Commutativity of operations is a way to provide a high degree of concurrency on shared data types. We present a technique to increase concurrency using operational transformations. This technique enforces commutativity even though the operations do not naturally commute. We report our experience on (i) automatically verifying the correctness of this transformation-based commutativity and (ii) developing new applications based on operational transformations.
Shared-memory concurrency plays an important role in modern computer systems: for example, in classic file systems and databases, and the evolving web and multi-core operating systems. Many of these systems make fundamental use of concurrent indexes. A concurrent index can be viewed as a mapping from key-values to data (typically pointers), which can be accessed simultaneously by many threads calling read/write operations on key-values. A user typically works with this abstract view of indexes, rather than with the intricate details of complex implementations. We could verify such implementations directly, but we instead choose to give a formal abstract specification of concurrent indexes, and verify that well-known implementations using B-Link trees and hash tables satisfy this specification.
In this talk, we give an abstract specification for concurrent indexes, and prove that it is satisfied by concrete implementations. Our specification captures high-level sharing of index elements, allowing collaboration between threads. We show that a widely-used implementation based on B-Link trees is correct with respect to our abstract specification.
The formal verification of concurrent datatypes is a challenging software verification problem. The difficulty comes from the combination of complex dynamic memory manipulation and the rather unstructured concurrent executions performed by an unbounded number of threads. On top of that, we are aiming at temporal verification, proving not only safety properties but also liveness properties of concurrent datatypes.
Separation logic and specialized algorithms for pointer reasoning have been two successful approaches to verify sequential heap-manipulating programs. Building on this success, most current efforts for the verification of concurrent datatypes try to extend these program logics with capabilities for concurrency.
In our work, we propose a complementary approach. We start from a powerful framework for the temporal verification of concurrent systems: the Manna-Pnueli style of temporal deductive verification, particularly using verification diagrams. We extend this framework to deal with pointer structures and an unbounded number of threads. The proof represented by a verification diagram is decomposed into proving a collection of verification conditions expressed in a first-order logic of predicates over states. To automate this process, it is crucial to use decision procedures that can handle pointer structures and that can be combined with decision procedures for other theories, like sets of values, sets of threads, memory regions, etc.