title: Automating object transformations for dynamic software updating

authors:
Stephen Magill
Michael Hicks
Suriya Subramanian
Kathryn S. McKinley

abstract: Dynamic software updating (DSU) systems eliminate costly downtime by dynamically fixing bugs and adding features to executing programs. Given a static code patch, most DSU systems construct runtime code changes automatically. However, a dynamic update must also specify how to change the running program's execution state, e.g., the stack and heap, to make it compatible with the new code. Constructing such state transformations correctly and automatically remains an open problem. This paper presents a solution called Targeted Object Synthesis (TOS). TOS first executes the same tests on the old and new program versions separately, observing the program heap state at a few corresponding points. Given two corresponding heap states, TOS matches objects in the two versions using key fields that uniquely identify objects and correlate old and new-version objects. Given example object pairs, TOS then synthesizes the simplest-possible function that transforms an old-version object to its new-version counterpart. We show that TOS is effective on updates to four open-source server programs for which it generates non-trivial transformation functions that use conditionals, operate on collections, and fix memory leaks. These transformations help programmers understand their changes and apply dynamic software updates.


venue: oopsla

title: An empirical study of the influence of static type systems on the usability of undocumented software

authors:
Clemens Mayer
Stefan Hanenberg
Romain Robbes
Éric Tanter
Andreas Stefik

abstract: Abstract Although the study of static and dynamic type systems plays a major role in research, relatively little is known about the impact of type systems on software development. Perhaps one of the more common arguments for static type systems in languages such as Java or C++ is that they require developers to annotate their code with type names, which is thus claimed to improve the documentation of software. In contrast, one common argument against static type systems is that they decrease flexibility, which may make them harder to use. While these arguments are found in the literature, rigorous empirical evidence is lacking. We report on a controlled experiment where 27 subjects performed programming tasks on an undocumented API with a static type system (requiring type annotations) as well as a dynamic type system (which does not). Our results show that for some tasks, programmers had faster completion times using a static type system, while for others, the opposite held. We conduct an exploratory study to try and theorize why.


title: Eval begone!: semi-automated removal of eval from javascript programs

authors:
Fadi Meawad
Gregor Richards
Floréal Morandat
Jan Vitek

abstract: Eval endows JavaScript developers with great power. It allows developers and end-users, by turning text into executable code, to seamlessly extend and customize the behavior of deployed applications as they are running. With great power comes great responsibility, though not in our experience. In previous work we demonstrated through a large corpus study that programmers wield that power in rather irresponsible and arbitrary ways. We showed that most calls to eval fall into a small number of very predictable patterns. We argued that those patterns could easily be recognized by an automated algorithm and that they could almost always be replaced with safer JavaScript idioms. In this paper we set out to validate our claim by designing and implementing a tool, which we call Evalorizer, that can assist programmers in getting rid of their unneeded evals. We use the tool to remove eval from a real-world website and validated our approach over logs taken from the top 100 websites with a success rate over 97% under an open world assumption.


title: Typestate-based semantic code search over partial programs

authors:
Alon Mishne
Sharon Shoham
Eran Yahav

abstract: We present a novel code search approach for answering queries focused on API-usage with code showing how the API should be used. To construct a search index, we develop new techniques for statically mining and consolidating temporal API specifications from code snippets. In contrast to existing semantic-based techniques, our approach handles partial programs in the form of code snippets. Handling snippets allows us to consume code from various sources such as parts of open source projects, educational resources (e.g. tutorials), and expert code sites. To handle code snippets, our approach (i) extracts a possibly partial temporal specification from each snippet using a relatively precise static analysis tracking a generalized notion of typestate, and (ii) consolidates the partial temporal specifications, combining consistent partial information to yield consolidated temporal specifications, each of which captures a full(er) usage scenario.


title: Towards a practical secure concurrent language

authors:
Stefan K. Muller
Stephen Chong

abstract: We demonstrate that a practical concurrent language can be extended in a natural way with information security mechanisms that provably enforce strong information security guarantees. We extend the X10 concurrent programming language with coarse-grained information-flow control. Central to X10 concurrency abstractions is the notion of a place: a container for data and computation. We associate a security level with each place, and restrict each place to store only data appropriate for that security level. When places interact only with other places at the same security level, then our security mechanisms impose no restrictions. When places of differing security levels interact, our information security analysis prevents potentially dangerous information flows, including information flow through covert scheduling channels. The X10 concurrency mechanisms simplify reasoning about information flow in concurrent programs. We present a static analysis that enforces a noninterference-based extensional information security condition in a calculus that captures the key aspects of X10's place abstraction and async-finish parallelism. We extend this security analysis to support many of X10's language features, and have implemented a prototype compiler for the resulting language.


title: Speculative analysis of integrated development environment recommendations

authors:
Kivanç Muslu
Yuriy Brun
Reid Holmes
Michael D. Ernst
David Notkin

abstract: Modern integrated development environments make recommendations and automate common tasks, such as refactorings, auto-completions, and error corrections. However, these tools present little or no information about the consequences of the recommended changes. For example, a rename refactoring may: modify the source code without changing program semantics; modify the source code and (incorrectly) change program semantics; modify the source code and (incorrectly) create compilation errors; show a name collision warning and require developer input; or show an error and not change the source code. Having to compute the consequences of a recommendation -- either mentally or by making source code changes -- puts an extra burden on the developers. This paper aims to reduce this burden with a technique that informs developers of the consequences of code transformations. Using Eclipse Quick Fix as a domain, we describe a plug-in, Quick Fix Scout, that computes the consequences of Quick Fix recommendations. In our experiments, developers completed compilation-error removal tasks 10% faster when using Quick Fix Scout than Quick Fix, although the sample size was not large enough to show statistical significance.


title: Predicate abstraction of Java programs with collections

authors:
Pavel Parízek
Ondrej Lhoták

abstract: Our goal is to develop precise and scalable verification techniques for Java programs that use collections and properties that depend on their content. We apply the popular approach of predicate abstraction to Java programs and collections. The main challenge in this context is precise and compact modeling of collections that enables practical verification. We define a predicate language for modeling the observable state of Java collections at the interface level. Changes of the state by API methods are captured by weakest preconditions. We adapt existing techniques for construction of abstract programs. Most notably, we designed optimizations based on specific features of the predicate language. We evaluated our approach on Java programs that use collections in advanced ways. Our results show that interesting properties, such as consistency between multiple collections, can be verified using our approach. The properties are specified using logic formulas that involve predicates introduced by our language.


title: Elixir: a system for synthesizing concurrent graph programs

authors:
Dimitrios Prountzos
Roman Manevich
Keshav Pingali

abstract: Algorithms in new application areas like machine learning and network analysis use "irregular" data structures such as graphs, trees and sets. Writing efficient parallel code in these problem domains is very challenging because it requires the programmer to make many choices: a given problem can usually be solved by several algorithms, each algorithm may have many implementations, and the best choice of algorithm and implementation can depend not only on the characteristics of the parallel platform but also on properties of the input data such as the structure of the graph. One solution is to permit the application programmer to experiment with different algorithms and implementations without writing every variant from scratch. Auto-tuning to find the best variant is a more ambitious solution. These solutions require a system for automatically producing efficient parallel implementations from high-level specifications. Elixir, the system described in this paper, is the first step towards this ambitious goal. Application programmers write specifications that consist of an operator, which describes the computations to be performed, and a schedule for performing these computations. Elixir uses sophisticated inference techniques to produce efficient parallel code from such specifications.


title: Checking reachability using matching logic

authors:
Grigore Rosu
Andrei Stefanescu

abstract: This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is language-independent and consists of eight proof rules. The proof system is proved partially correct and relatively complete (with respect to the programming language configuration model). To show its practicality, the generic framework is instantiated with a fragment of C and evaluated with encouraging results.


title: Exploring multi-threaded Java application performance on multicore hardware

authors:
Jennifer B. Sartor
Lieven Eeckhout

abstract: While there have been many studies of how to schedule applications to take advantage of increasing numbers of cores in modern-day multicore processors, few have focused on multi-threaded managed language applications which are prevalent from the embedded to the server domain. Managed languages complicate performance studies because they have additional virtual machine threads that collect garbage and dynamically compile, closely interacting with application threads. Further complexity is introduced as modern multicore machines have multiple sockets and dynamic frequency scaling options, broadening opportunities to reduce both power and running time.


title: Reducing the barriers to writing verified specifications

authors:
Todd W. Schiller
Michael D. Ernst

abstract: Formally verifying a program requires significant skill not only because of complex interactions between program subcomponents, but also because of deficiencies in current verification interfaces. These skill barriers make verification economically unattractive by preventing the use of less-skilled (less-expensive) workers and distributed workflows (i.e., crowdsourcing). This paper presents VeriWeb, a web-based IDE for verification that decomposes the task of writing verifiable specifications into manageable subproblems. To overcome the information loss caused by task decomposition, and to reduce the skill required to verify a program, VeriWeb incorporates several innovative user interface features: drag and drop condition construction, concrete counterexamples, and specification inlining.


title: Scaling symbolic execution using ranged analysis

authors:
Junaid Haroon Siddiqui
Sarfraz Khurshid

