DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2025.15

Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

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

Abstract

Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.

Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15: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.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.32

The Free Termination Property of Queries over Time

Authors: Conor Power, Paraschos Koutris, and Joseph M. Hellerstein

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Building on prior work on distributed databases and the CALM Theorem, we define and study the question of free termination: in the absence of distributed coordination, what query properties allow nodes in a distributed (database) system to unilaterally terminate execution even though they may receive additional data or messages in the future? This completeness question is complementary to the soundness questions studied in the CALM literature. We also develop a new model based on semiautomata that allows us to bridge from the relational transducer model of the CALM papers to algebraic models that are popular among software engineers (e.g. CRDTs) and of increasing interest to database theory for datalog extensions and incremental view maintenance.

Cite as

Conor Power, Paraschos Koutris, and Joseph M. Hellerstein. The Free Termination Property of Queries over Time. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{power_et_al:LIPIcs.ICDT.2025.32,
  author =	{Power, Conor and Koutris, Paraschos and Hellerstein, Joseph M.},
  title =	{{The Free Termination Property of Queries over Time}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.32},
  URN =		{urn:nbn:de:0030-drops-229736},
  doi =		{10.4230/LIPIcs.ICDT.2025.32},
  annote =	{Keywords: distributed systems, algebraic data models, coordination-free systems}
}

Document

Early Ideas

DOI: 10.4230/LIPIcs.CALCO.2023.22

CRDTs, Coalgebraically (Early Ideas)

Authors: Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, and Lindsey Kuper

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract

We describe ongoing work that models conflict-free replicated data types (CRDTs) from a coalgebraic point of view. CRDTs are data structures designed for replication across multiple physical locations in a distributed system. We show how to model a CRDT at the local replica level using a novel coalgebraic semantics for CRDTs. We believe this is the first step towards presenting a unified theory for specifying and verifying CRDTs and replicated state machines. As a case study, we consider emulation of CRDTs in terms of coalgebra.

