title: Application-Only Call Graph Construction

authors:
Karim Ali
Ondrej Lhoták


venue: ecoop

title: Java Wildcards Meet Definition-Site Variance

authors:
John Altidor
Christoph Reichenbach
Yannis Smaragdakis


title: Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics


title: Pause 'n' Play: Formalizing Asynchronous C#

authors:
Gavin M. Bierman
Claudio V. Russo
Geoffrey Mainland
Erik Meijer
Mads Torgersen


title: Magda: A New Language for Modularity

authors:
Viviana Bono
Jarek Kusmierek
Mauro Mulatero


title: Cloud Types for Eventual Consistency

authors:
Sebastian Burckhardt
Manuel Fähndrich
Daan Leijen
Benjamin P. Wood


title: Scalable Flow-Sensitive Pointer Analysis for Java with Strong Updates

authors:
Arnab De
Deepak D'Souza


title: Enhancing JavaScript with Transactions

authors:
Mohan Dhawan
Chung-chieh Shan
Vinod Ganapathy


title: Verification of Snapshot Isolation in Transactional Memory Java Programs

authors:
Ricardo J. Dias
Dino Distefano
João Costa Seco
João Lourenço


title: McSAF: A Static Analysis Framework for MATLAB

authors:
Jesse Doherty
Laurie J. Hendren


title: Static Sessional Dataflow

authors:
Dominic Duggan
Jianhua Yao


title: Program Sliding


title: Smaller Footprint for Java Collections

authors:
Joseph Gil
Yuval Shimron


title: Lock Inference in the Presence of Large Libraries

authors:
Khilan Gudka
Tim Harris
Susan Eisenbach


title: Inference and Checking of Object Ownership

authors:
Wei Huang
Werner Dietl
Ana L. Milanova
Michael D. Ernst


title: An Analysis of the Mozilla Jetpack Extension Framework

authors:
Rezwana Karim
Mohan Dhawan
Vinod Ganapathy
Chung-chieh Shan


title: JavaScript as an Embedded DSL

authors:
Grzegorz Kossakowski
Nada Amin
Tiark Rompf
Martin Odersky


title: Marco: Safe, Expressive Macros for Any Language

authors:
Byeongcheol Lee
Robert Grimm
Martin Hirzel
Kathryn S. McKinley


title: Evaluating the Design of the R Language - Objects and Functions for Data Analysis

authors:
Floréal Morandat
Brandon Hill
Leo Osvald
Jan Vitek


title: Is It Dangerous to Use Version Control Histories to Study Source Code Evolution?

authors:
Stas Negara
Mohsen Vakilian
Nicholas Chen
Ralph E. Johnson
Danny Dig


title: When Compilers Are Mirrors


title: Extensibility for the Masses - Practical Extensibility with Object Algebras

authors:
Bruno C. d. S. Oliveira
William R. Cook


title: Multiple Aggregate Entry Points for Ownership Types

authors:
Johan Östlund
Tobias Wrigstad


title: PQL: A Purely-Declarative Java Extension for Parallel Programming

authors:
Christoph Reichenbach
Yannis Smaragdakis
Neil Immerman


title: Extensions during Software Evolution: Do Objects Meet Their Promise?

authors:
Romain Robbes
David Röthlisberger
Éric Tanter


title: Lightweight Polymorphic Effects

authors:
Lukas Rytz
Martin Odersky
Philipp Haller


title: Correlation Tracking for Points-To Analysis of JavaScript

authors:
Manu Sridharan
Julian Dolby
Satish Chandra
Max Schäfer
Frank Tip


title: Constraint-Based Refactoring with Foresight

authors:
Friedrich Steimann
Jens von Pilgrim


title: Practical Permissions for Race-Free Parallelism

authors:
Edwin M. Westbrook
Jisheng Zhao
Zoran Budimlic
Vivek Sarkar


title: Structured Aliasing


title: Static Detection of Loop-Invariant Data Structures

authors:
Guoqing Xu
Dacong Yan
Atanas Rountev


title: Object Initialization in X10

authors:
Yoav Zibin
David Cunningham
Igor Peshansky
Vijay A. Saraswat


title: Averroes: Whole-Program Analysis without the Whole Program

authors:
Karim Ali
Ondrej Lhoták


title: Enabling Modularity and Re-use in Dynamic Program Analysis Tools for the Java Virtual Machine

authors:
Danilo Ansaloni
Stephen Kell
Yudi Zheng
Lubomír Bulej
Walter Binder
Petr Tuma


title: The Shape of Things to Run - Compiling Complex Stream Graphs to Reconfigurable Hardware in Lime

authors:
Joshua S. Auerbach
David F. Bacon
Perry Cheng
Steve Fink
Rodric M. Rabbah


title: QUIC Graphs: Relational Invariant Generation for Containers

authors:
Arlen Cox
Bor-Yuh Evan Chang
Sriram Sankaranarayanan


title: Trustworthy Proxies - Virtualizing Objects with Invariants

authors:
Tom Van Cutsem
Mark S. Miller


title: RedCard: Redundant Check Elimination for Dynamic Race Detectors

authors:
Cormac Flanagan
Stephen N. Freund


title: Implementing Federated Object Systems

