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 Self-Inferencing Reflection Resolution for Java Constructing Call Graphs of Scala Programs Finding Reference-Counting Errors in Python/C Programs with Affine Analysis |
| 13.30–15.00 |
Technical Papers II: Design Safely Composable Type-Specific Languages Graceful Dialects Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming |
| 15.00–15.30 | Coffee |
| 15.30–17.00 | Technical Papers III: Concurrency Reusable Concurrent Data Types TaDA: A Logic for Time and Data Abstraction Infrastructure-Free Logging and Replay of Concurrent Execution on Multiple Cores |
| 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 Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution Rely-Guarantee Protocols |
| 13.30–15.00 | Technical Papers V: Implementation Stream Processing with a Spreadsheet Implicit Staging of EDSL Expressions: A Bridge Between Shallow and Deep Embedding Babelsberg/JS - A Browser-based Implementation of an Object Constraint Language |
| 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
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 StatesBarbara 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 StatesGang 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 StatesJames 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, AustraliaRachid 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 KingdomThomas 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 StatesDohyeong 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 KingdomMartí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, SwitzerlandPhilipp 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, PortugalJonathan 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, JapanShigeru 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 efficiently. 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 StatesMohan 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 StatesCansu 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, JapanIzuru 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 StatesVivek Sarkar - Rice University, United States
In this paper, we address the problem of scheduling parallel tasks with general synchronization patterns using a cooperative runtime. Current implementations for task-parallel programming models provide efficient support for fork-join parallelism, but are unable to efficiently support more general synchronization patterns such as locks, futures, barriers and phasers. We propose a novel approach to addressing this challenge based on cooperative scheduling with one-shot delimited continuations (OSDeConts) and event-driven controls (EDCs). The use of OSDeConts enables the runtime to suspend a task at any point (thereby enabling the task's worker to switch to another task) whereas other runtimes may have forced the task's worker to be blocked. The use of EDCs ensures that identification of suspended tasks that are ready to be resumed can be performed efficiently. Furthermore, our approach is more efficient than schedulers that spawn additional worker threads to compensate for blocked worker threads. We have implemented our cooperative runtime in Habanero-Java (HJ), an explicitly parallel language with a large variety of synchronization patterns. The OSDeCont and EDC primitives are used to implement a wide range of synchronization constructs, including those where a task may trigger the enablement of multiple suspended tasks (as in futures, barriers and phasers). In contrast, current task-parallel runtimes and schedulers for the fork-join model (including schedulers for the Cilk language) focus on the case where only one continuation is enabled by an event (typically, the termination of the last child/descendant task in a join scope). Our experimental results show that the HJ cooperative runtime delivers significant improvements in performance and memory utilization on various benchmarks using future and phaser constructs, relative to a thread-blocking runtime system while using the same underlying work-stealing task scheduler.
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.
Diamond Sponsors
Gold Sponsors
Silver Sponsors
Bronze Sponsors
Organisers
In Cooperation With
Social:
