7 Search Results for "Ferreira, Carla"


Document
VeriFx: Correct Replicated Data Types for the Masses

Authors: Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix

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


Abstract
Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalization instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved for verification experts and is extremely time-consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a specialized programming language for RDTs with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala and JavaScript). VeriFx provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 51 CRDTs, 16 of which are used in industrial databases, and reproduce a study on the correctness of OT functions.

Cite as

Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 9:1-9:45, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{deporre_et_al:LIPIcs.ECOOP.2023.9,
  author =	{De Porre, Kevin and Ferreira, Carla and Gonzalez Boix, Elisa},
  title =	{{VeriFx: Correct Replicated Data Types for the Masses}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{9:1--9:45},
  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.9},
  URN =		{urn:nbn:de:0030-drops-182028},
  doi =		{10.4230/LIPIcs.ECOOP.2023.9},
  annote =	{Keywords: distributed systems, eventual consistency, replicated data types, verification}
}
Document
Artifact
VeriFx: Correct Replicated Data Types for the Masses (Artifact)

Authors: Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix

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


Abstract
Our related article presents our novel verification language, called VeriFx. We used VeriFx to implement and verify 51 Conflict-Free Replicated Data Types (CRDTs) and 9 Operational Transformation (OT) functions. This artifact bundles the implementation of the various CRDTs and OT functions described in the article. The artifact also contains a Docker file that can be used to reproduce the verification results (Table 1 and 2 in the article). In addition, the artifact can also be used to run custom VeriFx programs and verify their correctness.

