Issue
DARTS, Volume 9, Issue 2
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
-
Part of:
Volume:
DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2023-07-11
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts9
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Front Matter
Front Matter - ECOOP 2023 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Abstract
Front Matter - ECOOP 2023 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{deleon_et_al:DARTS.9.2.0,
author = {de Le\'{o}n, Hern\'{a}n Ponce and Winter, Stefan},
title = {{Front Matter - ECOOP 2023 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {de Le\'{o}n, Hern\'{a}n Ponce and Winter, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.0},
URN = {urn:nbn:de:0030-drops-182401},
doi = {10.4230/DARTS.9.2.0},
annote = {Keywords: Front Matter - ECOOP 2023 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
Artifact
Python Type Hints Are Turing Complete (Artifact)
Abstract
The artifact comprises a Docker image (virtual environment) containing the source code and experiments setup mentioned in the paper. The artifact is available on Zenodo. The anonymous version submitted to the ECOOP Artifact Evaluation Committee (AEC) is also available on Zenodo. The project is maintained on GitHub.
Cite as
Ori Roth. Python Type Hints Are Turing Complete (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{roth:DARTS.9.2.1,
author = {Roth, Ori},
title = {{Python Type Hints Are Turing Complete (Artifact)}},
pages = {1:1--1:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Roth, Ori},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.1},
URN = {urn:nbn:de:0030-drops-182418},
doi = {10.4230/DARTS.9.2.1},
annote = {Keywords: nominal Subtyping with Variance, Python}
}
Document
Artifact
Dependent Merges and First-Class Environments (Artifact)
Abstract
This artifact contains the mechanical formalization of the calculi associated with the paper Dependent Merges and First-Class Environments. All of the metatheory has been formalized in Coq theorem prover. The paper studies a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them.
Cite as
Jinhao Tan and Bruno C. d. S. Oliveira. Dependent Merges and First-Class Environments (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{tan_et_al:DARTS.9.2.2,
author = {Tan, Jinhao and Oliveira, Bruno C. d. S.},
title = {{Dependent Merges and First-Class Environments (Artifact)}},
pages = {2:1--2:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Tan, Jinhao and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.2},
URN = {urn:nbn:de:0030-drops-182427},
doi = {10.4230/DARTS.9.2.2},
annote = {Keywords: First-class Environments, Disjointness, Intersection Types}
}
Document
Artifact
Sinatra: Stateful Instantaneous Updates for Commercial Browsers Through Multi-Version eXecution (Artifact)
Abstract
This document describes the artifact for the paper Sinatra: Stateful Instantaneous Updates for Commercial Browsers through Multi-Version eXecution.
Cite as
Ugnius Rumsevicius, Siddhanth Venkateshwaran, Ellen Kidane, and Luís Pina. Sinatra: Stateful Instantaneous Updates for Commercial Browsers Through Multi-Version eXecution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{rumsevicius_et_al:DARTS.9.2.3,
author = {Rumsevicius, Ugnius and Venkateshwaran, Siddhanth and Kidane, Ellen and Pina, Lu{\'\i}s},
title = {{Sinatra: Stateful Instantaneous Updates for Commercial Browsers Through Multi-Version eXecution (Artifact)}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Rumsevicius, Ugnius and Venkateshwaran, Siddhanth and Kidane, Ellen and Pina, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.3},
URN = {urn:nbn:de:0030-drops-182431},
doi = {10.4230/DARTS.9.2.3},
annote = {Keywords: Internet browsers, dynamic software updating, multi-version execution}
}
Document
Artifact
Wiring Circuits Is Easy as {0, 1, ω}, or Is It... (Artifact)
Abstract
We present two proof-of-concept languages (Circuits & CirQTS) that showcases how fancy types (namely linear & dependent types) can enrich hardware design tooling such that we can move existing external static analysis checks into the language’s type-system. Using our approach will lead to the enhanced safety of designs, and increase in design productivity, through early identification and reduction of connection errors.
This artefact presents our verified implementations (as realised in Idris2) of the simply (Circuits) and fancily typed (CirQTS) languages, and the test suite used to assess efficacy of our approach.
Cite as
Jan de Muijnck-Hughes and Wim Vanderbauwhede. Wiring Circuits Is Easy as {0, 1, ω}, or Is It... (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{demuijnckhughes_et_al:DARTS.9.2.4,
author = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
title = {{Wiring Circuits Is Easy as \{0, 1, \omega\}, or Is It... (Artifact)}},
pages = {4:1--4:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.4},
URN = {urn:nbn:de:0030-drops-182442},
doi = {10.4230/DARTS.9.2.4},
annote = {Keywords: Hardware Design, Linear Types, Dependent Types, DSLs, Idris, SystemVerilog, Netlists}
}
Document
Artifact
Do Machine Learning Models Produce TypeScript Types That Type Check? (Artifact)
Abstract
Type migration is the process of adding types to untyped code to gain assurance at compile time. TypeScript and other gradual type systems facilitate type migration by allowing programmers to start with imprecise types and gradually strengthen them. However, adding types is a manual effort and several migrations on large, industry codebases have been reported to have taken several years. In the research community, there has been significant interest in using machine learning to automate TypeScript type migration. Existing machine learning models report a high degree of accuracy in predicting individual TypeScript type annotations. However, in this paper we argue that accuracy can be misleading, and we should address a different question: can an automatic type migration tool produce code that passes the TypeScript type checker?
We present TypeWeaver, a TypeScript type migration tool that can be used with an arbitrary type prediction model. We evaluate TypeWeaver with three models from the literature: DeepTyper, a recurrent neural network; LambdaNet, a graph neural network; and InCoder, a general-purpose, multi-language transformer that supports fill-in-the-middle tasks. Our tool automates several steps that are necessary for using a type prediction model, including (1) importing types for a project’s dependencies; (2) migrating JavaScript modules to TypeScript notation; (3) inserting predicted type annotations into the program to produce TypeScript when needed; and (4) rejecting non-type predictions when needed.
We evaluate TypeWeaver on a dataset of 513 JavaScript packages, including packages that have never been typed before. With the best type prediction model, we find that only 21% of packages type check, but more encouragingly, 69% of files type check successfully.
Cite as
Ming-Ho Yee and Arjun Guha. Do Machine Learning Models Produce TypeScript Types That Type Check? (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{yee_et_al:DARTS.9.2.5,
author = {Yee, Ming-Ho and Guha, Arjun},
title = {{Do Machine Learning Models Produce TypeScript Types That Type Check? (Artifact)}},
pages = {5:1--5:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Yee, Ming-Ho and Guha, Arjun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.5},
URN = {urn:nbn:de:0030-drops-182456},
doi = {10.4230/DARTS.9.2.5},
annote = {Keywords: Type migration, deep learning}
}
Document
Artifact
Semantics for Noninterference with Interaction Trees (Artifact)
Abstract
Noninterference is the strong information-security property that a program does not leak secrets through publicly-visible behavior. In the presence of effects such as nontermination, state, and exceptions, reasoning about noninterference quickly becomes subtle. We advocate using interaction trees (ITrees) to provide compositional mechanized proofs of noninterference for multi-language, effectful, nonterminating programs, while retaining executability of the semantics. We develop important foundations for security analysis with ITrees: two indistinguishability relations, leading to two standard notions of noninterference with adversaries of different strength, along with metatheory libraries for reasoning about each. We demonstrate the utility of our results using a simple imperative language with embedded assembly, along with a compiler into that assembly language.
Cite as
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{silver_et_al:DARTS.9.2.6,
author = {Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
title = {{Semantics for Noninterference with Interaction Trees (Artifact)}},
pages = {6:1--6:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.6},
URN = {urn:nbn:de:0030-drops-182465},
doi = {10.4230/DARTS.9.2.6},
annote = {Keywords: verification, information-flow, denotational semantics, monads}
}
Document
Artifact
Toward Tool-Independent Summaries for Symbolic Execution (Artifact)
Abstract
The artifact contains the extended versions of the tools angr and AVD with support for the symbolic reflection API proposed in the paper. Additionally, the artifact contains the source code of SumBoundVerify, our novel tool for the bounded-verification of symbolic summaries for the C programming language. The artifact contains all the scripts and datasets required to obtain the results presented in the paper, including: a library of 67 symbolic summaries implemented using the proposed symbolic reflection API; two symbolic test suites designed to test two open source C libraries; and the source code of the third-party summaries that were validated checked with SumBoundVerify.
Cite as
Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{ramos_et_al:DARTS.9.2.7,
author = {Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
title = {{Toward Tool-Independent Summaries for Symbolic Execution (Artifact)}},
pages = {7:1--7:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.7},
URN = {urn:nbn:de:0030-drops-182478},
doi = {10.4230/DARTS.9.2.7},
annote = {Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries}
}
Document
Artifact
Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)
Abstract
This paper presents a specification framework for monadic, recursive, interactive programs that supports auto-active verification, an approach that combines user-provided guidance with automatic verification techniques. This verification tool is designed to have the flexibility of a manual approach to verification along with the usability benefits of automatic approaches. We accomplish this by augmenting Interaction Trees, a Coq datastructure for representing effectful computations, with logical quantifier events. We show that this yields a language of specifications that are easy to understand, automatable, and are powerful enough to handle properties that involve non-termination. Our framework is implemented as a library in Coq. We demonstrate the effectiveness of this framework by verifying real, low-level code.
Cite as
Lucas Silver, Eddy Westbrook, Matthew Yacavone, and Ryan Scott. Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{silver_et_al:DARTS.9.2.8,
author = {Silver, Lucas and Westbrook, Eddy and Yacavone, Matthew and Scott, Ryan},
title = {{Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)}},
pages = {8:1--8:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Silver, Lucas and Westbrook, Eddy and Yacavone, Matthew and Scott, Ryan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.8},
URN = {urn:nbn:de:0030-drops-182485},
doi = {10.4230/DARTS.9.2.8},
annote = {Keywords: coinduction, specification, verification, monads}
}
Document
Artifact
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)
Abstract
We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop failures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is executable and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article.
Cite as
Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 9:1-9:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{barwell_et_al:DARTS.9.2.9,
author = {Barwell, Adam D. and Hou, Ping and Yoshida, Nobuko and Zhou, Fangyi},
title = {{Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)}},
pages = {9:1--9:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Barwell, Adam D. and Hou, Ping and Yoshida, Nobuko and Zhou, Fangyi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.9},
URN = {urn:nbn:de:0030-drops-182492},
doi = {10.4230/DARTS.9.2.9},
annote = {Keywords: Session Types, Concurrency, Failure Handling, Code Generation, Scala}
}
Document
Artifact
Dynamically Updatable Multiparty Session Protocols (Artifact)
Abstract
Multiparty Session Types (MPST) are typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang.
This artifact contains an implementation of Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. DMst guarantees deadlock-freedom and liveness. The artifact comprises a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate GoScr by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.
Cite as
David Castro-Perez and Nobuko Yoshida. Dynamically Updatable Multiparty Session Protocols (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{castroperez_et_al:DARTS.9.2.10,
author = {Castro-Perez, David and Yoshida, Nobuko},
title = {{Dynamically Updatable Multiparty Session Protocols (Artifact)}},
pages = {10:1--10:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Castro-Perez, David and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10},
URN = {urn:nbn:de:0030-drops-182505},
doi = {10.4230/DARTS.9.2.10},
annote = {Keywords: Multiparty Session Types, Correctness-by-construction, Concurrency, Golang}
}
Document
Artifact
LoRe: A Programming Model for Verifiably Safe Local-First Software (Artifact)
Abstract
Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions.
We propose LoRe, a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that LoRe simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.
Cite as
Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, and Mira Mezini. LoRe: A Programming Model for Verifiably Safe Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{haas_et_al:DARTS.9.2.11,
author = {Haas, Julian and Mogk, Ragnar and Yanakieva, Elena and Bieniusa, Annette and Mezini, Mira},
title = {{LoRe: A Programming Model for Verifiably Safe Local-First Software (Artifact)}},
pages = {11:1--11:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Haas, Julian and Mogk, Ragnar and Yanakieva, Elena and Bieniusa, Annette and Mezini, Mira},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.11},
URN = {urn:nbn:de:0030-drops-182510},
doi = {10.4230/DARTS.9.2.11},
annote = {Keywords: Local-First Software, Reactive Programming, Invariants, Consistency, Automated Verification}
}
Document
Artifact
Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact)
Abstract
In this artifact, we provide an implementation of the λ^res_var calculus, as described in the related article. The implementation is an extension of the Flix programming language compiler, supporting restrictable variants and the two partial pattern-matching constructs: choose and choose-⋆.
The artifact consists of the extended Flix compiler, a Visual Studio Code extension supporting common IDE features such as syntax highlighting and type hovering, and a collection of Flix files demonstrating the use of restrictable variants. The Flix files correspond to examples presented in the paper.
Users are invited to modify the Flix files in order to observe the influence of their changes on the inferred types in the provided programs.
Cite as
Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze. Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{madsen_et_al:DARTS.9.2.12,
author = {Madsen, Magnus and Starup, Jonathan Lindegaard and Lutze, Matthew},
title = {{Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact)}},
pages = {12:1--12:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Madsen, Magnus and Starup, Jonathan Lindegaard and Lutze, Matthew},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.12},
URN = {urn:nbn:de:0030-drops-182521},
doi = {10.4230/DARTS.9.2.12},
annote = {Keywords: restrictable variants, extensible variants, refinement types, Boolean unification}
}
Document
Artifact
The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Artifact)
Abstract
Programming languages are often designed as static, monolithic units. As a result, they are inflexible. We show a new mechanism of programming language design that allows to more flexible languages: by using compile-time function execution and metaprogramming, we implement a language mostly in itself. Our approach is usable for creating feature-rich, yet low-overhead system programming languages. We illustrate it on two systems, one that lowers to C and one that lowers to LLVM.
Cite as
Simon Henniger and Nada Amin. The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{henniger_et_al:DARTS.9.2.13,
author = {Henniger, Simon and Amin, Nada},
title = {{The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Artifact)}},
pages = {13:1--13:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Henniger, Simon and Amin, Nada},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.13},
URN = {urn:nbn:de:0030-drops-182532},
doi = {10.4230/DARTS.9.2.13},
annote = {Keywords: extensible languages, meta programming, macros, program generation, compilation}
}
Document
Artifact
Behavioural Types for Local-First Software (Artifact)
Abstract
This artifact supports the theory of swarm protocols presented in the related article. Specifically, following the top-down development typical of choreographic approaches, our artifact enables the specification of systems of peers communicating through an event notification mechanism from a global viewpoint which can then be projected to local specifications of peers, rendered as machines. To the best of our knowledge, ours is the first implementation of a behavioural type framework supporting the application of the principles of local-first software for network devices which collaborate on a common task while retaining full autonomy. The artifact can be integrated in the Actyx industrial platform; this proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.
Cite as
Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{kuhn_et_al:DARTS.9.2.14,
author = {Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
title = {{Behavioural Types for Local-First Software (Artifact)}},
pages = {14:1--14:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.14},
URN = {urn:nbn:de:0030-drops-182541},
doi = {10.4230/DARTS.9.2.14},
annote = {Keywords: Distributed coordination, local-first software, behavioural types, publish-subscribe, asynchronous communication}
}
Document
Artifact
Modular Verification of State-Based CRDTs in Separation Logic (Artifact)
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
ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact)
Abstract
SAT/SMT-solvers and model checkers automate formal verification of sequential programs. Formal reasoning about scalable concurrent programs is still manual and requires expert knowledge. But scalability is a fundamental requirement of current and future programs.
Sequential imperative programs compose statements, function/method calls and control flow constructs. Concurrent programming models provide constructs for concurrent composition. Concurrency abstractions such as threads and synchronization primitives such as locks compose the individual parts of a concurrent program that are meant to execute in parallel. We propose to rather compose the individual parts again using sequential composition and compile this sequential composition into a concurrent one. The developer can use existing tools to formally verify the sequential program while the translated concurrent program provides the dearly requested scalability.
Following this insight, we present ConDRust, a new programming model and compiler for Rust programs. The ConDRust compiler translates sequential composition into a concurrent composition based on threads and message-passing channels. During compilation, the compiler preserves the semantics of the sequential program along with much desired properties such as determinism.
Our evaluation shows that our ConDRust compiler generates concurrent deterministic code that can outperform even non-deterministic programs by up to a factor of three for irregular algorithms that are particularly hard to parallelize.
Cite as
Felix Suchert, Lisza Zeidler, Jeronimo Castrillon, and Sebastian Ertel. ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{suchert_et_al:DARTS.9.2.16,
author = {Suchert, Felix and Zeidler, Lisza and Castrillon, Jeronimo and Ertel, Sebastian},
title = {{ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs (Artifact)}},
pages = {16:1--16:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Suchert, Felix and Zeidler, Lisza and Castrillon, Jeronimo and Ertel, Sebastian},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.16},
URN = {urn:nbn:de:0030-drops-182562},
doi = {10.4230/DARTS.9.2.16},
annote = {Keywords: concurrent programming, verification, scalability}
}
Document
Artifact
A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact)
Abstract
Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code.
In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.
Cite as
David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 17:1-17:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{richter_et_al:DARTS.9.2.17,
author = {Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
title = {{A Direct-Style Effect Notation for Sequential and Parallel Programs (Artifact)}},
pages = {17:1--17:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.17},
URN = {urn:nbn:de:0030-drops-182573},
doi = {10.4230/DARTS.9.2.17},
annote = {Keywords: do-notation, parallelism, concurrency, effects}
}
Document
Artifact
Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)
Abstract
Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications.
In the related article ("Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types", in ECOOP 2023, LIPIcs, Vol. 263, pp. 42:1-42:30), we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically.
Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. In the related article, we present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before).
As evidence that the new techniques are implementable, we implemented them; this implementation is available in this artifact.
Cite as
Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{jongmans_et_al:DARTS.9.2.18,
author = {Jongmans, Sung-Shik and Ferreira, Francisco},
title = {{Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)}},
pages = {18:1--18:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Jongmans, Sung-Shik and Ferreira, Francisco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.18},
URN = {urn:nbn:de:0030-drops-182580},
doi = {10.4230/DARTS.9.2.18},
annote = {Keywords: behavioural types, multiparty session types, choreographies}
}
Document
Artifact
VeriFx: Correct Replicated Data Types for the Masses (Artifact)
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
Artifact
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)
Abstract
Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve.
We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard.
When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation.
The artifact contains the source code of Hoogle⋆, as well as scripts to reproduce the evaluation done in the paper.
Cite as
Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{botelhoguerra_et_al:DARTS.9.2.20,
author = {Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
title = {{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)}},
pages = {20:1--20:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.20},
URN = {urn:nbn:de:0030-drops-182609},
doi = {10.4230/DARTS.9.2.20},
annote = {Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}
Document
Artifact
Automata Learning with an Incomplete Teacher (Artifact)
Abstract
We provide an implementation of the automata learning software described in the associated ECOOP article. In particular, the artifact is a Docker image with the source code for nerode and nerode-learn, along with the scripts and benchmark inputs needed to reproduce the experiments described in the paper.
Cite as
Mark Moeller, Thomas Wiener, Alaia Solko-Breslin, Caleb Koch, Nate Foster, and Alexandra Silva. Automata Learning with an Incomplete Teacher (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 21:1-21:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{moeller_et_al:DARTS.9.2.21,
author = {Moeller, Mark and Wiener, Thomas and Solko-Breslin, Alaia and Koch, Caleb and Foster, Nate and Silva, Alexandra},
title = {{Automata Learning with an Incomplete Teacher (Artifact)}},
pages = {21:1--21:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Moeller, Mark and Wiener, Thomas and Solko-Breslin, Alaia and Koch, Caleb and Foster, Nate and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.21},
URN = {urn:nbn:de:0030-drops-182612},
doi = {10.4230/DARTS.9.2.21},
annote = {Keywords: Finite Automata, Active Learning, SMT Solvers}
}
Document
Artifact
super-Charging Object-Oriented Programming Through Precise Typing of Open Recursion (Artifact)
Abstract
This artifact consists of an SBT project with a Scala implementation of the MLscript programming language extended with "super-charged" object-oriented programming features (SuperOOP), introduced in the corresponding paper. We provide a test suite that includes SuperOOP examples and a web demo that gives live typing and running results of the user input source.
Cite as
Andong Fan and Lionel Parreaux. super-Charging Object-Oriented Programming Through Precise Typing of Open Recursion (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 22:1-22:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{fan_et_al:DARTS.9.2.22,
author = {Fan, Andong and Parreaux, Lionel},
title = {{super-Charging Object-Oriented Programming Through Precise Typing of Open Recursion (Artifact)}},
pages = {22:1--22:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Fan, Andong and Parreaux, Lionel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.22},
URN = {urn:nbn:de:0030-drops-182626},
doi = {10.4230/DARTS.9.2.22},
annote = {Keywords: Object-Oriented Programming, the Expression Problem, Open Recursion}
}
Document
Artifact
Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact)
Abstract
A mandatory feature for blockchain software, such as smart contracts and decentralized applications, is determinism. In fact, non-deterministic behaviors do not allow blockchain nodes to reach one common consensual state or a deterministic response, which causes the blockchain to be forked, stopped, or to deny services. While domain-specific languages are deterministic by design, general-purpose languages widely used for the development of smart contracts such as Go, provide many sources of non-determinism. However, not all non-deterministic behaviours are critical. In fact, only those that affect the state or the response of the blockchain can cause problems, as other uses (for example, logging) are only observable by the node that executes the application and not by others. Therefore, some frameworks for blockchains, such as Hyperledger Fabric or Cosmos SDK, do not prohibit the use of non-deterministic constructs but leave the programmer the burden of ensuring that the blockchain application is deterministic. In this paper, we present a flow-based approach to detect non-deterministic vulnerabilities which could compromise the blockchain. The analysis is implemented in GoLiSA, a semantics-based static analyzer for Go applications. Our experimental results show that GoLiSA is able to detect all vulnerabilities related to non-determinism on a significant set of applications, with better results than other open-source analyzers for blockchain software written in Go.
Cite as
Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, and Fausto Spoto. Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 23:1-23:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{olivieri_et_al:DARTS.9.2.23,
author = {Olivieri, Luca and Negrini, Luca and Arceri, Vincenzo and Tagliaferro, Fabio and Ferrara, Pietro and Cortesi, Agostino and Spoto, Fausto},
title = {{Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact)}},
pages = {23:1--23:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Olivieri, Luca and Negrini, Luca and Arceri, Vincenzo and Tagliaferro, Fabio and Ferrara, Pietro and Cortesi, Agostino and Spoto, Fausto},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.23},
URN = {urn:nbn:de:0030-drops-182633},
doi = {10.4230/DARTS.9.2.23},
annote = {Keywords: Static Analysis, Program Verification, Non-determinism, Blockchain, Smart contracts, DApps, Go language}
}
Document
Artifact
Determinacy Race Detector for Promises (Artifact)
Abstract
Much of the past work on dynamic data-race and determinacy-race detection algorithms for task parallelism has focused on structured parallelism with fork-join constructs and, more recently, with future constructs. This paper addresses the problem of dynamic detection of data-races and determinacy-races in task-parallel programs with promises, which are more general than fork-join constructs and futures.
We have introduced a dynamic data race detector, DRDP, to help examine task-parallelism programs with promises. DRDP is designed for the HCLIB parallel programming model and capable of pinpointing data races in a HCLIB program. In this artifact, we provide the race detector implementation and all benchmarks to help reproduce the reported results in the paper.
Cite as
Feiyang Jin and Lechen Yu. Determinacy Race Detector for Promises (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 24:1-24:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{jin_et_al:DARTS.9.2.24,
author = {Jin, Feiyang and Yu, Lechen},
title = {{Determinacy Race Detector for Promises (Artifact)}},
pages = {24:1--24:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Jin, Feiyang and Yu, Lechen},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.24},
URN = {urn:nbn:de:0030-drops-182649},
doi = {10.4230/DARTS.9.2.24},
annote = {Keywords: Race detection, Promise, Determinism, Determinacy-race}
}
Document
Artifact
Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact)
Abstract
Cite as
Sarah Harris, Simon Cooksey, Michael Vollmer, and Mark Batty. Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 25:1-25:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{harris_et_al:DARTS.9.2.25,
author = {Harris, Sarah and Cooksey, Simon and Vollmer, Michael and Batty, Mark},
title = {{Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact)}},
pages = {25:1--25:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Harris, Sarah and Cooksey, Simon and Vollmer, Michael and Batty, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.25},
URN = {urn:nbn:de:0030-drops-182650},
doi = {10.4230/DARTS.9.2.25},
annote = {Keywords: Compilers, Rust, Memory Safety, CHERI}
}
Document
Artifact
Algebraic Replicated Data Types: Programming Secure Local-First Software (Artifact)
Abstract
This work is about programming support for local-first applications that manage private data locally, but still synchronize data between multiple devices. Typical use cases are synchronizing settings and data, and collaboration between multiple users. Such applications must preserve the privacy and integrity of the user’s data without impeding or interrupting the user’s normal workflow - even when the device is offline or has a flaky network connection.
From the programming perspective, availability along with privacy and security concerns pose significant challenges, for which developers have to learn and use specialized solutions such as conflict-free replicated data types (CRDTs) or APIs for centralized data stores. This work relieves developers from this complexity by enabling the direct and automatic use of algebraic data types - which developers already use to express the business logic of the application - for synchronization and collaboration. Moreover, we use this approach to provide end-to-end encryption and authentication between multiple replicas (using a shared secret) that is suitable for a coordination-free setting.
This artifact demonstrates the approach in the context of a realistic case study. It shows that an implementation of the approach can handle realistic workloads, that the size of the data types does not grow indefinitely, and that it is feasible to always enable encryption for the intended scenario.
Cite as
Christian Kuessner, Ragnar Mogk, Anna-Katharina Wickert, and Mira Mezini. Algebraic Replicated Data Types: Programming Secure Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 26:1-26:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Article{kuessner_et_al:DARTS.9.2.26,
author = {Kuessner, Christian and Mogk, Ragnar and Wickert, Anna-Katharina and Mezini, Mira},
title = {{Algebraic Replicated Data Types: Programming Secure Local-First Software (Artifact)}},
pages = {26:1--26:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Kuessner, Christian and Mogk, Ragnar and Wickert, Anna-Katharina and Mezini, Mira},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.26},
URN = {urn:nbn:de:0030-drops-182668},
doi = {10.4230/DARTS.9.2.26},
annote = {Keywords: local-first, data privacy, coordination freedom, CRDTs, AEAD}
}