abstract: This paper introduces a novel approach to scale symbolic execution --- a program analysis technique for systematic exploration of bounded execution paths---for test input generation. While the foundations of symbolic execution were developed over three decades ago, recent years have seen a real resurgence of the technique, specifically for systematic bug finding. However, scaling symbolic execution remains a primary technical challenge due to the inherent complexity of the path-based exploration that lies at core of the technique.


title: Open and efficient type switch for C++

authors:
Yuriy Solodkyy
Gabriel Dos Reis
Bjarne Stroustrup

abstract: Selecting operations based on the run-time type of an object is key to many object-oriented and functional programming techniques. We present a technique for implementing open and efficient type switching on hierarchical extensible data types. The technique is general and copes well with C++ multiple inheritance. To simplify experimentation and gain realistic performance using production-quality compilers and tool chains, we implement a type switch construct as an ISO C++11 library, called Mach7. This library-only implementation provides concise notation and outperforms the visitor design pattern, commonly used for case analysis on types in object-oriented programming. For closed sets of types, its performance roughly equals equivalent code in functional languages, such as OCaml and Haskell. The type-switching code is easier to use and is more expressive than hand-coded visitors are. The library is non-intrusive and circumvents most of the extensibility restrictions typical of the visitor design pattern. It was motivated by applications involving large, typed, abstract syntax trees.


title: Safe compiler-driven transaction checkpointing and recovery

authors:
Jaswanth Sreeram
Santosh Pande

abstract: Several studies have shown that a large fraction of the work performed inside memory transactions in representative programs is wasted due to the transaction experiencing a conflict and aborting. Aborts inside long running transactions are especially influential to performance and the simplicity of the TM programming model (relative to using finegrained locking) in synchronizing large critical sections means that large transactions are common and this exacerbates the problem of wasted work. In this paper we present a practical transaction checkpoint and recovery scheme in which transactions that experience a conflict can restore their state (including the local context in which they were executing) to some dynamic program point before this access and begin execution from that point. This state saving and restoration is implemented by checkpoint operations that are generated by a compiler into the transaction's body and are also optimized to reduce the amount of state that is saved and restored. We also describe a runtime system that manages these checkpointed states and orchestrates the restoration of the right checkpointed state for a conflict on a particular transactional access. Moreover the synthesis of these save and restore operations, their optimization and invocation at runtime are completely transparent to the programmer. We have implemented the checkpoint generation and optimization scheme in the LLVM compiler and runtime support for the TL2 STM system. Our experiments indicate that for many parallel programs using such checkpoint recovery schemes can result in upto several orders of magnitude reduction in number of aborts and significant execution time speedups relative to plain transactional programs for the same number of threads.


title: Optimization coaching: optimizers learn to communicate with programmers

authors:
Vincent St-Amour
Sam Tobin-Hochstadt
Matthias Felleisen

abstract: Optimizing compilers map programs in high-level languages to high-performance target language code. To most programmers, such a compiler constitutes an impenetrable black box whose inner workings are beyond their understanding. Since programmers often must understand the workings of their compilers to achieve their desired performance goals, they typically resort to various forms of reverse engineering, such as examining compiled code or intermediate forms. Instead, optimizing compilers should engage programmers in a dialog. This paper introduces one such possible form of dialog: optimization coaching. An optimization coach watches while a program is compiled, analyzes the results, generates suggestions for enabling further compiler optimization in the source program, and presents a suitable synthesis of its results to the programmer. We present an evaluation based on case studies, which illustrate how an optimization coach can help programmers achieve optimizations resulting in substantial performance improvements.


title: Chaperones and impersonators: run-time support for reasonable interposition

authors:
T. Stephen Strickland
Sam Tobin-Hochstadt
Robert Bruce Findler
Matthew Flatt

abstract: Chaperones and impersonators provide run-time support for interposing on primitive operations such as function calls, array access and update, and structure field access and update. Unlike most interposition support, chaperones and impersonators are restricted so that they constrain the behavior of the interposing code to reasonable interposition, which in practice preserves the abstraction mechanisms and reasoning that programmers and compiler analyses rely on.


title: Type-based safe resource deallocation for shared-memory concurrency

authors:
Kohei Suenaga
Ryota Fukuda
Atsushi Igarashi

abstract: We propose a type system to guarantee safe resource deallocation for shared-memory concurrent programs by extending the previous type system based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are not left allocated when a program terminates. Our framework supports (1) fork/join parallelism, (2) synchronization with locks, and (3) dynamically allocated memory cells and locks. The type system is proved to be sound. We also provide a type inference algorithm for the type system and a prototype implementation of the algorithm.


title: Gradual typing for first-class classes

authors:
Asumu Takikawa
T. Stephen Strickland
Christos Dimoulas
Sam Tobin-Hochstadt
Matthias Felleisen

abstract: Dynamic type-checking and object-oriented programming often go hand-in-hand; scripting languages such as Python, Ruby, and JavaScript all embrace object-oriented (OO) programming. When scripts written in such languages grow and evolve into large programs, the lack of a static type discipline reduces maintainability. A programmer may thus wish to migrate parts of such scripts to a sister language with a static type system. Unfortunately, existing type systems neither support the flexible OO composition mechanisms found in scripting languages nor accommodate sound interoperation with untyped code. In this paper, we present the design of a gradual typing system that supports sound interaction between statically- and dynamically-typed units of class-based code. The type system uses row polymorphism for classes and thus supports mixin-based OO composition. To protect migration of mixins from typed to untyped components, the system employs a novel form of contracts that partially seal classes. The design comes with a theorem that guarantees the soundness of the type system even in the presence of untyped components.


title: Understanding the behavior of database operations under program control

authors:
Juan M. Tamayo
Alex Aiken
Nathan Grasso Bronson
Mooly Sagiv

abstract: Applications that combine general program logic with persistent databases (e.g., three-tier applications) often suffer large performance penalties from poor use of the database. We introduce a program analysis technique that combines information flow in the program with commutativity analysis of its database operations to produce a unified dependency graph for database statements, which provides programmers with a high-level view of how costly database operations are and how they are connected in the program. As an example application of our analysis we describe three optimizations that can be discovered by examining the structure of the dependency graph; each helps remove communication latency from the critical path of a multi-tier system. We implement our technique in a tool for Java applications using JDBC and experimentally validate it using the multi-tier component of the Dacapo benchmark.


title: Constrained kinds

authors:
Olivier Tardieu
Nathaniel Nystrom
Igor Peshansky
Vijay A. Saraswat

abstract: Modern object-oriented languages such as X10 require a rich framework for types capable of expressing both value-dependency and genericity, and supporting pluggable, domain-specific extensions. In earlier work, we presented a framework for constrained types in object-oriented languages, parametrized by an underlying constraint system. Types are viewed as formulas C{c} where C is the name of a class or an interface and c is a constraint on the immutable instance state (the properties) of C. Constraint systems are a very expressive framework for partial information. Many (value-)dependent type systems for object-oriented languages can be viewed as constrained types.


title: Higher-order symbolic execution via contracts

authors:
Sam Tobin-Hochstadt
David Van Horn

abstract: We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior.


title: Software data-triggered threads

authors:
Hung-Wei Tseng
Dean M. Tullsen

abstract: The data-triggered threads (DTT) programming and execution model can increase parallelism and eliminate redundant computation. However, the initial proposal requires significant architecture support, which impedes existing applications and architectures from taking advantage of this model. This work proposes a pure software solution that supports the DTT model without any hardware support. This research uses a prototype compiler and runtime libraries running on top of existing machines. Several enhancements to the initial software implementation are presented, which further improve the performance.


title: Exploiting inter-sequence correlations for program behavior prediction

authors:
Bo Wu
Zhijia Zhao
Xipeng Shen
Yunlian Jiang
Yaoqing Gao
Raúl Silvera

abstract: Prediction of program dynamic behaviors is fundamental to program optimizations, resource management, and architecture reconfigurations. Most existing predictors are based on locality of program behaviors, subject to some inherent limitations. In this paper, we revisit the design philosophy and systematically explore a second source of clues: statistical correlations between the behavior sequences of different program entities. Concentrated on loops, it examines the correlations' existence, strength, and values in enhancing the design of program behavior predictors. It creates the first taxonomy of program behavior sequence patterns. It develops a new form of predictors, named sequence predictors, to effectively translate the correlations into large-scope, proactive predictions of program behavior sequences. It demonstrates the usefulness of the prediction in dynamic version selection and loop importance estimation, showing 19% average speedup on a number of real-world utility applications. By taking scope and timing of behavior prediction as the first-order design objectives, the new approach overcomes limitations of existing program behavior predictors, opening up many new opportunities for runtime optimizations at various layers of computing.


title: Finding reusable data structures

abstract: A big source of run-time performance problems in large-scale, object-oriented applications is the frequent creation of data structures (by the same allocation site) whose lifetimes are disjoint, and whose shapes and data content are always the same. Constructing these data structures and computing the same data values many times is expensive; significant performance improvements can be achieved by reusing their instances, shapes, and/or data values rather than reconstructing them. This paper presents a run-time technique that can be used to help programmers find allocation sites that create such data structures to improve performance. At the heart of the technique are three reusability definitions and novel summarization approaches that compute summaries for data structures based on these definitions. The computed summaries are used subsequently to find data structures that have disjoint lifetimes, and/or that have the same shapes and content. We have implemented this technique in the Jikes RVM and performed extensive studies on large-scale, real-world programs. We describe our experience using six case studies, in which we have achieved large performance gains by fixing problems reported by our tool.


