A Brief Survey of Formal Models of Concurrency
Charles Averill
TL;DR
This survey contrasts four foundational formalisms for concurrency—Hoare’s axiomatic parallel programming, Milner’s π-calculus, O’Hearn’s Separation Logic extension, and the Iris framework—highlighting their approaches to modeling interaction, ownership, and invariants. It analyzes each model’s generality, simplicity, and impact on networking and formal verification, showing a trajectory from simple, rule-based reasoning to a highly expressive, machine-checked paradigm. The work underscores the trade-offs between accessibility and expressiveness, noting Iris as the most general and mechanizable, albeit complex. Overall, the paper maps how formal concurrency models evolved to support rigorous reasoning about real-world networking programs and security-critical infrastructures.
Abstract
The ubiquity of networking infrastructure in modern life necessitates scrutiny into networking fundamentals to ensure the safety and security of that infrastructure. The formalization of concurrent algorithms, a cornerstone of networking, is a longstanding area of research in which models and frameworks describing distributed systems are established. Despite its long history of study, the challenge of concisely representing and verifying concurrent algorithms remains unresolved. Existing formalisms, while powerful, often fail to capture the dynamic nature of real-world concurrency in a manner that is both comprehensive and scalable. This paper explores the evolution of formal models of concurrency over time, investigating their generality and utility for reasoning about real-world networking programs. Four foundational papers on formal concurrency are considered: Hoare's Parallel programming: An axiomatic approach, Milner's A Calculus of Mobile Processes, O'Hearn's Resources, Concurrency and Local Reasoning, and the recent development of Coq's Iris framework.