KnowledgeBase » SEMINAR » ID = 495

A Formal Framework for Modeling Memory

by Victor Luchangco
1998-1999

Abstract:

A memory consistency model specifies the semantics of concurrent access by multiple processors to shared data. One simple and intuitive model, sequential consistency, requires the memory to appear as if all accesses are handled by a single process in an order consistent with program order. However, this is expensive to maintain, and most multiprocessors instead provide relaxed models, allowing operations to be re-ordered and different processors to see different orderings.

Unfortunately, many models merely describe the underlying hardware, rather than providing a simple, abstract model that is easy to reason with. In this talk, I outline a formal framework for describing memory models intended to enable programmers to reason rigorously about their programs, and implementors to determine what guarantees their systems provide. The framework uses the notion of a computation to generalize the usual assumption of multiple sequential instruction streams, allowing us to model systems such as Cilk that do not make processors explicit, and to treat nonblocking and concurrent memory access uniformly.

I will begin by showing how to model precedence-based memories, which can express any conditions that rely only on operations being required to precede other operations. This is sufficient to express sequentially consistent memory, even when enriched with fork/join or similar constructs. I will then show how to incorporate locks, and indicate several results that can be proven within this framework.