Search Results

Documents authored by Dongol, Brijesh

Document
DOI: 10.4230/LIPIcs.DISC.2024.11
What Cannot Be Implemented on Weak Memory?

Authors: Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)

Abstract
We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties, identifying restrictions under which independent memory traces can be merged into a single valid memory trace. In turn, we show that the mergeability properties of the underlying memory model entail similar mergeability requirements on the specifications of objects that can be implemented on that memory model. We demonstrate the applicability of our approach to establish the impossibility of implementing standard distributed objects with different restrictions on memory traces on three memory models: strictly consistent memory, total store order, and release-acquire. These impossibility results allow us to identify tight and almost tight bounds for some objects, as well as new separation results between weak memory models, and between well-studied objects based on their implementability on weak memory models.
Cite as

Armando Castañeda, Gregory Chockler, Brijesh Dongol, and Ori Lahav. What Cannot Be Implemented on Weak Memory?. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{castaneda_et_al:LIPIcs.DISC.2024.11,
  author =	{Casta\~{n}eda, Armando and Chockler, Gregory and Dongol, Brijesh and Lahav, Ori},
  title =	{{What Cannot Be Implemented on Weak Memory?}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.11},
  URN =		{urn:nbn:de:0030-drops-212371},
  doi =		{10.4230/LIPIcs.DISC.2024.11},
  annote =	{Keywords: Impossibility, Weak Memory Models, Total-Store Order, Release-Acquire}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.31
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement

Authors: Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with only finite traces. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a (weak) progress condition, and prove that this weak progressive forward simulation is equivalent to strong observational refinement.
Cite as

Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dongol_et_al:LIPIcs.CONCUR.2022.31,
  author =	{Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.31},
  URN =		{urn:nbn:de:0030-drops-170947},
  doi =		{10.4230/LIPIcs.CONCUR.2022.31},
  annote =	{Keywords: Strong Observational Refinement, Hyperproperties, Forward Simulation, Weak Progressiveness}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2021.55
Brief Announcement: On Strong Observational Refinement and Forward Simulation

Authors: John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 209, 35th International Symposium on Distributed Computing (DISC 2021)

Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement.
Cite as

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Brief Announcement: On Strong Observational Refinement and Forward Simulation. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 55:1-55:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{derrick_et_al:LIPIcs.DISC.2021.55,
  author =	{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Brief Announcement: On Strong Observational Refinement and Forward Simulation}},
  booktitle =	{35th International Symposium on Distributed Computing (DISC 2021)},
  pages =	{55:1--55:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-210-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{209},
  editor =	{Gilbert, Seth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2021.55},
  URN =		{urn:nbn:de:0030-drops-148575},
  doi =		{10.4230/LIPIcs.DISC.2021.55},
  annote =	{Keywords: Strong Observational Refinement, Hyperproperties, Forward Simulation}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.15
Owicki-Gries Reasoning for C11 RAR (Artifact)

Authors: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
The paper "Owicki-Gries Reasoning for C11 RAR" introduces a new proof calculus for the C11 RAR memory model that allows Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. The proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. The artifact includes the Isabelle formalisation of the proof method introduced in the paper. It also contains the formalisation and proof of all case studies presented in the paper. All of the theorems are accompanied with their respective proofs.
Cite as

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{dalvandi_et_al:DARTS.6.2.15,
  author =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  title =	{{Owicki-Gries Reasoning for C11 RAR (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.15},
  URN =		{urn:nbn:de:0030-drops-132123},
  doi =		{10.4230/DARTS.6.2.15},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.11
Owicki-Gries Reasoning for C11 RAR

Authors: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover Isabelle.
Cite as

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 11:1-11:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dalvandi_et_al:LIPIcs.ECOOP.2020.11,
  author =	{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike},
  title =	{{Owicki-Gries Reasoning for C11 RAR}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{11:1--11:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.11},
  URN =		{urn:nbn:de:0030-drops-131687},
  doi =		{10.4230/LIPIcs.ECOOP.2020.11},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2018.45
Brief Announcement: Generalising Concurrent Correctness to Weak Memory

Authors: Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.
Cite as

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. Brief Announcement: Generalising Concurrent Correctness to Weak Memory. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 45:1-45:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doherty_et_al:LIPIcs.DISC.2018.45,
  author =	{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John},
  title =	{{Brief Announcement: Generalising Concurrent Correctness to Weak Memory}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{45:1--45:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.45},
  URN =		{urn:nbn:de:0030-drops-98344},
  doi =		{10.4230/LIPIcs.DISC.2018.45},
  annote =	{Keywords: Weak Memory, Concurrent Object, Execution Structure}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2016.35
Proving Opacity of a Pessimistic STM

Authors: Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
Transactional Memory (TM) is a high-level programming abstraction for concurrency control that provides programmers with the illusion of atomically executing blocks of code, called transactions. TMs come in two categories, optimistic and pessimistic, where in the latter transactions never abort. While this simplifies the programming model, high-performing pessimistic TMs can be complex. In this paper, we present the first formal verification of a pessimistic software TM algorithm, namely, an algorithm proposed by Matveev and Shavit. The correctness criterion used is opacity, formalising the transactional atomicity guarantees. We prove that this pessimistic TM is a refinement of an intermediate opaque I/O-automaton, known as TMS2. To this end, we develop a rely-guarantee approach for reducing the complexity of the proof. Proofs are mechanised in the interactive prover Isabelle.
Cite as

Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. Proving Opacity of a Pessimistic STM. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{doherty_et_al:LIPIcs.OPODIS.2016.35,
  author =	{Doherty, Simon and Dongol, Brijesh and Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike},
  title =	{{Proving Opacity of a Pessimistic STM}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.35},
  URN =		{urn:nbn:de:0030-drops-71040},
  doi =		{10.4230/LIPIcs.OPODIS.2016.35},
  annote =	{Keywords: Pessimistic STMs, Opacity, Verification, Isabelle, Simulation, TMS2}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.470
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures

Authors: Brijesh Dongol, John Derrick, Lindsay Groves, and Graeme Smith

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures. We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.
Cite as

Brijesh Dongol, John Derrick, Lindsay Groves, and Graeme Smith. Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 470-494, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dongol_et_al:LIPIcs.ECOOP.2015.470,
  author =	{Dongol, Brijesh and Derrick, John and Groves, Lindsay and Smith, Graeme},
  title =	{{Defining Correctness Conditions for Concurrent Objects in Multicore Architectures}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{470--494},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.470},
  URN =		{urn:nbn:de:0030-drops-52348},
  doi =		{10.4230/LIPIcs.ECOOP.2015.470},
  annote =	{Keywords: Concurrent objects, correctness, relaxed memory, verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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