Volume
LIPIcs, Volume 37
29th European Conference on Object-Oriented Programming (ECOOP 2015)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Event
ECOOP 2015, July 5-10, 2015, Prague, Czech RepublicEditor
Publication Details
- published at: 2015-06-29
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-86-6
- DBLP: db/conf/ecoop/ecoop2015
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 37, ECOOP'15, Complete Volume
Abstract
LIPIcs, Volume 37, ECOOP'15, Complete Volume
Cite as
29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{boyland:LIPIcs.ECOOP.2015,
title = {{LIPIcs, Volume 37, ECOOP'15, Complete Volume}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015},
URN = {urn:nbn:de:0030-drops-52737},
doi = {10.4230/LIPIcs.ECOOP.2015},
annote = {Keywords: Object-oriented Programming}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Artifacts, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Artifacts, Conference Organization
Cite as
29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. i-xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{boyland:LIPIcs.ECOOP.2015.i,
author = {Boyland, John Tang},
title = {{Front Matter, Table of Contents, Preface, Artifacts, Conference Organization}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {i--xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.i},
URN = {urn:nbn:de:0030-drops-52463},
doi = {10.4230/LIPIcs.ECOOP.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Artifacts, Conference Organization}
}
Document
Invited Talk
Object-Oriented Programming without Inheritance (Invited Talk)
Abstract
Object-oriented programming is often characterized as encapsulation plus polymorphism plus inheritance. The original Simula67 demonstrated that we could do without encapsulation and Kristen Nygaard insisted that some OOP could be done without inheritance. I present generic programming as providing encapsulation plus polymorphism. In C++, this view is directly supported by language facilities, such as classes, templates and (only recently) concepts. I show a range of type-and-resource-safe techniques covering a wide range of applications including containers, algebraic concepts, and numerical and non-numerical algorithms.
Cite as
Bjarne Stroustrup. Object-Oriented Programming without Inheritance (Invited Talk). In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{stroustrup:LIPIcs.ECOOP.2015.1,
author = {Stroustrup, Bjarne},
title = {{Object-Oriented Programming without Inheritance}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {1--1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.1},
URN = {urn:nbn:de:0030-drops-52129},
doi = {10.4230/LIPIcs.ECOOP.2015.1},
annote = {Keywords: object orientation, generic programming, polymorphism, concepts, encapsulation}
}
Document
Invited Talk
Programming in the Large for the Internet of Things (Invited Talk)
Abstract
The term Internet of Things (IoT) has generated a lot of buzz in the information technology and consumer electronics industries. In the IoT setting, a large number of physically dispersed devices - such as sensors, actuators and processing units - coordinate to bring useful capabilities to the user. A significant portion of these devices may have rather small computation and storage footprints, but at the same time, they can leverage support from potential enormous computation and storage resources via the cloud. Also, a large set of small footprint devices can serve not just a single logical app or service, but also many independent logical apps or services. This requires a careful separation of computational activities and their associated data within a device, for privacy and security purposes. Application development for the Internet of Things gives a whole new meaning to the term "programming in the large", and some of this is likely to be new to the practitioner. This talk will discuss what the IoT environment means to the practical programmer, and what apps and app ecosystems for IoT might look like. The talk will also discuss the issues and open challenges in software engineering brought on by this new environment, pointing towards new opportunities for researchers in our community.
Cite as
Jong-Deok Choi. Programming in the Large for the Internet of Things (Invited Talk). In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{choi:LIPIcs.ECOOP.2015.2,
author = {Choi, Jong-Deok},
title = {{Programming in the Large for the Internet of Things}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {2--2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.2},
URN = {urn:nbn:de:0030-drops-52132},
doi = {10.4230/LIPIcs.ECOOP.2015.2},
annote = {Keywords: software development methodologies, software architecture, programming model, software engineering, IoT}
}
Document
Invited Talk
Software Verification "Across the Stack" (Invited Talk)
Abstract
Producing reliable programs has always been tough, and the complexity and variety of programming tasks just keeps on growing. Fortunately, the growth of computing power has also enabled substantial advances in automated reasoning, particularly the development of SMT solvers and automatic theorem provers. In turn, this has resulted in new research directions for program correctness, with the aim of producing tools which can verify complex properties of software automatically.
Developing useful verification techniques requires balancing a number of competing factors. We want to be as expressive as possible in the program properties we can support - if we can write it down, we'd like to be able to prove it. But to progress beyond pen-and-paper efforts, we also need to tailor our approaches such that they can be implemented or encoded by tools, ideally with both precise and efficient results. To make things harder still, if we hope to produce tools which everyday programmers can benefit from, we also need techniques that require manageable interaction from a user, and give understandable feedback.
In this talk, I'll describe some of the fun experiences I've had working on these kinds of problems, from the design of front-end program logics and reasoning techniques to the development of underlying implementation technology, and the tricky encoding challenges that show up in between.
Cite as
Alexander J. Summers. Software Verification "Across the Stack" (Invited Talk). In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{summers:LIPIcs.ECOOP.2015.3,
author = {Summers, Alexander J.},
title = {{Software Verification "Across the Stack"}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {3--3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.3},
URN = {urn:nbn:de:0030-drops-52141},
doi = {10.4230/LIPIcs.ECOOP.2015.3},
annote = {Keywords: software verification, program logic, automatic verifier, program correctness, SMT solvers}
}
Document
Towards Practical Gradual Typing
Abstract
Over the past 20 years, programmers have embraced dynamically-typed programming languages. By now, they have also come to realize that programs in these languages lack reliable type information for software engineering purposes. Gradual typing addresses this problem; it empowers programmers to annotate an existing system with sound type information on a piecemeal basis. This paper presents an implementation of a gradual type system for a full-featured class-based language as well as a novel performance evaluation framework for gradual typing.
Cite as
Asumu Takikawa, Daniel Feltey, Earl Dean, Matthew Flatt, Robert Bruce Findler, Sam Tobin-Hochstadt, and Matthias Felleisen. Towards Practical Gradual Typing. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 4-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{takikawa_et_al:LIPIcs.ECOOP.2015.4,
author = {Takikawa, Asumu and Feltey, Daniel and Dean, Earl and Flatt, Matthew and Findler, Robert Bruce and Tobin-Hochstadt, Sam and Felleisen, Matthias},
title = {{Towards Practical Gradual Typing}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {4--27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.4},
URN = {urn:nbn:de:0030-drops-52156},
doi = {10.4230/LIPIcs.ECOOP.2015.4},
annote = {Keywords: Gradual typing, object-oriented programming, performance evaluation}
}
Document
TreatJS: Higher-Order Contracts for JavaScripts
Abstract
TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts.
TreatJS is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required. The impact of contracts on execution speed is evaluated using the Google Octane benchmark.
Cite as
Matthias Keil and Peter Thiemann. TreatJS: Higher-Order Contracts for JavaScripts. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 28-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{keil_et_al:LIPIcs.ECOOP.2015.28,
author = {Keil, Matthias and Thiemann, Peter},
title = {{TreatJS: Higher-Order Contracts for JavaScripts}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {28--51},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.28},
URN = {urn:nbn:de:0030-drops-52164},
doi = {10.4230/LIPIcs.ECOOP.2015.28},
annote = {Keywords: Higher-Order Contracts, JavaScript, Proxies}
}
Document
Trust, but Verify: Two-Phase Typing for Dynamic Languages
Abstract
A key challenge when statically typing so-called dynamic languages is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave according to the types of its arguments. Thus, to establish basic types, the analysis must reason precisely about values, but in the presence of higher-order functions and polymorphism, this reasoning itself can require basic types. In this paper we address this chicken-and-egg problem by introducing the framework of two-phased typing. The first "trust" phase performs classical, i.e. flow-, path- and value-insensitive type checking to assign basic types to various program expressions. When the check inevitably runs into "errors" due to value-insensitivity, it wraps problematic expressions with DEAD-casts, which explicate the trust obligations that must be discharged by the second phase. The second phase uses refinement typing, a flow- and path-sensitive analysis, that decorates the first phase's types with logical predicates to track value relationships and thereby verify the casts and establish other correctness properties for dynamically typed languages.
Cite as
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. Trust, but Verify: Two-Phase Typing for Dynamic Languages. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 52-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{vekris_et_al:LIPIcs.ECOOP.2015.52,
author = {Vekris, Panagiotis and Cosman, Benjamin and Jhala, Ranjit},
title = {{Trust, but Verify: Two-Phase Typing for Dynamic Languages}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {52--75},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.52},
URN = {urn:nbn:de:0030-drops-52173},
doi = {10.4230/LIPIcs.ECOOP.2015.52},
annote = {Keywords: Dynamic Languages, Type Systems, Refinement Types, Intersection Types, Overloading}
}
Document
Concrete Types for TypeScript
Abstract
Typescript extends JavaScript with optional type annotations that are, by design, unsound and, that the Typescript compiler discards as it emits code. This design point preserves programming idioms developers are familiar with, and allows them to leave their legacy code unchanged, while offering a measure of static error checking in parts of the program that have type annotations. We present an alternative design for TypeScript, one where it is possible to support the same degree of dynamism, but where types can be strengthened to provide hard guarantees. We report on an implementation, called StrongScript, that improves runtime performance of typed programs when run on a modified version of the V8 JavaScript engine.
Cite as
Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 76-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{richards_et_al:LIPIcs.ECOOP.2015.76,
author = {Richards, Gregor and Zappa Nardelli, Francesco and Vitek, Jan},
title = {{Concrete Types for TypeScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {76--100},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.76},
URN = {urn:nbn:de:0030-drops-52185},
doi = {10.4230/LIPIcs.ECOOP.2015.76},
annote = {Keywords: Gradual typing, dynamic languages}
}
Document
Simple and Effective Type Check Removal through Lazy Basic Block Versioning
Abstract
Dynamically typed programming languages such as JavaScript and Python defer type checking to run time. In order to maximize performance, dynamic language VM implementations must attempt to eliminate redundant dynamic type checks. However, type inference analyses are often costly and involve tradeoffs between compilation time and resulting precision. This has lead to the creation of increasingly complex multi-tiered VM architectures.
This paper introduces lazy basic block versioning, a simple JIT compilation technique which effectively removes redundant type checks from critical code paths. This novel approach lazily generates type-specialized versions of basic blocks on-the-fly while propagating context-dependent type information. This does not require the use of costly program analyses, is not restricted by the precision limitations of traditional type analyses and avoids the implementation complexity of speculative optimization techniques.
We have implemented intraprocedural lazy basic block versioning in a JavaScript JIT compiler. This approach is compared with a classical flow-based type analysis. Lazy basic block versioning performs as well or better on all benchmarks. On average, 71% of type tests are eliminated, yielding speedups of up to 50%. We also show that our implementation generates more efficient machine code than TraceMonkey, a tracing JIT compiler for JavaScript, on several benchmarks. The combination of implementation simplicity, low algorithmic complexity and good run time performance makes basic block versioning attractive for baseline JIT compilers.
Cite as
Maxime Chevalier-Boisvert and Marc Feeley. Simple and Effective Type Check Removal through Lazy Basic Block Versioning. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 101-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{chevalierboisvert_et_al:LIPIcs.ECOOP.2015.101,
author = {Chevalier-Boisvert, Maxime and Feeley, Marc},
title = {{Simple and Effective Type Check Removal through Lazy Basic Block Versioning}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {101--123},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.101},
URN = {urn:nbn:de:0030-drops-52196},
doi = {10.4230/LIPIcs.ECOOP.2015.101},
annote = {Keywords: Just-In-Time Compilation, Dynamic Optimization, Type Checking, Code Generation, JavaScript}
}
Document
Loop Tiling in the Presence of Exceptions
Abstract
Exceptions in OO languages provide a convenient mechanism to deal with anomalous situations. However, many of the loop optimization techniques cannot be applied in the presence of conditional throw statements in the body of the loop, owing to possible cross iteration control dependences. Compilers either ignore such throw statements and apply traditional loop optimizations (semantic non-preserving), or conservatively avoid invoking any of these optimizations altogether (inefficient). We define a loop optimization to be xception-safe, if the optimization can be applied even on (possibly) exception throwing loops, in a semantics preserving manner. In this paper, we present a generalized scheme to do exception-safe loop optimizations and present a scheme of optimized exception-safe loop tiling (oESLT), as a specialization thereof.
oESLT tiles the input loops, assuming that exceptions will never be thrown. To ensure the semantics preservation (in case an exception is thrown), oESLT generates code to rollback the updates done in the advanced iterations (iterations that the unoptimized code would not have executed, but executed speculatively by the oESLT generated code) and safely-execute the delayed iterations (ones that the unoptimized code would have executed, but not executed by the code generated by oESLT). For the rollback phase to work efficiently, oESLT identifies a minimal number of elements to backup and generates the necessary code. We implement oESLT, along with a naive scheme (nESLT, where we backup every element and do a full rollback and safe-execution in case an exception is thrown), in the Graphite framework of GCC 4.8. To help in this process, we define a new program region called ESCoPs (Extended Static Control Parts) that helps identify loops with multiple exit points and interface with the underlying polyhedral representation. We use the popular PolyBench suite to present a comparative evaluation of nESLT and oESLT against the unoptimized versions.
Cite as
Abhilash Bhandari and V. Krishna Nandivada. Loop Tiling in the Presence of Exceptions. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 124-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bhandari_et_al:LIPIcs.ECOOP.2015.124,
author = {Bhandari, Abhilash and Nandivada, V. Krishna},
title = {{Loop Tiling in the Presence of Exceptions}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {124--148},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.124},
URN = {urn:nbn:de:0030-drops-52202},
doi = {10.4230/LIPIcs.ECOOP.2015.124},
annote = {Keywords: Compiler optimizations, semantics preservation, exceptions, loop-tiling}
}
Document
Transparent Object Proxies in JavaScript
Abstract
Proxies are the swiss army knives of object adaptation. They introduce a level of indirection to intercept select operations on a target object and divert them as method calls to a handler. Proxies have many uses like implementing access control, enforcing contracts, virtualizing resources.
One important question in the design of a proxy API is whether a proxy object should inherit the identity of its target. Apparently proxies should have their own identity for security-related applications whereas other applications, in particular contract systems, require transparent proxies that compare equal to their target objects.
We examine the issue with transparency in various use cases for proxies, discuss different approaches to obtain transparency, and propose two designs that require modest modifications in the JavaScript engine and cannot be bypassed by the programmer.
We implement our designs in the SpiderMonkey JavaScript interpreter and bytecode compiler. Our evaluation shows that these modifications of have no statistically significant impact on the benchmark performance of the JavaScript engine. Furthermore, we demonstrate that contract systems based on wrappers require transparent proxies to avoid interference with program execution in realistic settings.
Cite as
Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. Transparent Object Proxies in JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 149-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{keil_et_al:LIPIcs.ECOOP.2015.149,
author = {Keil, Matthias and Guria, Sankha Narayan and Schlegel, Andreas and Geffken, Manuel and Thiemann, Peter},
title = {{Transparent Object Proxies in JavaScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {149--173},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.149},
URN = {urn:nbn:de:0030-drops-52299},
doi = {10.4230/LIPIcs.ECOOP.2015.149},
annote = {Keywords: JavaScript, Proxies, Equality, Contracts}
}
Document
A Theory of Tagged Objects
Abstract
Foundational models of object-oriented constructs typically model objects as records with a structural type. However, many object-oriented languages are class-based; statically-typed formal models of these languages tend to sacrifice the foundational nature of the record-based models, and in addition cannot express dynamic class loading or creation. In this paper, we explore how to model statically-typed object-oriented languages that support dynamic class creation using foundational constructs of type theory. We start with an extensible tag construct motivated by type theory, and adapt it to support static reasoning about class hierarchy and the tags supported by each object. The result is a model that better explains the relationship between object-oriented and functional programming paradigms, suggests a useful enhancement to functional programming languages, and paves the way for more expressive statically typed object-oriented languages. In that vein, we describe the design and implementation of the Wyvern language, which leverages our theory.
Cite as
Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. A Theory of Tagged Objects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 174-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{lee_et_al:LIPIcs.ECOOP.2015.174,
author = {Lee, Joseph and Aldrich, Jonathan and Shaw, Troy and Potanin, Alex},
title = {{A Theory of Tagged Objects}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {174--197},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.174},
URN = {urn:nbn:de:0030-drops-52305},
doi = {10.4230/LIPIcs.ECOOP.2015.174},
annote = {Keywords: objects, classes, tags, nominal and structural types}
}
Document
Brand Objects for Nominal Typing
Abstract
Combinations of structural and nominal object typing in systems such as Scala, Whiteoak, and Unity have focused on extending existing nominal, class-based systems with structural subtyping. The typical rules of nominal typing do not lend themselves to such an extension, resulting in major modifications. Adding object branding to an existing structural system integrates nominal and structural typing without excessively complicating the type system. We have implemented brand objects to explicitly type objects, using existing features of the structurally typed language Grace, along with a static type checker which treats the brands as nominal types. We demonstrate that the brands are useful in an existing implementation of Grace, and provide a formal model of the extension to the language.
Cite as
Timothy Jones, Michael Homer, and James Noble. Brand Objects for Nominal Typing. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 198-221, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{jones_et_al:LIPIcs.ECOOP.2015.198,
author = {Jones, Timothy and Homer, Michael and Noble, James},
title = {{Brand Objects for Nominal Typing}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {198--221},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.198},
URN = {urn:nbn:de:0030-drops-52314},
doi = {10.4230/LIPIcs.ECOOP.2015.198},
annote = {Keywords: brands, types, structural, nominal, Grace}
}
Document
Access-rights Analysis in the Presence of Subjects
Abstract
Modern software development and run-time environments, such as Java and the Microsoft .NET Common Language Runtime (CLR), have adopted a declarative form of access control. Permissions are granted to code providers, and during execution, the platform verifies compatibility between the permissions required by a security-sensitive operation and those granted to the executing code. While convenient, configuring the access-control policy of a program is not easy. If a code component is not granted sufficient permissions, authorization failures may occur. Thus, security administrators tend to define overly permissive policies, which violate the Principle of Least Privilege (PLP).
A considerable body of research has been devoted to building program-analysis tools for computing the optimal policy for a program. However, Java and the CLR also allow executing code under the authority of a subject (user or service), and no program-analysis solution has addressed the challenges of determining the policy of a program in the presence of subjects.
This paper introduces Subject Access Rights Analysis (SARA), a novel analysis algorithm for statically computing the permissions required by subjects at run time. We have applied SARA to 348 libraries in IBM WebSphere Application Server - a commercial enterprise application server written in Java that consists of >2 million lines of code and is required to support the Java permission- and subject-based security model. SARA detected 263 PLP violations, 219 cases of policies with missing permissions, and 29 bugs that led code to be unnecessarily executed under the authority of a subject. SARA corrected all these vulnerabilities automatically, and additionally synthesized fresh policies for all the libraries, with a false-positive rate of 5% and an average running time of 103 seconds per library. SARA also implements mechanisms for mitigating the risk of false negatives due to reflection and native code; according to a thorough result evaluation based on testing, no false negative was detected. SARA enabled IBM WebSphere Application Server to receive the Common Criteria for Information Technology Security Evaluation Assurance Level 4 certification.
Cite as
Paolina Centonze, Marco Pistoia, and Omer Tripp. Access-rights Analysis in the Presence of Subjects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 222-246, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{centonze_et_al:LIPIcs.ECOOP.2015.222,
author = {Centonze, Paolina and Pistoia, Marco and Tripp, Omer},
title = {{Access-rights Analysis in the Presence of Subjects}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {222--246},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.222},
URN = {urn:nbn:de:0030-drops-52249},
doi = {10.4230/LIPIcs.ECOOP.2015.222},
annote = {Keywords: Static Analysis, Security, Access Control}
}
Document
Variability Abstractions: Trading Precision for Speed in Family-Based Analyses
Abstract
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a SPL, and produces analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on the number of variants (which is exponential in the number of features, in the worst case). For a large number of features, the lifted analysis may be too costly or even infeasible. In this paper, we introduce variability abstractions defined as Galois connections and use abstract interpretation as a formal method for the calculational-based derivation of approximate (abstracted) lifted analyses of SPL programs, which are sound by construction. Moreover, given an abstraction we define a syntactic transformation that translates any SPL program into an abstracted version of it, such that the analysis of the abstracted SPL coincides with the corresponding abstracted analysis of the original SPL. We implement the transformation in a tool, that works on Object-Oriented Java program families, and evaluate the practicality of this approach on three Java SPL benchmarks.
Cite as
Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 247-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dimovski_et_al:LIPIcs.ECOOP.2015.247,
author = {Dimovski, Aleksandar S. and Brabrand, Claus and Wasowski, Andrzej},
title = {{Variability Abstractions: Trading Precision for Speed in Family-Based Analyses}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {247--270},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.247},
URN = {urn:nbn:de:0030-drops-52253},
doi = {10.4230/LIPIcs.ECOOP.2015.247},
annote = {Keywords: Software Product Lines, Family-Based Program Analysis, Abstract Interpretation}
}
Document
Optimization Coaching for JavaScript
Abstract
The performance of dynamic object-oriented programming languages such as JavaScript depends heavily on highly optimizing just-in-time compilers. Such compilers, like all compilers, can silently fall back to generating conservative, low-performance code during optimization. As a result, programmers may inadvertently cause performance issues on users' systems by making seemingly inoffensive changes to programs. This paper shows how to solve the problem of silent optimization failures. It specifically explains how to create a so-called optimization coach for an object-oriented just-in-time-compiled programming language. The development and evaluation build on the SpiderMonkey JavaScript engine, but the results should generalize to a variety of similar platforms.
Cite as
Vincent St-Amour and Shu-yu Guo. Optimization Coaching for JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 271-295, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{stamour_et_al:LIPIcs.ECOOP.2015.271,
author = {St-Amour, Vincent and Guo, Shu-yu},
title = {{Optimization Coaching for JavaScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {271--295},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.271},
URN = {urn:nbn:de:0030-drops-52260},
doi = {10.4230/LIPIcs.ECOOP.2015.271},
annote = {Keywords: Optimization Coaching, JavaScript, Performance Tools}
}
Document
PerfBlower: Quickly Detecting Memory-Related Performance Problems via Amplification
Abstract
Performance problems in managed languages are extremely difficult to find. Despite many efforts to find those problems, most existing work focuses on how to debug a user-provided test execution in which performance problems already manifest. It remains largely unknown how to effectively find performance bugs before software release. As a result, performance bugs often escape to production runs, hurting software reliability and user experience. This paper describes PerfBlower, a general performance testing framework that allows developers to quickly test Java programs to find memory-related performance problems. PerfBlower provides (1) a novel specification language ISL to describe a general class of performance problems that have observable symptoms; (2) an automated test oracle via \emph{virtual amplification}; and (3) precise reference-path-based diagnostic information via object mirroring. Using this framework, we have amplified three different types of problems. Our experimental results demonstrate that (1) ISL is expressive enough to describe various memory-related performance problems; (2) PerfBlower successfully distinguishes executions with and without problems; 8 unknown problems are quickly discovered under small workloads; and (3) PerfBlower outperforms existing detectors and does not miss any bugs studied before in the literature.
Cite as
Lu Fang, Liang Dou, and Guoqing Xu. PerfBlower: Quickly Detecting Memory-Related Performance Problems via Amplification. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 296-320, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fang_et_al:LIPIcs.ECOOP.2015.296,
author = {Fang, Lu and Dou, Liang and Xu, Guoqing},
title = {{PerfBlower: Quickly Detecting Memory-Related Performance Problems via Amplification}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {296--320},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.296},
URN = {urn:nbn:de:0030-drops-52278},
doi = {10.4230/LIPIcs.ECOOP.2015.296},
annote = {Keywords: Performance bugs, memory problems, managed languages, garbage collection\}}
}
Document
Hybrid DOM-Sensitive Change Impact Analysis for JavaScript
Abstract
JavaScript has grown to be among the most popular programming languages. However, performing change impact analysis on JavaScript applications is challenging due to features such as the seamless interplay with the DOM, event-driven and dynamic function calls, and asynchronous client/server communication. We first perform an empirical study of change propagation, the results of which show that the DOM-related and dynamic features of JavaScript need to be taken into consideration in the analysis since they affect change impact propagation. We propose a DOM-sensitive hybrid change impact analysis technique for Javascript through a combination of static and dynamic analysis. The proposed approach incorporates a novel ranking algorithm for indicating the importance of each entity in the impact set. Our approach is implemented in a tool called Tochal. The results of our evaluation reveal that Tochal provides a more complete analysis compared to static or dynamic methods. Moreover, through an industrial controlled experiment, we find that Tochal helps developers by improving their task completion duration by 78% and accuracy by 223%.
Cite as
Saba Alimadadi, Ali Mesbah, and Karthik Pattabiraman. Hybrid DOM-Sensitive Change Impact Analysis for JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 321-345, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{alimadadi_et_al:LIPIcs.ECOOP.2015.321,
author = {Alimadadi, Saba and Mesbah, Ali and Pattabiraman, Karthik},
title = {{Hybrid DOM-Sensitive Change Impact Analysis for JavaScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {321--345},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.321},
URN = {urn:nbn:de:0030-drops-52280},
doi = {10.4230/LIPIcs.ECOOP.2015.321},
annote = {Keywords: Change impact analysis, JavaScript, hybrid analysis}
}
Document
Intensional Effect Polymorphism
Abstract
Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve efficiency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, security, graphical user interface access, and memoization.
Cite as
Yuheng Long, Yu David Liu, and Hridesh Rajan. Intensional Effect Polymorphism. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 346-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{long_et_al:LIPIcs.ECOOP.2015.346,
author = {Long, Yuheng and Liu, Yu David and Rajan, Hridesh},
title = {{Intensional Effect Polymorphism}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {346--370},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.346},
URN = {urn:nbn:de:0030-drops-52213},
doi = {10.4230/LIPIcs.ECOOP.2015.346},
annote = {Keywords: intensional effect polymorphism, type system, hybrid typing}
}
Document
Type Inference for Place-Oblivious Objects
Abstract
In a distributed system, access to local data is much faster than access to remote data. As a help to programmers, some languages require every access to be local. A program in those languages can access remote data via first a shift of the place of computation and then a local access. To enforce this discipline, researchers have presented type systems that determine whether every access is local and every place shift is appropriate. However, those type systems fall short of handling a common programming pattern that we call place-oblivious objects. Such objects safely access other objects without knowledge of their place. In response, we present the first type system for place-oblivious objects along with an efficient inference algorithm and a proof that inference is P-complete. Our example language extends the Abadi-Cardelli object calculus with place shift and existential types, and our implementation has inferred types for some microbenchmarks.
Cite as
Riyaz Haque and Jens Palsberg. Type Inference for Place-Oblivious Objects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 371-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{haque_et_al:LIPIcs.ECOOP.2015.371,
author = {Haque, Riyaz and Palsberg, Jens},
title = {{Type Inference for Place-Oblivious Objects}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {371--395},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.371},
URN = {urn:nbn:de:0030-drops-52223},
doi = {10.4230/LIPIcs.ECOOP.2015.371},
annote = {Keywords: parallelism, locality, types}
}
Document
Asynchronous Liquid Separation Types
Abstract
We present a refinement type system for reasoning about asynchronous programs manipulating shared mutable state. Our type system guarantees the absence of races and the preservation of user-specified invariants using a combination of two ideas: refinement types and concurrent separation logic. Our type system allows precise reasoning about programs using two ingredients. First, our types are indexed by sets of resource names and the type system tracks the effect of program execution on individual heap locations and task handles. In particular, it allows making strong updates to the types of heap locations. Second, our types track ownership of shared state across concurrently posted tasks and allow reasoning about ownership transfer between tasks using permissions. We demonstrate through several examples that these two ingredients, on top of the framework of liquid types, are powerful enough to reason about correct behavior of practical, complex, asynchronous systems manipulating shared heap resources.
We have implemented type inference for our type system and have used it to prove complex invariants of asynchronous OCaml programs. We also show how the type system detects subtle concurrency bugs in a file system implementation.
Cite as
Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous Liquid Separation Types. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 396-420, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kloos_et_al:LIPIcs.ECOOP.2015.396,
author = {Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor},
title = {{Asynchronous Liquid Separation Types}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {396--420},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.396},
URN = {urn:nbn:de:0030-drops-52233},
doi = {10.4230/LIPIcs.ECOOP.2015.396},
annote = {Keywords: Liquid Types, Asynchronous Parallelism, Separation Logic, Type Systems}
}
Document
The Eureka Programming Model for Speculative Task Parallelism
Abstract
In this paper, we describe the Eureka Programming Model (EuPM) that simplifies the expression of speculative parallel tasks, and is especially well suited for parallel search and optimization applications. The focus of this work is to provide a clean semantics for, and efficiently support, such "eureka-style" computations (EuSCs) in general structured task parallel programming models. In EuSCs, a eureka event is a point in a program that announces that a result has been found. A eureka triggered by a speculative task can cause a group of related speculative tasks to become redundant, and enable them to be terminated at well-defined program points. Our approach provides a bound on the additional work done in redundant speculative tasks after such a eureka event occurs.
We identify various patterns that are supported by our eureka construct, which include search, optimization, convergence, and soft real-time deadlines. These different patterns of computations can also be safely combined or nested in the EuPM, along with regular task-parallel constructs, thereby enabling high degrees of composability and reusability. As demonstrated by our implementation, the EuPM can also be implemented efficiently. We use a cooperative runtime that uses delimited continuations to manage the termination of redundant tasks and their synchronization at join points. In contrast to current approaches, EuPM obviates the need for cumbersome manual refactoring by the programmer that may (for example) require the insertion of if checks and early return statements in every method in the call chain. Experimental results show that solutions using the EuPM simplify programmability, achieve performance comparable to hand-coded speculative task-based solutions and out-perform non-speculative task-based solutions.
Cite as
Shams Imam and Vivek Sarkar. The Eureka Programming Model for Speculative Task Parallelism. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 421-444, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{imam_et_al:LIPIcs.ECOOP.2015.421,
author = {Imam, Shams and Sarkar, Vivek},
title = {{The Eureka Programming Model for Speculative Task Parallelism}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {421--444},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.421},
URN = {urn:nbn:de:0030-drops-52327},
doi = {10.4230/LIPIcs.ECOOP.2015.421},
annote = {Keywords: Async-Finish Model, Delimited Continuations, Eureka Model, Parallel Programming, Speculative Parallelism, Task Cancellation, Task Termination}
}
Document
Cooking the Books: Formalizing JMM Implementation Recipes
Abstract
The Java Memory Model (JMM) is intended to characterize the meaning of concurrent Java programs. Because of the model's complexity, however, its definition cannot be easily transplanted within an optimizing Java compiler, even though an important rationale for its design was to ensure Java compiler optimizations are not unduly hampered because of the language's concurrency features. In response, Lea's JSR-133 Cookbook for Compiler Writers, an informal guide to realizing the principles underlying the JMM on different (relaxed-memory) platforms was developed. The goal of the cookbook is to give compiler writers a relatively simple, yet reasonably efficient, set of reordering-based recipes that satisfy JMM constraints.
In this paper, we present the first formalization of the cookbook, providing a semantic basis upon which the relationship between the recipes defined by the cookbook and the guarantees enforced by the JMM can be rigorously established. Notably, one artifact of our investigation is that the rules defined by the cookbook for compiling Java onto Power are inconsistent with the requirements of the JMM, a surprising result, and one which justifies our belief in the need for formally provable definitions to reason about sophisticated (and racy) concurrency patterns in Java, and their implementation on modern-day relaxed-memory hardware.
Our formalization enables simulation arguments between an architecture-independent intermediate representation of the kind suggested by Lea with machine abstractions for Power and x86. Moreover, we provide fixes for cookbook recipes that are inconsistent with the behaviors admitted by the target platform, and prove the correctness of these repairs.
Cite as
Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the Books: Formalizing JMM Implementation Recipes. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 445-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{petri_et_al:LIPIcs.ECOOP.2015.445,
author = {Petri, Gustavo and Vitek, Jan and Jagannathan, Suresh},
title = {{Cooking the Books: Formalizing JMM Implementation Recipes}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {445--469},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.445},
URN = {urn:nbn:de:0030-drops-52334},
doi = {10.4230/LIPIcs.ECOOP.2015.445},
annote = {Keywords: Concurrency, Java, Memory Model, Relaxed-Memory}
}
Document
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures
Abstract
Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures.
We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.
Cite as
Brijesh Dongol, John Derrick, Lindsay Groves, and Graeme Smith. Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 470-494, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dongol_et_al:LIPIcs.ECOOP.2015.470,
author = {Dongol, Brijesh and Derrick, John and Groves, Lindsay and Smith, Graeme},
title = {{Defining Correctness Conditions for Concurrent Objects in Multicore Architectures}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {470--494},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.470},
URN = {urn:nbn:de:0030-drops-52348},
doi = {10.4230/LIPIcs.ECOOP.2015.470},
annote = {Keywords: Concurrent objects, correctness, relaxed memory, verification}
}
Document
The Love/Hate Relationship with the C Preprocessor: An Interview Study
Abstract
The C preprocessor has received strong criticism in academia, among others regarding separation of concerns, error proneness, and code obfuscation, but is widely used in practice. Many (mostly academic) alternatives to the preprocessor exist, but have not been adopted in practice. Since developers continue to use the preprocessor despite all criticism and research, we ask how practitioners perceive the C preprocessor. We performed interviews with 40 developers, used grounded theory to analyze the data, and cross-validated the results with data from a survey among 202 developers, repository mining, and results from previous studies. In particular, we investigated four research questions related to why the preprocessor is still widely used in practice, common problems, alternatives, and the impact of undisciplined annotations. Our study shows that developers are aware of the criticism the C preprocessor receives, but use it nonetheless, mainly for portability and variability. Many developers indicate that they regularly face preprocessor-related problems and preprocessor-related bugs. The majority of our interviewees do not see any current C-native technologies that can entirely replace the C preprocessor. However, developers tend to mitigate problems with guidelines, even though those guidelines are not enforced consistently. We report the key insights gained from our study and discuss implications for practitioners and researchers on how to better use the C preprocessor to minimize its negative impact.
Cite as
Flávio Medeiros, Christian Kästner, Márcio Ribeiro, Sarah Nadi, and Rohit Gheyi. The Love/Hate Relationship with the C Preprocessor: An Interview Study. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 495-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{medeiros_et_al:LIPIcs.ECOOP.2015.495,
author = {Medeiros, Fl\'{a}vio and K\"{a}stner, Christian and Ribeiro, M\'{a}rcio and Nadi, Sarah and Gheyi, Rohit},
title = {{The Love/Hate Relationship with the C Preprocessor: An Interview Study}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {495--518},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.495},
URN = {urn:nbn:de:0030-drops-52350},
doi = {10.4230/LIPIcs.ECOOP.2015.495},
annote = {Keywords: C Preprocessor, CPP, Interviews, Surveys, and Grounded Theory}
}
Document
The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript
Abstract
Most popular programming languages support situations where a value of one type is converted into a value of another type without any explicit cast. Such implicit type conversions, or type coercions, are a highly controversial language feature. Proponents argue that type coercions enable writing concise code. Opponents argue that type coercions are error-prone and that they reduce the understandability of programs. This paper studies the use of type coercions in JavaScript, a language notorious for its widespread use of coercions. We dynamically analyze hundreds of programs, including real-world web applications and popular benchmark programs. We find that coercions are widely used (in 80.42% of all function executions) and that most coercions are likely to be harmless (98.85%). Furthermore, we identify a set of rarely occurring and potentially harmful coercions that safer subsets of JavaScript or future language designs may want to disallow. Our results suggest that type coercions are significantly less evil than commonly assumed and that analyses targeted at real-world JavaScript programs must consider coercions.
Cite as
Michael Pradel and Koushik Sen. The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 519-541, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{pradel_et_al:LIPIcs.ECOOP.2015.519,
author = {Pradel, Michael and Sen, Koushik},
title = {{The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {519--541},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.519},
URN = {urn:nbn:de:0030-drops-52367},
doi = {10.4230/LIPIcs.ECOOP.2015.519},
annote = {Keywords: Types, Type coercions, JavaScript, Dynamically typed languages}
}
Document
A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization
Abstract
This paper introduces a core calculus for pattern-matching in production rule languages: the Calculus for Aggregating Matching Patterns (CAMP). CAMP is expressive enough to capture modern rule languages such as JRules, including extensions for aggregation. We show how CAMP can be compiled into a nested-relational algebra (NRA), with only minimal extension. This paves the way for applying relational techniques to running rules over large stores. Furthermore, we show that NRA can also be compiled back to CAMP, using named nested-relational calculus (NNRC) as an intermediate step. We mechanize proofs of correctness, program size preservation, and type preservation of the translations using modern theorem-proving techniques. A corollary of the type preservation is that polymorphic type inference for both CAMP and NRA is NP-complete. CAMP and its correspondence to NRA provide the foundations for efficient implementations of rules languages using databases technologies.
Cite as
Avraham Shinnar, Jérôme Siméon, and Martin Hirzel. A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 542-567, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{shinnar_et_al:LIPIcs.ECOOP.2015.542,
author = {Shinnar, Avraham and Sim\'{e}on, J\'{e}r\^{o}me and Hirzel, Martin},
title = {{A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {542--567},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.542},
URN = {urn:nbn:de:0030-drops-52374},
doi = {10.4230/LIPIcs.ECOOP.2015.542},
annote = {Keywords: Rules, Pattern Matching, Aggregation, Nested Queries, Mechanization}
}
Document
Global Sequence Protocol: A Robust Abstraction for Replicated Shared State
Abstract
In the age of cloud-connected mobile devices, users want responsive apps that read and write shared data everywhere, at all times, even if network connections are slow or unavailable. The solution is to replicate data and propagate updates asynchronously. Unfortunately, such mechanisms are notoriously difficult to understand, explain, and implement.
To address these challenges, we present GSP (global sequence protocol), an operational model for replicated shared data. GSP is simple and abstract enough to serve as a mental reference model, and offers fine control over the asynchronous update propagation (update transactions, strong synchronization). It abstracts the data model and thus applies both to simple key-value stores, and complex structured data. We then show how to implement GSP robustly on a client-server architecture (masking silent client crashes, server crash-recovery failures, and arbitrary network failures) and efficiently (transmitting and storing minimal information by reducing update sequences).
Cite as
Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 568-590, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{burckhardt_et_al:LIPIcs.ECOOP.2015.568,
author = {Burckhardt, Sebastian and Leijen, Daan and Protzenko, Jonathan and F\"{a}hndrich, Manuel},
title = {{Global Sequence Protocol: A Robust Abstraction for Replicated Shared State}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {568--590},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.568},
URN = {urn:nbn:de:0030-drops-52385},
doi = {10.4230/LIPIcs.ECOOP.2015.568},
annote = {Keywords: distributed computing, eventual consistency, GSP protocol}
}
Document
Streams a la carte: Extensible Pipelines with Object Algebras
Abstract
Streaming libraries have become ubiquitous in object-oriented languages, with recent offerings in Java, C#, and Scala. All such libraries, however, suffer in terms of extensibility: there is no way to change the semantics of a streaming pipeline (e.g., to fuse filter operators, to perform computations lazily, to log operations) without changes to the library code. Furthermore, in some languages it is not even possible to add new operators (e.g., a zip operator, in addition to the standard map, filter, etc.) without changing the library.
We address such extensibility shortcomings with a new design for streaming libraries. The architecture underlying this design borrows heavily from Oliveira and Cook's object algebra solution to the expression problem, extended with a design that exposes the push/pull character of the iteration, and an encoding of higher-kinded polymorphism. We apply our design to Java and show that the addition of full extensibility is accompanied by high performance, matching or exceeding that of the original, highly-optimized Java streams library.
Cite as
Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Smaragdakis. Streams a la carte: Extensible Pipelines with Object Algebras. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 591-613, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{biboudis_et_al:LIPIcs.ECOOP.2015.591,
author = {Biboudis, Aggelos and Palladinos, Nick and Fourtounis, George and Smaragdakis, Yannis},
title = {{Streams a la carte: Extensible Pipelines with Object Algebras}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {591--613},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.591},
URN = {urn:nbn:de:0030-drops-52392},
doi = {10.4230/LIPIcs.ECOOP.2015.591},
annote = {Keywords: object algebras, streams, extensibility, domain-specific languages, expression problem, library design}
}
Document
Lightweight Support for Magic Wands in an Automatic Verifier
Abstract
Permission-based verification logics such as separation logic have led to the development of many practical verification tools over the last decade. Verifiers employ the separating conjunction A*B to elegantly handle aliasing problems, framing, race conditions, etc.
Introduced along with the separating conjunction, the magic wand connective, written A -* B, can describe hypothetical modifications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verification tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures.
In this paper, we show how to integrate support for the magic wand into an automatic verifier, requiring low specification overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specification features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques.
We have implemented our approach, and a prototype verifier is available to download, along with a collection of examples.
Cite as
Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 614-638, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{schwerhoff_et_al:LIPIcs.ECOOP.2015.614,
author = {Schwerhoff, Malte and Summers, Alexander J.},
title = {{Lightweight Support for Magic Wands in an Automatic Verifier}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {614--638},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.614},
URN = {urn:nbn:de:0030-drops-52408},
doi = {10.4230/LIPIcs.ECOOP.2015.614},
annote = {Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames}
}
Document
Modular Verification of Finite Blocking in Non-terminating Programs
Abstract
Most multi-threaded programs synchronize threads via blocking operations such as acquiring locks or joining other threads. An important correctness property of such programs is for each thread to make progress, that is, not to be blocked forever. For programs in which all threads terminate, progress essentially follows from deadlock freedom. However, for the common case that a program contains non-terminating threads such as servers or actors, deadlock freedom is not sufficient. For instance, a thread may be blocked forever by a non-terminating thread if it attempts to join that thread or to acquire a lock held by that thread.
In this paper, we present a verification technique for finite blocking in non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that unblocks another thread, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a measure to ensure that it is fulfilled within finitely many steps. Obligations may be used in specifications, which makes verification modular. We formalize our technique via an encoding into Boogie, which treats different kinds of obligations uniformly. It subsumes termination checking as a special case.
Cite as
Pontus Boström and Peter Müller. Modular Verification of Finite Blocking in Non-terminating Programs. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 639-663, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bostrom_et_al:LIPIcs.ECOOP.2015.639,
author = {Bostr\"{o}m, Pontus and M\"{u}ller, Peter},
title = {{Modular Verification of Finite Blocking in Non-terminating Programs}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {639--663},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.639},
URN = {urn:nbn:de:0030-drops-52416},
doi = {10.4230/LIPIcs.ECOOP.2015.639},
annote = {Keywords: Program verification, concurrency, liveness, progress, obligations}
}
Document
Modular Termination Verification
Abstract
We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.
Cite as
Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper. Modular Termination Verification. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 664-688, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{jacobs_et_al:LIPIcs.ECOOP.2015.664,
author = {Jacobs, Bart and Bosnacki, Dragan and Kuiper, Ruurd},
title = {{Modular Termination Verification}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {664--688},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.664},
URN = {urn:nbn:de:0030-drops-52422},
doi = {10.4230/LIPIcs.ECOOP.2015.664},
annote = {Keywords: Termination, program verification, modular verification, separation logic, well-founded relations}
}
Document
Framework for Static Analysis of PHP Applications
Abstract
Dynamic languages, such as PHP and JavaScript, are widespread and heavily used. They provide dynamic features such as dynamic type system, virtual and dynamic method calls, dynamic includes, and built-in dynamic data structures. This makes it hard to create static analyses, e.g., for automatic error discovery. Yet exploiting errors in such programs, especially in web applications, can have significant impacts. In this paper, we present static analysis framework for PHP, automatically resolving features common to dynamic languages and thus reducing the complexity of defining new static analyses. In particular, the framework enables defining value and heap analyses for dynamic languages independently and composing them automatically and soundly. We used the framework to implement static taint analysis for finding security vulnerabilities. The analysis has revealed previously unknown security problems in real application. Comparing to existing state-of-the-art analysis tools for PHP, it has found more real problems with a lower false-positive rate.
Cite as
David Hauzar and Jan Kofron. Framework for Static Analysis of PHP Applications. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 689-711, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hauzar_et_al:LIPIcs.ECOOP.2015.689,
author = {Hauzar, David and Kofron, Jan},
title = {{Framework for Static Analysis of PHP Applications}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {689--711},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.689},
URN = {urn:nbn:de:0030-drops-52435},
doi = {10.4230/LIPIcs.ECOOP.2015.689},
annote = {Keywords: Static analysis, abstract interpretation, dynamic languages, PHP, security}
}
Document
Adaptive Context-sensitive Analysis for JavaScript
Abstract
Context sensitivity is a technique to improve program analysis precision by distinguishing between function calls. A specific context-sensitive analysis is usually designed to accommodate the programming paradigm of a particular programming language. JavaScript features both the object-oriented and functional programming paradigms. Our empirical study suggests that there is no single context-sensitive analysis that always produces precise results for JavaScript applications. This observation motivated us to design an adaptive analysis, selecting a context-sensitive analysis from multiple choices for each function. Our two-staged adaptive context-sensitive analysis first extracts function characteristics from an inexpensive points-to analysis and then chooses a specialized context-sensitive analysis per function based on the heuristics. The experimental results show that our adaptive analysis achieved more precise results than any single context-sensitive analysis for several JavaScript programs in the benchmarks.
Cite as
Shiyi Wei and Barbara G. Ryder. Adaptive Context-sensitive Analysis for JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 712-734, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wei_et_al:LIPIcs.ECOOP.2015.712,
author = {Wei, Shiyi and Ryder, Barbara G.},
title = {{Adaptive Context-sensitive Analysis for JavaScript}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {712--734},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.712},
URN = {urn:nbn:de:0030-drops-52446},
doi = {10.4230/LIPIcs.ECOOP.2015.712},
annote = {Keywords: Context Sensitivity, JavaScript, Static Program Analysis}
}
Document
Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity
Abstract
The numbers and sizes of JavaScript applications are ever growing but static analysis techniques for analyzing large-scale JavaScript applications are not yet ready in a scalable and precise manner. Even when building complex software like compilers and operating systems in JavaScript, developers do not get much benefits from existing static analyzers, which suffer from mutually intermingled problems of scalability and imprecision.
In this paper, we present Loop-Sensitive Analysis (LSA) that improves the analysis scalability by enhancing the analysis precision in loops. LSA distinguishes loop iterations as many as needed by automatically choosing loop unrolling numbers during analysis. We formalize LSA in the abstract interpretation framework and prove its soundness and precision theorems using Coq. We evaluate our implementation of LSA using the analysis results of main web pages in the 5 most popular websites and those of the programs that use top 5 JavaScript libraries, and show that it outperforms the state-of-the-art JavaScript static analyzers in terms of analysis scalability. Our mechanization and implementation of LSA are both publicly available.
Cite as
Changhee Park and Sukyoung Ryu. Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 735-756, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{park_et_al:LIPIcs.ECOOP.2015.735,
author = {Park, Changhee and Ryu, Sukyoung},
title = {{Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity}},
booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)},
pages = {735--756},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-86-6},
ISSN = {1868-8969},
year = {2015},
volume = {37},
editor = {Boyland, John Tang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.735},
URN = {urn:nbn:de:0030-drops-52458},
doi = {10.4230/LIPIcs.ECOOP.2015.735},
annote = {Keywords: JavaScript, static analysis, loops}
}