bluuebunny/crossref_metadata_2025 huggingface dataset:
Compiler-assisted detection of transient memory errors
Authors: Tavarageri Sanket , Krishnamoorthy Sriram , Sadayappan P.
Published: September 2014

The probability of bit flips in hardware memory systems is projected to increase significantly as memory systems continue to scale in size and complexity. Effective hardware-based error detection and correction require that the complete data path, involving all parts of the memory system, be protected with sufficient redundancy. First, this may be costly to employ on commodity computing platforms, and second, even on high-end systems, protection against multi-bit errors may be lacking. Therefore, augmenting hardware error detection schemes with software techniques is of considerable interest.

In this paper, we consider software-level mechanisms to comprehensively detect transient memory faults. We develop novel compile-time algorithms to instrument application programs with checksum computation codes to detect memory errors. Unlike prior approaches that employ checksums on computational and architectural states, our scheme verifies every data access and works by tracking variables as they are produced and consumed. Experimental evaluation demonstrates that the proposed comprehensive error detection solution is viable as a completely software-only scheme. We also demonstrate that with limited hardware support, overheads of error detection can be further reduced.
FlowDroid
Authors: Arzt Steven , Rasthofer Siegfried , Fritz Christian , Bodden Eric , Bartel Alexandre , Klein Jacques , Le Traon Yves , Octeau Damien , McDaniel Patrick
Published: September 2014

Today's smartphones are a ubiquitous source of private and confidential data. At the same time, smartphone users are plagued by carelessly programmed apps that leak important data by accident, and by malicious apps that exploit their given privileges to copy such data intentionally. While existing static taint-analysis approaches have the potential of detecting such data leaks ahead of time, all approaches for Android use a number of coarse-grain approximations that can yield high numbers of missed leaks and false alarms.

In this work we thus present FlowDroid, a novel and highly precise static taint analysis for Android applications. A precise model of Android's lifecycle allows the analysis to properly handle callbacks invoked by the Android framework, while context, flow, field and object-sensitivity allows the analysis to reduce the number of false alarms. Novel on-demand algorithms help FlowDroid maintain high efficiency and precision at the same time.

We also propose DroidBench, an open test suite for evaluating the effectiveness and accuracy of taint-analysis tools specifically for Android apps. As we show through a set of experiments using SecuriBench Micro, DroidBench, and a set of well-known Android test applications, FlowDroid finds a very high fraction of data leaks while keeping the rate of false positives low. On DroidBench, FlowDroid achieves 93% recall and 86% precision, greatly outperforming the commercial tools IBM AppScan Source and Fortify SCA. FlowDroid successfully finds leaks in a subset of 500 apps from Google Play and about 1,000 malware apps from the VirusShare project.
Stochastic optimization of floating-point programs with tunable precision
Authors: Schkufza Eric , Sharma Rahul , Aiken Alex
Published: September 2014

The aggressive optimization of floating-point computations is an important problem in high-performance computing. Unfortunately, floating-point instruction sets have complicated semantics that often force compilers to preserve programs as written. We present a method that treats floating-point optimization as a stochastic search problem. We demonstrate the ability to generate reduced precision implementations of Intel's handwritten C numeric library which are up to 6 times faster than the original code, and achieve end-to-end speedups of over 30% on a direct numeric simulation and a ray tracer by optimizing kernels that can tolerate a loss of precision while still remaining correct. Because these optimizations are mostly not amenable to formal verification using the current state of the art, we present a stochastic search technique for characterizing maximum error. The technique comes with an asymptotic guarantee and provides strong evidence of correctness.
A theory of changes for higher-order languages
Authors: Cai Yufei , Giarrusso Paolo G. , Rendel Tillmann , Ostermann Klaus
Published: September 2014

If the result of an expensive computation is invalidated by a small change to the input, the old result should be updated incrementally instead of reexecuting the whole computation. We incrementalize programs through their
derivative
. A derivative maps changes in the program's input directly to changes in the program's output, without reexecuting the original program. We present a program transformation taking programs to their derivatives, which is fully static and automatic, supports first-class functions, and produces derivatives amenable to standard optimization.

We prove the program transformation correct in Agda for a family of simply-typed λ-calculi, parameterized by base types and primitives. A precise interface specifies what is required to incrementalize the chosen primitives.

We investigate performance by a case study: We implement in Scala the program transformation, a plugin and improve performance of a nontrivial program by orders of magnitude.
Globally precise-restartable execution of parallel programs
Authors: Gupta Gagan , Sridharan Srinath , Sohi Gurindar S.
Published: September 2014

