title: Efficiently speeding up sequential computation through the n-way programming model

authors:
Romain Cledat
Tushar Kumar
Santosh Pande

abstract: With core counts on the rise, the sequential components of applications are becoming the major bottleneck in performance scaling as predicted by Amdahl's law. We are therefore faced with the simultaneous problems of occupying an increasing number of cores and speeding up sequential sections. In this work, we reconcile these two seemingly incompatible problems with a novel programming model called N-way. The core idea behind N-way is to benefit from the algorithmic diversity available to express certain key computational steps. By simultaneously launching in parallel multiple ways to solve a given computation, a runtime can just-in-time pick the best (for example the fastest) way and therefore achieve speedup.


venue: oopsla

title: Trustworthy numerical computation in Scala

authors:
Eva Darulova
Viktor Kuncak

abstract: Modern computing has adopted the floating point type as a default way to describe computations with real numbers. Thanks to dedicated hardware support, such computations are efficient on modern architectures, even in double precision. However, rigorous reasoning about the resulting programs remains difficult. This is in part due to a large gap between the finite floating point representation and the infinite-precision real-number semantics that serves as the developers' mental model. Because programming languages do not provide support for estimating errors, some computations in practice are performed more and some less precisely than needed.


title: Immutable specifications for more concise and precise verification

authors:
Cristina David
Wei-Ngan Chin

abstract: In the current work, we investigate the benefits of immutability guarantees for allowing more flexible handling of aliasing, as well as more precise and concise specifications. Our approach supports finer levels of control that can mark data structures as being immutable through the use of immutability annotations. By using such annotations to encode immutability guarantees, we expect to obtain better specifications that can more accurately describe the intentions, as well as prohibitions, of the method. Ultimately, our goal is improving the precision of the verification process, as well as making the specifications more readable, more precise and as an enforceable program documentation. We have designed and implemented a new entailment procedure to formally and automatically reason about immutability enhanced specifications. We have also formalised the soundness for our new procedure through an operational semantics with mutability assertions on the heap. Lastly, we have carried out a set of experiments to both validate and affirm the utility of our current proposal on immutability enhanced specification mechanism.


title: Product lines of theorems

authors:
Benjamin Delaware
William R. Cook
Don S. Batory

abstract: Mechanized proof assistants are powerful verification tools, but proof development can be difficult and time-consuming. When verifying a family of related programs, the effort can be reduced by proof reuse. In this paper, we show how to engineer product lines with theorems and proofs built from feature modules. Each module contains proof fragments which are composed together to build a complete proof of correctness for each product. We consider a product line of programming languages, where each variant includes metatheory proofs verifying the correctness of its semantic definitions. This approach has been realized in the Coq proof assistant, with the proofs of each feature independently certifiable by Coq. These proofs are composed for each language variant, with Coq mechanically verifying that the composite proofs are correct. As validation, we formalize a core calculus for Java in Coq which can be extended with any combination of casts, interfaces, or generics.


title: Reactive imperative programming with dataflow constraints

authors:
Camil Demetrescu
Irene Finocchi
Andrea Ribichini

abstract: Dataflow languages provide natural support for specifying constraints between objects in dynamic applications, where programs need to react efficiently to changes of their environment. Researchers have long investigated how to take advantage of dataflow constraints by embedding them into procedural languages. Previous mixed imperative/dataflow systems, however, require syntactic extensions or libraries of ad hoc data types for binding the imperative program to the dataflow solver. In this paper we propose a novel approach that smoothly combines the two paradigms without placing undue burden on the programmer. In our framework, programmers can define ordinary statements of the imperative host language that enforce constraints between objects stored in special memory locations designated as "reactive". Differently from previous approaches, reactive objects can be of any legal type in the host language, including primitive data types, pointers, arrays, and structures. Statements defining constraints are automatically re-executed every time their input memory locations change, letting a program behave like a spreadsheet where the values of some variables depend upon the values of other variables. The constraint solving mechanism is handled transparently by altering the semantics of elementary operations of the host language for reading and modifying objects. We provide a formal semantics and describe a concrete embodiment of our technique into C/C++, showing how to implement it efficiently in conventional platforms using off-the-shelf compilers. We discuss common coding idioms and relevant applications to reactive scenarios, including incremental computation, observer design pattern, and data structure repair. The performance of our implementation is compared to ad hoc problem-specific change propagation algorithms, as well as to language-centric approaches such as self-adjusting computation and subject/observer communication mechanisms, showing that the proposed approach is efficient in practice.


title: Kind analysis for MATLAB

authors:
Jesse Doherty
Laurie J. Hendren
Soroush Radpour

abstract: MATLAB is a popular dynamic programming language used for scientific and numerical programming. As a language, it has evolved from a small scripting language intended as an interactive interface to numerical libraries, to a very popular language supporting many language features and libraries. The overloaded syntax and dynamic nature of the language, plus the somewhat organic addition of language features over the years, makes static analysis of modern MATLAB quite challenging. A fundamental problem in MATLAB is determining the kind of an identifier. Does an identifier refer to a variable, a named function or a prefix? Although this is a trivial problem for most programming languages, it was not clear how to do this properly in MATLAB. Furthermore, there was no simple explanation of kind analysis suitable for MATLAB programmers, nor a publicly-available implementation suitable for compiler researchers.


title: SugarJ: library-based syntactic language extensibility

authors:
Sebastian Erdweg
Tillmann Rendel
Christian Kästner
Klaus Ostermann

abstract: Existing approaches to extend a programming language with syntactic sugar often leave a bitter taste, because they cannot be used with the same ease as the main extension mechanism of the programming language - libraries. Sugar libraries are a novel approach for syntactically extending a programming language within the language. A sugar library is like an ordinary library, but can, in addition, export syntactic sugar for using the library. Sugar libraries maintain the composability and scoping properties of ordinary libraries and are hence particularly well-suited for embedding a multitude of domain-specific languages into a host language. They also inherit self-applicability from libraries, which means that sugar libraries can provide syntactic extensions for the definition of other sugar libraries. To demonstrate the expressiveness and applicability of sugar libraries, we have developed SugarJ, a language on top of Java, SDF and Stratego, which supports syntactic extensibility. SugarJ employs a novel incremental parsing technique, which allows changing the syntax within a source file. We demonstrate SugarJ by five language extensions, including embeddings of XML and closures in Java, all available as sugar libraries. We illustrate the utility of self-applicability by embedding XML Schema, a metalanguage to define XML languages.

awards: Most Influential OOPSLA Paper (awarded 2021)


title: Tool-supported refactoring for JavaScript

authors:
Asger Feldthaus
Todd D. Millstein
Anders Møller
Max Schäfer
Frank Tip

abstract: Refactoring is a popular technique for improving the structure of existing programs while maintaining their behavior. For statically typed programming languages such as Java, a wide variety of refactorings have been described, and tool support for performing refactorings and ensuring their correctness is widely available in modern IDEs. For the JavaScript programming language, however, existing refactoring tools are less mature and often unable to ensure that program behavior is preserved. Refactoring algorithms that have been developed for statically typed languages are not applicable to JavaScript because of its dynamic nature. We propose a framework for specifying and implementing JavaScript refactorings based on pointer analysis. We describe novel refactorings motivated by best practice recommendations for JavaScript programming, and demonstrate how they can be described concisely in terms of queries provided by our framework. Experiments performed with a prototype implementation on a suite of existing applications show that our approach is well-suited for developing practical refactoring tools for JavaScript.


title: Automatic fine-grain locking using shape properties

authors:
Guy Golan-Gueta
Nathan Grasso Bronson
Alex Aiken
G. Ramalingam
Mooly Sagiv
Eran Yahav

abstract: We present a technique for automatically adding fine-grain locking to an abstract data type that is implemented using a dynamic forest -i.e., the data structures may be mutated, even to the point of violating forestness temporarily during the execution of a method of the ADT. Our automatic technique is based on Domination Locking, a novel locking protocol. Domination locking is designed specifically for software concurrency control, and in particular is designed for object-oriented software with destructive pointer updates. Domination locking is a strict generalization of existing locking protocols for dynamically changing graphs. We show our technique can successfully add fine-grain locking to libraries where manually performing locking is extremely challenging. We show that automatic fine-grain locking is more efficient than coarse-grain locking, and obtains similar performance to hand-crafted fine-grain locking.


title: Self-adjusting stack machines

authors:
Matthew A. Hammer
Georg Neis
Yan Chen
Umut A. Acar

abstract: Self-adjusting computation offers a language-based approach to writing programs that automatically respond to dynamically changing data. Recent work made significant progress in developing sound semantics and associated implementations of self-adjusting computation for high-level, functional languages. These techniques, however, do not address issues that arise for low-level languages, i.e., stack-based imperative languages that lack strong type systems and automatic memory management. In this paper, we describe techniques for self-adjusting computation which are suitable for low-level languages. Necessarily, we take a different approach than previous work: instead of starting with a high-level language with additional primitives to support self-adjusting computation, we start with a low-level intermediate language, whose semantics is given by a stack-based abstract machine. We prove that this semantics is sound: it always updates computations in a way that is consistent with full reevaluation. We give a compiler and runtime system for the intermediate language used by our abstract machine. We present an empirical evaluation that shows that our approach is efficient in practice, and performs favorably compared to prior proposals.


