Volume
LIPIcs, Volume 74
31st European Conference on Object-Oriented Programming (ECOOP 2017)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
ECOOP 2017, June 19-23, 2017, Barcelona, SpainEditor
Publication Details
- published at: 2017-06-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-035-4
- DBLP: db/conf/ecoop/ecoop2017
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 74, ECOOP'17, Complete Volume
Abstract
LIPIcs, Volume 74, ECOOP'17, Complete Volume
Cite as
31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Proceedings{muller:LIPIcs.ECOOP.2017,
title = {{LIPIcs, Volume 74, ECOOP'17, Complete Volume}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017},
URN = {urn:nbn:de:0030-drops-72993},
doi = {10.4230/LIPIcs.ECOOP.2017},
annote = {Keywords: Programming Techniques; Software Engineering}
}
Document
Front Matter
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors
Abstract
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors
Cite as
31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 0:i-0:xxvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{muller:LIPIcs.ECOOP.2017.0,
author = {M\"{u}ller, Peter},
title = {{Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {0:i--0:xxvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.0},
URN = {urn:nbn:de:0030-drops-72783},
doi = {10.4230/LIPIcs.ECOOP.2017.0},
annote = {Keywords: Programming Techniques, Software Engineering}
}
Document
Invited Talk
Challenges to Achieving High Availability at Scale (Invited Talk)
Abstract
Facebook is a social network that connects more than 1.8 billion people. To serve these many users requires infrastructure which is composed of thousands of interdependent systems that span geographically distributed data centers. But what is the guiding principle for building and operating these systems?
For Facebook’s infrastructure teams the answer is: Systems must always be available and never lose data. This talk will explore this quest. We will focus on three aspects.
Availability and consistency. What form of consistency do Facebook’s systems guarantee? Strong consistency makes understanding easy but has latency penalties, weak consistency is fast but difficult to reason for developers and users. We describe our usage of eventual consistency and delve into how Facebook constructs its caching and replicated storage systems to minimize the duration for achieving consistency. We share empirical data that measures the effectiveness of our design.
Availability and correctness. With network partitions, relaxed forms of consistency, and software bugs, how do we guarantee a consistent state? We present two systems to find and repair structural errors in Facebook’s social graph, one batch and one real-time.
Availability and scale. Sharding is one of the standard answers to operate at scale. But how can we develop one system that can shard storage as well as compute? We will introduce a new Sharding-as-a-Service component. We will show and evaluate how its design and service policies control for latency, failure tolerance and operationally efficiency.
Cite as
Wolfram Schulte. Challenges to Achieving High Availability at Scale (Invited Talk). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{schulte:LIPIcs.ECOOP.2017.1,
author = {Schulte, Wolfram},
title = {{Challenges to Achieving High Availability at Scale}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.1},
URN = {urn:nbn:de:0030-drops-72503},
doi = {10.4230/LIPIcs.ECOOP.2017.1},
annote = {Keywords: Distributed Systems, Availability, Reliability, Fault Tolerance, Consistency, Scalability, Replication, Sharding, Caching}
}
Document
Invited Talk
Composing Software in an Age of Dissonance (Invited Talk)
Abstract
The power of languages is rooted in composition. An infinite number of sentences can be composed from a finite set of generative rules. The more uniformly the rules apply, the more valid compositions there are. Hence simpler rules give rise to richer discourse - a case of ‘less is more’. We must however be careful as to which distinctions we preserve and which we eliminate. If we abstract too much we risk creating an undifferentiated soup with no landmarks to
orient us.
A uniform space of objects with simple rules governing their interaction is an obvious example of these ideas, but objects also serve as a cautionary tale. Achieving simplicity is not easy; it requires taste, judgement, experience and dedication. Ingenuity is essential as well, but left unchecked, it often leads to uncontrollable complexity. The path of least resistance follows the
tautological principle that ‘more is more’, and who can argue with a tautology? Dissonance dominates.
I will endeavour to illustrate these rather abstract principles by means of examples from my own work and that of others, in programming languages, software and other domains. We may speak of many things - mixins, modules and memory, graphics and generics, patterns and parsers, architecture and automobiles, objects or other things entirely.
Cite as
Gilad Bracha. Composing Software in an Age of Dissonance (Invited Talk). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bracha:LIPIcs.ECOOP.2017.2,
author = {Bracha, Gilad},
title = {{Composing Software in an Age of Dissonance}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.2},
URN = {urn:nbn:de:0030-drops-72796},
doi = {10.4230/LIPIcs.ECOOP.2017.2},
annote = {Keywords: Object-orientation, Programming languages, Modularity, IDEs, Software Design}
}
Document
Invited Talk
Retargeting Gradual Typing (Invited Talk)
Abstract
Gradual typing is often motivated by efforts to add types to massive untyped code bases. A major challenge here is the fact that these code bases were not written with types in mind, yet the goal is to add types to them without requiring any significant changes in their implementation. Thus, critical to this application is the notion that gradual typing is being added onto a preexisting system.
But gradual typing also has applications in education, prototyping, and scripting. It allows programmers to ignore types while they are learning programmatic reasoning, while they are experimenting with new designs, or while they are interacting with external systems. At the same time, gradual typing allows these programmers to utilize APIs with types that provide navigable documentation, that concisely describe interfaces, and that enable IDEs to provide assistance. In these applications, programmers are working with types even when they are not writing types. By targeting just these applications, we
can lift a major burden from gradual typing. Rather than being added to something that already exists, here gradual typing can be integrated into the software-development process, into the core language design, and into the run-time environment, with each component designed to support gradual typing from conception.
This retargeting provides significant flexibility, enabling designers to tradeoff various capabilities of gradual typing. For example, a designer might choose to require some minor annotation burden in untyped programs for, say, a hundred-fold improvement in run-time performance. For the past half decade I have been exploring gradual typing behind the scenes in both academia and industry, and I will be presenting my experiences with these design tradeoffs so
far.
Cite as
Ross Tate. Retargeting Gradual Typing (Invited Talk). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{tate:LIPIcs.ECOOP.2017.3,
author = {Tate, Ross},
title = {{Retargeting Gradual Typing}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.3},
URN = {urn:nbn:de:0030-drops-72802},
doi = {10.4230/LIPIcs.ECOOP.2017.3},
annote = {Keywords: Design, Efficiency, Gradual Typing, Nominal Types}
}
Document
Parallelizing Julia with a Non-Invasive DSL
Abstract
Computational scientists often prototype software using productivity
languages that offer high-level programming abstractions. When higher
performance is needed, they are obliged to rewrite their code in a
lower-level efficiency language. Different solutions have been
proposed to address this trade-off between productivity and
efficiency. One promising approach is to create embedded
domain-specific languages that sacrifice generality for productivity
and performance, but practical experience with DSLs points to some
road blocks preventing widespread adoption. This paper proposes a
non-invasive domain-specific language that makes as few visible
changes to the host programming model as possible. We present ParallelAccelerator,
a library and compiler for high-level, high-performance scientific
computing in Julia. ParallelAccelerator's programming model is aligned with existing
Julia programming idioms. Our compiler exposes the implicit
parallelism in high-level array-style programs and compiles them to
fast, parallel native code. Programs can also run in "library-only"
mode, letting users benefit from the full Julia environment and
libraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.
Cite as
Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{anderson_et_al:LIPIcs.ECOOP.2017.4,
author = {Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
title = {{Parallelizing Julia with a Non-Invasive DSL}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {4:1--4:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.4},
URN = {urn:nbn:de:0030-drops-72693},
doi = {10.4230/LIPIcs.ECOOP.2017.4},
annote = {Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}
Document
Modelling Homogeneous Generative Meta-Programming
Abstract
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Template Haskell. The calculus is designed such that it can be gradually enhanced with the features needed to model many of the
advanced features of real languages. We demonstrate this by showing how a simple, staged type system as found in Template Haskell can be added to the calculus.
Cite as
Martin Berger, Laurence Tratt, and Christian Urban. Modelling Homogeneous Generative Meta-Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{berger_et_al:LIPIcs.ECOOP.2017.5,
author = {Berger, Martin and Tratt, Laurence and Urban, Christian},
title = {{Modelling Homogeneous Generative Meta-Programming}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {5:1--5:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.5},
URN = {urn:nbn:de:0030-drops-72775},
doi = {10.4230/LIPIcs.ECOOP.2017.5},
annote = {Keywords: Formal Methods, Meta-Programming, Operational Semantics, Types, Quasi-Quotes, Abstract Syntax Trees}
}
Document
Relaxed Linear References for Lock-free Data Structures
Abstract
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom.
This paper presents LOLCAT, a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads.
The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.
Cite as
Elias Castegren and Tobias Wrigstad. Relaxed Linear References for Lock-free Data Structures. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 6:1-6:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{castegren_et_al:LIPIcs.ECOOP.2017.6,
author = {Castegren, Elias and Wrigstad, Tobias},
title = {{Relaxed Linear References for Lock-free Data Structures}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {6:1--6:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.6},
URN = {urn:nbn:de:0030-drops-72670},
doi = {10.4230/LIPIcs.ECOOP.2017.6},
annote = {Keywords: Type systems, Concurrency, Lock-free programming}
}
Document
Type Abstraction for Relaxed Noninterference
Abstract
Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the different information flow approaches to declassification, a particularly expressive approach was proposed by Li and Zdancewic, enforcing a notion of relaxed noninterference by allowing programmers to specify declassification policies that capture the intended manner in which public information can be computed from private data.
This paper shows how we can exploit the familiar notion of type abstraction to support expressive declassification policies in a simpler, yet more expressive manner. In particular, the type-based approach to declassification---which we develop in an object-oriented setting---addresses several issues and challenges with respect to prior work, including a simple notion of label ordering based on subtyping, support for recursive declassification policies, and a local, modular reasoning principle for relaxed noninterference. This work paves the way for integrating declassification policies in practical security-typed languages.
Cite as
Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 7:1-7:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cruz_et_al:LIPIcs.ECOOP.2017.7,
author = {Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
title = {{Type Abstraction for Relaxed Noninterference}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {7:1--7:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.7},
URN = {urn:nbn:de:0030-drops-72688},
doi = {10.4230/LIPIcs.ECOOP.2017.7},
annote = {Keywords: type abstraction, relaxed noninterference, information flow control}
}
Document
Concurrent Data Structures Linked in Time
Abstract
Arguments about correctness of a concurrent data structure are
typically carried out by using the notion of linearizability and
specifying the linearization points of the data structure's
procedures. Such arguments are often cumbersome as the linearization
points' position in time can be dynamic (depend on the interference,
run-time values and events from the past, or even future), non-local
(appear in procedures other than the one considered), and whose
position in the execution trace may only be determined after the
considered procedure has already terminated.
In this paper we propose a new method, based on a separation-style
logic, for reasoning about concurrent objects with such linearization
points. We embrace the dynamic nature of linearization points, and
encode it as part of the data structure's auxiliary state, so that it
can be dynamically modified in place by auxiliary code, as needed when
some appropriate run-time event occurs. We name the idea
linking-in-time, because it reduces temporal reasoning to spatial
reasoning. For example, modifying a temporal position of a
linearization point can be modeled similarly to a pointer update in
separation logic. Furthermore, the auxiliary state provides a
convenient way to concisely express the properties essential for
reasoning about clients of such concurrent objects. We illustrate the
method by verifying (mechanically in Coq) an intricate optimal
snapshot algorithm due to Jayanti, as well as some clients.
Cite as
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{delbianco_et_al:LIPIcs.ECOOP.2017.8,
author = {Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
title = {{Concurrent Data Structures Linked in Time}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {8:1--8:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.8},
URN = {urn:nbn:de:0030-drops-72558},
doi = {10.4230/LIPIcs.ECOOP.2017.8},
annote = {Keywords: Separation logic, Linearization Points, Concurrent snapshots, FCSL}
}
Document
Contracts in the Wild: A Study of Java Programs
Abstract
The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checking — has progressed. In the case of Java, built-in features of the language (e.g. assertions and exceptions) can be used for this. Furthermore, a number of libraries which facilitate contract checking have arisen.
In this paper, we catalogue 25 techniques and tools for lightweight contract checking in Java, and present the results of an empirical study looking at a dataset extracted from the 200 most popular projects found on Maven Central, constituting roughly 351,034 KLOC. We examine (1) the extent to which contracts are used and (2) what kind of contracts are used. We then investigate how contracts are used to safeguard code, and study problems in the context of two types of substitutability that can be guarded by contracts: (3) unsafe evolution of APIs that may break client programs and (4) violations of Liskovs Substitution Principle (LSP) when methods are overridden. We find that: (1) a wide range of techniques and constructs are used to represent contracts, and often the same program uses different techniques at the same time; (2) overall, contracts are used less than expected, with significant differences between programs; (3) projects that use contracts continue to do so, and expand the use of contracts as they grow and evolve; and, (4) there are cases where the use of contracts points to unsafe subtyping (violations of Liskov's Substitution Principle) and unsafe evolution.
Cite as
Jens Dietrich, David J. Pearce, Kamil Jezek, and Premek Brada. Contracts in the Wild: A Study of Java Programs. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 9:1-9:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dietrich_et_al:LIPIcs.ECOOP.2017.9,
author = {Dietrich, Jens and Pearce, David J. and Jezek, Kamil and Brada, Premek},
title = {{Contracts in the Wild: A Study of Java Programs}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {9:1--9:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.9},
URN = {urn:nbn:de:0030-drops-72590},
doi = {10.4230/LIPIcs.ECOOP.2017.9},
annote = {Keywords: verification, design-by-contract, assertions, preconditions, postconditions, runtime checking, java, input validation}
}
Document
Evil Pickles: DoS Attacks Based on Object-Graph Engineering
Abstract
In recent years, multiple vulnerabilities exploiting the serialisation APIs of various programming languages, including Java, have been discovered. These vulnerabilities can be used to devise in- jection attacks, exploiting the presence of dynamic programming language features like reflection or dynamic proxies. In this paper, we investigate a new type of serialisation-related vulnerabilit- ies for Java that exploit the topology of object graphs constructed from classes of the standard library in a way that deserialisation leads to resource exhaustion, facilitating denial of service attacks. We analyse three such vulnerabilities that can be exploited to exhaust stack memory, heap memory and CPU time. We discuss the language and library design features that enable these vulnerabilities, and investigate whether these vulnerabilities can be ported to C#, Java- Script and Ruby. We present two case studies that demonstrate how the vulnerabilities can be used in attacks on two widely used servers, Jenkins deployed on Tomcat and JBoss. Finally, we propose a mitigation strategy based on contract injection.
Cite as
Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin. Evil Pickles: DoS Attacks Based on Object-Graph Engineering. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dietrich_et_al:LIPIcs.ECOOP.2017.10,
author = {Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed and Potanin, Alex},
title = {{Evil Pickles: DoS Attacks Based on Object-Graph Engineering}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {10:1--10:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.10},
URN = {urn:nbn:de:0030-drops-72606},
doi = {10.4230/LIPIcs.ECOOP.2017.10},
annote = {Keywords: serialisation, denial of service, degradation of service, Java, C#, JavaScript, Ruby, vulnerabilities, library design, collection libraries}
}
Document
Mixing Metaphors: Actors as Channels and Channels as Actors
Abstract
Channel- and actor-based programming languages are both used in
practice, but the two are often confused. Languages such as Go
provide anonymous processes which communicate using buffers or rendezvous points---known as channels---while languages such as Erlang provide addressable processes---known as actors---each with a single incoming message queue.
The lack of a common representation makes it difficult to reason about
translations that exist in the folklore. We define a calculus
lambda-ch for typed asynchronous channels, and a calculus lambda-act for
typed actors. We define translations from lambda-act into lambda-ch and
lambda-ch into lambda-act and prove that both are type- and
semantics-preserving.
We show that our approach accounts for synchronisation and selective
receive in actor systems and discuss future extensions to support guarded
choice and behavioural types.
Cite as
Simon Fowler, Sam Lindley, and Philip Wadler. Mixing Metaphors: Actors as Channels and Channels as Actors. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fowler_et_al:LIPIcs.ECOOP.2017.11,
author = {Fowler, Simon and Lindley, Sam and Wadler, Philip},
title = {{Mixing Metaphors: Actors as Channels and Channels as Actors}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {11:1--11:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.11},
URN = {urn:nbn:de:0030-drops-72536},
doi = {10.4230/LIPIcs.ECOOP.2017.11},
annote = {Keywords: Actors, Channels, Communication centric Programming Languages}
}
Document
muPuppet: A Declarative Subset of the Puppet Configuration Language
Abstract
Puppet is a popular declarative framework for specifying and managing complex system configurations. The Puppet framework includes a domain-specific language with several advanced features inspired by object-oriented programming, including user-defined resource types, ‘classes’ with a form of inheritance, and dependency management. Like most real-world languages, the language has evolved in an ad hoc fashion, resulting in a design with numerous features, some of which are complex, hard to understand, and difficult to use correctly.
We present an operational semantics for muPuppet, a representative subset of the Puppet language that covers the distinctive features of Puppet, while excluding features that are either deprecated or work-in-progress. Formalising the semantics sheds light on difficult parts of the language, identifies opportunities for future improvements, and provides a foundation for future analysis or debugging techniques, such as static typechecking or provenance tracking. Our semantics leads straightforwardly to a reference implementation in Haskell. We also discuss some of Puppet’s idiosyncrasies, particularly its handling of classes and scope, and present an initial corpus of test cases supported by our formal semantics.
Cite as
Weili Fu, Roly Perera, Paul Anderson, and James Cheney. muPuppet: A Declarative Subset of the Puppet Configuration Language. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 12:1-12:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fu_et_al:LIPIcs.ECOOP.2017.12,
author = {Fu, Weili and Perera, Roly and Anderson, Paul and Cheney, James},
title = {{muPuppet: A Declarative Subset of the Puppet Configuration Language}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {12:1--12:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.12},
URN = {urn:nbn:de:0030-drops-72656},
doi = {10.4230/LIPIcs.ECOOP.2017.12},
annote = {Keywords: configuration languages, Puppet, operational semantics}
}
Document
A Generic Approach to Flow-Sensitive Polymorphic Effects
Abstract
Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant.
Understanding such systems in terms of a lattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems.
By contrast, sequential effect systems --- where the order of effects is important --- lack a clear algebraic characterization.
We derive an algebraic characterization from the shape of prior concrete sequential effect systems.
We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale --- an algebraic structure with well-defined properties that can model a range of existing order-sensitive effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems.
We show that effect quantales provide a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work.
Identifying and applying the right algebraic structure led us to subtle insights into the design of order-sensitive effect systems, which provides guidance on non-obvious points of designing order-sensitive effect systems.
Effect quantales have clear relationships to the recent category theoretic work on order-sensitive effect systems, but are explained without recourse to category theory. In addition, our derived iteration construct should generalize to these semantic structures, addressing limitations of that work.
Cite as
Colin S. Gordon. A Generic Approach to Flow-Sensitive Polymorphic Effects. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gordon:LIPIcs.ECOOP.2017.13,
author = {Gordon, Colin S.},
title = {{A Generic Approach to Flow-Sensitive Polymorphic Effects}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {13:1--13:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.13},
URN = {urn:nbn:de:0030-drops-72561},
doi = {10.4230/LIPIcs.ECOOP.2017.13},
annote = {Keywords: Type systems, effect systems, quantales, polymorphism}
}
Document
IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition
Abstract
Derived values are values calculated from base values. They can be expressed with views in relational databases, or with expressions in incremental or reactive programming. However, relational views do not provide multiplicity bounds, and incremental and reactive programming require significant boilerplate code in order to encode bidirectional derived values. Moreover, the composition of various strategies for calculating derived values is either disallowed, or not checked for producing derived values which will be consistent with the derived values they depend upon.
In this paper we present IceDust2, an extension of the declarative data modeling language IceDust with derived bidirectional relations with multiplicity bounds and support for statically checked composition of calculation strategies. Derived bidirectional relations, multiplicity bounds, and calculation strategies all influence runtime behavior of changes to data, leading to hundreds of possible behavior definitions. IceDust2 uses a product-line based code generator to avoid explicitly defining all possible combinations, making it easier to reason about correctness. The type system allows only sound composition of strategies and guarantees multiplicity bounds. Finally, our case studies validate the usability of IceDust2 in applications.
Cite as
Daco C. Harkes and Eelco Visser. IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 14:1-14:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{harkes_et_al:LIPIcs.ECOOP.2017.14,
author = {Harkes, Daco C. and Visser, Eelco},
title = {{IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {14:1--14:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.14},
URN = {urn:nbn:de:0030-drops-72518},
doi = {10.4230/LIPIcs.ECOOP.2017.14},
annote = {Keywords: Incremental Computing, Data Modeling, Domain Specific Language}
}
Document
What'’s the Optimal Performance of Precise Dynamic Race Detection? –A Redundancy Perspective
Abstract
In a precise data race detector, a race is detected only if the execution exhibits a real race. In such tools, every memory access from each thread is typically checked by a happens-before algorithm. What’s the optimal runtime performance of such tools? In this paper, we identify that a significant percentage of memory access checks in real-world program executions are often redundant: removing these checks affects neither the precision nor the capability of race detection. We show that if all such redundant checks were eliminated with no cost, the optimal performance of a state-of-the-art dynamic race detector, FastTrack, could be improved by 90%, reducing its runtime overhead from 68X to 7X on a collection of CPU intensive benchmarks. We further develop a purely dynamic technique, ReX, that efficiently filters out redundant checks and apply it to FastTrack. With ReX, the runtime performance of FastTrack is improved by 31% on average.
Cite as
Jeff Huang and Arun K. Rajagopalan. What'’s the Optimal Performance of Precise Dynamic Race Detection? –A Redundancy Perspective. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{huang_et_al:LIPIcs.ECOOP.2017.15,
author = {Huang, Jeff and Rajagopalan, Arun K.},
title = {{What'’s the Optimal Performance of Precise Dynamic Race Detection? –A Redundancy Perspective}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {15:1--15:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.15},
URN = {urn:nbn:de:0030-drops-72722},
doi = {10.4230/LIPIcs.ECOOP.2017.15},
annote = {Keywords: Data Race Detection, Dynamic Analysis, Concurrency, Redundancy}
}
Document
Speeding Up Maximal Causality Reduction with Static Dependency Analysis
Abstract
Stateless Model Checking (SMC) offers a powerful approach to verifying multithreaded programs but suffers from the state-space explosion problem caused by the huge thread interleaving space. The pioneering reduction technique Partial Order Reduction (POR) mitigates this problem by pruning equivalent interleavings from the state space. However, limited by the happens-before relation, POR still explores redundant executions. The recent advance, Maximal Causality Reduction (MCR), shows a promising performance improvement over the existing reduction techniques, but it has to construct complicated constraints to ensure the feasibility of the derived execution due to the lack of dependency information. In this work, we present a new technique, which extends MCR with static analysis to reduce the size of the constraints, thus speeding up the exploration of the state space. We also address the redundancy problem caused by the use of static analysis. We capture the dependency between a read and a later event e in the trace from the system dependency graph and identify those reads that e is not control dependent on. Our approach then ignores the constraints over such reads to reduce the complexity of the constraints. The experimental results show that compared to MCR, the number of the constraints and the solving time by our approach are averagely reduced by 31.6% and 27.8%, respectively.
Cite as
Shiyou Huang and Jeff Huang. Speeding Up Maximal Causality Reduction with Static Dependency Analysis. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{huang_et_al:LIPIcs.ECOOP.2017.16,
author = {Huang, Shiyou and Huang, Jeff},
title = {{Speeding Up Maximal Causality Reduction with Static Dependency Analysis}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {16:1--16:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.16},
URN = {urn:nbn:de:0030-drops-72523},
doi = {10.4230/LIPIcs.ECOOP.2017.16},
annote = {Keywords: Model Checking, Dynamic Analysis, Program Dependency Analysis}
}
Document
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
Abstract
The field of concurrent separation logics (CSLs) has recently
undergone two exciting developments: (1) the Iris framework for
encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency.
Unfortunately, these developments are seemingly incompatible, since
Iris only applies to languages with an operational interleaving
semantics, while C11 is defined by a declarative (axiomatic)
semantics. In this paper, we show that, on the contrary, it is not
only feasible but useful to marry these developments together. Our
first step is to provide a novel operational characterization of
RA+NA, the fragment of C11 containing RA accesses and "non-atomic"
(normal data) accesses. Instantiating Iris with this semantics, we
then derive higher-order variants of two prominent RA+NA logics, GPS
and RSL. Finally, we deploy these derived logics in order to perform
the first mechanical verifications (in Coq) of several interesting
case studies of RA+NA programming. In a nutshell, we provide the
first foundationally verified framework for proving programs correct
under C11's weak-memory semantics.
Cite as
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kaiser_et_al:LIPIcs.ECOOP.2017.17,
author = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
title = {{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {17:1--17:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.17},
URN = {urn:nbn:de:0030-drops-72753},
doi = {10.4230/LIPIcs.ECOOP.2017.17},
annote = {Keywords: Weak memory models, release-acquire, concurrency, separation logic}
}
Document
A Co-contextual Type Checker for Featherweight Java
Abstract
This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented languages: Subtype polymorphism, nominal typing, and implementation inheritance. Type checkers encode these features in the form of class tables, an additional form of typing context inhibiting incrementalization.
In the present work, we demonstrate that an appropriate co-contextual notion to class tables exists, paving the way to efficient incremental type checkers for object-oriented languages. This yields a novel formulation of Igarashi et al.'s Featherweight Java (FJ) type system, where we replace class tables by the dual concept of class table requirements and class table operations by dual operations on class table requirements. We prove the equivalence of FJ's type system and our co-contextual formulation. Based on our formulation, we implemented an incremental FJ type checker and compared its performance against javac on a number of realistic example programs.
Cite as
Edlira Kuci, Sebastian Erdweg, Oliver Bracevac, Andi Bejleri, and Mira Mezini. A Co-contextual Type Checker for Featherweight Java. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 18:1-18:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kuci_et_al:LIPIcs.ECOOP.2017.18,
author = {Kuci, Edlira and Erdweg, Sebastian and Bracevac, Oliver and Bejleri, Andi and Mezini, Mira},
title = {{A Co-contextual Type Checker for Featherweight Java}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {18:1--18:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.18},
URN = {urn:nbn:de:0030-drops-72628},
doi = {10.4230/LIPIcs.ECOOP.2017.18},
annote = {Keywords: type checking, co-contextual, constraints, class table, Featherweight Java}
}
Document
Proactive Synthesis of Recursive Tree-to-String Functions from Examples
Abstract
Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute to foundations of such techniques and present a complete algorithm for synthesis of a class of recursive functions defined by structural recursion over a given algebraic data type definition. The functions we consider map an algebraic data type to a string; they are useful for, e.g., pretty printing and serialization of programs and data. We formalize our problem as learning deterministic sequential
top-down tree-to-string transducers with a single state (1STS).
The first problem we consider is learning a tree-to-string
transducer from any set of input/output examples provided by the user. We show that, given a set of input/output examples, checking whether there exists a 1STS consistent with these examples is NP-complete in general. In contrast, the problem can be solved in polynomial time under a (practically useful) closure condition that each
subtree of a tree in the input/output example set is also
part of the input/output examples.
Because coming up with relevant input/output examples may be
difficult for the user while creating hard constraint problems
for the synthesizer, we also study a more automated
active learning scenario in which the algorithm chooses the
inputs for which the user provides the outputs. Our
algorithm asks a worst-case linear number of queries as a
function of the size of the algebraic data type definition
to determine a unique transducer.
To construct our algorithms we present two new results on
formal languages.
First, we define a class of word equations, called
sequential word equations, for which we prove that
satisfiability can be solved in deterministic polynomial
time. This is in contrast to the general word equations for
which the best known complexity upper bound is in linear space.
Second, we close a long-standing open problem about the
asymptotic size of test sets for context-free languages. A
test set of a language of words L is a subset T of L
such that any two word homomorphisms equivalent on T are
also equivalent on L. We prove that it is possible to
build test sets of cubic size for context-free languages,
matching for the first time the lower bound found 20 years
ago.
Cite as
Mikaël Mayer, Jad Hamza, and Viktor Kuncak. Proactive Synthesis of Recursive Tree-to-String Functions from Examples. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{mayer_et_al:LIPIcs.ECOOP.2017.19,
author = {Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
title = {{Proactive Synthesis of Recursive Tree-to-String Functions from Examples}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {19:1--19:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.19},
URN = {urn:nbn:de:0030-drops-72575},
doi = {10.4230/LIPIcs.ECOOP.2017.19},
annote = {Keywords: programming by example, active learning, program synthesis}
}
Document
A Capability-Based Module System for Authority Control
Abstract
The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application's attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions.
In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are first-class, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is type-safe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability.
Our approach allows developers to determine a module's authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module's interface, without needing to examine the module's implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.
Cite as
Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{melicher_et_al:LIPIcs.ECOOP.2017.20,
author = {Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
title = {{A Capability-Based Module System for Authority Control}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {20:1--20:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.20},
URN = {urn:nbn:de:0030-drops-72709},
doi = {10.4230/LIPIcs.ECOOP.2017.20},
annote = {Keywords: Language-based security, capabilities, authority, modules}
}
Document
Data Exploration through Dot-driven Development
Abstract
Data literacy is becoming increasingly important in the modern world. While spreadsheets make simple data analytics accessible to a large number of people, creating transparent scripts that
can be checked, modified, reproduced and formally analyzed requires expert programming skills. In this paper, we describe the design of a data exploration language that makes the task more accessible by embedding advanced programming concepts into a simple core language.
The core language uses type providers, but we employ them in a novel way -- rather than providing types with members for accessing data, we provide types with members that allow the user to also compose rich and correct queries using just member access ('dot'). This way, we recreate functionality that usually requires complex type systems (row polymorphism, type state and dependent typing) in an extremely simple object-based language.
We formalize our approach using an object-based calculus and prove that programs constructed using the provided types represent valid data transformations. We discuss a case study developed using the
language, together with additional editor tooling that bridges some of the gaps between programming and spreadsheets. We believe that this work provides a pathway towards democratizing data science
- our use of type providers significantly reduce the complexity of languages that one needs to understand in order to write scripts for exploring data.
Cite as
Tomas Petricek. Data Exploration through Dot-driven Development. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{petricek:LIPIcs.ECOOP.2017.21,
author = {Petricek, Tomas},
title = {{Data Exploration through Dot-driven Development}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {21:1--21:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.21},
URN = {urn:nbn:de:0030-drops-72610},
doi = {10.4230/LIPIcs.ECOOP.2017.21},
annote = {Keywords: Data science, type providers, pivot tables, aggregation}
}
Document
Promising Compilation to ARMv8 POP
Abstract
We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the "promising" semantics of [Kang et al. POPL'17] to the ARMv8 POP machine of [Flur et al. POPL'16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP.
Cite as
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Promising Compilation to ARMv8 POP. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{podkopaev_et_al:LIPIcs.ECOOP.2017.22,
author = {Podkopaev, Anton and Lahav, Ori and Vafeiadis, Viktor},
title = {{Promising Compilation to ARMv8 POP}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {22:1--22:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.22},
URN = {urn:nbn:de:0030-drops-72667},
doi = {10.4230/LIPIcs.ECOOP.2017.22},
annote = {Keywords: ARM, Compilation Correctness, Weak Memory Model}
}
Document
Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis
Abstract
Function duplication is widely used by JIT compilers to efficiently implement dynamic languages. When the source language supports higher order functions, the called function's identity is not generally known when compiling a call site, thus limiting the use of function duplication. This paper presents a JIT compilation technique enabling function duplication in the presence of higher order functions. Unlike existing techniques, our approach uses dynamic dispatch at call sites instead of relying on a conservative analysis to discover function identity. We have implemented the technique in a JIT compiler for Scheme.
Experiments show that it is efficient at removing type checks, allowing the removal of almost all the run time type checks for several benchmarks.
This allows the compiler to generate code up to 50% faster. We show that the technique can be used to duplicate functions using other run time information opening up new applications such as register allocation based duplication and aggressive inlining.
Cite as
Baptiste Saleil and Marc Feeley. Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{saleil_et_al:LIPIcs.ECOOP.2017.23,
author = {Saleil, Baptiste and Feeley, Marc},
title = {{Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {23:1--23:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.23},
URN = {urn:nbn:de:0030-drops-72711},
doi = {10.4230/LIPIcs.ECOOP.2017.23},
annote = {Keywords: Just-in-time compilation, Interprocedural optimization, Dynamic language, Higher-order function, Scheme}
}
Document
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming
Abstract
Multiparty Session Types (MPST) is a typing discipline for
message-passing distributed processes that can ensure properties such
as absence of communication errors and deadlocks, and protocol
conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address
this problem by (1) developing the first encoding of a
full-fledged multiparty session pi-calculus into linear
pi-calculus, and (2) using the encoding as the foundation of a
practical toolchain for safe multiparty programming in Scala.
Our encoding is type-preserving and operationally sound and complete.
Crucially, it keeps the distributed choreographic nature of
MPST, illuminating that the safety properties of multiparty sessions
can be precisely represented with a decomposition into binary
linear channels. Previous works have only studied the relation
between (limited) multiparty and binary sessions via centralised
orchestration means. We exploit these results to implement an
automated generation of Scala APIs for multiparty sessions,
abstracting existing libraries for binary communication channels.
This allows multiparty systems to be safely implemented over binary
message transports, as commonly found in practice. Our implementation
is the first to support distributed multiparty delegation: our
encoding yields it for free, via existing mechanisms for binary
delegation.
Cite as
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{scalas_et_al:LIPIcs.ECOOP.2017.24,
author = {Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
title = {{A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {24:1--24:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.24},
URN = {urn:nbn:de:0030-drops-72637},
doi = {10.4230/LIPIcs.ECOOP.2017.24},
annote = {Keywords: process calculi, session types, concurrent programming, Scala}
}
Document
Mailbox Abstractions for Static Analysis of Actor Programs
Abstract
Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs.
This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors.
We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program.
We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes.
Sound abstraction of these mailboxes is crucial to the precision of any such technique.
We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox.
We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs.
The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.
Cite as
Quentin Stiévenart, Jens Nicolay, Wolfgang De Meuter, and Coen De Roover. Mailbox Abstractions for Static Analysis of Actor Programs. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 25:1-25:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{stievenart_et_al:LIPIcs.ECOOP.2017.25,
author = {Sti\'{e}venart, Quentin and Nicolay, Jens and De Meuter, Wolfgang and De Roover, Coen},
title = {{Mailbox Abstractions for Static Analysis of Actor Programs}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {25:1--25:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.25},
URN = {urn:nbn:de:0030-drops-72541},
doi = {10.4230/LIPIcs.ECOOP.2017.25},
annote = {Keywords: static analysis, abstraction, abstract interpretation, actors, mailbox}
}
Document
Compiling Tree Transforms to Operate on Packed Representations
Abstract
When written idiomatically in most programming languages, programs
that traverse and construct trees operate over pointer-based data
structures, using one heap object per-leaf and per-node. This
representation is efficient for random access and shape-changing
modifications, but for traversals, such as compiler passes, that
process most or all of a tree in bulk, it can be inefficient. In this
work we instead compile tree traversals to operate on
pointer-free pre-order serializations of trees. On modern
architectures such programs often run significantly faster than
their pointer-based counterparts, and additionally are directly suited
to storage and transmission without requiring marshaling.
We present a prototype compiler, Gibbon, that compiles a
small first-order, purely functional language sufficient for tree
traversals. The compiler transforms this language into intermediate
representation with explicit pointers into input and output buffers
for packed data. The key compiler technologies include an effect
system for capturing traversal behavior, combined with an algorithm to
insert destination cursors. We evaluate our compiler on tree
transformations over a real-world dataset of source-code syntax trees.
For traversals touching the whole tree, such as maps and folds, packed
data allows speedups of over 2x compared to a highly-optimized
pointer-based baseline.
Cite as
Michael Vollmer, Sarah Spall, Buddhika Chamith, Laith Sakka, Chaitanya Koparkar, Milind Kulkarni, Sam Tobin-Hochstadt, and Ryan R. Newton. Compiling Tree Transforms to Operate on Packed Representations. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 26:1-26:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{vollmer_et_al:LIPIcs.ECOOP.2017.26,
author = {Vollmer, Michael and Spall, Sarah and Chamith, Buddhika and Sakka, Laith and Koparkar, Chaitanya and Kulkarni, Milind and Tobin-Hochstadt, Sam and Newton, Ryan R.},
title = {{Compiling Tree Transforms to Operate on Packed Representations}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {26:1--26:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.26},
URN = {urn:nbn:de:0030-drops-72737},
doi = {10.4230/LIPIcs.ECOOP.2017.26},
annote = {Keywords: compiler optimization, program transformation, tree traversal}
}
Document
Towards Strong Normalization for Dependent Object Types (DOT)
Abstract
The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof for
DOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully.
Cite as
Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 27:1-27:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.ECOOP.2017.27,
author = {Wang, Fei and Rompf, Tiark},
title = {{Towards Strong Normalization for Dependent Object Types (DOT)}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {27:1--27:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.27},
URN = {urn:nbn:de:0030-drops-72763},
doi = {10.4230/LIPIcs.ECOOP.2017.27},
annote = {Keywords: Scala, DOT, strong normalization, logical relations, recursive types}
}
Document
Mixed Messages: Measuring Conformance and Non-Interference in TypeScript
Abstract
TypeScript participates in the recent trend among programming
languages to support gradual typing. The DefinitelyTyped Repository
for TypeScript supplies type definitions for over 2000 popular
JavaScript libraries. However, there is no guarantee that
implementations conform to their corresponding declarations.
We present a practical evaluation of gradual typing for TypeScript.
We have developed a tool for use with TypeScript, based on the
polymorphic blame calculus, for monitoring JavaScript libraries and
TypeScript clients against the TypeScript definition. We apply our
tool, TypeScript TPD, to those libraries in the DefinitelyTyped
Repository which had adequate test code to use. Of the 122 libraries
we checked, 62 had cases where either the library or its tests
failed to conform to the declaration.
Gradual typing should satisfy non-interference. Monitoring a program
should never change its behaviour, except to raise a type error
should a value not conform to its declared type. However, our
experience also suggests serious technical concerns with the use of
the JavaScript proxy mechanism for enforcing contracts. Of the 122
libraries we checked, 22 had cases where the library or its tests
violated non-interference.
Cite as
Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{williams_et_al:LIPIcs.ECOOP.2017.28,
author = {Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
title = {{Mixed Messages: Measuring Conformance and Non-Interference in TypeScript}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {28:1--28:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.28},
URN = {urn:nbn:de:0030-drops-72640},
doi = {10.4230/LIPIcs.ECOOP.2017.28},
annote = {Keywords: Gradual Typing, TypeScript, JavaScript, Proxies}
}
Document
EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse
Abstract
Object Algebras are a design pattern that enables extensibility, modularity, and reuse in mainstream object-oriented languages such as Java. The theoretical foundations of Object Algebras are rooted on Church encodings of datatypes, which are in turn closely related to folds in functional programming. Unfortunately, it is well-known that certain programs are difficult to write, and may incur performance penalties when using Church-encodings/folds.
This paper presents EVF: an extensible and expressive Java Visitor framework. The visitors supported by EVF generalize Object Algebras and enable writing programs using a generally recursive style rather than folds. The use of such generally recursive style enables users to more naturally write programs, which would otherwise require contrived workarounds using a fold-like structure. EVF visitors retain the type-safe extensibility of Object Algebras. The key advance in EVF is a novel technique to support extensible external visitors. Extensible external visitors are able to control traversals with direct access to the data structure being traversed, allowing dependent operations to be defined modularly without the need of advanced type system features. To make EVF practical, the framework employs annotations to automatically generate large amounts of boilerplate code related to visitors and traversals. To illustrate the applicability of EVF we conduct a case study, which refactors a large number of non-modular interpreters from the “Types and Programming Languages” (TAPL) book. Using EVF we are able to create a modular software product line (SPL) of the TAPL interpreters, enabling sharing of large portions of code and features. The TAPL software product line contains several modular operations, which would be non-trivial to define with standard Object Algebras.
Cite as
Weixin Zhang and Bruno C. d. S. Oliveira. EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 29:1-29:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{zhang_et_al:LIPIcs.ECOOP.2017.29,
author = {Zhang, Weixin and Oliveira, Bruno C. d. S.},
title = {{EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {29:1--29:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.29},
URN = {urn:nbn:de:0030-drops-72749},
doi = {10.4230/LIPIcs.ECOOP.2017.29},
annote = {Keywords: Visitor Pattern, Object Algebras, Modularity, Domain-Specific Languages}
}
Document
An Empirical Study on Deoptimization in the Graal Compiler
Abstract
Managed language platforms such as the Java Virtual Machine or the Common Language Runtime rely on a dynamic compiler to achieve high performance. Besides making optimization decisions based on the actual program execution and the underlying hardware platform, a dynamic compiler is also in an ideal position to perform speculative optimizations. However, these tend to increase the compilation costs, because unsuccessful speculations trigger deoptimization and recompilation of the affected parts of the program, wasting previous work. Even though speculative optimizations are widely used, the costs of these optimizations in terms of extra compilation work has not been previously studied. In this paper, we analyze the behavior of the Graal dynamic compiler integrated in Oracle's HotSpot Virtual Machine. We focus on situations which cause program execution to switch from machine code to the interpreter, and compare application performance using three different deoptimization strategies which influence the amount of extra compilation work done by Graal. Using an adaptive deoptimization strategy, we managed to improve the average start-up performance of benchmarks from the DaCapo, ScalaBench, and Octane benchmark suites, mostly by avoiding wasted compilation work. On a single-core system, we observed an average speed-up of 6.4% for the DaCapo and ScalaBench workloads, and a speed-up of 5.1% for the Octane workloads; the improvement decreases with an increasing number of available CPU cores. We also find that the choice of a deoptimization strategy has negligible impact on steady-state performance. This indicates that the cost of speculation matters mainly during start-up, where it can disturb the delicate balance between executing the program and the compiler, but is quickly amortized in steady state.
Cite as
Yudi Zheng, Lubomír Bulej, and Walter Binder. An Empirical Study on Deoptimization in the Graal Compiler. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 30:1-30:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{zheng_et_al:LIPIcs.ECOOP.2017.30,
author = {Zheng, Yudi and Bulej, Lubom{\'\i}r and Binder, Walter},
title = {{An Empirical Study on Deoptimization in the Graal Compiler}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {30:1--30:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {M\"{u}ller, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.30},
URN = {urn:nbn:de:0030-drops-72583},
doi = {10.4230/LIPIcs.ECOOP.2017.30},
annote = {Keywords: dynamic compiler, profile-guided optimization, deoptimization}
}