DROPS

Volume

LIPIcs, Volume 109

32nd European Conference on Object-Oriented Programming (ECOOP 2018)

ECOOP 2018, July 16-21, 2018, Amsterdam, Netherlands

Editors: Todd Millstein

Document

Complete Volume

DOI: 10.4230/LIPIcs.ECOOP.2018

LIPIcs, Volume 109, ECOOP'18, Complete Volume

Authors: Todd Millstein

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.0

Front Matter, Table of Contents, Preface, Conference Organization

Authors: Todd Millstein

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.1

Fault-tolerant Distributed Reactive Programming

Authors: Ragnar Mogk, Lars Baumgärtner, Guido Salvaneschi, Bernd Freisleben, and Mira Mezini

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.2

ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions

Authors: Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.3

Theory and Practice of Coroutines with Snapshots

Authors: Aleksandar Prokopec and Fengyun Liu

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.4

A Concurrent Specification of POSIX File Systems

Authors: Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.5

A Characteristic Study of Parameterized Unit Tests in .NET Open Source Projects

Authors: Wing Lam, Siwakorn Srisakaokul, Blake Bassett, Peyman Mahdian, Tao Xie, Pratap Lakshman, and Jonathan de Halleux

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.6

Learning to Accelerate Symbolic Execution via Code Transformation

Authors: Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, and Lu Zhang

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.7

Type Regression Testing to Detect Breaking Changes in Node.js Libraries

Authors: Gianluca Mezzetti, Anders Møller, and Martin Toldam Torp

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.8

Targeted Test Generation for Actor Systems

Authors: Sihan Li, Farah Hariri, and Gul Agha

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.9

Typed First-Class Traits

Authors: Xuan Bi and Bruno C. d. S. Oliveira

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.10

CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs

Authors: Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.11

Safe Transferable Regions

Authors: Gowtham Kaki and G. Ramalingam

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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

DOI: 10.4230/LIPIcs.ECOOP.2018.12

KafKa: Gradual Typing for Objects

Authors: Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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}
}

30 Search Results for "Millstein, Todd"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message