Search Results

Documents authored by Vafeiadis, Viktor

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.33
Automating Memory Model Metatheory with Intersections

Authors: Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
In the weak memory consistency literature, the semantics of concurrent programs is typically defined as a constraint on execution graphs, expressed in relational algebra. Prior work has shown that basic metatheoretic questions about memory models are decidable as long as they can be expressed as irreflexivity and emptiness constraints over Kleene Algebra with Tests (KAT), a condition that rules out practical memory models such the C/C++ and the Linux kernel models. In this paper, we extend these results to memory models containing arbitrary intersections with uninterpreted relations. We can thus automatically establish compilation correctness and derive efficient incremental consistency checkers for RC11, LKMM, and other memory models.
Cite as

Aristotelis Koutsouridis, Michalis Kokologiannakis, and Viktor Vafeiadis. Automating Memory Model Metatheory with Intersections. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{koutsouridis_et_al:LIPIcs.CONCUR.2024.33,
  author =	{Koutsouridis, Aristotelis and Kokologiannakis, Michalis and Vafeiadis, Viktor},
  title =	{{Automating Memory Model Metatheory with Intersections}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.33},
  URN =		{urn:nbn:de:0030-drops-208050},
  doi =		{10.4230/LIPIcs.CONCUR.2024.33},
  annote =	{Keywords: Kleene Algebra, Weak Memory Models}
}
Document
DOI: 10.4230/DagRep.13.10.50
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)

Authors: Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, and Anton Podkopaev

Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)