authors:
Tobias Freudenreich
Patrick Eugster
Sebastian Frischbier
Stefan Appel
Alejandro P. Buchmann


title: Systematic Testing of Refactoring Engines on Real Software Projects

authors:
Milos Gligoric
Farnaz Behrang
Yilong Li
Jeffrey Overbey
Munawar Hafiz
Darko Marinov


title: Java UI : Effects for Controlling UI Object Access

authors:
Colin S. Gordon
Werner Dietl
Michael D. Ernst
Dan Grossman


title: Ownership-Based Isolation for Concurrent Actors on Multi-core Machines

authors:
Olivier Gruber
Fabienne Boyer


title: Is This a Bug or an Obsolete Test?

authors:
Dan Hao
Tian Lan
Hongyu Zhang
Chao Guo
Lu Zhang


title: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions

authors:
Stefan Heule
Ioannis T. Kassios
Peter Müller
Alexander J. Summers


title: Combining Form and Function: Static Types for JQuery Programs

authors:
Benjamin S. Lerner
Liam Elberty
Jincheng Li
Shriram Krishnamurthi


title: Higher-Order Reactive Programming with Incremental Lists

authors:
Ingo Maier
Martin Odersky


title: A Comparative Study of Manual and Automated Refactorings

authors:
Stas Negara
Nicholas Chen
Mohsen Vakilian
Ralph E. Johnson
Danny Dig


title: Feature-Oriented Programming with Object Algebras

authors:
Bruno C. d. S. Oliveira
Tijs van der Storm
Alex Loh
William R. Cook


title: The Billion-Dollar Fix - Safe Modular Circular Initialisation with Placeholders and Placeholder Types

authors:
Marco Servetto
Julian Mackay
Alex Potanin
James Noble


title: Detecting Refactored Clones

authors:
Mati Shomrat
Yishai A. Feldman


title: Composition and Reuse with Compiled Domain-Specific Languages

authors:
Arvind K. Sujeeth
Tiark Rompf
Kevin J. Brown
HyoukJoong Lee
Hassan Chafi
Victoria Popic
Michael Wu
Aleksandar Prokopec
Vojin Jovanovic
Martin Odersky
Kunle Olukotun


title: A Formal Semantics for Isorecursive and Equirecursive State Abstractions

authors:
Alexander J. Summers
Sophia Drossopoulou


title: Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library

authors:
Kasper Svendsen
Lars Birkedal
Matthew J. Parkinson


title: Why Do Scala Developers Mix the Actor Model with other Concurrency Models?

authors:
Samira Tasharofi
Peter Dinges
Ralph E. Johnson


title: What Programmers Do with Inheritance in Java

authors:
Ewan D. Tempero
Hong Yul Yang
James Noble


title: Reducing Lookups for Invariant Checking

authors:
Jakob G. Thomsen
Christian Clausen
Kristoffer Just Andersen
John Danaher
Erik Ernst


title: Really Automatic Scalable Object-Oriented Reengineering

authors:
Marco Trudel
Carlo A. Furia
Martin Nordio
Bertrand Meyer


title: A Compositional Paradigm of Automating Refactorings

authors:
Mohsen Vakilian
Nicholas Chen
Roshanak Zilouchian Moghaddam
Stas Negara
Ralph E. Johnson


title: Simple Profile Rectifications Go a Long Way - Statistically Exploring and Alleviating the Effects of Sampling Errors for Program Optimizations

authors:
Bo Wu
Mingzhou Zhou
Xipeng Shen
Yaoqing Gao
Raúl Silvera
Graham Yiu


title: CoCo: Sound and Adaptive Replacement of Java Collections


title: Heap Decomposition Inference with Linear Programming

authors:
Haitao Steve Zhu
Yu David Liu


title: Constructing Call Graphs of Scala Programs

authors:
Karim Ali
Marianna Rapoport
Ondrej Lhoták
Julian Dolby
Frank Tip


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

authors:
Davide Ancona
Andrea Corradi


title: Understanding TypeScript

authors:
Gavin M. Bierman
Martín Abadi
Mads Torgersen


title: Semantics of (Resilient) X10

authors:
Silvia Crafa
David Cunningham
Vijay A. Saraswat
Avraham Shinnar
Olivier Tardieu

abstract: 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.


title: Capture-Avoiding and Hygienic Program Transformations

authors:
Sebastian Erdweg
Tijs van der Storm
Yi Dai

abstract:
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, inlining, lambda lifting, and compilers for two domain-specific languages.


title: Babelsberg/JS - A Browser-Based Implementation of an Object Constraint Language

authors:
Tim Felgentreff
Alan Borning
Robert Hirschfeld
Jens Lincke
Yoshiki Ohshima
Bert Freudenberg
Robert Krahn


title: An Executable Formal Semantics of PHP

authors:
Daniele Filaretti
Sergio Maffeis


title: Reusable Concurrent Data Types

authors:
Vincent Gramoli
Rachid Guerraoui


title: Graceful Dialects

authors:
Michael Homer
Timothy Jones
James Noble
Kim B. Bruce
Andrew P. Black


title: Cooperative Scheduling of Parallel Tasks with General Synchronization Patterns

