# ECOOP / Presentation of Papers

European Conference on Object-Oriented Programming

# Schedule

Mon Tue Wed Thu Fri
28 Jul 29 Jul 30 Jul 31 Jul 1 Aug
FTfJP COP ECOOP
JSTools IWACO
ICOOOLPS COOMPL
PLE PLAS
Scala
PhD Symp
UPMARC Summer School ECOOP Summer School

## Wednesday

 8.15–8.30 Welcome—Tobias Wrigstad 8.30–9.30 Keynote: "Molecular Programming" —Luca Cardelli 9.30–10.00 Coffee 10.00–12.00 Technical Papers I: Analysis State-Sensitive Points-to Analysis for the Dynamic Behavior of JavaScript Objects Shiyi Wei and Barbara G. Ryder Self-Inferencing Reflection Resolution for Java Yue Li, Tian Tan, Yulei Sui and Jingling Xue Constructing Call Graphs of Scala Programs Karim Ali, Marianna Rapoport, Ondřej Lhoták, Julian Dolby and Frank Tip Finding Reference-Counting Errors in Python/C Programs with Affine Analysis Siliang Li and Gang Tan 13.30–15.00 Technical Papers II: Design Safely Composable Type-Specific Languages Cyrus Omar, Darya Kurilova, Ligia Nistor, Benjamin Chung, Alex Potanin and Jonathan Aldrich Graceful Dialects Michael Homer, Timothy Jones, James Noble, Kim B. Bruce and Andrew P. Black Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming Joshua Sunshine, James D. Herbsleb and Jonathan Aldrich 15.00–15.30 Coffee 15.30–17.00 Technical Papers III: Concurrency Reusable Concurrent Data Types Vincent Gramoli and Rachid Guerraoui TaDA: A Logic for Time and Data Abstraction Pedro da Rocha Pinto, Thomas Dinsdale-Young and Philippa Gardner Infrastructure-Free Logging and Replay of Concurrent Execution on Multiple Cores Kyu Hyung Lee, Dohyeong Kim and Xiangyu Zhang 17.15–18.45 Demonstrations (see Demos and Tutorial)

## Thursday

 8.30–9.30 Dahl-Nygaard Award Keynote: "Software Environmentalism"—Tudor Gîrba 9.30–10.00 Coffee 10.00–12.00 Technical Papers IV: Types Understanding TypeScript Gavin Bierman, Martín Abadi and Mads Torgersen Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages Davide Ancona and Andrea Corradi Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution Heather Miller, Philipp Haller and Martin Odersky Rely-Guarantee Protocols Filipe Militão, Jonathan Aldrich and Luís Caires 13.30–15.00 Technical Papers V: Implementation Stream Processing with a Spreadsheet Mandana Vaziri, Olivier Tardieu, Rodric Rabbah, Philippe Suter and Martin Hirzel Implicit Staging of EDSL Expressions: A Bridge Between Shallow and Deep Embedding Maximilian Scherr and Shigeru Chiba Babelsberg/JS - A Browser-based Implementation of an Object Constraint Language Tim Felgentreff, Alan Borning, Jens Lincke, Robert Hirschfeld, Yoshiki Ohshima, Bert Freudenberg and Robert Krahn 15.00–15.30 Coffee 15.30–16.15 Artifacts 16.15–17.15 Dahl-Nygaard Award Keynote: "How do you like your software models?"—Robert France 17.20–18.45 Demonstrations and Tutorial (see Demos and Tutorial)

## Friday

 8.30–9.30 Dahl-Nygaard Award Keynote: "A View on the Past, Present and Future of Objects"—William Cook 9.30–10.00 Coffee 10.00–12.00 Technical Papers VI: Refactoring Automated Multi-Language Artifact Binding and Refactoring between Java and DSLs used by Java Frameworks Philip Mayer and Andreas Schroeder Retargetting Legacy Browser Extensions to Modern Extension Frameworks Rezwana Karim, Mohan Dhawan and Vinod Ganapathy Capture-Avoiding and Hygienic Program Transformations Sebastian Erdweg, Tijs van der Storm and Yi Dai Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions Semih Okur, Cansu Erdogan and Danny Dig 13.30–15.00 Technical Papers VII: Javascript, PHP and Frameworks Portable and Efficient Run-time Monitoring of JavaScript Applications using Virtual Machine Layering Erick Lavoie, Bruno Dufour and Marc Feeley An Executable Formal Semantics of PHP Daniele Filaretti and Sergio Maffeis Identifying Mandatory Code for Framework Use via a Single Application Trace Naoya Nitta, Izuru Kume and Yasuhiro Takemura 15.00–15.30 Coffee 15.30–17.00 Technical Papers VIII: Parallelism Cooperative Scheduling of Parallel Tasks with General Synchronization Patterns Shams Imam and Vivek Sarkar MiCA: A Compositional Architecture for Gossip Protocols Lonnie Princehouse, Rakesh Chenchu, Zhefu Jiang, Kenneth Birman, Nate Foster and Robert Soulé Semantics of (Resilient) X10 Silvia Crafa, David Cunningham, Vijay Saraswat, Avraham Shinnar and Olivier Tardieu

