DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2024.16

Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning

Authors: Cormac Flanagan and Stephen N. Freund

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract

Rely-guarantee (RG) logic uses thread interference specifications (relies and guarantees) to reason about the correctness of multithreaded software. Unfortunately, RG logic requires each function postcondition to be "stabilized" or specialized to the behavior of other threads, making it difficult to write function specifications that are reusable at multiple call sites. This paper presents mover logic, which extends RG logic to address this problem via the notion of atomic functions. Atomic functions behave as if they execute serially without interference from concurrent threads, and so they can be assigned more general and reusable specifications that avoid the stabilization requirement of RG logic. Several practical verifiers (Calvin-R, QED, CIVL, Armada, Anchor, etc.) have demonstrated the modularity benefits of atomic function specifications. However, the complexity of these systems and their correctness proofs makes it challenging to understand and extend these systems. Mover logic formalizes the central ideas of reduction in a declarative program logic that provides a foundation for future work in this area.

Cite as

Cormac Flanagan and Stephen N. Freund. Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{flanagan_et_al:LIPIcs.ECOOP.2024.16,
  author =	{Flanagan, Cormac and Freund, Stephen N.},
  title =	{{Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{16:1--16:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.16},
  URN =		{urn:nbn:de:0030-drops-208654},
  doi =		{10.4230/LIPIcs.ECOOP.2024.16},
  annote =	{Keywords: concurrent program verification, reduction, rely-guarantee reasoning, synchronization}
}

Document

DOI: 10.4230/DagSemProc.09361.1

09361 Abstracts Collection – Design and Validation of Concurrent Systems

Authors: Cormac Flanagan, Susanne Graf, Madhusan Parthasarathy, and Shaz Quadeer

Published in: Dagstuhl Seminar Proceedings, Volume 9361, Design and Validation of Concurrent Systems (2010)

Abstract

The Dagstuhl Seminar 09361 ``Design and Validation of Concurrent Systems'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics from August 30 to September 4, 2009. During the seminar, participants presented their current research, and ongoing work and open problems were discussed. This paper reviews the seminar topics and goals, and provides abstracts of the presentations given during the seminar. Links to extended abstracts or full papers are provided, if available.

Cite as

Cormac Flanagan, Susanne Graf, Madhusan Parthasarathy, and Shaz Quadeer. 09361 Abstracts Collection – Design and Validation of Concurrent Systems. In Design and Validation of Concurrent Systems. Dagstuhl Seminar Proceedings, Volume 9361, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{flanagan_et_al:DagSemProc.09361.1,
  author =	{Flanagan, Cormac and Graf, Susanne and Parthasarathy, Madhusan and Quadeer, Shaz},
  title =	{{09361 Abstracts Collection – Design and Validation of Concurrent Systems}},
  booktitle =	{Design and Validation of Concurrent Systems},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9361},
  editor =	{Cormac Flanagan and Madhusan Parthasarathy and Shaz Quadeer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09361.1},
  URN =		{urn:nbn:de:0030-drops-25498},
  doi =		{10.4230/DagSemProc.09361.1},
  annote =	{Keywords: Concurrency, Specification, Programming, Verification, Validation, Testing}
}

Search Results

Documents authored by Flanagan, Cormac

Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning

Abstract

Cite as

09361 Abstracts Collection – Design and Validation of Concurrent Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message