Cite as

Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 19:1-19:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{deporre_et_al:DARTS.9.2.19,
  author =	{De Porre, Kevin and Ferreira, Carla and Gonzalez Boix, Elisa},
  title =	{{VeriFx: Correct Replicated Data Types for the Masses (Artifact)}},
  pages =	{19:1--19:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{De Porre, Kevin and Ferreira, Carla and Gonzalez Boix, Elisa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.19},
  URN =		{urn:nbn:de:0030-drops-182596},
  doi =		{10.4230/DARTS.9.2.19},
  annote =	{Keywords: distributed systems, eventual consistency, replicated data types, verification}
}
Document
Programming Languages for Distributed Systems and Distributed Data Management (Dagstuhl Seminar 19442)

Authors: Carla Ferreira, Philipp Haller, and Guido Salvaneschi

Published in: Dagstuhl Reports, Volume 9, Issue 10 (2020)


Abstract
Programming language advances have played an important role in various areas of distributed systems research, including consistency, communication, and fault tolerance, enabling automated reasoning and performance optimization. However, over the last few years, researchers focusing on this area have been scattered across different communities such as language design and implementation, (distributed) databases, Big Data processing and IoT/edge computing -- resulting in limited interaction. The goal of this seminar is to build a community of researchers interested in programming language techniques for distributed systems and distributed data management, share current research results and set up a common research agenda. This report documents the program and the outcomes of Dagstuhl Seminar 19442 "Programming Languages for Distributed Systems and Distributed Data Management."

Cite as

Carla Ferreira, Philipp Haller, and Guido Salvaneschi. Programming Languages for Distributed Systems and Distributed Data Management (Dagstuhl Seminar 19442). In Dagstuhl Reports, Volume 9, Issue 10, pp. 117-133, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Article{ferreira_et_al:DagRep.9.10.117,
  author =	{Ferreira, Carla and Haller, Philipp and Salvaneschi, Guido},
  title =	{{Programming Languages for Distributed Systems and Distributed Data Management (Dagstuhl Seminar 19442)}},
  pages =	{117--133},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{10},
  editor =	{Ferreira, Carla and Haller, Philipp and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.10.117},
  URN =		{urn:nbn:de:0030-drops-118586},
  doi =		{10.4230/DagRep.9.10.117},
  annote =	{Keywords: Programming Languages, Distributed Systems, Data Management}
}
Document
Robustness Against Transactional Causal Consistency

Authors: Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model that is widely used in practice. In this paper, we investigate application-specific relationships between several variations of causal consistency and we address the issue of verifying automatically if a given transactional program is robust against causal consistency, i.e., all its behaviors when executed over an arbitrary causally consistent database are serializable. We show that programs without write-write races have the same set of behaviors under all these variations, and we show that checking robustness is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. A surprising corollary of the latter result is that causal consistency variations which admit incomparable sets of behaviors admit comparable sets of robust programs. This reduction also opens the door to leveraging existing methods and tools for the verification of concurrent programs (assuming sequential consistency) for reasoning about programs running over causally consistent databases. Furthermore, it allows to establish that the problem of checking robustness is decidable when the programs executed at different sites are finite-state.

Cite as

Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. Robustness Against Transactional Causal Consistency. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{beillahi_et_al:LIPIcs.CONCUR.2019.30,
  author =	{Beillahi, Sidi Mohamed and Bouajjani, Ahmed and Enea, Constantin},
  title =	{{Robustness Against Transactional Causal Consistency}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.30},
  URN =		{urn:nbn:de:0030-drops-109321},
  doi =		{10.4230/LIPIcs.CONCUR.2019.30},
  annote =	{Keywords: Distributed Databases, Causal Consistency, Model Checking}
}
Document
Graph-of-Entity: A Model for Combined Data Representation and Retrieval

Authors: José Devezas, Carla Lopes, and Sérgio Nunes

Published in: OASIcs, Volume 74, 8th Symposium on Languages, Applications and Technologies (SLATE 2019)


Abstract
Managing large volumes of digital documents along with the information they contain, or are associated with, can be challenging. As systems become more intelligent, it increasingly makes sense to power retrieval through all available data, where every lead makes it easier to reach relevant documents or entities. Modern search is heavily powered by structured knowledge, but users still query using keywords or, at the very best, telegraphic natural language. As search becomes increasingly dependent on the integration of text and knowledge, novel approaches for a unified representation of combined data present the opportunity to unlock new ranking strategies. We tackle entity-oriented search using graph-based approaches for representation and retrieval. In particular, we propose the graph-of-entity, a novel approach for indexing combined data, where terms, entities and their relations are jointly represented. We compare the graph-of-entity with the graph-of-word, a text-only model, verifying that, overall, it does not yet achieve a better performance, despite obtaining a higher precision. Our assessment was based on a small subset of the INEX 2009 Wikipedia Collection, created from a sample of 10 topics and respectively judged documents. The offline evaluation we do here is complementary to its counterpart from TREC 2017 OpenSearch track, where, during our participation, we had assessed graph-of-entity in an online setting, through team-draft interleaving.

Cite as

José Devezas, Carla Lopes, and Sérgio Nunes. Graph-of-Entity: A Model for Combined Data Representation and Retrieval. In 8th Symposium on Languages, Applications and Technologies (SLATE 2019). Open Access Series in Informatics (OASIcs), Volume 74, pp. 1:1-1:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{devezas_et_al:OASIcs.SLATE.2019.1,
  author =	{Devezas, Jos\'{e} and Lopes, Carla and Nunes, S\'{e}rgio},
  title =	{{Graph-of-Entity: A Model for Combined Data Representation and Retrieval}},
  booktitle =	{8th Symposium on Languages, Applications and Technologies (SLATE 2019)},
  pages =	{1:1--1:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-114-6},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{74},
  editor =	{Rodrigues, Ricardo and Janou\v{s}ek, Jan and Ferreira, Lu{\'\i}s and Coheur, Lu{\'\i}sa and Batista, Fernando and Gon\c{c}alo Oliveira, Hugo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2019.1},
  URN =		{urn:nbn:de:0030-drops-108686},
  doi =		{10.4230/OASIcs.SLATE.2019.1},
  annote =	{Keywords: Entity-oriented search, graph-based models, collection-based graph}
}
Document
Version Control Is for Your Data Too

Authors: Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan

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


Abstract
Programmers regularly use distributed version control systems (DVCS) such as Git to facilitate collaborative software development. The primary purpose of a DVCS is to maintain integrity of source code in the presence of concurrent, possibly conflicting edits from collaborators. In addition to safely merging concurrent non-conflicting edits, a DVCS extensively tracks source code provenance to help programmers contextualize and resolve conflicts. Provenance also facilitates debugging by letting programmers see diffs between versions and quickly find those edits that introduced the offending conflict (e.g., via git blame). In this paper, we posit that analogous workflows to collaborative software development also arise in distributed software execution; we argue that the characteristics that make a DVCS an ideal fit for the former also make it an ideal fit for the latter. Building on this observation, we propose a distributed programming model, called carmot that views distributed shared state as an entity evolving in time, manifested as a sequence of persistent versions, and relies on an explicitly defined merge semantics to reconcile concurrent conflicting versions. We show examples demonstrating how carmot simplifies distributed programming, while also enabling novel workflows integral to modern applications such as blockchains. We also describe a prototype implementation of carmot that we use to evaluate its practicality.

Cite as

Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan. Version Control Is for Your Data Too. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kaki_et_al:LIPIcs.SNAPL.2019.8,
  author =	{Kaki, Gowtham and Sivaramakrishnan, KC and Jagannathan, Suresh},
  title =	{{Version Control Is for Your Data Too}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{8:1--8:18},
  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.8},
  URN =		{urn:nbn:de:0030-drops-105516},
  doi =		{10.4230/LIPIcs.SNAPL.2019.8},
  annote =	{Keywords: replication, distributed systems, version control}
}
Document
A Tour of Gallifrey, a Language for Geodistributed Programming

Authors: Mae Milano, Rolph Recto, Tom Magrino, and Andrew C. Myers

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


Abstract
Programming efficient distributed, concurrent systems requires new abstractions that go beyond traditional sequential programming. But programmers already have trouble getting sequential code right, so simplicity is essential. The core problem is that low-latency, high-availability access to data requires replication of mutable state. Keeping replicas fully consistent is expensive, so the question is how to expose asynchronously replicated objects to programmers in a way that allows them to reason simply about their code. We propose an answer to this question in our ongoing work designing a new language, Gallifrey, which provides orthogonal replication through _restrictions_ with _merge strategies_, _contingencies_ for conflicts arising from concurrency, and _branches_, a novel concurrency control construct inspired by version control, to contain provisional behavior.

Cite as

Mae Milano, Rolph Recto, Tom Magrino, and Andrew C. Myers. A Tour of Gallifrey, a Language for Geodistributed Programming. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{milano_et_al:LIPIcs.SNAPL.2019.11,
  author =	{Milano, Mae and Recto, Rolph and Magrino, Tom and Myers, Andrew C.},
  title =	{{A Tour of Gallifrey, a Language for Geodistributed Programming}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{11:1--11:19},
  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.11},
  URN =		{urn:nbn:de:0030-drops-105549},
  doi =		{10.4230/LIPIcs.SNAPL.2019.11},
  annote =	{Keywords: programming languages, distributed systems, weak consistency, linear types}
}
  • Refine by Author
  • 3 Ferreira, Carla
  • 2 De Porre, Kevin
  • 2 Gonzalez Boix, Elisa
  • 1 Beillahi, Sidi Mohamed
  • 1 Bouajjani, Ahmed
  • Show More...

  • Refine by Classification
  • 3 Computing methodologies → Distributed programming languages
  • 2 Software and its engineering → Domain specific languages
  • 2 Theory of computation → Distributed algorithms
  • 1 Information systems → Document representation
  • 1 Information systems → Retrieval models and ranking
  • Show More...

  • Refine by Keyword
  • 4 distributed systems
  • 2 eventual consistency
  • 2 replicated data types
  • 2 verification
  • 1 Causal Consistency
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 4 2019
  • 2 2023
  • 1 2020

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