title: AC: composable asynchronous IO for native languages

authors:
Tim Harris
Martín Abadi
Rebecca Isaacs
Ross McIlroy

abstract: This paper introduces AC, a set of language constructs for composable asynchronous IO in native languages such as C/C++. Unlike traditional synchronous IO interfaces, AC lets a thread issue multiple IO requests so that they can be serviced concurrently, and so that long-latency operations can be overlapped with computation. Unlike traditional asynchronous IO interfaces, AC retains a sequential style of programming without requiring code to use multiple threads, and without requiring code to be "stack-ripped" into chains of callbacks. AC provides an "async" statement to identify opportunities for IO operations to be issued concurrently, a "do..finish" block that waits until any enclosed "async" work is complete, and a "cancel" statement that requests cancellation of unfinished IO within an enclosing "do..finish". We give an operational semantics for a core language. We describe and evaluate implementations that are integrated with message passing on the Barrelfish research OS, and integrated with asynchronous file and network IO on Microsoft Windows. We show that AC offers comparable performance to existing C/C++ interfaces for asynchronous IO, while providing a simpler programming model.


title: Declaratively programming the mobile web with Mobl

authors:
Zef Hemel
Eelco Visser

abstract: A new generation of mobile touch devices, such as the iPhone, iPad and Android devices, are equipped with powerful, modern browsers. However, regular websites are not optimized for the specific features and constraints of these devices, such as limited screen estate, unreliable Internet access, touch-based interaction patterns, and features such as GPS. While recent advances in web technology enable web developers to build web applications that take advantage of the unique properties of mobile devices, developing such applications exposes a number of problems, specifically: developers are required to use many loosely coupled languages with limited tool support and application code is often verbose and imperative. We introduce mobl, a new language designed to declaratively construct mobile web applications. Mobl integrates languages for user interface design, styling, data modeling, querying and application logic into a single, unified language that is flexible, expressive, enables early detection of errors, and has good IDE support.


title: Ribbons: a partially shared memory programming model

authors:
Kevin J. Hoffman
Harrison Metzger
Patrick Eugster

abstract: The need for programs to execute subcomponents in isolation from each other or with lower privileges is prevalent among today's systems. We introduce ribbons: a shared memory programming model that allows for more implicit sharing of memory than processes but is more restrictive than threads. Ribbons structure the heap into protection domains. Privileges between these protection domains are carefully controlled in order to confine computation. We propose RibbonJ, a backwards-compatible extension of Java, to easily create or port programs to use the ribbons model. We study the progress and isolation properties of a subset of the language. Building on JikesRVM we implement ribbons by leveraging existing memory protection mechanisms in modern hardware and operating systems, avoiding the overhead of inline security checks and read or write barriers. We evaluate efficiency via microbenchmarks and the DaCapo suite, observing minor overhead. Additionally, we refactor Apache Tomcat to use ribbons for application isolation, discuss the refactoring's design and complexity, and evaluate performance using the SPECweb2009 benchmark.


title: A syntactic type system for recursive modules

authors:
Hyeonseung Im
Keiko Nakata
Jacques Garrigue
Sungwoo Park

abstract: A practical type system for ML-style recursive modules should address at least two technical challenges. First, it needs to solve the double vision problem, which refers to an inconsistency between external and internal views of recursive modules. Second, it needs to overcome the tension between practical decidability and expressivity which arises from the potential presence of cyclic type definitions caused by recursion between modules. Although type systems in previous proposals solve the double vision problem and are also decidable, they fail to typecheck common patterns of recursive modules, such as functor fixpoints, that are essential to the expressivity of the module system and the modular development of recursive modules. This paper proposes a novel type system for recursive modules that solves the double vision problem and typechecks common patterns of recursive modules including functor fixpoints. First, we design a type system with a type equivalence based on weak bisimilarity, which does not lend itself to practical implementation in general, but accommodates a broad range of cyclic type definitions. Then, we identify a practically implementable fragment using a type equivalence based on type normalization, which is expressive enough to typecheck typical uses of recursive modules. Our approach is purely syntactic and the definition of the type system is ready for use in an actual implementation.


title: Gradual typing for generics

authors:
Lintaro Ina
Atsushi Igarashi

abstract: Gradual typing is a framework to combine static and dynamic typing in a single programming language. In this paper, we develop a gradual type system for class-based object-oriented languages with generics. We introduce a special type to denote dynamically typed parts of a program; unlike dynamic types introduced to C# 4.0, however, our type system allows for more seamless integration of dynamically and statically typed code.


title: Kismet: parallel speedup estimates for serial programs

authors:
Donghwan Jeon
Saturnino Garcia
Christopher M. Louie
Michael Bedford Taylor

abstract: Software engineers now face the difficult task of refactoring serial programs for parallel execution on multicore processors. Currently, they are offered little guidance as to how much benefit may come from this task, or how close they are to the best possible parallelization. This paper presents Kismet, a tool that creates parallel speedup estimates for unparallelized serial programs. Kismet differs from previous approaches in that it does not require any manual analysis or modification of the program. This difference allows quick analysis of many programs, avoiding wasted engineering effort on those that are fundamentally limited. To accomplish this task, Kismet builds upon the hierarchical critical path analysis (HCPA) technique, a recently developed dynamic analysis that localizes parallelism to each of the potentially nested regions in the target program. It then uses a parallel execution time model to compute an approximate upper bound for performance, modeling constraints that stem from both hardware parameters and internal program structure.


title: Enhancing locality for recursive traversals of recursive structures

authors:
Youngjoon Jo
Milind Kulkarni

abstract: While there has been decades of work on developing automatic, locality-enhancing transformations for regular programs that operate over dense matrices and arrays, there has been little investigation of such transformations for irregular programs, which operate over pointer-based data structures such as graphs, trees and lists. In this paper, we argue that, for a class of irregular applications we call traversal codes, there exists substantial data reuse and hence opportunity for locality exploitation. We develop a novel optimization called point blocking, inspired by the classic tiling loop transformation, and show that it can substantially enhance temporal locality in traversal codes. We then present a transformation and optimization framework called TreeTiler that automatically detects opportunities for applying point blocking and applies the transformation. TreeTiler uses autotuning techniques to determine appropriate parameters for the transformation. For a series of traversal algorithms drawn from real-world applications, we show that TreeTiler is able to deliver performance improvements of up to 245% over an optimized (but non-transformed) parallel baseline, and in several cases, significantly better scalability.


title: PREFAIL: a programmable tool for multiple-failure injection

authors:
Pallavi Joshi
Haryadi S. Gunawi
Koushik Sen

abstract: As hardware failures are no longer rare in the era of cloud computing, cloud software systems must "prevail" against multiple, diverse failures that are likely to occur. Testing software against multiple failures poses the problem of combinatorial explosion of multiple failures. To address this problem, we present PreFail, a programmable failure-injection tool that enables testers to write a wide range of policies to prune down the large space of multiple failures. We integrate PreFail to three cloud software systems (HDFS, Cassandra, and ZooKeeper), show a wide variety of useful pruning policies that we can write for them, and evaluate the speed-ups in testing time that we obtain by using the policies. In our experiments, our testing approach with appropriate policies found all the bugs that one can find using exhaustive testing while spending 10X--200X less time than exhaustive testing.


title: Catch me if you can: performance bug detection in the wild

authors:
Milan Jovic
Andrea Adamoli
Matthias Hauswirth

abstract: Profilers help developers to find and fix performance problems. But do they find performance bugs -- performance problems that real users actually notice? In this paper we argue that -- especially in the case of interactive applications -- traditional profilers find irrelevant problems but fail to find relevant bugs.


title: Variability-aware parsing in the presence of lexical macros and conditional compilation

authors:
Christian Kästner
Paolo G. Giarrusso
Tillmann Rendel
Sebastian Erdweg
Klaus Ostermann
Thorsten Berger

abstract: In many projects, lexical preprocessors are used to manage different variants of the project (using conditional compilation) and to define compile-time code transformations (using macros). Unfortunately, while being a simple way to implement variability, conditional compilation and lexical macros hinder automatic analysis, even though such analysis is urgently needed to combat variability-induced complexity. To analyze code with its variability, we need to parse it without preprocessing it. However, current parsing solutions use unsound heuristics, support only a subset of the language, or suffer from exponential explosion. As part of the TypeChef project, we contribute a novel variability-aware parser that can parse almost all unpreprocessed code without heuristics in practicable time. Beyond the obvious task of detecting syntax errors, our parser paves the road for further analysis, such as variability-aware type checking. We implement variability-aware parsers for Java and GNU C and demonstrate practicability by parsing the product line MobileMedia and the entire X86 architecture of the Linux kernel with 6065 variable features.


title: Integrated language definition testing: enabling test-driven language development

authors:
Lennart C. L. Kats
Rob Vermaas
Eelco Visser

abstract: The reliability of compilers, interpreters, and development environments for programming languages is essential for effective software development and maintenance. They are often tested only as an afterthought. Languages with a smaller scope, such as domain-specific languages, often remain untested. General-purpose testing techniques and test case generation methods fall short in providing a low-threshold solution for test-driven language development. In this paper we introduce the notion of a language-parametric testing language (LPTL) that provides a reusable, generic basis for declaratively specifying language definition tests. We integrate the syntax, semantics, and editor services of a language under test into the LPTL for writing test inputs. This paper describes the design of an LPTL and the tool support provided for it, shows use cases using examples, and describes our implementation in the form of the Spoofax testing language.


