DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2025.33

Scott’s Representation Theorem and the Univalent Karoubi Envelope

Authors: Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category. We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms.

Cite as

Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanderleer_et_al:LIPIcs.ITP.2025.33,
  author =	{van der Leer, Arnoud and Wullaert, Kobe and Ahrens, Benedikt},
  title =	{{Scott’s Representation Theorem and the Univalent Karoubi Envelope}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.33},
  URN =		{urn:nbn:de:0030-drops-246318},
  doi =		{10.4230/LIPIcs.ITP.2025.33},
  annote =	{Keywords: Lambda calculi, algebraic theories, categorical semantics, Karoubi envelope, formalization, Rocq-UniMath, univalent foundations}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.26

Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.

Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.22

Partial-Order Reduction Is Hard

Authors: Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.

Cite as

Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz. Partial-Order Reduction Is Hard. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2025.22,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Larroze-Jardin\'{e}, Sarah and Walukiewicz, Igor},
  title =	{{Partial-Order Reduction Is Hard}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22},
  URN =		{urn:nbn:de:0030-drops-239727},
  doi =		{10.4230/LIPIcs.CONCUR.2025.22},
  annote =	{Keywords: Formal verification, Concurrent systems, Partial-order reduction, Complexity}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2025.2

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk)

Authors: Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the "neural" and "symbolic" program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle - standing as an abbreviation for a "verification condition language" - an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle’s overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.

Cite as

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{daggitt_et_al:LIPIcs.FSCD.2025.2,
  author =	{Daggitt, Matthew L. and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca},
  title =	{{Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.2},
  URN =		{urn:nbn:de:0030-drops-236172},
  doi =		{10.4230/LIPIcs.FSCD.2025.2},
  annote =	{Keywords: Neural Network Verification, Types, Interactive Theorem Provers}
}

Document

Pearl/Brave New Idea

DOI: 10.4230/LIPIcs.ECOOP.2025.41

Shouting at Memory: Where Did My Write Go? (Pearl/Brave New Idea)

Authors: Vasileios Klimis

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

Non-Volatile Memory (NVM) promises persistent data, but verifying that promise on real hardware is challenging due to opaque caching and internal buffers like Intel’s WPQ, which obscure the true state of writes. Traditional validation methods often fall short. This paper introduces a novel perspective: leveraging the subtle timing variations of memory accesses as a direct probe into write persistence. We present a software technique, inspired by echolocation, that uses high-resolution timers to measure memory load latencies. These timings act as distinct signatures ("echoes") revealing whether a write’s data resides in volatile caches or has reached the NVM persistence domain. This offers a non-invasive method to track write progression towards durability. To reliably interpret these potentially noisy timing signatures and systematically explore complex persistence behaviours, we integrate this echolocation probe into an active model learning framework. This synergy enables the automated inference of a system’s actual persistency semantics directly from black-box hardware observations. The approach is hardware-agnostic, adaptive, and scalable. Preliminary experiments on Intel x86 - a platform where persistence validation is notably challenged by the opaque Write Pending Queue (WPQ) - demonstrate the feasibility of our technique. We observed distinct latency clusters differentiating volatile cache accesses from those reaching the persistence domain. This combined approach offers a promising path towards robust and automated validation of NVM persistency across diverse architectures.

Cite as

Vasileios Klimis. Shouting at Memory: Where Did My Write Go? (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 41:1-41:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{klimis:LIPIcs.ECOOP.2025.41,
  author =	{Klimis, Vasileios},
  title =	{{Shouting at Memory: Where Did My Write Go?}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{41:1--41:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan 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.ECOOP.2025.41},
  URN =		{urn:nbn:de:0030-drops-233339},
  doi =		{10.4230/LIPIcs.ECOOP.2025.41},
  annote =	{Keywords: Persistency Memory Semantics, Fuzz Testing, Model Learning}
}

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.CONCUR.2022.2

Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk)

Authors: Philippa Gardner

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

Abstract

Scalable verification for concurrent programs with shared memory is a long-standing, difficult problem. In 2004, O'Hearn and Brookes introduced concurrent separation logic to provide compositional reasoning about coarse-grained concurrent programs with synchronisation primitives (Gödel prize, 2016). In 2010, I introduced logical abstraction (the fiction of separation) to CSL, developing the CAP logic for reasoning about fine-grained concurrent programs in general and fine-grained lock algorithms in particular. In one logic, it was possible to provide two-sided specifications of concurrent operations, with formally verified implementations and clients. In 2014, I introduced logical atomicity (the fiction of atomicity) to concurrent separation logics, developing the TaDA logic to capture when individual operations behave atomically. Unlike CAP, where synchronisation primitives leak into the specifications, with TaDA the specifications are "just right" in that they provide more general atomic functions specifications to capture, for example, the full behaviour of lock operations. In 2021, I introduced environment liveness conditions to concurrent separation logics, developing the TaDA Live logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. The fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. In this talk, I will explain this on-going journey in the wonderful world of concurrent separation logics. I will also explain why I have a bright green office chair in the corner of my office, patterned in gold lamé. Many thanks to my fabulous coauthors on concurrent separation logics: Thomas Dinsdale-Young, Emanuele D'Osualdo, Mike Dodds, Azadeh Farzan, Matthew Parkinson, Pedro da Rocha Pinto, Julian Sutherland, Viktor Vafeiadis and more. Suggested Reading: - Peter O'Hearn: Resources, Concurrency and Local Reasoning, Journal of Theoretical Computer Science, Festschrift for John C Reynolds 70th birthday, 2007. - Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner: A Perspective on Specifying and Verifying Concurrent Modules, Journal of Logical and Algebraic Methods in Programming, 2018. - Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland: TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 2021.

Cite as

Philippa Gardner. Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gardner:LIPIcs.CONCUR.2022.2,
  author =	{Gardner, Philippa},
  title =	{{Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{2:1--2:1},
  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.2},
  URN =		{urn:nbn:de:0030-drops-170659},
  doi =		{10.4230/LIPIcs.CONCUR.2022.2},
  annote =	{Keywords: Concurrent separation logic}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.6

Compiling Volatile Correctly in Java

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.

Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 6:1-6:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.ECOOP.2022.6,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{6:1--6:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.6},
  URN =		{urn:nbn:de:0030-drops-162346},
  doi =		{10.4230/LIPIcs.ECOOP.2022.6},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}

Document

Artifact

DOI: 10.4230/DARTS.8.2.3

Compiling Volatile Correctly in Java (Artifact)

Authors: Shuyang Liu, John Bender, and Jens Palsberg

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.

Cite as

Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{liu_et_al:DARTS.8.2.3,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.3},
  URN =		{urn:nbn:de:0030-drops-162018},
  doi =		{10.4230/DARTS.8.2.3},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}

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

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

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

19 Search Results for "Vafeiadis, Viktor"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message