This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behavior, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalize in Rocq. This method can be seen as a specialized induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviours by standard techniques.
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | |||
14:00 22mTalk | Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis CPP | ||
14:22 22mTalk | Enhancing Symbolic Execution with Machine-Checked Safety Proofs CPP Pre-print | ||
14:45 22mTalk | Layers of Confluence for Actors CPP Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Einar Broch Johnsen University of Oslo, Åsmund Aqissiaq Arild Kløvstad University of Oslo (UiO), Violet Ka I Pun Western Norway University of Applied Sciences, Yannick Zakowski Inria | ||
15:07 22mTalk | Towards composable proofs of cache coherence protocols CPP | ||