title: Safe parallel programming using dynamic dependence hints

authors:
Chuanle Ke
Lei Liu
Chao Zhang
Tongxin Bai
Bryan Jacobs
Chen Ding

abstract: Speculative parallelization divides a sequential program into possibly parallel tasks and permits these tasks to run in parallel if and only if they show no dependences with each other. The parallelization is safe in that a speculative execution always produces the same output as the sequential execution.


title: JIT compilation policy for modern machines

abstract: Dynamic or Just-in-Time (JIT) compilation is crucial to achieve acceptable performance for applications (written in managed languages, such as Java and C#) distributed as intermediate language binary codes for a virtual machine (VM) architecture. Since it occurs at runtime, JIT compilation needs to carefully tune its compilation policy to make effective decisions regarding 'if' and 'when' to compile different program regions to achieve the best overall program performance. Past research has extensively tuned JIT compilation policies, but mainly for VMs with a single compiler thread and for execution on single-processor machines.


title: SOS: saving time in dynamic race detection with stationary analysis

authors:
Du Li
Witawas Srisa-an
Matthew B. Dwyer

abstract: Data races are subtle and difficult to detect errors that arise during concurrent program execution. Traditional testing techniques fail to find these errors, but recent research has shown that targeted dynamic analysis techniques can be developed to precisely detect races (i.e., no false race reports are generated) that occur during program execution. Unfortunately, precise race detection is still too expensive to be used in practice. State-of-the-art techniques still slow down program execution by a factor of eight or more. In this paper, we incorporate an optimization technique based on the observation that many thread-shared objects are written early in their lifetimes and then become read-only for the remainder of their lifetimes; these are known as stationary objects. The main contribution of our work is the insight that once a stationary object becomes thread-shared, races cannot occur. Therefore, our proposed approach does not monitor access to these objects. As such, our system only incurs an average overhead of 45% of that of an implementation of FastTrack, a low-overhead dynamic race detector. We then compared the effectiveness of our approach to de- tect races in deployed environments with that of Pacer, a sampling based race detector based on FastTrack. We found that our approach can detect over five times more races than Pacer when we budget 50% for runtime overhead.


title: JET: exception checking in the Java native interface

authors:
Siliang Li
Gang Tan

abstract: Java's type system enforces exception-checking rules that stipulate a checked exception thrown by a method must be declared in the throws clause of the method. Software written in Java often invokes native methods through the use of the Java Native Interface (JNI). Java's type system, however, cannot enforce the same exception-checking rules on Java exceptions raised in native methods. This gap makes Java software potentially buggy and often difficult to debug when an exception is raised in native code. In this paper, we propose a complete static-analysis framework called JET to extend exception-checking rules even on native code. The framework has a two-stage design where the first stage throws away a large portion of irrelevant code so that the second stage, a fine-grained analysis, can concentrate on a small set of code for accurate bug finding. This design achieves both high efficiency and accuracy. We have applied JET on a set of benchmark programs with a total over 227K lines of source code and identified 12 inconsistent native-method exception declarations.


title: SHERIFF: precise detection and automatic mitigation of false sharing

authors:
Tongping Liu
Emery D. Berger

abstract: False sharing is an insidious problem for multithreaded programs running on multicore processors, where it can silently degrade performance and scalability. Previous tools for detecting false sharing are severely limited: they cannot distinguish false sharing from true sharing, have high false positive rates, and provide limited assistance to help programmers locate and resolve false sharing.


title: Cedalion: a language for language oriented programming

authors:
David H. Lorenz
Boaz Rosenan

abstract: Language Oriented Programming (LOP) is a paradigm that puts domain specific programming languages (DSLs) at the center of the software development process. Currently, there are three main approaches to LOP: (1) the use of internal DSLs, implemented as libraries in a given host language; (2) the use of external DSLs, implemented as interpreters or compilers in an external language; and (3) the use of language workbenches, which are integrated development environments (IDEs) for defining and using external DSLs. In this paper, we contribute: (4) a novel language-oriented approach to LOP for defining and using internal DSLs. While language workbenches adapt internal DSL features to overcome some of the limitations of external DSLs, our approach adapts language workbench features to overcome some of the limitations of internal DSLs. We introduce Cedalion, an LOP host language for internal DSLs, featuring static validation and projectional editing. To validate our approach we present a case study in which Cedalion was used by biologists in designing a DNA microarray for molecular Biology research.


title: Delegated isolation

authors:
Roberto Lublinerman
Jisheng Zhao
Zoran Budimlic
Swarat Chaudhuri
Vivek Sarkar

abstract: Isolation---the property that a task can access shared data without interference from other tasks---is one of the most basic concerns in parallel programming. In this paper, we present Aida, a new model of isolated execution for parallel programs that perform frequent, irregular accesses to pointer-based shared data structures. The three primary benefits of Aida are dynamism, safety and liveness guarantees, and programmability. First, Aida allows tasks to dynamically select and modify, in an isolated manner, arbitrary fine-grained regions in shared data structures, all the while maintaining a high level of concurrency. Consequently, the model can achieve scalable parallelization of regular as well as irregular shared-memory applications. Second, the model offers freedom from data races, deadlocks, and livelocks. Third, no extra burden is imposed on programmers, who access the model via a simple, declarative isolation construct that is similar to that for transactional memory. The key new insight in Aida is a notion of delegation among concurrent isolated tasks (known in Aida as assemblies). Each assembly A is equipped with a region in the shared heap that it owns---the only objects accessed by A are those it owns, guaranteeing race-freedom. The region owned by A can grow or shrink flexibly---however, when A needs to own a datum owned by B, A delegates itself, as well as its owned region, to B. From now on, B has the responsibility of re-executing the task A set out to complete. Delegation as above is the only inter-assembly communication primitive in Aida. In addition to reducing contention in a local, data-driven manner, it guarantees freedom from deadlocks and livelocks.


title: Null dereference verification via over-approximated weakest pre-conditions analysis

authors:
Ravichandhran Madhavan
Raghavan Komondoor

abstract: Null dereferences are a bane of programming in languages such as Java. In this paper we propose a sound, demand-driven, inter-procedurally context-sensitive dataflow analysis technique to verify a given dereference as safe or potentially unsafe. Our analysis uses an abstract lattice of formulas to find a pre-condition at the entry of the program such that a null-dereference can occur only if the initial state of the program satisfies this pre-condition. We use a simplified domain of formulas, abstracting out integer arithmetic, as well as unbounded access paths due to recursive data structures. For the sake of precision we model aliasing relationships explicitly in our abstract lattice, enable strong updates, and use a limited notion of path sensitivity. For the sake of scalability we prune formulas continually as they get propagated, reducing to true conjuncts that are less likely to be useful in validating or invalidating the formula. We have implemented our approach, and present an evaluation of it on a set of ten real Java programs. Our results show that the set of design features we have incorporated enable the analysis to (a) explore long, inter-procedural paths to verify each dereference, with (b) reasonable accuracy, and (c) very quick response time per dereference, making it suitable for use in desktop development environments.


title: Backstage Java: making a difference in metaprogramming

authors:
Zachary Palmer
Scott F. Smith

abstract: We propose Backstage Java (BSJ), a Java language extension which allows algorithmic, contextually-aware generation and transformation of code. BSJ explicitly and concisely represents design patterns and other encodings by employing compile-time metaprogramming: a practice in which the programmer writes instructions which are executed over the program's AST during compilation. While compile-time metaprogramming has been successfully used in functional languages such as Template Haskell, a number of language properties (scope, syntactic structure, mutation, etc.) have thus far prevented this theory from translating to the imperative world. BSJ uses the novel approach of difference-based metaprogramming to provide an imperative programming style amenable to the Java community and to enforce that metaprograms are consistent and semantically unambiguous. To make the feasibility of BSJ metaprogramming evident, we have developed a compiler implementation and numerous working code examples.


title: A simple abstraction for complex concurrent indexes

authors:
Pedro da Rocha Pinto
Thomas Dinsdale-Young
Mike Dodds
Philippa Gardner
Mark J. Wheelhouse

abstract: Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes accessed concurrently. We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B-Link trees. The complexity of these algorithms, in particular the B-Link tree algorithm, can be completely hidden from the client's view by our abstract specification.


title: Synthesis of first-order dynamic programming algorithms

authors:
Yewen Pu
Rastislav Bodík
Saurabh Srivastava

abstract: To solve a problem with a dynamic programming algorithm, one must reformulate the problem such that its solution can be formed from solutions to overlapping subproblems. Because overlapping subproblems may not be apparent in the specification, it is desirable to obtain the algorithm directly from the specification. We describe a semi-automatic synthesizer of linear-time dynamic programming algorithms. The programmer supplies a declarative specification of the problem and the operators that might appear in the solution. The synthesizer obtains the algorithm by searching a space of candidate algorithms; internally, the search is implemented with constraint solving. The space of candidate algorithms is defined with a program template reusable across all linear-time dynamic programming algorithms, which we characterize as first-order recurrences. This paper focuses on how to write the template so that the constraint solving process scales to real-world linear-time dynamic programming algorithms. We show how to reduce the space with (i)~symmetry reduction and (ii)~domain knowledge of dynamic programming algorithms. We have synthesized algorithms for variants of maximal substring matching, an assembly-line optimization, and the extended Euclid algorithm. We have also synthesized a problem outside the class of first-order recurrences, by composing three instances of the algorithm template.


title: Exploiting coarse-grain speculative parallelism

authors:
Hari K. Pyla
Calvin J. Ribbens
Srinidhi Varadarajan

abstract: Speculative execution at coarse granularities (e.g., code-blocks, methods, algorithms) offers a promising programming model for exploiting parallelism on modern architectures. In this paper we present Anumita, a framework that includes programming constructs and a supporting runtime system to enable the use of coarse-grain speculation to improve program performance, without burdening the programmer with the complexity of creating, managing and retiring speculations. Speculations may be composed by specifying surrogate code blocks at any arbitrary granularity, which are then executed concurrently, with a single winner ultimately modifying program state. Anumita provides expressive semantics for winner selection that go beyond time to solution to include user-defined notions of quality of solution. Anumita can be used to improve the performance of hard to parallelize algorithms whose performance is highly dependent on input data. Anumita is implemented as a user-level runtime with programming interfaces to C, C++, Fortran and as an OpenMP extension. Performance results from several applications show the efficacy of using coarse-grain speculation to achieve (a) robustness when surrogates fail and (b) significant speedup over static algorithm choices.


title: Sprint: speculative prefetching of remote data

authors:
Arun Raman
Greta Yorsh
Martin T. Vechev
Eran Yahav

abstract: Remote data access latency is a significant performance bottleneck in many modern programs that use remote databases and web services. We present Sprint - a run-time system for optimizing such programs by prefetching and caching data from remote sources in parallel to the execution of the original program. Sprint separates the concerns of exposing potentially-independent data accesses from the mechanism for executing them efficiently in parallel or in a batch. In contrast to prior work, Sprint can efficiently prefetch data in the presence of irregular or input-dependent access patterns, while preserving the semantics of the original program.


title: Automated construction of JavaScript benchmarks

authors:
Gregor Richards
Andreas Gal
Brendan Eich
Jan Vitek

abstract: JavaScript is a highly dynamic language for web-based applications. Innovative implementation techniques for improving its speed and responsiveness have been developed in recent years. Industry benchmarks such as WebKit SunSpider are often cited as a measure of the efficacy of these techniques. However, recent studies have shown that these benchmarks fail to accurately represent the dynamic nature of modern JavaScript applications, and so may be poor predictors of real-world performance. Worse, they may guide the development of optimizations which are unhelpful for real applications. Our goal is to develop a tool and techniques to automate the creation of realistic and representative benchmarks from existing web applications. We propose a record-and-replay approach to capture JavaScript sessions which has sufficient fidelity to accurately recreate key characteristics of the original application, and at the same time is sufficiently flexible that a recording produced on one platform can be replayed on a different one. We describe JSBench, a flexible tool for workload capture and benchmark generation, and demonstrate its use in creating eight benchmarks based on popular sites. Using a variety of runtime metrics collected with instrumented versions of Firefox, Internet Explorer, and Safari, we show that workloads created by JSBench match the behavior of the original web applications.


title: Da capo con scala: design and analysis of a scala benchmark suite for the java virtual machine

authors:
Andreas Sewe
Mira Mezini
Aibek Sarimbekov
Walter Binder

abstract: Originally conceived as the target platform for Java alone, the Java Virtual Machine (JVM) has since been targeted by other languages, one of which is Scala. This trend, however, is not yet reflected by the benchmark suites commonly used in JVM research. In this paper, we thus present the design and analysis of the first full-fledged benchmark suite for Scala. We furthermore compare the benchmarks contained therein with those from the well-known DaCapo 9.12 benchmark suite and show where the differences are between Scala and Java code---and where not.


title: Testing atomicity of composed concurrent operations

authors:
Ohad Shacham
Nathan Grasso Bronson
Alex Aiken
Mooly Sagiv
Martin T. Vechev
Eran Yahav

abstract: We address the problem of testing atomicity of composed concurrent operations. Concurrent libraries help programmers exploit parallel hardware by providing scalable concurrent operations with the illusion that each operation is executed atomically. However, client code often needs to compose atomic operations in such a way that the resulting composite operation is also atomic while preserving scalability. We present a novel technique for testing the atomicity of client code composing scalable concurrent operations. The challenge in testing this kind of client code is that a bug may occur very rarely and only on a particular interleaving with a specific thread configuration. Our technique is based on modular testing of client code in the presence of an adversarial environment; we use commutativity specifications to drastically reduce the number of executions explored to detect a bug. We implemented our approach in a tool called COLT, and evaluated its effectiveness on a range of 51 real-world concurrent Java programs. Using COLT, we found 56 atomicity violations in Apache Tomcat, Cassandra, MyFaces Trinidad, and other applications.


title: Hybrid partial evaluation

authors:
Amin Shali
William R. Cook

abstract: Hybrid partial evaluation (HPE) is a pragmatic approach to partial evaluation that borrows ideas from both online and offline partial evaluation. HPE performs offline-style specialization using an online approach without static binding time analysis. The goal of HPE is to provide a practical and predictable level of optimization for programmers, with an implementation strategy that fits well within existing compilers or interpreters. HPE requires the programmer to specify where partial evaluation should be applied. It provides no termination guarantee and reports errors in situations that violate simple binding time rules, or have incorrect use of side effects in compile-time code. We formalize HPE for a small imperative object-oriented language and describe Civet, a straightforward implementation of HPE as a relatively simple extension of a Java compiler. Code optimized by Civet performs as well as the output of a state-of-the-art offline partial evaluator.


title: RoleCast: finding missing security checks when you do not know what checks are

authors:
Sooel Son
Kathryn S. McKinley
Vitaly Shmatikov

abstract: Web applications written in languages such as PHP and JSP are notoriously vulnerable to accidentally omitted authorization checks and other security bugs. Existing techniques that find missing security checks in library and system code assume that (1) security checks can be recognized syntactically and (2) the same pattern of checks applies universally to all programs. These assumptions do not hold for Web applications. Each Web application uses different variables and logic to check the user's permissions. Even within the application, security logic varies based on the user's role, e.g., regular users versus administrators. This paper describes ROLECAST, the first system capable of statically identifying security logic that mediates security-sensitive events (such as database writes) in Web applications, rather than taking a specification of this logic as input. We observe a consistent software engineering pattern-the code that implements distinct user role functionality and its security logic resides in distinct methods and files-and develop a novel algorithm for discovering this pattern in Web applications. Our algorithm partitions the set of file contexts (a coarsening of calling contexts) on which security-sensitive events are control dependent into roles. Roles are based on common functionality and security logic. ROLECAST identifies security-critical variables and applies rolespecific variable consistency analysis to find missing security checks. ROLECAST discovered 13 previously unreported, remotely exploitable vulnerabilities in 11 substantial PHP and JSP applications, with only 3 false positives.


title: F4F: taint analysis of framework-based web applications

authors:
Manu Sridharan
Shay Artzi
Marco Pistoia
Salvatore Guarnieri
Omer Tripp
Ryan Berg

abstract: This paper presents F4F (Framework For Frameworks), a system for effective taint analysis of framework-based web applications. Most modern web applications utilize one or more web frameworks, which provide useful abstractions for common functionality. Due to extensive use of reflective language constructs in framework implementations, existing static taint analyses are often ineffective when applied to framework-based applications. While previous work has included ad hoc support for certain framework constructs, adding support for a large number of frameworks in this manner does not scale from an engineering standpoint.


title: Freedom before commitment: a lightweight type system for object initialisation

authors:
Alexander J. Summers
Peter Müller

abstract: One of the main purposes of object initialisation is to establish invariants such as a field being non-null or an immutable data structure containing specific values. These invariants are then implicitly assumed by the rest of the implementation, for instance, to ensure that a field may be safely dereferenced or that immutable data may be accessed concurrently. Consequently, letting an object escape from its constructor is dangerous; the escaping object might not yet satisfy its invariants, leading to errors in code that relies on them. Nevertheless, preventing objects entirely from escaping from their constructors is too restrictive; it is often useful to call auxiliary methods on the object under initialisation or to pass it to another constructor to set up mutually-recursive structures.


title: First-class state change in plaid

authors:
Joshua Sunshine
Karl Naden
Sven Stork
Jonathan Aldrich
Éric Tanter

abstract: Objects model the world, and state is fundamental to a faithful modeling. Engineers use state machines to understand and reason about state transitions, but programming languages provide little support for building software based on state abstractions. We propose Plaid, a language in which objects are modeled not just in terms of classes, but in terms of changing abstract states. Each state may have its own representation, as well as methods that may transition the object into a new state. A formal model precisely defines the semantics of core Plaid constructs such as state transition and trait-like state composition. We evaluate Plaid through a series of examples taken from the Plaid compiler and the standard libraries of Smalltalk and Java. These examples show how Plaid can more closely model state-based designs, enhancing understandability, enhancing dynamic error checking, and providing reuse benefits.


title: The sequential prison

abstract: We are trapped in a sequential prison. We use sequential character strings to write sequential programs to control sequential computers. No wonder concurrency remains elusive. How did we come to be here? The high cost of vacuum tube logic forced sequence upon early computer builders. Sequential character strings were the economic way to describe what sequential computers should do. Sequential programs controlled the expensive part of the machine, namely logic. The lethargic pace of logic circuits masked the cost of moving data over distance, allowing programming languages to ignore the cost of communication. Today, the time delay and energy cost of communicating over distance dominate modern computers; logic is essentially free. Why then, do programming languages continue to control logic and largely ignore communication? It will take a broad effort to escape our sequential prison, requiring changes in hardware, programming notations and the ways in which they are expressed. Most importantly, it will require recognizing that we are in sequential prison, and planning for an escape.


title: Synthesizing method sequences for high-coverage testing

authors:
Suresh Thummalapenta
Tao Xie
Nikolai Tillmann
Jonathan de Halleux
Zhendong Su

abstract: High-coverage testing is challenging. Modern object-oriented programs present additional challenges for testing. One key difficulty is the generation of proper method sequences to construct desired objects as method parameters. In this paper, we cast the problem as an instance of program synthesis that automatically generates candidate programs to satisfy a user-specified intent. In our setting, candidate programs are method sequences, and desired object states specify an intent. Automatic generation of desired method sequences is difficult due to its large search space---sequences often involve methods from multiple classes and require specific primitive values. This paper introduces a novel approach, called Seeker, to intelligently navigate the large search space. Seeker synergistically combines static and dynamic analyses: (1) dynamic analysis generates method sequences to cover branches; (2) static analysis uses dynamic analysis information for not-covered branches to generate candidate sequences; and (3) dynamic analysis explores and eliminates statically generated sequences. For evaluation, we have implemented Seeker and demonstrate its effectiveness on four subject applications totalling 28K LOC. We show that Seeker achieves higher branch coverage and def-use coverage than existing state-of-the-art approaches. We also show that Seeker detects 34 new defects missed by existing tools.


title: A step towards transparent integration of input-consciousness into dynamic program optimizations

authors:
Kai Tian
Eddy Z. Zhang
Xipeng Shen

abstract: Dynamic program optimizations are critical for the efficiency of applications in managed programming languages and scripting languages. Recent studies have shown that exploitation of program inputs may enhance the effectiveness of dynamic optimizations significantly. However, current solutions for enabling the exploitation require either programmers' annotations or intensive offline profiling, impairing the practical adoption of the techniques.


title: A theory of substructural types and control

authors:
Jesse A. Tov
Riccardo Pucella

abstract: Exceptions are invaluable for structured error handling in high-level languages, but they are at odds with linear types. More generally, control effects may delete or duplicate portions of the stack, which, if we are not careful, can invalidate all substructural usage guarantees for values on the stack. We have developed a type-and-effect system that tracks control effects and ensures that values on the stack are never wrongly duplicated or dropped. We present the system first with abstract control effects and prove its soundness. We then give examples of three instantiations with particular control effects, including exceptions and delimited continuations, and show that they meet the soundness criteria for specific control effects.


title: HAWKEYE: effective discovery of dataflow impediments to parallelization

authors:
Omer Tripp
Greta Yorsh
John Field
Mooly Sagiv

abstract: Parallelization transformations are an important vehicle for improving the performance and scalability of a software system. Utilizing concurrency requires that the developer first identify a suitable parallelization scope: one that poses as a performance bottleneck, and at the same time, exhibits considerable available parallelism. However, having identified a candidate scope, the developer still needs to ensure the correctness of the transformation. This is a difficult undertaking, where a major source of complication lies in tracking down sequential dependencies that inhibit parallelization and addressing them.


title: Scalable join patterns

authors:
Aaron Joseph Turon
Claudio V. Russo

abstract: Coordination can destroy scalability in parallel programming. A comprehensive library of scalable synchronization primitives is therefore an essential tool for exploiting parallelism. Unfortunately, such primitives do not easily combine to yield solutions to more complex problems. We demonstrate that a concurrency library based on Fournet and Gonthier's join calculus can provide declarative and scalable coordination. By declarative, we mean that the programmer needs only to write down the constraints of a coordination problem, and the library will automatically derive a correct solution. By scalable, we mean that the derived solutions deliver robust performance both as the number of processors increases, and as the complexity of the coordination problem grows. We validate our claims empirically on seven coordination problems, comparing our generic solution to specialized algorithms from the literature.


title: Flexible object layouts: enabling lightweight language extensions by intercepting slot access

authors:
Toon Verwaest
Camillo Bruni
Mircea Lungu
Oscar Nierstrasz

abstract: Programming idioms, design patterns and application libraries often introduce cumbersome and repetitive boilerplate code to a software system. Language extensions and external DSLs (domain specific languages) are sometimes introduced to reduce the need for boilerplate code, but they also complicate the system by introducing the need for language dialects and inter-language mediation. To address this, we propose to extend the structural reflective model of the language with object layouts, layout scopes and slots. Based on the new reflective language model we can 1) provide behavioral hooks to object layouts that are triggered when the fields of an object are accessed and 2) simplify the implementation of state-related language extensions such as stateful traits. By doing this we show how many idiomatic use cases that normally require boilerplate code can be more effectively supported.


