Volume
LIPIcs, Volume 134
33rd European Conference on Object-Oriented Programming (ECOOP 2019)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
ECOOP 2019, July 15-19, 2019, London, United KingdomEditor
Publication Details
- published at: 2019-07-10
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-111-5
- DBLP: db/conf/ecoop/ecoop2019
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
Complete Volume
LIPIcs, Volume 134, ECOOP'19, Complete Volume
Abstract
LIPIcs, Volume 134, ECOOP'19, Complete Volume
Cite as
33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{donaldson:LIPIcs.ECOOP.2019,
title = {{LIPIcs, Volume 134, ECOOP'19, Complete Volume}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019},
URN = {urn:nbn:de:0030-drops-108979},
doi = {10.4230/LIPIcs.ECOOP.2019},
annote = {Keywords: Software and its engineering}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 0:i-0:xxv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{donaldson:LIPIcs.ECOOP.2019.0,
author = {Donaldson, Alastair F.},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {0:i--0:xxv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.0},
URN = {urn:nbn:de:0030-drops-107928},
doi = {10.4230/LIPIcs.ECOOP.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Lifestate: Event-Driven Protocols and Callback Control Flow
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. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{meier_et_al:LIPIcs.ECOOP.2019.1,
author = {Meier, Shawn and Mover, Sergio and Chang, Bor-Yuh Evan},
title = {{Lifestate: Event-Driven Protocols and Callback Control Flow}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {1:1--1:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.1},
URN = {urn:nbn:de:0030-drops-107932},
doi = {10.4230/LIPIcs.ECOOP.2019.1},
annote = {Keywords: event-driven systems, application-programming protocols, application framework interfaces, callbacks, sound framework modeling, predictive dynamic verification}
}
Document
Godot: All the Benefits of Implicit and Explicit Futures
Abstract
Concurrent programs often make use of futures, handles to the results of asynchronous operations. Futures provide means to communicate not yet computed results, and simplify the implementation of operations that synchronise on the result of such asynchronous operations. Futures can be characterised as implicit or explicit, depending on the typing discipline used to type them.
Current future implementations suffer from "future proliferation", either at the type-level or at run-time. The former adds future type wrappers, which hinders subtype polymorphism and exposes the client to the internal asynchronous communication architecture. The latter increases latency, by traversing nested future structures at run-time. Many languages suffer both kinds.
Previous work offer partial solutions to the future proliferation problems; in this paper we show how these solutions can be integrated in an elegant and coherent way, which is more expressive than either system in isolation. We describe our proposal formally, and state and prove its key properties, in two related calculi, based on the two possible families of future constructs (data-flow futures and control-flow futures). The former relies on static type information to avoid unwanted future creation, and the latter uses an algebraic data type with dynamic checks. We also discuss how to implement our new system efficiently.
Cite as
Kiko Fernandez-Reyes, Dave Clarke, Ludovic Henrio, Einar Broch Johnsen, and Tobias Wrigstad. Godot: All the Benefits of Implicit and Explicit Futures. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{fernandezreyes_et_al:LIPIcs.ECOOP.2019.2,
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}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {2:1--2:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.2},
URN = {urn:nbn:de:0030-drops-107949},
doi = {10.4230/LIPIcs.ECOOP.2019.2},
annote = {Keywords: Futures, Concurrency, Type Systems, Formal Semantics}
}
Document
Multitier Modules
Abstract
Multitier programming languages address the complexity of developing distributed systems abstracting over low level implementation details such as data representation, serialization and network protocols. Since the functionalities of different peers can be defined in the same compilation unit, multitier languages do not force developers to modularize software along network boundaries. Unfortunately, combining the code for all tiers into the same compilation unit poses a scalability challenge or forces developers to resort to traditional modularization abstractions that are agnostic to the multitier nature of the language.
In this paper, we address this issue with a module system for multitier languages. Our module system supports encapsulating each (cross-peer) functionality and defining it over abstract peer types. As a result, we disentangle modularization and distribution and we enable the definition of a distributed system as a composition of multitier modules, each representing a subsystem. Our case studies on distributed algorithms, distributed data structures, as well as on the Apache Flink task distribution system, show that multitier modules allow the definition of reusable (abstract) patterns of interaction in distributed software and enable separating the modularization and distribution concerns, properly separating functionalities in distributed systems.
Cite as
Pascal Weisenburger and Guido Salvaneschi. Multitier Modules. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 3:1-3:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{weisenburger_et_al:LIPIcs.ECOOP.2019.3,
author = {Weisenburger, Pascal and Salvaneschi, Guido},
title = {{Multitier Modules}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {3:1--3:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.3},
URN = {urn:nbn:de:0030-drops-107957},
doi = {10.4230/LIPIcs.ECOOP.2019.3},
annote = {Keywords: Distributed Programming, Multitier Programming, Abstract Peer Types, Placement Types, Module Systems, Scala}
}
Document
Scopes and Frames Improve Meta-Interpreter Specialization
Abstract
DynSem is a domain-specific language for concise specification of the dynamic semantics of programming languages, aimed at rapid experimentation and evolution of language designs. To maintain a short definition-to-execution cycle, DynSem specifications are meta-interpreted. Meta-interpretation introduces runtime overhead that is difficult to remove by using interpreter optimization frameworks such as the Truffle/Graal Java tools; previous work has shown order-of-magnitude improvements from applying Truffle/Graal to a meta-interpreter, but this is still far slower than what can be achieved with a language-specific interpreter. In this paper, we show how specifying the meta-interpreter using scope graphs, which encapsulate static name binding and resolution information, produces much better optimization results from Truffle/Graal. Furthermore, we identify that JIT compilation is hindered by large numbers of calls between small polymorphic rules and we introduce rule cloning to derive larger monomorphic rules at run time as a countermeasure. Our contributions improve the performance of DynSem-derived interpreters to within an order of magnitude of a handwritten language-specific interpreter.
Cite as
Vlad Vergu, Andrew Tolmach, and Eelco Visser. Scopes and Frames Improve Meta-Interpreter Specialization. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{vergu_et_al:LIPIcs.ECOOP.2019.4,
author = {Vergu, Vlad and Tolmach, Andrew and Visser, Eelco},
title = {{Scopes and Frames Improve Meta-Interpreter Specialization}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {4:1--4:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.4},
URN = {urn:nbn:de:0030-drops-107969},
doi = {10.4230/LIPIcs.ECOOP.2019.4},
annote = {Keywords: Definitional interpreters, partial evaluation}
}
Document
Transient Typechecks Are (Almost) Free
Abstract
Transient gradual typing imposes run-time type tests that typically cause a linear slowdown. This performance impact discourages the use of type annotations because adding types to a program makes the program slower. A virtual machine can employ standard just-in-time optimizations to reduce the overhead of transient checks to near zero. These optimizations can give gradually-typed languages performance comparable to state-of-the-art dynamic languages, so programmers can add types to their code without affecting their programs' performance.
Cite as
Richard Roberts, Stefan Marr, Michael Homer, and James Noble. Transient Typechecks Are (Almost) Free. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{roberts_et_al:LIPIcs.ECOOP.2019.5,
author = {Roberts, Richard and Marr, Stefan and Homer, Michael and Noble, James},
title = {{Transient Typechecks Are (Almost) Free}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {5:1--5:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.5},
URN = {urn:nbn:de:0030-drops-107974},
doi = {10.4230/LIPIcs.ECOOP.2019.5},
annote = {Keywords: dynamic type checking, gradual types, optional types, Grace, Moth, object-oriented programming}
}
Document
A Typing Discipline for Hardware Interfaces
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 separation of concerns, the 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 using 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. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{demuijnckhughes_et_al:LIPIcs.ECOOP.2019.6,
author = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
title = {{A Typing Discipline for Hardware Interfaces}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {6:1--6:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.6},
URN = {urn:nbn:de:0030-drops-107983},
doi = {10.4230/LIPIcs.ECOOP.2019.6},
annote = {Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing}
}
Document
On Satisfiability of Nominal Subtyping with Variance
Abstract
Nominal type systems with variance, the core of the subtyping relation in object-oriented programming languages like Java, C# and Scala, have been extensively studied by Kennedy and Pierce: they have shown the undecidability of the subtyping between ground types and proposed the decidable fragments of such type systems. However, modular verification of object-oriented code may require reasoning about the relations of open types. In this paper, we formalize and investigate the satisfiability problem for nominal subtyping with variance. We define the problem in the context of first-order logic. We show that although the non-expansive ground nominal subtyping with variance is decidable, its satisfiability problem is undecidable. Our proof uses a remarkably small fragment of the type system. In fact, we demonstrate that even for the non-expansive class tables with only nullary and unary covariant and invariant type constructors, the satisfiability of quantifier-free conjunctions of positive subtyping atoms is undecidable. We discuss this result in detail, as well as show one decidable fragment and a scheme for obtaining other decidable fragments.
Cite as
Aleksandr Misonizhnik and Dmitry Mordvinov. On Satisfiability of Nominal Subtyping with Variance. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{misonizhnik_et_al:LIPIcs.ECOOP.2019.7,
author = {Misonizhnik, Aleksandr and Mordvinov, Dmitry},
title = {{On Satisfiability of Nominal Subtyping with Variance}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.7},
URN = {urn:nbn:de:0030-drops-107997},
doi = {10.4230/LIPIcs.ECOOP.2019.7},
annote = {Keywords: nominal type systems, structural subtyping, first-order logic, decidability, software verification}
}
Document
Static Analysis for Asynchronous JavaScript Programs
Abstract
Asynchrony has become an inherent element of JavaScript, as an effort to improve the scalability and performance of modern web applications. To this end, JavaScript provides programmers with a wide range of constructs and features for developing code that performs asynchronous computations, including but not limited to timers, promises, and non-blocking I/O.
However, the data flow imposed by asynchrony is implicit, and not always well-understood by the developers who introduce many asynchrony-related bugs to their programs. Worse, there are few tools and techniques available for analyzing and reasoning about such asynchronous applications. In this work, we address this issue by designing and implementing one of the first static analysis schemes capable of dealing with almost all the asynchronous primitives of JavaScript up to the 7th edition of the ECMAScript specification.
Specifically, we introduce the callback graph, a representation for capturing data flow between asynchronous code. We exploit the callback graph for designing a more precise analysis that respects the execution order between different asynchronous functions. We parameterize our analysis with one novel context-sensitivity flavor, and we end up with multiple analysis variations for building callback graph.
We performed a number of experiments on a set of hand-written and real-world JavaScript programs. Our results show that our analysis can be applied to medium-sized programs achieving 79% precision, on average. The findings further suggest that analysis sensitivity is beneficial for the vast majority of the benchmarks. Specifically, it is able to improve precision by up to 28.5%, while it achieves an 88% precision on average without highly sacrificing performance.
Cite as
Thodoris Sotiropoulos and Benjamin Livshits. Static Analysis for Asynchronous JavaScript Programs. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sotiropoulos_et_al:LIPIcs.ECOOP.2019.8,
author = {Sotiropoulos, Thodoris and Livshits, Benjamin},
title = {{Static Analysis for Asynchronous JavaScript Programs}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {8:1--8:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.8},
URN = {urn:nbn:de:0030-drops-108007},
doi = {10.4230/LIPIcs.ECOOP.2019.8},
annote = {Keywords: static analysis, asynchrony, JavaScript}
}
Document
A Program Logic for First-Order Encapsulated WebAssembly
Abstract
We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.
Cite as
Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{watt_et_al:LIPIcs.ECOOP.2019.9,
author = {Watt, Conrad and Maksimovi\'{c}, Petar and Krishnaswami, Neelakantan R. and Gardner, Philippa},
title = {{A Program Logic for First-Order Encapsulated WebAssembly}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {9:1--9:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.9},
URN = {urn:nbn:de:0030-drops-108011},
doi = {10.4230/LIPIcs.ECOOP.2019.9},
annote = {Keywords: WebAssembly, program logic, separation logic, soundness, mechanisation}
}
Document
Garbage-Free Abstract Interpretation Through Abstract Reference Counting
Abstract
Abstract garbage collection is the application of garbage collection to an abstract interpreter. Existing work has shown that abstract garbage collection can improve both the interpreter’s precision and performance. Current approaches rely on heuristics to decide when to apply abstract garbage collection. Garbage will build up and impact precision and performance when the collection is applied infrequently, while too frequent applications will bring about their own performance overhead. A balance between these tradeoffs is often difficult to strike.
We propose a new approach to cope with the buildup of garbage in the results of an abstract interpreter. Our approach is able to eliminate all garbage, therefore obtaining the maximum precision and performance benefits of abstract garbage collection. At the same time, our approach does not require frequent heap traversals, and therefore adds little to the interpreters’s running time. The core of our approach uses reference counting to detect and eliminate garbage as soon as it arises. However, reference counting cannot deal with cycles, and we show that cycles are much more common in an abstract interpreter than in its concrete counterpart. To alleviate this problem, our approach detects cycles and employs reference counting at the level of strongly connected components. While this technique in general works for any system that uses reference counting, we argue that it works particularly well for an abstract interpreter. In fact, we show formally that for the continuation store, where most of the cycles occur, the cycle detection technique only requires O(1) amortized operations per continuation push.
We present our approach formally, and provide a proof-of-concept implementation in the Scala-AM framework. We empirically show our approach achieves both the optimal precision and significantly better performance compared to existing approaches to abstract garbage collection.
Cite as
Noah Van Es, Quentin Stiévenart, and Coen De Roover. Garbage-Free Abstract Interpretation Through Abstract Reference Counting. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 10:1-10:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{vanes_et_al:LIPIcs.ECOOP.2019.10,
author = {Van Es, Noah and Sti\'{e}venart, Quentin and De Roover, Coen},
title = {{Garbage-Free Abstract Interpretation Through Abstract Reference Counting}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {10:1--10:33},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.10},
URN = {urn:nbn:de:0030-drops-108022},
doi = {10.4230/LIPIcs.ECOOP.2019.10},
annote = {Keywords: abstract interpretation, abstract garbage collection, reference counting}
}
Document
Eventually Sound Points-To Analysis with Specifications
Abstract
Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing code, and then inserts runtime checks that report counterexamples to these assumptions that occur during execution. Our approach guarantees eventual soundness, which combines two guarantees: (i) the runtime checks are guaranteed to catch the first counterexample that occurs during any execution, in which case execution can be terminated to prevent harm, and (ii) only finitely many counterexamples ever occur, implying that the static analysis eventually becomes statically sound with respect to all remaining executions. We implement Optix, an eventually sound points-to analysis for Android apps, where the Android framework is missing. We show that the runtime checks added by Optix incur low overhead on real programs, and demonstrate how Optix improves a client information flow analysis for detecting Android malware.
Cite as
Osbert Bastani, Rahul Sharma, Lazaro Clapp, Saswat Anand, and Alex Aiken. Eventually Sound Points-To Analysis with Specifications. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bastani_et_al:LIPIcs.ECOOP.2019.11,
author = {Bastani, Osbert and Sharma, Rahul and Clapp, Lazaro and Anand, Saswat and Aiken, Alex},
title = {{Eventually Sound Points-To Analysis with Specifications}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {11:1--11:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.11},
URN = {urn:nbn:de:0030-drops-108038},
doi = {10.4230/LIPIcs.ECOOP.2019.11},
annote = {Keywords: specification inference, static points-to analysis, runtime monitoring}
}
Document
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
Abstract
The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used to represent packet data in P4, namely header types, lacks basic safety guarantees. Over the last few years, experience with an increasing number of programs has shown the risks of the unsafe approach, which often leads to subtle software bugs.
This paper proposes SafeP4, a domain-specific language for programmable data planes in which all packet data is guaranteed to have a well-defined meaning and satisfy essential safety guarantees. We equip SafeP4 with a formal semantics and a static type system that statically guarantees header validity - a common source of safety bugs according to our analysis of real-world P4 programs. Statically ensuring header validity is challenging because the set of valid headers can be modified at runtime, making it a dynamic program property. Our type system achieves static safety by using a form of path-sensitive reasoning that tracks dynamic information from conditional statements, routing tables, and the control plane. Our evaluation shows that SafeP4’s type system can effectively eliminate common failures in many real-world programs.
Cite as
Matthias Eichholz, Eric Campbell, Nate Foster, Guido Salvaneschi, and Mira Mezini. How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 12:1-12:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{eichholz_et_al:LIPIcs.ECOOP.2019.12,
author = {Eichholz, Matthias and Campbell, Eric and Foster, Nate and Salvaneschi, Guido and Mezini, Mira},
title = {{How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {12:1--12:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.12},
URN = {urn:nbn:de:0030-drops-108041},
doi = {10.4230/LIPIcs.ECOOP.2019.12},
annote = {Keywords: P4, data plane programming, type systems}
}
Document
Fling - A Fluent API Generator
Abstract
We present the first general and practical solution of the fluent API problem - an algorithm, that given a deterministic 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 accompanied by an actual tool Fling - a fluent API compiler-compiler in the venue of YACC, tailored for embedding DSLs in Java.
Cite as
Yossi Gil and Ori Roth. Fling - A Fluent API Generator. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 13:1-13:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{gil_et_al:LIPIcs.ECOOP.2019.13,
author = {Gil, Yossi and Roth, Ori},
title = {{Fling - A Fluent API Generator}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {13:1--13:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.13},
URN = {urn:nbn:de:0030-drops-108053},
doi = {10.4230/LIPIcs.ECOOP.2019.13},
annote = {Keywords: fluent API, type system, compilation, code generation}
}
Document
NumLin: Linear Types for Linear Algebra
Abstract
We present NumLin, a functional programming language whose type system is designed to enforce the safe usage of the APIs of low-level linear algebra libraries (such as BLAS/LAPACK). We do so through a brief description of its key features and several illustrative examples. We show that NumLin’s type system is sound and that its implementation improves upon naïve implementations of linear algebra programs, almost towards C-levels of performance. By doing so, we demonstrate (a) that linear types are well-suited to expressing the APIs of low-level linear algebra libraries accurately and concisely and (b) that, despite the complexity of prior work on it, fractional permissions can actually be implemented using simple, well-known techniques and be used practically in real programs.
Cite as
Dhruv C. Makwana and Neelakantan R. Krishnaswami. NumLin: Linear Types for Linear Algebra. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 14:1-14:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{makwana_et_al:LIPIcs.ECOOP.2019.14,
author = {Makwana, Dhruv C. and Krishnaswami, Neelakantan R.},
title = {{NumLin: Linear Types for Linear Algebra}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {14:1--14:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.14},
URN = {urn:nbn:de:0030-drops-108069},
doi = {10.4230/LIPIcs.ECOOP.2019.14},
annote = {Keywords: numerical, linear, algebra, types, permissions, OCaml}
}
Document
Deep Static Modeling of invokedynamic
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. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{fourtounis_et_al:LIPIcs.ECOOP.2019.15,
author = {Fourtounis, George and Smaragdakis, Yannis},
title = {{Deep Static Modeling of invokedynamic}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {15:1--15:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.15},
URN = {urn:nbn:de:0030-drops-108076},
doi = {10.4230/LIPIcs.ECOOP.2019.15},
annote = {Keywords: static analysis, invokedynamic}
}
Document
Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language
Abstract
Foreign function interfaces (FFIs) allow programs written in one language (called the host language) to call functions written in another language (called the guest language), and are widespread throughout modern programming languages, with C FFIs being the most prevalent. Unfortunately, reasoning about C FFIs can be very challenging, particularly when using traditional methods which necessitate a full model of the guest language in order to guarantee anything about the whole language. To address this, we propose a framework for defining whole language semantics of FFIs without needing to model the guest language, which makes reasoning about C FFIs feasible. We show that with such a semantics, one can guarantee some form of soundness of the overall language, as well as attribute errors in well-typed host language programs to the guest language. We also present an implementation of this scheme, Poseidon Lua, which shows a speedup over a traditional Lua C FFI.
Cite as
Alexi Turcotte, Ellen Arteca, and Gregor Richards. Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 16:1-16:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{turcotte_et_al:LIPIcs.ECOOP.2019.16,
author = {Turcotte, Alexi and Arteca, Ellen and Richards, Gregor},
title = {{Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {16:1--16:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.16},
URN = {urn:nbn:de:0030-drops-108087},
doi = {10.4230/LIPIcs.ECOOP.2019.16},
annote = {Keywords: Formal Semantics, Language Interoperation, Lua, C, Foreign Function Interfaces}
}
Document
DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access
Abstract
Object-oriented programming has long been regarded as too inefficient for SIMD high-performance computing, despite the fact that many important HPC applications have an inherent object structure. On SIMD accelerators, including GPUs, this is mainly due to performance problems with memory allocation and memory access: There are a few libraries that support parallel memory allocation directly on accelerator devices, but all of them suffer from uncoalesed memory accesses.
We discovered a broad class of object-oriented programs with many important real-world applications that can be implemented efficiently on massively parallel SIMD accelerators. We call this class Single-Method Multiple-Objects (SMMO), because parallelism is expressed by running a method on all objects of a type.
To make fast GPU programming available to domain experts who are less experienced in GPU programming, we developed DynaSOAr, a CUDA framework for SMMO applications. DynaSOAr consists of (1) a fully-parallel, lock-free, dynamic memory allocator, (2) a data layout DSL and (3) an efficient, parallel do-all operation. DynaSOAr achieves performance superior to state-of-the-art GPU memory allocators by controlling both memory allocation and memory access.
DynaSOAr improves the usage of allocated memory with a Structure of Arrays (SOA) data layout and achieves low memory fragmentation through efficient management of free and allocated memory blocks with lock-free, hierarchical bitmaps. Contrary to other allocators, our design is heavily based on atomic operations, trading raw (de)allocation performance for better overall application performance. In our benchmarks, DynaSOAr achieves a speedup of application code of up to 3x over state-of-the-art allocators. Moreover, DynaSOAr manages heap memory more efficiently than other allocators, allowing programmers to run up to 2x larger problem sizes with the same amount of memory.
Cite as
Matthias Springer and Hidehiko Masuhara. DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 17:1-17:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{springer_et_al:LIPIcs.ECOOP.2019.17,
author = {Springer, Matthias and Masuhara, Hidehiko},
title = {{DynaSOAr: A Parallel Memory Allocator for Object-Oriented Programming on GPUs with Efficient Memory Access}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {17:1--17:37},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.17},
URN = {urn:nbn:de:0030-drops-108098},
doi = {10.4230/LIPIcs.ECOOP.2019.17},
annote = {Keywords: CUDA, Data Layout, Dynamic Memory Allocation, GPUs, Object-oriented Programming, SIMD, Single-Instruction Multiple-Objects, Structure of Arrays}
}
Document
Reliable State Machines: A Framework for Programming Reliable Cloud Services
Abstract
Building reliable applications for the cloud is challenging because of unpredictable failures during a program’s execution. This paper presents a programming framework, called Reliable State Machines (RSMs), that offers fault-tolerance by construction. In our framework, an application comprises several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is fault-tolerant by design, thereby offering the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide a .NET implementation of the RSM framework for deploying services to Microsoft Azure. We carry out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrite a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance.
Cite as
Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj, Pantazis Deligiannis, Chandramouleswaran Ravichandran, Akash Lal, Aseem Rastogi, and Raja Krishnaswamy. Reliable State Machines: A Framework for Programming Reliable Cloud Services. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{mukherjee_et_al:LIPIcs.ECOOP.2019.18,
author = {Mukherjee, Suvam and Raj, Nitin John and Govindraj, Krishnan and Deligiannis, Pantazis and Ravichandran, Chandramouleswaran and Lal, Akash and Rastogi, Aseem and Krishnaswamy, Raja},
title = {{Reliable State Machines: A Framework for Programming Reliable Cloud Services}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {18:1--18:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.18},
URN = {urn:nbn:de:0030-drops-108101},
doi = {10.4230/LIPIcs.ECOOP.2019.18},
annote = {Keywords: Fault tolerance, Cloud computing, Actor framework}
}
Document
Transferring Obligations Through Synchronizations
Abstract
One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.
Cite as
Jafar Hamin and Bart Jacobs. Transferring Obligations Through Synchronizations. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 19:1-19:58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{hamin_et_al:LIPIcs.ECOOP.2019.19,
author = {Hamin, Jafar and Jacobs, Bart},
title = {{Transferring Obligations Through Synchronizations}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {19:1--19:58},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.19},
URN = {urn:nbn:de:0030-drops-108113},
doi = {10.4230/LIPIcs.ECOOP.2019.19},
annote = {Keywords: Hoare logic, separation logic, modular program verification, synchronization, transferring obligations, deadlock-freedom}
}
Document
Tool Insights Paper
Automated Large-Scale Multi-Language Dynamic Program Analysis in the Wild (Tool Insights Paper)
Abstract
Today’s availability of open-source software is overwhelming, and the number of free, ready-to-use software components in package repositories such as NPM, Maven, or SBT is growing exponentially. In this paper we address two straightforward yet important research questions: would it be possible to develop a tool to automate dynamic program analysis on public open-source software at a large scale? Moreover, and perhaps more importantly, would such a tool be useful? We answer the first question by introducing NAB, a tool to execute large-scale dynamic program analysis of open-source software in the wild. NAB is fully-automatic, language-agnostic, and can scale dynamic program analyses on open-source software up to thousands of projects hosted in code repositories. Using NAB, we analyzed more than 56K Node.js, Java, and Scala projects. Using the data collected by NAB we were able to (1) study the adoption of new language constructs such as JavaScript Promises, (2) collect statistics about bad coding practices in JavaScript, and (3) identify Java and Scala task-parallel workloads suitable for inclusion in a domain-specific benchmark suite. We consider such findings and the collected data an affirmative answer to the second question.
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 (Tool Insights Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{villazon_et_al:LIPIcs.ECOOP.2019.20,
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}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {20:1--20:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.20},
URN = {urn:nbn:de:0030-drops-108127},
doi = {10.4230/LIPIcs.ECOOP.2019.20},
annote = {Keywords: Dynamic program analysis, code repositories, GitHub, Node.js, Java, Scala, promises, JIT-unfriendly code, task granularity}
}
Document
Tool Insights Paper
MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper)
Abstract
In the past, many static analyses have been created in academia, but only a few of them have found widespread use in industry. Those analyses which are adopted by developers usually have IDE support in the form of plugins, without which developers have no convenient mechanism to use the analysis. Hence, the key to making static analyses more accessible to developers is to integrate the analyses into IDEs and editors. However, integrating static analyses into IDEs is non-trivial: different IDEs have different UI workflows and APIs, expertise in those matters is required to write such plugins, and analysis experts are not typically familiar with doing this. As a result, especially in academia, most analysis tools are headless and only have command-line interfaces. To make static analyses more usable, we propose MagpieBridge - a general approach to integrating static analyses into IDEs and editors. MagpieBridge reduces the mxn complexity problem of integrating m analyses into n IDEs to m+n complexity because each analysis and type of plugin need be done just once for MagpieBridge itself. We demonstrate our approach by integrating two existing analyses, Ariadne and CogniCrypt, into IDEs; these two analyses illustrate the generality of MagpieBridge, as they are based on different program analysis frameworks - WALA and Soot respectively - for different application areas - machine learning and security - and different programming languages - Python and Java. We show further generality of MagpieBridge by using multiple popular IDEs and editors, such as Eclipse, IntelliJ, PyCharm, Jupyter, Sublime Text and even Emacs and Vim.
Cite as
Linghui Luo, Julian Dolby, and Eric Bodden. MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 21:1-21:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{luo_et_al:LIPIcs.ECOOP.2019.21,
author = {Luo, Linghui and Dolby, Julian and Bodden, Eric},
title = {{MagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {21:1--21:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.21},
URN = {urn:nbn:de:0030-drops-108139},
doi = {10.4230/LIPIcs.ECOOP.2019.21},
annote = {Keywords: IDE, Tool Support, Static Analysis, Language Server Protocol}
}
Document
Experience Report
Semantic Patches for Java Program Transformation (Experience Report)
Abstract
Developing software often requires code changes that are widespread and applied to multiple locations. There are tools for Java that allow developers to specify patterns for program matching and source-to-source transformation. However, to our knowledge, none allows for transforming code based on its control-flow context. We prototype Coccinelle4J, an extension to Coccinelle, which is a program transformation tool designed for widespread changes in C code, in order to work on Java source code. We adapt Coccinelle to be able to apply scripts written in the Semantic Patch Language (SmPL), a language provided by Coccinelle, to Java source files. As a case study, we demonstrate the utility of Coccinelle4J with the task of API migration. We show 6 semantic patches to migrate from deprecated Android API methods on several open source Android projects. We describe how SmPL can be used to express several API migrations and justify several of our design decisions.
Cite as
Hong Jin Kang, Ferdian Thung, Julia Lawall, Gilles Muller, Lingxiao Jiang, and David Lo. Semantic Patches for Java Program Transformation (Experience Report). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kang_et_al:LIPIcs.ECOOP.2019.22,
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}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {22:1--22:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.22},
URN = {urn:nbn:de:0030-drops-108140},
doi = {10.4230/LIPIcs.ECOOP.2019.22},
annote = {Keywords: Program transformation, Java}
}
Document
Pearl
Minimal Session Types (Pearl)
Abstract
Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols.
Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction-passing), we prove that every process typable with standard (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types.
Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow’s results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.
Cite as
Alen Arslanagić, Jorge A. Pérez, and Erik Voogd. Minimal Session Types (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{arslanagic_et_al:LIPIcs.ECOOP.2019.23,
author = {Arslanagi\'{c}, Alen and P\'{e}rez, Jorge A. and Voogd, Erik},
title = {{Minimal Session Types}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {23:1--23:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.23},
URN = {urn:nbn:de:0030-drops-108151},
doi = {10.4230/LIPIcs.ECOOP.2019.23},
annote = {Keywords: Session types, process calculi, pi-calculus}
}
Document
Pearl
Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl)
Abstract
The Julia programming language supports multiple dispatch and provides a rich type annotation language to specify method applicability. When multiple methods are applicable for a given call, Julia relies on subtyping between method signatures to pick the correct method to invoke. Julia’s subtyping algorithm is surprisingly complex, and determining whether it is correct remains an open question. In this paper, we focus on one piece of this problem: the interaction between union types and covariant tuples. Previous work normalized unions inside tuples to disjunctive normal form. However, this strategy has two drawbacks: complex type signatures induce space explosion, and interference between normalization and other features of Julia’s type system. In this paper, we describe the algorithm that Julia uses to compute subtyping between tuples and unions - an algorithm that is immune to space explosion and plays well with other features of the language. We prove this algorithm correct and complete against a semantic-subtyping denotational model in Coq.
Cite as
Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{chung_et_al:LIPIcs.ECOOP.2019.24,
author = {Chung, Benjamin and Zappa Nardelli, Francesco and Vitek, Jan},
title = {{Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {24:1--24:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.24},
URN = {urn:nbn:de:0030-drops-108165},
doi = {10.4230/LIPIcs.ECOOP.2019.24},
annote = {Keywords: Type systems, Subtyping, Union types}
}
Document
Pearl
Finally, a Polymorphic Linear Algebra Language (Pearl)
Abstract
Many different data analytics tasks boil down to linear algebra primitives. In practice, for each different type of workload, data scientists use a particular specialised library. In this paper, we present Pilatus, a polymorphic iterative linear algebra language, applicable to various types of data analytics workloads. The design of this domain-specific language (DSL) is inspired by both mathematics and programming languages: its basic constructs are borrowed from abstract algebra, whereas the key technology behind its polymorphic design uses the tagless final approach (a.k.a. polymorphic embedding/object algebras). This design enables us to change the behaviour of arithmetic operations to express matrix algebra, graph algorithms, logical probabilistic programs, and differentiable programs. Crucially, the polymorphic design of Pilatus allows us to use multi-stage programming and rewrite-based optimisation to recover the performance of specialised code, supporting fixed sized matrices, algebraic optimisations, and fusion.
Cite as
Amir Shaikhha and Lionel Parreaux. Finally, a Polymorphic Linear Algebra Language (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 25:1-25:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{shaikhha_et_al:LIPIcs.ECOOP.2019.25,
author = {Shaikhha, Amir and Parreaux, Lionel},
title = {{Finally, a Polymorphic Linear Algebra Language}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {25:1--25:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.25},
URN = {urn:nbn:de:0030-drops-108172},
doi = {10.4230/LIPIcs.ECOOP.2019.25},
annote = {Keywords: Linear Algebra, Domain-Specific Languages, Tagless Final, Polymorphic Embedding, Object Algebra, Multi-Stage Programming, Graph Processing, Probabilistic Programming, Automatic Differentiation}
}
Document
Brave New Idea Paper
Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications (Brave New Idea Paper)
Abstract
Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This paper focuses on the specification of semantic editor services, those that use the semantic model of a program. The specification of refactorings is a common subject of study, but many other semantic editor services have received little attention. We propose a language-parametric approach to the definition of semantic editor services, using a declarative specification of the static semantics of the programming language, and constraint solving. Editor services are specified as constraint problems, and language specifications are used to ensure correctness. We describe our approach for the following semantic editor services: reference resolution, find usages, goto subclasses, code completion, and the extract definition refactoring. We do this in the context of Statix, a constraint language for the specification of type systems. We investigate the specification of editor services in terms of Statix constraints, and the requirements these impose on a suitable solver.
Cite as
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, and Eelco Visser. Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{pelsmaeker_et_al:LIPIcs.ECOOP.2019.26,
author = {Pelsmaeker, Daniel A. A. and van Antwerpen, Hendrik and Visser, Eelco},
title = {{Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.26},
URN = {urn:nbn:de:0030-drops-108182},
doi = {10.4230/LIPIcs.ECOOP.2019.26},
annote = {Keywords: semantics, constraint solving, Statix, name binding, editor services, reference resolution, code completion, refactoring}
}
Document
Brave New Idea Paper
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper)
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, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow us to explore a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the right conditions are not triggered.
As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allows 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 multiverse debugger implemented on top of the AmbientTalk operational semantics. 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
Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{torreslopez_et_al:LIPIcs.ECOOP.2019.27,
author = {Torres Lopez, Carmen and Gurdeep Singh, Robbert and Marr, Stefan and Gonzalez Boix, Elisa and Scholliers, Christophe},
title = {{Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {27:1--27:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.27},
URN = {urn:nbn:de:0030-drops-108192},
doi = {10.4230/LIPIcs.ECOOP.2019.27},
annote = {Keywords: Debugging, Parallelism, Concurrency, Actors, Formal Semantics}
}
Document
Brave New Idea Paper
Motion Session Types for Robotic Interactions (Brave New Idea Paper)
Abstract
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning.
We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time.
We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision.
We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.
Cite as
Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey. Motion Session Types for Robotic Interactions (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{majumdar_et_al:LIPIcs.ECOOP.2019.28,
author = {Majumdar, Rupak and Pirron, Marcus and Yoshida, Nobuko and Zufferey, Damien},
title = {{Motion Session Types for Robotic Interactions}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {28:1--28:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Donaldson, Alastair F.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.28},
URN = {urn:nbn:de:0030-drops-108205},
doi = {10.4230/LIPIcs.ECOOP.2019.28},
annote = {Keywords: Session Types, Robotics, Concurrent Programming, Motions, Communications, Multiparty Session Types, Deadlock Freedom}
}