Track: Concurrency verification papers

[rikosellic]

To push our verification to the extreme, we should consider all the levels of concurrency (concurrent algorithms, weak memory models, multiprocessors). Not all of these are guaranteed to be doable in Verus, but we should at least learn and understand the extent to which the PL community has accomplished in concurrent reasoning.

This issue tracks a list of papers about concurrency verification, which I think is worth reading.

• x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors : a formalized model for x86 multiprocessor. (Communications of the ACM, 2010)
• Mathematizing C++ Concurrency: formalization of C/C++ 11 concurrency memory model. (POPL 2011)
• Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning: the first paper of the ground-breaking concurrent separation logic framework Iris. (POPL 2015)
• Verifying Read-Copy-Update in a Logic for Weak Memory: the first formalization of RCU under weak memory model (acquire-release). (PLDI 2015)
• Iris from the ground up: an extremely long technical report that covers every detail of Iris 3.1. (2018)
• The Future is Ours: Prophecy Variables in Separation Logic: the implementation of prophecy variable in Iris. (POPL 2020)
• Leaf: Modularity for Temporary Sharing in Separation Logic: the extension of shared resource in Iris, the theortical foundation of VerusSync.
• Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems: the design of tokenized_state_machine in VerusSync.
• Verifying Concurrent System Code: the doctoral thesis that covers the theoretical foundation of Verus. (2024)
• Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic: the first verification of RCU on a relaxed memory model built upon Iris. (PLDI 2025)
• VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System: the soundness proof of Verus constructs with Iris. (PLDI 2026)

There are some other papers which I have not investigated yet or not so closely related: RusBelt, RustHornBelt, Stacked Borrows, Tree Borrows, etc. CertiKOS seems to take a different approach (concurrent certified abstraction layer, which seems closer to CompCert) that deviates from the Iris technology roadmap.

[hiroki-chen]

Thanks for the shortlist!