title: Accentuating the positive: atomicity inference and enforcement using correct executions

authors:
Dasarath Weeratunge
Xiangyu Zhang
Suresh Jagannathan

abstract: Concurrency bugs are often due to inadequate synchronization that fail to prevent specific (undesirable) thread interleavings. Such errors, often referred to as Heisenbugs, are difficult to detect, prevent, and repair. In this paper, we present a new technique to increase program robustness against Heisenbugs. We profile correct executions from provided test suites to infer fine-grained atomicity properties. Additional deadlock-free locking is injected into the program to guarantee these properties hold on production runs. Notably, our technique does not rely on witnessing or analyzing erroneous executions. The end result is a scheme that only permits executions which are guaranteed to preserve the atomicity properties derived from the profile. Evaluation results on large, real-world, open-source programs show that our technique can effectively suppress subtle concurrency bugs, with small runtime overheads (typically less than 15%).


title: Reducing trace selection footprint for large-scale Java applications without performance loss

authors:
Peng Wu
Hiroshige Hayashizaki
Hiroshi Inoue
Toshio Nakatani

abstract: When optimizing large-scale applications, striking the balance between steady-state performance, start-up time, and code size has always been a grand challenge. While recent advances in trace compilation have significantly improved the steady-state performance of trace JITs for large-scale Java applications, the size control aspect of a trace compilation system remains largely overlooked. For instance, using the DaCapo 9.12 benchmarks, we observe that 40% of traces selected by a state-of-the-art trace selection algorithm are short-lived and, on average, each selected basic block is replicated 13 times in the trace cache.