Emerging trends in computer design and use are likely to make
exceptions
, once rare, the norm, especially as the system size grows. Due to exceptions, arising from hardware faults, approximate computing, dynamic resource management, etc., successful and error-free execution of programs may no longer be assured. Yet, designers will want to tolerate the exceptions so that the programs execute completely, efficiently and without external intervention.

Modern computers easily handle exceptions in sequential programs, using precise interrupts. But they are ill-equipped to handle exceptions in parallel programs, which are growing in prevalence. In this work we introduce the notion of
globally precise-restartable
execution of parallel programs, analogous to precise-interruptible execution of sequential programs. We present a software runtime recovery system based on the approach to handle exceptions in suitably-written parallel programs. Qualitative and quantitative analyses show that the proposed system scales with the system size, especially when exceptions are frequent, unlike the conventional checkpoint-and-recovery method.
First-class runtime generation of high-performance types using exotypes
Authors: DeVito Zachary , Ritchie Daniel , Fisher Matt , Aiken Alex , Hanrahan Pat
Published: September 2014

We introduce
exotypes
, user-defined types that combine the flexibility of meta-object protocols in dynamically-typed languages with the performance control of low-level languages. Like objects in dynamic languages, exotypes are defined programmatically at run-time, allowing behavior based on external data such as a database schema. To achieve high performance, we use staged programming to define the behavior of an exotype during a runtime compilation step and implement exotypes in Terra, a low-level staged programming language.

We show how exotype constructors compose, and use exotypes to implement high-performance libraries for serialization, dynamic assembly, automatic differentiation, and probabilistic programming. Each exotype achieves expressiveness similar to libraries written in dynamically-typed languages but implements optimizations that exceed the performance of existing libraries written in low-level statically-typed languages. Though each implementation is significantly shorter, our serialization library is 11 times faster than Kryo, and our dynamic assembler is 3--20 times faster than Google's Chrome assembler.
Fast
Authors: D'Antoni Loris , Veanes Margus , Livshits Benjamin , Molnar David
Published: September 2014

Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many real-world applications operate over infinite domains such as integers, this is often a limitation. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting infinite alphabets makes these models more general and succinct than their classical counterparts. Despite this, we show how the main operations, such as composition and language equivalence, remain computable given a decision procedure for the alphabet theory.

We introduce a high-level language called Fast that acts as a front-end for the above formalisms. Fast supports symbolic alphabets through tight integration with state-of-the-art satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on practical case studies, covering a wide range of applications.
SCCharts: sequentially constructive statecharts for safety-critical applications
Authors: von Hanxleden Reinhard , Duderstadt Björn , Motika Christian , Smyth Steven , Mendler Michael , Aguado Joaquín , Mercer Stephen , O'Brien Owen
Published: September 2014

We present a new visual language,SCCharts, designed for specifying safety-critical reactive systems. SCCharts use a statechart notation and provide determinate concurrency based on a synchronous model of computation (MoC), without restrictions common to previous synchronous MoCs. Specifically, we lift earlier limitations on sequential accesses to shared variables, by leveraging the sequentially constructive MoC. The semantics and key features of SCCharts are defined by a very small set of elements, theCore SCCharts, consisting of state machines plus fork/join concurrency. We also present a compilation chain that allows efficient synthesis of software and hardware.
Persistent pointer information
Authors: Xiao Xiao , Zhang Qirun , Zhou Jinguo , Zhang Charles
Published: September 2014

Pointer information, indispensable for static analysis tools, is expensive to compute and query. We provide a query-efficient persistence technique, Pestrie, to mitigate the costly computation and slow querying of precise pointer information. Leveraging equivalence and hub properties, Pestrie can compress pointer information and answers pointer related queries very efficiently. The experiment shows that Pestrie produces 10.5X and 17.5X smaller persistent files than the traditional bitmap and BDD encodings. Meanwhile, Pestrie is 2.9X to 123.6X faster than traditional demand-driven approaches for serving points-to related queries.
Maximal sound predictive race detection with control flow abstraction
Authors: Huang Jeff , Meredith Patrick O'Neil , Rosu Grigore
Published: September 2014

Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are unsound, meaning that they report false positives. We present a sound race detection technique that achieves a provably higher detection capability than existing sound techniques. A key insight of our technique is the inclusion of abstracted control flow information into the execution model, which increases the space of the causal model permitted by classical happens-before or causally-precedes based detectors. By encoding the control flow and a minimal set of feasibility constraints as a group of first-order logic formulae, we formulate race detection as a constraint solving problem. Moreover, we formally prove that our formulation achieves the maximal possible detection capability for any sound dynamic race detector with respect to the same input trace under the sequential consistency memory model. We demonstrate via extensive experimentation that our technique detects more races than the other state-of-the-art sound race detection techniques, and that it is scalable to executions of real world concurrent applications with tens of millions of critical events. These experiments also revealed several previously unknown races in real systems (e.g., Eclipse) that have been confirmed or fixed by the developers. Our tool is also adopted by Eclipse developers.
Surgical precision JIT compilers
Authors: Rompf Tiark , Sujeeth Arvind K. , Brown Kevin J. , Lee HyoukJoong , Chafi Hassan , Olukotun Kunle
Published: September 2014

Just-in-time (JIT) compilation of running programs provides more optimization opportunities than offline compilation. Modern JIT compilers, such as those in virtual machines like Oracle's HotSpot for Java or Google's V8 for JavaScript, rely on dynamic profiling as their key mechanism to guide optimizations. While these JIT compilers offer good average performance, their behavior is a black box and the achieved performance is highly unpredictable.

In this paper, we propose to turn JIT compilation into a precision tool by adding two essential and generic metaprogramming facilities: First, allow programs to invoke JIT compilation explicitly. This enables controlled specialization of arbitrary code at run-time, in the style of partial evaluation. It also enables the JIT compiler to report warnings and errors to the program when it is unable to compile a code path in the demanded way. Second, allow the JIT compiler to call back into the program to perform compile-time computation. This lets the program itself define the translation strategy for certain constructs on the fly and gives rise to a powerful JIT macro facility that enables "smart" libraries to supply domain-specific compiler optimizations or safety checks.

We present Lancet, a JIT compiler framework for Java bytecode that enables such a tight, two-way integration with the running program. Lancet itself was derived from a high-level Java bytecode interpreter: staging the interpreter using LMS (Lightweight Modular Staging) produced a simple bytecode compiler. Adding abstract interpretation turned the simple compiler into an optimizing compiler. This fact provides compelling evidence for the scalability of the staged-interpreter approach to compiler construction.

In the case of Lancet, JIT macros also provide a natural interface to existing LMS-based toolchains such as the Delite parallelism and DSL framework, which can now serve as accelerator macros for arbitrary JVM bytecode.
Selective context-sensitivity guided by impact pre-analysis
Authors: Oh Hakjoo , Lee Wonchan , Heo Kihong , Yang Hongseok , Yi Kwangkeun
Published: September 2014

We present a method for selectively applying context-sensitivity during interprocedural program analysis. Our method applies context-sensitivity only when and where doing so is likely to improve the precision that matters for resolving given queries. The idea is to use a pre-analysis to estimate the impact of context-sensitivity on the main analysis's precision, and to use this information to find out when and where the main analysis should turn on or off its context-sensitivity. We formalize this approach and prove that the analysis always benefits from the pre-analysis-guided context-sensitivity. We implemented this selective method for an existing industrial-strength interval analyzer for full C. The method reduced the number of (false) alarms by 24.4%, while increasing the analysis cost by 27.8% on average.

The use of the selective method is not limited to context-sensitivity. We demonstrate this generality by following the same principle and developing a selective relational analysis.
Introspective analysis
Authors: Smaragdakis Yannis , Kastrinis George , Balatsouras George
Published: September 2014

Context-sensitivity is the primary approach for adding more precision to a points-to analysis, while hopefully also maintaining scalability. An oft-reported problem with context-sensitive analyses, however, is that they are bi-modal: either the analysis is precise enough that it manipulates only manageable sets of data, and thus scales impressively well, or the analysis gets quickly derailed at the first sign of imprecision and becomes orders-of-magnitude more expensive than would be expected given the program's size. There is currently no approach that makes precise context-sensitive analyses (of any flavor: call-site-, object-, or type-sensitive) scale across the board at a level comparable to that of a context-insensitive analysis. To address this issue, we propose introspective analysis: a technique for uniformly scaling context-sensitive analysis by eliminating its performance-detrimental behavior, at a small precision expense. Introspective analysis consists of a common adaptivity pattern: first perform a context-insensitive analysis, then use the results to selectively refine (i.e., analyze context-sensitively) program elements that will not cause explosion in the running time or space. The technical challenge is to appropriately identify such program elements. We show that a simple but principled approach can be remarkably effective, achieving scalability (often with dramatic speedup) for benchmarks previously completely out-of-reach for deep context-sensitive analyses.
Code completion with statistical language models
Authors: Raychev Veselin , Vechev Martin , Yahav Eran
Published: September 2014

We address the problem of synthesizing code completions for programs using APIs. Given a program with holes, we synthesize completions for holes with the most likely sequences of method calls.

Our main idea is to reduce the problem of code completion to a natural-language processing problem of predicting probabilities of sentences. We design a simple and scalable static analysis that extracts sequences of method calls from a large codebase, and index these into a statistical language model. We then employ the language model to find the highest ranked sentences, and use them to synthesize a code completion. Our approach is able to synthesize sequences of calls across multiple objects together with their arguments.

Experiments show that our approach is fast and effective. Virtually all computed completions typecheck, and the desired completion appears in the top 3 results in 90% of the cases.
DoubleChecker
Authors: Biswas Swarnendu , Huang Jipeng , Sengupta Aritra , Bond Michael D.
Published: September 2014

Atomicity is a key correctness property that allows programmers to reason about code regions in isolation. However, programs often fail to enforce atomicity correctly, leading to atomicity violations that are difficult to detect. Dynamic program analysis can detect atomicity violations based on an atomicity specification, but existing approaches slow programs substantially.

This paper presents DoubleChecker, a novel sound and precise atomicity checker whose key insight lies in its use of two new cooperating dynamic analyses. Its
imprecise
analysis tracks cross-thread dependences soundly but imprecisely with significantly better performance than a fully precise analysis. Its
precise
analysis is more expensive but only needs to process a subset of the execution identified as potentially involved in atomicity violations by the imprecise analysis. If DoubleChecker operates in
single-run
mode, the two analyses execute in the same program run, which guarantees soundness and precision but requires logging program accesses to pass from the imprecise to the precise analysis. In
multi-run
mode, the first program run executes only the imprecise analysis, and a second run executes both analyses. Multi-run mode trades accuracy for performance; each run of multi-run mode outperforms single-run mode, but can potentially miss violations.

We have implemented DoubleChecker and an existing state-of-the-art atomicity checker called Velodrome in a high-performance Java virtual machine. DoubleChecker's single-run mode significantly outperforms Velodrome, while still providing full soundness and precision. DoubleChecker's multi-run mode improves performance further, without significantly impacting soundness in practice. These results suggest that DoubleChecker's approach is a promising direction for improving the performance of dynamic atomicity checking over prior work.
Natural proofs for data structure manipulation in C using separation logic
Authors: Pek Edgar , Qiu Xiaokang , Madhusudan P.
Published: September 2014

The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32].

In this work, we develop a framework called VCDryad that extends the Vcc framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing Vcc framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing Vcc to find natural proofs using primarily decidable theories.

We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, well-known open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without
any user-provided proof tactics
. VCDryad is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
On abstraction refinement for program analyses in Datalog
Authors: Zhang Xin , Mangal Ravi , Grigore Radu , Naik Mayur , Yang Hongseok
Published: September 2014

A central task for a program analysis concerns how to efficiently find a program abstraction that keeps only information relevant for proving properties of interest. We present a new approach for finding such abstractions for program analyses written in Datalog. Our approach is based on counterexample-guided abstraction refinement: when a Datalog analysis run fails using an abstraction, it seeks to generalize the cause of the failure to other abstractions, and pick a new abstraction that avoids a similar failure. Our solution uses a boolean satisfiability formulation that is general, complete, and optimal: it is independent of the Datalog solver, it generalizes the failure of an abstraction to as many other abstractions as possible, and it identifies the cheapest refined abstraction to try next. We show the performance of our approach on a pointer analysis and a typestate analysis, on eight real-world Java benchmark programs.
Compositional solution space quantification for probabilistic software analysis
Authors: Borges Mateus , Filieri Antonio , d'Amorim Marcelo , Păsăreanu Corina S. , Visser Willem
Published: September 2014

Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.

We present a compositional statistical approach for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. The approach leverages interval constraint propagation to improve the accuracy of the estimation by focusing the sampling on the regions of the input domain containing the sought solutions. Preliminary experiments show significant improvement on previous approaches both in results accuracy and analysis time.
A model counter for constraints over unbounded strings
Authors: Luu Loi , Shinde Shweta , Saxena Prateek , Demsky Brian
Published: September 2014

Model counting is the problem of determining the number of solutions that satisfy a given set of constraints. Model counting has numerous applications in the quantitative analyses of program execution time, information flow, combinatorial circuit designs as well as probabilistic reasoning. We present a new approach to model counting for structured data types, specifically strings in this work. The key ingredient is a new technique that leverages generating functions as a basic primitive for combinatorial counting. Our tool SMC which embodies this approach can model count for constraints specified in an expressive string language efficiently and precisely, thereby outperforming previous finite-size analysis tools. SMC is expressive enough to model constraints arising in real-world JavaScript applications and UNIX C utilities. We demonstrate the practical feasibility of performing quantitative analyses arising in security applications, such as determining the comparative strengths of password strength meters and determining the information leakage via side channels.
Improving JavaScript performance by deconstructing the type system
Authors: Ahn Wonsun , Choi Jiho , Shull Thomas , Garzarán María J. , Torrellas Josep
Published: September 2014

Increased focus on JavaScript performance has resulted in vast performance improvements for many benchmarks. However, for actual code used in websites, the attained improvements often lag far behind those for popular benchmarks.

This paper shows that the main reason behind this short-fall is how the compiler understands types. JavaScript has no concept of types, but the compiler assigns types to objects anyway for ease of code generation. We examine the way that the Chrome V8 compiler defines types, and identify two design decisions that are the main reasons for the lack of improvement: (1) the inherited prototype object is part of the current object's type definition, and (2) method bindings are also part of the type definition. These requirements make types very unpredictable, which hinders type specialization by the compiler. Hence, we modify V8 to remove these requirements, and use it to compile the JavaScript code assembled by JSBench from real websites. On average, we reduce the execution time of JSBench by 36%, and the dynamic instruction count by 49%.
FlashExtract
Authors: Le Vu , Gulwani Sumit
Published: September 2014

Various document types that combine model and view (e.g., text files, webpages, spreadsheets) make it easy to organize (possibly hierarchical) data, but make it difficult to extract raw data for any further manipulation or querying. We present a general framework FlashExtract to extract relevant data from semi-structured documents using examples. It includes: (a) an interaction model that allows end-users to give examples to extract various fields and to relate them in a hierarchical organization using structure and sequence constructs. (b) an inductive synthesis algorithm to synthesize the intended program from few examples in
any
underlying domain-specific language for data extraction that has been built using our specified algebra of few core operators (map, filter, merge, and pair). We describe instantiation of our framework to three different domains: text files, webpages, and spreadsheets. On our benchmark comprising 75 documents, FlashExtract is able to extract intended data using an average of 2.36 examples in 0.84 seconds per field.
Accurate application progress analysis for large-scale parallel debugging
Authors: Mitra Subrata , Laguna Ignacio , Ahn Dong H. , Bagchi Saurabh , Schulz Martin , Gamblin Todd
Published: September 2014

Debugging large-scale parallel applications is challenging. In most HPC applications, parallel tasks progress in a coordinated fashion, and thus a fault in one task can quickly propagate to other tasks, making it difficult to debug. Finding the least-progressed tasks can significantly reduce the effort to identify the task where the fault originated. However, existing approaches for detecting them suffer low accuracy and large overheads; either they use imprecise static analysis or are unable to infer progress dependence inside loops. We present a loop-aware progress-dependence analysis tool, Prodometer, which determines relative progress among parallel tasks via dynamic analysis. Our fault-injection experiments suggest that its accuracy and precision are over 90% for most cases and that it scales well up to 16,384 MPI tasks. Further, our case study shows that it significantly helped diagnosing a perplexing error in MPI, which only manifested at large scale.
Automatic runtime error repair and containment via recovery shepherding
Authors: Long Fan , Sidiroglou-Douskos Stelios , Rinard Martin
Published: September 2014

We present a system, RCV, for enabling software applications to survive divide-by-zero and null-dereference errors. RCV operates directly on off-the-shelf, production, stripped x86 binary executables. RCV implements
recovery shepherding
, which attaches to the application process when an error occurs, repairs the execution, tracks the repair effects as the execution continues, contains the repair effects within the application process, and detaches from the process after all repair effects are flushed from the process state. RCV therefore incurs negligible overhead during the normal execution of the application.

We evaluate RCV on all divide-by-zero and null-dereference errors available in the CVE database [2] from January 2011 to March 2013 that 1) provide publicly-available inputs that trigger the error which 2) we were able to use to trigger the reported error in our experimental environment. We collected a total of 18 errors in seven real world applications, Wireshark, the FreeType library, Claws Mail, LibreOffice, GIMP, the PHP interpreter, and Chromium. For 17 of the 18 errors, RCV enables the application to continue to execute to provide acceptable output and service to its users on the error-triggering inputs. For 13 of the 18 errors, the continued RCV execution eventually flushes all of the repair effects and RCV detaches to restore the application to full clean functionality. We perform a manual analysis of the source code relevant to our benchmark errors, which indicates that for 11 of the 18 errors the RCV and later patched versions produce identical or equivalent results on all inputs.
Automating formal proofs for reactive systems
Authors: Ricketts Daniel , Robert Valentin , Jang Dongseok , Tatlock Zachary , Lerner Sorin
Published: September 2014

Implementing systems in proof assistants like Coq and proving their correctness in full formal detail has consistently demonstrated promise for making extremely strong guarantees about critical software, ranging from compilers and operating systems to databases and web browsers. Unfortunately, these verifications demand such heroic manual proof effort, even for a
single
system, that the approach has not been widely adopted.

We demonstrate a technique to eliminate the manual proof burden for verifying many properties within an entire
class
of applications, in our case reactive systems, while only expending effort comparable to the manual verification of a single system. A crucial insight of our approach is simultaneously designing both (1) a domain-specific language (DSL) for expressing reactive systems and their correctness properties and (2) proof automation which exploits the constrained language of both programs and properties to enable fully automatic, pushbutton verification. We apply this insight in a deeply embedded Coq DSL, dubbed Reflex, and illustrate Reflex's expressiveness by implementing and automatically verifying realistic systems including a modern web browser, an SSH server, and a web server. Using Reflex radically reduced the proof burden: in previous, similar versions of our benchmarks written in Coq by experts, proofs accounted for over 80% of the code base; our versions require no manual proofs.
Chlorophyll
Authors: Phothilimthana Phitchaya Mangpo , Jelvis Tikhon , Shah Rohin , Totla Nishant , Chasins Sarah , Bodik Rastislav
Published: September 2014

We developed Chlorophyll, a synthesis-aided programming model and compiler for the GreenArrays GA144, an extremely minimalist low-power spatial architecture that requires partitioning the program into fragments of no more than 256 instructions and 64 words of data. This processor is 100-times more energy efficient than its competitors, but currently can only be programmed using a low-level stack-based language.

The Chlorophyll programming model allows programmers to provide human insight by specifying partial partitioning of data and computation. The Chlorophyll compiler relies on synthesis, sidestepping the need to develop classical optimizations, which may be challenging given the unusual architecture. To scale synthesis to real problems, we decompose the compilation into smaller synthesis subproblems---partitioning, layout, and code generation. We show that the synthesized programs are no more than 65% slower than highly optimized expert-written programs and are faster than programs produced by a heuristic, non-synthesizing version of our compiler.
A framework for enhancing data reuse via associative reordering
Authors: Stock Kevin , Kong Martin , Grosser Tobias , Pouchet Louis-Noël , Rastello Fabrice , Ramanujam J. , Sadayappan P.
Published: September 2014

The freedom to reorder computations involving associative operators has been widely recognized and exploited in designing parallel algorithms and to a more limited extent in optimizing compilers.

In this paper, we develop a novel framework utilizing the associativity and commutativity of operations in regular loop computations to enhance register reuse. Stencils represent a particular class of important computations where the optimization framework can be applied to enhance performance. We show how stencil operations can be implemented to better exploit register reuse and reduce load/stores. We develop a multi-dimensional retiming formalism to characterize the space of valid implementations in conjunction with other program transformations. Experimental results demonstrate the effectiveness of the framework on a collection of high-order stencils.
Tracelet-based code search in executables
Authors: David Yaniv , Yahav Eran
Published: September 2014

We address the problem of code search in executables. Given a function in binary form and a large code base, our goal is to statically find similar functions in the code base. Towards this end, we present a novel technique for computing similarity between functions. Our notion of similarity is based on decomposition of functions into
tracelets
: continuous, short, partial traces of an execution. To establish tracelet similarity in the face of low-level compiler transformations, we employ a simple rewriting engine. This engine uses constraint solving over alignment constraints and data dependencies to match registers and memory addresses between tracelets, bridging the gap between tracelets that are otherwise similar. We have implemented our approach and applied it to find matches in
over a million
binary functions. We compare tracelet matching to approaches based on n-grams and graphlets and show that tracelet matching obtains dramatically better precision and recall.
Æminium
Authors: Stork Sven , Naden Karl , Sunshine Joshua , Mohr Manual , Fonseca Alcides , Marques Paulo , Aldrich Jonathan
Published: September 2014

The aim of ÆMINIUM is to study the implications of having a concurrent-by-default programming language. This includes language design, runtime system, performance and software engineering considerations.

We conduct our study through the design of the concurrent-by-default ÆMINIUM programming language. ÆMINIUM leverages the permission flow of object and group permissions through the program to validate the program's correctness and to automatically infer a possible parallelization strategy via a dataflow graph. ÆMINIUM supports not only fork-join parallelism but more general dataflow patterns of parallelism.

In this paper we present a formal system, called μÆMINIUM, modeling the core concepts of ÆMINIUM. μÆMINIUM's static type system is based on Featherweight Java with ÆMINIUM-specific extensions. Besides checking for correctness ÆMINIUM's type system it also uses the permission flow to compute a potential parallel execution strategy for the program. μÆMINIUM's dynamic semantics use a concurrent-by-default evaluation approach. Along with the formal system we present its soundness proof.

We provide a full description of the implementation along with the description of various optimization techniques we used. We implemented ÆMINIUM as an extension of the Plaid programming language, which has first-class support for permissions built-in. The ÆMINIUM implementation and all case studies are publicly available under the General Public License.

We use various case studies to evaluate ÆMINIUM's applicability and to demonstrate that ÆMINIUM parallelized code has performance improvements compared to its sequential counterpart. We chose to use case studies from common domains or problems that are known to benefit from parallelization, to show that ÆMINIUM is powerful enough to encode them. We demonstrate through a webserver application, which evaluates ÆMINIUM's impact on latency-bound applications, that ÆMINIUM can achieve a 70% performance improvement over the sequential counterpart. In another case study we chose to implement a dictionary function to evaluate ÆMINIUM's capabilities to express essential data structures. Our evaluation demonstrates that ÆMINIUM can be used to express parallelism in such data-structures and that the performance benefits scale with the amount of annotation effort which is put into the implementation. We chose an integral computationally example to evaluate pure functional programming and computational intensive use cases. Our experiments show that ÆMINIUM is capable of extracting parallelism from functional code and achieving performance improvements up to the limits of Plaid's inherent performance bounds.

Overall, we hope that the work helps to advance concurrent programming in modern programming environments.
Specialization slicing
Authors: Aung Min , Horwitz Susan , Joiner Rich , Reps Thomas
Published: September 2014

In this paper, we investigate opportunities to be gained from broadening the definition of program slicing. A major inspiration for our work comes from the field of partial evaluation, in which a wide repertoire of techniques have been developed for specializing programs. While slicing can also be harnessed for specializing programs, the kind of specialization obtainable via slicing has heretofore been quite restricted, compared to the kind of specialization allowed in partial evaluation. In particular, most slicing algorithms are what the partial-evaluation community calls
monovariant
: each program element of the original program generates
at most one element
in the answer. In contrast, partial-evaluation algorithms can be
polyvariant
, i.e., one program element in the original program may correspond to more than one element in the specialized program.

The full paper appears in
ACM TOPLAS 36
(2), 2014.
Atomicity refinement for verified compilation
Authors: Jagannathan Suresh , Laporte Vincent , Petri Gustavo , Pichardie David , Vitek Jan
Published: September 2014

We consider the
verified compilation
of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. In this environment, the interactions between application threads and the language runtime (
e.g.
, the garbage collector) are regulated by compiler-injected code snippets. Example of snippets include allocation fast paths among others. In our TOPLAS paper we propose a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector.
ASAC
Authors: Roy Pooja , Ray Rajarshi , Wang Chundong , Wong Weng Fai
Published: September 2014

The approximation based programming paradigm is especially attractive for developing error-resilient applications, targeting low power embedded devices. It allows for program data to be computed and stored approximately for better energy efficiency. The duration of battery in the smartphones, tablets, etc. is generally more of a concern to users than an application's accuracy or fidelity beyond certain acceptable quality of service. Therefore, relaxing accuracy to improve energy efficiency is an attractive trade-off when permissible by the application's domain. Recent works suggest source code annotations and type qualifiers to facilitate safe approximate computation and data manipulation. It requires rewriting of programs or the availability of source codes for annotations. This may not be feasible as real-world applications tend to be large, with source code that is not readily available.

In this paper, we propose a novel sensitivity analysis that automatically generates annotations for programs for the purpose of approximate computing. Our framework, ASAC, extracts information about the sensitivity of the output with respect to program data. We show that the program output is sensitive to only a subset of program data that we deem critical, and hence must be precise. The rest of the data can be computed and stored approximately.We evaluated our analysis on a range of applications, and achieved a 86% accuracy compared to manual annotations by programmers. We validated our analysis by showing that the applications are within the acceptable QoS threshold if we approximate the non-critical data.
CASM
Authors: Lezuo Roland , Paulweber Philipp , Krall Andreas
Published: September 2014

In this paper we present CASM, a language based on Abstract State Machines (ASM), and its optimizing compiler. ASM is a well-defined (formal) method based on algebraic concepts. A distinct feature of ASM is its combination of parallel and sequential execution semantics. This makes it an excellent choice to formally specify and verify micro-architectures. We present a compilation scheme and an implementation of a runtime system supporting efficient execution of ASM.

After introducing novel analysis techniques we present optimizations allowing us to eliminate many costly operations.

Benchmark results show that our baseline compiler is 2-3 magnitudes faster than other ASM implementations. The optimizations further increase the performance of the compiled programs up to 264%. The achieved performance allows our ASM implementation to be used with industry-size applications.
Cache-related preemption delay analysis for FIFO caches
Authors: Ballabriga Clément , Chong Lee Kee , Roychoudhury Abhik
Published: September 2014

Hard real-time systems are typically composed of multiple tasks, subjected to timing constraints. To guarantee that these constraints will be respected, the Worst-Case Response Time (WCRT) of each task is needed. In the presence of systems supporting preemptible tasks, we need to take into account the time lost due to task preemption. A major part of this delay is the Cache-Related Preemption Delay (CRPD), which represents the penalties due to cache block evictions by preempting tasks. Previous works on CRPD have focused on caches with Least Recently used (LRU) replacement policy. However, for many real-world processors such as ARM9 or ARM11, the use of First-in-first-out (FIFO) cache replacement policy is common.

In this paper, we propose an approach to compute CRPD in the presence of instruction caches with FIFO replacement policy. We use the result of a FIFO instruction cache categorization analysis to account for single-task cache misses, and we model as an Integer Linear Programming (ILP) system the additional preemption-related cache misses. We study the effect of cache related timing anomalies, our work is the first to deal with the effect of timing anomalies in CRPD computation. We also present a WCRT computation method that takes advantage of the fact that our computed CRPD does not increase linearly with respect to the preemption count. We evaluated our method by computing the CRPD with realistic benchmarks (e.g. drone control application, robot controller application), under various cache configuration parameters. The experimentation shows that our method is able to compute tight CRPD bound for benchmark tasks.
Combinatorial spill code optimization and ultimate coalescing
Authors: Castañeda Lozano Roberto , Carlsson Mats , Hjort Blindell Gabriel , Schulte Christian
Published: September 2014

This paper presents a novel combinatorial model that integrates global register allocation based on ultimate coalescing, spill code optimization, register packing, and multiple register banks with instruction scheduling (including VLIW). The model exploits alternative temporaries that hold the same value as a new concept for ultimate coalescing and spill code optimization.

The paper presents Unison as a code generator based on the model and advanced solving techniques using constraint programming. Thorough experiments using MediaBench and a processor (Hexagon) that are typical for embedded systems demonstrate that Unison: is robust and scalable; generates faster code than LLVM (up to 41% with a mean improvement of 7%); possibly generates optimal code (for 29% of the experiments); effortlessly supports different optimization criteria (code size on par with LLVM).

Unison is significant as it addresses the same aspects as traditional code generation algorithms, yet is based on a simple integrated model and robustly can generate optimal code.
Superoptimization of memory subsystems
Authors: Wingbermuehle Joseph G. , Cytron Ron K. , Chamberlain Roger D.
Published: September 2014

The disparity in performance between processors and main memories has led computer architects to incorporate large cache hierarchies in modern computers. Because these cache hierarchies are designed to be general-purpose, they may not provide the best possible performance for a given application. In this paper, we determine a memory subsystem well suited for a given application and main memory by discovering a memory subsystem comprised of caches,scratchpads, and other components that are combined to provide better performance. We draw motivation from the superoptimization of instruction sequences, which successfully finds unusually clever instruction sequences for programs. Targeting both ASIC and FPGA devices, we show that it is possible to discover unusual memory subsystems that provide performance improvements over a typical memory subsystem.