title: Maple: a coverage-driven testing tool for multithreaded programs

authors:
Jie Yu
Satish Narayanasamy
Cristiano Pereira
Gilles Pokam

abstract: Testing multithreaded programs is a hard problem, because it is challenging to expose those rare interleavings that can trigger a concurrency bug. We propose a new thread interleaving coverage-driven testing tool called Maple that seeks to expose untested thread interleavings as much as possible. It memoizes tested interleavings and actively seeks to expose untested interleavings for a given test input to increase interleaving coverage. We discuss several solutions to realize the above goal. First, we discuss a coverage metric based on a set of interleaving idioms. Second, we discuss an online technique to predict untested interleavings that can potentially be exposed for a given test input. Finally, the predicted untested interleavings are exposed by actively controlling the thread schedule while executing for the test input. We discuss our experiences in using the tool to expose several known and unknown bugs in real-world applications such as Apache and MySQL.


title: Refactoring android Java code for on-demand computation offloading

authors:
Ying Zhang
Gang Huang
Xuanzhe Liu
Wei Zhang
Hong Mei
Shunxiang Yang

abstract: Computation offloading is a promising way to improve the performance as well as reducing the battery power consumption of a smartphone application by executing some parts of the application on a remote server. Supporting such capability is not easy for smartphone application developers due to (1) correctness: some code, e.g., that for GPS, gravity, and other sensors, can run only on the smartphone so that developers have to identify which parts of the application cannot be offloaded; (2) effectiveness: the reduced execution time must be greater than the network delay caused by computation offloading so that developers need to calculate which parts are worth offloading; (3) adaptability: smartphone applications often face changes of user requirements and runtime environments so that developers need to implement the adaptation on offloading. More importantly, considering the large number of today's smartphone applications, solutions applicable for legacy applications will be much more valuable. In this paper, we present a tool, named DPartner, that automatically refactors Android applications to be the ones with computation offloading capability. For a given Android application, DPartner first analyzes its bytecode for discovering the parts worth offloading, then rewrites the bytecode to implement a special program structure supporting on-demand offloading, and finally generates two artifacts to be deployed onto an Android phone and the server, respectively. We evaluated DPartner on three real-world Android applications, demonstrating the reduction of execution time by 46%-97% and battery power consumption by 27%-83%.


title: The HipHop compiler for PHP

authors:
Haiping Zhao
Iain Proctor
Minghui Yang
Xin Qi
Mark Williams
Qi Gao
Guilherme Ottoni
Andrew Paroski
Scott MacVicar
Jason Evans
Stephen Tu

abstract: Scripting languages are widely used to quickly accomplish a variety of tasks because of the high productivity they enable. Among other reasons, this increased productivity results from a combination of extensive libraries, fast development cycle, dynamic typing, and polymorphism. The dynamic features of scripting languages are traditionally associated with interpreters, which is the approach used to implement most scripting languages. Although easy to implement, interpreters are generally slow, which makes scripting languages prohibitive for implementing large, CPU-intensive applications. This efficiency problem is particularly important for PHP given that it is the most commonly used language for server-side web development. This paper presents the design, implementation, and an evaluation of the HipHop compiler for PHP. HipHop goes against the standard practice and implements a very dynamic language through static compilation. After describing the most challenging PHP features to support through static compilation, this paper presents HipHop's design and techniques that support almost all PHP features. We then present a thorough evaluation of HipHop running both standard benchmarks and the Facebook web site. Overall, our experiments demonstrate that HipHop is about 5.5x faster than standard, interpreted PHP engines. As a result, HipHop has reduced the number of servers needed to run Facebook and other web sites by a factor between 4 and 6, thus drastically cutting operating costs.


title: Data-driven equivalence checking

authors:
Rahul Sharma
Eric Schkufza
Berkeley R. Churchill
Alex Aiken

abstract: We present a data driven algorithm for equivalence checking of two loops. The algorithm infers simulation relations using data from test runs. Once a candidate simulation relation has been obtained, off-the-shelf SMT solvers are used to check whether the simulation relation actually holds. The algorithm is sound: insufficient data will cause the proof to fail. We demonstrate a prototype implementation, called DDEC, of our algorithm, which is the first sound equivalence checker for loops written in x86 assembly.


title: Targeted and depth-first exploration for systematic testing of android apps

authors:
Tanzirul Azim
Iulian Neamtiu

abstract: Systematic exploration of Android apps is an enabler for a variety of app analysis and testing tasks. Performing the exploration while apps run on actual phones is essential for exploring the full range of app capabilities. However, exploring real-world apps on real phones is challenging due to non-determinism, non-standard control flow, scalability and overhead constraints. Relying on end-users to conduct the exploration might not be very effective: we performed a 7-use study on popular Android apps, and found that the combined 7-use coverage was 30.08% of the app screens and 6.46% of the app methods. Prior approaches for automated exploration of Android apps have run apps in an emulator or focused on small apps whose source code was available. To address these problems, we present A3E, an approach and tool that allows substantial Android apps to be explored systematically while running on actual phones, yet without requiring access to the app's source code. The key insight of our approach is to use a static, taint-style, dataflow analysis on the app bytecode in a novel way, to construct a high-level control flow graph that captures legal transitions among activities (app screens). We then use this graph to develop an exploration strategy named Targeted Exploration that permits fast, direct exploration of activities, including activities that would be difficult to reach during normal use. We also developed a strategy named Depth-first Exploration that mimics user actions for exploring activities and their constituents in a slower, but more systematic way. To measure the effectiveness of our techniques, we use two metrics: activity coverage (number of screens explored) and method coverage. Experiments with using our approach on 25 popular Android apps including BBC News, Gas Buddy, Amazon Mobile, YouTube, Shazam Encore, and CNN, show that our exploration techniques achieve 59.39--64.11% activity coverage and 29.53--36.46% method coverage.


title: Class hierarchy complementation: soundly completing a partial type graph

authors:
George Balatsouras
Yannis Smaragdakis

abstract: We present the problem of class hierarchy complementation: given a partially known hierarchy of classes together with subtyping constraints ("A has to be a transitive subtype of B") complete the hierarchy so that it satisfies all constraints. The problem has immediate practical application to the analysis of partial programs--e.g., it arises in the process of providing a sound handling of "phantom classes" in the Soot program analysis framework. We provide algorithms to solve the hierarchy complementation problem in the single inheritance and multiple inheritance settings. We also show that the problem in a language such as Java, with single inheritance but multiple subtyping and distinguished class vs. interface types, can be decomposed into separate single- and multiple-subtyping instances. We implement our algorithms in a tool, JPhantom, which complements partial Java bytecode programs so that the result is guaranteed to satisfy the Java verifier requirements. JPhantom is highly scalable and runs in mere seconds even for large input applications and complex constraints (with a maximum of 14s for a 19MB binary).


title: On-the-fly detection of instability problems in floating-point program execution

authors:
Tao Bao
Xiangyu Zhang

abstract: The machine representation of floating point values has limited precision such that errors may be introduced during execution. These errors may get propagated and magnified by the following operations, leading to instability problems, e.g., control flow path may be undesirably altered and faulty output may be emitted. In this paper, we develop an on-the-fly efficient monitoring technique that can predict if an execution is stable. The technique does not explicitly compute errors as doing so incurs high overhead. Instead, it detects possible places where an error becomes substantially inflated regarding the corresponding value, and then tags the value with one bit to denote that it has an inflated error. It then tracks inflation bit propagation, taking care of operations that may cut off such propagation. It reports instability if any inflation bit reaches a critical execution point, such as a predicate, where the inflated error may induce substantial execution difference, such as different execution paths. Our experiment shows that with appropriate thresholds, the technique can correctly detect that over 99.999996% of the inputs of all the programs we studied are stable while a traditional technique relying solely on inflation detection mistakenly classifies majority of the inputs as unstable for some of the programs. Compared to the state of the art technique that is based on high precision computation and causes several hundred times slowdown, our technique only causes 7.91 times slowdown on average and can report all the true unstable executions with the appropriate thresholds.


title: Input-covering schedules for multithreaded programs

authors:
Tom Bergan
Luis Ceze
Dan Grossman

abstract: We propose constraining multithreaded execution to small sets of input-covering schedules, which we define as follows: given a program P, we say that a set of schedules ∑ covers all inputs of program P if, when given any input, P's execution can be constrained to some schedule in ∑ and still produce a semantically valid result.


title: Combining concern input with program analysis for bloat detection

authors:
Suparna Bhattacharya
Kanchi Gopinath
Mangala Gowri Nanda

abstract: Framework based software tends to get bloated by accumulating optional features (or concerns) just-in-case they are needed. The good news is that such feature bloat need not always cause runtime execution bloat. The bad news is that often enough, only a few statements from an optional concern may cause execution bloat that may result in as much as 50% runtime overhead.


title: Bottle graphs: visualizing scalability bottlenecks in multi-threaded applications

authors:
Kristof Du Bois
Jennifer B. Sartor
Stijn Eyerman
Lieven Eeckhout