title: Safe and atomic run-time code evolution for Java and its application to dynamic AOP

authors:
Thomas Würthinger
Danilo Ansaloni
Walter Binder
Christian Wimmer
Hanspeter Mössenböck

abstract: Dynamic updates to running programs improve development productivity and reduce downtime of long-running applications. This feature is however severely limited in current virtual machines for object-oriented languages. In particular, changes to classes often apply only to methods invoked after a class change, but not to active methods on the call stack of threads. Additionally, adding and removing methods as well as fields is often not supported.


title: Why nothing matters: the impact of zeroing

authors:
Xi Yang
Stephen M. Blackburn
Daniel Frampton
Jennifer B. Sartor
Kathryn S. McKinley

abstract: Memory safety defends against inadvertent and malicious misuse of memory that may compromise program correctness and security. A critical element of memory safety is zero initialization. The direct cost of zero initialization is surprisingly high: up to 12.7%, with average costs ranging from 2.7 to 4.5% on a high performance virtual machine on IA32 architectures. Zero initialization also incurs indirect costs due to its memory bandwidth demands and cache displacement effects. Existing virtual machines either: a) minimize direct costs by zeroing in large blocks, or b) minimize indirect costs by zeroing in the allocation sequence, which reduces cache displacement and bandwidth. This paper evaluates the two widely used zero initialization designs, showing that they make different tradeoffs to achieve very similar performance. Our analysis inspires three better designs: (1) bulk zeroing with cache-bypassing (non-temporal) instructions to reduce the direct and indirect zeroing costs simultaneously, (2) concurrent non-temporal bulk zeroing that exploits parallel hardware to move work off the application's critical path, and (3) adaptive zeroing, which dynamically chooses between (1) and (2) based on available hardware parallelism. The new software strategies offer speedups sometimes greater than the direct overhead, improving total performance by 3% on average. Our findings invite additional optimizations and microarchitectural support.


title: Data-driven synthesis for object-oriented frameworks

authors:
Kuat Yessenov
Zhilei Xu
Armando Solar-Lezama

abstract: Software construction today often involves the use of large frameworks. The challenge in this type of programming is that object-oriented frameworks tend to grow exceedingly intricate; they spread functionality among numerous classes, and any use of the framework requires knowledge of many interacting components. We present a system named MATCHMAKER that from a simple query synthesizes code that interacts with the framework. The query consists of names of two framework classes, and our system produces code enabling interaction between them. MATCHMAKER relies on a database of dynamic program traces called DELIGHT that uses novel abstraction-based indexing techniques to answer queries about the evolution of heap connectivity in a matter of seconds.