## Abstracts

### Keynote: "Molecular Programming" — Luca Cardelli

Nucleic acids (DNA/RNA) encode information digitally, and are currently the only truly user-programmable' entities at the molecular scale. They can be used to manufacture nano-scale structures, to produce physical forces, to act as sensors and actuators, and to do computation in between. Eventually we will be able to use them to produce nanomaterials at the bottom end of Moore’s Law, and to interface them with biological machinery to detect and cure diseases at the cellular level under program control. Recently, computational schemes have been developed that are autonomous (run on their own power) and involve only short, easily producible, DNA strands with no other complex molecules. While simple in mechanism, these schemes are highly combinatorial and concurrent. Understanding and programming systems of this new kind requires new software technologies. Computer science has developed a large body of techniques for analyzing (modeling) and developing (engineering) complex programmable systems. Many of those techniques have a degree of mathematical generality that makes them suitable for applications to new domains. This is where we can make critical contributions: in developing and applying programming techniques (in a broad sense) that are unique to computing to other areas of science and engineering, and in particular at the interface between biology and nanotechnology.

### State-sensitive Points-to Analysis for the Dynamic Behavior of JavaScript Objects

Shiyi Wei - Virginia Tech, United States
Barbara G. Ryder - Virginia Tech, United States

JavaScript object behavior is dynamic and adheres to prototype-based inheritance. The behavior of a JavaScript object can be changed by adding and removing properties at runtime. Points-to analysis calculates the set of values a reference property or variable may have during execution. We present a novel, partially flow-sensitive, context-sensitive points-to algorithm that accurately models dynamic changes in object behavior. The algorithm represents objects by their creation sites and local property names; it tracks property updates via a new control-flow graph representation. The calling context comprises the receiver object, its local properties and prototype chain. We compare the new points-to algorithm with an existing JavaScript points-to algorithm in terms of their respective performance and accuracy on a client application. The experimental results on real JavaScript websites show that the new points-to analysis significantly improves precision, uniquely resolving on average 11% more property lookup statements.

### Self-Inferencing Reflection Resolution for Java

Yue Li - School of Computer Science and Engineering, UNSW, Australia
Tian Tan - School of Computer Science and Engineering, UNSW, Australia
Yulei Sui - School of Computer Science and Engineering, UNSW, Australia
Jingling Xue - School of Computer Science and Engineering, UNSW, Australia

Reflection has always been an obstacle both for sound and for effective under-approximate pointer analysis for Java applications. In pointer analysis tools, reflection is either ignored or handled partially, resulting in missed, important behaviors. This paper presents our findings on reflection usage in Java applications. Guided by these findings, we introduce a static reflection analysis, ELF, by exploiting a self-inferencing property inherent in reflective calls. Given a reflective call, the basic idea behind ELF is to automatically infer its targets based on the dynamic types of the arguments of its target calls and the downcasts on their returned values, if its targets cannot be already obtained from the metaobjects on which the reflective call is made. We evaluate ELF against DOOP's state-of-the-art reflection analysis using all 11 DaCapo benchmarks and two applications. ELF can make a disciplined tradeoff among soundness, precision and scalability while also discovering usually more reflective targets.

### Constructing Call Graphs of Scala Programs

Karim Ali - University of Waterloo, Canada
Marianna Rapoport - University of Waterloo, Canada
Ondřej Lhoták - University of Waterloo, Canada
Julian Dolby - IBM T.J. Watson Research Center, United States
Frank Tip - University of Waterloo, Canada