abstract: Understanding and analyzing multi-threaded program performance and scalability is far from trivial, which severely complicates parallel software development and optimization. In this paper, we present bottle graphs, a powerful analysis tool that visualizes multi-threaded program performance, in regards to both per-thread parallelism and execution time. Each thread is represented as a box, with its height equal to the share of that thread in the total program execution time, its width equal to its parallelism, and its area equal to its total running time. The boxes of all threads are stacked upon each other, leading to a stack with height equal to the total program execution time. Bottle graphs show exactly how scalable each thread is, and thus guide optimization towards those threads that have a smaller parallel component (narrower), and a larger share of the total execution time (taller), i.e. to the 'neck' of the bottle.


title: Storage strategies for collections in dynamically typed languages

authors:
Carl Friedrich Bolz
Lukas Diekmann
Laurence Tratt

abstract: Dynamically typed language implementations often use more memory and execute slower than their statically typed cousins, in part because operations on collections of elements are unoptimised. This paper describes storage strategies, which dynamically optimise collections whose elements are instances of the same primitive type. We implement storage strategies in the PyPy virtual machine, giving a performance increase of 18% on wide-ranging benchmarks of real Python programs. We show that storage strategies are simple to implement, needing only 1500LoC in PyPy, and have applicability to a wide range of virtual machines.


title: OCTET: capturing and controlling cross-thread dependences efficiently

authors:
Michael D. Bond
Milind Kulkarni
Man Cao
Minjia Zhang
Meisam Fathi Salmi
Swarnendu Biswas
Aritra Sengupta
Jipeng Huang

abstract: Parallel programming is essential for reaping the benefits of parallel hardware, but it is notoriously difficult to develop and debug reliable, scalable software systems. One key challenge is that modern languages and systems provide poor support for ensuring concurrency correctness properties - atomicity, sequential consistency, and multithreaded determinism - because all existing approaches are impractical. Dynamic, software-based approaches slow programs by up to an order of magnitude because capturing and controlling cross-thread dependences (i.e., conflicting accesses to shared memory) requires synchronization at virtually every access to potentially shared memory.


title: Verifying quantitative reliability for programs that execute on unreliable hardware

authors:
Michael Carbin
Sasa Misailovic
Martin C. Rinard

abstract: Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors.


title: Guided GUI testing of android apps with minimal restart and approximate learning

authors:
Wontae Choi
George C. Necula
Koushik Sen

abstract: Smartphones and tablets with rich graphical user interfaces (GUI) are becoming increasingly popular. Hundreds of thousands of specialized applications, called apps, are available for such mobile platforms. Manual testing is the most popular technique for testing graphical user interfaces of such apps. Manual testing is often tedious and error-prone. In this paper, we propose an automated technique, called Swift-Hand, for generating sequences of test inputs for Android apps. The technique uses machine learning to learn a model of the app during testing, uses the learned model to generate user inputs that visit unexplored states of the app, and uses the execution of the app on the generated inputs to refine the model. A key feature of the testing algorithm is that it avoids restarting the app, which is a significantly more expensive operation than executing the app on a sequence of inputs. An important insight behind our testing algorithm is that we do not need to learn a precise model of an app, which is often computationally intensive, if our goal is to simply guide test execution into unexplored parts of the state space. We have implemented our testing algorithm in a publicly available tool for Android apps written in Java. Our experimental results show that we can achieve significantly better coverage than traditional random testing and L*-based testing in a given time budget. Our algorithm also reaches peak coverage faster than both random and L*-based testing.


title: Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels

authors:
Nathan Chong
Alastair F. Donaldson
Paul H. J. Kelly
Jeroen Ketema
Shaz Qadeer

abstract: Data-dependent GPU kernels, whose data or control flow are dependent on the input of the program, are difficult to verify because they require reasoning about shared state manipulated by many parallel threads. Existing verification techniques for GPU kernels achieve soundness and scalability by using a two-thread reduction and making the contents of the shared state nondeterministic each time threads synchronise at a barrier, to account for all possible thread interactions. This coarse abstraction prohibits verification of data-dependent kernels. We present barrier invariants, a novel abstraction technique which allows key properties about the shared state of a kernel to be preserved across barriers during formal reasoning. We have integrated barrier invariants with the GPUVerify tool, and present a detailed case study showing how they can be used to verify three prefix sum algorithms, allowing efficient modular verification of a stream compaction kernel, a key building block for GPU programming. This analysis goes significantly beyond what is possible using existing verification techniques for GPU kernels.


title: Fully concurrent garbage collection of actors on many-core machines

authors:
Sylvan Clebsch
Sophia Drossopoulou

abstract: Disposal of dead actors in actor-model languages is as important as disposal of unreachable objects in object-oriented languages. In current practice, programmers are required to either manually terminate actors, or they have to rely on garbage collection systems that monitor actor mutation through write barriers, thread coordination through locks etc. These techniques, however, prevent the collector from being fully concurrent.


title: Bounded partial-order reduction

authors:
Katherine E. Coons
Madan Musuvathi
Kathryn S. McKinley

abstract: Eliminating concurrency errors is increasingly important as systems rely more on parallelism for performance. Exhaustively exploring the state-space of a program's thread interleavings finds concurrency errors and provides coverage guarantees, but suffers from exponential state-space explosion. Two prior approaches alleviate state-space explosion. (1) Dynamic partial-order reduction (DPOR) provides full coverage and explores only one interleaving of independent transitions. (2) Bounded search provides bounded coverage by enumerating interleavings that do not exceed a bound. In particular, we focus on preemption-bounding. Combining partial-order reduction with preemption-bounding had remained an open problem.


title: Ball-Larus path profiling across multiple loop iterations

authors:
Daniele Cono D'Elia
Camil Demetrescu

abstract: Identifying the hottest paths in the control flow graph of a routine can direct optimizations to portions of the code where most resources are consumed. This powerful methodology, called path profiling, was introduced by Ball and Larus in the mid 90's [4] and has received considerable attention in the last 15 years for its practical relevance. A shortcoming of the Ball-Larus technique was the inability to profile cyclic paths, making it difficult to mine execution patterns that span multiple loop iterations. Previous results, based on rather complex algorithms, have attempted to circumvent this limitation at the price of significant performance losses even for a small number of iterations. In this paper, we present a new approach to multi-iteration path profiling, based on data structures built on top of the original Ball-Larus numbering technique. Our approach allows the profiling of all executed paths obtained as a concatenation of up to k Ball-Larus acyclic paths, where k is a user-defined parameter. We provide examples showing that this method can reveal optimization opportunities that acyclic-path profiling would miss. An extensive experimental investigation on a large variety of Java benchmarks on the Jikes RVM shows that our approach can be even faster than Ball-Larus due to fewer operations on smaller hash tables, producing compact representations of cyclic paths even for large values of k.


title: Ironclad C++: a library-augmented type-safe subset of c++

authors:
Christian DeLozier
Richard A. Eisenberg
Santosh Nagarakatte
Peter-Michael Osera
Milo M. K. Martin
Steve Zdancewic

abstract: The C++ programming language remains widely used, despite inheriting many unsafe features from C---features that often lead to failures of type or memory safety that manifest as buffer overflows, use-after-free vulnerabilities, or abstraction violations. Malicious attackers can exploit such violations to compromise application and system security.


title: Efficient concurrency-bug detection across inputs

authors:
Dongdong Deng
Wei Zhang
Shan Lu

abstract: In the multi-core era, it is critical to efficiently test multi-threaded software and expose concurrency bugs before software release. Previous work has made significant progress in detecting and validating concurrency bugs under a given input. Unfortunately, software testing always faces large sets of test inputs, and existing techniques are still too expensive to be applied to every test input in practice.


title: Inductive invariant generation via abductive inference

authors:
Isil Dillig
Thomas Dillig
Boyang Li
Kenneth L. McMillan

abstract: This paper presents a new method for generating inductive loop invariants that are expressible as boolean combinations of linear integer constraints. The key idea underlying our technique is to perform a backtracking search that combines Hoare-style verification condition generation with a logical abduction procedure based on quantifier elimination to speculate candidate invariants. Starting with true, our method iteratively strengthens loop invariants until they are inductive and strong enough to verify the program. A key feature of our technique is that it is lazy: It only infers those invariants that are necessary for verifying program correctness. Furthermore, our technique can infer arbitrary boolean combinations (including disjunctions) of linear invariants. We have implemented the proposed approach in a tool called HOLA. Our experiments demonstrate that HOLA can infer interesting invariants that are beyond the reach of existing state-of-the-art invariant generation tools.


title: Option contracts

authors:
Christos Dimoulas
Robert Bruce Findler
Matthias Felleisen

abstract: Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious run-time cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails.


title: Semi-automatic rename refactoring for JavaScript

authors:
Asger Feldthaus
Anders Møller

abstract: Modern IDEs support automated refactoring for many programming languages, but support for JavaScript is still primitive. To perform renaming, which is one of the fundamental refactorings, there is often no practical alternative to simple syntactic search-and-replace. Although more sophisticated alternatives have been developed, they are limited by whole-program assumptions and poor scalability.


title: Forsaking inheritance: supercharged delegation in DelphJ

authors:
Prodromos Gerakios
Aggelos Biboudis
Yannis Smaragdakis