title: Efficiently combining parallel software using fine-grained, language-level, hierarchical resource management policies

abstract: This paper presents Poli-C, a language extension, runtime library, and system daemon enabling fine-grained, language-level, hierarchical resource management policies. Poli-C is suitable for use in applications that compose parallel libraries, frameworks, and programs. In particular, we have added a powerful new statement to C for expressing resource limits and guarantees in such a way that programmers can set resource management policies even when the source code of parallel libraries and frameworks is not available. Poli-C enables application programmers to manage any resource exposed by the underlying OS, for example cores or IO bandwidth. Additionally, we have developed a domain-specific language for defining high-level resource management policies, and a facility for extending the kinds of resources that can be managed with our language extension. Finally, through a number of useful variations, our design offers a high degree of composability. We evaluate Poli-C by way of three case-studies: a scientific application, an image processing webserver, and a pair of parallel database join implementations. We found that using Poli-C yields efficiency gains that require the addition of only a few lines of code to applications.


title: k-Calling context profiling

authors:
Giorgio Ausiello
Camil Demetrescu
Irene Finocchi
Donatella Firmani

abstract: Calling context trees are one of the most fundamental data structures for representing the interprocedural control flow of a program, providing valuable information for program understanding and optimization. Nodes of a calling context tree associate performance metrics to whole distinct paths in the call graph starting from the root function. However, no explicit information is provided for detecting short hot sequences of activations, which may be a better optimization target in large modular programs where groups of related functions are reused in many different parts of the code. Furthermore, calling context trees can grow prohibitively large in some scenarios. Another classical approach, called edge profiling, collects performance metrics for caller-callee pairs in the call graph, allowing it to detect hot paths of fixed length one. We study a generalization of edge and context-sensitive profiles by introducing a novel data structure called k-calling context forest (k-CCF). Nodes in a k-CCF associate performance metrics to paths of length at most k that lead to each distinct routine of the program, providing edge profiles for k=1, full context-sensitive profiles for k equal to infinity, as well as any other intermediate point in the spectrum. We study the properties of the k-CCF both theoretically and experimentally on a large suite of prominent Linux applications, showing how to construct it efficiently and discussing its relationships with the calling context tree. Our experiments show that the k-CCF can provide effective space-accuracy tradeoffs for interprocedural contextual profiling, yielding useful clues to the hot spots of a program that may be hidden in a calling context tree and using less space for small values of k, which appear to be the most interesting in practice.


title: White box sampling in uncertain data processing enabled by program analysis

authors:
Tao Bao
Yunhui Zheng
Xiangyu Zhang

abstract: Sampling is a very important and low-cost approach to uncertain data processing, in which output variations caused by input errors are sampled. Traditional methods tend to treat a program as a blackbox. In this paper, we show that through program analysis, we can expose the internals of sample executions so that the process can become more selective and focused. In particular, we develop a sampling runtime that can selectively sample in input error bounds to expose discontinuity in output functions. It identifies all the program factors that can potentially lead to discontinuity and hash the values of such factors during execution in a cost-effective way. The hash values are used to guide the sampling process. Our results show that the technique is very effective for real-world programs. It can achieve the precision of a high sampling rate with the cost of a lower sampling rate.


title: AutoMan: a platform for integrating human-based and digital computation

authors:
Daniel W. Barowy
Charlie Curtsinger
Emery D. Berger
Andrew McGregor

abstract: Humans can perform many tasks with ease that remain difficult or impossible for computers. Crowdsourcing platforms like Amazon's Mechanical Turk make it possible to harness human-based computational power at an unprecedented scale. However, their utility as a general-purpose computational platform remains limited. The lack of complete automation makes it difficult to orchestrate complex or interrelated tasks. Scheduling more human workers to reduce latency costs real money, and jobs must be monitored and rescheduled when workers fail to complete their tasks. Furthermore, it is often difficult to predict the length of time and payment that should be budgeted for a given task. Finally, the results of human-based computations are not necessarily reliable, both because human skills and accuracy vary widely, and because workers have a financial incentive to minimize their effort.


title: GPUVerify: a verifier for GPU kernels

authors:
Adam Betts
Nathan Chong
Alastair F. Donaldson
Shaz Qadeer
Paul Thomson

abstract: We present a technique for verifying race- and divergence-freedom of GPU kernels that are written in mainstream kernel programming languages such as OpenCL and CUDA. Our approach is founded on a novel formal operational semantics for GPU programming termed synchronous, delayed visibility (SDV) semantics. The SDV semantics provides a precise definition of barrier divergence in GPU kernels and allows kernel verification to be reduced to analysis of a sequential program, thereby completely avoiding the need to reason about thread interleavings, and allowing existing modular techniques for program verification to be leveraged. We describe an efficient encoding for data race detection and propose a method for automatically inferring loop invariants required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, which can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 163 kernels drawn from public and commercial sources. Our evaluation demonstrates that GPUVerify is capable of efficient, automatic verification of a large number of real-world kernels.

awards: Most Influential OOPSLA Paper (awarded 2022)


title: Molecule: using monadic and streaming I/O to compose process networks on the JVM

authors:
Sébastien Bocq
Koen Daenen

abstract: Molecule is a domain specific language library embedded in Scala for easing the creation of scalable and modular concurrent applications on the JVM. Concurrent applications are modeled as parallel process networks that exchange information over mobile and type-safe messaging interfaces. In this paper, we present a concurrent programming environment that combines functional and imperative programming. Using a monad, we structure the sequential or parallel coordination of user-level threads, without JVM modifications or compiler support. Our mobile channel interfaces expose reusable and parallelizable higher-order functions, as if they were streams in a lazily evaluated functional programming language. The support for graceful termination of entire process networks is simplified by integrating channel poisoning with monadic exceptions and resource control. Our runtime and system-level interfaces leverage message batching and a novel flow parallel scheduler to limit expensive context switches in multicore environments. We illustrate the expressiveness and performance benefits on a 24-core AMD Opteron machine with three classical examples: a thread ring, a genuine prime sieve and a chameneos-redux.


title: On the benefits and pitfalls of extending a statically typed language JIT compiler for dynamic scripting languages

authors:
José G. Castaños
David Edelsohn
Kazuaki Ishizaki
Priya Nagpurkar
Toshio Nakatani
Takeshi Ogasawara
Peng Wu

abstract: Whenever the need to compile a new dynamically typed language arises, an appealing option is to repurpose an existing statically typed language Just-In-Time (JIT) compiler (repurposed JIT compiler). Existing repurposed JIT compilers (RJIT compilers), however, have not yet delivered the hoped-for performance boosts. The performance of JVM languages, for instance, often lags behind standard interpreter implementations. Even more customized solutions that extend the internals of a JIT compiler for the target language compete poorly with those designed specifically for dynamically typed languages. Our own Fiorano JIT compiler is an example of this problem. As a state-of-the-art, RJIT compiler for Python, the Fiorano JIT compiler outperforms two other RJIT compilers (Unladen Swallow and Jython), but still shows a noticeable performance gap compared to PyPy, today's best performing Python JIT compiler. In this paper, we discuss techniques that have proved effective in the Fiorano JIT compiler as well as limitations of our current implementation. More importantly, this work offers the first in-depth look at benefits and limitations of the repurposed JIT compiler approach. We believe the most common pitfall of existing RJIT compilers is not focusing sufficiently on specialization, an abundant optimization opportunity unique to dynamically typed languages. Unfortunately, the lack of specialization cannot be overcome by applying traditional optimizations.


title: Dependent types for JavaScript

authors:
Ravi Chugh
David Herman
Ranjit Jhala

abstract: We present Dependent JavaScript (DJS), a statically typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources, including the popular book JavaScript: The Good Parts and the SunSpider benchmark suite.


title: Energy types

authors:
Michael Cohen
Haitao Steve Zhu
Senem Ezgi Emgin
Yu David Liu

abstract: This paper presents a novel type system to promote and facilitate energy-aware programming. Energy Types is built upon a key insight into today's energy-efficient systems and applications: despite the popular perception that energy and power can only be described in joules and watts, real-world energy management is often based on discrete phases and modes, which in turn can be reasoned about by type systems very effectively. A phase characterizes a distinct pattern of program workload, and a mode represents an energy state the program is expected to execute in. This paper describes a programming model where phases and modes can be intuitively specified by programmers or inferred by the compiler as type information. It demonstrates how a type-based approach to reasoning about phases and modes can help promote energy efficiency. The soundness of our type system and the invariants related to inter-phase and inter-mode interactions are rigorously proved. Energy Types is implemented as the core of a prototyped object-oriented language ET for smartphone programming. Preliminary studies show ET can lead to significant energy savings for Android Apps.


title: An abstract interpretation framework for refactoring with application to extract methods with contracts

authors:
Patrick Cousot
Radhia Cousot
Francesco Logozzo
Michael Barnett