As Scala gains popularity, there is growing interest in programming tools for it. Such tools often require call graphs. However, call graph construction algorithms in the literature do not handle Scala features, such as traits and abstract type members. Applying existing call graph construction algorithms to the JVM bytecodes generated by the Scala compiler produces very imprecise results due to type information being lost during compilation. We adapt existing call graph construction algorithms, Name-Based Resolution (RA) and Rapid Type Analysis (RTA), for Scala, and present a formalization based on Featherweight Scala. We evaluate our algorithms on a collection of Scala programs. Our results show that careful handling of complex Scala constructs greatly helps precision and that our most precise analysis generates call graphs with 1.1-3.7 times fewer nodes and 1.5-18.7 times fewer edges than a bytecode-based RTA analysis.

### Finding Reference-Counting Errors in Python/C Programs with Affine Analysis

Siliang Li - Lehigh University, United States
Gang Tan - Lehigh University, United States

Python is a popular programming language that uses reference counting to manage heap objects. Python also has a Foreign Function Interface (FFI) that allows Python extension modules to be written in native code such as C and C++. Native code, however, is outside Python's system of memory management; therefore extension programmers are responsible for making sure these objects are reference counted correctly. This is an error prone process when code becomes complex. In this paper, we propose Pungi, a system that statically checks whether Python objects' reference counts are adjusted correctly in Python/C interface code. Pungi transforms Python/C interface code into affine programs with respect to our proposed abstractions of reference counts. Our system performs static analysis on transformed affine programs and reports possible reference counting errors. Our prototype implementation found over 150 errors in a set of Python/C programs.

### Safely Composable Type-Specific Languages

Cyrus Omar - Carnegie Mellon University, United States
Darya Kurilova - Carnegie Mellon University, United States
Ligia Nistor - Carnegie Mellon University, United States
Benjamin Chung - Carnegie Mellon University, United States
Alex Potanin - Victoria University of Wellington, New Zealand
Jonathan Aldrich - Carnegie Mellon University, United States

Programming languages often include specialized syntax for common datatypes and some also build in support for specific specialized datatypes (e.g. regular expressions), but user-defined types must use general-purpose syntax. Frustration with this causes developers to turn to strings, leading to correctness, performance, security, and usability issues. Allowing library providers to extend a language with new syntax could help address these issues. Unfortunately, prior mechanisms either limit expressiveness or are not safely composable: individually unambiguous extensions can lead to ambiguities when used together. We introduce type-specific languages (TSLs): logic associated with a type that determines how the bodies of generic literals, able to contain arbitrary syntax, are parsed and elaborated, hygienically. A TSL is invoked only when a literal appears where a term of its type is expected, guaranteeing non-interference. We give evidence supporting the applicability of TSLs and formally specify them with a bidirectionally typed elaboration semantics for Wyvern.

### Graceful Dialects

Michael Homer - Victoria University of Wellington, New Zealand
Timothy Jones - Victoria University of Wellington, New Zealand
James Noble - Victoria University of Wellington, New Zealand
Kim B. Bruce - Pomona College, United States
Andrew P. Black - Portland State University, United States

Programming languages are enormously diverse, both in their essential concepts and in their accidental aspects. This creates a problem when teaching programming. To let students experience the diversity of essential concepts, the students must also be exposed to an overwhelming variety of accidental and irrelevant detail: the accidental differences between the languages are likely to obscure the teaching point. The dialect system of the Grace programming language allows instructors to tailor and vary the language to suit their courses, while staying within the same stylistic, syntactic and semantic framework, as well as permitting authors to define advanced internal domain-specific languages. The dialect system achieves this power though a combination of well-known language features: lexical nesting, lambda expressions, multi-part method names, optional typing, and pluggable checkers. Grace's approach to dialects is validated by a series of case studies, including both extensions and restrictions of the base language.

### Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming

Joshua Sunshine - Carnegie Mellon University, United States
James D. Herbsleb - Carnegie Mellon University, United States
Jonathan Aldrich - Carnegie Mellon University, United States

Application Programming Interfaces (APIs) often define object protocols. Objects with protocols have a finite number of states and in each state a different set of method calls is valid. Many researchers have developed protocol verification tools because protocols are notoriously difficult to follow correctly. However, recent research suggests that a major challenge for API protocol programmers is effectively searching the state space. Verification is an ineffective guide for this kind of search. In this paper we instead propose Plaiddoc, which is like Javadoc except it organizes methods by state instead of by class and it includes explicit state transitions, state-based type specifications, and rich state relationships. We compare Plaiddoc to a Javadoc control in a between-subjects laboratory experiment. We find that Plaiddoc participants complete state search tasks in significantly less time and with significantly fewer errors than Javadoc participants.

