Issue
DARTS, Volume 5, Issue 2
Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
-
Part of:
Volume:
DARTS, Volume 5 (ECOOP 2019)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Publication Details
- published at: 2019-07-11
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts5
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 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Abstract
Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as
Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 0:i-0:xi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{christakis_et_al:DARTS.5.2.0,
author = {Christakis, Maria and Rigger, Manuel},
title = {{Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
pages = {0:i--0:xi},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Christakis, Maria and Rigger, Manuel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.0},
URN = {urn:nbn:de:0030-drops-107779},
doi = {10.4230/DARTS.5.2.0},
annote = {Keywords: Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
Artifact
Godot: All the Benefits of Implicit and Explicit Futures (Artifact)
Abstract
This artifact contains an implementation of data-flow futures in terms of control-flow futures, in the Scala language. In the implementation, we show microbenchmarks that solve the three identified problems from the paper:
1) The Type Proliferation Problem,
2) The Fulfilment Observation Problem, and
3) The Future Proliferation Problem
There are also detailed instructions on design decisions that differ from the formal semantics and restrictions on the limits of how much can be encoded in the Scala language. We provide examples, e.g., creation of a proxy service using data-flow futures, as well as tests that exercise different parts of the type system.
Cite as
Kiko Fernandez-Reyes, Dave Clarke, Ludovic Henrio, Einar Broch Johnsen, and Tobias Wrigstad. Godot: All the Benefits of Implicit and Explicit Futures (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{fernandezreyes_et_al:DARTS.5.2.1,
author = {Fernandez-Reyes, Kiko and Clarke, Dave and Henrio, Ludovic and Johnsen, Einar Broch and Wrigstad, Tobias},
title = {{Godot: All the Benefits of Implicit and Explicit Futures}},
pages = {1:1--1:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Fernandez-Reyes, Kiko and Clarke, Dave and Henrio, Ludovic and Johnsen, Einar Broch and Wrigstad, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.1},
URN = {urn:nbn:de:0030-drops-107786},
doi = {10.4230/DARTS.5.2.1},
annote = {Keywords: Futures, Concurrency, Type Systems, Formal Semantics}
}
Document
Artifact
DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access (Artifact)
Abstract
This artifact contains the source code of DynaSOAr, a CUDA framework for Single-Method Multiple-Objects (SMMO) applications. SMMO is a type of object-oriented programs in which parallelism is expressed by running the same method on all applications of a type.
DynaSOAr is a dynamic memory allocator, combined with a data layout DSL and a parallel do-all operation. This artifact provides a tutorial explaining the API of DynaSOAr, along with nine benchmark applications from different domains. All benchmarks can be configured to use a different memory allocator to allow for a comparison with other state-of-the-art memory allocators.
Cite as
Matthias Springer and Hidehiko Masuhara. DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{springer_et_al:DARTS.5.2.2,
author = {Springer, Matthias and Masuhara, Hidehiko},
title = {{DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access}},
pages = {2:1--2:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Springer, Matthias and Masuhara, Hidehiko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.2},
URN = {urn:nbn:de:0030-drops-107793},
doi = {10.4230/DARTS.5.2.2},
annote = {Keywords: CUDA, Data Layout, Dynamic Memory Allocation, GPUs, Object-oriented Programming, SIMD, Single-Instruction Multiple-Objects, Structure of Arrays}
}
Document
Artifact
NumLin: Linear Types for Linear Algebra (Artifact)
Abstract
The artifact package includes a Debian 9.7 Stretch VirtualBox virtual machine on which is the implementation of NumLin and the required OCaml platform and packages.
Cite as
Dhruv C. Makwana and Neelakantan R. Krishnaswami. NumLin: Linear Types for Linear Algebra (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{makwana_et_al:DARTS.5.2.3,
author = {Makwana, Dhruv C. and Krishnaswami, Neelakantan R.},
title = {{NumLin: Linear Types for Linear Algebra}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Makwana, Dhruv C. and Krishnaswami, Neelakantan R.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.3},
URN = {urn:nbn:de:0030-drops-107806},
doi = {10.4230/DARTS.5.2.3},
annote = {Keywords: numerical, linear, algebra, types, permissions, OCaml}
}
Document
Artifact
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Artifact)
Abstract
Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, their non-deterministic behavior makes it hard to debug. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow exploring a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the conditions to trigger are not reached. As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allow developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a proof of concept multiverse debugger that takes as input Featherweight AmbientTalk programs written in PLT-Redex, and allows programmers to interactively browse all possible execution states by means of multiverse breakpoints and stepping commands. We provide a proof of non-interference, i.e we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.
Cite as
Robbert Gurdeep Singh, Carmen Torres Lopez, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{singh_et_al:DARTS.5.2.4,
author = {Singh, Robbert Gurdeep and Lopez, Carmen Torres and Marr, Stefan and Boix, Elisa Gonzalez and Scholliers, Christophe},
title = {{Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs}},
pages = {4:1--4:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Singh, Robbert Gurdeep and Lopez, Carmen Torres and Marr, Stefan and Boix, Elisa Gonzalez and Scholliers, Christophe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.4},
URN = {urn:nbn:de:0030-drops-107815},
doi = {10.4230/DARTS.5.2.4},
annote = {Keywords: Debugging, Concurrency, Actors, Formal Semantics}
}
Document
Artifact
Minimal Session Types (Artifact)
Abstract
This artifact contains MISTY, a tool that decomposes message-passing programs with session types into programs typable with the minimal session types we introduce in our ECOOP paper. MISTY incorporates a domain-specific language for message-passing concurrency based on a higher-order process calculus with {session types}. Given a source program in this language, MISTY follows the results in our ECOOP paper to produce LaTeX code for its corresponding decomposition. To demonstrate the tight connection between source and decomposed programs, MISTY also allows users to simulate their corresponding reductions.
Cite as
Alen Arslanagić, Jorge A. Pérez, and Erik Voogd. Minimal Session Types (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{arslanagic_et_al:DARTS.5.2.5,
author = {Arslanagi\'{c}, Alen and P\'{e}rez, Jorge A. and Voogd, Erik},
title = {{Minimal Session Types}},
pages = {5:1--5:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Arslanagi\'{c}, Alen and P\'{e}rez, Jorge A. and Voogd, Erik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.5},
URN = {urn:nbn:de:0030-drops-107825},
doi = {10.4230/DARTS.5.2.5},
annote = {Keywords: Session types, process calculi, pi-calculus}
}
Document
Artifact
Deep Static Modeling of invokedynamic (Artifact)
Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.
Cite as
George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 6:1-6:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{fourtounis_et_al:DARTS.5.2.6,
author = {Fourtounis, George and Smaragdakis, Yannis},
title = {{Deep Static Modeling of invokedynamic}},
pages = {6:1--6:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Fourtounis, George and Smaragdakis, Yannis},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.6},
URN = {urn:nbn:de:0030-drops-107835},
doi = {10.4230/DARTS.5.2.6},
annote = {Keywords: invokedynamic, lambdas, static analysis}
}
Document
Artifact
Garbage-Free Abstract Interpretation Through Abstract Reference Counting (Artifact)
Abstract
This artifact is a modified version of Scala-AM, an abstract interpretation framework implemented in Scala. Specifically, we extended Scala-AM with several implementations of machine abstractions that each employ a different approach to abstract garbage collection. These include traditional (tracing-based) approaches to abstract garbage collection, as well as our own novel approach using abstract reference counting. In particular, using the machine abstraction that employs abstract reference counting (with cycle detection) results in a garbage-free abstract interpreter can greatly improve both the precision and performance of the corresponding machine abstraction in the original version of the Scala-AM framework.
We have set up the framework in such a way that one can easily run a variety of experiments to use, evaluate and compare these approaches to abstract garbage collection. This artifact contains documentation on how these experiments can be configured, specifically to reproduce the results presented in the companion paper.
Cite as
Noah Van Es, Quentin Stiévenart, and Coen De Roover. Garbage-Free Abstract Interpretation Through Abstract Reference Counting (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{vanes_et_al:DARTS.5.2.7,
author = {Van Es, Noah and Sti\'{e}venart, Quentin and De Roover, Coen},
title = {{Garbage-Free Abstract Interpretation Through Abstract Reference Counting}},
pages = {7:1--7:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Van Es, Noah and Sti\'{e}venart, Quentin and De Roover, Coen},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.7},
URN = {urn:nbn:de:0030-drops-107843},
doi = {10.4230/DARTS.5.2.7},
annote = {Keywords: static analysis, abstract interpretation, abstract garbage collection, reference counting}
}
Document
Artifact
On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact)
Abstract
This is the artifact for the pearl paper "On Julia’s efficient algorithm for subtyping union types and covariant tuples."
Cite as
Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{chung_et_al:DARTS.5.2.8,
author = {Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
title = {{On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples}},
pages = {8:1--8:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.8},
URN = {urn:nbn:de:0030-drops-107855},
doi = {10.4230/DARTS.5.2.8},
annote = {Keywords: Type systems, subtyping, algorithmic type systems, distributive unions}
}
Document
Artifact
Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language (Artifact)
Abstract
There are two components to this artifact. First, a we provide a mechanization of the formalization in the paper, as well as mechanized proofs of the main results from the paper. Second, we provide a full implementation of Poseidon Lua, the language implemented in the paper. Instructions for all components of the artifact are included this document.
Cite as
Alexi Turcotte, Ellen Arteca, and Gregor Richards. Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{turcotte_et_al:DARTS.5.2.9,
author = {Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
title = {{Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language}},
pages = {9:1--9:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.9},
URN = {urn:nbn:de:0030-drops-107863},
doi = {10.4230/DARTS.5.2.9},
annote = {Keywords: Language design, Language interoperation, Formal semantics}
}
Document
Artifact
Semantic Patches for Java Program Transformation (Artifact)
Abstract
The program transformation tool Coccinelle is designed for making changes that is required in many locations within a software project. It has been shown to be useful for C code and has been been adopted for use in the Linux kernel by many developers. Over 6000 commits mentioning the use of Coccinelle have been made in the Linux kernel.
Our artifact, Coccinelle4J, is an extension to Coccinelle in order for it to apply program transformations to Java source code. This artifact accompanies our experience report "Semantic Patches for Java Program Transformation", in which we show a case study of applying code transformations to upgrade usage of deprecated Android API methods to replacement API methods.
Cite as
Hong Jin Kang, Ferdian Thung, Julia Lawall, Gilles Muller, Lingxiao Jiang, and David Lo. Semantic Patches for Java Program Transformation (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{kang_et_al:DARTS.5.2.10,
author = {Kang, Hong Jin and Thung, Ferdian and Lawall, Julia and Muller, Gilles and Jiang, Lingxiao and Lo, David},
title = {{Semantic Patches for Java Program Transformation}},
pages = {10:1--10:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Kang, Hong Jin and Thung, Ferdian and Lawall, Julia and Muller, Gilles and Jiang, Lingxiao and Lo, David},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.10},
URN = {urn:nbn:de:0030-drops-107875},
doi = {10.4230/DARTS.5.2.10},
annote = {Keywords: Java, semantic patches, automatic program transformation}
}
Document
Artifact
Automated Large-Scale Multi-Language Dynamic Program Analysis in the Wild (Artifact)
Abstract
This artifact provides a preliminary release of NAB, a distributed infrastructure for executing large-scale dynamic program analyses (DPAs). The artifact consists of ready-to-use Docker containers that allow one to run different DPA tools (Deep-Promise, JITProf, and tgp) on Node.js, Java, and Scala projects hosted on GitHub. The artifact enables the reproduction of the figures and tables of the related paper "Automated Large-scale Multi-language Dynamic Program Analysis in the Wild" with pre-collected data (several GBs) and the execution of DPAs on specific sets of GitHub projects.
Cite as
Alex Villazón, Haiyang Sun, Andrea Rosà, Eduardo Rosales, Daniele Bonetta, Isabella Defilippis, Sergio Oporto, and Walter Binder. Automated Large-Scale Multi-Language Dynamic Program Analysis in the Wild (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 11:1-11:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{villazon_et_al:DARTS.5.2.11,
author = {Villaz\'{o}n, Alex and Sun, Haiyang and Ros\`{a}, Andrea and Rosales, Eduardo and Bonetta, Daniele and Defilippis, Isabella and Oporto, Sergio and Binder, Walter},
title = {{Automated Large-Scale Multi-Language Dynamic Program Analysis in the Wild}},
pages = {11:1--11:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Villaz\'{o}n, Alex and Sun, Haiyang and Ros\`{a}, Andrea and Rosales, Eduardo and Bonetta, Daniele and Defilippis, Isabella and Oporto, Sergio and Binder, Walter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.11},
URN = {urn:nbn:de:0030-drops-107881},
doi = {10.4230/DARTS.5.2.11},
annote = {Keywords: Dynamic program analysis, code repositories, GitHub, Node.js, Java, Scala, promises, JIT-unfriendly code, task granularity}
}
Document
Artifact
Fling - A Fluent API Generator (Artifact)
Abstract
The first general and practical solution of the fluent API problem is presented. We give an algorithm that given a deterministic context free language (equivalently, LR(k), k >= 0 language) encodes it in an unbounded parametric polymorphism type system employing only a polynomial number of types. The theoretical result is employed in an actual tool Fling - a fluent API compiler-compiler in the style of YACC, tailored for embedding DSLs in Java.
Cite as
Ori Roth and Yossi Gil. Fling - A Fluent API Generator (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 12:1-12:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{roth_et_al:DARTS.5.2.12,
author = {Roth, Ori and Gil, Yossi},
title = {{Fling - A Fluent API Generator}},
pages = {12:1--12:9},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Roth, Ori and Gil, Yossi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.12},
URN = {urn:nbn:de:0030-drops-107897},
doi = {10.4230/DARTS.5.2.12},
annote = {Keywords: Fluent API, compilation, generics, code generation}
}
Document
Artifact
Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact)
Abstract
Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.
Cite as
Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{meier_et_al:DARTS.5.2.13,
author = {Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
title = {{Lifestate: Event-Driven Protocols and Callback Control Flow}},
pages = {13:1--13:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
number = {2},
editor = {Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.13},
URN = {urn:nbn:de:0030-drops-107902},
doi = {10.4230/DARTS.5.2.13},
annote = {Keywords: domain-specific languages, event-based programming, language implementation, new programming models or languages, object-oriented programming, semantics, testing, verification, automated}
}
Document
Artifact
A Typing Discipline for Hardware Interfaces (Artifact)
Abstract
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such a separation of concerns, such tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.
Cite as
Jan de Muijnck-Hughes and Wim Vanderbauwhede. A Typing Discipline for Hardware Interfaces (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 14:1-14:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Article{demuijnckhughes_et_al:DARTS.5.2.14,
author = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
title = {{A Typing Discipline for Hardware Interfaces}},
pages = {14:1--14:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2019},
volume = {5},
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-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.14},
URN = {urn:nbn:de:0030-drops-107919},
doi = {10.4230/DARTS.5.2.14},
annote = {Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing}
}