abstract: We propose DelphJ: a Java-based OO language that eschews inheritance completely, in favor of a combination of class morphing and (deep) delegation. Compared to past delegation approaches, the novel aspect of our design is the ability to emulate the best aspects of inheritance while retaining maximum flexibility: using morphing, a class can select any of the methods of its delegatee and export them (if desired) or transform them (e.g., to add extra arguments or modify type signatures), yet without needing to name these methods explicitly and handle them one-by-one. Compared to past work on morphing, our approach adopts and adapts advanced delegation mechanisms, in order to add late binding capabilities and, thus, provide a full substitute of inheritance. Additionally, we explore complex semantic issues in the interaction of delegation with late binding. We present our language design both informally, with numerous examples, and formally in a core calculus.


title: River trail: a path to parallelism in JavaScript

authors:
Stephan Herhut
Richard L. Hudson
Tatiana Shpeisman
Jaswanth Sreeram

abstract: JavaScript is the most popular language on the web and is a crucial component of HTML5 applications and services that run on consumer platforms ranging from desktops to phones. However, despite ample amount of hardware parallelism available to web applications on such platforms, JavaScript web applications remain predominantly sequential. Common parallel programming solutions accepted by other programming languages failed to transfer themselves to JavaScript due to differences in programming models, the additional requirements of the web and different developer expectations.


title: Do developers benefit from generic types?: an empirical comparison of generic and raw types in java

authors:
Michael Hoppe
Stefan Hanenberg

abstract: Type systems that permit developers to express themselves more precisely are one of the primary topics in programming language research, as well as in industrial software development. While it seems plausible that an expressive static type system increases developer productivity, there is little empirical evidence for or against this hypothesis. Generic types in Java are an example: as an extension of Java's original type system, some claim that Java 1.5 improves the type system's "expressiveness." Even if this claim is true, there exists little empirical evidence that claimed expressiveness leads to a measurable increase in developer productivity. This paper introduces an experiment where generic types (in comparison to raw types) have been evaluated in three different directions: (1) the documentation impact on undocumented APIs, (2) the time required for fixing type errors, and (3) the extensibility of a generic type hierarchy. The results of the experiment suggest that generic types improve documentation and reduce extensibility -- without revealing a difference in the time required for fixing type errors.


title: Efficient context sensitivity for dynamic analyses via calling context uptrees and customized memory management

authors:
Jipeng Huang
Michael D. Bond

abstract: State-of-the-art dynamic bug detectors such as data race and memory leak detectors report program locations that are likely causes of bugs. However, programmers need more than static program locations to understand the behavior of increasingly complex and concurrent software. Dynamic calling context provides additional information, but it is expensive to record calling context frequently, e.g., at every read and write. Context-sensitive dynamic analyses can build and maintain a calling context tree (CCT) to track calling context--but in order to reuse existing nodes, CCT-based approaches require an expensive lookup.


title: The latency, accuracy, and battery (LAB) abstraction: programmer productivity and energy efficiency for continuous mobile context sensing

authors:
Aman Kansal
T. Scott Saponas
A. J. Bernheim Brush
Kathryn S. McKinley
Todd Mytkowicz
Ryder Ziola

abstract: Emerging mobile applications that sense context are poised to delight and entertain us with timely news and events, health tracking, and social connections. Unfortunately, sensing algorithms quickly drain the phone's battery. Developers can overcome battery drain by carefully optimizing context sensing but that makes programming with context arduous and ties applications to current sensing hardware. These types of applications embody a twist on the classic tension between programmer productivity and performance due to their combination of requirements.


title: Synthesis modulo recursive functions

authors:
Etienne Kneuss
Ivan Kuraj
Viktor Kuncak
Philippe Suter

abstract: We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures.


title: Steering symbolic execution to less traveled paths

authors:
You Li
Zhendong Su
Linzhang Wang
Xuandong Li

abstract: Symbolic execution is a promising testing and analysis methodology. It systematically explores a program's execution space and can generate test cases with high coverage. One significant practical challenge for symbolic execution is how to effectively explore the enormous number of program paths in real-world programs. Various heuristics have been proposed for guiding symbolic execution, but they are generally inefficient and ad-hoc. In this paper, we introduce a novel, unified strategy to guide symbolic execution to less explored parts of a program. Our key idea is to exploit a specific type of path spectra, namely the length-n subpath program spectra, to systematically approximate full path information for guiding path exploration. In particular, we use frequency distributions of explored length-n subpaths to prioritize "less traveled" parts of the program to improve test coverage and error detection. We have implemented our general strategy in KLEE, a state-of-the-art symbolic execution engine. Evaluation results on the GNU Coreutils programs show that (1) varying the length n captures program-specific information and exhibits different degrees of effectiveness, and (2) our general approach outperforms traditional strategies in both coverage and error detection.


title: Empirical analysis of programming language adoption

authors:
Leo A. Meyerovich
Ariel S. Rabkin

abstract: Some programming languages become widely popular while others fail to grow beyond their niche or disappear altogether. This paper uses survey methodology to identify the factors that lead to language adoption. We analyze large datasets, including over 200,000 SourceForge projects, 590,000 projects tracked by Ohloh, and multiple surveys of 1,000-13,000 programmers.

awards: Most Influential OOPSLA Paper (awarded 2023)


title: Instant pickles: generating object-oriented pickler combinators for fast and extensible serialization

authors:
Heather Miller
Philipp Haller
Eugene Burmako
Martin Odersky

abstract: As more applications migrate to the cloud, and as "big data" edges into even more production environments, the performance and simplicity of exchanging data between compute nodes/devices is increasing in importance. An issue central to distributed programming, yet often under-considered, is serialization or pickling, i.e., persisting runtime objects by converting them into a binary or text representation. Pickler combinators are a popular approach from functional programming; their composability alleviates some of the tedium of writing pickling code by hand, but they don't translate well to object-oriented programming due to qualities like open class hierarchies and subtyping polymorphism. Furthermore, both functional pickler combinators and popular, Java-based serialization frameworks tend to be tied to a specific pickle format, leaving programmers with no choice of how their data is persisted. In this paper, we present object-oriented pickler combinators and a framework for generating them at compile-time, called scala/pickling, designed to be the default serialization mechanism of the Scala programming language. The static generation of OO picklers enables significant performance improvements, outperforming Java and Kryo in most of our benchmarks. In addition to high performance and the need for little to no boilerplate, our framework is extensible: using the type class pattern, users can provide both (1) custom, easily interchangeable pickle formats and (2) custom picklers, to override the default behavior of the pickling framework. In benchmarks, we compare scala/pickling with other popular industrial frameworks, and present results on time, memory usage, and size when pickling/unpickling a number of data types used in real-world, large-scale distributed applications and frameworks.


title: On-the-fly capacity planning

authors:
Nick Mitchell
Peter F. Sweeney

abstract: When resolving performance problems, a simple histogram of hot call stacks does not cut it, especially given the highly fluid nature of modern deployments. Why bother tuning, when adding a few CPUs via the management console will quickly resolve the problem? The findings of these tools are also presented without any sense of context: e.g. string conversion may be expensive, but only matters if it contributes greatly to the response time of user logins.


title: Online feedback-directed optimizations for parallel Java code

authors:
Albert Noll
Thomas R. Gross

abstract: The performance of parallel code significantly depends on the parallel task granularity (PTG). If the PTG is too coarse, performance suffers due to load imbalance; if the PTG is too fine, performance suffers from the overhead that is induced by parallel task creation and scheduling.


title: CDSchecker: checking concurrent data structures written with C/C++ atomics

authors:
Brian Norris
Brian Demsky

abstract: Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak memory model, enabling developers to write portable and efficient multithreaded code.


title: Python: the full monty

authors:
Joe Gibbs Politz
Alejandro Martinez
Mae Milano
Sumner Warren
Daniel Patterson
Junsong Li
Anand Chitipothu
Shriram Krishnamurthi

abstract: We present a small-step operational semantics for the Python programming language. We present both a core language for Python, suitable for tools and proofs, and a translation process for converting Python source to this core. We have tested the composition of translation and evaluation of the core for conformance with the primary Python implementation, thereby giving confidence in the fidelity of the semantics. We briefly report on the engineering of these components. Finally, we examine subtle aspects of the language, identifying scope as a pervasive concern that even impacts features that might be considered orthogonal.


title: Multiverse: efficiently supporting distributed high-level speculation

authors:
Kaushik Ravichandran
Santosh Pande

abstract: Algorithmic speculation or high-level speculation is a promising programming paradigm which allows programmers to speculatively branch an execution into multiple independent parallel sections and then choose the best (perhaps fastest) amongst them. The continuing execution after the speculatively branched section sees only the modifications made by the best one. This programming paradigm allows programmers to harness parallelism and can provide dramatic performance improvements.


title: Refactoring with synthesis

authors:
Veselin Raychev
Max Schäfer
Manu Sridharan
Martin T. Vechev

abstract: Refactoring has become an integral part of modern software development, with wide support in popular integrated development environments (IDEs). Modern IDEs provide a fixed set of supported refactorings, listed in a refactoring menu. But with IDEs supporting more and more refactorings, it is becoming increasingly difficult for programmers to discover and memorize all their names and meanings. Also, since the set of refactorings is hard-coded, if a programmer wants to achieve a slightly different code transformation, she has to either apply a (possibly non-obvious) sequence of several built-in refactorings, or just perform the transformation by hand.