authors:
Shams Mahmood Imam
Vivek Sarkar


title: Retargetting Legacy Browser Extensions to Modern Extension Frameworks

authors:
Rezwana Karim
Mohan Dhawan
Vinod Ganapathy


title: Portable and Efficient Run-time Monitoring of JavaScript Applications Using Virtual Machine Layering

authors:
Erick Lavoie
Bruno Dufour
Marc Feeley


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

authors:
Kyu Hyung Lee
Dohyeong Kim
Xiangyu Zhang


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

authors:
Siliang Li
Gang Tan


title: Self-inferencing Reflection Resolution for Java

authors:
Yue Li
Tian Tan
Yulei Sui
Jingling Xue


title: Automated Multi-Language Artifact Binding and Rename Refactoring between Java and DSLs Used by Java Frameworks

authors:
Philip Mayer
Andreas Schroeder


title: Rely-Guarantee Protocols

authors:
Filipe Militão
Jonathan Aldrich
Luís Caires

abstract: 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.


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

authors:
Heather Miller
Philipp Haller
Martin Odersky


title: Identifying Mandatory Code for Framework Use via a Single Application Trace

authors:
Naoya Nitta
Izuru Kume
Yasuhiro Takemura


title: Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions

authors:
Semih Okur
Cansu Erdogan
Danny Dig


title: Safely Composable Type-Specific Languages

authors:
Cyrus Omar
Darya Kurilova
Ligia Nistor
Benjamin Chung
Alex Potanin
Jonathan Aldrich

abstract: Programming languages often include specialized syntax for common datatypes e.g. lists 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 use strings, rather than structured data, with alarming frequency, leading to correctness, performance, security, and usability issues. Allowing library providers to modularly 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 still cause 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. The TSL for a type is invoked only when a literal appears where a term of that type is expected, guaranteeing non-interference. We give evidence supporting the applicability of this approach and formally specify it with a bidirectionally typed elaboration semantics for the Wyvern programming language.


title: TaDA: A Logic for Time and Data Abstraction

authors:
Pedro da Rocha Pinto
Thomas Dinsdale-Young
Philippa Gardner


title: MiCA: A Compositional Architecture for Gossip Protocols

authors:
Lonnie Princehouse
Rakesh Chenchu
Zhefu Jiang
Kenneth P. Birman
Nate Foster
Robert Soulé


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

authors:
Maximilian Scherr
Shigeru Chiba


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

authors:
Joshua Sunshine
James D. Herbsleb
Jonathan Aldrich

abstract: 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.


title: Stream Processing with a Spreadsheet

authors:
Mandana Vaziri
Olivier Tardieu
Rodric Rabbah
Philippe Suter
Martin Hirzel


title: State-Sensitive Points-to Analysis for the Dynamic Behavior of JavaScript Objects

authors:
Shiyi Wei
Barbara G. Ryder


title: Hybrid DOM-Sensitive Change Impact Analysis for JavaScript

authors:
Saba Alimadadi
Ali Mesbah
Karthik Pattabiraman

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%.


title: Loop Tiling in the Presence of Exceptions

authors:
Abhilash Bhandari
V. Krishna Nandivada

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.


title: Streams a la carte: Extensible Pipelines with Object Algebras

authors:
Aggelos Biboudis
Nick Palladinos
George Fourtounis
Yannis Smaragdakis

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.


title: Modular Verification of Finite Blocking in Non-terminating Programs

authors:
Pontus Boström
Peter Müller


title: Global Sequence Protocol: A Robust Abstraction for Replicated Shared State

authors:
Sebastian Burckhardt
Daan Leijen
Jonathan Protzenko
Manuel Fähndrich

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).


title: Access-rights Analysis in the Presence of Subjects

authors:
Paolina Centonze
Marco Pistoia
Omer Tripp

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.


title: Simple and Effective Type Check Removal through Lazy Basic Block Versioning

authors:
Maxime Chevalier-Boisvert
Marc Feeley

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.


title: 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.


title: Variability Abstractions: Trading Precision for Speed in Family-Based Analyses

authors:
Aleksandar S. Dimovski
Claus Brabrand
Andrzej Wasowski

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.


title: Defining Correctness Conditions for Concurrent Objects in Multicore Architectures

authors:
Brijesh Dongol
John Derrick
Lindsay Groves
Graeme Smith

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.


title: PerfBlower: Quickly Detecting Memory-Related Performance Problems via Amplification

authors:
Lu Fang
Liang Dou
Guoqing Xu

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.


title: Type Inference for Place-Oblivious Objects

authors:
Riyaz Haque
Jens Palsberg

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.


title: Framework for Static Analysis of PHP Applications

authors:
David Hauzar
Jan Kofron

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.


title: The Eureka Programming Model for Speculative Task Parallelism

authors:
Shams Imam
Vivek Sarkar

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.


title: Modular Termination Verification

authors:
Bart Jacobs
Dragan Bosnacki
Ruurd Kuiper

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.


title: Brand Objects for Nominal Typing

authors:
Timothy Jones
Michael Homer
James Noble

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.


title: Transparent Object Proxies in JavaScript

authors:
Matthias Keil
Sankha Narayan Guria
Andreas Schlegel
Manuel Geffken
Peter Thiemann

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.