### Reusable Concurrent Data Types

Vincent Gramoli - NICTA and University of Sydney, Australia
Rachid Guerraoui - EPFL, Switzerland

This paper contributes to address the fundamental challenge of building Concurrent Data Types (CDT) that are reusable and scalable at the same time. We do so by proposing the abstraction of Polymorphic Transactions (PT): a new programming abstraction that offers different compatible transactions that can run concurrently in the same application. We outline the commonality of the problem in various object-oriented languages and implement PT and a reusable package in Java. With PT, annotating sequential ADTs guarantee novice programmers to obtain an atomic and deadlock-free CDT and let an advanced programmer leverage the application semantics to get higher performance. We compare our polymorphic synchronization against transaction-based, lock-based and lock-free synchronizations on SPARC and x86-64 architectures and we integrate our methodology to a travel reservation benchmark. Although our reusable CDTs are sometimes less efficient than non-composable handcrafted CDTs from the JDK, they outperform all reusable Java CDTs.

### TaDA: A Logic for Time and Data Abstraction

Pedro da Rocha Pinto - Imperial College London, United Kingdom
Thomas Dinsdale-Young - Aarhus University, Denmark
Philippa Gardner - Imperial College London, United Kingdom

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources. We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.

### Infrastructure-Free Logging and Replay of Concurrent Execution on Multiple Cores

Kyu Hyung Lee - Purdue University, United States
Dohyeong Kim - Purdue University, United States
Xiangyu Zhang - Purdue University, United States

We develop a logging and replay technique for real concurrent execution on multiple cores. Our technique directly works on binaries and does not require any hardware or complex software infrastructure support. We focus on minimizing logging overhead as it only logs a subset of system calls and thread spawns. Replay is on a single core. During replay, our technique first tries to follow only the event order in the log. However, due to schedule differences, replay may fail. An exploration process is then triggered to search for a schedule that allows the replay to make progress. Exploration is performed within a window preceding the point of replay failure. During exploration, our technique first tries to reorder synchronized blocks. If that does not lead to progress, it further reorders shared variable accesses. The exploration is facilitated by a sophisticated caching mechanism. Our experiments on real world programs and real workload show that the proposed technique has very low logging overhead (2.6% on average) and fast schedule reconstruction.

### Keynote: "Software Environmentalism" — Tudor Gîrba

Software systems get larger and larger, and they are being created at an ever increasing rate. While this might appear to be great, we are facing a significant long run problem as we need to assess and recycle them. In fact, the problem is already here: Engineers spend as much as half of the effort on understanding software systems to figure out how to approach subsequent evolutions and the percentage grows with the size and age of the system. In essence, software engineering is more about dealing with existing systems as it is about building systems. Reverse engineering and program comprehension are established areas that deal with the problem of approaching existing systems. However, in spite of several decades of research and many proposed approaches, the state of practice still shows that, to a large extent, engineers rely on manual code reading as the preferred means to understand the system. The main reason for it is that most existing approaches tend to be generic and ignore the context of systems. This situation does not scale and it should not perpetuate given the large costs associated with it. We cannot continue to let systems loose in the wild without any concern for how we will deal with them at a later time. Two decades ago, Richard Gabriel coined the idea of software habitability. Indeed, given that engineers spend a significant part of their active life inside software systems, it is desirable for that system to be suitable for humans to live there. We go further and introduce the concept of software environmentalism as a systematic discipline to pursue and achieve habitability. Engineers have the right to build upon assessable systems and have the responsibility of producing assessable systems. For example, even if code has often a text shape, it is not text. The same applies to logs and anything else related to a software system. It's all data, and data is best dealt with through tools. No system should get away without dedicated tools that help us take it apart and recycle it effectively. For example, every significant object in a system should be allowed to have dedicated inspectors to reveal its various facets and interactions, and every significant library should come with dedicated debugging possibilities. Who should build those tools? Engineers. This implies that they have to be empowered to do it, and that the cost of building those tools is manageable. We need to go back to the drawing board to (1) construct moldable development environments that help us drill into the context of systems effectively, (2) reinvent our underlying languages and technologies so that we can build assessable systems all the way down, and (3) reeducate our perception of what software engineering is.

### Understanding TypeScript

