A Formal Executable Semantics of PROMELA
summary
Provides an executable, interpreter-like semantics of PROMELA mechanized in the K framework and based on a new Load-and-Fire pattern over forked continuations that makes guarded nondeterminism, cross-process interference, and atomic actions explicit. From this semantics K automatically generates a model checker and a deductive verifier; the verifier proves Lamport’s bakery mutual exclusion (infinite state) in about five minutes, a result that SPIN’s explicit-state model checking cannot achieve.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:50SPIN limitations
- 3:57PROMELA core features
- 6:04Executable semantics challenges
- 9:34Load and fire pattern
- 12:46Load and fire example
- 17:43Mechanizing in K
- 19:30Bakery algorithm case study
- 21:17Conclusion
- 22:19Q&A
related talks
23mA Reachability Logic for a Weak Memory Model with Promises
31mProgramming with Explicit Effects in ReML
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
21mMechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
20mThe Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc
21mCSL and relaxed memory