title: TreatJS: Higher-Order Contracts for JavaScripts

authors:
Matthias Keil
Peter Thiemann

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.


title: Asynchronous Liquid Separation Types

authors:
Johannes Kloos
Rupak Majumdar
Viktor Vafeiadis

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.


title: A Theory of Tagged Objects

authors:
Joseph Lee
Jonathan Aldrich
Troy Shaw
Alex Potanin

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.


title: Intensional Effect Polymorphism

authors:
Yuheng Long
Yu David Liu
Hridesh Rajan

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.


title: The Love/Hate Relationship with the C Preprocessor: An Interview Study

authors:
Flávio Medeiros
Christian Kästner
Márcio Ribeiro
Sarah Nadi
Rohit Gheyi

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.


title: Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity

authors:
Changhee Park
Sukyoung Ryu

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.


title: Cooking the Books: Formalizing JMM Implementation Recipes

authors:
Gustavo Petri
Jan Vitek
Suresh Jagannathan

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.


title: The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript

authors:
Michael Pradel
Koushik Sen

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.


title: Concrete Types for TypeScript

authors:
Gregor Richards
Francesco Zappa Nardelli
Jan Vitek

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.


title: Lightweight Support for Magic Wands in an Automatic Verifier

authors:
Malte Schwerhoff
Alexander J. Summers

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.


title: A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization

authors:
Avraham Shinnar
Jérôme Siméon
Martin Hirzel

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.


title: Optimization Coaching for JavaScript

authors:
Vincent St-Amour
Shu-yu Guo

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.


title: 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.


title: 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.


title: Towards Practical Gradual Typing

authors:
Asumu Takikawa
Daniel Feltey
Earl Dean
Matthew Flatt
Robert Bruce Findler
Sam Tobin-Hochstadt
Matthias Felleisen

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.


title: Trust, but Verify: Two-Phase Typing for Dynamic Languages

authors:
Panagiotis Vekris
Benjamin Cosman
Ranjit Jhala

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.


title: Adaptive Context-sensitive Analysis for JavaScript

authors:
Shiyi Wei
Barbara G. Ryder

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.


title: Front Matter, Table of Contents, Preface, Artifacts, Conference Organization


title: Object Inheritance Without Classes

authors:
Timothy Jones
Michael Homer
James Noble
Kim B. Bruce

abstract: Which comes first: the object or the class? Language designers enjoy the conceptual simplicity of object-based languages (such as Emerald or Self) while many programmers prefer the pragmatic utility of classical inheritance (as in Simula and Java). Programmers in object-based languages have a tendency to build libraries to support traditional inheritance, and language implementations are often contorted to the same end. In this paper, we revisit the relationship between classes and objects. We model various kinds of inheritance in the context of an object-oriented language whose objects are not defined by classes, and explain why class inheritance and initialisation cannot be easily modelled purely by delegation.


title: A Calculus for Variational Programming

authors:
Sheng Chen
Martin Erwig
Eric Walkingshaw

abstract: Variation is ubiquitous in software. Many applications can benefit from making this variation explicit, then manipulating and computing with it directly---a technique we call "variational programming". This idea has been independently discovered in several application domains, such as efficiently analyzing and verifying software product lines, combining bounded and symbolic model-checking, and computing with alternative privacy profiles. Although these domains share similar core problems, and there are also many similarities in the solutions, there is no dedicated programming language support for variational programming. This makes the various implementations tedious, prone to errors, hard to maintain and reuse, and difficult to compare. In this paper we present a calculus that forms the basis of a programming language with explicit support for representing, manipulating, and computing with variation in programs and data. We illustrate how such a language can simplify the implementation of variational programming tasks. We present the syntax and semantics of the core calculus, a sound type system, and a type inference algorithm that produces principal types.


title: Trace Typing: An Approach for Evaluating Retrofitted Type Systems

authors:
Esben Andreasen
Colin S. Gordon
Satish Chandra
Manu Sridharan
Frank Tip
Koushik Sen

abstract: Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking. We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space. We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.


title: QL: Object-oriented Queries on Relational Data

authors:
Pavel Avgustinov
Oege de Moor
Michael Peyton Jones
Max Schäfer

abstract: This paper describes QL, a language for querying complex, potentially recursive data structures. QL compiles to Datalog and runs on a standard relational database, yet it provides familiar-looking object-oriented features such as classes and methods, reinterpreted in logical terms: classes are logical properties describing sets of values, subclassing is implication, and virtual calls are dispatched dynamically by considering the most specific classes containing the receiver. Furthermore, types in QL are prescriptive and actively influence program evaluation rather than just describing it. In combination, these features enable the development of concise queries based on reusable libraries, which are written in a purely declarative style, yet can be efficiently executed even on very large data sets. In particular, we have used QL to implement static analyses for various programming languages, which scale to millions of lines of code.


title: Fine-grained Language Composition: A Case Study

authors:
Edd Barrett
Carl Friedrich Bolz
Lukas Diekmann
Laurence Tratt