Abstract
Recently developed non-volatile memory (NVM) devices provide persistency guarantees along with byte-addressable accesses and performance characteristics that are much closer to volatile random-access memory (RAM). However, writing programs that correctly use these devices is challenging, and bugs related to their use can cause permanent data loss in applications. This Dagstuhl Seminar brought together experts in a range of areas related to concurrency and persistent memory to explore and develop formal methods for ensuring the correctness of applications that use persistent memory. Talks and discussions at the seminar highlighted challenges related to correctness criteria for concurrent objects using persistent memory, liveness properties of persistent objects, and how changes in NVM and related technologies should shape the development of formal methods for NVM.
Cite as

Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, and Anton Podkopaev. Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). In Dagstuhl Reports, Volume 13, Issue 10, pp. 50-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{lahav_et_al:DagRep.13.10.50,
  author =	{Lahav, Ori and Raad, Azalea and Tassarotti, Joseph and Vafeiadis, Viktor and Podkopaev, Anton},
  title =	{{Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)}},
  pages =	{50--64},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{Lahav, Ori and Raad, Azalea and Tassarotti, Joseph and Vafeiadis, Viktor and Podkopaev, Anton},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.50},
  URN =		{urn:nbn:de:0030-drops-198337},
  doi =		{10.4230/DagRep.13.10.50},
  annote =	{Keywords: concurrency, formal methods, non-volatile-memory, persistency, verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CALCO.2021.4
The Challenges of Weak Persistency (Invited Talk)

Authors: Viktor Vafeiadis

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
Non-volatile memory (NVM) is a new hardware technology that provides durable storage at performance similar to that of plain volatile RAM. As such, there is a lot of interest in exploiting this technology to improve the performance of existing disk-bound applications and to find new applications for it. Nevertheless, developing correct programs that interact with non-volatile memory is by no means easy, since mainstream architectures provide rather weak persistency semantics and rather low-level and expensive mechanisms in order to avoid weak behaviors. This creates many opportunities for researchers in programming language semantics, logic, and verification to develop techniques to assist programmers writing NVM programs. This short paper and the associated talk outline the challenges caused by NVM and the research opportunities for PL researchers.
Cite as

Viktor Vafeiadis. The Challenges of Weak Persistency (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{vafeiadis:LIPIcs.CALCO.2021.4,
  author =	{Vafeiadis, Viktor},
  title =	{{The Challenges of Weak Persistency}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{4:1--4:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4},
  URN =		{urn:nbn:de:0030-drops-153593},
  doi =		{10.4230/LIPIcs.CALCO.2021.4},
  annote =	{Keywords: Weak Persistency, Non-Volatile Memory}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.4
Reconciling Event Structures with Modern Multiprocessors (Artifact)

Authors: Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis

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

Abstract
The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package weakestmoToImm contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.
Cite as

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{moiseenko_et_al:DARTS.6.2.4,
  author =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  title =	{{Reconciling Event Structures with Modern Multiprocessors (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.4},
  URN =		{urn:nbn:de:0030-drops-132015},
  doi =		{10.4230/DARTS.6.2.4},
  annote =	{Keywords: Weak Memory Consistency, Event Structures, IMM, Weakestmo}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.5
Reconciling Event Structures with Modern Multiprocessors

Authors: Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis

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

Abstract
Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem and to enable efficient compilation to hardware. Nevertheless, this latter property - compilation correctness - has not yet been formally established. This paper closes this gap by establishing correctness of the intended compilation schemes from Weakestmo to a wide range of formal hardware memory models (x86, POWER, ARMv7, ARMv8) in the Coq proof assistant. Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids "out-of-thin-air" behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.
Cite as

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{moiseenko_et_al:LIPIcs.ECOOP.2020.5,
  author =	{Moiseenko, Evgenii and Podkopaev, Anton and Lahav, Ori and Melkonian, Orestis and Vafeiadis, Viktor},
  title =	{{Reconciling Event Structures with Modern Multiprocessors}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{5:1--5: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.5},
  URN =		{urn:nbn:de:0030-drops-131622},
  doi =		{10.4230/LIPIcs.ECOOP.2020.5},
  annote =	{Keywords: Weak Memory Consistency, Event Structures, IMM, Weakestmo}
}
Document
DOI: 10.4230/DARTS.3.2.15
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)

Authors: Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact provides the soundness proofs for the encodings in Iris the RSL and GPS logics, as well as the verification for all standard examples known to be verifiable in those logics. All of these proofs are formalized in Coq, which is the main content of this artifact. The formalization is provided in a virtual machine for the convenience of testing, but can also be built from source.
Cite as

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{kaiser_et_al:DARTS.3.2.15,
  author =	{Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
  title =	{{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.15},
  URN =		{urn:nbn:de:0030-drops-72966},
  doi =		{10.4230/DARTS.3.2.15},
  annote =	{Keywords: weak memory models, release-acquire, concurrency, separation logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.17
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris

Authors: Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
The field of concurrent separation logics (CSLs) has recently undergone two exciting developments: (1) the Iris framework for encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency. Unfortunately, these developments are seemingly incompatible, since Iris only applies to languages with an operational interleaving semantics, while C11 is defined by a declarative (axiomatic) semantics. In this paper, we show that, on the contrary, it is not only feasible but useful to marry these developments together. Our first step is to provide a novel operational characterization of RA+NA, the fragment of C11 containing RA accesses and "non-atomic" (normal data) accesses. Instantiating Iris with this semantics, we then derive higher-order variants of two prominent RA+NA logics, GPS and RSL. Finally, we deploy these derived logics in order to perform the first mechanical verifications (in Coq) of several interesting case studies of RA+NA programming. In a nutshell, we provide the first foundationally verified framework for proving programs correct under C11's weak-memory semantics.
Cite as

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.ECOOP.2017.17,
  author =	{Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
  title =	{{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{17:1--17:29},
  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.17},
  URN =		{urn:nbn:de:0030-drops-72753},
  doi =		{10.4230/LIPIcs.ECOOP.2017.17},
  annote =	{Keywords: Weak memory models, release-acquire, concurrency, separation logic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.22
Promising Compilation to ARMv8 POP

Authors: Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the "promising" semantics of [Kang et al. POPL'17] to the ARMv8 POP machine of [Flur et al. POPL'16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP.
Cite as

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Promising Compilation to ARMv8 POP. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{podkopaev_et_al:LIPIcs.ECOOP.2017.22,
  author =	{Podkopaev, Anton and Lahav, Ori and Vafeiadis, Viktor},
  title =	{{Promising Compilation to ARMv8 POP}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{22:1--22:28},
  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.22},
  URN =		{urn:nbn:de:0030-drops-72667},
  doi =		{10.4230/LIPIcs.ECOOP.2017.22},
  annote =	{Keywords: ARM, Compilation Correctness, Weak Memory Model}
}
Document
DOI: 10.4230/DagRep.5.11.1
Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)

Authors: Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)

Abstract
This report documents the programme and the outcome of Dagstuhl Seminar 15451 "Verification of Evolving Graph Structures". The aim was to bring together researchers from different communities (shape analysis, separation logic, graph transformation, verification of infinite-state systems) who are interested in developing techniques for the analysis of graph manipulations, i.e., methods that are able to handle the challenges that arise in current verification problems. Apart from scientific talks, the programme also included four tutorial talks and four working groups, which are summarized in this report.
Cite as

Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis. Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). In Dagstuhl Reports, Volume 5, Issue 11, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{azizabdulla_et_al:DagRep.5.11.1,
  author =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  title =	{{Verification of Evolving Graph Structures (Dagstuhl Seminar 15451)}},
  pages =	{1--28},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Aziz Abdulla, Parosh and Gadducci, Fabio and K\"{o}nig, Barbara and Vafeiadis, Viktor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.11.1},
  URN =		{urn:nbn:de:0030-drops-57614},
  doi =		{10.4230/DagRep.5.11.1},
  annote =	{Keywords: dynamic systems, graph transformation, graphs, heap analysis, separation logic, shape analysis, static analysis, verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.483
Rely/Guarantee Reasoning for Asynchronous Programs

Authors: Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.
Cite as

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 483-496, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gavran_et_al:LIPIcs.CONCUR.2015.483,
  author =	{Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor},
  title =	{{Rely/Guarantee Reasoning for Asynchronous Programs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{483--496},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.483},
  URN =		{urn:nbn:de:0030-drops-53902},
  doi =		{10.4230/LIPIcs.CONCUR.2015.483},
  annote =	{Keywords: Asynchronous programs, rely/guarantee reasoning}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.396
Asynchronous Liquid Separation Types

Authors: Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis

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

Abstract
We present a refinement type system for reasoning about asynchronous programs manipulating shared mutable state. Our type system guarantees the absence of races and the preservation of user-specified invariants using a combination of two ideas: refinement types and concurrent separation logic. Our type system allows precise reasoning about programs using two ingredients. First, our types are indexed by sets of resource names and the type system tracks the effect of program execution on individual heap locations and task handles. In particular, it allows making strong updates to the types of heap locations. Second, our types track ownership of shared state across concurrently posted tasks and allow reasoning about ownership transfer between tasks using permissions. We demonstrate through several examples that these two ingredients, on top of the framework of liquid types, are powerful enough to reason about correct behavior of practical, complex, asynchronous systems manipulating shared heap resources. We have implemented type inference for our type system and have used it to prove complex invariants of asynchronous OCaml programs. We also show how the type system detects subtle concurrency bugs in a file system implementation.
Cite as

Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous Liquid Separation Types. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 396-420, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kloos_et_al:LIPIcs.ECOOP.2015.396,
  author =	{Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor},
  title =	{{Asynchronous Liquid Separation Types}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{396--420},
  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.396},
  URN =		{urn:nbn:de:0030-drops-52233},
  doi =		{10.4230/LIPIcs.ECOOP.2015.396},
  annote =	{Keywords: Liquid Types, Asynchronous Parallelism, Separation Logic, Type Systems}
}
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