DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.23

When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency

Authors: Luke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, and Matthew J. Parkinson

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract

Behaviour-oriented concurrency (BoC) is a recently established programming model in which programmers define concurrent operations that execute atomically across multiple isolated resources. This allows for expressive interactions but introduces complex causal dependencies determined by dynamic resource overlap. Previous work defines the causal guarantees of BoC operationally, but mixes intended design constraints with incidental implementation details, leading to unintended causal orders. BoC is now being implemented across multiple languages and runtimes, all relying on the operational descriptions of causality. This paper develops an axiomatic model of BoC executions that makes the intrinsic orders explicit and derives the intended causal relation from their interaction. Using a set of representative programs and candidate executions, we motivate the design of this causal relation. We then prove that a representative minimal core calculus for BoC is sound with respect to this axiomatic model. Together, these results provide an implementation-independent foundation for reasoning about BoC causality across runtimes, schedulers and optimisation decisions.

Cite as

Luke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, and Matthew J. Parkinson. When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cheeseman_et_al:LIPIcs.CONCUR.2026.23,
  author =	{Cheeseman, Luke and Castegren, Elias and Wrigstad, Tobias and Drossopoulou, Sophia and Parkinson, Matthew J.},
  title =	{{When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.23},
  URN =		{urn:nbn:de:0030-drops-273549},
  doi =		{10.4230/LIPIcs.CONCUR.2026.23},
  annote =	{Keywords: Concurrency, Parallelism, Language Design, Causality}
}

Search Results

Documents authored by Cheeseman, Luke

When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency

Abstract

Cite as

Thanks for your feedback!

Could not send message