abstract: Although run-time language composition is common, it normally takes the form of a crude Foreign Function Interface (FFI). While useful, such compositions tend to be coarse-grained and slow. In this paper we introduce a novel fine-grained syntactic composition of PHP and Python which allows users to embed each language inside the other, including referencing variables across languages. This composition raises novel design and implementation challenges. We show that good solutions can be found to the design challenges; and that the resulting implementation imposes an acceptable performance overhead of, at most, 2.6x.


title: Making an Embedded DBMS JIT-friendly

authors:
Carl Friedrich Bolz
Darya Kurilova
Laurence Tratt

abstract: This artifact contains: the SQPyte prototype, a JIT for executing SQLite queries; and PyPy-SQPyte, a version of the PyPy Python VM which embeds SQPyte. In addition, a benchmark suite is included, which allows performance comparison against standard SQLite and the Java embedded database H2.


title: Reference Capabilities for Concurrency Control

authors:
Elias Castegren
Tobias Wrigstad

abstract: The proliferation of shared mutable state in object-oriented programming complicates software development as two seemingly unrelated operations may interact via an alias and produce unexpected results. In concurrent programming this manifests itself as data-races. Concurrent object-oriented programming further suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism. This paper presents a reference capability approach to concurrent and parallel object-oriented programming where all uses of aliases are guaranteed to be data-race free. The static type of an alias describes its possible sharing without using explicit ownership or effect annotations. Type information can express non-interfering deterministic parallelism without dynamic concurrency control, thread-locality, lock-based schemes, and guarded-by relations giving multi-object atomicity to nested data structures. Unification of capabilities and traits allows trait-based reuse across multiple concurrency scenarios with minimal code duplication. The resulting system brings together features from a wide range of prior work in a unified way.


title: Interprocedural Type Specialization of JavaScript Programs Without Type Analysis

authors:
Maxime Chevalier-Boisvert
Marc Feeley

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.


title: C++ const and Immutability: An Empirical Study of Writes-Through-const

authors:
Jon Eyolfson
Patrick Lam

abstract: The ability to specify immutability in a programming language is a powerful tool for developers, enabling them to better understand and more safely transform their code without fearing unintended changes to program state. The C++ programming language allows developers to specify a form of immutability using the const keyword. In this work, we characterize the meaning of the C++ const qualifier and present the ConstSanitizer tool, which dynamically verifies a stricter form of immutability than that defined in C++: it identifies const uses that are either not consistent with transitive immutability, that write to mutable fields, or that write to formerly-const objects whose const-ness has been cast away. We evaluate a set of 7 C++ benchmark programs to find writes-through-const, establish root causes for how they fail to respect our stricter definition of immutability, and assign attributes to each write (namely: synchronized, not visible, buffer/cache, delayed initialization, and incorrect). ConstSanitizer finds 17 archetypes for writes in these programs which do not respect our version of immutability. Over half of these seem unnecessary to us. Our classification and observations of behaviour in practice contribute to the understanding of a widely-used C++ language feature.


title: LJGS: Gradual Security Types for Object-Oriented Languages

authors:
Luminous Fennell
Peter Thiemann

abstract: LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS.


title: Formal Language Recognition with the Java Type Checker

authors:
Yossi Gil
Tomer Levy

abstract: This paper is a theoretical study of a practical problem: the automatic generation of Java Fluent APIs from their specification. We explain why the problem's core lies with the expressive power of Java generics. Our main result is that automatic generation is possible whenever the specification is an instance of the set of deterministic context-free languages, a set which contains most "practical" languages. Other contributions include a collection of techniques and idioms of the limited meta-programming possible with Java generics, and an empirical measurement demonstrating that the runtime of the "javac" compiler of Java may be exponential in the program's length, even for programs composed of a handful of lines and which do not rely on overly complex use of generics.


title: IceDust: Incremental and Eventual Computation of Derived Values in Persistent Object Graphs

authors:
Daco Harkes
Danny M. Groenewegen
Eelco Visser

abstract: Derived values are values calculated from base values. They can be expressed in object-oriented languages by means of getters calculating the derived value, and in relational or logic databases by means of (materialized) views. However, switching to a different calculation strategy (for example caching) in object-oriented programming requires invasive code changes, and the databases limit expressiveness by disallowing recursive aggregation. In this paper, we present IceDust, a data modeling language for expressing derived attribute values without committing to a calculation strategy. IceDust provides three strategies for calculating derived values in persistent object graphs: Calculate-on-Read, Calculate-on-Write, and Calculate-Eventually. We have developed a path-based abstract interpretation that provides static dependency analysis to generate code for these strategies. Benchmarks show that different strategies perform better in different scenarios. In addition we have conducted a case study that suggests that derived value calculations of systems used in practice can be expressed in IceDust.


title: One Way to Select Many

authors:
Jaakko Järvi
Sean Parent

abstract: Selecting items from a collection is one of the most common tasks users perform with graphical user interfaces. Practically every application supports this task with a selection feature different from that of any other application. Defects are common, especially in manipulating selections of non-adjacent elements, and flexible selection features are often missing when they would clearly be useful. As a consequence, user effort is wasted. The loss of productivity is experienced in small doses, but all computer users are impacted. The undesirable state of support for multi-element selection prevails because the same selection features are redesigned and reimplemented repeatedly. This article seeks to establish common abstractions for multi-selection. It gives generic but precise meanings to selection operations and makes multi-selection reusable; a JavaScript implementation is described. Application vendors benefit because of reduced development effort. Users benefit because correct and consistent multi-selection becomes available in more contexts.


