Volume
LIPIcs, Volume 109
32nd European Conference on Object-Oriented Programming (ECOOP 2018)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
ECOOP 2018, July 16-21, 2018, Amsterdam, NetherlandsEditor
Publication Details
- published at: 2018-07-10
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-079-8
- DBLP: db/conf/ecoop/ecoop2018
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 109, ECOOP'18, Complete Volume
Abstract
LIPIcs, Volume 109, ECOOP'18, Complete Volume
Cite as
32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{millstein:LIPIcs.ECOOP.2018,
title = {{LIPIcs, Volume 109, ECOOP'18, Complete Volume}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018},
URN = {urn:nbn:de:0030-drops-93014},
doi = {10.4230/LIPIcs.ECOOP.2018},
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
32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{millstein:LIPIcs.ECOOP.2018.0,
author = {Millstein, Todd},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {0:i--0:xx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.0},
URN = {urn:nbn:de:0030-drops-92054},
doi = {10.4230/LIPIcs.ECOOP.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Fault-tolerant Distributed Reactive Programming
Abstract
In this paper, we present a holistic approach to provide fault tolerance for distributed reactive programming. Our solution automatically stores and recovers program state to handle crashes, automatically updates and shares distributed parts of the state to provide eventual consistency, and handles errors in a fine-grained manner to allow precise manual control when necessary. By making use of the reactive programming paradigm, we provide these mechanisms without changing the behavior of existing programs and with reasonable performance, as indicated by our experimental evaluation.
Cite as
Ragnar Mogk, Lars Baumgärtner, Guido Salvaneschi, Bernd Freisleben, and Mira Mezini. Fault-tolerant Distributed Reactive Programming. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{mogk_et_al:LIPIcs.ECOOP.2018.1,
author = {Mogk, Ragnar and Baumg\"{a}rtner, Lars and Salvaneschi, Guido and Freisleben, Bernd and Mezini, Mira},
title = {{Fault-tolerant Distributed Reactive Programming}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {1:1--1:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.1},
URN = {urn:nbn:de:0030-drops-92064},
doi = {10.4230/LIPIcs.ECOOP.2018.1},
annote = {Keywords: reactive programming, distributed systems, CRDTs, snapshots, restoration, error handling, fault tolerance}
}
Document
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions
Abstract
Context-aware applications, whose behavior reactively depends on the time-varying status of the surrounding environment - such as network connection, battery level, and sensors - are getting more and more pervasive and important. The term "context-awareness" usually suggests prompt reactions to context changes: as the context change signals that the current execution cannot be continued, the application should immediately abort its execution, possibly does some clean-up tasks, and suspend until the context allows it to restart. Interruptions, or asynchronous exceptions, are useful to achieve context-awareness. It is, however, difficult to program with interruptions in a compositional way in most programming languages because their support is too primitive, relying on synchronous exception handling mechanism such as try-catch.
We propose a new domain-specific language ContextWorkflow for interruptible programs as a solution to the problem. A basic unit of an interruptible program is a workflow, i.e., a sequence of atomic computations accompanied with compensation actions. The uniqueness of ContextWorkflow is that, during its execution, a workflow keeps watching the context between atomic actions and decides if the computation should be continued, aborted, or suspended. Our contribution of this paper is as follows; (1) the design of a workflow-like language with asynchronous interruption, checkpointing, sub-workflows and suspension; (2) a formal semantics of the core language; (3) a monadic interpreter corresponding to the semantics; and (4) its concrete implementation as an embedded domain-specific language in Scala.
Cite as
Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 2:1-2:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{inoue_et_al:LIPIcs.ECOOP.2018.2,
author = {Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
title = {{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {2:1--2:33},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.2},
URN = {urn:nbn:de:0030-drops-92074},
doi = {10.4230/LIPIcs.ECOOP.2018.2},
annote = {Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
Document
Theory and Practice of Coroutines with Snapshots
Abstract
While event-driven programming is a widespread model for asynchronous computing, its inherent control flow fragmentation makes event-driven programs notoriously difficult to understand and maintain. Coroutines are a general control flow construct that can eliminate control flow fragmentation. However, coroutines are still missing in many popular languages. This gap is partly caused by the difficulties of supporting suspendable computations in the language runtime.
We introduce first-class, type-safe, stackful coroutines with snapshots, which unify many variants of suspendable computing. Our design relies solely on the static metaprogramming support of the host language, without modifying the language implementation or the runtime. We also develop a formal model for type-safe, stackful and delimited coroutines, and we prove the respective safety properties. We show that the model is sufficiently general to express iterators, single-assignment variables, async-await, actors, event streams, backtracking, symmetric coroutines and continuations. Performance evaluations reveal that the proposed metaprogramming-based approach has a decent performance, with workload-dependent overheads of 1.03-2.11 x compared to equivalent manually written code, and improvements of up to 6 x compared to other approaches.
Cite as
Aleksandar Prokopec and Fengyun Liu. Theory and Practice of Coroutines with Snapshots. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 3:1-3:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{prokopec_et_al:LIPIcs.ECOOP.2018.3,
author = {Prokopec, Aleksandar and Liu, Fengyun},
title = {{Theory and Practice of Coroutines with Snapshots}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {3:1--3:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.3},
URN = {urn:nbn:de:0030-drops-92087},
doi = {10.4230/LIPIcs.ECOOP.2018.3},
annote = {Keywords: coroutines, continuations, coroutine snapshots, asynchronous programming, inversion of control, event-driven programming}
}
Document
A Concurrent Specification of POSIX File Systems
Abstract
POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files.
Cite as
Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. A Concurrent Specification of POSIX File Systems. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ntzik_et_al:LIPIcs.ECOOP.2018.4,
author = {Ntzik, Gian and da Rocha Pinto, Pedro and Sutherland, Julian and Gardner, Philippa},
title = {{A Concurrent Specification of POSIX File Systems}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {4:1--4:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.4},
URN = {urn:nbn:de:0030-drops-92092},
doi = {10.4230/LIPIcs.ECOOP.2018.4},
annote = {Keywords: POSIX, concurrency, file systems, refinement, separation logic, atomicity}
}
Document
A Characteristic Study of Parameterized Unit Tests in .NET Open Source Projects
Abstract
In the past decade, parameterized unit testing has emerged as a promising method to specify program behaviors under test in the form of unit tests. Developers can write parameterized unit tests (PUTs), unit-test methods with parameters, in contrast to conventional unit tests, without parameters. The use of PUTs can enable powerful test generation tools such as Pex to have strong test oracles to check against, beyond just uncaught runtime exceptions. In addition, PUTs have been popularly supported by various unit testing frameworks for .NET and the JUnit framework for Java. However, there exists no study to offer insights on how PUTs are written by developers in either proprietary or open source development practices, posing barriers for various stakeholders to bring PUTs to widely adopted practices in software industry. To fill this gap, we first present categorization results of the Microsoft MSDN Pex Forum posts (contributed primarily by industrial practitioners) related to PUTs. We then use the categorization results to guide the design of the first characteristic study of PUTs in .NET open source projects. We study hundreds of PUTs that open source developers wrote for these open source projects. Our study findings provide valuable insights for various stakeholders such as current or prospective PUT writers (e.g., developers), PUT framework designers, test-generation tool vendors, testing researchers, and testing educators.
Cite as
Wing Lam, Siwakorn Srisakaokul, Blake Bassett, Peyman Mahdian, Tao Xie, Pratap Lakshman, and Jonathan de Halleux. A Characteristic Study of Parameterized Unit Tests in .NET Open Source Projects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 5:1-5:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{lam_et_al:LIPIcs.ECOOP.2018.5,
author = {Lam, Wing and Srisakaokul, Siwakorn and Bassett, Blake and Mahdian, Peyman and Xie, Tao and Lakshman, Pratap and de Halleux, Jonathan},
title = {{A Characteristic Study of Parameterized Unit Tests in .NET Open Source Projects}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {5:1--5:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.5},
URN = {urn:nbn:de:0030-drops-92105},
doi = {10.4230/LIPIcs.ECOOP.2018.5},
annote = {Keywords: Parameterized unit testing, automated test generation, unit testing}
}
Document
Learning to Accelerate Symbolic Execution via Code Transformation
Abstract
Symbolic execution is an effective but expensive technique for automated test generation. Over the years, a large number of refined symbolic execution techniques have been proposed to improve its efficiency. However, the symbolic execution efficiency problem remains, and largely limits the application of symbolic execution in practice. Orthogonal to refined symbolic execution, in this paper we propose to accelerate symbolic execution through semantic-preserving code transformation on the target programs. During the initial stage of this direction, we adopt a particular code transformation, compiler optimization, which is initially proposed to accelerate program concrete execution by transforming the source program into another semantic-preserving target program with increased efficiency (e.g., faster or smaller). However, compiler optimizations are mostly designed to accelerate program concrete execution rather than symbolic execution. Recent work also reported that unified settings on compiler optimizations that can accelerate symbolic execution for any program do not exist at all. Therefore, in this work we propose a machine-learning based approach to tuning compiler optimizations to accelerate symbolic execution, whose results may also aid further design of specific code transformations for symbolic execution. In particular, the proposed approach LEO separates source-code functions and libraries through our program-splitter, and predicts individual compiler optimization (i.e., whether a type of code transformation is chosen) separately through analyzing the performance of existing symbolic execution. Finally, LEO applies symbolic execution on the code transformed by compiler optimization (through our local-optimizer). We conduct an empirical study on GNU Coreutils programs using the KLEE symbolic execution engine. The results show that LEO significantly accelerates symbolic execution, outperforming the default KLEE configurations (i.e., turning on/off all compiler optimizations) in various settings, e.g., with the default training/testing time, LEO achieves the highest line coverage in 50/68 programs, and its average improvement rate on all programs is 46.48%/88.92% in terms of line coverage compared with turning on/off all compiler optimizations.
Cite as
Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, and Lu Zhang. Learning to Accelerate Symbolic Execution via Code Transformation. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.ECOOP.2018.6,
author = {Chen, Junjie and Hu, Wenxiang and Zhang, Lingming and Hao, Dan and Khurshid, Sarfraz and Zhang, Lu},
title = {{Learning to Accelerate Symbolic Execution via Code Transformation}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {6:1--6:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.6},
URN = {urn:nbn:de:0030-drops-92115},
doi = {10.4230/LIPIcs.ECOOP.2018.6},
annote = {Keywords: Symbolic Execution, Code Transformation, Machine Learning}
}
Document
Type Regression Testing to Detect Breaking Changes in Node.js Libraries
Abstract
The npm repository contains JavaScript libraries that are used by millions of software developers. Its semantic versioning system relies on the ability to distinguish between breaking and non-breaking changes when libraries are updated. However, the dynamic nature of JavaScript often causes unintended breaking changes to be detected too late, which undermines the robustness of the applications.
We present a novel technique, type regression testing, to automatically determine whether an update of a library implementation affects the types of its public interface, according to how the library is being used by other npm packages. By leveraging available test suites of clients, type regression testing uses a dynamic analysis to learn models of the library interface. Comparing the models before and after an update effectively amplifies the existing tests by revealing changes that may affect the clients.
Experimental results on 12 widely used libraries show that the technique can identify type-related breaking changes with high accuracy. It fully automatically classifies at least 90% of the updates correctly as either major or as minor or patch, and it detects 26 breaking changes among the minor and patch updates.
Cite as
Gianluca Mezzetti, Anders Møller, and Martin Toldam Torp. Type Regression Testing to Detect Breaking Changes in Node.js Libraries. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{mezzetti_et_al:LIPIcs.ECOOP.2018.7,
author = {Mezzetti, Gianluca and M{\o}ller, Anders and Torp, Martin Toldam},
title = {{Type Regression Testing to Detect Breaking Changes in Node.js Libraries}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {7:1--7:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.7},
URN = {urn:nbn:de:0030-drops-92128},
doi = {10.4230/LIPIcs.ECOOP.2018.7},
annote = {Keywords: JavaScript, semantic versioning, dynamic analysis}
}
Document
Targeted Test Generation for Actor Systems
Abstract
This paper addresses the problem of targeted test generation for actor systems. Specifically, we propose a method to support generation of system-level tests to cover a given code location in an actor system. The test generation method consists of two phases. First, static analysis is used to construct an abstraction of an entire actor system in terms of a message flow graph (MFG). An MFG captures potential actor interactions that are defined in a program. Second, a backwards symbolic execution (BSE) from a target location to an "entry point" of the actor system is performed. BSE uses the MFG constructed in the first phase of our targeted test generation method to guide execution across actors. Because concurrency leads to a huge search space which can potentially be explored through BSE, we prune the search space by using two heuristics combined with a feedback-directed technique. We implement our method in Tap, a tool for Java Akka programs, and evaluate Tap on the Savina benchmarks as well as four open source projects. Our evaluation shows that the Tap achieves a relatively high target coverage (78% on 1,000 targets) and detects six previously unreported bugs in the subjects.
Cite as
Sihan Li, Farah Hariri, and Gul Agha. Targeted Test Generation for Actor Systems. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 8:1-8:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{li_et_al:LIPIcs.ECOOP.2018.8,
author = {Li, Sihan and Hariri, Farah and Agha, Gul},
title = {{Targeted Test Generation for Actor Systems}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {8:1--8:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.8},
URN = {urn:nbn:de:0030-drops-92135},
doi = {10.4230/LIPIcs.ECOOP.2018.8},
annote = {Keywords: actors, symbolic execution, test generation, static analysis}
}
Document
Typed First-Class Traits
Abstract
Many dynamically-typed languages (including JavaScript, Ruby, Python or Racket) support first-class classes, or related concepts such as first-class traits and/or mixins. In those languages classes are first-class values and, like any other values, they can be passed as an argument, or returned from a function. Furthermore first-class classes support dynamic inheritance: i.e. they can inherit from other classes at runtime, enabling programmers to abstract over the inheritance hierarchy. In contrast, type system limitations prevent most statically-typed languages from having first-class classes and dynamic inheritance.
This paper shows the design of SEDEL: a polymorphic statically-typed language with first-class traits, supporting dynamic inheritance as well as conventional OO features such as dynamic dispatching and abstract methods. To address the challenges of type-checking first-class traits, SEDEL employs a type system based on the recent work on disjoint intersection types and disjoint polymorphism. The novelty of SEDEL over core disjoint intersection calculi are source level features for practical OO programming, including first-class traits with dynamic inheritance, dynamic dispatching and abstract methods. Inspired by Cook and Palsberg's work on the denotational semantics for inheritance, we show how to design a source language that can be elaborated into Alpuim et al.'s F_{i} (a core polymorphic calculus with records supporting disjoint polymorphism). We illustrate the applicability of SEDEL with several example uses for first-class traits, and a case study that modularizes programming language interpreters using a highly modular form of visitors.
Cite as
Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 9:1-9:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bi_et_al:LIPIcs.ECOOP.2018.9,
author = {Bi, Xuan and Oliveira, Bruno C. d. S.},
title = {{Typed First-Class Traits}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {9:1--9:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.9},
URN = {urn:nbn:de:0030-drops-92145},
doi = {10.4230/LIPIcs.ECOOP.2018.9},
annote = {Keywords: traits, extensible designs}
}
Document
CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs
Abstract
Various studies have empirically shown that the majority of Java and Android apps misuse cryptographic libraries, causing devastating breaches of data security. It is crucial to detect such misuses early in the development process. To detect cryptography misuses, one must first define secure uses, a process mastered primarily by cryptography experts, and not by developers.
In this paper, we present CrySL, a definition language for bridging the cognitive gap between cryptography experts and developers. CrySL enables cryptography experts to specify the secure usage of the cryptographic libraries that they provide. We have implemented a compiler that translates such CrySL specification into a context-sensitive and flow-sensitive demand-driven static analysis. The analysis then helps developers by automatically checking a given Java or Android app for compliance with the CrySL-encoded rules.
We have designed an extensive CrySL rule set for the Java Cryptography Architecture (JCA), and empirically evaluated it by analyzing 10,000 current Android apps. Our results show that misuse of cryptographic APIs is still widespread, with 95% of apps containing at least one misuse. Our easily extensible CrySL rule set covers more violations than previous special-purpose tools with hard-coded rules, with our tooling offering a more precise analysis.
Cite as
Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kruger_et_al:LIPIcs.ECOOP.2018.10,
author = {Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira},
title = {{CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {10:1--10:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.10},
URN = {urn:nbn:de:0030-drops-92151},
doi = {10.4230/LIPIcs.ECOOP.2018.10},
annote = {Keywords: cryptography, domain-specific language, static analysis}
}
Document
Safe Transferable Regions
Abstract
There is an increasing interest in alternative memory management schemes that seek to combine the convenience of garbage collection and the performance of manual memory management in a single language framework. Unfortunately, ensuring safety in presence of manual memory management remains as great a challenge as ever. In this paper, we present a C#-like object-oriented language called Broom that uses a combination of region type system and lightweight runtime checks to enforce safety in presence of user-managed memory regions called transferable regions. Unsafe transferable regions have been previously used to contain the latency due to unbounded GC pauses. Our approach shows that it is possible to restore safety without compromising on the benefits of transferable regions. We prove the type safety of Broom in a formal framework that includes its C#-inspired features, such as higher-order functions and generics. We complement our type system with a type inference algorithm, which eliminates the need for programmers to write region annotations on types. The inference algorithm has been proven sound and relatively complete. We describe a prototype implementation of the inference algorithm, and our experience of using it to enforce memory safety in dataflow programs.
Cite as
Gowtham Kaki and G. Ramalingam. Safe Transferable Regions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 11:1-11:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kaki_et_al:LIPIcs.ECOOP.2018.11,
author = {Kaki, Gowtham and Ramalingam, G.},
title = {{Safe Transferable Regions}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {11:1--11:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.11},
URN = {urn:nbn:de:0030-drops-92160},
doi = {10.4230/LIPIcs.ECOOP.2018.11},
annote = {Keywords: Memory Safety, Formal Methods, Type System, Type Inference, Regions, Featherweight Java}
}
Document
KafKa: Gradual Typing for Objects
Abstract
A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems embody fundamentally different ideas of what it means to be well-typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. We present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.
Cite as
Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chung_et_al:LIPIcs.ECOOP.2018.12,
author = {Chung, Benjamin and Li, Paley and Zappa Nardelli, Francesco and Vitek, Jan},
title = {{KafKa: Gradual Typing for Objects}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {12:1--12:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.12},
URN = {urn:nbn:de:0030-drops-92170},
doi = {10.4230/LIPIcs.ECOOP.2018.12},
annote = {Keywords: Gradual typing, object-orientation, language design, type systems}
}
Document
Dependent Types for Class-based Mutable Objects
Abstract
We present an imperative object-oriented language featuring a dependent type system designed to support class-based programming and inheritance. Programmers implement classes in the usual imperative style, and may take advantage of a richer dependent type system to express class invariants and restrictions on how objects are allowed to change and be used as arguments to methods. By way of example, we implement insertion and deletion for binary search trees in an imperative style, and come up with types that ensure the binary search tree invariant. This is the first dependently-typed language with mutable objects that we know of to bring classes and index refinements into play, enabling types (classes) to be refined by indices drawn from some constraint domain. We give a declarative type system that supports objects whose types may change, despite being sound. We also give an algorithmic type system that provides a precise account of quantifier instantiation in a bidirectional style, and from which it is straightforward to read off an implementation. Moreover, all the examples in the paper have been run, compiled and executed in a fully functional prototype that includes a plugin for the Eclipse IDE.
Cite as
Joana Campos and Vasco T. Vasconcelos. Dependent Types for Class-based Mutable Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 13:1-13:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{campos_et_al:LIPIcs.ECOOP.2018.13,
author = {Campos, Joana and Vasconcelos, Vasco T.},
title = {{Dependent Types for Class-based Mutable Objects}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {13:1--13:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.13},
URN = {urn:nbn:de:0030-drops-92182},
doi = {10.4230/LIPIcs.ECOOP.2018.13},
annote = {Keywords: dependent types, index refinements, mutable objects, type systems}
}
Document
Static Typing of Complex Presence Constraints in Interfaces
Abstract
Many functions in libraries and APIs have the notion of optional parameters, which can be mapped onto optional properties of an object representing those parameters. The fact that properties are optional opens up the possibility for APIs and libraries to design a complex "dependency logic" between properties: for example, some properties may be mutually exclusive, some properties may depend on others, etc. Existing type systems are not strong enough to express such dependency logic, which can lead to the creation of invalid objects and accidental usage of absent properties. In this paper we propose TypeScriptIPC: a variant of TypeScript with a novel type system that enables programmers to express complex presence constraints on properties. We prove that it is sound with respect to enforcing complex dependency logic defined by the programmer when an object is created, modified or accessed.
Cite as
Nathalie Oostvogels, Joeri De Koster, and Wolfgang De Meuter. Static Typing of Complex Presence Constraints in Interfaces. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 14:1-14:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{oostvogels_et_al:LIPIcs.ECOOP.2018.14,
author = {Oostvogels, Nathalie and De Koster, Joeri and De Meuter, Wolfgang},
title = {{Static Typing of Complex Presence Constraints in Interfaces}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {14:1--14:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.14},
URN = {urn:nbn:de:0030-drops-92196},
doi = {10.4230/LIPIcs.ECOOP.2018.14},
annote = {Keywords: type checking, interfaces, dependency logic}
}
Document
Mailbox Types for Unordered Interactions
Abstract
We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.
Cite as
Ugo de'Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{deliguoro_et_al:LIPIcs.ECOOP.2018.15,
author = {de'Liguoro, Ugo and Padovani, Luca},
title = {{Mailbox Types for Unordered Interactions}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {15:1--15:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.15},
URN = {urn:nbn:de:0030-drops-92209},
doi = {10.4230/LIPIcs.ECOOP.2018.15},
annote = {Keywords: actors, concurrent objects, first-class mailboxes, unordered communication protocols, behavioral types, protocol conformance, deadlock freedom, junk freedom}
}
Document
Accelerating Dynamically-Typed Languages on Heterogeneous Platforms Using Guards Optimization
Abstract
Scientific applications are ideal candidates for the "heterogeneous computing" paradigm, in which parts of a computation are "offloaded" to available accelerator hardware such as GPUs. However, when such applications are written in dynamic languages such as Python or R, as they increasingly are, things become less straightforward. The same flexibility that makes these languages so appealing to programmers also significantly complicates the problem of automatically and transparently partitioning a program's execution between a CPU and available accelerator hardware without having to rely on programmer annotations.
A common way of handling the features of dynamic languages is by introducing speculation in conjunction with guards to ascertain the validity of assumptions made in the speculative computation. Unfortunately, a single guard violation during the execution of "offloaded" code may result in a huge performance penalty and necessitate the complete re-execution of the offloaded computation. In the case of dynamic languages, this problem is compounded by the fact that a full compiler analysis is not always possible ahead of time.
This paper presents MegaGuards, a new approach for speculatively executing dynamic languages on heterogeneous platforms in a fully automatic and transparent manner. Our method translates each target loop into a single static region devoid of any dynamic type features. The dynamic parts are instead handled by a construct that we call a mega guard which checks all the speculative assumptions ahead of its corresponding static region. Notably, the advantage of MegaGuards is not limited to heterogeneous computing; because it removes guards from compute-intensive loops, the approach also improves sequential performance.
We have implemented MegaGuards along with an automatic loop parallelization backend in ZipPy, a Python Virtual Machine. The results of a careful and detailed evaluation reveal very significant speedups of an order of magnitude on average with a maximum speedup of up to two orders of magnitudes when compared to the original ZipPy performance as a baseline. These results demonstrate the potential for applying heterogeneous computing to dynamic languages.
Cite as
Mohaned Qunaibit, Stefan Brunthaler, Yeoul Na, Stijn Volckaert, and Michael Franz. Accelerating Dynamically-Typed Languages on Heterogeneous Platforms Using Guards Optimization. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{qunaibit_et_al:LIPIcs.ECOOP.2018.16,
author = {Qunaibit, Mohaned and Brunthaler, Stefan and Na, Yeoul and Volckaert, Stijn and Franz, Michael},
title = {{Accelerating Dynamically-Typed Languages on Heterogeneous Platforms Using Guards Optimization}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {16:1--16:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.16},
URN = {urn:nbn:de:0030-drops-92217},
doi = {10.4230/LIPIcs.ECOOP.2018.16},
annote = {Keywords: Type Specialization, Guards Optimization, Automatic Heterogeneous Computing, Automatic Parallelism}
}
Document
CROCHET: Checkpoint and Rollback via Lightweight Heap Traversal on Stock JVMs
Abstract
Checkpoint/rollback (CR) mechanisms create snapshots of the state of a running application, allowing it to later be restored to that checkpointed snapshot. Support for checkpoint/rollback enables many program analyses and software engineering techniques, including test generation, fault tolerance, and speculative execution.
Fully automatic CR support is built into some modern operating systems. However, such systems perform checkpoints at the coarse granularity of whole pages of virtual memory, which imposes relatively high overhead to incrementally capture the changing state of a process, and makes it difficult for applications to checkpoint only some logical portions of their state. CR systems implemented at the application level and with a finer granularity typically require complex developer support to identify: (1) where checkpoints can take place, and (2) which program state needs to be copied. A popular compromise is to implement CR support in managed runtime environments, e.g. the Java Virtual Machine (JVM), but this typically requires specialized, non-standard runtime environments, limiting portability and adoption of this approach.
In this paper, we present a novel approach for Checkpoint ROllbaCk via lightweight HEap Traversal (Crochet), which enables fully automatic fine-grained lightweight checkpoints within unmodified commodity JVMs (specifically Oracle's HotSpot and OpenJDK). Leveraging key insights about the internal design common to modern JVMs, Crochet works entirely through bytecode rewriting and standard debug APIs, utilizing special proxy objects to perform a lazy heap traversal that starts at the root references and traverses the heap as objects are accessed, copying or restoring state as needed and removing each proxy immediately after it is used. We evaluated Crochet on the DaCapo benchmark suite, finding it to have very low runtime overhead in steady state (ranging from no overhead to 1.29x slowdown), and that it often outperforms a state-of-the-art system-level checkpoint tool when creating large checkpoints.
Cite as
Jonathan Bell and Luís Pina. CROCHET: Checkpoint and Rollback via Lightweight Heap Traversal on Stock JVMs. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 17:1-17:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bell_et_al:LIPIcs.ECOOP.2018.17,
author = {Bell, Jonathan and Pina, Lu{\'\i}s},
title = {{CROCHET: Checkpoint and Rollback via Lightweight Heap Traversal on Stock JVMs}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {17:1--17:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.17},
URN = {urn:nbn:de:0030-drops-92223},
doi = {10.4230/LIPIcs.ECOOP.2018.17},
annote = {Keywords: Checkpoint rollback, runtime systems, dynamic analysis}
}
Document
ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications
Abstract
The Internet of Things (IoT) has gained wide popularity both in academic and industrial contexts. As IoT devices become increasingly powerful, they can run more and more complex applications written in higher-level languages, such as JavaScript. However, by their nature, IoT devices are subject to resource constraints, which require applications to be dynamically migrated between devices (and the cloud). Further, IoT applications are also becoming more stateful, and hence we need to save their state during migration transparently to the programmer.
In this paper, we present ThingsMigrate, a middleware providing VM-independent migration of stateful JavaScript applications across IoT devices. ThingsMigrate captures and reconstructs the internal JavaScript program state by instrumenting application code before run time, without modifying the underlying Virtual Machine (VM), thus providing platform and VM-independence. We evaluated ThingsMigrate against standard benchmarks, and over two IoT platforms and a cloud-like environment. We show that it can successfully migrate even highly CPU-intensive applications, with acceptable overheads (about 30%), and supports multiple migrations.
Cite as
Julien Gascon-Samson, Kumseok Jung, Shivanshu Goyal, Armin Rezaiean-Asel, and Karthik Pattabiraman. ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 18:1-18:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gasconsamson_et_al:LIPIcs.ECOOP.2018.18,
author = {Gascon-Samson, Julien and Jung, Kumseok and Goyal, Shivanshu and Rezaiean-Asel, Armin and Pattabiraman, Karthik},
title = {{ThingsMigrate: Platform-Independent Migration of Stateful JavaScript IoT Applications}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {18:1--18:33},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.18},
URN = {urn:nbn:de:0030-drops-92236},
doi = {10.4230/LIPIcs.ECOOP.2018.18},
annote = {Keywords: JavaScript, Code Migration, Closures, IoT, Node.js}
}
Document
Automating Object Transformations for Dynamic Software Updating via Online Execution Synthesis
Abstract
Dynamic software updating (DSU) is a technique to upgrade a running software system on the fly without stopping the system. During updating, the runtime state of the modified components of the system needs to be properly transformed into a new state, so that the modified components can still correctly interact with the rest of the system. However, the transformation is non-trivial to realize due to the gap between the low-level implementations of two versions of a program. This paper presents AOTES, a novel approach to automating object transformations for dynamic updating of Java programs. AOTES bridges the gap by abstracting the old state of an object to a history of method invocations, and re-invoking the new version of all methods in the history to get the desired new state. AOTES requires no instrumentation to record any data and thus has no overhead during normal execution. We propose and implement a novel technique that can synthesize an equivalent history of method invocations based on the current object state only. We evaluated AOTES on software updates taken from Apache Commons Collections, Tomcat, FTP Server and SSHD Server. Experimental results show that AOTES successfully handled 51 of 61 object transformations of 21 updated classes, while two state-of-the-art approaches only handled 11 and 6 of 61, respectively.
Cite as
Tianxiao Gu, Xiaoxing Ma, Chang Xu, Yanyan Jiang, Chun Cao, and Jian Lu. Automating Object Transformations for Dynamic Software Updating via Online Execution Synthesis. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 19:1-19:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gu_et_al:LIPIcs.ECOOP.2018.19,
author = {Gu, Tianxiao and Ma, Xiaoxing and Xu, Chang and Jiang, Yanyan and Cao, Chun and Lu, Jian},
title = {{Automating Object Transformations for Dynamic Software Updating via Online Execution Synthesis}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {19:1--19:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.19},
URN = {urn:nbn:de:0030-drops-92243},
doi = {10.4230/LIPIcs.ECOOP.2018.19},
annote = {Keywords: Dynamic Software Update, Program Synthesis, Execution Synthesis}
}
Document
FHJ: A Formal Model for Hierarchical Dispatching and Overriding
Abstract
Multiple inheritance is a valuable feature for Object-Oriented Programming. However, it is also tricky to get right, as illustrated by the extensive literature on the topic. A key issue is the ambiguity arising from inheriting multiple parents, which can have conflicting methods. Numerous existing work provides solutions for conflicts which arise from diamond inheritance: i.e. conflicts that arise from implementations sharing a common ancestor. However, most mechanisms are inadequate to deal with unintentional method conflicts: conflicts which arise from two unrelated methods that happen to share the same name and signature.
This paper presents a new model called Featherweight Hierarchical Java (FHJ) that deals with unintentional method conflicts. In our new model, which is partly inspired by C++, conflicting methods arising from unrelated methods can coexist in the same class, and hierarchical dispatching supports unambiguous lookups in the presence of such conflicting methods. To avoid ambiguity, hierarchical information is employed in method dispatching, which uses a combination of static and dynamic type information to choose the implementation of a method at run-time. Furthermore, unlike all existing inheritance models, our model supports hierarchical method overriding: that is, methods can be independently overridden along the multiple inheritance hierarchy. We give illustrative examples of our language and features and formalize FHJ as a minimal Featherweight-Java style calculus.
Cite as
Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto. FHJ: A Formal Model for Hierarchical Dispatching and Overriding. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.ECOOP.2018.20,
author = {Wang, Yanlin and Zhang, Haoyuan and Oliveira, Bruno C. d. S. and Servetto, Marco},
title = {{FHJ: A Formal Model for Hierarchical Dispatching and Overriding}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {20:1--20:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.20},
URN = {urn:nbn:de:0030-drops-92259},
doi = {10.4230/LIPIcs.ECOOP.2018.20},
annote = {Keywords: multiple inheritance, hierarchical dispatching, OOP, language design}
}
Document
Modeling Infinite Behaviour by Corules
Abstract
Generalized inference systems have been recently introduced, and used, among other applications, to define semantic judgments which uniformly model terminating computations and divergence. We show that the approach can be successfully extended to more sophisticated notions of infinite behaviour, that is, to express that a diverging computation produces some possibly infinite result. This also provides a motivation to smoothly extend the theory of generalized inference systems to include, besides coaxioms, also corules, a more general notion for which significant examples were missing until now. We first illustrate the approach on a lambda-calculus with output effects, for which we also provide an alternative semantics based on standard notions, and a complete proof of the equivalence of the two semantics. Then, we consider a more involved example, that is, an imperative Java-like language with I/O primitives.
Cite as
Davide Ancona, Francesco Dagnino, and Elena Zucca. Modeling Infinite Behaviour by Corules. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ancona_et_al:LIPIcs.ECOOP.2018.21,
author = {Ancona, Davide and Dagnino, Francesco and Zucca, Elena},
title = {{Modeling Infinite Behaviour by Corules}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {21:1--21:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.21},
URN = {urn:nbn:de:0030-drops-92267},
doi = {10.4230/LIPIcs.ECOOP.2018.21},
annote = {Keywords: Operational semantics, coinduction, trace semantics}
}
Document
The Essence of Nested Composition
Abstract
Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition, which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce's work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalized in Coq, and we have an implementation of our calculus.
Cite as
Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 22:1-22:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bi_et_al:LIPIcs.ECOOP.2018.22,
author = {Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
title = {{The Essence of Nested Composition}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {22:1--22:33},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.22},
URN = {urn:nbn:de:0030-drops-92275},
doi = {10.4230/LIPIcs.ECOOP.2018.22},
annote = {Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Document
Defensive Points-To Analysis: Effective Soundness via Laziness
Abstract
We present a defensive may-point-to analysis approach, which offers soundness even in the presence of arbitrary opaque code: all non-empty points-to sets computed are guaranteed to be over-approximations of the sets of values arising at run time. A key design tenet of the analysis is laziness: the analysis computes points-to relationships only for variables or objects that are guaranteed to never escape into opaque code. This means that the analysis misses some valid inferences, yet it also never wastes work to compute sets of values that are not "complete", i.e., that may be missing elements due to opaque code. Laziness enables great efficiency, allowing a highly precise points-to analysis (such as a 5-call-site-sensitive, flow-sensitive analysis).
Despite its conservative nature, our analysis yields sound, actionable results for a large subset of the program code, achieving (under worst-case assumptions) 34-74% of the program coverage of an unsound state-of-the-art analysis for real-world programs.
Cite as
Yannis Smaragdakis and George Kastrinis. Defensive Points-To Analysis: Effective Soundness via Laziness. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{smaragdakis_et_al:LIPIcs.ECOOP.2018.23,
author = {Smaragdakis, Yannis and Kastrinis, George},
title = {{Defensive Points-To Analysis: Effective Soundness via Laziness}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {23:1--23:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.23},
URN = {urn:nbn:de:0030-drops-92287},
doi = {10.4230/LIPIcs.ECOOP.2018.23},
annote = {Keywords: static analysis, soundness, defensive analysis}
}
Document
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates
Abstract
Modern software increasingly relies on external resources whose location or content can change during program execution. Examples of such resources include remote network hosts, database entries, dynamically updated configuration options, etc. Long running, adaptable programs must handle these changes gracefully and correctly. Dealing with all possible resource update scenarios is difficult to get right, especially if, as is common, external resources can be modified without prior warning by code and/or users outside of the application's direct control. If a resource unexpectedly changes during a computation, an application may observe multiple, inconsistent states of the resource, leading to incorrect program behavior.
This paper presents a sound and precise static analysis, Legato, that verifies programs correctly handle changes in external resources. Our analysis ensures that every value computed by an application reflects a single, consistent version of every external resource's state. Although consistent computation in the presence of concurrent resource updates is fundamentally a concurrency issue, our analysis relies on the novel at-most-once condition to avoid explicitly reasoning about concurrency. The at-most-once condition requires that all values depend on at most one access of each resource. Our analysis is flow-, field-, and context-sensitive. It scales to real-world Java programs while producing a moderate number of false positives. We applied Legato to 10 applications with dynamically updated configurations, and found several non-trivial consistency bugs.
Cite as
John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 24:1-24:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{toman_et_al:LIPIcs.ECOOP.2018.24,
author = {Toman, John and Grossman, Dan},
title = {{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {24:1--24:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.24},
URN = {urn:nbn:de:0030-drops-92290},
doi = {10.4230/LIPIcs.ECOOP.2018.24},
annote = {Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
Definite Reference Mutability
Abstract
Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable reference may be mutable due to approximation.
In this paper, we present ReM (for definite Re[ference] M[utability]). It separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all mutable references are definitely mutable.
Cite as
Ana Milanova. Definite Reference Mutability. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 25:1-25:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{milanova:LIPIcs.ECOOP.2018.25,
author = {Milanova, Ana},
title = {{Definite Reference Mutability}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {25:1--25:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.25},
URN = {urn:nbn:de:0030-drops-92303},
doi = {10.4230/LIPIcs.ECOOP.2018.25},
annote = {Keywords: reference immutability, type inference, CFL-reachability, precision}
}
Document
Efficient Reflection String Analysis via Graph Coloring
Abstract
Static analyses for reflection and other dynamic language features have recently increased in number and advanced in sophistication. Most such analyses rely on a whole-program model of the flow of strings, through the stack and heap. We show that this global modeling of strings remains a major bottleneck of static analyses and propose a compact encoding, in order to battle unnecessary complexity. In our encoding, strings are maximally merged if they can never serve to differentiate class members in reflection operations. We formulate the problem as an instance of graph coloring and propose a fast polynomial-time algorithm that exploits the unique features of the setting (esp. large cliques, leading to hundreds of colors for realistic programs). The encoding is applied to two different frameworks for string-guided Java reflection analysis from past literature and leads to significant optimization (e.g., a ~2x reduction in the number of string-flow inferences), for a whole-program points-to analysis that uses strings.
Cite as
Neville Grech, George Kastrinis, and Yannis Smaragdakis. Efficient Reflection String Analysis via Graph Coloring. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 26:1-26:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{grech_et_al:LIPIcs.ECOOP.2018.26,
author = {Grech, Neville and Kastrinis, George and Smaragdakis, Yannis},
title = {{Efficient Reflection String Analysis via Graph Coloring}},
booktitle = {32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
pages = {26:1--26:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-079-8},
ISSN = {1868-8969},
year = {2018},
volume = {109},
editor = {Millstein, Todd},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.26},
URN = {urn:nbn:de:0030-drops-92319},
doi = {10.4230/LIPIcs.ECOOP.2018.26},
annote = {Keywords: reflection, static analysis, graph coloring}
}