UPMARC Workshop on Memory Models (MM'15)

Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Yet programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop a polynomial-time (per execution) approximation to refinement checking. The approximation is parameterized by an accuracy k ∈ N representing the degree to which refinement violations are visible. In principle, more violations are detectable as k increases, and in the limit, all are detectable. Our insight for this approximation arises from foundational properties on the partial orders characterizing the happens-before relations between object invocations: they are interval orders, with a well defined measure of complexity, i.e., their length. Approximating the happens-before relation with a possibly-weaker interval order of bounded length can be efficiently implemented by maintaining a bounded number of integer counters. In practice, we find that refinement violations can be detected with very small values of k, and that our approach scales far beyond existing refinement-checking approaches. This is joint work with Ahmed Bouajjani, Michael Emmi, and Jad Hamza.

Modern Internet services often rely on geo-replicated databases that provide consistency models for transactions weaker than serialisability. We investigate a promising consistency model of Parallel Snapshot Isolation (PSI), which weakens the classical snapshot isolation in a way that allows more efficient geo-replicated implementations: - We give a declarative specification to PSI that does not refer to implementation-level concepts and thus allows reasoning about the behaviour of PSI databases more easily. - Using our specification, we propose a criterion for checking when an application using a PSI database exhibits only serialisable behaviours. - We additionally propose a criterion for checking when a set of transactions executing on PSI can be chopped into smaller pieces without introducing new behaviours, thus improving performance. This is joint work with Andrea Cerone (IMDEA), Giovanni Bernardi (IMDEA) and Hongseok Yang (Oxford).

Replicating modifiable data is a challenge in large-scale distributed systems, as it suffers from a fundamental tension between availability and data consistency. Eventual consistency sidesteps the problem of availability under network partitioning, but remains ad-hoc, error-prone, and difficult to apply for programmers. In this talk, we will review replicated data types that require no blocking synchronization: an update can execute immediately, irrespective of network latency, faults, or disconnection; this approach is highly scalable and fault-tolerant. In discussing several use cases, we will see benefits and limitations of this approach and outline recent results. Related project: https://syncfree.lip6.fr

The cache coherence protocol is a hardware mechanism present in shared memory multiprocessors, that ensures that memory operations are made visible to not only the processor that has initiated it, but also to other processors. Traditional coherence protocols are designed for the strictest consistency model, sequential consistency (SC). When they are used for processors that support relaxed memory consistency models, such protocols turn out to be unnecessarily strict at the cost of scalability (in terms of per core storage), which poses a problem with increasing number of cores in today’s CMPs. Because of the wide adoption of Total Store Order (TSO) and its variants in x86 processors, we propose TSO-CC, a cache coherence protocol for the TSO memory consistency model. TSO-CC relies on self-invalidation and detection of potential acquires using timestamps to satisfy the TSO memory consistency model lazily. Our results show that TSO-CC achieves average performance comparable to a conventional (MESI directory protocol), while TSO-CC’s storage overhead per cache line scales logarithmically with increasing core count. We will conclude by outlining the challenges of verifying such consistency-directed (and also conventional) coherence protocols.

TBA

Cache coherence protocols based on self-invalidation allow a simpler design compared to traditional invalidation-based protocols, by relying on data-race-free (DRF) semantics and applying self-invalidation on racy synchronization points ex- posed to the hardware. Their simplicity lies in the absence of invalidation traffic, which eliminates the need to track readers in a directory, and reduces the number of transient protocol states. With the addition of self-downgrade these protocols can become effectively directory-free. While this works well for race-free data, unfortunately, lack of explicit invalidations compromises the effectiveness of any synchronization that re- lies on races. This includes any form of spin waiting, which is employed for signaling, locking, and barrier primitives. In this work we propose a new solution for spin-waiting in these protocols, the callback mechanism, that is simpler and more efficient than explicit invalidation. Callbacks are set by reads involved in spin waiting, and are satisfied by writes (that can even precede these reads). To implement callbacks we use a small (just a few entries) directory-cache structure that is intended to service only these “spin-waiting” races. This directory structure is self-contained and is not backed up in any way. Entries are created on demand and can be evicted without the need to preserve their information. Our evaluation shows a significant improvement both over explicit invalidation and over exponential back-off, the state-of-the-art mechanism for self-invalidation protocols to avoid spinning in the shared cache.

Existing multi-threaded applications perform synchronization either in an explicit way, e.g., making use of the functionality provided by synchronization libraries or in an implicit or ``covert'' way, e.g., using shared variables. Unfortunately, the implicit synchronization constructs are prone to errors and difficult to detect. This talk presents a tool that is able to detect implicit synchronization in multi-threaded applications. The detection is performed by ensuring that during the execution of an application under a memory model that provides sequential consistency for data-race-free applications (SC for DRF), every read returns the same value as if running under sequential consistency. If the previous condition is not fulfilled by the execution, the application has data races, which may be intended to perform implicit synchronization. We analyze the applications in the Splash2 benchmark suite with the presented tool and we detect data races in 7 out of the 14 Splash2 applications. These data races perform implicit synchronization in all but one of the applications (6 out of 7). We analyze these implicit synchronization constructs and discuss their correctness.

This talk concerns the adaptation of the Owicki-Gries method for verifying concurrent programs to the release-acquire weak memory model. We show that the standard Owicki-Gries non-interference check is unsound even for TSO, but that a slightly stronger check is not only sound for the release-acquire memory model, but is also actually useful for verifying a number of intricate examples.

Memory models may be specified operationally or axiomatically. Psi calculi provide a unified framework that supports formal verification for a range of specification styles. We have instantiated psi calculi to obtain a bespoke process calculus, which we have used to model the MESI cache coherence protocol at different levels of abstraction. Our modeling language conveniently supports both a monolithic and a distributed view of the protocol. Sequential consistency of the protocol is established through a simulation proof.

There is a joke where a physicist and a mathematician are asked to herd cats. The physicist starts with an infinitely large pen which he reduces until it is of reasonable diameter yet contains all the cats. The mathematician builds a fence around himself and declares the outside to be the inside. Defining memory models is akin to herding cats: both the physicist's or mathematician's attitudes are tempting, but we cannot rely on one more than on the other. I have mostly been involved in studying weak memory (i.e. the execution models of multiprocessors). Understanding precisely what our machines guarantee is crucial for writing correct programs, especially since weak memory forces us to revise the programming model that we have been taught at school, namely Lamport's Sequential Consistency. In this talk, I will show ways of defining formal models for weak memory, within a generic framework in which one can represent for example Sequential Consistency (SC), Intel x86 (i.e. Sparc Total Store Order, TSO), IBM Power, ARM, C++ and GPUs. I will then present some work on how to exploit these models for devising tools to verify concurrent programs. Parts of this talk are joint work with Luc Maranget, others with Daniel Kroening, Vincent Nimal, Daniel Poetzl and Michael Tautschnig.

We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Chronological traces induce a partial order relation on relaxed memory executions, capturing dependencies that are needed to represent the interaction via shared variables. They are optimal in the sense that they only distinguish computations that are inequivalent under the widely-used representation by Shasha and Snir. This allows an optimal dynamic partial order reduction algorithm to explore a minimal number of executions while still guaranteeing full coverage. We apply our techniques to check, under the TSO and PSO memory models, LLVM assembly produced for C/pthreads programs. Our experiments show that our technique reduces the verification effort for relaxed memory models to be almost that for the standard model of sequential consistency. In many cases, our implementation significantly outperforms other comparable tools.

For performance reasons, modern multiprocessors implement relaxed memory consistency models that admit out-of-program-order and non-store atomic executions. While data race-free programs are not sensitive to these relaxations, they pose a serious problem to the development of the underlying concurrency libraries. Library routines that work correctly under Sequential Consistency (SC) show undesirable effects when run under a relaxed memory model. These routines are not robust against the relaxations that the processor supports. To enforce robustness, the programmer has to add safety net instructions to the code that control the hardware --- a task that has proven to be difficult, even for experts. We recently developed algorithms that check and, if necessary, enforce robustness against prominent relaxed memory models like TSO implemented in x86 processors and Power implemented in IBM architectures. Given a program, our algorithms decide whether the actual behavior on the processor coincides with the SC semantics. If this is not the case, they synthesize safety net instructions that enforce robustness. When built into a compiler, our algorithms thus hide the relaxed memory model from the programmer and provide the illusion of Sequential Consistency. In this talk, we motivate the robustness problem and explain how to reduce it to a standard SC reachability query.

We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving (SC) semantics. We instantiate our framework for the Total Store Ordering (TSO) memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes. Based on our method, we have implemented a tool and run it successfully on a wide range benchmarks. The experimental results confirm the superiority of our tool compared to existing tools for analysis of programs running under TSO.