title: Magic with Dynamo -- Flexible Cross-Component Linking for Java with Invokedynamic

authors:
Kamil Jezek
Jens Dietrich

abstract: Modern software systems are not built from scratch. They use functionality provided by libraries. These libraries evolve and often upgrades are deployed without the systems being recompiled. In Java, this process is particularly error-prone due to the mismatch between source and binary compatibility, and the lack of API stability in many popular libraries. We propose a novel approach to mitigate this problem based on the use of invokedynamic instructions for cross-component method invocations. The dispatch mechanism of invokedynamic is used to provide on-the-fly signature adaptation. We show how this idea can be used to construct a Java compiler that produces more resilient bytecode. We present the dynamo compiler, a proof-of-concept implemented as a javac post compiler. We evaluate our approach using several benchmark examples and two case studies showing how the dynamo compiler can prevent certain types of linkage and stack overflow errors that have been observed in real-world systems.


title: Program Tailoring: Slicing by Sequential Criteria

authors:
Yue Li
Tian Tan
Yifei Zhang
Jingling Xue

abstract: Protocol and typestate analyses often report some sequences of statements ending at a program point P that needs to be scrutinized, since P may be erroneous or imprecisely analyzed. Program slicing focuses only on the behavior at P by computing a slice of the program affecting the values at P. In this paper, we propose to restrict our attention to the subset of that behavior at P affected by one or several statement sequences, called a sequential criterion (SC). By leveraging the ordering information in a SC, e.g., the temporal order in a few valid/invalid API method invocation sequences, we introduce a new technique, program tailoring, to compute a tailored program that comprises the statements in all possible execution paths passing through at least one sequence in SC in the given order. With a prototyping implementation, Tailor, we show why tailoring is practically useful by conducting two case studies on seven large real-world Java applications. For program debugging and understanding, Tailor can complement program slicing by removing SC-irrelevant statements. For program analysis, Tailor can enable a pointer analysis, which is unscalable to a program, to perform a more focused and therefore potentially scalable analysis to its specific parts containing hard language features such as reflection.


title: Composing Interfering Abstract Protocols

authors:
Filipe Militão
Jonathan Aldrich
Luís Caires

abstract: The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.


title: The Elements of Decision Alignment

authors:
Mark S. Miller
Bill Tulloh

abstract: When one object makes a request of another, why do we expect that the second object's behavior correctly satisfies the first object's wishes? The need to cope with such principal-agent problems shapes programming practice as much as it shapes human organizations and economies. However, the literature about such plan coordination issues among humans is almost disjoint from the literature about these issues among objects. Even the terms used are unrelated. These fields have much to learn from each other---both from their similarities and from the causes of their differences. We propose a framework for thinking about decision alignment as a bridge between these disciplines.


title: A Calculus with Partially Dynamic Records for Typeful Manipulation of JSON Objects

authors:
Atsushi Ohori
Katsuhiro Ueno
Tomohiro Sasaki
Daisuke Kikuchi

abstract: This paper investigates language constructs for high-level and type-safe manipulation of JSON objects in a typed functional language. A major obstacle in representing JSON in a static type system is their heterogeneous nature: in most practical JSON APIs, a JSON array is a heterogeneous list consisting of, for example, objects having common fields and possibly some optional fields. This paper presents a typed calculus that reconciles static typing constraints and heterogeneous JSON arrays based on the idea of partially dynamic records originally proposed and sketched by Buneman and Ohori for complex database object manipulation. Partially dynamic records are dynamically typed records, but some parts of their structures are statically known. This feature enables us to represent JSON objects as typed data structures. The proposed calculus smoothly extends with ML-style pattern matching and record polymorphism. These results yield a typed functional language where the programmer can directly import JSON data as terms having static types, and can manipulate them with the full benefits of static polymorphic type-checking. The proposed calculus has been embodied in SML#, an extension of Standard ML with record polymorphism and other practically useful features. This paper also reports on the details of the implementation and demonstrates its feasibility through examples using actual Web APIs. The SML# version 3.1.0 compiler includes JSON support presented in this paper, and is available from Tohoku University as open-source software under a BSD-style license.


title: Higher-Order Demand-Driven Program Analysis

authors:
Zachary Palmer
Scott F. Smith

abstract: We explore a novel approach to higher-order program analysis that brings ideas of on-demand lookup from first-order CFL-reachability program analyses to higher-order programs. The analysis needs to produce only a control-flow graph; it can derive all other information including values of variables directly from the graph. Several challenges had to be overcome, including how to build the control-flow graph on-the-fly and how to deal with non-local variables in functions. The resulting analysis is flow- and context-sensitive with a provable polynomial-time bound. The analysis is formalized and proved correct and terminating, and an initial implementation is described.


title: Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics

authors:
Casper Bach Poulsen
Pierre Néron
Andrew P. Tolmach
Eelco Visser

abstract: Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.


title: Lightweight Session Programming in Scala

