Search Results

Documents authored by Schellhorn, Gerhard

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
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 About DROPS Imprint Privacy Contact