title: Effective race detection for event-driven programs

authors:
Veselin Raychev
Martin T. Vechev
Manu Sridharan

abstract: Like shared-memory multi-threaded programs, event-driven programs such as client-side web applications are susceptible to data races that are hard to reproduce and debug. Race detection for such programs is hampered by their pervasive use of ad hoc synchronization, which can lead to a prohibitive number of false positives. Race detection also faces a scalability challenge, as a large number of short-running event handlers can quickly overwhelm standard vector-clock-based techniques.


title: Flexible access control for javascript

authors:
Gregor Richards
Christian Hammer
Francesco Zappa Nardelli
Suresh Jagannathan
Jan Vitek

abstract: Providing security guarantees for systems built out of untrusted components requires the ability to define and enforce access control policies over untrusted code. In Web 2.0 applications, JavaScript code from different origins is often combined on a single page, leading to well-known vulnerabilities. We present a security infrastructure which allows users and content providers to specify access control policies over subsets of a JavaScript program by leveraging the concept of delimited histories with revocation. We implement our proposal in WebKit and evaluate it with three policies on 50 widely used websites with no changes to their JavaScript code and report performance overheads and violations.


title: Interacting with dead objects

authors:
Robin Salkeld
Gregor Kiczales

abstract: Debugging and analyzing a snapshot of a crashed program's memory is far more difficult than working with a live program, because debuggers can no longer execute code to help make sense of the program state. We present an architecture that supports the restricted execution of ordinary code starting from the snapshot, as if the dead objects within it had been restored, but without access to their original external environment. We demonstrate the feasibility of this approach via an implementation for Java that does not require a custom virtual machine, show that it performs competitively with live execution, and use it to diagnose an unresolved memory leak in a mature mainstream application.


title: Taking off the gloves with reference counting Immix

authors:
Rifat Shahriyar
Stephen M. Blackburn
Xi Yang
Kathryn S. McKinley

abstract: Despite some clear advantages and recent advances, reference counting remains a poor cousin to high-performance tracing garbage collectors. The advantages of reference counting include a) immediacy of reclamation, b) incrementality, and c) local scope of its operations. After decades of languishing with hopelessly bad performance, recent work narrowed the gap between reference counting and the fastest tracing collectors to within 10%. Though a major advance, this gap remains a substantial barrier to adoption in performance-conscious application domains.


title: Code optimizations using formally verified properties

authors:
Yao Shi
Bernard Blackham
Gernot Heiser

abstract: Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification.


title: Set-based pre-processing for points-to analysis

authors:
Yannis Smaragdakis
George Balatsouras
George Kastrinis

abstract: We present set-based pre-analysis: a virtually universal optimization technique for flow-insensitive points-to analysis. Points-to analysis computes a static abstraction of how object values flow through a program's variables. Set-based pre-analysis relies on the observation that much of this reasoning can take place at the set level rather than the value level. Computing constraints at the set level results in significant optimization opportunities: we can rewrite the input program into a simplified form with the same essential points-to properties. This rewrite results in removing both local variables and instructions, thus simplifying the subsequent value-based points-to computation. Effectively, set-based pre-analysis puts the program in a normal form optimized for points-to analysis.


title: MrCrypt: static analysis for secure cloud computations

authors:
Sai Deep Tetali
Mohsen Lesani
Rupak Majumdar
Todd D. Millstein

abstract: In a common use case for cloud computing, clients upload data and computation to servers that are managed by a third-party infrastructure provider. We describe MrCrypt, a system that provides data confidentiality in this setting by executing client computations on encrypted data. MrCrypt statically analyzes a program to identify the set of operations on each input data column, in order to select an appropriate homomorphic encryption scheme for that column, and then transforms the program to operate over encrypted data. The encrypted data and transformed program are uploaded to the server and executed as usual, and the result of the computation is decrypted on the client side. We have implemented MrCrypt for Java and illustrate its practicality on three standard benchmark suites for the Hadoop MapReduce framework. We have also formalized the approach and proven several soundness and security guarantees.


title: Language support for dynamic, hierarchical data partitioning

authors:
Sean Treichler
Michael Bauer
Alex Aiken

abstract: Applications written for distributed-memory parallel architectures must partition their data to enable parallel execution. As memory hierarchies become deeper, it is increasingly necessary that the data partitioning also be hierarchical to match. Current language proposals perform this hierarchical partitioning statically, which excludes many important applications where the appropriate partitioning is itself data dependent and so must be computed dynamically. We describe Legion, a region-based programming system, where each region may be partitioned into subregions. Partitions are computed dynamically and are fully programmable. The division of data need not be disjoint and subregions of a region may overlap, or alias one another. Computations use regions with certain privileges (e.g., expressing that a computation uses a region read-only) and data coherence (e.g., expressing that the computation need only be atomic with respect to other operations on the region), which can be controlled on a per-region (or subregion) basis.


title: Turning nondeterminism into parallelism

authors:
Omer Tripp
Eric Koskinen
Mooly Sagiv

abstract: Nondeterminism is a useful and prevalent concept in the design and implementation of software systems. An important property of nondeterminism is its latent parallelism: A nondeterministic action can evaluate to multiple behaviors. If at least one of these behaviors does not conflict with concurrent tasks, then there is an admissible execution of the action in parallel with these tasks. Unfortunately, existing implementations of the atomic paradigm - optimistic as well as pessimistic - are unable to fully exhaust the parallelism potential of nondeterministic actions, lacking the means to guide concurrent tasks toward nondeterministic choices that minimize interference.


title: Miniboxing: improving the speed to code size tradeoff in parametric polymorphism translations

authors:
Vlad Ureche
Cristian Talau
Martin Odersky

abstract: Parametric polymorphism enables code reuse and type safety. Underneath the uniform interface exposed to programmers, however, its low level implementation has to cope with inherently non-uniform data: value types of different sizes and semantics (bytes, integers, floating point numbers) and reference types (pointers to heap objects). On the Java Virtual Machine, parametric polymorphism is currently translated to bytecode using two competing approaches: homogeneous and heterogeneous. Homogeneous translation requires boxing, and thus introduces indirect access delays. Heterogeneous translation duplicates and adapts code for each value type individually, producing more bytecode. Therefore bytecode speed and size are at odds with each other. This paper proposes a novel translation that significantly reduces the bytecode size without affecting the execution speed. The key insight is that larger value types (such as integers) can hold smaller ones (such as bytes) thus reducing the duplication necessary in heterogeneous translations. In our implementation, on the Scala compiler, we encode all primitive value types in long integers. The resulting bytecode approaches the performance of monomorphic code, matches the performance of the heterogeneous translation and obtains speedups of up to 22x over the homogeneous translation, all with modest increases in size.


title: Relaxed separation logic: a program logic for C11 concurrency

authors:
Viktor Vafeiadis
Chinmay Narayan

abstract: We introduce relaxed separation logic (RSL), the first program logic for reasoning about concurrent programs running under the C11 relaxed memory model. From a user's perspective, RSL is an extension of concurrent separation logic (CSL) with proof rules for the various kinds of C11 atomic accesses. As in CSL, individual threads are allowed to access non-atomically only the memory that they own, thus preventing data races. Ownership can, however, be transferred via certain atomic accesses. For SC-atomic accesses, we permit arbitrary ownership transfer; for acquire/release atomic accesses, we allow ownership transfer only in one direction; whereas for relaxed atomic accesses, we rule out ownership transfer completely. We illustrate RSL with a few simple examples and prove its soundness directly over the axiomatic C11 weak memory model.


title: Resurrector: a tunable object lifetime profiling technique for optimizing real-world programs

abstract: Modern object-oriented applications commonly suffer from severe performance problems that need to be optimized away for increased efficiency and user satisfaction. Many existing optimization techniques (such as object pooling and pretenuring) require precise identification of object lifetimes. However, it is particularly challenging to obtain object lifetimes both precisely and efficiently: precise profiling techniques such as Merlin introduce several hundred times slowdown even for small programs while efficient approximation techniques often sacrifice precision and produce less useful lifetime information. This paper presents a tunable profiling technique, called Resurrector, that explores the middle ground between high precision and high efficiency to find the precision-efficiency sweetspot for various livenessbased optimization techniques. Our evaluation shows that Resurrector is both more precise and more efficient than the GC-based approximation, and it is orders-of-magnitude faster than Merlin. To demonstrate Resurrector's usefulness, we have developed client analyses to find allocation sites that create large data structures with disjoint lifetimes. By inspecting program source code and reusing data structures created from these allocation sites, we have achieved significant performance gains. We have also improved the precision of an existing optimization technique using the lifetime information collected by Resurrector.


title: Injecting mechanical faults to localize developer faults for evolving software

authors:
Lingming Zhang
Lu Zhang
Sarfraz Khurshid