abstract: Method extraction is a common refactoring feature provided by most modern IDEs. It replaces a user-selected piece of code with a call to an automatically generated method. We address the problem of automatically inferring contracts (precondition, postcondition) for the extracted method. We require the inferred contract: (a) to be valid for the extracted method (validity); (b) to guard the language and programmer assertions in the body of the extracted method by an opportune precondition (safety); (c) to preserve the proof of correctness of the original code when analyzing the new method separately (completeness); and (d) to be the most general possible (generality). These requirements rule out trivial solutions (e.g., inlining, projection, etc). We propose two theoretical solutions to the problem. The first one is simple and optimal. It is valid, safe, complete and general but unfortunately not effectively computable (except for unrealistic finiteness/decidability hypotheses). The second one is based on an iterative forward/backward method. We show it to be valid, safe, and, under reasonable assumptions, complete and general. We prove that the second solution subsumes the first. All justifications are provided with respect to a new, set-theoretic version of Hoare logic (hence without logic), and abstractions of Hoare logic, revisited to avoid surprisingly unsound inference rules.


title: Talk versus work: characteristics of developer collaboration on the jazz platform

authors:
Subhajit Datta
Renuka Sindhgatta
Bikram Sengupta

abstract: IBM's Jazz initiative offers a state-of-the-art collaborative development environment (CDE) facilitating developer interactions around interdependent units of work. In this paper, we analyze development data across two versions of a major IBM product developed on the Jazz platform, covering in total 19 months of development activity, including 17,000+ work items and 61,000+ comments made by more than 190 developers in 35 locations. By examining the relation between developer talk and work, we find evidence that developers maintain a reasonably high level of connectivity with peer developers with whom they share work dependencies, but the span of a developer's communication goes much beyond the known dependencies of his/her work items. Using multiple linear regression models, we find that the number of defects owned by a developer is impacted by the number of other developers (s)he is connected through talk, his/her interpersonal influence in the network of work dependencies, the number of work items (s)he comments on, and the number work items (s)he owns. These effects are maintained even after controlling for workload, role, work dependency, and connection related factors. We discuss the implications of our results for collaborative software development and project governance.


title: Taming MATLAB

authors:
Anton Willy Dubrau
Laurie J. Hendren

abstract: MATLAB is a dynamic scientific language used by scientists, engineers and students worldwide. Although MATLAB is very suitable for rapid prototyping and development, MATLAB users often want to convert their final MATLAB programs to a static language such as FORTRAN. This paper presents an extensible object-oriented toolkit for supporting the generation of static programs from dynamic MATLAB programs. Our open source toolkit, called the MATLAB Tamer, identifies a large tame subset of MATLAB, supports the generation of a specialized Tame IR for that subset, provides a principled approach to handling the large number of builtin MATLAB functions, and supports an extensible interprocedural value analysis for estimating MATLAB types and call graphs.


title: IFRit: interference-free regions for dynamic data-race detection

authors:
Laura Effinger-Dean
Brandon Lucia
Luis Ceze
Dan Grossman
Hans-Juergen Boehm

abstract: We propose a new algorithm for dynamic data-race detection. Our algorithm reports no false positives and runs on arbitrary C and C++ code. Unlike previous algorithms, we do not have to instrument every memory access or track a full happens-before relation. Our data-race detector, which we call IFRit, is based on a run-time abstraction called an interference-free region (IFR). An IFR is an interval of one thread's execution during which any write to a specific variable by a different thread is a data race. We insert instrumentation at compile time to monitor active IFRs at run-time. If the runtime observes overlapping IFRs for conflicting accesses to the same variable in two different threads, it reports a race. The static analysis aggregates information for multiple accesses to the same variable, avoiding the expense of having to instrument every memory access in the program.


title: Uniqueness and reference immutability for safe parallelism

authors:
Colin S. Gordon
Matthew J. Parkinson
Jared Parsons
Aleks Bromfield
Joe Duffy

abstract: A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-effects. We provide a novel combination of immutable and unique (isolated) types that ensures safe parallelism (race freedom and deterministic execution). The type system includes support for polymorphism over type qualifiers, and can easily create cycles of immutable objects. Key to the system's flexibility is the ability to recover immutable or externally unique references after violating uniqueness without any explicit alias tracking. Our type system models a prototype extension to C# that is in active use by a Microsoft team. We describe their experiences building large systems with this extension. We prove the soundness of the type system by an embedding into a program logic.


title: Reusing debugging knowledge via trace-based bug search

authors:
Zhongxian Gu
Earl T. Barr
Drew Schleck
Zhendong Su

abstract: Some bugs, among the millions that exist, are similar to each other. One bug-fixing tactic is to search for similar bugs that have been reported and resolved in the past. A fix for a similar bug can help a developer understand a bug, or even directly fix it. Studying bugs with similar symptoms, programmers may determine how to detect or resolve them. To speed debugging, we advocate the systematic capture and reuse of debugging knowledge, much of which is currently wasted. The core challenge here is how to search for similar bugs. To tackle this problem, we exploit semantic bug information in the form of execution traces, which precisely capture bug semantics. This paper introduces novel tool and language support for semantically querying and analyzing bugs. We describe OSCILLOSCOPE, an Eclipse plugin, that uses a bug trace to exhaustively search its database for similar bugs and return their bug reports. OSCILLOSCOPE displays the traces of the bugs it returns against the trace of the target bug, so a developer can visually examine the quality of the matches. OSCILLOSCOPE rests on our bug query language (BQL), a flexible query language over traces. To realize OSCILLOSCOPE, we developed an open infrastructure that consists of a trace collection engine, BQL, a Hadoop-based query engine for BQL, a trace-indexed bug database, as well as a web-based frontend. OSCILLOSCOPE records and uploads bug traces to its infrastructure; it does so automatically when a JUnit test fails. We evaluated OSCILLOSCOPE on bugs collected from popular open-source projects. We show that OSCILLOSCOPE accurately and efficiently finds similar bugs, some of which could have been immediately used to fix open bugs.


title: Kitsune: efficient, general-purpose dynamic software updating for C

authors:
Christopher M. Hayden
Edward K. Smith
Michail Denchev
Michael Hicks
Jeffrey S. Foster

abstract: Dynamic software updating (DSU) systems allow programs to be updated while running, thereby permitting developers to add features and fix bugs without downtime. This paper introduces Kitsune, a new DSU system for C whose design has three notable features. First, Kitsune's updating mechanism updates the whole program, not individual functions. This mechanism is more flexible than most prior approaches and places no restrictions on data representations or allowed compiler optimizations. Second, Kitsune makes the important aspects of updating explicit in the program text, making the program's semantics easy to understand while minimizing programmer effort. Finally, the programmer can write simple specifications to direct Kitsune to generate code that traverses and transforms old-version state for use by new code; such state transformation is often necessary, and is significantly more difficult in prior DSU systems. We have used Kitsune to update five popular, open-source, single- and multi-threaded programs, and find that few program changes are required to use Kitsune, and that it incurs essentially no performance overhead.


title: Reim & ReImInfer: checking and inference of reference immutability and method purity

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

abstract: Reference immutability ensures that a reference is not used to modify the referenced object, and enables the safe sharing of object structures. A pure method does not cause side-effects on the objects that existed in the pre-state of the method execution. Checking and inference of reference immutability and method purity enables a variety of program analyses and optimizations. We present ReIm, a type system for reference immutability, and ReImInfer, a corresponding type inference analysis. The type system is concise and context-sensitive. The type inference analysis is precise and scalable, and requires no manual annotations. In addition, we present a novel application of the reference immutability type system: method purity inference.


title: LEAN: simplifying concurrency bug reproduction via replay-supported execution reduction

authors:
Jeff Huang
Charles Zhang

abstract: Debugging concurrent programs is known to be difficult due to scheduling non-determinism. The technique of multiprocessor deterministic replay substantially assists debugging by making the program execution reproducible. However, facing the huge replay traces and long replay time, the debugging task remains stunningly challenging for long running executions. We present a new technique, LEAN, on top of replay, that significantly reduces the complexity of the replay trace and the length of the replay time without losing the determinism in reproducing concurrency bugs. The cornerstone of our work is a redundancy criterion that characterizes the redundant computation in a buggy trace. Based on the redundancy criterion, we have developed two novel techniques to automatically identify and remove redundant threads and instructions in the bug reproduction execution. Our evaluation results with several real world concurrency bugs in large complex server programs demonstrate that LEAN is able to reduce the size, the number of threads, and the number of thread context switches of the replay trace by orders of magnitude, and accordingly greatly shorten the replay time.


title: Execution privatization for scheduler-oblivious concurrent programs

abstract: Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious: their execution is deterministic, regardless of the scheduling behavior. We present and formally prove a fundamental observation of the privatizability property for scheduler-oblivious programs, that paves the theoretical foundation for privatizing shared data accesses on a path segment. With privatization, the non-deterministic thread interleavings on the privatized accesses are isolated and as the consequence many concurrency problems are alleviated. We further present a path and context sensitive privatization algorithm that safely privatizes the program without introducing any additional program behavior. Our evaluation results show that the privatization opportunity pervasively exists in real world large complex concurrent systems. Through privatization, several real concurrency bugs are fixed and notable performance improvements are also achieved on benchmarks.


title: Integrating task parallelism with actors

authors:
Shams Mahmood Imam
Vivek Sarkar

