Reference. Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing
Mixed choice multiparty message passing is an expressive concurrency programming paradigm where components use non-determinism to choose between concurrent options for sending and receiving messages. This flexibility makes it possible to program advanced algorithms, such as leader election protocols, succinctly. We present Mixtris, a mechanised higher-order separation logic for reasoning about functional correctness of higher-order imperative programs with mixed choice multiparty message passing in a shared memory setting. Mixtris builds upon recent work on separation logic for (non-mixed choice) multiparty message-passing programs, by drawing inspiration from session type systems for mixed choice multiparty message-passing programs. Mixtris is the first program logic for mixed choice multiparty message passing. We prove soundness of Mixtris using a novel model of our mixed choice multiparty protocols. We demonstrate how Mixtris can be used to formally reason about challenging examples, including some leader election protocols such as Chang and Roberts’s ring leader election protocol. All the results in the paper (both meta-theory and examples) have been formalised in the Rocq proof assistant on top of the Iris program logic framework.
Cite
Cites 40 works (4 here)
With notes (4)
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols gondelman-2023-verifying
We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top of UDP and features characteristic traits of existing protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission/acknowledgement mechanisms. We verify the library in the Aneris distributed separation logic using a novel proof pattern—dubbed the session escrow pattern—based on the existing escrow proof pattern and the so-called dependent separation protocols, which hitherto have only been used in a non-distributed concurrent setting. We demonstrate how our specification of the reliable communication library simplifies formal reasoning about applications, such as a remote procedure call library, which we in turn use to verify a lazily replicated key-value store with leader-followers and clients thereof. Our development is highly modular—each component is verified relative to specifications of the components it uses (not the implementation). All our results are formalized in the Coq proof assistant.
Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
Higher-order ghost state jung_higher-order_2016
The development of concurrent separation logic (CSL) has sparked a long line of work on modular verification of sophisticated concurrent programs. Two of the most important features supported by several existing extensions to CSL are higher-order quantification and custom ghost state. However, none of the logics that support both of these features reap the full potential of their combination. In particular, none of them provide general support for a feature we dub “higher-order ghost state”: the ability to store arbitrary higher-order separation-logic predicates in ghost variables. In this paper, we propose higher-order ghost state as a interesting and useful extension to CSL, which we formalize in the framework of Jung et al.‘s recently developed Iris logic. To justify its soundness, we develop a novel algebraic structure called CMRAs (“cameras”), which can be thought of as “step-indexed partial commutative monoids”. Finally, we show that Iris proofs utilizing higher-order ghost state can be effectively formalized in Coq, and discuss the challenges we faced in formalizing them.
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-iris
External (36)
- Rocq Mechanisation of "Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing" (2026)
- Modular Multiparty Sessions with Mixed Choice (2025)
- Clojure (https://clojure.org) (2025)
- The Go programming language (https://go.dev) (2025)
- Iris HeapLang documentation (heap_lang.md) (2025)
- The Rocq Prover (https://rocq-prover.org) (2025)
- Multris: Functional Verification of Multiparty Message Passing in Separation Logic (2024)
- Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing (2024)
- Separation and Encodability in Mixed Choice Multiparty Sessions (2024)
- Synthetic Behavioural Typing: Sound Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea) (2023)
- Safe Asynchronous Mixed-Choice for Timed Interactions (2023)
- Multiparty GV: functional multiparty session types with certified deadlock freedom (2022)
- Machine-checked semantic session typing (2021)
- Generalising Projection in Asynchronous Multiparty Session Types (2021)
- Discourje: Runtime Verification of Communication Protocols in Clojure (2020)
- Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic (2020)
- Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types (2020)
- Less is more: multiparty session types revisited (2019)
- MoSeL: a general, extensible modal framework for interactive proofs in separation logic (2018)
- Modular Reasoning about Separation of Concurrent Data Structures (2013)
- On Global Types and Multi-Party Sessions (2012)
- Is it a "Good" Encoding of Mixed Choice? (Technical Report) (2012)
- Propositions as sessions (2012)
- Linear type theory for asynchronous session types (2009)
- Parallel concurrent ML (2009)
- A randomized encoding of the Pi-calculus with mixed choice (2005)
- Comparing the expressive power of the synchronous and asynchronous $pi$-calculi (2003)
- Foundational proof-carrying code (2001)
- What is a "Good" Encoding of Guarded Choice? (2000)
- A Facile Tutorial (1996)
- Fault-Tolerant Algorithms for Fair Interprocess Synchronization (1994)
- A Distributed Protocol for Channel-Based Communication with Choice (1992)
- A calculus of mobile processes, I (1992)
- Consensus in the presence of partial synchrony (1988)
- An Effective Implementation for the Generalized Input-Output Construct of CSP (1983)
- An improved algorithm for decentralized extrema-finding in circular configurations of processes (1979)