abstract: This paper presents a novel methodology for localizing faults in code as it evolves. Our insight is that the essence of failure-inducing edits made by the developer can be captured using mechanical program transformations (e.g., mutation changes). Based on the insight, we present the FIFL framework, which uses both the spectrum information of edits (obtained using the existing FaultTracer approach) as well as the potential impacts of edits (simulated by mutation changes) to achieve more accurate fault localization. We evaluate FIFL on real-world repositories of nine Java projects ranging from 5.7KLoC to 88.8KLoC. The experimental results show that FIFL is able to outperform the state-of-the-art FaultTracer technique for localizing failure-inducing program edits significantly. For example, all 19 FIFL strategies that use both the spectrum information and simulated impact information for each edit outperform the existing FaultTracer approach statistically at the significance level of 0.01. In addition, FIFL with its default settings outperforms FaultTracer by 2.33% to 86.26% on 16 of the 26 studied version pairs, and is only inferior than FaultTracer on one version pair.


title: Isolation for nested task parallelism

authors:
Jisheng Zhao
Roberto Lublinerman
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. Whilethere is a large body of past work on isolated task-parallelism, the integration of isolation, task-parallelism, and nesting of tasks has been a difficult and unresolved challenge. In this pa- per, we present a programming and execution model called Otello where isolation is extended to arbitrarily nested parallel tasks with irregular accesses to heap data. At the same time, no additional burden is imposed on the programmer, who only exposes parallelism by creating and synchronizing parallel tasks, leaving the job of ensuring isolation to the underlying compiler and runtime system.


title: Detecting API documentation errors

authors:
Hao Zhong
Zhendong Su

abstract: When programmers encounter an unfamiliar API library, they often need to refer to its documentations, tutorials, or discussions on development forums to learn its proper usage. These API documents contain valuable information, but may also mislead programmers as they may contain errors (e.g., broken code names and obsolete code samples). Although most API documents are actively maintained and updated, studies show that many new and latent errors do exist. It is tedious and error-prone to find such errors manually as API documents can be enormous with thousands of pages. Existing tools are ineffective in locating documentation errors because traditional natural language (NL) tools do not understand code names and code samples, and traditional code analysis tools do not understand NL sentences. In this paper, we propose the first approach, DOCREF, specifically designed and developed to detect API documentation errors. We formulate a class of inconsistencies to indicate potential documentation errors, and combine NL and code analysis techniques to detect and report such inconsistencies. We have implemented DOCREF and evaluated its effectiveness on the latest documentations of five widely-used API libraries. DOCREF has detected more than 1,000 new documentation errors, which we have reported to the authors. Many of the errors have already been confirmed and fixed, after we reported them.


title: The hiphop virtual machine

authors:
Keith Adams
Jason Evans
Bertrand Maher
Guilherme Ottoni
Andrew Paroski
Brett Simmers
Edwin Smith
Owen Yamauchi

abstract: The HipHop Virtual Machine (HHVM) is a JIT compiler and runtime for PHP. While PHP values are dynamically typed, real programs often have latent types that are useful for optimization once discovered. Some types can be proven through static analysis, but limitations in the ahead-of-time approach leave some types to be discovered at run time. And even though many values have latent types, PHP programs can also contain polymorphic variables and expressions, which must be handled without catastrophic slowdown.


title: Confined gradual typing

authors:
Esteban Allende
Johan Fabry
Ronald Garcia
Éric Tanter

abstract: Gradual typing combines static and dynamic typing flexibly and safely in a single programming language. To do so, gradually typed languages implicitly insert casts where needed, to ensure at runtime that typing assumptions are not violated by untyped code. However, the implicit nature of cast insertion, especially on higher-order values, can jeopardize reliability and efficiency: higher-order casts can fail at any time, and are costly to execute. We propose Confined Gradual Typing, which extends gradual typing with two new type qualifiers that let programmers control the flow of values between the typed and the untyped worlds, and thereby trade some flexibility for more reliability and performance. We formally develop two variants of Confined Gradual Typing that capture different flexibility/guarantee tradeoffs. We report on the implementation of Confined Gradual Typing in Gradualtalk, a gradually-typed Smalltalk, which confirms the performance advantage of avoiding unwanted higher-order casts and the low overhead of the approach.


title: Refactoring Java generics by inferring wildcards, in practice

authors:
John Altidor
Yannis Smaragdakis

abstract: Wildcard annotations can improve the generality of Java generic libraries, but require heavy manual effort. We present an algorithm for refactoring and inferring more general type instantiations of Java generics using wildcards. Compared to past approaches, our work is practical and immediately applicable: we assume no changes to the Java type system, while taking into account all its intricacies. Our system allows users to select declarations (variables, method parameters, return types, etc.) to generalize and considers declarations not declared in available source code. It then performs an inter-procedural flow analysis and a method body analysis, in order to generalize type signatures. We evaluate our technique on six Java generic libraries. We find that 34% of available declarations of variant type signatures can be generalized - i.e., relaxed with more general wildcard types. On average, 146 other declarations need to be updated when a declaration is generalized, showing that this refactoring would be too tedious and error-prone to perform manually.


title: Foundations of path-dependent types

authors:
Nada Amin
Tiark Rompf
Martin Odersky

abstract: A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. An essential ingredient of this unification is the concept of objects with type members, which can be referenced through path-dependent types. Unfortunately, path-dependent types are not well-understood, and have been a roadblock in grounding the Scala type system on firm theory.


title: Determinacy in static analysis for jQuery

authors:
Esben Andreasen
Anders Møller

abstract: Static analysis for JavaScript can potentially help programmers find errors early during development. Although much progress has been made on analysis techniques, a major obstacle is the prevalence of libraries, in particular jQuery, which apply programming patterns that have detrimental consequences on the analysis precision and performance. Previous work on dynamic determinacy analysis has demonstrated how information about program expressions that always resolve to a fixed value in some call context may lead to significant scalability improvements of static analysis for such code. We present a static dataflow analysis for JavaScript that infers and exploits determinacy information on-the-fly, to enable analysis of some of the most complex parts of jQuery. The analysis combines selective context and path sensitivity, constant propagation, and branch pruning, based on a systematic investigation of the main causes of analysis imprecision when using a more basic analysis.


title: CheckCell: data debugging for spreadsheets

authors:
Daniel W. Barowy
Dimitar Gochev
Emery D. Berger

abstract: Testing and static analysis can help root out bugs in programs, but not in data. This paper introduces data debugging, an approach that combines program analysis and statistical analysis to automatically find potential data errors. Since it is impossible to know a priori whether data are erroneous, data debugging instead locates data that has a disproportionate impact on the computation. Such data is either very important, or wrong. Data debugging is especially useful in the context of data-intensive programming environments that intertwine data with programs in the form of queries or formulas.


title: Tardis: affordable time-travel debugging in managed runtimes

authors:
Earl T. Barr
Mark Marron

abstract: Developers who set a breakpoint a few statements too late or who are trying to diagnose a subtle bug from a single core dump often wish for a time-traveling debugger. The ability to rewind time to see the exact sequence of statements and program values leading to an error has great intuitive appeal but, due to large time and space overheads, time traveling debuggers have seen limited adoption. A managed runtime, such as the Java JVM or a JavaScript engine, has already paid much of the cost of providing core features - type safety, memory management, and virtual IO - that can be reused to implement a low overhead time-traveling debugger. We leverage this insight to design and build affordable time-traveling debuggers for managed languages. Tardis realizes our design: it provides affordable time-travel with an average overhead of only 7% during normal execution, a rate of 0.6MB/s of history logging, and a worst-case 0.68s time-travel latency on our benchmark applications. Tardis can also debug optimized code using time-travel to reconstruct state. This capability, coupled with its low overhead, makes Tardis suitable for use as the default debugger for managed languages, promising to bring time-traveling debugging into the mainstream and transform the practice of debugging.


title: Rate types for stream programs

authors:
Thomas Bartenstein
Yu David Liu

abstract: We introduce RATE TYPES, a novel type system to reason about and optimize data-intensive programs. Built around stream languages, RATE TYPES performs static quantitative reasoning about stream rates -- the frequency of data items in a stream being consumed, processed, and produced. Despite the fact that streams are fundamentally dynamic, we find two essential concepts of stream rate control -- throughput ratio and natural rate -- are intimately related to the program structure itself and can be effectively reasoned about by a type system. RATE TYPES is proven to correspond with a time-aware and parallelism-aware operational semantics. The strong correspondence result tolerates arbitrary schedules, and does not require any synchronization between stream filters.We further implement RATE TYPES, demonstrating its effectiveness in predicting stream data rates in real-world stream programs.


title: Phosphor: illuminating dynamic data flow in commodity jvms

authors:
Jonathan Bell
Gail E. Kaiser

abstract: Dynamic taint analysis is a well-known information flow analysis problem with many possible applications. Taint tracking allows for analysis of application data flow by assigning labels to data, and then propagating those labels through data flow. Taint tracking systems traditionally compromise among performance, precision, soundness, and portability. Performance can be critical, as these systems are often intended to be deployed to production environments, and hence must have low overhead. To be deployed in security-conscious settings, taint tracking must also be sound and precise. Dynamic taint tracking must be portable in order to be easily deployed and adopted for real world purposes, without requiring recompilation of the operating system or language interpreter, and without requiring access to application source code.


title: Symbolic execution of multithreaded programs from arbitrary program contexts

authors:
Tom Bergan
Dan Grossman
Luis Ceze

abstract: We describe an algorithm to perform symbolic execution of a multithreaded program starting from an arbitrary program context. We argue that this can enable more efficient symbolic exploration of deep code paths in multithreaded programs by allowing the symbolic engine to jump directly to program contexts of interest.


title: StreamJIT: a commensal compiler for high-performance stream programming

authors:
Jeffrey Bosboom
Sumanaruban Rajadurai
Weng-Fai Wong
Saman P. Amarasinghe

abstract: There are many domain libraries, but despite the performance benefits of compilation, domain-specific languages are comparatively rare due to the high cost of implementing an optimizing compiler. We propose commensal compilation, a new strategy for compiling embedded domain-specific languages by reusing the massive investment in modern language virtual machine platforms. Commensal compilers use the host language's front-end, use host platform APIs that enable back-end optimizations by the host platform JIT, and use an autotuner for optimization selection. The cost of implementing a commensal compiler is only the cost of implementing the domain-specific optimizations. We demonstrate the concept by implementing a commensal compiler for the stream programming language StreamJIT atop the Java platform. Our compiler achieves performance 2.8 times better than the StreamIt native code (via GCC) compiler with considerably less implementation effort.


title: Static analysis for independent app developers

authors:
Lucas Brutschy
Pietro Ferrara
Peter Müller

abstract: Mobile app markets have lowered the barrier to market entry for software producers. As a consequence, an increasing number of independent app developers offer their products, and recent platforms such as the MIT App Inventor and Microsoft's TouchDevelop enable even lay programmers to develop apps and distribute them in app markets.


title: Atlas: leveraging locks for non-volatile memory consistency

authors:
Dhruva R. Chakrabarti
Hans-Juergen Boehm
Kumud Bhandari

abstract: Non-volatile main memory, such as memristors or phase change memory, can revolutionize the way programs persist data. In-memory objects can themselves be persistent without the need for a separate persistent data storage format. However, the challenge is to ensure that such data remains consistent if a failure occurs during execution.


title: Continuously measuring critical section pressure with the free-lunch profiler

authors:
Florian David
Gaël Thomas
Julia Lawall
Gilles Muller

abstract: Today, Java is regularly used to implement large multi-threaded server-class applications that use locks to protect access to shared data. However, understanding the impact of locks on the performance of a system is complex, and thus the use of locks can impede the progress of threads on configurations that were not anticipated by the developer, during specific phases of the execution.


title: Natural proofs for asynchronous programs using almost-synchronous reductions

authors:
Ankush Desai
Pranav Garg
P. Madhusudan

abstract: We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants - invariants consisting of global states where message buffers are close to empty. The reduction finds almost-synchronous invariants and simultaneously argues that they cover all local states. We show that asynchronous programs often have almost-synchronous invariants and that we can exploit this to build natural proofs that they are correct. We implement our reduction strategy, which is sound and complete, and show that it is more effective in proving programs correct as well as more efficient in finding bugs in several programs, compared to current search strategies which almost always diverge. The high point of our experiments is that our technique can prove the Windows Phone USB Driver written in P [9]correct for the responsiveness property, which was hitherto not provable using state-of-the-art model-checkers.


title: Distributed REScala: an update algorithm for distributed reactive programming

authors:
Joscha Drechsler
Guido Salvaneschi
Ragnar Mogk
Mira Mezini

abstract: Reactive programming improves the design of reactive applications by relocating the logic for managing dependencies between dependent values away from the application logic to the language implementation. Many distributed applications are reactive. Yet, existing change propagation algorithms are not suitable in a distributed setting.


title: Checking correctness of TypeScript interfaces for JavaScript libraries

authors:
Asger Feldthaus
Anders Møller

abstract: The TypeScript programming language adds optional types to JavaScript, with support for interaction with existing JavaScript libraries via interface declarations. Such declarations have been written for hundreds of libraries, but they can be difficult to write and often contain errors, which may affect the type checking and misguide code completion for the application code in IDEs.


title: Automated migration of build scripts using dynamic analysis and search-based refactoring

authors:
Milos Gligoric
Wolfram Schulte
Chandra Prasad
Danny van Velzen
Iman Narasamdya
Benjamin Livshits

abstract: The efficiency of a build system is an important factor for developer productivity. As a result, developer teams have been increasingly adopting new build systems that allow higher build parallelization. However, migrating the existing legacy build scripts to new build systems is a tedious and error-prone process. Unfortunately, there is insufficient support for automated migration of build scripts, making the migration more problematic.


title: Region-based memory management for GPU programming languages: enabling rich data structures on a spartan host

authors:
Eric Holk
Ryan Newton
Jeremy G. Siek
Andrew Lumsdaine

abstract: Graphics processing units (GPUs) can effectively accelerate many applications, but their applicability has been largely limited to problems whose solutions can be expressed neatly in terms of linear algebra. Indeed, most GPU programming languages limit the user to simple data structures - typically only multidimensional rectangular arrays of scalar values. Many algorithms are more naturally expressed using higher level language features, such as algebraic data types (ADTs) and first class procedures, yet building these structures in a manner suitable for a GPU remains a challenge. We present a region-based memory management approach that enables rich data structures in Harlan, a language for data parallel computing. Regions enable rich data structures by providing a uniform representation for pointers on both the CPU and GPU and by providing a means of transferring entire data structures between CPU and GPU memory. We demonstrate Harlan's increased expressiveness on several example programs and show that Harlan performs well on more traditional data-parallel problems.


title: Alembic: automatic locality extraction via migration

authors:
Brandon Holt
Preston Briggs
Luis Ceze
Mark Oskin

abstract: Partitioned Global Address Space (PGAS) environments simplify writing parallel code for clusters because they make data movement implicit - dereferencing global pointers automatically moves data around. However, it does not free the programmer from needing to reason about locality - poor placement of data can lead to excessive and even unnecessary communication. For this reason, modern PGAS languages such as X10, Chapel, and UPC allow programmers to express data-layout constraints and explicitly move computation. This places an extra burden on the programmer, and is less effective for applications with limited or data-dependent locality (e.g., graph analytics).


title: Using web corpus statistics for program analysis

authors:
Chun-Hung Hsiao
Michael J. Cafarella
Satish Narayanasamy

abstract: Several program analysis tools - such as plagiarism detection and bug finding - rely on knowing a piece of code's relative semantic importance. For example, a plagiarism detector should not bother reporting two programs that have an identical simple loop counter test, but should report programs that share more distinctive code. Traditional program analysis techniques (e.g., finding data and control dependencies) are useful, but do not say how surprising or common a line of code is. Natural language processing researchers have encountered a similar problem and addressed it using an n-gram model of text frequency, derived from statistics computed over text corpora.


title: Staged parser combinators for efficient data processing

authors:
Manohar Jonnalagedda
Thierry Coppey
Sandro Stucki
Tiark Rompf
Martin Odersky

abstract: Parsers are ubiquitous in computing, and many applications depend on their performance for decoding data efficiently. Parser combinators are an intuitive tool for writing parsers: tight integration with the host language enables grammar specifications to be interleaved with processing of parse results. Unfortunately, parser combinators are typically slow due to the high overhead of the host language abstraction mechanisms that enable composition.


title: An experimental survey of energy management across the stack

authors:
Melanie Kambadur
Martha A. Kim

abstract: Modern demand for energy-efficient computation has spurred research at all levels of the stack, from devices to microarchitecture, operating systems, compilers, and languages. Unfortunately, this breadth has resulted in a disjointed space, with technologies at different levels of the system stack rarely compared, let alone coordinated.


title: MIX10: compiling MATLAB to X10 for high performance

authors:
Vineet Kumar
Laurie J. Hendren

abstract: MATLAB is a popular dynamic array-based language commonly used by students, scientists and engineers who appreciate the interactive development style, the rich set of array operators, the extensive builtin library, and the fact that they do not have to declare static types. Even though these users like to program in MATLAB, their computations are often very compute-intensive and are better suited for emerging high performance computing systems. This paper reports on MIX10, a source-to-source compiler that automatically translates MATLAB programs to X10, a language designed for "Performance and Productivity at Scale"; thus, helping scientific programmers make better use of high performance computing systems.


title: Flint: fixing linearizability violations

authors:
Peng Liu
Omer Tripp
Xiangyu Zhang

abstract: Writing concurrent software while achieving both correctness and efficiency is a grand challenge. To facilitate this task, concurrent data structures have been introduced into the standard library of popular languages like Java and C#. Unfortunately, while the operations exposed by concurrent data structures are atomic (or linearizable), compositions of these operations are not necessarily atomic. Recent studies have found many erroneous implementations of composed concurrent operations.


title: Chisel: reliability- and accuracy-aware optimization of approximate computational kernels

authors:
Sasa Misailovic
Michael Carbin
Sara Achour
Zichao Qi
Martin C. Rinard

abstract: The accuracy of an approximate computation is the distance between the result that the computation produces and the corresponding fully accurate result. The reliability of the computation is the probability that it will produce an acceptably accurate result. Emerging approximate hardware platforms provide approximate operations that, in return for reduced energy consumption and/or increased performance, exhibit reduced reliability and/or accuracy.


title: i3QL: language-integrated live data views

authors:
Ralf Mitschke
Sebastian Erdweg
Mirko Köhler
Mira Mezini
Guido Salvaneschi

abstract: An incremental computation updates its result based on a change to its input, which is often an order of magnitude faster than a recomputation from scratch. In particular, incrementalization can make expensive computations feasible for settings that require short feedback cycles, such as interactive systems, IDEs, or (soft) real-time systems.