abstract: This paper introduces a unified concurrent programming model combining the previously developed Actor Model (AM) and the task-parallel Async-Finish Model (AFM). With the advent of multi-core computers, there is a renewed interest in programming models that can support a wide range of parallel programming patterns. The proposed unified model shows how the divide-and-conquer approach of the AFM and the no-shared mutable state and event-driven philosophy of the AM can be combined to solve certain classes of problems more efficiently and productively than either of the aforementioned models individually. The unified model adds actor creation and coordination to the AFM, while also enabling parallelization within actors. This paper describes two implementations of the unified model as extensions of Habanero-Java and Habanero-Scala. The unified model adds to the foundations of parallel programs, and to the tools available for the programmer to aid in productivity and performance while developing parallel software.


title: Adaptive multi-level compilation in a trace-based Java JIT compiler

authors:
Hiroshi Inoue
Hiroshige Hayashizaki
Peng Wu
Toshio Nakatani

abstract: This paper describes our multi-level compilation techniques implemented in a trace-based Java JIT compiler (trace-JIT). Like existing multi-level compilation for method-based compilers, we start JIT compilation with a small compilation scope and a low optimization level so the program can start running quickly. Then we identify hot paths with a timer-based sampling profiler, generate long traces that capture the hot paths, and recompile them with a high optimization level to improve the peak performance. A key to high performance is selecting long traces that effectively capture the entire hot paths for upgrade recompilations. To do this, we introduce a new technique to generate a directed graph representing the control flow, a TTgraph, and use the TTgraph in the trace selection engine to efficiently select long traces. We show that our multi-level compilation improves the peak performance of programs by up to 58.5% and 22.2% on average compared to compiling all of the traces only at a low optimization level. Comparing the performance with our multi-level compilation to the performance when compiling all of the traces at a high optimization level, our technique can reduce the startup times of programs by up to 61.1% and 31.3% on average without significant reduction in the peak performance. Our results show that our adaptive multi-level compilation can balance the peak performance and startup time by taking advantage of different optimization levels.


title: Automatically enhancing locality for tree traversals with traversal splicing

authors:
Youngjoon Jo
Milind Kulkarni

abstract: Generally applicable techniques for improving temporal locality in irregular programs, which operate over pointer-based data structures such as trees and graphs, are scarce. Focusing on a subset of irregular programs, namely, tree traversal algorithms like Barnes-Hut and nearest neighbor, previous work has proposed point blocking, a technique analogous to loop tiling in regular programs, to improve locality. However point blocking is highly dependent on point sorting, a technique to reorder points so that consecutive points will have similar traversals. Performing this a priori sort requires an understanding of the semantics of the algorithm and hence highly application specific techniques. In this work, we propose traversal splicing, a new, general, automatic locality optimization for irregular tree traversal codes, that is less sensitive to point order, and hence can deliver substantially better performance, even in the absence of semantic information. For six benchmark algorithms, we show that traversal splicing can deliver single-thread speedups of up to 9.147 (geometric mean: 3.095) over baseline implementations, and up to 4.752 (geometric mean: 2.079) over point-blocked implementations. Further, we show that in many cases, automatically applying traversal splicing to a baseline implementation yields performance that is better than carefully hand-optimized implementations.


title: A black-box approach to understanding concurrency in DaCapo

authors:
Tomas Kalibera
Matthew Mole
Richard E. Jones
Jan Vitek

abstract: Increasing levels of hardware parallelism are one of the main challenges for programmers and implementers of managed runtimes. Any concurrency or scalability improvements must be evaluated experimentally. However, application benchmarks available today may not reflect the highly concurrent applications we anticipate in the future. They may also behave in ways that VM developers do not expect. We provide a set of platform independent concurrency related metrics and an in-depth observational study of current state of the art benchmarks, discovering how concurrent they really are, how they scale the work and how they synchronise and communicate via shared memory.


title: Formal specification of a JavaScript module system

authors:
Seonghoon Kang
Sukyoung Ryu

abstract: The JavaScript programming language, originally developed as a simple scripting language, is now the language of choice for web applications. All the top 100 sites on the web use JavaScript and its use outside web pages is rapidly growing. However, JavaScript is not yet ready for programming in the large: it does not support a module system. Lack of namespaces introduces module patterns, and makes it difficult to use multiple JavaScript frameworks together.


title: A variability-aware module system

authors:
Christian Kästner
Klaus Ostermann
Sebastian Erdweg

abstract: Module systems enable a divide and conquer strategy to software development. To implement compile-time variability in software product lines, modules can be composed in different combinations. However, this way, variability dictates a dominant decomposition. As an alternative, we introduce a variability-aware module system that supports compile-time variability inside a module and its interface. So, each module can be considered a product line that can be type checked in isolation. Variability can crosscut multiple modules. The module system breaks with the antimodular tradition of a global variability model in product-line development and provides a path toward software ecosystems and product lines of product lines developed in an open fashion. We discuss the design and implementation of such a module system on a core calculus and provide an implementation for C as part of the TypeChef project. Our implementation supports variability inside modules from #ifdef preprocessor directives and variable linking at the composition level. With our implementation, we type check all configurations of all modules of the open source product line Busybox with 811~compile-time options, perform linker check of all configurations, and report found type and linker errors -- without resorting to a brute-force strategy.


title: Bolt: on-demand infinite loop escape in unmodified binaries

authors:
Michael Kling
Sasa Misailovic
Michael Carbin
Martin C. Rinard

abstract: We present Bolt, a novel system for escaping from infinite and long-running loops. Directed by a user, Bolt can attach to a running process and determine if the program is executing an infinite loop. If so, Bolt can deploy multiple strategies to escape the loop, restore the responsiveness of the program, and enable the program to deliver useful output.


title: Mitigating the compiler optimization phase-ordering problem using machine learning

authors:
Sameer Kulkarni
John Cavazos

abstract: Today's compilers have a plethora of optimizations to choose from, and the correct choice of optimizations can have a significant impact on the performance of the code being optimized. Furthermore, choosing the correct order in which to apply those optimizations has been a long standing problem in compilation research. Each of these optimizations interacts with the code and in turn with all other optimizations in complicated ways. Traditional compilers typically apply the same set of optimization in a fixed order to all functions in a program, without regard the code being optimized.


title: Work-stealing without the baggage

authors:
Vivek Kumar
Daniel Frampton
Stephen M. Blackburn
David Grove
Olivier Tardieu

abstract: Work-stealing is a promising approach for effectively exploiting software parallelism on parallel hardware. A programmer who uses work-stealing explicitly identifies potential parallelism and the runtime then schedules work, keeping otherwise idle hardware busy while relieving overloaded hardware of its burden. Prior work has demonstrated that work-stealing is very effective in practice. However, work-stealing comes with a substantial overhead: as much as 2x to 12x slowdown over orthodox sequential code.


title: Program extrapolation with jennisys

authors:
K. Rustan M. Leino
Aleksandar Milicevic

abstract: The desired behavior of a program can be described using an abstract model. Compiling such a model into executable code requires advanced compilation techniques known as synthesis. This paper presents an object-based language, called Jennisys, where programming is done by introducing an abstract model, defining a concrete data representation for the model, and then being aided by automatic synthesis to produce executable code. The paper also presents a synthesis technique for the language. The technique is built on an automatic program verifier that, via an underlying SMT solver, is capable of providing concrete models to failed verifications. The technique proceeds by obtaining sample input/output values from concrete models and then extrapolating programs from the sample points. The synthesis aims to produce code with assignments, branching structure, and possibly recursive calls. It is the first to synthesize code that creates and uses objects in dynamic data structures or aggregate objects. A prototype of the language and synthesis technique has been implemented.


title: From clarity to efficiency for distributed algorithms

authors:
Yanhong A. Liu
Scott D. Stoller
Bo Lin
Michael Gorbovitski

abstract: This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly.


title: Modular and verified automatic program repair

authors:
Francesco Logozzo
Thomas Ball

abstract: We study the problem of suggesting code repairs at design time, based on the warnings issued by modular program verifiers. We introduce the concept of a verified repair, a change to a program's source that removes bad execution traces while increasing the number of good traces, where the bad/good traces form a partition of all the traces of a program. Repairs are property-specific. We demonstrate our framework in the context of warnings produced by the modular cccheck (a.k.a. Clousot) abstract interpreter, and generate repairs for missing contracts, incorrect locals and objects initialization, wrong conditionals, buffer overruns, arithmetic overflow and incorrect floating point comparisons. We report our experience with automatically generating repairs for the .NET framework libraries, generating verified repairs for over 80% of the warnings generated by cccheck.


title: Detecting problematic message sequences and frequencies in distributed systems

authors:
Charles Lucas
Sebastian G. Elbaum
David S. Rosenblum

abstract: Testing the components of a distributed system is challenging as it requires consideration of not just the state of a component, but also the sequence of messages it may receive from the rest of the system or the environment. Such messages may vary in type and content, and more particularly, in the frequency at which they are generated. All of these factors, in the right combination, may lead to faulty behavior. In this paper we present an approach to address these challenges by systematically analyzing a component in a distributed system to identify specific message sequences and frequencies at which a failure can occur. At the core of the analysis is the generation of a test driver that defines the space of message sequences to be generated, the exploration of that space through the use of dynamic symbolic execution, and the timing and analysis of the generated tests to identify problematic frequencies. We implemented our approach in the context of the popular Robotic Operating System and investigated its application to three systems of increasing complexity.