3 Search Results for "Castegren, Elias"

Document
DOI: 10.4230/OASIcs.Gabbrielli.10
Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages

Authors: Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.
Cite as

Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deboer_et_al:OASIcs.Gabbrielli.10,
  author =	{de Boer, Frank S. and Johnsen, Einar Broch and Schlatte, Rudolf and Tapia Tarifa, Silvia Lizeth and Tveito, Lars},
  title =	{{Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{10:1--10:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.10},
  URN =		{urn:nbn:de:0030-drops-132322},
  doi =		{10.4230/OASIcs.Gabbrielli.10},
  annote =	{Keywords: Testing, Symbolic Traces, Guarded Commands, Partial Order Reduction}
}
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}
}
  • Refine by Type
  • 3 Document/PDF

  • Refine by Publication Year
  • 1 2020
  • 1 2017
  • 1 2016

  • Refine by Author
  • 2 Castegren, Elias
  • 2 Wrigstad, Tobias
  • 1 Johnsen, Einar Broch
  • 1 Schlatte, Rudolf
  • 1 Tapia Tarifa, Silvia Lizeth
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Semantics
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Semantics and reasoning

  • Refine by Keyword
  • 2 Concurrency
  • 2 Type systems
  • 1 Capabilities
  • 1 Guarded Commands
  • 1 Lock-free programming
  • Show More...

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