authors:
Alceste Scalas
Nobuko Yoshida


title: Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java

authors:
Johannes Späth
Lisa Nguyen Quang Do
Karim Ali
Eric Bodden

abstract: Many current program analyses require highly precise pointer information about small, tar- geted parts of a given program. This motivates the need for demand-driven pointer analyses that compute information only where required. Pointer analyses generally compute points-to sets of program variables or answer boolean alias queries. However, many client analyses require richer pointer information. For example, taint and typestate analyses often need to know the set of all aliases of a given variable under a certain calling context. With most current pointer analyses, clients must compute such information through repeated points-to or alias queries, increasing complexity and computation time for them. This paper presents Boomerang, a demand-driven, flow-, field-, and context-sensitive pointer analysis for Java programs. Boomerang computes rich results that include both the possible allocation sites of a given pointer (points-to information) and all pointers that can point to those allocation sites (alias information). For increased precision and scalability, clients can query Boomerang with respect to particular calling contexts of interest. Our experiments show that Boomerang is more precise than existing demand-driven pointer analyses. Additionally, using Boomerang, the taint analysis FlowDroid issues up to 29.4x fewer pointer queries compared to using other pointer analyses that return simpler pointer infor- mation. Furthermore, the search space of Boomerang can be significantly reduced by requesting calling contexts from the client analysis.


title: Transactional Tasks: Parallelism in Software Transactions

authors:
Janwillem Swalens
Joeri De Koster
Wolfgang De Meuter

abstract: Many programming languages, such as Clojure, Scala, and Haskell, support different concurrency models. In practice these models are often combined, however the semantics of the combinations are not always well-defined. In this paper, we study the combination of futures and Software Transactional Memory. Currently, futures created within a transaction cannot access the transactional state safely, violating the serializability of the transactions and leading to undesired behavior. We define transactional tasks: a construct that allows futures to be created in transactions. Transactional tasks allow the parallelism in a transaction to be exploited, while providing safe access to the state of their encapsulating transaction. We show that transactional tasks have several useful properties: they are coordinated, they maintain serializability, and they do not introduce non-determinism. As such, transactional tasks combine futures and Software Transactional Memory, allowing the potential parallelism of a program to be fully exploited, while preserving the properties of the separate models where possible.


title: Staccato: A Bug Finder for Dynamic Configuration Updates

authors:
John Toman
Dan Grossman

abstract: Modern software applications are highly configurable, allowing configuration options to be changed even during program execution. When dynamic configuration updating is implemented incorrectly, program errors can result. These program errors occur primarily when stale data—computed from old configurations—or inconsistent data—computed from different configurations—are used. We introduce Staccato, the first tool designed to detect these errors. Staccato uses a dynamic analysis in the style of taint analysis to find the use of stale configuration data in Java programs. It supports concurrent programs running on commodity JVMs. In some cases, Staccato can provide automatic bug avoidance and semi-automatic repair when errors occur. We evaluated Staccato on 3 open-source applications that support complex reconfigurability. Staccato found multiple errors in all of them. Staccato requires only modest annotation overhead and has moderate performance overhead.


title: Transforming Programs between APIs with Many-to-Many Mappings

authors:
Chenglong Wang
Jiajun Jiang
Jun Li
Yingfei Xiong
Xiangyu Luo
Lu Zhang
Zhenjiang Hu

abstract: Transforming programs between two APIs or different versions of the same API is a common software engineering task. However, existing languages supporting for such transformation cannot satisfactorily handle the cases when the relations between elements in the old API and the new API are many-to-many mappings: multiple invocations to the old API are supposed to be replaced by multiple invocations to the new API. Since the multiple invocations of the original APIs may not appear consecutively and the variables in these calls may have different names, writing a tool correctly to cover all such invocation cases is not an easy task. In this paper we propose a novel guided-normalization approach to address this problem. Our core insight is that programs in different forms can be semantics-equivalently normalized into a basic form guided by transformation goals, and developers only need to write rules for the basic form to address the transformation. Based on this approach, we design a declarative program transformation language, PATL, for adapting Java programs between different APIs. PATL has simple syntax and basic semantics to handle transformations only considering consecutive statements inside basic blocks, while with guided-normalization, it can be extended to handle complex forms of invocations. Furthermore, PATL ensures that the user-written rules would not accidentally break def-use relations in the program. We formalize the semantics of PATL on Middleweight Java and prove the semantics-preserving property of guided-normalization. We also evaluated our language with three non-trivial case studies: i.e. updating Google Calendar API, switching from JDom to Dom4j, and switching from Swing to SWT. The result is encouraging; it shows that our language allows successful transformations of real world programs with a small number of rules and little manual resolution.


title: Front Matter, Table of Contents, Preface, List of Authors


title: Towards Ontology-Based Program Analysis

authors:
Yue Zhao
Guoyang Chen
Chunhua Liao
Xipeng Shen

abstract: Program analysis is fundamental for program optimizations, debugging, and many other tasks. But developing program analyses has been a challenging and error-prone process for general users. Declarative program analysis has shown the promise to dramatically improve the productivity in the development of program analyses. Current declarative program analysis is however subject to some major limitations in supporting cooperations among analysis tools, guiding program optimizations, and often requires much effort for repeated program preprocessing. In this work, we advocate the integration of ontology into declarative program analysis. As a way to standardize the definitions of concepts in a domain and the representation of the knowledge in the domain, ontology offers a promising way to address the limitations of current declarative program analysis. We develop a prototype framework named PATO for conducting program analysis upon ontology-based program representation. Experiments on six program analyses confirm the potential of ontology for complementing existing declarative program analysis. It supports multiple analyses without separate program preprocessing, promotes cooperative Liveness analysis between two compilers, and effectively guides a data placement optimization for Graphic Processing Units (GPU).


title: What's the Optimal Performance of Precise Dynamic Race Detection? - A Redundancy Perspective

authors:
Jeff Huang
Arun K. Rajagopalan

abstract: In a precise data race detector, a race is detected only if the execution exhibits a real race. In such tools, every memory access from each thread is typically checked by a happens-before algorithm. What’s the optimal runtime performance of such tools? In this paper, we identify that a significant percentage of memory access checks in real-world program executions are often redundant: removing these checks affects neither the precision nor the capability of race detection. We show that if all such redundant checks were eliminated with no cost, the optimal performance of a state-of-the-art dynamic race detector, FastTrack, could be improved by 90%, reducing its runtime overhead from 68X to 7X on a collection of CPU intensive benchmarks. We further develop a purely dynamic technique, ReX, that efficiently filters out redundant checks and apply it to FastTrack. With ReX, the runtime performance of FastTrack is improved by 31% on average.


title: Parallelizing Julia with a Non-Invasive DSL

authors:
Todd A. Anderson
Hai Liu
Lindsey Kuper
Ehsan Totoni
Jan Vitek
Tatiana Shpeisman

abstract: Computational scientists often prototype software using productivity languages that offer high-level programming abstractions. When higher performance is needed, they are obliged to rewrite their code in a lower-level efficiency language. Different solutions have been proposed to address this trade-off between productivity and efficiency. One promising approach is to create embedded domain-specific languages that sacrifice generality for productivity and performance, but practical experience with DSLs points to some road blocks preventing widespread adoption. This paper proposes a non-invasive domain-specific language that makes as few visible changes to the host programming model as possible. We present ParallelAccelerator, a library and compiler for high-level, high-performance scientific computing in Julia. ParallelAccelerator's programming model is aligned with existing Julia programming idioms. Our compiler exposes the implicit parallelism in high-level array-style programs and compiles them to fast, parallel native code. Programs can also run in "library-only" mode, letting users benefit from the full Julia environment and libraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.


title: Modelling Homogeneous Generative Meta-Programming

authors:
Martin Berger
Laurence Tratt
Christian Urban

abstract: Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Template Haskell. The calculus is designed such that it can be gradually enhanced with the features needed to model many of the advanced features of real languages. We demonstrate this by showing how a simple, staged type system as found in Template Haskell can be added to the calculus.


title: Composing Software in an Age of Dissonance (Invited Talk)

abstract: The power of languages is rooted in composition. An infinite number of sentences can be composed from a finite set of generative rules. The more uniformly the rules apply, the more valid compositions there are. Hence simpler rules give rise to richer discourse - a case of ‘less is more’. We must however be careful as to which distinctions we preserve and which we eliminate. If we abstract too much we risk creating an undifferentiated soup with no landmarks to orient us. A uniform space of objects with simple rules governing their interaction is an obvious example of these ideas, but objects also serve as a cautionary tale. Achieving simplicity is not easy; it requires taste, judgement, experience and dedication. Ingenuity is essential as well, but left unchecked, it often leads to uncontrollable complexity. The path of least resistance follows the tautological principle that ‘more is more’, and who can argue with a tautology? Dissonance dominates. I will endeavour to illustrate these rather abstract principles by means of examples from my own work and that of others, in programming languages, software and other domains. We may speak of many things - mixins, modules and memory, graphics and generics, patterns and parsers, architecture and automobiles, objects or other things entirely.


title: Relaxed Linear References for Lock-free Data Structures

authors:
Elias Castegren
Tobias Wrigstad


title: Type Abstraction for Relaxed Noninterference

authors:
Raimil Cruz
Tamara Rezk
Bernard P. Serpette
Éric Tanter

abstract: Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the different information flow approaches to declassification, a particularly expressive approach was proposed by Li and Zdancewic, enforcing a notion of relaxed noninterference by allowing programmers to specify declassification policies that capture the intended manner in which public information can be computed from private data. This paper shows how we can exploit the familiar notion of type abstraction to support expressive declassification policies in a simpler, yet more expressive manner. In particular, the type-based approach to declassification---which we develop in an object-oriented setting---addresses several issues and challenges with respect to prior work, including a simple notion of label ordering based on subtyping, support for recursive declassification policies, and a local, modular reasoning principle for relaxed noninterference. This work paves the way for integrating declassification policies in practical security-typed languages.


title: Concurrent Data Structures Linked in Time

authors:
Germán Andrés Delbianco
Ilya Sergey
Aleksandar Nanevski
Anindya Banerjee

abstract: Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated. In this paper we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We name the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. We illustrate the method by verifying (mechanically in Coq) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients.