A Brief Survey of Formal Models of Concurrency

TL;DR

This survey reviews the evolution of formal models of concurrency, highlighting their importance in ensuring the safety of networking infrastructure and discussing their ability to represent real-world concurrent systems.

Contribution

It provides a comprehensive overview of key formal models of concurrency, analyzing their development, strengths, and limitations for reasoning about networking programs.

Findings

Formal models have evolved to better capture real-world concurrency.

Existing formalisms vary in their scalability and expressiveness.

The survey discusses foundational frameworks like Hoare's, Milner's, O'Hearn's, and Iris.

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.