Cite as

Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, and Lindsey Kuper. CRDTs, Coalgebraically (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{liittschwager_et_al:LIPIcs.CALCO.2023.22,
  author =	{Liittschwager, Nathan and Tsampas, Stelios and Castello, Jonathan and Kuper, Lindsey},
  title =	{{CRDTs, Coalgebraically}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{22:1--22:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.22},
  URN =		{urn:nbn:de:0030-drops-188198},
  doi =		{10.4230/LIPIcs.CALCO.2023.22},
  annote =	{Keywords: Coalgebra, Distributed Systems, Concurrency, Bisimulation}
}

Document

DOI: 10.4230/LIPIcs.SNAPL.2019.10

Toward Domain-Specific Solvers for Distributed Consistency

Authors: Lindsey Kuper and Peter Alvaro

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract

To guard against machine failures, modern internet services store multiple replicas of the same application data within and across data centers, which introduces the problem of keeping geo-distributed replicas consistent with one another in the face of network partitions and unpredictable message latency. To avoid costly and conservative synchronization protocols, many real-world systems provide only weak consistency guarantees (e.g., eventual, causal, or PRAM consistency), which permit certain kinds of disagreement among replicas. There has been much recent interest in language support for specifying and verifying such consistency properties. Although these properties are usually beyond the scope of what traditional type checkers or compiler analyses can guarantee, solver-aided languages are up to the task. Inspired by systems like Liquid Haskell [Vazou et al., 2014] and Rosette [Torlak and Bodik, 2014], we believe that close integration between a language and a solver is the right path to consistent-by-construction distributed applications. Unfortunately, verifying distributed consistency properties requires reasoning about transitive relations (e.g., causality or happens-before), partial orders (e.g., the lattice of replica states under a convergent merge operation), and properties relevant to message processing or API invocation (e.g., commutativity and idempotence) that cannot be easily or efficiently carried out by general-purpose SMT solvers that lack native support for this kind of reasoning. We argue that domain-specific SMT-based tools that exploit the mathematical foundations of distributed consistency would enable both more efficient verification and improved ease of use for domain experts. The principle of exploiting domain knowledge for efficiency and expressivity that has borne fruit elsewhere - such as in the development of high-performance domain-specific languages that trade off generality to gain both performance and productivity - also applies here. Languages augmented with domain-specific, consistency-aware solvers would support the rapid implementation of formally verified programming abstractions that guarantee distributed consistency. In the long run, we aim to democratize the development of such domain-specific solvers by creating a framework for domain-specific solver development that brings new theory solver implementation within the reach of programmers who are not necessarily SMT solver internals experts.

Cite as

Lindsey Kuper and Peter Alvaro. Toward Domain-Specific Solvers for Distributed Consistency. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuper_et_al:LIPIcs.SNAPL.2019.10,
  author =	{Kuper, Lindsey and Alvaro, Peter},
  title =	{{Toward Domain-Specific Solvers for Distributed Consistency}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.10},
  URN =		{urn:nbn:de:0030-drops-105530},
  doi =		{10.4230/LIPIcs.SNAPL.2019.10},
  annote =	{Keywords: distributed consistency, SMT solving, theory solvers}
}

Document

DOI: 10.4230/DARTS.3.2.7

Parallelizing Julia with a Non-Invasive DSL (Artifact)

Authors: Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman

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

Abstract

This artifact is based on ParallelAccelerator, an embedded domain-specific language (DSL) and compiler for speeding up compute-intensive Julia programs. In particular, Julia code that makes heavy use of aggregate array operations is a good candidate for speeding up with ParallelAccelerator. ParallelAccelerator is a non-invasive DSL that makes as few changes to the host programming model as possible.

Cite as

Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{anderson_et_al:DARTS.3.2.7,
  author =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  title =	{{Parallelizing Julia with a Non-Invasive DSL (Artifact)}},
  pages =	{7:1--7:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.7},
  URN =		{urn:nbn:de:0030-drops-72888},
  doi =		{10.4230/DARTS.3.2.7},
  annote =	{Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2017.4

Parallelizing Julia with a Non-Invasive DSL

Authors: Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman

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

Abstract

Computational scientists often prototype software using productivity languages that offer high-level programming abstractions. When higher performance is needed, they are obliged to rewrite their code in a lower-level efficiency language. Different solutions have been proposed to address this trade-off between productivity and efficiency. One promising approach is to create embedded domain-specific languages that sacrifice generality for productivity and performance, but practical experience with DSLs points to some road blocks preventing widespread adoption. This paper proposes a non-invasive domain-specific language that makes as few visible changes to the host programming model as possible. We present ParallelAccelerator, a library and compiler for high-level, high-performance scientific computing in Julia. ParallelAccelerator's programming model is aligned with existing Julia programming idioms. Our compiler exposes the implicit parallelism in high-level array-style programs and compiles them to fast, parallel native code. Programs can also run in "library-only" mode, letting users benefit from the full Julia environment and libraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.

Cite as

Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{anderson_et_al:LIPIcs.ECOOP.2017.4,
  author =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  title =	{{Parallelizing Julia with a Non-Invasive DSL}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{4:1--4: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.4},
  URN =		{urn:nbn:de:0030-drops-72693},
  doi =		{10.4230/LIPIcs.ECOOP.2017.4},
  annote =	{Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}

6 Search Results for "Kuper, Lindsey"

Certified Implementability of Global Multiparty Protocols

Abstract

Cite as

The Free Termination Property of Queries over Time

Abstract

Cite as

CRDTs, Coalgebraically (Early Ideas)

Abstract

Cite as

Toward Domain-Specific Solvers for Distributed Consistency

Abstract

Cite as

Parallelizing Julia with a Non-Invasive DSL (Artifact)

Abstract

Cite as

Parallelizing Julia with a Non-Invasive DSL

Abstract

Cite as

Thanks for your feedback!

Could not send message