Gavin Bierman - Oracle, United Kingdom
Martín Abadi - Microsoft Research, United States
Mads Torgersen - Microsoft, United States

TypeScript is an extension of JavaScript intended to enable easier development of large-scale JavaScript applications. While every JavaScript program is a TypeScript program, TypeScript offers a module system, classes, interfaces, and a rich gradual type system. The intention is that TypeScript provides a smooth transition for JavaScript programmers---well-established JavaScript programming idioms are supported without any major rewriting or annotations. One interesting consequence is that the TypeScript type system is not statically sound by design. The goal of this paper is to capture the essence of TypeScript by giving a precise definition of this type system on a core set of constructs of the language. Our main contribution, beyond the familiar advantages of a robust, mathematical formalization, is a refactoring into a safe inner fragment and an additional layer of unsafe rules.

### Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages

Davide Ancona - Universitá di Genova, Italy
Andrea Corradi - Universitá di Genova, Italy

Structural subtyping is an important notion for effective static type analysis; it can be defined either axiomatically by a collection of subtyping rules, or by means of set inclusion between type interpretations, following the more intuitive approach of semantic subtyping, which allows simpler proofs of the expected properties of the subtyping relation. In object-oriented programming, recursive types are typically interpreted inductively; however, cyclic objects can be represented more precisely by coinductive types. We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming, and develop and implement a sound and complete top-down direct and effective algorithm for deciding it. To our knowledge, this is the first proposal for a sound and complete top-down direct algorithm for semantic subtyping between coinductive types.

### Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Heather Miller - EPFL, Switzerland
Philipp Haller - Typesafe, Inc., Switzerland
Martin Odersky - EPFL, Switzerland

Functional programming is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint (immutable data transformed by function application) has even lead to a number of object-oriented programming languages adopting functional features such as lambdas and thereby function closures. However, despite this established viewpoint of FP as an enabler, reliably distributing closures over a network, or using them in concurrent environments nonetheless remains a challenge across FP and OO languages. This paper takes a step towards more principled distributed and concurrent programming by introducing a new closure-like abstraction and type system, called spores, that can guarantee closures to be serializable, thread-safe, or even have custom user-defined properties. Crucially, our system is based on the principle of encoding type information corresponding to captured variables in the type of a spore. We prove our type system sound, implement our approach for Scala, and show the power of these guarantees through a case analysis of real-world distributed/concurrent frameworks that this safe foundation for migratable closures facilitates.

### Rely-Guarantee Protocols

Filipe Militão - Carnegie Mellon University & Universidade Nova Lisboa, Portugal
Jonathan Aldrich - Carnegie Mellon University, United States
Luís Caires - Universidade Nova Lisboa, Portugal

The use of shared mutable state, commonly seen in object-oriented systems, is often problematic due to the potential conflicting interactions between aliases to the same state. We present a substructural type system outfitted with a novel lightweight interference control mechanism, rely-guarantee protocols, that enables controlled aliasing of shared resources. By assigning each alias separate roles, encoded in a novel protocol abstraction in the spirit of rely-guarantee reasoning, our type system ensures that challenging uses of shared state will never interfere in an unsafe fashion. In particular, rely-guarantee protocols ensure that each alias will never observe an unexpected value, or type, when inspecting shared memory regardless of how the changes to that shared state (originating from potentially unknown program contexts) are interleaved at run-time.

### Stream Processing with a Spreadsheet

Mandana Vaziri - IBM T.J. Watson Research Center, United States
Olivier Tardieu - IBM T.J. Watson Research Center, United States
Rodric Rabbah - IBM T.J. Watson Research Center, United States
Philippe Suter - IBM T.J. Watson Research Center, United States
Martin Hirzel - IBM T.J. Watson Research Center, United States

Continuous data streams are ubiquitous and represent such a high volume of data that they cannot be stored to disk, yet it is often crucial for them to be analyzed in real-time. Stream processing is a programming paradigm that processes these immediately, and enables continuous analytics. Our objective is to make it easier for analysts, with little programming experience, to develop continuous analytics applications directly. We propose enhancing a spreadsheet, a pervasive tool, to obtain a programming platform for stream processing. We present the design and implementation of an enhanced spreadsheet that enables visualizing live streams, live programming to compute new streams, and exporting computations to be run on a server where they can be shared with other users, and persisted beyond the life of the spreadsheet. We formalize our core language, and present case studies that cover a range of stream processing applications.

### Implicit Staging of EDSL Expressions: A Bridge between Shallow and Deep Embedding

