Search Results

Documents authored by Doherty, Simon

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}
}
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