Concurrency and Memory Models
Concurrency and memory models define how concurrent programs are structured and how their interacting threads observe shared memory, underpinning correct parallel software.
Definition
Concurrency models describe how independently executing computations are composed and communicate, while a memory model specifies which values reads may observe when concurrent threads access shared memory, defining the contract between programmer, language, and hardware.
Scope
This area covers the language and theory of concurrency: process calculi and concurrency models for communication and synchronization, memory consistency models that specify the allowed orderings of memory operations, synchronization mechanisms and data-race freedom, and type systems for concurrency such as session types. It addresses how languages give meaning to programs that execute simultaneously and share state.
Sub-topics
Core questions
- How can concurrent communicating processes be modeled and reasoned about?
- What orderings of memory operations may a program observe?
- How is freedom from data races guaranteed or specified?
- How can types discipline communication and prevent concurrency errors?
Key theories
- Process calculi
- Hoare's CSP and Milner's CCS and pi-calculus provide algebraic theories of concurrent, communicating processes, with operators for composition and synchronization and notions of behavioral equivalence such as bisimulation.
- Sequential consistency
- Lamport defined sequential consistency as the requirement that a multiprocessor execution appear as some interleaving of each processor's operations in program order, the baseline against which weaker memory models are compared.
- Memory consistency models
- Adve and Gharachorloo systematize the spectrum of shared-memory consistency models, explaining how relaxed orderings enable performance while complicating reasoning about concurrent programs.
Clinical relevance
Memory models are now part of mainstream language specifications (for example in C++ and Java) because multicore hardware made relaxed orderings observable; getting them right is essential for correct, portable concurrent software. Process calculi and session types inform the design of message-passing languages and protocols.
History
Concurrency theory grew from Petri nets and the 1970s work of Hoare (CSP) and Milner (CCS), later the pi-calculus for mobile processes. Lamport defined sequential consistency in 1979; as relaxed hardware proliferated, memory models were formalized for languages such as Java and C++ in the 2000s, and weak-memory semantics became an active research area.
Debates
- Strong versus relaxed memory consistency
- Designers trade the intuitive simplicity of strong models like sequential consistency against the performance of relaxed models that permit reordering, which complicate reasoning and require careful language-level semantics.
Key figures
- C. A. R. Hoare
- Robin Milner
- Leslie Lamport
- Sarita Adve
Related topics
Seminal works
- hoare1978
- milner1989
- lamport1979
- adve1996
Frequently asked questions
- What is a memory model?
- A memory model is the formal contract that specifies which values a read can return when multiple threads access shared memory, defining what reorderings the compiler and hardware may perform and what the programmer can rely on.
- What is sequential consistency?
- Sequential consistency requires that a concurrent execution behave as some single interleaving of the threads' operations that respects each thread's program order, making it the most intuitive (but often relaxed) memory model.