Search Results

Documents authored by Castegren, Elias

Artifact
Software
DOI: 10.4230/artifacts.27655
A Mechanised Axiomatic Model for Behaviour-Oriented Concurrency

Authors: Elias Castegren

Abstract
Cite as

Elias Castegren. A Mechanised Axiomatic Model for Behaviour-Oriented Concurrency (Software, Proofs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{mechanisation,
   title = {{A Mechanised Axiomatic Model for Behaviour-Oriented Concurrency}}, 
   author = {Castegren, Elias},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:24350cf7167ab1b9d00f8a2d64cc3fe32dfb4560;origin=https://github.com/fxpl/axiomatic_boc;visit=swh:1:snp:c48cc5ab1e4ba98c4d2b00e3952ff04556c4aa51;anchor=swh:1:rev:82781c3c964d0042c285cc53071e2d690d9a90bb}{\texttt{swh:1:dir:24350cf7167ab1b9d00f8a2d64cc3fe32dfb4560}} (visited on 2026-08-24)},
   url = {https://github.com/fxpl/axiomatic_boc},
   doi = {10.4230/artifacts.27655},
}
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}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.6
Relaxed Linear References for Lock-free Data Structures

Authors: Elias Castegren and Tobias Wrigstad

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom. This paper presents LOLCAT, a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads. The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.
Cite as

Elias Castegren and Tobias Wrigstad. Relaxed Linear References for Lock-free Data Structures. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 6:1-6:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{castegren_et_al:LIPIcs.ECOOP.2017.6,
  author =	{Castegren, Elias and Wrigstad, Tobias},
  title =	{{Relaxed Linear References for Lock-free Data Structures}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{6:1--6:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.6},
  URN =		{urn:nbn:de:0030-drops-72670},
  doi =		{10.4230/LIPIcs.ECOOP.2017.6},
  annote =	{Keywords: Type systems, Concurrency, Lock-free programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.5
Reference Capabilities for Concurrency Control

Authors: Elias Castegren and Tobias Wrigstad

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
The proliferation of shared mutable state in object-oriented programming complicates software development as two seemingly unrelated operations may interact via an alias and produce unexpected results. In concurrent programming this manifests itself as data-races. Concurrent object-oriented programming further suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism. This paper presents a reference capability approach to concurrent and parallel object-oriented programming where all uses of aliases are guaranteed to be data-race free. The static type of an alias describes its possible sharing without using explicit ownership or effect annotations. Type information can express non-interfering deterministic parallelism without dynamic concurrency control, thread-locality, lock-based schemes, and guarded-by relations giving multi-object atomicity to nested data structures. Unification of capabilities and traits allows trait-based reuse across multiple concurrency scenarios with minimal code duplication. The resulting system brings together features from a wide range of prior work in a unified way.
Cite as

Elias Castegren and Tobias Wrigstad. Reference Capabilities for Concurrency Control. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{castegren_et_al:LIPIcs.ECOOP.2016.5,
  author =	{Castegren, Elias and Wrigstad, Tobias},
  title =	{{Reference Capabilities for Concurrency Control}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{5:1--5:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.5},
  URN =		{urn:nbn:de:0030-drops-60998},
  doi =		{10.4230/LIPIcs.ECOOP.2016.5},
  annote =	{Keywords: Type systems, Capabilities, Traits, Concurrency, Object-Oriented}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact