Search Results

Documents authored by Nieto, Abel

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.22
Modular Verification of State-Based CRDTs in Separation Logic

Authors: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal

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

Abstract
Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTs, while respecting the desiderata (a)-(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. When taken together with prior work, our technique thus provides a unified approach to specification and verification of op- and state-based CRDTs. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.
Cite as

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2023.22,
  author =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  title =	{{Modular Verification of State-Based CRDTs in Separation Logic}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{22:1--22:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim 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.2023.22},
  URN =		{urn:nbn:de:0030-drops-182154},
  doi =		{10.4230/LIPIcs.ECOOP.2023.22},
  annote =	{Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.15
Modular Verification of State-Based CRDTs in Separation Logic (Artifact)

Authors: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
This is the documentation of the artifact for the paper "Modular Verification of State-Based CRDTs in Separation Logic". The artifact consists of a Coq formalization of the safety proofs for state-based CRDTs described in the paper. The Coq proofs are written in the Aneris distributed separation logic.
Cite as

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{nieto_et_al:DARTS.9.2.15,
  author =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  title =	{{Modular Verification of State-Based CRDTs in Separation Logic (Artifact)}},
  pages =	{15:1--15:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.15},
  URN =		{urn:nbn:de:0030-drops-182553},
  doi =		{10.4230/DARTS.9.2.15},
  annote =	{Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.10
Blame for Null (Artifact)

Authors: Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták

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

Abstract
This artifact is a companion to the paper "Blame for Null", where we formalize multiple calculi to reason about the interoperability between languages where nullability is explicit and those where nullability is implicit. Our main result is a theorem that states that nullability errors can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. We summarize our result with the slogan explicitly nullable programs can't be blamed. The artifact consists of a mechanized Coq proof of the results presented in the paper.
Cite as

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{nieto_et_al:DARTS.6.2.10,
  author =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Blame for Null (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.10},
  URN =		{urn:nbn:de:0030-drops-132070},
  doi =		{10.4230/DARTS.6.2.10},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.14
Scala with Explicit Nulls (Artifact)

Authors: Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu

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

Abstract
This artifact is a companion to the paper "Scala with Explicit Nulls", where we present a modification to the Scala type system that makes nullability explicit in the types. Specifically, we make reference types non-nullable by default, while still allowing for nullable types via union types. The artifact contains an implementation of this new type system design as a fork of the Dotty (Scala 3) compiler. Additionally, the artifact contains the source code of multiple Scala libraries that we used to evaluate our design.
Cite as

Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with Explicit Nulls (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{nieto_et_al:DARTS.6.2.14,
  author =	{Nieto, Abel and Zhao, Yaoyu and Lhot\'{a}k, Ond\v{r}ej and Chang, Angela and Pu, Justin},
  title =	{{Scala with Explicit Nulls (Artifact)}},
  pages =	{14:1--14:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Nieto, Abel and Zhao, Yaoyu and Lhot\'{a}k, Ond\v{r}ej and Chang, Angela and Pu, Justin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.14},
  URN =		{urn:nbn:de:0030-drops-132117},
  doi =		{10.4230/DARTS.6.2.14},
  annote =	{Keywords: Scala, Java, nullability, language interoperability, type systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.3
Blame for Null

Authors: Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták

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

Abstract
Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this paper, we show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, we introduce a calculus, λ_null, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of λ_null, we then create a second calculus, λ_null^s, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. Our main result is a theorem that states that nullability errors in λ_null^s can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. We summarize our result with the slogan explicitly nullable programs can't be blamed. All our results are formalized in the Coq proof assistant.
Cite as

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2020.3,
  author =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Blame for Null}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{3:1--3:28},
  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.3},
  URN =		{urn:nbn:de:0030-drops-131606},
  doi =		{10.4230/LIPIcs.ECOOP.2020.3},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.25
Scala with Explicit Nulls

Authors: Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu

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

Abstract
The Scala programming language makes all reference types implicitly nullable. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors. In this paper, we present a modification to the Scala type system that makes nullability explicit in the types. Specifically, we make reference types non-nullable by default, while still allowing for nullable types via union types. We have implemented this design for explicit nulls as a fork of the Dotty (Scala 3) compiler. We evaluate our scheme by migrating a number of Scala libraries to use explicit nulls. Finally, we give a denotational semantics of type nullification, the interoperability layer between Java and Scala with explicit nulls. We show a soundness theorem stating that, for variants of System F_ω that model Java and Scala, nullification preserves values of types.
Cite as

Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with Explicit Nulls. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 25:1-25:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2020.25,
  author =	{Nieto, Abel and Zhao, Yaoyu and Lhot\'{a}k, Ond\v{r}ej and Chang, Angela and Pu, Justin},
  title =	{{Scala with Explicit Nulls}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{25:1--25: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.25},
  URN =		{urn:nbn:de:0030-drops-131821},
  doi =		{10.4230/LIPIcs.ECOOP.2020.25},
  annote =	{Keywords: Scala, Java, nullability, language interoperability, 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