Maximilian Scherr - The University of Tokyo, Japan
Shigeru Chiba - The University of Tokyo, Japan

Common implementation approaches for embedding DSLs in general-purpose host languages force developers to choose between a shallow (single-staged) embedding which offers seamless usage, but limits DSL developers, or a deep (multi-staged) embedding which offers freedom to optimize at will, but is less seamless to use and incurs additional runtime overhead. We propose a metaprogrammatic approach for extracting domain-specific programs from user programs for custom processing. This allows for similar optimization options as deep embedding, while still allowing for seamless embedded usage. We have implemented a simplified instance of this approach in a prototype framework for Java-embedded EDSL expressions, which relies on load-time reflection for improved deployability and usability.

### Babelsberg/JS - A Browser-based Implementation of an Object Constraint Language

Tim Felgentreff - Hasso Plattner Institute, Germany
Alan Borning - University of Washington, United States
Robert Hirschfeld - Hasso Plattner Institute, Germany
Jens Lincke - Hasso Plattner Institute, Germany
Yoshiki Ohshima - Viewpoints Research Institute, Japan
Bert Freudenberg - Viewpoints Research Institute, Germany
Robert Krahn - Communications Design Group, SAP Labs, United States

Constraints provide a useful technique for ensuring that desired properties hold in an application. They have been used in a wide range of applications, including graphical layout, simulation, and scheduling. We describe the design and implementation of an Object Constraint Programming language, a language that cleanly integrates constraints with an object-oriented language in a way that respects encapsulation and OO programming techniques, and that runs in browser-based applications. Prior work on OCP has relied on modifying the underlying VM, but that is not an option for web-based applications, which are increasingly prominent. In this paper, we demonstrate a language, Babelsberg/JS, a number of its applications, and provide performance measurements. Programs without constraints run at the same speed as pure JavaScript, while programs with constraints still run eï¬ƒciently. Our design and implementation incorporate incremental re-solving as well as a cooperating solvers architecture that allows multiple solvers to work together.

### Keynote: "How do you like your software models?" — Robert France

The terms Model Driven Development/Engineering (MDD/E) are typically used to describe software development approaches in which models of software systems play a pivotal role. In the past I have argued that good support for software modeling is essential to bringing software development closer to an engineering endeavor. As in other engineering disciplines, modeling should be an integral part of software processes that tackle the very challenging problems associated with the creation and evolution of complex software-based systems. While MDD/E research targets important software development problems, the results have not yet led to widespread effective use of software modeling practices. While the wicked problems associated with the development of complex systems is a factor, another is a lack of attention to the issue of fitness-for-purpose with respect to modeling methods and tools. The state-of-the-art leaves some practitioners with the impression that modeling techniques add significant accidental complexity to the software development process. In this talk, I argue that there is a need to take a more empathetic approach to the design of tools and methods. In {\em empathetic design}, methodologists and tool developers actively consider and evaluate how their tools and methods fit with how modeling practitioners across a wide skill spectrum (expert, average, novice modelers) work. This should lead to methods and tools that are fit-for-purpose, and open the door for more widespread use of software modeling techniques.

### Keynote: "A View on the Past, Present and Future of Objects" — William Cook

Object-oriented programming has always been somewhat mysterious. It has been realized in a fairly pure form in several ways, in Smalltalk, Beta, COM, and SELF. There are several theories (three in Pierce's Types and Programming Languages, and more given by Abadi \& Cardelli, Bruce and others). Many partial and failed theories have been published. Most programming languages today are hybrids of objects with other styles of programming. Yet many programming language researchers believe that objects are somehow evil. And still we are experimenting with different forms and inventing new ideas on top of objects. Objects have won' as far as I am concerned, or at least objects have won a place at the table. So where do we go from here? While there are many low-level improvements that can be made, it is a reasonable time to consider the big picture. One of the original views of objects was as a form of modeling. Modeling has taken on a life of its own, but has not been as successful as objects were. In this talk I will sketch out a path forward for objects and modeling to work together.

### Automated Multi-Language Artifact Binding and Rename Refactoring between Java and DSLs used by Java Frameworks

Philip Mayer - Programming & Software Engineering Group, LMU Munich, Germany
Andreas Schroeder - Programming & Software Engineering Group, LMU Munich, Germany

Developing non-trivial software applications involves using multiple programming languages. Although each language is used to describe a particular aspect of the system, artifacts defined inside those languages reference each other across language boundaries; such references are often only resolved at runtime. However, it is important for developers to be aware of these references during development time for programming understanding, bug prevention, and refactoring. In this work, we report on a) an approach and tool for automatically identifying multi-language relevant artifacts, finding references between artifacts in different languages, and (rename-) refactoring them, and b) on an experimental evaluation of the approach on seven open-source case studies which use a total of six languages found in three frameworks. As our main result, we provide insights into the incidence of multi-language bindings in the case studies as well as the feasibility of automated multi-language rename refactorings.

### Retargetting Legacy Browser Extensions to Modern Extension Frameworks

Rezwana Karim - Rutgers University, United States
Mohan Dhawan - IBM Research, Delhi, India, India
Vinod Ganapathy - Rutgers University, United States

Most modern Web browsers expose a rich API that allows third-party extensions to access privileged browser objects. However, this API can also be misused by attacks directed against vulnerable extensions. Web browser vendors have therefore recently developed new frameworks aimed at better isolating extensions while still allowing access to privileged browser state. Examples of such frameworks include the Google Chrome extension architecture and the Mozilla Jetpack extension framework. We present Morpheus, a tool to port legacy browser extensions to these new frameworks. Specifically, Morpheus targets legacy extensions for the Mozilla Firefox browser, and ports them to the Jetpack framework. We describe the key techniques used by Morpheus to analyze and transform legacy extensions so that they conform to the constraints imposed by Jetpack and simplify runtime policy enforcement. Finally, we present an experimental evaluation of Morpheus by applying it to port 52 legacy Firefox extensions to the Jetpack framework.

### Capture-Avoiding and Hygienic Program Transformations

Sebastian Erdweg - TU Darmstadt, Germany
Tijs van der Storm - CWI, Amsterdam, The Netherlands
Yi Dai - University of Marburg, Germany

Program transformations in terms of abstract syntax trees compromise referential integrity by introducing variable capture. Variable capture occurs when in the generated program a variable declaration accidentally shadows the intended target of a variable reference. Existing transformation systems either do not guarantee the avoidance of variable capture or impair the implementation of transformations. We present an algorithm called name-fix that automatically eliminates variable capture from a generated program by systematically renaming variables. name-fix is guided by a graph representation of the binding structure of a program, and requires name-resolution algorithms for the source language and the target language of a transformation. name-fix is generic and works for arbitrary transformations in any transformation system that supports origin tracking for names. We verify the correctness of name-fix and identify an interesting class of transformations for which name-fix provides hygiene. We demonstrate the applicability of name-fix for implementing capture-avoiding substitution, inlinig, lambda lifting, and compilers for two domain-specific languages.

### Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions

Semih Okur - University of Illinois at Urbana-Champaign, United States
Cansu Erdogan - University of Illinois at Urbana-Champaign, United States
Danny Dig - Oregon State University, United States

Parallel libraries continuously evolve from low-level to higher-level abstractions. However, developers are not up-to-date with these higher-level abstractions, thus their parallel code might be hard to read, slow, and unscalable. Using a corpus of 880 open-source C# applications, we found that developers still use the old Thread and ThreadPool abstractions in 62% of the cases when they use parallel abstractions. Converting code to higher-level abstractions is (i) tedious and (ii) error-prone. We present two automated migration tools, Taskifier and Simplifier that work for C# code. The first tool transforms old style Thread and ThreadPool abstractions to Task abstractions. The second tool transforms code with Task abstractions into higher-level design patterns. Using our code corpus, we have applied these tools 3026 and 405 times, respectively. Our empirical evaluation shows that the tools (i) are highly applicable, (ii) reduce the code bloat, (iii) are much safer than manual transformations.

### Portable and Efficient Run-time Monitoring of JavaScript Applications using Virtual Machine Layering

Erick Lavoie - McGill University, Canada
Bruno Dufour - Université de Montréal, Canada
Marc Feeley - Université de Montréal, Canada

Run-time monitoring of JavaScript applications is typically achieved either by instrumenting a browser's virtual machine, usually degrading performance to the level of a simple interpreter, or through complex ad hoc source-to-source transformations. This paper reports on an experiment in layering a portable JS VM on the host VM to expose implementation-level operations that can then be redefined at run-time to monitor an application execution. Our prototype, Photon, exposes object operations and function calls through a meta-object protocol. In order to limit the performance overhead, a dynamic translation of the client program selectively modifies source elements and run-time feedback optimizes monitoring operations. Photon introduces a 4.7 to 191 slowdown when executing benchmarks on popular web browsers. Compared to the Firefox interpreter, it is between 5.5 slower and 7 faster, showing the layering approach is competitive with the instrumentation of a browser VM while being faster and simpler than other source-to-source transformations.

### An Executable Formal Semantics of PHP

Daniele Filaretti - Imperial College London, United Kingdom
Sergio Maffeis - Imperial College London, United Kingdom

PHP is among the most used languages for server-side scripting. Although substantial effort has been spent on the problem of automatically analysing PHP code, vulnerabilities remain pervasive in web applications, and analysis tools do not provide any formal guarantees of soundness or coverage. This is partly due to the lack of a precise specification of the language, which is highly dynamic and often exhibits subtle behaviour. We present the first formal semantics for a substantial core of PHP, based on the official documentation and experiments with the Zend reference implementation. Our semantics is executable, and is validated by testing it against the Zend test suite. We define the semantics of PHP in a term-rewriting framework which supports LTL model checking and symbolic execution. As a demonstration, we extend LTL with predicates for the verification of PHP programs, and analyse two common PHP functions.

### Identifying Mandatory Code for Framework Use via a Single Application Trace

Naoya Nitta - Graduate School of Natural ScienceKonan University, Japan
Izuru Kume - Graduate School of Information Science, Nara Institute of Science and Technology, Japan
Yasuhiro Takemura - Department of Character Creative Arts, Osaka University of Arts, Japan

Application frameworks allow application developers to effectively reuse both designs and implementations which frequently appear in their intended domains. However, when using a framework with large scale APIs, its usage to implement an application-specific behavior tends to be complicated. Thus, in practice, application developers use existing sample application code as references for their development, but the task to locate the parts which are related to their application usually becomes a burden. To address this problem, in this paper, we characterize the problem as a kind of dynamic flow analysis problem, and based on the characterization, we present a method to automatically identify the mandatory code for the framework use using only a single sample application's trace. We have conducted case studies with several real-world frameworks to validate our method and the results indicate that the method is suitable to extract the mandatory framework usage.

### Cooperative Scheduling of Parallel Tasks with General Synchronization Patterns

Shams Imam - Rice University, United States
Vivek Sarkar - Rice University, United States

### MiCA: A Compositional Architecture for Gossip Protocols

Lonnie Princehouse - Cornell University, United States
Rakesh Chenchu - Cornell University, United States
Zhefu Jiang - Cornell University, United States
Kenneth Birman - Cornell University, United States
Nate Foster - Cornell University, United States
Robert Soulé - University of Lugano, Switzerland

The developers of today's cloud computing systems are expected to not only create applications that scale well, but also to create management services that will monitor run-time conditions and intervene to address problems as conditions evolve. Management tasks are generally not performance intensive, but robustness is critical: when a large system becomes unstable, the management infrastructure must remain reliable, predictable, and fault-tolerant. A wide range of management tasks can be expressed as gossip protocols, where nodes in the system periodically interact with random peers and exchange information about their respective states. MiCA is a new system for building gossip-based management tools that are highly resistant to disruptions and make efficient use of system resources. MiCA provides abstractions custom-tailored for gossip, a collection of composition operators that facilitates constructing sophisticated protocols in a modular style, and automatic optimizations that can often greatly reduce the number and size of messages used.

### Semantics of (Resilient) X10

Silvia Crafa - University of Padova, Italy
David Cunningham - Google, Inc, United States
Vijay Saraswat - IBM TJ Watson Research Center, United States
Avraham Shinnar - IBM TJ Watson Research Center, United States
Olivier Tardieu - IBM TJ Watson Research Center, United States

We present a formal small-step structural operational semantics for a large fragment of X10, unifying past work. The fragment covers multiple places, mutable objects on the heap, sequencing, try/catch, async, finish, and at constructs. This model accurately captures the behavior of a large class of concurrent, multi-place X10 programs. Further, we introduce a formal model of resilience in X10. During execution of an X10 program, a place may fail for many reasons. Resilient X10 permits the program to continue executing, losing the data at the failed place, and most of the control state, and repairing the global control state in such a way that key semantic principles hold, the Happens Before Invariance Principle, and the Exception Masking Principle. These principles permit an X10 programmer to write clean code that continues to work in the presence of place failure. The given semantics have additionally been mechanized in Coq.