A B C D E F G H I J K L M N O P Q R S T V W Y Z

	Agrawal, Kunal	PLDI '15: "Efficient Execution of Recursive ..." Efficient Execution of Recursive Programs on Commodity Vector Hardware Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni (Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA) The pursuit of computational efficiency has led to the proliferation of throughput-oriented hardware, from GPUs to increasingly wide vector units on commodity processors and accelerators. This hardware is designed to efficiently execute data-parallel computations in a vectorized manner. However, many algorithms are more naturally expressed as divide-and-conquer, recursive, task-parallel computations. In the absence of data parallelism, it seems that such algorithms are not well suited to throughput-oriented architectures. This paper presents a set of novel code transformations that expose the data parallelism latent in recursive, task-parallel programs. These transformations facilitate straightforward vectorization of task-parallel programs on commodity hardware. We also present scheduling policies that maintain high utilization of vector resources while limiting space usage. Across several task-parallel benchmarks, we demonstrate both efficient vector resource utilization and substantial speedup on chips using Intel’s SSE4.2 vector units, as well as accelerators using Intel’s AVX512 units. @InProceedings{PLDI15p509, author = {Bin Ren and Youngjoon Jo and Sriram Krishnamoorthy and Kunal Agrawal and Milind Kulkarni}, title = {Efficient Execution of Recursive Programs on Commodity Vector Hardware}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {509--520}, doi = {}, year = {2015}, } aec-badge-pldi
	Aiken, Alex	PLDI '15: "Composing Concurrency Control ..." Composing Concurrency Control Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv (Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India) Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking. @InProceedings{PLDI15p240, author = {Ofri Ziv and Alex Aiken and Guy Golan-Gueta and G. Ramalingam and Mooly Sagiv}, title = {Composing Concurrency Control}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {240--249}, doi = {}, year = {2015}, } Video PLDI '15: "Verification of Producer-Consumer ..." Verification of Producer-Consumer Synchronization in GPU Programs Rahul Sharma, Michael Bauer, and Alex Aiken (Stanford University, USA; NVIDIA Research, USA) Previous efforts to formally verify code written for GPUs have focused solely on kernels written within the traditional data-parallel GPU programming model. No previous work has considered the higher performance, but more complex, warp-specialized kernels based on producer-consumer named barriers available on current hardware. In this work we present the first formal operational semantics for named barriers and define what it means for a warp-specialized kernel to be correct. We give algorithms for verifying the correctness of warp-specialized kernels and prove that they are both sound and complete for the most common class of warp-specialized programs. We also present WEFT, a verification tool for checking warp-specialized code. Using WEFT, we discover several non-trivial bugs in production warp-specialized kernels. @InProceedings{PLDI15p88, author = {Rahul Sharma and Michael Bauer and Alex Aiken}, title = {Verification of Producer-Consumer Synchronization in GPU Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {88--98}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Amarasinghe, Saman	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, } PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Anderson, Thomas	PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Ansel, Jason	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, }
	Appel, Andrew W.	PLDI '15: "Verification of a Cryptographic ..." Verification of a Cryptographic Primitive: SHA-256 (Abstract) Andrew W. Appel (Princeton University, USA) A full formal machine-checked verification of a C program: the OpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C is a separation logic for the C language, proved sound w.r.t. the operational semantics for C, connected to the CompCert verified optimizing C compiler. @InProceedings{PLDI15p153, author = {Andrew W. Appel}, title = {Verification of a Cryptographic Primitive: SHA-256 (Abstract)}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {153--153}, doi = {}, year = {2015}, }
	Balakrishna, Shruthi	PLDI '15: "Tree Dependence Analysis ..." Tree Dependence Analysis Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni (Purdue University, USA) We develop a new framework for analyzing recursive methods that perform traversals over trees, called tree dependence analysis. This analysis translates dependence analysis techniques for regular programs to the irregular space, identifying the structure of dependences within a recursive method that traverses trees. We develop a dependence test that exploits the dependence structure of such programs, and can prove that several locality- and parallelism- enhancing transformations are legal. In addition, we extend our analysis with a novel path-dependent, conditional analysis to refine the dependence test and prove the legality of transformations for a wider range of algorithms. We then use these analyses to show that several common algorithms that manipulate trees recursively are amenable to several locality- and parallelism-enhancing transformations. This work shows that classical dependence analysis techniques, which have largely been confined to nested loops over array data structures, can be extended and translated to work for complex, recursive programs that operate over pointer-based data structures. @InProceedings{PLDI15p314, author = {Yusheng Weijiang and Shruthi Balakrishna and Jianqiao Liu and Milind Kulkarni}, title = {Tree Dependence Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {314--325}, doi = {}, year = {2015}, } aec-badge-pldi
	Banerjee, Anindya	PLDI '15: "Mechanized Verification of ..." Mechanized Verification of Fine-Grained Concurrent Programs Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee (IMDEA Software Institute, Spain) Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization. In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded DSL in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures. @InProceedings{PLDI15p77, author = {Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee}, title = {Mechanized Verification of Fine-Grained Concurrent Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {77--87}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Barowy, Daniel W.	PLDI '15: "FlashRelate: Extracting Relational ..." FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn (University of Massachusetts at Amherst, USA; Microsoft Research, USA) With hundreds of millions of users, spreadsheets are one of the most important end-user applications. Spreadsheets are easy to use and allow users great flexibility in storing data. This flexibility comes at a price: users often treat spreadsheets as a poor man's database, leading to creative solutions for storing high-dimensional data. The trouble arises when users need to answer queries with their data. Data manipulation tools make strong assumptions about data layouts and cannot read these ad-hoc databases. Converting data into the appropriate layout requires programming skills or a major investment in manual reformatting. The effect is that a vast amount of real-world data is "locked-in" to a proliferation of one-off formats. We introduce FlashRelate, a synthesis engine that lets ordinary users extract structured relational data from spreadsheets without programming. Instead, users extract data by supplying examples of output relational tuples. FlashRelate uses these examples to synthesize a program in Flare. Flare is a novel extraction language that extends regular expressions with geometric constructs. An interactive user interface on top of FlashRelate lets end users extract data by point-and-click. We demonstrate that correct Flare programs can be synthesized in seconds from a small set of examples for 43 real-world scenarios. Finally, our case study demonstrates FlashRelate's usefulness addressing the widespread problem of data trapped in corporate and government formats. @InProceedings{PLDI15p218, author = {Daniel W. Barowy and Sumit Gulwani and Ted Hart and Benjamin Zorn}, title = {FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {218--228}, doi = {}, year = {2015}, } aec-badge-pldi
	Bauer, Michael	PLDI '15: "Verification of Producer-Consumer ..." Verification of Producer-Consumer Synchronization in GPU Programs Rahul Sharma, Michael Bauer, and Alex Aiken (Stanford University, USA; NVIDIA Research, USA) Previous efforts to formally verify code written for GPUs have focused solely on kernels written within the traditional data-parallel GPU programming model. No previous work has considered the higher performance, but more complex, warp-specialized kernels based on producer-consumer named barriers available on current hardware. In this work we present the first formal operational semantics for named barriers and define what it means for a warp-specialized kernel to be correct. We give algorithms for verifying the correctness of warp-specialized kernels and prove that they are both sound and complete for the most common class of warp-specialized programs. We also present WEFT, a verification tool for checking warp-specialized code. Using WEFT, we discover several non-trivial bugs in production warp-specialized kernels. @InProceedings{PLDI15p88, author = {Rahul Sharma and Michael Bauer and Alex Aiken}, title = {Verification of Producer-Consumer Synchronization in GPU Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {88--98}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Bosboom, Jeffrey	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Bowman, William J.	PLDI '15: "Profile-Guided Meta-Programming ..." Profile-Guided Meta-Programming William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig (Northeastern University, USA; Cisco Systems, USA) Contemporary compiler systems such as GCC, .NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems---the syntactic extensions systems of Chez Scheme and Racket---and provide several profile-guided meta-programs as usability case studies. @InProceedings{PLDI15p403, author = {William J. Bowman and Swaha Miller and Vincent St-Amour and R. Kent Dybvig}, title = {Profile-Guided Meta-Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {403--412}, doi = {}, year = {2015}, }
	Burgstaller, Bernd	PLDI '15: "LaminarIR: Compile-Time Queues ..." LaminarIR: Compile-Time Queues for Structured Streams Yousun Ko, Bernd Burgstaller, and Bernhard Scholz (Yonsei University, South Korea; University of Sydney, Australia) Stream programming languages employ FIFO (first-in, first-out) semantics to model data channels between producers and consumers. A FIFO data channel stores tokens in a buffer that is accessed indirectly via read- and write-pointers. This indirect token-access decouples a producer’s write-operations from the read-operations of the consumer, thereby making dataflow implicit. For a compiler, indirect token-access obscures data-dependencies, which renders standard optimizations ineffective and impacts stream program performance negatively. In this paper we propose a transformation for structured stream programming languages such as StreamIt that shifts FIFO buffer management from run-time to compile-time and eliminates splitters and joiners, whose task is to distribute and merge streams. To show the effectiveness of our lowering transformation, we have implemented a StreamIt to C compilation framework. We have developed our own intermediate representation (IR) called LaminarIR, which facilitates the transformation. We report on the enabling effect of the LaminarIR on LLVM’s optimizations, which required the conversion of several standard StreamIt benchmarks from static to randomized input, to prevent computation of partial results at compile-time. We conducted our experimental evaluation on the Intel i7-2600K, AMD Opteron 6378, Intel Xeon Phi 3120A and ARM Cortex-A15 platforms. Our LaminarIR reduces data-communication on average by 35.9% and achieves platform-specific speedups between 3.73x and 4.98x over StreamIt. We reduce memory accesses by more than 60% and achieve energy savings of up to 93.6% on the Intel i7-2600K. @InProceedings{PLDI15p121, author = {Yousun Ko and Bernd Burgstaller and Bernhard Scholz}, title = {LaminarIR: Compile-Time Queues for Structured Streams}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {121--130}, doi = {}, year = {2015}, } Info
	Carbonneaux, Quentin	PLDI '15: "Compositional Certified Resource ..." Compositional Certified Resource Bounds Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao (Yale University, USA) This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for state-of-the-art techniques: compositionality, user interaction, generation of proof certificates, and scalability. Compositionality is achieved by incorporating the potential method of amortized analysis. It enables the derivation of global whole-program bounds with local derivation rules by naturally tracking size changes of variables in sequenced loops and function calls. The resource consumption of functions is described abstractly and a function call can be analyzed without access to the function body. User interaction is supported with a new mechanism that clearly separates qualitative and quantitative verification. A user can guide the analysis to derive complex non-linear bounds by using auxiliary variables and assertions. The assertions are separately proved using established qualitative techniques such as abstract interpretation or Hoare logic. Proof certificates are automatically generated from the local derivation rules. A soundness proof of the derivation system with respect to a formal cost semantics guarantees the validity of the certificates. Scalability is attained by an efficient reduction of bound inference to a linear optimization problem that can be solved by off-the-shelf LP solvers. The analysis framework is implemented in the publicly-available tool C4B. An experimental evaluation demonstrates the advantages of the new technique with a comparison of C4B with existing tools on challenging micro benchmarks and the analysis of more than 2900 lines of C code from the cBench benchmark suite. @InProceedings{PLDI15p467, author = {Quentin Carbonneaux and Jan Hoffmann and Zhong Shao}, title = {Compositional Certified Resource Bounds}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {467--478}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Černý, Pavol	PLDI '15: "Efficient Synthesis of Network ..." Efficient Synthesis of Network Updates Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster (University of Colorado at Boulder, USA; Cornell University, USA) Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes. @InProceedings{PLDI15p196, author = {Jedidiah McClurg and Hossein Hojjat and Pavol Černý and Nate Foster}, title = {Efficient Synthesis of Network Updates}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {196--207}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Chaudhuri, Swarat	PLDI '15: "Synthesizing Data Structure ..." Synthesizing Data Structure Transformations from Input-Output Examples John K. Feser, Swarat Chaudhuri, and Isil Dillig (Rice University, USA; University of Texas at Austin, USA) We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples. Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs. We have implemented our method in a tool called λ2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of λ2. A highlight is the synthesis of a program believed to be the world's earliest functional pearl. @InProceedings{PLDI15p229, author = {John K. Feser and Swarat Chaudhuri and Isil Dillig}, title = {Synthesizing Data Structure Transformations from Input-Output Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {229--239}, doi = {}, year = {2015}, }
	Chin, Wei-Ngan	PLDI '15: "Termination and Non-termination ..." Termination and Non-termination Specification Inference Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin (National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China) Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non- termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers. @InProceedings{PLDI15p489, author = {Ton Chanh Le and Shengchao Qin and Wei-Ngan Chin}, title = {Termination and Non-termination Specification Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {489--498}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Chitil, Olaf	PLDI '15: "Algorithmic Debugging of Real-World ..." Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack Maarten Faddegon and Olaf Chitil (University of Kent, UK) Existing algorithmic debuggers for Haskell require a transformation of all modules in a program, even libraries that the user does not want to debug and which may use language features not supported by the debugger. This is a pity, because a promising approach to debugging is therefore not applicable to many real-world programs. We use the cost centre stack from the Glasgow Haskell Compiler profiling environment together with runtime value observations as provided by the Haskell Object Observation Debugger (HOOD) to collect enough information for algorithmic debugging. Program annotations are in suspected modules only. With this technique algorithmic debugging is applicable to a much larger set of Haskell programs. This demonstrates that for functional languages in general a simple stack trace extension is useful to support tasks such as profiling and debugging. @InProceedings{PLDI15p33, author = {Maarten Faddegon and Olaf Chitil}, title = {Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {33--42}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Chong, Nathan	PLDI '15: "Many-Core Compiler Fuzzing ..." Many-Core Compiler Fuzzing Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson (Imperial College London, UK; University College London, UK) We address the compiler correctness problem for many-core systems through novel applications of fuzz testing to OpenCL compilers. Focusing on two methods from prior work, random differential testing and testing via equivalence modulo inputs (EMI), we present several strategies for random generation of deterministic, communicating OpenCL kernels, and an injection mechanism that allows EMI testing to be applied to kernels that otherwise exhibit little or no dynamically-dead code. We use these methods to conduct a large, controlled testing campaign with respect to 21 OpenCL (device, compiler) configurations, covering a range of CPU, GPU, accelerator, FPGA and emulator implementations. Our study provides independent validation of claims in prior work related to the effectiveness of random differential testing and EMI testing, proposes novel methods for lifting these techniques to the many-core setting and reveals a significant number of OpenCL compiler bugs in commercial implementations. @InProceedings{PLDI15p65, author = {Christopher Lidbury and Andrei Lascu and Nathan Chong and Alastair F. Donaldson}, title = {Many-Core Compiler Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {65--76}, doi = {}, year = {2015}, } aec-badge-pldi
	Chong, Stephen	PLDI '15: "Exploring and Enforcing Security ..." Exploring and Enforcing Security Guarantees via Program Dependence Graphs Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong (Harvard University, USA; MIT Lincoln Laboratory, USA) We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities. @InProceedings{PLDI15p291, author = {Andrew Johnson and Lucas Waye and Scott Moore and Stephen Chong}, title = {Exploring and Enforcing Security Guarantees via Program Dependence Graphs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {291--302}, doi = {}, year = {2015}, }
	Chu, Duc-Hiep	PLDI '15: "Automatic Induction Proofs ..." Automatic Induction Proofs of Data-Structures in Imperative Programs Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh (National University of Singapore, Singapore) We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we find a sequence of transformations that produces a final formula which is obviously provable by simply matching terms. Our contribution here is the addition of the fundamental principle of induction to this automated process. We first show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained by using the fold/unfold operations. While the adding of induction is an obvious need in general, no automated method has managed to include this in a systematic and general way. The main reason for this is the problem of avoiding circular reasoning. We overcome this with a novel checking condition. In summary, our contribution is a proof method which – beyond U+M – performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. In the practical evaluation part of this paper, we show how the commonly used technique of using unproven lemmas can be avoided, using realistic benchmarks. This not only removes the current burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce a large search space. In the end, our method can automatically reason about a new class of formulas arising from practical program verification. @InProceedings{PLDI15p457, author = {Duc-Hiep Chu and Joxan Jaffar and Minh-Thai Trinh}, title = {Automatic Induction Proofs of Data-Structures in Imperative Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {457--466}, doi = {}, year = {2015}, }
	Crary, Karl	PLDI '15: "Peer-to-Peer Affine Commitment ..." Peer-to-Peer Affine Commitment using Bitcoin Karl Crary and Michael J. Sullivan (Carnegie Mellon University, USA) The power of linear and affine logic lies in their ability to model state change. However, in a trustless, peer-to-peer setting, it is difficult to force principals to commit to state changes. We show how to solve the peer-to-peer affine commitment problem using a generalization of Bitcoin in which transactions deal in types rather than numbers. This has applications to proof-carrying authorization and mechanically executable contracts. Importantly, our system can be---and is---implemented on top of the existing Bitcoin network, so there is no need to recruit computing power to a new protocol. @InProceedings{PLDI15p479, author = {Karl Crary and Michael J. Sullivan}, title = {Peer-to-Peer Affine Commitment using Bitcoin}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {479--488}, doi = {}, year = {2015}, }
	Deligiannis, Pantazis	PLDI '15: "Asynchronous Programming, ..." Asynchronous Programming, Analysis and Testing with State Machines Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson (Imperial College London, UK; Microsoft Research, India) Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. @InProceedings{PLDI15p154, author = {Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema and Akash Lal and Paul Thomson}, title = {Asynchronous Programming, Analysis and Testing with State Machines}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154--164}, doi = {}, year = {2015}, } aec-badge-pldi
	Dillig, Isil	PLDI '15: "Synthesizing Data Structure ..." Synthesizing Data Structure Transformations from Input-Output Examples John K. Feser, Swarat Chaudhuri, and Isil Dillig (Rice University, USA; University of Texas at Austin, USA) We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples. Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs. We have implemented our method in a tool called λ2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of λ2. A highlight is the synthesis of a program believed to be the world's earliest functional pearl. @InProceedings{PLDI15p229, author = {John K. Feser and Swarat Chaudhuri and Isil Dillig}, title = {Synthesizing Data Structure Transformations from Input-Output Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {229--239}, doi = {}, year = {2015}, } PLDI '15: "Static Detection of Asymptotic ..." Static Detection of Asymptotic Performance Bugs in Collection Traversals Oswaldo Olivo, Isil Dillig, and Calvin Lin (University of Texas at Austin, USA) This paper identifies and formalizes a prevalent class of asymptotic performance bugs called redundant traversal bugs and presents a novel static analysis for automatically detecting them. We evaluate our technique by implementing it in a tool called CLARITY and applying it to widely-used software packages such as the Google Core Collections Library, the Apache Common Collections, and the Apache Ant build tool. Across 1.6M lines of Java code, CLARITY finds 92 instances of redundant traversal bugs, including 72 that have never been previously reported, with just 5 false positives. To evaluate the performance impact of these bugs, we manually repair these programs and find that for an input size of 50,000, all repaired programs are at least 2.45 faster than their original code. @InProceedings{PLDI15p369, author = {Oswaldo Olivo and Isil Dillig and Calvin Lin}, title = {Static Detection of Asymptotic Performance Bugs in Collection Traversals}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {369--378}, doi = {}, year = {2015}, }
	Ding, Wei	PLDI '15: "Optimizing Off-Chip Accesses ..." Optimizing Off-Chip Accesses in Multicores Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay (Pennsylvania State University, USA; Intel, USA) In a network-on-chip (NoC) based manycore architecture, an off-chip data access (main memory access) needs to travel through the on-chip network, spending considerable amount of time within the chip (in addition to the memory access latency). In addition, it contends with on-chip (cache) accesses as both use the same NoC resources. In this paper, focusing on data-parallel, multithreaded applications, we propose a compiler-based off-chip data access localization strategy, which places data elements in the memory space such that an off-chip access traverses a minimum number of links (hops) to reach the memory controller that handles this access. This brings three main benefits. First, the network latency of off-chip accesses gets reduced; second, the network latency of on-chip accesses gets reduced; and finally, the memory latency of off-chip accesses improves, due to reduced queue latencies. We present an experimental evaluation of our optimization strategy using a set of 13 multithreaded application programs under both private and shared last-level caches. The results collected emphasize the importance of optimizing the off-chip data accesses. @InProceedings{PLDI15p131, author = {Wei Ding and Xulong Tang and Mahmut Kandemir and Yuanrui Zhang and Emre Kultursay}, title = {Optimizing Off-Chip Accesses in Multicores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {131--142}, doi = {}, year = {2015}, }
	Ding, Yufei	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, }
	Donaldson, Alastair F.	PLDI '15: "Asynchronous Programming, ..." Asynchronous Programming, Analysis and Testing with State Machines Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson (Imperial College London, UK; Microsoft Research, India) Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. @InProceedings{PLDI15p154, author = {Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema and Akash Lal and Paul Thomson}, title = {Asynchronous Programming, Analysis and Testing with State Machines}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154--164}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Many-Core Compiler Fuzzing ..." Many-Core Compiler Fuzzing Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson (Imperial College London, UK; University College London, UK) We address the compiler correctness problem for many-core systems through novel applications of fuzz testing to OpenCL compilers. Focusing on two methods from prior work, random differential testing and testing via equivalence modulo inputs (EMI), we present several strategies for random generation of deterministic, communicating OpenCL kernels, and an injection mechanism that allows EMI testing to be applied to kernels that otherwise exhibit little or no dynamically-dead code. We use these methods to conduct a large, controlled testing campaign with respect to 21 OpenCL (device, compiler) configurations, covering a range of CPU, GPU, accelerator, FPGA and emulator implementations. Our study provides independent validation of claims in prior work related to the effectiveness of random differential testing and EMI testing, proposes novel methods for lifting these techniques to the many-core setting and reveals a significant number of OpenCL compiler bugs in commercial implementations. @InProceedings{PLDI15p65, author = {Christopher Lidbury and Andrei Lascu and Nathan Chong and Alastair F. Donaldson}, title = {Many-Core Compiler Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {65--76}, doi = {}, year = {2015}, } aec-badge-pldi
	Dreyer, Derek	PLDI '15: "Verifying Read-Copy-Update ..." Verifying Read-Copy-Update in a Logic for Weak Memory Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis (Carnegie Mellon University, USA; MPI-SWS, Germany) Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. Optimized implementations rely only on the weaker memory orderings provided by modern hardware, avoiding the need for expensive synchronization instructions (such as memory barriers) as much as possible. Using GPS, a recently developed program logic for the C/C++11 memory model, we verify an implementation of RCU for a singly-linked list assuming "release-acquire" semantics. Although release-acquire synchronization is stronger than what is required by real RCU implementations, it is nonetheless significantly weaker than the assumption of sequential consistency made in prior work on RCU verification. Ours is the first formal proof of correctness for an implementation of RCU under a weak memory model. @InProceedings{PLDI15p110, author = {Joseph Tassarotti and Derek Dreyer and Viktor Vafeiadis}, title = {Verifying Read-Copy-Update in a Logic for Weak Memory}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {110--120}, doi = {}, year = {2015}, }
	Ducasse, Stéphane	PLDI '15: "Zero-Overhead Metaprogramming: ..." Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises Stefan Marr, Chris Seaton, and Stéphane Ducasse (INRIA, France; Oracle Labs, USA; University of Manchester, UK) Runtime metaprogramming enables many useful applications and is often a convenient solution to solve problems in a generic way, which makes it widely used in frameworks, middleware, and domain-specific languages. However, powerful metaobject protocols are rarely supported and even common concepts such as reflective method invocation or dynamic proxies are not optimized. Solutions proposed in literature either restrict the metaprogramming capabilities or require application or library developers to apply performance improving techniques. For overhead-free runtime metaprogramming, we demonstrate that dispatch chains, a generalized form of polymorphic inline caches common to self-optimizing interpreters, are a simple optimization at the language-implementation level. Our evaluation with self-optimizing interpreters shows that unrestricted metaobject protocols can be realized for the first time without runtime overhead, and that this optimization is applicable for just-in-time compilation of interpreters based on meta-tracing as well as partial evaluation. In this context, we also demonstrate that optimizing common reflective operations can lead to significant performance improvements for existing applications. @InProceedings{PLDI15p545, author = {Stefan Marr and Chris Seaton and Stéphane Ducasse}, title = {Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {545--554}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Dybvig, R. Kent	PLDI '15: "Profile-Guided Meta-Programming ..." Profile-Guided Meta-Programming William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig (Northeastern University, USA; Cisco Systems, USA) Contemporary compiler systems such as GCC, .NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems---the syntactic extensions systems of Chez Scheme and Racket---and provide several profile-guided meta-programs as usability case studies. @InProceedings{PLDI15p403, author = {William J. Bowman and Swaha Miller and Vincent St-Amour and R. Kent Dybvig}, title = {Profile-Guided Meta-Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {403--412}, doi = {}, year = {2015}, }
	Ellison, Chucky	PLDI '15: "Defining the Undefinedness ..." Defining the Undefinedness of C Chris Hathhorn, Chucky Ellison, and Grigore Roşu (University of Missouri, USA; University of Illinois at Urbana-Champaign, USA) We present a ``negative'' semantics of the C11 language---a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself. @InProceedings{PLDI15p336, author = {Chris Hathhorn and Chucky Ellison and Grigore Roşu}, title = {Defining the Undefinedness of C}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {336--345}, doi = {}, year = {2015}, }
	Emani, Murali Krishna	PLDI '15: "Celebrating Diversity: A Mixture ..." Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments Murali Krishna Emani and Michael O'Boyle (University of Edinburgh, UK) Matching program parallelism to platform parallelism using thread selection is difficult when the environment and available resources dynamically change. Existing compiler or runtime approaches are typically based on a one-size fits all policy. There is little ability to either evaluate or adapt the policy when encountering new external workloads or hardware resources. This paper focuses on selecting the best number of threads for a parallel application in dynamic environments. It develops a new scheme based on a mixture of experts approach. It learns online which, of a number of existing policies, or experts, is best suited for a particular environment without having to try out each policy. It does this by using a novel environment predictor as a proxy for the quality of an expert thread selection policy. Additional expert policies can easily be added and are selected only when appropriate. We evaluate our scheme in environments with varying external workloads and hardware resources.We then consider the case when workloads use affinity scheduling or are themselves adaptive and show that our approach, in all cases, outperforms existing schemes and surprisingly improves workload performance. On average, we improve 1.66x over OpenMP default, 1.34x over an online scheme, 1.25x over an offline policy and 1.2x over a state-of-art analytic model. Determining the right number and type of experts is an open problem and our initial analysis shows that adding more experts improves accuracy and performance. @InProceedings{PLDI15p499, author = {Murali Krishna Emani and Michael O'Boyle}, title = {Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {499--508}, doi = {}, year = {2015}, }
	Emmi, Michael	PLDI '15: "Monitoring Refinement via ..." Monitoring Refinement via Symbolic Reasoning Michael Emmi, Constantin Enea, and Jad Hamza (IMDEA Software Institute, Spain; University of Paris Diderot, France) Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions. @InProceedings{PLDI15p260, author = {Michael Emmi and Constantin Enea and Jad Hamza}, title = {Monitoring Refinement via Symbolic Reasoning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {260--269}, doi = {}, year = {2015}, } aec-badge-pldi
	Enea, Constantin	PLDI '15: "Monitoring Refinement via ..." Monitoring Refinement via Symbolic Reasoning Michael Emmi, Constantin Enea, and Jad Hamza (IMDEA Software Institute, Spain; University of Paris Diderot, France) Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions. @InProceedings{PLDI15p260, author = {Michael Emmi and Constantin Enea and Jad Hamza}, title = {Monitoring Refinement via Symbolic Reasoning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {260--269}, doi = {}, year = {2015}, } aec-badge-pldi
	Engelhardt, Kai	PLDI '15: "Relaxing Safely: Verified ..." Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO Peter Gammie, Antony L. Hosking, and Kai Engelhardt (NICTA, Australia; Purdue University, USA; UNSW, Australia) We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward. @InProceedings{PLDI15p99, author = {Peter Gammie and Antony L. Hosking and Kai Engelhardt}, title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {99--109}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Ernst, Michael D.	PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Faddegon, Maarten	PLDI '15: "Algorithmic Debugging of Real-World ..." Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack Maarten Faddegon and Olaf Chitil (University of Kent, UK) Existing algorithmic debuggers for Haskell require a transformation of all modules in a program, even libraries that the user does not want to debug and which may use language features not supported by the debugger. This is a pity, because a promising approach to debugging is therefore not applicable to many real-world programs. We use the cost centre stack from the Glasgow Haskell Compiler profiling environment together with runtime value observations as provided by the Haskell Object Observation Debugger (HOOD) to collect enough information for algorithmic debugging. Program annotations are in suspected modules only. With this technique algorithmic debugging is applicable to a much larger set of Haskell programs. This demonstrates that for functional languages in general a simple stack trace extension is useful to support tasks such as profiling and debugging. @InProceedings{PLDI15p33, author = {Maarten Faddegon and Olaf Chitil}, title = {Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {33--42}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Feser, John K.	PLDI '15: "Synthesizing Data Structure ..." Synthesizing Data Structure Transformations from Input-Output Examples John K. Feser, Swarat Chaudhuri, and Isil Dillig (Rice University, USA; University of Texas at Austin, USA) We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples. Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs. We have implemented our method in a tool called λ2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of λ2. A highlight is the synthesis of a program believed to be the world's earliest functional pearl. @InProceedings{PLDI15p229, author = {John K. Feser and Swarat Chaudhuri and Isil Dillig}, title = {Synthesizing Data Structure Transformations from Input-Output Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {229--239}, doi = {}, year = {2015}, }
	Foster, Nate	PLDI '15: "Efficient Synthesis of Network ..." Efficient Synthesis of Network Updates Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster (University of Colorado at Boulder, USA; Cornell University, USA) Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes. @InProceedings{PLDI15p196, author = {Jedidiah McClurg and Hossein Hojjat and Pavol Černý and Nate Foster}, title = {Efficient Synthesis of Network Updates}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {196--207}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Gammie, Peter	PLDI '15: "Relaxing Safely: Verified ..." Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO Peter Gammie, Antony L. Hosking, and Kai Engelhardt (NICTA, Australia; Purdue University, USA; UNSW, Australia) We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward. @InProceedings{PLDI15p99, author = {Peter Gammie and Antony L. Hosking and Kai Engelhardt}, title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {99--109}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Garbuzov, Dmitri	PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Golan-Gueta, Guy	PLDI '15: "Composing Concurrency Control ..." Composing Concurrency Control Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv (Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India) Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking. @InProceedings{PLDI15p240, author = {Ofri Ziv and Alex Aiken and Guy Golan-Gueta and G. Ramalingam and Mooly Sagiv}, title = {Composing Concurrency Control}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {240--249}, doi = {}, year = {2015}, } Video
	Gonnord, Laure	PLDI '15: "Synthesis of Ranking Functions ..." Synthesis of Ranking Functions using Extremal Counterexamples Laure Gonnord, David Monniaux, and Gabriel Radanne (Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France) We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow). Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included. Experiments with our tool Termite show marked performance and scalability improvements compared to other systems. @InProceedings{PLDI15p608, author = {Laure Gonnord and David Monniaux and Gabriel Radanne}, title = {Synthesis of Ranking Functions using Extremal Counterexamples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {608--618}, doi = {}, year = {2015}, }
	Gulwani, Sumit	PLDI '15: "FlashRelate: Extracting Relational ..." FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn (University of Massachusetts at Amherst, USA; Microsoft Research, USA) With hundreds of millions of users, spreadsheets are one of the most important end-user applications. Spreadsheets are easy to use and allow users great flexibility in storing data. This flexibility comes at a price: users often treat spreadsheets as a poor man's database, leading to creative solutions for storing high-dimensional data. The trouble arises when users need to answer queries with their data. Data manipulation tools make strong assumptions about data layouts and cannot read these ad-hoc databases. Converting data into the appropriate layout requires programming skills or a major investment in manual reformatting. The effect is that a vast amount of real-world data is "locked-in" to a proliferation of one-off formats. We introduce FlashRelate, a synthesis engine that lets ordinary users extract structured relational data from spreadsheets without programming. Instead, users extract data by supplying examples of output relational tuples. FlashRelate uses these examples to synthesize a program in Flare. Flare is a novel extraction language that extends regular expressions with geometric constructs. An interactive user interface on top of FlashRelate lets end users extract data by point-and-click. We demonstrate that correct Flare programs can be synthesized in seconds from a small set of examples for 43 real-world scenarios. Finally, our case study demonstrates FlashRelate's usefulness addressing the widespread problem of data trapped in corporate and government formats. @InProceedings{PLDI15p218, author = {Daniel W. Barowy and Sumit Gulwani and Ted Hart and Benjamin Zorn}, title = {FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {218--228}, doi = {}, year = {2015}, } aec-badge-pldi
	Hall, Mary	PLDI '15: "Loop and Data Transformations ..." Loop and Data Transformations for Sparse Matrix Code Anand Venkat, Mary Hall, and Michelle Strout (University of Utah, USA; Colorado State University, USA) This paper introduces three new compiler transformations for representing and transforming sparse matrix computations and their data representations. In cooperation with run-time inspection, our compiler derives transformed matrix representations and associated transformed code to implement a variety of representations targeting different architecture platforms. This systematic approach to combining code and data transformations on sparse computations, which extends a polyhedral transformation and code generation framework, permits the compiler to compose these transformations with other transformations to generate code that is on average within 5% and often exceeds manually-tuned, high-performance sparse matrix libraries CUSP and OSKI. Additionally, the compiler-generated inspector codes are on average 1.5 faster than OSKI and perform comparably to CUSP, respectively. @InProceedings{PLDI15p521, author = {Anand Venkat and Mary Hall and Michelle Strout}, title = {Loop and Data Transformations for Sparse Matrix Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {521--532}, doi = {}, year = {2015}, }
	Hamza, Jad	PLDI '15: "Monitoring Refinement via ..." Monitoring Refinement via Symbolic Reasoning Michael Emmi, Constantin Enea, and Jad Hamza (IMDEA Software Institute, Spain; University of Paris Diderot, France) Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations — or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violation-detection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions. @InProceedings{PLDI15p260, author = {Michael Emmi and Constantin Enea and Jad Hamza}, title = {Monitoring Refinement via Symbolic Reasoning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {260--269}, doi = {}, year = {2015}, } aec-badge-pldi
	Hart, Ted	PLDI '15: "FlashRelate: Extracting Relational ..." FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn (University of Massachusetts at Amherst, USA; Microsoft Research, USA) With hundreds of millions of users, spreadsheets are one of the most important end-user applications. Spreadsheets are easy to use and allow users great flexibility in storing data. This flexibility comes at a price: users often treat spreadsheets as a poor man's database, leading to creative solutions for storing high-dimensional data. The trouble arises when users need to answer queries with their data. Data manipulation tools make strong assumptions about data layouts and cannot read these ad-hoc databases. Converting data into the appropriate layout requires programming skills or a major investment in manual reformatting. The effect is that a vast amount of real-world data is "locked-in" to a proliferation of one-off formats. We introduce FlashRelate, a synthesis engine that lets ordinary users extract structured relational data from spreadsheets without programming. Instead, users extract data by supplying examples of output relational tuples. FlashRelate uses these examples to synthesize a program in Flare. Flare is a novel extraction language that extends regular expressions with geometric constructs. An interactive user interface on top of FlashRelate lets end users extract data by point-and-click. We demonstrate that correct Flare programs can be synthesized in seconds from a small set of examples for 43 real-world scenarios. Finally, our case study demonstrates FlashRelate's usefulness addressing the widespread problem of data trapped in corporate and government formats. @InProceedings{PLDI15p218, author = {Daniel W. Barowy and Sumit Gulwani and Ted Hart and Benjamin Zorn}, title = {FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {218--228}, doi = {}, year = {2015}, } aec-badge-pldi
	Hathhorn, Chris	PLDI '15: "Defining the Undefinedness ..." Defining the Undefinedness of C Chris Hathhorn, Chucky Ellison, and Grigore Roşu (University of Missouri, USA; University of Illinois at Urbana-Champaign, USA) We present a ``negative'' semantics of the C11 language---a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself. @InProceedings{PLDI15p336, author = {Chris Hathhorn and Chucky Ellison and Grigore Roşu}, title = {Defining the Undefinedness of C}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {336--345}, doi = {}, year = {2015}, }
	Hoffmann, Jan	PLDI '15: "Compositional Certified Resource ..." Compositional Certified Resource Bounds Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao (Yale University, USA) This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for state-of-the-art techniques: compositionality, user interaction, generation of proof certificates, and scalability. Compositionality is achieved by incorporating the potential method of amortized analysis. It enables the derivation of global whole-program bounds with local derivation rules by naturally tracking size changes of variables in sequenced loops and function calls. The resource consumption of functions is described abstractly and a function call can be analyzed without access to the function body. User interaction is supported with a new mechanism that clearly separates qualitative and quantitative verification. A user can guide the analysis to derive complex non-linear bounds by using auxiliary variables and assertions. The assertions are separately proved using established qualitative techniques such as abstract interpretation or Hoare logic. Proof certificates are automatically generated from the local derivation rules. A soundness proof of the derivation system with respect to a formal cost semantics guarantees the validity of the certificates. Scalability is attained by an efficient reduction of bound inference to a linear optimization problem that can be solved by off-the-shelf LP solvers. The analysis framework is implemented in the publicly-available tool C4B. An experimental evaluation demonstrates the advantages of the new technique with a comparison of C4B with existing tools on challenging micro benchmarks and the analysis of more than 2900 lines of C code from the cBench benchmark suite. @InProceedings{PLDI15p467, author = {Quentin Carbonneaux and Jan Hoffmann and Zhong Shao}, title = {Compositional Certified Resource Bounds}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {467--478}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Hojjat, Hossein	PLDI '15: "Efficient Synthesis of Network ..." Efficient Synthesis of Network Updates Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster (University of Colorado at Boulder, USA; Cornell University, USA) Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes. @InProceedings{PLDI15p196, author = {Jedidiah McClurg and Hossein Hojjat and Pavol Černý and Nate Foster}, title = {Efficient Synthesis of Network Updates}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {196--207}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Hosking, Antony L.	PLDI '15: "Relaxing Safely: Verified ..." Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO Peter Gammie, Antony L. Hosking, and Kai Engelhardt (NICTA, Australia; Purdue University, USA; UNSW, Australia) We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward. @InProceedings{PLDI15p99, author = {Peter Gammie and Antony L. Hosking and Kai Engelhardt}, title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {99--109}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Huang, Jeff	PLDI '15: "Stateless Model Checking Concurrent ..." Stateless Model Checking Concurrent Programs with Maximal Causality Reduction Jeff Huang (Texas A&M University, USA) We present maximal causality reduction (MCR), a new technique for stateless model checking. MCR systematically explores the state-space of concurrent programs with a provably minimal number of executions. Each execution corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent executions. Moreover, MCR is embarrassingly parallel by shifting the runtime exploration cost to offline analysis. We have designed and implemented MCR using a constraint-based approach and compared with iterative context bounding (ICB) and dynamic partial order reduction (DPOR) on both benchmarks and real-world programs. MCR reduces the number of executions explored by ICB and ICB+DPOR by orders of magnitude, and significantly improves the scalability, efficiency, and effectiveness of the state-of-the-art for both state-space exploration and bug finding. In our experiments, MCR has also revealed several new data races and null pointer dereference errors in frequently studied real-world programs. @InProceedings{PLDI15p165, author = {Jeff Huang}, title = {Stateless Model Checking Concurrent Programs with Maximal Causality Reduction}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {165--174}, doi = {}, year = {2015}, } Video Info
	Hur, Chung-Kil	PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Isradisaikul, Chinawat	PLDI '15: "Finding Counterexamples from ..." Finding Counterexamples from Parsing Conflicts Chinawat Isradisaikul and Andrew C. Myers (Cornell University, USA) Writing a parser remains remarkably painful. Automatic parser generators offer a powerful and systematic way to parse complex grammars, but debugging conflicts in grammars can be time-consuming even for experienced language designers. Better tools for diagnosing parsing conflicts will alleviate this difficulty. This paper proposes a practical algorithm that generates compact, helpful counterexamples for LALR grammars. For each parsing conflict in a grammar, a counterexample demonstrating the conflict is constructed. When the grammar in question is ambiguous, the algorithm usually generates a compact counterexample illustrating the ambiguity. This algorithm has been implemented as an extension to the CUP parser generator. The results from applying this implementation to a diverse collection of faulty grammars show that the algorithm is practical, effective, and suitable for inclusion in other LALR parser generators. @InProceedings{PLDI15p555, author = {Chinawat Isradisaikul and Andrew C. Myers}, title = {Finding Counterexamples from Parsing Conflicts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {555--564}, doi = {}, year = {2015}, } Video Info
	Jaffar, Joxan	PLDI '15: "Automatic Induction Proofs ..." Automatic Induction Proofs of Data-Structures in Imperative Programs Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh (National University of Singapore, Singapore) We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we find a sequence of transformations that produces a final formula which is obviously provable by simply matching terms. Our contribution here is the addition of the fundamental principle of induction to this automated process. We first show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained by using the fold/unfold operations. While the adding of induction is an obvious need in general, no automated method has managed to include this in a systematic and general way. The main reason for this is the problem of avoiding circular reasoning. We overcome this with a novel checking condition. In summary, our contribution is a proof method which – beyond U+M – performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. In the practical evaluation part of this paper, we show how the commonly used technique of using unproven lemmas can be avoided, using realistic benchmarks. This not only removes the current burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce a large search space. In the end, our method can automatically reason about a new class of formulas arising from practical program verification. @InProceedings{PLDI15p457, author = {Duc-Hiep Chu and Joxan Jaffar and Minh-Thai Trinh}, title = {Automatic Induction Proofs of Data-Structures in Imperative Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {457--466}, doi = {}, year = {2015}, }
	Jagannathan, Suresh	PLDI '15: "Synthesizing Racy Tests ..." Synthesizing Racy Tests Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan (Indian Institute of Science, India; Purdue University, USA) Subtle concurrency errors in multithreaded libraries that arise because of incorrect or inadequate synchronization are often difficult to pinpoint precisely using only static techniques. On the other hand, the effectiveness of dynamic race detectors is critically dependent on multithreaded test suites whose execution can be used to identify and trigger races. Usually, such multithreaded tests need to invoke a specific combination of methods with objects involved in the invocations being shared appropriately to expose a race. Without a priori knowledge of the race, construction of such tests can be challenging. In this paper, we present a lightweight and scalable technique for synthesizing precisely these kinds of tests. Given a multithreaded library and a sequential test suite, we describe a fully automated analysis that examines sequential execution traces, and produces as its output a concurrent client program that drives shared objects via library method calls to states conducive for triggering a race. Experimental results on a variety of well-tested Java libraries yield 101 synthesized multithreaded tests in less than four minutes. Analyzing the execution of these tests using an off-the-shelf race detector reveals 187 harmful races, including several previously unreported ones. Our implementation, named NARADA, and the results of our experiments are available at http://www.csa.iisc.ernet.in/~sss/tools/narada. @InProceedings{PLDI15p175, author = {Malavika Samak and Murali Krishna Ramanathan and Suresh Jagannathan}, title = {Synthesizing Racy Tests}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {175--185}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Declarative Programming over ..." Declarative Programming over Eventually Consistent Data Stores KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan (University of Cambridge, UK; Purdue University, USA) User-facing online services utilize geo-distributed data stores to minimize latency and tolerate partial failures, with the intention of providing a fast, always-on experience. However, geo-distribution does not come for free; application developers have to contend with weak consistency behaviors, and the lack of abstractions to composably construct high-level replicated data types, necessitating the need for complex application logic and invariably exposing inconsistencies to the user. Some commercial distributed data stores and several academic proposals provide a lattice of consistency levels, with stronger consistency guarantees incurring increased latency and throughput costs. However, correctly assigning the right consistency level for an operation requires subtle reasoning and is often an error-prone task. In this paper, we present QUELEA, a declarative programming model for eventually consistent data stores (ECDS), equipped with a contract language, capable of specifying fine-grained application - level consistency properties. A contract enforcement system analyses contracts, and automatically generates the appropriate consistency protocol for the method protected by the contract. We describe an implementation of QUELEA on top of an off-the-shelf ECDS that provides support for coordination-free transactions. Several benchmarks including two large web applications, illustrate the effectiveness of our approach. @InProceedings{PLDI15p413, author = {KC Sivaramakrishnan and Gowtham Kaki and Suresh Jagannathan}, title = {Declarative Programming over Eventually Consistent Data Stores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {413--424}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Jo, Youngjoon	PLDI '15: "Efficient Execution of Recursive ..." Efficient Execution of Recursive Programs on Commodity Vector Hardware Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni (Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA) The pursuit of computational efficiency has led to the proliferation of throughput-oriented hardware, from GPUs to increasingly wide vector units on commodity processors and accelerators. This hardware is designed to efficiently execute data-parallel computations in a vectorized manner. However, many algorithms are more naturally expressed as divide-and-conquer, recursive, task-parallel computations. In the absence of data parallelism, it seems that such algorithms are not well suited to throughput-oriented architectures. This paper presents a set of novel code transformations that expose the data parallelism latent in recursive, task-parallel programs. These transformations facilitate straightforward vectorization of task-parallel programs on commodity hardware. We also present scheduling policies that maintain high utilization of vector resources while limiting space usage. Across several task-parallel benchmarks, we demonstrate both efficient vector resource utilization and substantial speedup on chips using Intel’s SSE4.2 vector units, as well as accelerators using Intel’s AVX512 units. @InProceedings{PLDI15p509, author = {Bin Ren and Youngjoon Jo and Sriram Krishnamoorthy and Kunal Agrawal and Milind Kulkarni}, title = {Efficient Execution of Recursive Programs on Commodity Vector Hardware}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {509--520}, doi = {}, year = {2015}, } aec-badge-pldi
	Johnson, Andrew	PLDI '15: "Exploring and Enforcing Security ..." Exploring and Enforcing Security Guarantees via Program Dependence Graphs Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong (Harvard University, USA; MIT Lincoln Laboratory, USA) We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities. @InProceedings{PLDI15p291, author = {Andrew Johnson and Lucas Waye and Scott Moore and Stephen Chong}, title = {Exploring and Enforcing Security Guarantees via Program Dependence Graphs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {291--302}, doi = {}, year = {2015}, }
	Kaki, Gowtham	PLDI '15: "Declarative Programming over ..." Declarative Programming over Eventually Consistent Data Stores KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan (University of Cambridge, UK; Purdue University, USA) User-facing online services utilize geo-distributed data stores to minimize latency and tolerate partial failures, with the intention of providing a fast, always-on experience. However, geo-distribution does not come for free; application developers have to contend with weak consistency behaviors, and the lack of abstractions to composably construct high-level replicated data types, necessitating the need for complex application logic and invariably exposing inconsistencies to the user. Some commercial distributed data stores and several academic proposals provide a lattice of consistency levels, with stronger consistency guarantees incurring increased latency and throughput costs. However, correctly assigning the right consistency level for an operation requires subtle reasoning and is often an error-prone task. In this paper, we present QUELEA, a declarative programming model for eventually consistent data stores (ECDS), equipped with a contract language, capable of specifying fine-grained application - level consistency properties. A contract enforcement system analyses contracts, and automatically generates the appropriate consistency protocol for the method protected by the contract. We describe an implementation of QUELEA on top of an off-the-shelf ECDS that provides support for coordination-free transactions. Several benchmarks including two large web applications, illustrate the effectiveness of our approach. @InProceedings{PLDI15p413, author = {KC Sivaramakrishnan and Gowtham Kaki and Suresh Jagannathan}, title = {Declarative Programming over Eventually Consistent Data Stores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {413--424}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Kamil, Shoaib	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Kandemir, Mahmut	PLDI '15: "Optimizing Off-Chip Accesses ..." Optimizing Off-Chip Accesses in Multicores Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay (Pennsylvania State University, USA; Intel, USA) In a network-on-chip (NoC) based manycore architecture, an off-chip data access (main memory access) needs to travel through the on-chip network, spending considerable amount of time within the chip (in addition to the memory access latency). In addition, it contends with on-chip (cache) accesses as both use the same NoC resources. In this paper, focusing on data-parallel, multithreaded applications, we propose a compiler-based off-chip data access localization strategy, which places data elements in the memory space such that an off-chip access traverses a minimum number of links (hops) to reach the memory controller that handles this access. This brings three main benefits. First, the network latency of off-chip accesses gets reduced; second, the network latency of on-chip accesses gets reduced; and finally, the memory latency of off-chip accesses improves, due to reduced queue latencies. We present an experimental evaluation of our optimization strategy using a set of 13 multithreaded application programs under both private and shared last-level caches. The results collected emphasize the importance of optimizing the off-chip data accesses. @InProceedings{PLDI15p131, author = {Wei Ding and Xulong Tang and Mahmut Kandemir and Yuanrui Zhang and Emre Kultursay}, title = {Optimizing Off-Chip Accesses in Multicores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {131--142}, doi = {}, year = {2015}, }
	Kang, Jeehoon	PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Ketema, Jeroen	PLDI '15: "Asynchronous Programming, ..." Asynchronous Programming, Analysis and Testing with State Machines Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson (Imperial College London, UK; Microsoft Research, India) Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. @InProceedings{PLDI15p154, author = {Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema and Akash Lal and Paul Thomson}, title = {Asynchronous Programming, Analysis and Testing with State Machines}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154--164}, doi = {}, year = {2015}, } aec-badge-pldi
	Ko, Yousun	PLDI '15: "LaminarIR: Compile-Time Queues ..." LaminarIR: Compile-Time Queues for Structured Streams Yousun Ko, Bernd Burgstaller, and Bernhard Scholz (Yonsei University, South Korea; University of Sydney, Australia) Stream programming languages employ FIFO (first-in, first-out) semantics to model data channels between producers and consumers. A FIFO data channel stores tokens in a buffer that is accessed indirectly via read- and write-pointers. This indirect token-access decouples a producer’s write-operations from the read-operations of the consumer, thereby making dataflow implicit. For a compiler, indirect token-access obscures data-dependencies, which renders standard optimizations ineffective and impacts stream program performance negatively. In this paper we propose a transformation for structured stream programming languages such as StreamIt that shifts FIFO buffer management from run-time to compile-time and eliminates splitters and joiners, whose task is to distribute and merge streams. To show the effectiveness of our lowering transformation, we have implemented a StreamIt to C compilation framework. We have developed our own intermediate representation (IR) called LaminarIR, which facilitates the transformation. We report on the enabling effect of the LaminarIR on LLVM’s optimizations, which required the conversion of several standard StreamIt benchmarks from static to randomized input, to prevent computation of partial results at compile-time. We conducted our experimental evaluation on the Intel i7-2600K, AMD Opteron 6378, Intel Xeon Phi 3120A and ARM Cortex-A15 platforms. Our LaminarIR reduces data-communication on average by 35.9% and achieves platform-specific speedups between 3.73x and 4.98x over StreamIt. We reduce memory accesses by more than 60% and achieve energy savings of up to 93.6% on the Intel i7-2600K. @InProceedings{PLDI15p121, author = {Yousun Ko and Bernd Burgstaller and Bernhard Scholz}, title = {LaminarIR: Compile-Time Queues for Structured Streams}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {121--130}, doi = {}, year = {2015}, } Info
	Koskinen, Eric	PLDI '15: "The Push/Pull Model of Transactions ..." The Push/Pull Model of Transactions Eric Koskinen and Matthew Parkinson (IBM Research, USA; Microsoft Research, UK) We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton's left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules' criteria. @InProceedings{PLDI15p186, author = {Eric Koskinen and Matthew Parkinson}, title = {The Push/Pull Model of Transactions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {186--195}, doi = {}, year = {2015}, }
	Krishnamoorthy, Sriram	PLDI '15: "Efficient Execution of Recursive ..." Efficient Execution of Recursive Programs on Commodity Vector Hardware Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni (Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA) The pursuit of computational efficiency has led to the proliferation of throughput-oriented hardware, from GPUs to increasingly wide vector units on commodity processors and accelerators. This hardware is designed to efficiently execute data-parallel computations in a vectorized manner. However, many algorithms are more naturally expressed as divide-and-conquer, recursive, task-parallel computations. In the absence of data parallelism, it seems that such algorithms are not well suited to throughput-oriented architectures. This paper presents a set of novel code transformations that expose the data parallelism latent in recursive, task-parallel programs. These transformations facilitate straightforward vectorization of task-parallel programs on commodity hardware. We also present scheduling policies that maintain high utilization of vector resources while limiting space usage. Across several task-parallel benchmarks, we demonstrate both efficient vector resource utilization and substantial speedup on chips using Intel’s SSE4.2 vector units, as well as accelerators using Intel’s AVX512 units. @InProceedings{PLDI15p509, author = {Bin Ren and Youngjoon Jo and Sriram Krishnamoorthy and Kunal Agrawal and Milind Kulkarni}, title = {Efficient Execution of Recursive Programs on Commodity Vector Hardware}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {509--520}, doi = {}, year = {2015}, } aec-badge-pldi
	Kulkarni, Milind	PLDI '15: "Tree Dependence Analysis ..." Tree Dependence Analysis Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni (Purdue University, USA) We develop a new framework for analyzing recursive methods that perform traversals over trees, called tree dependence analysis. This analysis translates dependence analysis techniques for regular programs to the irregular space, identifying the structure of dependences within a recursive method that traverses trees. We develop a dependence test that exploits the dependence structure of such programs, and can prove that several locality- and parallelism- enhancing transformations are legal. In addition, we extend our analysis with a novel path-dependent, conditional analysis to refine the dependence test and prove the legality of transformations for a wider range of algorithms. We then use these analyses to show that several common algorithms that manipulate trees recursively are amenable to several locality- and parallelism-enhancing transformations. This work shows that classical dependence analysis techniques, which have largely been confined to nested loops over array data structures, can be extended and translated to work for complex, recursive programs that operate over pointer-based data structures. @InProceedings{PLDI15p314, author = {Yusheng Weijiang and Shruthi Balakrishna and Jianqiao Liu and Milind Kulkarni}, title = {Tree Dependence Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {314--325}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Efficient Execution of Recursive ..." Efficient Execution of Recursive Programs on Commodity Vector Hardware Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni (Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA) The pursuit of computational efficiency has led to the proliferation of throughput-oriented hardware, from GPUs to increasingly wide vector units on commodity processors and accelerators. This hardware is designed to efficiently execute data-parallel computations in a vectorized manner. However, many algorithms are more naturally expressed as divide-and-conquer, recursive, task-parallel computations. In the absence of data parallelism, it seems that such algorithms are not well suited to throughput-oriented architectures. This paper presents a set of novel code transformations that expose the data parallelism latent in recursive, task-parallel programs. These transformations facilitate straightforward vectorization of task-parallel programs on commodity hardware. We also present scheduling policies that maintain high utilization of vector resources while limiting space usage. Across several task-parallel benchmarks, we demonstrate both efficient vector resource utilization and substantial speedup on chips using Intel’s SSE4.2 vector units, as well as accelerators using Intel’s AVX512 units. @InProceedings{PLDI15p509, author = {Bin Ren and Youngjoon Jo and Sriram Krishnamoorthy and Kunal Agrawal and Milind Kulkarni}, title = {Efficient Execution of Recursive Programs on Commodity Vector Hardware}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {509--520}, doi = {}, year = {2015}, } aec-badge-pldi
	Kultursay, Emre	PLDI '15: "Optimizing Off-Chip Accesses ..." Optimizing Off-Chip Accesses in Multicores Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay (Pennsylvania State University, USA; Intel, USA) In a network-on-chip (NoC) based manycore architecture, an off-chip data access (main memory access) needs to travel through the on-chip network, spending considerable amount of time within the chip (in addition to the memory access latency). In addition, it contends with on-chip (cache) accesses as both use the same NoC resources. In this paper, focusing on data-parallel, multithreaded applications, we propose a compiler-based off-chip data access localization strategy, which places data elements in the memory space such that an off-chip access traverses a minimum number of links (hops) to reach the memory controller that handles this access. This brings three main benefits. First, the network latency of off-chip accesses gets reduced; second, the network latency of on-chip accesses gets reduced; and finally, the memory latency of off-chip accesses improves, due to reduced queue latencies. We present an experimental evaluation of our optimization strategy using a set of 13 multithreaded application programs under both private and shared last-level caches. The results collected emphasize the importance of optimizing the off-chip data accesses. @InProceedings{PLDI15p131, author = {Wei Ding and Xulong Tang and Mahmut Kandemir and Yuanrui Zhang and Emre Kultursay}, title = {Optimizing Off-Chip Accesses in Multicores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {131--142}, doi = {}, year = {2015}, }
	Kusano, Markus	PLDI '15: "Dynamic Partial Order Reduction ..." Dynamic Partial Order Reduction for Relaxed Memory Models Naling Zhang, Markus Kusano, and Chao Wang (Virginia Tech, USA) Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there is a large body of work on mitigating the scheduling nondeterminism during runtime verification, methods for soundly mitigating the store buffering nondeterminism are lacking. We propose a new dynamic partial order reduction (POR) algorithm for verifying concurrent programs under TSO and PSO. Our method relies on modeling both types of nondeterminism in a unified framework, which allows us to extend existing POR techniques to TSO and PSO without overhauling the verification algorithm. In addition to sound POR, we also propose a buffer-bounding method for more aggressively reducing the state space. We have implemented our new methods in a stateless model checking tool and demonstrated their effectiveness on a set of multithreaded C benchmarks. @InProceedings{PLDI15p250, author = {Naling Zhang and Markus Kusano and Chao Wang}, title = {Dynamic Partial Order Reduction for Relaxed Memory Models}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {250--259}, doi = {}, year = {2015}, } Video
	Lahtinen, Eric	PLDI '15: "Automatic Error Elimination ..." Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications Stelios Sidiroglou-Douskos, Eric Lahtinen, Fan Long, and Martin Rinard (Massachusetts Institute of Technology, USA) We present Code Phage (CP), a system for automatically transferring correct code from donor applications into recipient applications that process the same inputs to successfully eliminate errors in the recipient. Experimental results using seven donor applications to eliminate ten errors in seven recipient applications highlight the ability of CP to transfer code across applications to eliminate out of bounds access, integer overflow, and divide by zero errors. Because CP works with binary donors with no need for source code or symbolic information, it supports a wide range of use cases. To the best of our knowledge, CP is the first system to automatically transfer code across multiple applications. @InProceedings{PLDI15p43, author = {Stelios Sidiroglou-Douskos and Eric Lahtinen and Fan Long and Martin Rinard}, title = {Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {43--54}, doi = {}, year = {2015}, }
	Lal, Akash	PLDI '15: "Asynchronous Programming, ..." Asynchronous Programming, Analysis and Testing with State Machines Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson (Imperial College London, UK; Microsoft Research, India) Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. @InProceedings{PLDI15p154, author = {Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema and Akash Lal and Paul Thomson}, title = {Asynchronous Programming, Analysis and Testing with State Machines}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154--164}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "DAG Inlining: A Decision Procedure ..." DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs Akash Lal and Shaz Qadeer (Microsoft Research, India; Microsoft Research, USA) A hierarchical program is one with multiple procedures but no loops or recursion. This paper studies the problem of deciding reachability queries in hierarchical programs where individual statements can be encoded in a decidable logic (say in SMT). This problem is fundamental to verification and most directly applicable to doing bounded reachability in programs, i.e., reachability under a bound on the number of loop iterations and recursive calls. The usual method of deciding reachability in hierarchical programs is to first inline all procedures and then do reachability on the resulting single-procedure program. Such inlining unfolds the call graph of the program to a tree and may lead to an exponential increase in the size of the program. We design and evaluate a method called DAG inlining that unfolds the call graph to a directed acyclic graph (DAG) instead of a tree by sharing the bodies of procedures at certain points during inlining. DAG inlining can produce much more compact representations than tree inlining. Empirically, we show that it leads to significant improvements in the running time of a state-of-the-art verifier. @InProceedings{PLDI15p280, author = {Akash Lal and Shaz Qadeer}, title = {DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {280--290}, doi = {}, year = {2015}, }
	Lascu, Andrei	PLDI '15: "Many-Core Compiler Fuzzing ..." Many-Core Compiler Fuzzing Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson (Imperial College London, UK; University College London, UK) We address the compiler correctness problem for many-core systems through novel applications of fuzz testing to OpenCL compilers. Focusing on two methods from prior work, random differential testing and testing via equivalence modulo inputs (EMI), we present several strategies for random generation of deterministic, communicating OpenCL kernels, and an injection mechanism that allows EMI testing to be applied to kernels that otherwise exhibit little or no dynamically-dead code. We use these methods to conduct a large, controlled testing campaign with respect to 21 OpenCL (device, compiler) configurations, covering a range of CPU, GPU, accelerator, FPGA and emulator implementations. Our study provides independent validation of claims in prior work related to the effectiveness of random differential testing and EMI testing, proposes novel methods for lifting these techniques to the many-core setting and reveals a significant number of OpenCL compiler bugs in commercial implementations. @InProceedings{PLDI15p65, author = {Christopher Lidbury and Andrei Lascu and Nathan Chong and Alastair F. Donaldson}, title = {Many-Core Compiler Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {65--76}, doi = {}, year = {2015}, } aec-badge-pldi
	Le, Ton Chanh	PLDI '15: "Termination and Non-termination ..." Termination and Non-termination Specification Inference Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin (National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China) Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non- termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers. @InProceedings{PLDI15p489, author = {Ton Chanh Le and Shengchao Qin and Wei-Ngan Chin}, title = {Termination and Non-termination Specification Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {489--498}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Lerner, Sorin	PLDI '15: "Interactive Parser Synthesis ..." Interactive Parser Synthesis by Example Alan Leung, John Sarracino, and Sorin Lerner (University of California at San Diego, USA) Despite decades of research on parsing, the construction of parsers remains a painstaking, manual process prone to subtle bugs and pitfalls. We present a programming-by-example framework called Parsify that is able to synthesize a parser from input/output examples. The user does not write a single line of code. To achieve this, Parsify provides: (a) an iterative algorithm for synthesizing and refining a grammar one example at a time, (b) an interface that provides immediate visual feedback in response to changes in the grammar being refined, and (c) a graphical mechanism for specifying example parse trees using only textual selections. We empirically demonstrate the viability of our approach by using Parsify to construct parsers for source code drawn from Verilog, SQL, Apache, and Tiger. @InProceedings{PLDI15p565, author = {Alan Leung and John Sarracino and Sorin Lerner}, title = {Interactive Parser Synthesis by Example}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {565--574}, doi = {}, year = {2015}, } aec-badge-pldi
	Leung, Alan	PLDI '15: "Interactive Parser Synthesis ..." Interactive Parser Synthesis by Example Alan Leung, John Sarracino, and Sorin Lerner (University of California at San Diego, USA) Despite decades of research on parsing, the construction of parsers remains a painstaking, manual process prone to subtle bugs and pitfalls. We present a programming-by-example framework called Parsify that is able to synthesize a parser from input/output examples. The user does not write a single line of code. To achieve this, Parsify provides: (a) an iterative algorithm for synthesizing and refining a grammar one example at a time, (b) an interface that provides immediate visual feedback in response to changes in the grammar being refined, and (c) a graphical mechanism for specifying example parse trees using only textual selections. We empirically demonstrate the viability of our approach by using Parsify to construct parsers for source code drawn from Verilog, SQL, Apache, and Tiger. @InProceedings{PLDI15p565, author = {Alan Leung and John Sarracino and Sorin Lerner}, title = {Interactive Parser Synthesis by Example}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {565--574}, doi = {}, year = {2015}, } aec-badge-pldi
	Lidbury, Christopher	PLDI '15: "Many-Core Compiler Fuzzing ..." Many-Core Compiler Fuzzing Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson (Imperial College London, UK; University College London, UK) We address the compiler correctness problem for many-core systems through novel applications of fuzz testing to OpenCL compilers. Focusing on two methods from prior work, random differential testing and testing via equivalence modulo inputs (EMI), we present several strategies for random generation of deterministic, communicating OpenCL kernels, and an injection mechanism that allows EMI testing to be applied to kernels that otherwise exhibit little or no dynamically-dead code. We use these methods to conduct a large, controlled testing campaign with respect to 21 OpenCL (device, compiler) configurations, covering a range of CPU, GPU, accelerator, FPGA and emulator implementations. Our study provides independent validation of claims in prior work related to the effectiveness of random differential testing and EMI testing, proposes novel methods for lifting these techniques to the many-core setting and reveals a significant number of OpenCL compiler bugs in commercial implementations. @InProceedings{PLDI15p65, author = {Christopher Lidbury and Andrei Lascu and Nathan Chong and Alastair F. Donaldson}, title = {Many-Core Compiler Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {65--76}, doi = {}, year = {2015}, } aec-badge-pldi
	Lin, Calvin	PLDI '15: "Static Detection of Asymptotic ..." Static Detection of Asymptotic Performance Bugs in Collection Traversals Oswaldo Olivo, Isil Dillig, and Calvin Lin (University of Texas at Austin, USA) This paper identifies and formalizes a prevalent class of asymptotic performance bugs called redundant traversal bugs and presents a novel static analysis for automatically detecting them. We evaluate our technique by implementing it in a tool called CLARITY and applying it to widely-used software packages such as the Google Core Collections Library, the Apache Common Collections, and the Apache Ant build tool. Across 1.6M lines of Java code, CLARITY finds 92 instances of redundant traversal bugs, including 72 that have never been previously reported, with just 5 false positives. To evaluate the performance impact of these bugs, we manually repair these programs and find that for an input size of 50,000, all repaired programs are at least 2.45 faster than their original code. @InProceedings{PLDI15p369, author = {Oswaldo Olivo and Isil Dillig and Calvin Lin}, title = {Static Detection of Asymptotic Performance Bugs in Collection Traversals}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {369--378}, doi = {}, year = {2015}, }
	Liskov, Barbara	PLDI '15: "Lightweight, Flexible Object-Oriented ..." Lightweight, Flexible Object-Oriented Generics Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers (Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA) The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report. @InProceedings{PLDI15p436, author = {Yizhou Zhang and Matthew C. Loring and Guido Salvaneschi and Barbara Liskov and Andrew C. Myers}, title = {Lightweight, Flexible Object-Oriented Generics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {436--445}, doi = {}, year = {2015}, } aec-badge-pldi
	Liu, Jianqiao	PLDI '15: "Tree Dependence Analysis ..." Tree Dependence Analysis Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni (Purdue University, USA) We develop a new framework for analyzing recursive methods that perform traversals over trees, called tree dependence analysis. This analysis translates dependence analysis techniques for regular programs to the irregular space, identifying the structure of dependences within a recursive method that traverses trees. We develop a dependence test that exploits the dependence structure of such programs, and can prove that several locality- and parallelism- enhancing transformations are legal. In addition, we extend our analysis with a novel path-dependent, conditional analysis to refine the dependence test and prove the legality of transformations for a wider range of algorithms. We then use these analyses to show that several common algorithms that manipulate trees recursively are amenable to several locality- and parallelism-enhancing transformations. This work shows that classical dependence analysis techniques, which have largely been confined to nested loops over array data structures, can be extended and translated to work for complex, recursive programs that operate over pointer-based data structures. @InProceedings{PLDI15p314, author = {Yusheng Weijiang and Shruthi Balakrishna and Jianqiao Liu and Milind Kulkarni}, title = {Tree Dependence Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {314--325}, doi = {}, year = {2015}, } aec-badge-pldi
	Liu, Peng	PLDI '15: "Light: Replay via Tightly ..." Light: Replay via Tightly Bounded Recording Peng Liu, Xiangyu Zhang, Omer Tripp, and Yunhui Zheng (Purdue University, USA; IBM Research, USA) Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependences is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependences, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them. @InProceedings{PLDI15p55, author = {Peng Liu and Xiangyu Zhang and Omer Tripp and Yunhui Zheng}, title = {Light: Replay via Tightly Bounded Recording}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {55--64}, doi = {}, year = {2015}, }
	Long, Fan	PLDI '15: "Automatic Error Elimination ..." Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications Stelios Sidiroglou-Douskos, Eric Lahtinen, Fan Long, and Martin Rinard (Massachusetts Institute of Technology, USA) We present Code Phage (CP), a system for automatically transferring correct code from donor applications into recipient applications that process the same inputs to successfully eliminate errors in the recipient. Experimental results using seven donor applications to eliminate ten errors in seven recipient applications highlight the ability of CP to transfer code across applications to eliminate out of bounds access, integer overflow, and divide by zero errors. Because CP works with binary donors with no need for source code or symbolic information, it supports a wide range of use cases. To the best of our knowledge, CP is the first system to automatically transfer code across multiple applications. @InProceedings{PLDI15p43, author = {Stelios Sidiroglou-Douskos and Eric Lahtinen and Fan Long and Martin Rinard}, title = {Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {43--54}, doi = {}, year = {2015}, }
	Longfield, Stephen	PLDI '15: "Preventing Glitches and Short ..." Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate (Cornell University, USA) Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors. @InProceedings{PLDI15p270, author = {Stephen Longfield and Brittany Nkounkou and Rajit Manohar and Ross Tate}, title = {Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {270--279}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Lopes, Nuno P.	PLDI '15: "Provably Correct Peephole ..." Provably Correct Peephole Optimizations with Alive Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr (Microsoft Research, UK; Rutgers University, USA; University of Utah, USA) Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong. @InProceedings{PLDI15p22, author = {Nuno P. Lopes and David Menendez and Santosh Nagarakatte and John Regehr}, title = {Provably Correct Peephole Optimizations with Alive}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {22--32}, doi = {}, year = {2015}, } Video
	Loring, Matthew C.	PLDI '15: "Lightweight, Flexible Object-Oriented ..." Lightweight, Flexible Object-Oriented Generics Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers (Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA) The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report. @InProceedings{PLDI15p436, author = {Yizhou Zhang and Matthew C. Loring and Guido Salvaneschi and Barbara Liskov and Andrew C. Myers}, title = {Lightweight, Flexible Object-Oriented Generics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {436--445}, doi = {}, year = {2015}, } aec-badge-pldi
	Lucia, Brandon	PLDI '15: "A Simpler, Safer Programming ..." A Simpler, Safer Programming and Execution Model for Intermittent Systems Brandon Lucia and Benjamin Ransford (Carnegie Mellon University, USA; University of Washington, USA) Energy harvesting enables novel devices and applications without batteries, but intermittent operation under energy harvesting poses new challenges to memory consistency that threaten to leave applications in failed states not reachable in continuous execution. This paper presents analytical models that aid in reasoning about intermittence. Using these, we develop DINO (Death Is Not an Option), a programming and execution model that simplifies programming for intermittent systems and ensures volatile and nonvolatile data consistency despite near-constant interruptions. DINO is the first system to address these consistency problems in the context of intermittent execution. We evaluate DINO on three energy-harvesting hardware platforms running different applications. The applications fail and exhibit error without DINO, but run correctly with DINO’s modest 1.8–2.7× run-time overhead. DINO also dramatically simplifies programming, reducing the set of possible failure- related control transfers by 5–9×. @InProceedings{PLDI15p575, author = {Brandon Lucia and Benjamin Ransford}, title = {A Simpler, Safer Programming and Execution Model for Intermittent Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {575--585}, doi = {}, year = {2015}, } PLDI '15: "Concurrency Debugging with ..." Concurrency Debugging with Differential Schedule Projections Nuno Machado, Brandon Lucia, and Luís Rodrigues (Universidade de Lisboa, Portugal; Carnegie Mellon University, USA) We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% less data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix. @InProceedings{PLDI15p586, author = {Nuno Machado and Brandon Lucia and Luís Rodrigues}, title = {Concurrency Debugging with Differential Schedule Projections}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {586--595}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Machado, Nuno	PLDI '15: "Concurrency Debugging with ..." Concurrency Debugging with Differential Schedule Projections Nuno Machado, Brandon Lucia, and Luís Rodrigues (Universidade de Lisboa, Portugal; Carnegie Mellon University, USA) We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% less data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix. @InProceedings{PLDI15p586, author = {Nuno Machado and Brandon Lucia and Luís Rodrigues}, title = {Concurrency Debugging with Differential Schedule Projections}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {586--595}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Manevich, Roman	PLDI '15: "Synthesizing Parallel Graph ..." Synthesizing Parallel Graph Programs via Automated Planning Dimitrios Prountzos, Roman Manevich, and Keshav Pingali (University of Texas at Austin, USA; Ben-Gurion University of the Negev, Israel) We describe a system that uses automated planning to synthesize correct and efficient parallel graph programs from high-level algorithmic specifications. Automated planning allows us to use constraints to declaratively encode program transformations such as scheduling, implementation selection, and insertion of synchronization. Each plan emitted by the planner satisfies all constraints simultaneously, and corresponds to a composition of these transformations. In this way, we obtain an integrated compilation approach for a very challenging problem domain. We have used this system to synthesize parallel programs for four graph problems: triangle counting, maximal independent set computation, preflow-push maxflow, and connected components. Experiments on a variety of inputs show that the synthesized implementations perform competitively with hand-written, highly-tuned code. @InProceedings{PLDI15p533, author = {Dimitrios Prountzos and Roman Manevich and Keshav Pingali}, title = {Synthesizing Parallel Graph Programs via Automated Planning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {533--544}, doi = {}, year = {2015}, }
	Manohar, Rajit	PLDI '15: "Preventing Glitches and Short ..." Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate (Cornell University, USA) Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors. @InProceedings{PLDI15p270, author = {Stephen Longfield and Brittany Nkounkou and Rajit Manohar and Ross Tate}, title = {Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {270--279}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Mansky, William	PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Marr, Stefan	PLDI '15: "Zero-Overhead Metaprogramming: ..." Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises Stefan Marr, Chris Seaton, and Stéphane Ducasse (INRIA, France; Oracle Labs, USA; University of Manchester, UK) Runtime metaprogramming enables many useful applications and is often a convenient solution to solve problems in a generic way, which makes it widely used in frameworks, middleware, and domain-specific languages. However, powerful metaobject protocols are rarely supported and even common concepts such as reflective method invocation or dynamic proxies are not optimized. Solutions proposed in literature either restrict the metaprogramming capabilities or require application or library developers to apply performance improving techniques. For overhead-free runtime metaprogramming, we demonstrate that dispatch chains, a generalized form of polymorphic inline caches common to self-optimizing interpreters, are a simple optimization at the language-implementation level. Our evaluation with self-optimizing interpreters shows that unrestricted metaobject protocols can be realized for the first time without runtime overhead, and that this optimization is applicable for just-in-time compilation of interpreters based on meta-tracing as well as partial evaluation. In this context, we also demonstrate that optimizing common reflective operations can lead to significant performance improvements for existing applications. @InProceedings{PLDI15p545, author = {Stefan Marr and Chris Seaton and Stéphane Ducasse}, title = {Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {545--554}, doi = {}, year = {2015}, } Info aec-badge-pldi
	McClurg, Jedidiah	PLDI '15: "Efficient Synthesis of Network ..." Efficient Synthesis of Network Updates Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster (University of Colorado at Boulder, USA; Cornell University, USA) Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes. @InProceedings{PLDI15p196, author = {Jedidiah McClurg and Hossein Hojjat and Pavol Černý and Nate Foster}, title = {Efficient Synthesis of Network Updates}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {196--207}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Mehta, Sanyam	PLDI '15: "Improving Compiler Scalability: ..." Improving Compiler Scalability: Optimizing Large Programs at Small Price Sanyam Mehta and Pen-Chung Yew (University of Minnesota, USA) Compiler scalability is a well known problem: reasoning about the application of useful optimizations over large program scopes consumes too much time and memory during compilation. This problem is exacerbated in polyhedral compilers that use powerful yet costly integer programming algorithms to compose loop optimizations. As a result, the benefits that a polyhedral compiler has to offer to programs such as real scientific applications that contain sequences of loop nests, remain impractical for the common users. In this work, we address this scalability problem in polyhedral compilers. We identify three causes of unscalability, each of which stems from large number of statements and dependences in the program scope. We propose a one-shot solution to the problem by reducing the effective number of statements and dependences as seen by the compiler. We achieve this by representing a sequence of statements in a program by a single super-statement. This set of super-statements exposes the minimum sufficient constraints to the Integer Linear Programming (ILP) solver for finding correct optimizations. We implement our approach in the PLuTo polyhedral compiler and find that it condenses the program statements and program dependences by factors of 4.7x and 6.4x, respectively, averaged over 9 hot regions (ranging from 48 to 121 statements) in 5 real applications. As a result, the improvements in time and memory requirement for compilation are 268x and 20x, respectively, over the latest version of the PLuTo compiler. The final compile times are comparable to the Intel compiler while the performance is 1.92x better on average due to the latter’s conservative approach to loop optimization. @InProceedings{PLDI15p143, author = {Sanyam Mehta and Pen-Chung Yew}, title = {Improving Compiler Scalability: Optimizing Large Programs at Small Price}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {143--152}, doi = {}, year = {2015}, }
	Mendis, Charith	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Menendez, David	PLDI '15: "Provably Correct Peephole ..." Provably Correct Peephole Optimizations with Alive Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr (Microsoft Research, UK; Rutgers University, USA; University of Utah, USA) Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong. @InProceedings{PLDI15p22, author = {Nuno P. Lopes and David Menendez and Santosh Nagarakatte and John Regehr}, title = {Provably Correct Peephole Optimizations with Alive}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {22--32}, doi = {}, year = {2015}, } Video
	Miller, Swaha	PLDI '15: "Profile-Guided Meta-Programming ..." Profile-Guided Meta-Programming William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig (Northeastern University, USA; Cisco Systems, USA) Contemporary compiler systems such as GCC, .NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems---the syntactic extensions systems of Chez Scheme and Racket---and provide several profile-guided meta-programs as usability case studies. @InProceedings{PLDI15p403, author = {William J. Bowman and Swaha Miller and Vincent St-Amour and R. Kent Dybvig}, title = {Profile-Guided Meta-Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {403--412}, doi = {}, year = {2015}, }
	Monniaux, David	PLDI '15: "Synthesis of Ranking Functions ..." Synthesis of Ranking Functions using Extremal Counterexamples Laure Gonnord, David Monniaux, and Gabriel Radanne (Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France) We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow). Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included. Experiments with our tool Termite show marked performance and scalability improvements compared to other systems. @InProceedings{PLDI15p608, author = {Laure Gonnord and David Monniaux and Gabriel Radanne}, title = {Synthesis of Ranking Functions using Extremal Counterexamples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {608--618}, doi = {}, year = {2015}, }
	Moore, Scott	PLDI '15: "Exploring and Enforcing Security ..." Exploring and Enforcing Security Guarantees via Program Dependence Graphs Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong (Harvard University, USA; MIT Lincoln Laboratory, USA) We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities. @InProceedings{PLDI15p291, author = {Andrew Johnson and Lucas Waye and Scott Moore and Stephen Chong}, title = {Exploring and Enforcing Security Guarantees via Program Dependence Graphs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {291--302}, doi = {}, year = {2015}, }
	Myers, Andrew C.	PLDI '15: "Diagnosing Type Errors with ..." Diagnosing Type Errors with Class Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones (Cornell University, USA; Microsoft Research, UK) Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC)--including type classes, GADTs, and type families--it is possible to identify the most likely source of the type error, rather than the first source that the inference engine trips over. To determine which are the likely error sources, we apply a simple Bayesian model to a graph representation of the typing constraints; the satisfiability or unsatisfiability of paths within the graph provides evidence for or against possible explanations. While we build on prior work on error diagnosis for simpler type systems, inference in the richer type system of Haskell requires extending the graph with new nodes. The augmentation of the graph creates challenges both for Bayesian reasoning and for ensuring termination. Using a large corpus of Haskell programs, we show that this error localization technique is practical and significantly improves accuracy over the state of the art. @InProceedings{PLDI15p12, author = {Danfeng Zhang and Andrew C. Myers and Dimitrios Vytiniotis and Simon Peyton-Jones}, title = {Diagnosing Type Errors with Class}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {12--21}, doi = {}, year = {2015}, } PLDI '15: "Lightweight, Flexible Object-Oriented ..." Lightweight, Flexible Object-Oriented Generics Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers (Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA) The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report. @InProceedings{PLDI15p436, author = {Yizhou Zhang and Matthew C. Loring and Guido Salvaneschi and Barbara Liskov and Andrew C. Myers}, title = {Lightweight, Flexible Object-Oriented Generics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {436--445}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Finding Counterexamples from ..." Finding Counterexamples from Parsing Conflicts Chinawat Isradisaikul and Andrew C. Myers (Cornell University, USA) Writing a parser remains remarkably painful. Automatic parser generators offer a powerful and systematic way to parse complex grammars, but debugging conflicts in grammars can be time-consuming even for experienced language designers. Better tools for diagnosing parsing conflicts will alleviate this difficulty. This paper proposes a practical algorithm that generates compact, helpful counterexamples for LALR grammars. For each parsing conflict in a grammar, a counterexample demonstrating the conflict is constructed. When the grammar in question is ambiguous, the algorithm usually generates a compact counterexample illustrating the ambiguity. This algorithm has been implemented as an extension to the CUP parser generator. The results from applying this implementation to a diverse collection of faulty grammars show that the algorithm is practical, effective, and suitable for inclusion in other LALR parser generators. @InProceedings{PLDI15p555, author = {Chinawat Isradisaikul and Andrew C. Myers}, title = {Finding Counterexamples from Parsing Conflicts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {555--564}, doi = {}, year = {2015}, } Video Info
	Nagarakatte, Santosh	PLDI '15: "Provably Correct Peephole ..." Provably Correct Peephole Optimizations with Alive Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr (Microsoft Research, UK; Rutgers University, USA; University of Utah, USA) Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong. @InProceedings{PLDI15p22, author = {Nuno P. Lopes and David Menendez and Santosh Nagarakatte and John Regehr}, title = {Provably Correct Peephole Optimizations with Alive}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {22--32}, doi = {}, year = {2015}, } Video
	Nanevski, Aleksandar	PLDI '15: "Mechanized Verification of ..." Mechanized Verification of Fine-Grained Concurrent Programs Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee (IMDEA Software Institute, Spain) Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization. In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded DSL in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures. @InProceedings{PLDI15p77, author = {Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee}, title = {Mechanized Verification of Fine-Grained Concurrent Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {77--87}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Nguyễn, Phúc C.	PLDI '15: "Relatively Complete Counterexamples ..." Relatively Complete Counterexamples for Higher-Order Programs Phúc C. Nguyễn and David Van Horn (University of Maryland, USA) In this paper, we study the problem of generating inputs to a higher-order program causing it to error. We first approach the problem in the setting of PCF, a typed, core functional language and contribute the first relatively complete method for constructing counterexamples for PCF programs. The method is relatively complete with respect to a first-order solver over the base types of PCF. In practice, this means an SMT solver can be used for the effective, automated generation of higher-order counterexamples for a large class of programs. We achieve this result by employing a novel form of symbolic execution for higher-order programs. The remarkable aspect of this symbolic execution is that even though symbolic higher-order inputs and values are considered, the path condition remains a first-order formula. Our handling of symbolic function application enables the reconstruction of higher-order counterexamples from this first-order formula. After establishing our main theoretical results, we sketch how to apply the approach to untyped, higher-order, stateful languages with first-class contracts and show how counterexample generation can be used to detect contract violations in this setting. To validate our approach, we implement a tool generating counterexamples for erroneous modules written in Racket. @InProceedings{PLDI15p446, author = {Phúc C. Nguyễn and David Van Horn}, title = {Relatively Complete Counterexamples for Higher-Order Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {446--456}, doi = {}, year = {2015}, } aec-badge-pldi
	Nkounkou, Brittany	PLDI '15: "Preventing Glitches and Short ..." Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate (Cornell University, USA) Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors. @InProceedings{PLDI15p270, author = {Stephen Longfield and Brittany Nkounkou and Rajit Manohar and Ross Tate}, title = {Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {270--279}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Nori, Aditya V.	PLDI '15: "Efficient Synthesis of Probabilistic ..." Efficient Synthesis of Probabilistic Programs Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy (Microsoft Research, India; IIT Delhi, India) We show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow the programmer to write a skeleton program with ``holes''. Sketches enable the programmer to communicate domain-specific intuition about the structure of the desired program and prune the search space, and (2) we design an efficient Markov Chain Monte Carlo (MCMC) based synthesis algorithm to instantiate the holes in the sketch with program fragments. Our algorithm efficiently synthesizes a probabilistic program that is most consistent with the data. A core difficulty in synthesizing probabilistic programs is computing the likelihood L(P | D) of a candidate program P generating data D. We propose an approximate method to compute likelihoods using mixtures of Gaussian distributions, thereby avoiding expensive computation of integrals. The use of such approximations enables us to speed up evaluation of the likelihood of candidate programs by a factor of 1000, and makes Markov Chain Monte Carlo based search feasible. We have implemented our algorithm in a tool called PSKETCH, and our results are encouraging PSKETCH is able to automatically synthesize 16 non-trivial real-world probabilistic programs. @InProceedings{PLDI15p208, author = {Aditya V. Nori and Sherjil Ozair and Sriram K. Rajamani and Deepak Vijaykeerthy}, title = {Efficient Synthesis of Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {208--217}, doi = {}, year = {2015}, }
	O'Boyle, Michael	PLDI '15: "Celebrating Diversity: A Mixture ..." Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments Murali Krishna Emani and Michael O'Boyle (University of Edinburgh, UK) Matching program parallelism to platform parallelism using thread selection is difficult when the environment and available resources dynamically change. Existing compiler or runtime approaches are typically based on a one-size fits all policy. There is little ability to either evaluate or adapt the policy when encountering new external workloads or hardware resources. This paper focuses on selecting the best number of threads for a parallel application in dynamic environments. It develops a new scheme based on a mixture of experts approach. It learns online which, of a number of existing policies, or experts, is best suited for a particular environment without having to try out each policy. It does this by using a novel environment predictor as a proxy for the quality of an expert thread selection policy. Additional expert policies can easily be added and are selected only when appropriate. We evaluate our scheme in environments with varying external workloads and hardware resources.We then consider the case when workloads use affinity scheduling or are themselves adaptive and show that our approach, in all cases, outperforms existing schemes and surprisingly improves workload performance. On average, we improve 1.66x over OpenMP default, 1.34x over an online scheme, 1.25x over an offline policy and 1.2x over a state-of-art analytic model. Determining the right number and type of experts is an open problem and our initial analysis shows that adding more experts improves accuracy and performance. @InProceedings{PLDI15p499, author = {Murali Krishna Emani and Michael O'Boyle}, title = {Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {499--508}, doi = {}, year = {2015}, }
	Olivo, Oswaldo	PLDI '15: "Static Detection of Asymptotic ..." Static Detection of Asymptotic Performance Bugs in Collection Traversals Oswaldo Olivo, Isil Dillig, and Calvin Lin (University of Texas at Austin, USA) This paper identifies and formalizes a prevalent class of asymptotic performance bugs called redundant traversal bugs and presents a novel static analysis for automatically detecting them. We evaluate our technique by implementing it in a tool called CLARITY and applying it to widely-used software packages such as the Google Core Collections Library, the Apache Common Collections, and the Apache Ant build tool. Across 1.6M lines of Java code, CLARITY finds 92 instances of redundant traversal bugs, including 72 that have never been previously reported, with just 5 false positives. To evaluate the performance impact of these bugs, we manually repair these programs and find that for an input size of 50,000, all repaired programs are at least 2.45 faster than their original code. @InProceedings{PLDI15p369, author = {Oswaldo Olivo and Isil Dillig and Calvin Lin}, title = {Static Detection of Asymptotic Performance Bugs in Collection Traversals}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {369--378}, doi = {}, year = {2015}, }
	O’Reilly, Una-May	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, }
	Osera, Peter-Michael	PLDI '15: "Type-and-Example-Directed ..." Type-and-Example-Directed Program Synthesis Peter-Michael Osera and Steve Zdancewic (University of Pennsylvania, USA) This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs. @InProceedings{PLDI15p619, author = {Peter-Michael Osera and Steve Zdancewic}, title = {Type-and-Example-Directed Program Synthesis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {619--630}, doi = {}, year = {2015}, } aec-badge-pldi
	Ozair, Sherjil	PLDI '15: "Efficient Synthesis of Probabilistic ..." Efficient Synthesis of Probabilistic Programs Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy (Microsoft Research, India; IIT Delhi, India) We show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow the programmer to write a skeleton program with ``holes''. Sketches enable the programmer to communicate domain-specific intuition about the structure of the desired program and prune the search space, and (2) we design an efficient Markov Chain Monte Carlo (MCMC) based synthesis algorithm to instantiate the holes in the sketch with program fragments. Our algorithm efficiently synthesizes a probabilistic program that is most consistent with the data. A core difficulty in synthesizing probabilistic programs is computing the likelihood L(P | D) of a candidate program P generating data D. We propose an approximate method to compute likelihoods using mixtures of Gaussian distributions, thereby avoiding expensive computation of integrals. The use of such approximations enables us to speed up evaluation of the likelihood of candidate programs by a factor of 1000, and makes Markov Chain Monte Carlo based search feasible. We have implemented our algorithm in a tool called PSKETCH, and our results are encouraging PSKETCH is able to automatically synthesize 16 non-trivial real-world probabilistic programs. @InProceedings{PLDI15p208, author = {Aditya V. Nori and Sherjil Ozair and Sriram K. Rajamani and Deepak Vijaykeerthy}, title = {Efficient Synthesis of Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {208--217}, doi = {}, year = {2015}, }
	Panchekha, Pavel	PLDI '15: "Automatically Improving Accuracy ..." Automatically Improving Accuracy for Floating Point Expressions Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock (University of Washington, USA) Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature provides techniques to mitigate rounding error, applying these techniques requires manually rearranging expressions and understanding the finer details of floating point arithmetic. We introduce Herbie, a tool which automatically discovers the rewrites experts perform to improve accuracy. Herbie's heuristic search estimates and localizes rounding error using sampled points (rather than static error analysis), applies a database of rules to generate improvements, takes series expansions, and combines improvements for different input regions. We evaluated Herbie on examples from a classic numerical methods textbook, and found that Herbie was able to improve accuracy on each example, some by up to 60 bits, while imposing a median performance overhead of 40%. Colleagues in machine learning have used Herbie to significantly improve the results of a clustering algorithm, and a mathematical library has accepted two patches generated using Herbie. @InProceedings{PLDI15p1, author = {Pavel Panchekha and Alex Sanchez-Stern and James R. Wilcox and Zachary Tatlock}, title = {Automatically Improving Accuracy for Floating Point Expressions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1--11}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Paris, Sylvain	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Park, Daejun	PLDI '15: "KJS: A Complete Formal Semantics ..." KJS: A Complete Formal Semantics of JavaScript Daejun Park, Andrei Stefănescu, and Grigore Roşu (University of Illinois at Urbana-Champaign, USA) This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability. @InProceedings{PLDI15p346, author = {Daejun Park and Andrei Stefănescu and Grigore Roşu}, title = {KJS: A Complete Formal Semantics of JavaScript}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {346--356}, doi = {}, year = {2015}, } aec-badge-pldi
	Parkinson, Matthew	PLDI '15: "The Push/Pull Model of Transactions ..." The Push/Pull Model of Transactions Eric Koskinen and Matthew Parkinson (IBM Research, USA; Microsoft Research, UK) We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton's left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules' criteria. @InProceedings{PLDI15p186, author = {Eric Koskinen and Matthew Parkinson}, title = {The Push/Pull Model of Transactions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {186--195}, doi = {}, year = {2015}, }
	Peyton-Jones, Simon	PLDI '15: "Diagnosing Type Errors with ..." Diagnosing Type Errors with Class Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones (Cornell University, USA; Microsoft Research, UK) Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC)--including type classes, GADTs, and type families--it is possible to identify the most likely source of the type error, rather than the first source that the inference engine trips over. To determine which are the likely error sources, we apply a simple Bayesian model to a graph representation of the typing constraints; the satisfiability or unsatisfiability of paths within the graph provides evidence for or against possible explanations. While we build on prior work on error diagnosis for simpler type systems, inference in the richer type system of Haskell requires extending the graph with new nodes. The augmentation of the graph creates challenges both for Bayesian reasoning and for ensuring termination. Using a large corpus of Haskell programs, we show that this error localization technique is practical and significantly improves accuracy over the state of the art. @InProceedings{PLDI15p12, author = {Danfeng Zhang and Andrew C. Myers and Dimitrios Vytiniotis and Simon Peyton-Jones}, title = {Diagnosing Type Errors with Class}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {12--21}, doi = {}, year = {2015}, }
	Pingali, Keshav	PLDI '15: "Synthesizing Parallel Graph ..." Synthesizing Parallel Graph Programs via Automated Planning Dimitrios Prountzos, Roman Manevich, and Keshav Pingali (University of Texas at Austin, USA; Ben-Gurion University of the Negev, Israel) We describe a system that uses automated planning to synthesize correct and efficient parallel graph programs from high-level algorithmic specifications. Automated planning allows us to use constraints to declaratively encode program transformations such as scheduling, implementation selection, and insertion of synchronization. Each plan emitted by the planner satisfies all constraints simultaneously, and corresponds to a composition of these transformations. In this way, we obtain an integrated compilation approach for a very challenging problem domain. We have used this system to synthesize parallel programs for four graph problems: triangle counting, maximal independent set computation, preflow-push maxflow, and connected components. Experiments on a variety of inputs show that the synthesized implementations perform competitively with hand-written, highly-tuned code. @InProceedings{PLDI15p533, author = {Dimitrios Prountzos and Roman Manevich and Keshav Pingali}, title = {Synthesizing Parallel Graph Programs via Automated Planning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {533--544}, doi = {}, year = {2015}, }
	Prountzos, Dimitrios	PLDI '15: "Synthesizing Parallel Graph ..." Synthesizing Parallel Graph Programs via Automated Planning Dimitrios Prountzos, Roman Manevich, and Keshav Pingali (University of Texas at Austin, USA; Ben-Gurion University of the Negev, Israel) We describe a system that uses automated planning to synthesize correct and efficient parallel graph programs from high-level algorithmic specifications. Automated planning allows us to use constraints to declaratively encode program transformations such as scheduling, implementation selection, and insertion of synchronization. Each plan emitted by the planner satisfies all constraints simultaneously, and corresponds to a composition of these transformations. In this way, we obtain an integrated compilation approach for a very challenging problem domain. We have used this system to synthesize parallel programs for four graph problems: triangle counting, maximal independent set computation, preflow-push maxflow, and connected components. Experiments on a variety of inputs show that the synthesized implementations perform competitively with hand-written, highly-tuned code. @InProceedings{PLDI15p533, author = {Dimitrios Prountzos and Roman Manevich and Keshav Pingali}, title = {Synthesizing Parallel Graph Programs via Automated Planning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {533--544}, doi = {}, year = {2015}, }
	Püschel, Markus	PLDI '15: "Making Numerical Program Analysis ..." Making Numerical Program Analysis Fast Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Numerical abstract domains are a fundamental component in modern static program analysis and are used in a wide range of scenarios (e.g. computing array bounds, disjointness, etc). However, analysis with these domains can be very expensive, deeply affecting the scalability and practical applicability of the static analysis. Hence, it is critical to ensure that these domains are made highly efficient. In this work, we present a complete approach for optimizing the performance of the Octagon numerical abstract domain, a domain shown to be particularly effective in practice. Our optimization approach is based on two key insights: i) the ability to perform online decomposition of the octagons leading to a massive reduction in operation counts, and ii) leveraging classic performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement and others, for improving the key bottlenecks of the domain. Applying these ideas, we designed new algorithms for the core Octagon operators with better asymptotic runtime than prior work and combined them with the optimization techniques to achieve high actual performance. We implemented our approach in the Octagon operators exported by the popular APRON C library, thus enabling existing static analyzers using APRON to immediately benefit from our work. To demonstrate the performance benefits of our approach, we evaluated our framework on three published static analyzers showing massive speed-ups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speed-ups (up to 18.7x). Based on these results, we believe that our framework can serve as a new basis for static analysis with the Octagon numerical domain. @InProceedings{PLDI15p303, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Making Numerical Program Analysis Fast}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {303--313}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Qadeer, Shaz	PLDI '15: "DAG Inlining: A Decision Procedure ..." DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs Akash Lal and Shaz Qadeer (Microsoft Research, India; Microsoft Research, USA) A hierarchical program is one with multiple procedures but no loops or recursion. This paper studies the problem of deciding reachability queries in hierarchical programs where individual statements can be encoded in a decidable logic (say in SMT). This problem is fundamental to verification and most directly applicable to doing bounded reachability in programs, i.e., reachability under a bound on the number of loop iterations and recursive calls. The usual method of deciding reachability in hierarchical programs is to first inline all procedures and then do reachability on the resulting single-procedure program. Such inlining unfolds the call graph of the program to a tree and may lead to an exponential increase in the size of the program. We design and evaluate a method called DAG inlining that unfolds the call graph to a directed acyclic graph (DAG) instead of a tree by sharing the bodies of procedures at certain points during inlining. DAG inlining can produce much more compact representations than tree inlining. Empirically, we show that it leads to significant improvements in the running time of a state-of-the-art verifier. @InProceedings{PLDI15p280, author = {Akash Lal and Shaz Qadeer}, title = {DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {280--290}, doi = {}, year = {2015}, }
	Qin, Shengchao	PLDI '15: "Termination and Non-termination ..." Termination and Non-termination Specification Inference Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin (National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China) Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non- termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers. @InProceedings{PLDI15p489, author = {Ton Chanh Le and Shengchao Qin and Wei-Ngan Chin}, title = {Termination and Non-termination Specification Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {489--498}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Radanne, Gabriel	PLDI '15: "Synthesis of Ranking Functions ..." Synthesis of Ranking Functions using Extremal Counterexamples Laure Gonnord, David Monniaux, and Gabriel Radanne (Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France) We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow). Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included. Experiments with our tool Termite show marked performance and scalability improvements compared to other systems. @InProceedings{PLDI15p608, author = {Laure Gonnord and David Monniaux and Gabriel Radanne}, title = {Synthesis of Ranking Functions using Extremal Counterexamples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {608--618}, doi = {}, year = {2015}, }
	Ragan-Kelley, Jonathan	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Rajamani, Sriram K.	PLDI '15: "Efficient Synthesis of Probabilistic ..." Efficient Synthesis of Probabilistic Programs Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy (Microsoft Research, India; IIT Delhi, India) We show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow the programmer to write a skeleton program with ``holes''. Sketches enable the programmer to communicate domain-specific intuition about the structure of the desired program and prune the search space, and (2) we design an efficient Markov Chain Monte Carlo (MCMC) based synthesis algorithm to instantiate the holes in the sketch with program fragments. Our algorithm efficiently synthesizes a probabilistic program that is most consistent with the data. A core difficulty in synthesizing probabilistic programs is computing the likelihood L(P | D) of a candidate program P generating data D. We propose an approximate method to compute likelihoods using mixtures of Gaussian distributions, thereby avoiding expensive computation of integrals. The use of such approximations enables us to speed up evaluation of the likelihood of candidate programs by a factor of 1000, and makes Markov Chain Monte Carlo based search feasible. We have implemented our algorithm in a tool called PSKETCH, and our results are encouraging PSKETCH is able to automatically synthesize 16 non-trivial real-world probabilistic programs. @InProceedings{PLDI15p208, author = {Aditya V. Nori and Sherjil Ozair and Sriram K. Rajamani and Deepak Vijaykeerthy}, title = {Efficient Synthesis of Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {208--217}, doi = {}, year = {2015}, }
	Ramalingam, G.	PLDI '15: "Composing Concurrency Control ..." Composing Concurrency Control Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv (Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India) Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking. @InProceedings{PLDI15p240, author = {Ofri Ziv and Alex Aiken and Guy Golan-Gueta and G. Ramalingam and Mooly Sagiv}, title = {Composing Concurrency Control}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {240--249}, doi = {}, year = {2015}, } Video
	Ramanathan, Murali Krishna	PLDI '15: "Synthesizing Racy Tests ..." Synthesizing Racy Tests Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan (Indian Institute of Science, India; Purdue University, USA) Subtle concurrency errors in multithreaded libraries that arise because of incorrect or inadequate synchronization are often difficult to pinpoint precisely using only static techniques. On the other hand, the effectiveness of dynamic race detectors is critically dependent on multithreaded test suites whose execution can be used to identify and trigger races. Usually, such multithreaded tests need to invoke a specific combination of methods with objects involved in the invocations being shared appropriately to expose a race. Without a priori knowledge of the race, construction of such tests can be challenging. In this paper, we present a lightweight and scalable technique for synthesizing precisely these kinds of tests. Given a multithreaded library and a sequential test suite, we describe a fully automated analysis that examines sequential execution traces, and produces as its output a concurrent client program that drives shared objects via library method calls to states conducive for triggering a race. Experimental results on a variety of well-tested Java libraries yield 101 synthesized multithreaded tests in less than four minutes. Analyzing the execution of these tests using an off-the-shelf race detector reveals 187 harmful races, including several previously unreported ones. Our implementation, named NARADA, and the results of our experiments are available at http://www.csa.iisc.ernet.in/~sss/tools/narada. @InProceedings{PLDI15p175, author = {Malavika Samak and Murali Krishna Ramanathan and Suresh Jagannathan}, title = {Synthesizing Racy Tests}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {175--185}, doi = {}, year = {2015}, } aec-badge-pldi
	Ransford, Benjamin	PLDI '15: "A Simpler, Safer Programming ..." A Simpler, Safer Programming and Execution Model for Intermittent Systems Brandon Lucia and Benjamin Ransford (Carnegie Mellon University, USA; University of Washington, USA) Energy harvesting enables novel devices and applications without batteries, but intermittent operation under energy harvesting poses new challenges to memory consistency that threaten to leave applications in failed states not reachable in continuous execution. This paper presents analytical models that aid in reasoning about intermittence. Using these, we develop DINO (Death Is Not an Option), a programming and execution model that simplifies programming for intermittent systems and ensures volatile and nonvolatile data consistency despite near-constant interruptions. DINO is the first system to address these consistency problems in the context of intermittent execution. We evaluate DINO on three energy-harvesting hardware platforms running different applications. The applications fail and exhibit error without DINO, but run correctly with DINO’s modest 1.8–2.7× run-time overhead. DINO also dramatically simplifies programming, reducing the set of possible failure- related control transfers by 5–9×. @InProceedings{PLDI15p575, author = {Brandon Lucia and Benjamin Ransford}, title = {A Simpler, Safer Programming and Execution Model for Intermittent Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {575--585}, doi = {}, year = {2015}, }
	Regehr, John	PLDI '15: "Provably Correct Peephole ..." Provably Correct Peephole Optimizations with Alive Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr (Microsoft Research, UK; Rutgers University, USA; University of Utah, USA) Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong. @InProceedings{PLDI15p22, author = {Nuno P. Lopes and David Menendez and Santosh Nagarakatte and John Regehr}, title = {Provably Correct Peephole Optimizations with Alive}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {22--32}, doi = {}, year = {2015}, } Video
	Ren, Bin	PLDI '15: "Efficient Execution of Recursive ..." Efficient Execution of Recursive Programs on Commodity Vector Hardware Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni (Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA) The pursuit of computational efficiency has led to the proliferation of throughput-oriented hardware, from GPUs to increasingly wide vector units on commodity processors and accelerators. This hardware is designed to efficiently execute data-parallel computations in a vectorized manner. However, many algorithms are more naturally expressed as divide-and-conquer, recursive, task-parallel computations. In the absence of data parallelism, it seems that such algorithms are not well suited to throughput-oriented architectures. This paper presents a set of novel code transformations that expose the data parallelism latent in recursive, task-parallel programs. These transformations facilitate straightforward vectorization of task-parallel programs on commodity hardware. We also present scheduling policies that maintain high utilization of vector resources while limiting space usage. Across several task-parallel benchmarks, we demonstrate both efficient vector resource utilization and substantial speedup on chips using Intel’s SSE4.2 vector units, as well as accelerators using Intel’s AVX512 units. @InProceedings{PLDI15p509, author = {Bin Ren and Youngjoon Jo and Sriram Krishnamoorthy and Kunal Agrawal and Milind Kulkarni}, title = {Efficient Execution of Recursive Programs on Commodity Vector Hardware}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {509--520}, doi = {}, year = {2015}, } aec-badge-pldi
	Reps, Thomas	PLDI '15: "Synthesis of Machine Code ..." Synthesis of Machine Code from Semantics Venkatesh Srinivasan and Thomas Reps (University of Wisconsin-Madison, USA; GrammaTech, USA) In this paper, we present a technique to synthesize machine-code instructions from a semantic specification, given as a Quantifier-Free Bit-Vector (QFBV) logic formula. Our technique uses an instantiation of the Counter-Example Guided Inductive Synthesis (CEGIS) framework, in combination with search-space pruning heuristics to synthesize instruction-sequences. To counter the exponential cost inherent in enumerative synthesis, our technique uses a divide-and-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the sub-formulas. Synthesizers created by our technique could be used to create semantics-based binary rewriting tools such as optimizers, partial evaluators, program obfuscators/de-obfuscators, etc. Our experiments for Intel's IA-32 instruction set show that, in comparison to our baseline algorithm, our search-space pruning heuristics reduce the synthesis time by a factor of 473, and our divide-and-conquer strategy reduces the synthesis time by a further 3 to 5 orders of magnitude. @InProceedings{PLDI15p596, author = {Venkatesh Srinivasan and Thomas Reps}, title = {Synthesis of Machine Code from Semantics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {596--607}, doi = {}, year = {2015}, }
	Rinard, Martin	PLDI '15: "Automatic Error Elimination ..." Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications Stelios Sidiroglou-Douskos, Eric Lahtinen, Fan Long, and Martin Rinard (Massachusetts Institute of Technology, USA) We present Code Phage (CP), a system for automatically transferring correct code from donor applications into recipient applications that process the same inputs to successfully eliminate errors in the recipient. Experimental results using seven donor applications to eliminate ten errors in seven recipient applications highlight the ability of CP to transfer code across applications to eliminate out of bounds access, integer overflow, and divide by zero errors. Because CP works with binary donors with no need for source code or symbolic information, it supports a wide range of use cases. To the best of our knowledge, CP is the first system to automatically transfer code across multiple applications. @InProceedings{PLDI15p43, author = {Stelios Sidiroglou-Douskos and Eric Lahtinen and Fan Long and Martin Rinard}, title = {Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {43--54}, doi = {}, year = {2015}, }
	Rodrigues, Luís	PLDI '15: "Concurrency Debugging with ..." Concurrency Debugging with Differential Schedule Projections Nuno Machado, Brandon Lucia, and Luís Rodrigues (Universidade de Lisboa, Portugal; Carnegie Mellon University, USA) We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% less data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix. @InProceedings{PLDI15p586, author = {Nuno Machado and Brandon Lucia and Luís Rodrigues}, title = {Concurrency Debugging with Differential Schedule Projections}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {586--595}, doi = {}, year = {2015}, } Video aec-badge-pldi
	Roşu, Grigore	PLDI '15: "Defining the Undefinedness ..." Defining the Undefinedness of C Chris Hathhorn, Chucky Ellison, and Grigore Roşu (University of Missouri, USA; University of Illinois at Urbana-Champaign, USA) We present a ``negative'' semantics of the C11 language---a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself. @InProceedings{PLDI15p336, author = {Chris Hathhorn and Chucky Ellison and Grigore Roşu}, title = {Defining the Undefinedness of C}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {336--345}, doi = {}, year = {2015}, } PLDI '15: "KJS: A Complete Formal Semantics ..." KJS: A Complete Formal Semantics of JavaScript Daejun Park, Andrei Stefănescu, and Grigore Roşu (University of Illinois at Urbana-Champaign, USA) This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability. @InProceedings{PLDI15p346, author = {Daejun Park and Andrei Stefănescu and Grigore Roşu}, title = {KJS: A Complete Formal Semantics of JavaScript}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {346--356}, doi = {}, year = {2015}, } aec-badge-pldi
	Sagiv, Mooly	PLDI '15: "Composing Concurrency Control ..." Composing Concurrency Control Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv (Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India) Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking. @InProceedings{PLDI15p240, author = {Ofri Ziv and Alex Aiken and Guy Golan-Gueta and G. Ramalingam and Mooly Sagiv}, title = {Composing Concurrency Control}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {240--249}, doi = {}, year = {2015}, } Video
	Salvaneschi, Guido	PLDI '15: "Lightweight, Flexible Object-Oriented ..." Lightweight, Flexible Object-Oriented Generics Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers (Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA) The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report. @InProceedings{PLDI15p436, author = {Yizhou Zhang and Matthew C. Loring and Guido Salvaneschi and Barbara Liskov and Andrew C. Myers}, title = {Lightweight, Flexible Object-Oriented Generics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {436--445}, doi = {}, year = {2015}, } aec-badge-pldi
	Samak, Malavika	PLDI '15: "Synthesizing Racy Tests ..." Synthesizing Racy Tests Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan (Indian Institute of Science, India; Purdue University, USA) Subtle concurrency errors in multithreaded libraries that arise because of incorrect or inadequate synchronization are often difficult to pinpoint precisely using only static techniques. On the other hand, the effectiveness of dynamic race detectors is critically dependent on multithreaded test suites whose execution can be used to identify and trigger races. Usually, such multithreaded tests need to invoke a specific combination of methods with objects involved in the invocations being shared appropriately to expose a race. Without a priori knowledge of the race, construction of such tests can be challenging. In this paper, we present a lightweight and scalable technique for synthesizing precisely these kinds of tests. Given a multithreaded library and a sequential test suite, we describe a fully automated analysis that examines sequential execution traces, and produces as its output a concurrent client program that drives shared objects via library method calls to states conducive for triggering a race. Experimental results on a variety of well-tested Java libraries yield 101 synthesized multithreaded tests in less than four minutes. Analyzing the execution of these tests using an off-the-shelf race detector reveals 187 harmful races, including several previously unreported ones. Our implementation, named NARADA, and the results of our experiments are available at http://www.csa.iisc.ernet.in/~sss/tools/narada. @InProceedings{PLDI15p175, author = {Malavika Samak and Murali Krishna Ramanathan and Suresh Jagannathan}, title = {Synthesizing Racy Tests}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {175--185}, doi = {}, year = {2015}, } aec-badge-pldi
	Sanchez-Stern, Alex	PLDI '15: "Automatically Improving Accuracy ..." Automatically Improving Accuracy for Floating Point Expressions Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock (University of Washington, USA) Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature provides techniques to mitigate rounding error, applying these techniques requires manually rearranging expressions and understanding the finer details of floating point arithmetic. We introduce Herbie, a tool which automatically discovers the rewrites experts perform to improve accuracy. Herbie's heuristic search estimates and localizes rounding error using sampled points (rather than static error analysis), applies a database of rules to generate improvements, takes series expansions, and combines improvements for different input regions. We evaluated Herbie on examples from a classic numerical methods textbook, and found that Herbie was able to improve accuracy on each example, some by up to 60 bits, while imposing a median performance overhead of 40%. Colleagues in machine learning have used Herbie to significantly improve the results of a clustering algorithm, and a mathematical library has accepted two patches generated using Herbie. @InProceedings{PLDI15p1, author = {Pavel Panchekha and Alex Sanchez-Stern and James R. Wilcox and Zachary Tatlock}, title = {Automatically Improving Accuracy for Floating Point Expressions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1--11}, doi = {}, year = {2015}, } aec-badge-pldi
	Sarracino, John	PLDI '15: "Interactive Parser Synthesis ..." Interactive Parser Synthesis by Example Alan Leung, John Sarracino, and Sorin Lerner (University of California at San Diego, USA) Despite decades of research on parsing, the construction of parsers remains a painstaking, manual process prone to subtle bugs and pitfalls. We present a programming-by-example framework called Parsify that is able to synthesize a parser from input/output examples. The user does not write a single line of code. To achieve this, Parsify provides: (a) an iterative algorithm for synthesizing and refining a grammar one example at a time, (b) an interface that provides immediate visual feedback in response to changes in the grammar being refined, and (c) a graphical mechanism for specifying example parse trees using only textual selections. We empirically demonstrate the viability of our approach by using Parsify to construct parsers for source code drawn from Verilog, SQL, Apache, and Tiger. @InProceedings{PLDI15p565, author = {Alan Leung and John Sarracino and Sorin Lerner}, title = {Interactive Parser Synthesis by Example}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {565--574}, doi = {}, year = {2015}, } aec-badge-pldi
	Scholz, Bernhard	PLDI '15: "LaminarIR: Compile-Time Queues ..." LaminarIR: Compile-Time Queues for Structured Streams Yousun Ko, Bernd Burgstaller, and Bernhard Scholz (Yonsei University, South Korea; University of Sydney, Australia) Stream programming languages employ FIFO (first-in, first-out) semantics to model data channels between producers and consumers. A FIFO data channel stores tokens in a buffer that is accessed indirectly via read- and write-pointers. This indirect token-access decouples a producer’s write-operations from the read-operations of the consumer, thereby making dataflow implicit. For a compiler, indirect token-access obscures data-dependencies, which renders standard optimizations ineffective and impacts stream program performance negatively. In this paper we propose a transformation for structured stream programming languages such as StreamIt that shifts FIFO buffer management from run-time to compile-time and eliminates splitters and joiners, whose task is to distribute and merge streams. To show the effectiveness of our lowering transformation, we have implemented a StreamIt to C compilation framework. We have developed our own intermediate representation (IR) called LaminarIR, which facilitates the transformation. We report on the enabling effect of the LaminarIR on LLVM’s optimizations, which required the conversion of several standard StreamIt benchmarks from static to randomized input, to prevent computation of partial results at compile-time. We conducted our experimental evaluation on the Intel i7-2600K, AMD Opteron 6378, Intel Xeon Phi 3120A and ARM Cortex-A15 platforms. Our LaminarIR reduces data-communication on average by 35.9% and achieves platform-specific speedups between 3.73x and 4.98x over StreamIt. We reduce memory accesses by more than 60% and achieve energy savings of up to 93.6% on the Intel i7-2600K. @InProceedings{PLDI15p121, author = {Yousun Ko and Bernd Burgstaller and Bernhard Scholz}, title = {LaminarIR: Compile-Time Queues for Structured Streams}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {121--130}, doi = {}, year = {2015}, } Info
	Seaton, Chris	PLDI '15: "Zero-Overhead Metaprogramming: ..." Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises Stefan Marr, Chris Seaton, and Stéphane Ducasse (INRIA, France; Oracle Labs, USA; University of Manchester, UK) Runtime metaprogramming enables many useful applications and is often a convenient solution to solve problems in a generic way, which makes it widely used in frameworks, middleware, and domain-specific languages. However, powerful metaobject protocols are rarely supported and even common concepts such as reflective method invocation or dynamic proxies are not optimized. Solutions proposed in literature either restrict the metaprogramming capabilities or require application or library developers to apply performance improving techniques. For overhead-free runtime metaprogramming, we demonstrate that dispatch chains, a generalized form of polymorphic inline caches common to self-optimizing interpreters, are a simple optimization at the language-implementation level. Our evaluation with self-optimizing interpreters shows that unrestricted metaobject protocols can be realized for the first time without runtime overhead, and that this optimization is applicable for just-in-time compilation of interpreters based on meta-tracing as well as partial evaluation. In this context, we also demonstrate that optimizing common reflective operations can lead to significant performance improvements for existing applications. @InProceedings{PLDI15p545, author = {Stefan Marr and Chris Seaton and Stéphane Ducasse}, title = {Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {545--554}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Sergey, Ilya	PLDI '15: "Mechanized Verification of ..." Mechanized Verification of Fine-Grained Concurrent Programs Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee (IMDEA Software Institute, Spain) Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization. In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded DSL in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures. @InProceedings{PLDI15p77, author = {Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee}, title = {Mechanized Verification of Fine-Grained Concurrent Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {77--87}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Shao, Zhong	PLDI '15: "Compositional Certified Resource ..." Compositional Certified Resource Bounds Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao (Yale University, USA) This paper presents a new approach for automatically deriving worst-case resource bounds for C programs. The described technique combines ideas from amortized analysis and abstract interpretation in a unified framework to address four challenges for state-of-the-art techniques: compositionality, user interaction, generation of proof certificates, and scalability. Compositionality is achieved by incorporating the potential method of amortized analysis. It enables the derivation of global whole-program bounds with local derivation rules by naturally tracking size changes of variables in sequenced loops and function calls. The resource consumption of functions is described abstractly and a function call can be analyzed without access to the function body. User interaction is supported with a new mechanism that clearly separates qualitative and quantitative verification. A user can guide the analysis to derive complex non-linear bounds by using auxiliary variables and assertions. The assertions are separately proved using established qualitative techniques such as abstract interpretation or Hoare logic. Proof certificates are automatically generated from the local derivation rules. A soundness proof of the derivation system with respect to a formal cost semantics guarantees the validity of the certificates. Scalability is attained by an efficient reduction of bound inference to a linear optimization problem that can be solved by off-the-shelf LP solvers. The analysis framework is implemented in the publicly-available tool C4B. An experimental evaluation demonstrates the advantages of the new technique with a comparison of C4B with existing tools on challenging micro benchmarks and the analysis of more than 2900 lines of C code from the cBench benchmark suite. @InProceedings{PLDI15p467, author = {Quentin Carbonneaux and Jan Hoffmann and Zhong Shao}, title = {Compositional Certified Resource Bounds}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {467--478}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Sharma, Rahul	PLDI '15: "Verification of Producer-Consumer ..." Verification of Producer-Consumer Synchronization in GPU Programs Rahul Sharma, Michael Bauer, and Alex Aiken (Stanford University, USA; NVIDIA Research, USA) Previous efforts to formally verify code written for GPUs have focused solely on kernels written within the traditional data-parallel GPU programming model. No previous work has considered the higher performance, but more complex, warp-specialized kernels based on producer-consumer named barriers available on current hardware. In this work we present the first formal operational semantics for named barriers and define what it means for a warp-specialized kernel to be correct. We give algorithms for verifying the correctness of warp-specialized kernels and prove that they are both sound and complete for the most common class of warp-specialized programs. We also present WEFT, a verification tool for checking warp-specialized code. Using WEFT, we discover several non-trivial bugs in production warp-specialized kernels. @InProceedings{PLDI15p88, author = {Rahul Sharma and Michael Bauer and Alex Aiken}, title = {Verification of Producer-Consumer Synchronization in GPU Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {88--98}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Shen, Xipeng	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, }
	Sidiroglou-Douskos, Stelios	PLDI '15: "Automatic Error Elimination ..." Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications Stelios Sidiroglou-Douskos, Eric Lahtinen, Fan Long, and Martin Rinard (Massachusetts Institute of Technology, USA) We present Code Phage (CP), a system for automatically transferring correct code from donor applications into recipient applications that process the same inputs to successfully eliminate errors in the recipient. Experimental results using seven donor applications to eliminate ten errors in seven recipient applications highlight the ability of CP to transfer code across applications to eliminate out of bounds access, integer overflow, and divide by zero errors. Because CP works with binary donors with no need for source code or symbolic information, it supports a wide range of use cases. To the best of our knowledge, CP is the first system to automatically transfer code across multiple applications. @InProceedings{PLDI15p43, author = {Stelios Sidiroglou-Douskos and Eric Lahtinen and Fan Long and Martin Rinard}, title = {Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {43--54}, doi = {}, year = {2015}, }
	Siek, Jeremy	PLDI '15: "Blame and Coercion: Together ..." Blame and Coercion: Together Again for the First Time Jeremy Siek, Peter Thiemann, and Philip Wadler (Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK) C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types. We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work. @InProceedings{PLDI15p425, author = {Jeremy Siek and Peter Thiemann and Philip Wadler}, title = {Blame and Coercion: Together Again for the First Time}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {425--435}, doi = {}, year = {2015}, }
	Singh, Gagandeep	PLDI '15: "Making Numerical Program Analysis ..." Making Numerical Program Analysis Fast Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Numerical abstract domains are a fundamental component in modern static program analysis and are used in a wide range of scenarios (e.g. computing array bounds, disjointness, etc). However, analysis with these domains can be very expensive, deeply affecting the scalability and practical applicability of the static analysis. Hence, it is critical to ensure that these domains are made highly efficient. In this work, we present a complete approach for optimizing the performance of the Octagon numerical abstract domain, a domain shown to be particularly effective in practice. Our optimization approach is based on two key insights: i) the ability to perform online decomposition of the octagons leading to a massive reduction in operation counts, and ii) leveraging classic performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement and others, for improving the key bottlenecks of the domain. Applying these ideas, we designed new algorithms for the core Octagon operators with better asymptotic runtime than prior work and combined them with the optimization techniques to achieve high actual performance. We implemented our approach in the Octagon operators exported by the popular APRON C library, thus enabling existing static analyzers using APRON to immediately benefit from our work. To demonstrate the performance benefits of our approach, we evaluated our framework on three published static analyzers showing massive speed-ups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speed-ups (up to 18.7x). Based on these results, we believe that our framework can serve as a new basis for static analysis with the Octagon numerical domain. @InProceedings{PLDI15p303, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Making Numerical Program Analysis Fast}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {303--313}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Sivaramakrishnan, KC	PLDI '15: "Declarative Programming over ..." Declarative Programming over Eventually Consistent Data Stores KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan (University of Cambridge, UK; Purdue University, USA) User-facing online services utilize geo-distributed data stores to minimize latency and tolerate partial failures, with the intention of providing a fast, always-on experience. However, geo-distribution does not come for free; application developers have to contend with weak consistency behaviors, and the lack of abstractions to composably construct high-level replicated data types, necessitating the need for complex application logic and invariably exposing inconsistencies to the user. Some commercial distributed data stores and several academic proposals provide a lattice of consistency levels, with stronger consistency guarantees incurring increased latency and throughput costs. However, correctly assigning the right consistency level for an operation requires subtle reasoning and is often an error-prone task. In this paper, we present QUELEA, a declarative programming model for eventually consistent data stores (ECDS), equipped with a contract language, capable of specifying fine-grained application - level consistency properties. A contract enforcement system analyses contracts, and automatically generates the appropriate consistency protocol for the method protected by the contract. We describe an implementation of QUELEA on top of an off-the-shelf ECDS that provides support for coordination-free transactions. Several benchmarks including two large web applications, illustrate the effectiveness of our approach. @InProceedings{PLDI15p413, author = {KC Sivaramakrishnan and Gowtham Kaki and Suresh Jagannathan}, title = {Declarative Programming over Eventually Consistent Data Stores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {413--424}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Srinivasan, Venkatesh	PLDI '15: "Synthesis of Machine Code ..." Synthesis of Machine Code from Semantics Venkatesh Srinivasan and Thomas Reps (University of Wisconsin-Madison, USA; GrammaTech, USA) In this paper, we present a technique to synthesize machine-code instructions from a semantic specification, given as a Quantifier-Free Bit-Vector (QFBV) logic formula. Our technique uses an instantiation of the Counter-Example Guided Inductive Synthesis (CEGIS) framework, in combination with search-space pruning heuristics to synthesize instruction-sequences. To counter the exponential cost inherent in enumerative synthesis, our technique uses a divide-and-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the sub-formulas. Synthesizers created by our technique could be used to create semantics-based binary rewriting tools such as optimizers, partial evaluators, program obfuscators/de-obfuscators, etc. Our experiments for Intel's IA-32 instruction set show that, in comparison to our baseline algorithm, our search-space pruning heuristics reduce the synthesis time by a factor of 473, and our divide-and-conquer strategy reduces the synthesis time by a further 3 to 5 orders of magnitude. @InProceedings{PLDI15p596, author = {Venkatesh Srinivasan and Thomas Reps}, title = {Synthesis of Machine Code from Semantics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {596--607}, doi = {}, year = {2015}, }
	St-Amour, Vincent	PLDI '15: "Profile-Guided Meta-Programming ..." Profile-Guided Meta-Programming William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig (Northeastern University, USA; Cisco Systems, USA) Contemporary compiler systems such as GCC, .NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems---the syntactic extensions systems of Chez Scheme and Racket---and provide several profile-guided meta-programs as usability case studies. @InProceedings{PLDI15p403, author = {William J. Bowman and Swaha Miller and Vincent St-Amour and R. Kent Dybvig}, title = {Profile-Guided Meta-Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {403--412}, doi = {}, year = {2015}, }
	Stefănescu, Andrei	PLDI '15: "KJS: A Complete Formal Semantics ..." KJS: A Complete Formal Semantics of JavaScript Daejun Park, Andrei Stefănescu, and Grigore Roşu (University of Illinois at Urbana-Champaign, USA) This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability. @InProceedings{PLDI15p346, author = {Daejun Park and Andrei Stefănescu and Grigore Roşu}, title = {KJS: A Complete Formal Semantics of JavaScript}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {346--356}, doi = {}, year = {2015}, } aec-badge-pldi
	Strout, Michelle	PLDI '15: "Loop and Data Transformations ..." Loop and Data Transformations for Sparse Matrix Code Anand Venkat, Mary Hall, and Michelle Strout (University of Utah, USA; Colorado State University, USA) This paper introduces three new compiler transformations for representing and transforming sparse matrix computations and their data representations. In cooperation with run-time inspection, our compiler derives transformed matrix representations and associated transformed code to implement a variety of representations targeting different architecture platforms. This systematic approach to combining code and data transformations on sparse computations, which extends a polyhedral transformation and code generation framework, permits the compiler to compose these transformations with other transformations to generate code that is on average within 5% and often exceeds manually-tuned, high-performance sparse matrix libraries CUSP and OSKI. Additionally, the compiler-generated inspector codes are on average 1.5 faster than OSKI and perform comparably to CUSP, respectively. @InProceedings{PLDI15p521, author = {Anand Venkat and Mary Hall and Michelle Strout}, title = {Loop and Data Transformations for Sparse Matrix Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {521--532}, doi = {}, year = {2015}, }
	Sullivan, Michael J.	PLDI '15: "Peer-to-Peer Affine Commitment ..." Peer-to-Peer Affine Commitment using Bitcoin Karl Crary and Michael J. Sullivan (Carnegie Mellon University, USA) The power of linear and affine logic lies in their ability to model state change. However, in a trustless, peer-to-peer setting, it is difficult to force principals to commit to state changes. We show how to solve the peer-to-peer affine commitment problem using a generalization of Bitcoin in which transactions deal in types rather than numbers. This has applications to proof-carrying authorization and mechanically executable contracts. Importantly, our system can be---and is---implemented on top of the existing Bitcoin network, so there is no need to recruit computing power to a new protocol. @InProceedings{PLDI15p479, author = {Karl Crary and Michael J. Sullivan}, title = {Peer-to-Peer Affine Commitment using Bitcoin}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {479--488}, doi = {}, year = {2015}, }
	Tang, Xulong	PLDI '15: "Optimizing Off-Chip Accesses ..." Optimizing Off-Chip Accesses in Multicores Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay (Pennsylvania State University, USA; Intel, USA) In a network-on-chip (NoC) based manycore architecture, an off-chip data access (main memory access) needs to travel through the on-chip network, spending considerable amount of time within the chip (in addition to the memory access latency). In addition, it contends with on-chip (cache) accesses as both use the same NoC resources. In this paper, focusing on data-parallel, multithreaded applications, we propose a compiler-based off-chip data access localization strategy, which places data elements in the memory space such that an off-chip access traverses a minimum number of links (hops) to reach the memory controller that handles this access. This brings three main benefits. First, the network latency of off-chip accesses gets reduced; second, the network latency of on-chip accesses gets reduced; and finally, the memory latency of off-chip accesses improves, due to reduced queue latencies. We present an experimental evaluation of our optimization strategy using a set of 13 multithreaded application programs under both private and shared last-level caches. The results collected emphasize the importance of optimizing the off-chip data accesses. @InProceedings{PLDI15p131, author = {Wei Ding and Xulong Tang and Mahmut Kandemir and Yuanrui Zhang and Emre Kultursay}, title = {Optimizing Off-Chip Accesses in Multicores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {131--142}, doi = {}, year = {2015}, }
	Tassarotti, Joseph	PLDI '15: "Verifying Read-Copy-Update ..." Verifying Read-Copy-Update in a Logic for Weak Memory Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis (Carnegie Mellon University, USA; MPI-SWS, Germany) Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. Optimized implementations rely only on the weaker memory orderings provided by modern hardware, avoiding the need for expensive synchronization instructions (such as memory barriers) as much as possible. Using GPS, a recently developed program logic for the C/C++11 memory model, we verify an implementation of RCU for a singly-linked list assuming "release-acquire" semantics. Although release-acquire synchronization is stronger than what is required by real RCU implementations, it is nonetheless significantly weaker than the assumption of sequential consistency made in prior work on RCU verification. Ours is the first formal proof of correctness for an implementation of RCU under a weak memory model. @InProceedings{PLDI15p110, author = {Joseph Tassarotti and Derek Dreyer and Viktor Vafeiadis}, title = {Verifying Read-Copy-Update in a Logic for Weak Memory}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {110--120}, doi = {}, year = {2015}, }
	Tate, Ross	PLDI '15: "Preventing Glitches and Short ..." Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate (Cornell University, USA) Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors. @InProceedings{PLDI15p270, author = {Stephen Longfield and Brittany Nkounkou and Rajit Manohar and Ross Tate}, title = {Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {270--279}, doi = {}, year = {2015}, } Info aec-badge-pldi
	Tatlock, Zachary	PLDI '15: "Automatically Improving Accuracy ..." Automatically Improving Accuracy for Floating Point Expressions Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock (University of Washington, USA) Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature provides techniques to mitigate rounding error, applying these techniques requires manually rearranging expressions and understanding the finer details of floating point arithmetic. We introduce Herbie, a tool which automatically discovers the rewrites experts perform to improve accuracy. Herbie's heuristic search estimates and localizes rounding error using sampled points (rather than static error analysis), applies a database of rules to generate improvements, takes series expansions, and combines improvements for different input regions. We evaluated Herbie on examples from a classic numerical methods textbook, and found that Herbie was able to improve accuracy on each example, some by up to 60 bits, while imposing a median performance overhead of 40%. Colleagues in machine learning have used Herbie to significantly improve the results of a clustering algorithm, and a mathematical library has accepted two patches generated using Herbie. @InProceedings{PLDI15p1, author = {Pavel Panchekha and Alex Sanchez-Stern and James R. Wilcox and Zachary Tatlock}, title = {Automatically Improving Accuracy for Floating Point Expressions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1--11}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Thiemann, Peter	PLDI '15: "Blame and Coercion: Together ..." Blame and Coercion: Together Again for the First Time Jeremy Siek, Peter Thiemann, and Philip Wadler (Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK) C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types. We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work. @InProceedings{PLDI15p425, author = {Jeremy Siek and Peter Thiemann and Philip Wadler}, title = {Blame and Coercion: Together Again for the First Time}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {425--435}, doi = {}, year = {2015}, }
	Thomson, Paul	PLDI '15: "Asynchronous Programming, ..." Asynchronous Programming, Analysis and Testing with State Machines Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson (Imperial College London, UK; Microsoft Research, India) Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs. @InProceedings{PLDI15p154, author = {Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema and Akash Lal and Paul Thomson}, title = {Asynchronous Programming, Analysis and Testing with State Machines}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {154--164}, doi = {}, year = {2015}, } aec-badge-pldi
	Trinh, Minh-Thai	PLDI '15: "Automatic Induction Proofs ..." Automatic Induction Proofs of Data-Structures in Imperative Programs Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh (National University of Singapore, Singapore) We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we find a sequence of transformations that produces a final formula which is obviously provable by simply matching terms. Our contribution here is the addition of the fundamental principle of induction to this automated process. We first show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained by using the fold/unfold operations. While the adding of induction is an obvious need in general, no automated method has managed to include this in a systematic and general way. The main reason for this is the problem of avoiding circular reasoning. We overcome this with a novel checking condition. In summary, our contribution is a proof method which – beyond U+M – performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. In the practical evaluation part of this paper, we show how the commonly used technique of using unproven lemmas can be avoided, using realistic benchmarks. This not only removes the current burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce a large search space. In the end, our method can automatically reason about a new class of formulas arising from practical program verification. @InProceedings{PLDI15p457, author = {Duc-Hiep Chu and Joxan Jaffar and Minh-Thai Trinh}, title = {Automatic Induction Proofs of Data-Structures in Imperative Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {457--466}, doi = {}, year = {2015}, }
	Tripp, Omer	PLDI '15: "Light: Replay via Tightly ..." Light: Replay via Tightly Bounded Recording Peng Liu, Xiangyu Zhang, Omer Tripp, and Yunhui Zheng (Purdue University, USA; IBM Research, USA) Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependences is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependences, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them. @InProceedings{PLDI15p55, author = {Peng Liu and Xiangyu Zhang and Omer Tripp and Yunhui Zheng}, title = {Light: Replay via Tightly Bounded Recording}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {55--64}, doi = {}, year = {2015}, }
	Vafeiadis, Viktor	PLDI '15: "Verifying Read-Copy-Update ..." Verifying Read-Copy-Update in a Logic for Weak Memory Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis (Carnegie Mellon University, USA; MPI-SWS, Germany) Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. Optimized implementations rely only on the weaker memory orderings provided by modern hardware, avoiding the need for expensive synchronization instructions (such as memory barriers) as much as possible. Using GPS, a recently developed program logic for the C/C++11 memory model, we verify an implementation of RCU for a singly-linked list assuming "release-acquire" semantics. Although release-acquire synchronization is stronger than what is required by real RCU implementations, it is nonetheless significantly weaker than the assumption of sequential consistency made in prior work on RCU verification. Ours is the first formal proof of correctness for an implementation of RCU under a weak memory model. @InProceedings{PLDI15p110, author = {Joseph Tassarotti and Derek Dreyer and Viktor Vafeiadis}, title = {Verifying Read-Copy-Update in a Logic for Weak Memory}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {110--120}, doi = {}, year = {2015}, } PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Van Horn, David	PLDI '15: "Relatively Complete Counterexamples ..." Relatively Complete Counterexamples for Higher-Order Programs Phúc C. Nguyễn and David Van Horn (University of Maryland, USA) In this paper, we study the problem of generating inputs to a higher-order program causing it to error. We first approach the problem in the setting of PCF, a typed, core functional language and contribute the first relatively complete method for constructing counterexamples for PCF programs. The method is relatively complete with respect to a first-order solver over the base types of PCF. In practice, this means an SMT solver can be used for the effective, automated generation of higher-order counterexamples for a large class of programs. We achieve this result by employing a novel form of symbolic execution for higher-order programs. The remarkable aspect of this symbolic execution is that even though symbolic higher-order inputs and values are considered, the path condition remains a first-order formula. Our handling of symbolic function application enables the reconstruction of higher-order counterexamples from this first-order formula. After establishing our main theoretical results, we sketch how to apply the approach to untyped, higher-order, stateful languages with first-class contracts and show how counterexample generation can be used to detect contract violations in this setting. To validate our approach, we implement a tool generating counterexamples for erroneous modules written in Racket. @InProceedings{PLDI15p446, author = {Phúc C. Nguyễn and David Van Horn}, title = {Relatively Complete Counterexamples for Higher-Order Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {446--456}, doi = {}, year = {2015}, } aec-badge-pldi
	Vechev, Martin	PLDI '15: "Making Numerical Program Analysis ..." Making Numerical Program Analysis Fast Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Numerical abstract domains are a fundamental component in modern static program analysis and are used in a wide range of scenarios (e.g. computing array bounds, disjointness, etc). However, analysis with these domains can be very expensive, deeply affecting the scalability and practical applicability of the static analysis. Hence, it is critical to ensure that these domains are made highly efficient. In this work, we present a complete approach for optimizing the performance of the Octagon numerical abstract domain, a domain shown to be particularly effective in practice. Our optimization approach is based on two key insights: i) the ability to perform online decomposition of the octagons leading to a massive reduction in operation counts, and ii) leveraging classic performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement and others, for improving the key bottlenecks of the domain. Applying these ideas, we designed new algorithms for the core Octagon operators with better asymptotic runtime than prior work and combined them with the optimization techniques to achieve high actual performance. We implemented our approach in the Octagon operators exported by the popular APRON C library, thus enabling existing static analyzers using APRON to immediately benefit from our work. To demonstrate the performance benefits of our approach, we evaluated our framework on three published static analyzers showing massive speed-ups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speed-ups (up to 18.7x). Based on these results, we believe that our framework can serve as a new basis for static analysis with the Octagon numerical domain. @InProceedings{PLDI15p303, author = {Gagandeep Singh and Markus Püschel and Martin Vechev}, title = {Making Numerical Program Analysis Fast}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {303--313}, doi = {}, year = {2015}, } Video Info aec-badge-pldi
	Veeramachaneni, Kalyan	PLDI '15: "Autotuning Algorithmic Choice ..." Autotuning Algorithmic Choice for Input Sensitivity Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe (North Carolina State University, USA; Massachusetts Institute of Technology, USA) A daunting challenge faced by program performance autotuning is input sensitivity, where the best autotuned configuration may vary with different input sets. This paper presents a novel two-level input learning algorithm to tackle the challenge for an important class of autotuning problems, algorithmic autotuning. The new approach uses a two-level input clustering method to automatically refine input grouping, feature selection, and classifier construction. Its design solves a series of open issues that are particularly essential to algorithmic autotuning, including the enormous optimization space, complex influence by deep input features, high cost in feature extraction, and variable accuracy of algorithmic choices. Experimental results show that the new solution yields up to a 3x speedup over using a single configuration for all inputs, and a 34x speedup over a traditional one-level method for addressing input sensitivity in program optimizations. @InProceedings{PLDI15p379, author = {Yufei Ding and Jason Ansel and Kalyan Veeramachaneni and Xipeng Shen and Una-May O’Reilly and Saman Amarasinghe}, title = {Autotuning Algorithmic Choice for Input Sensitivity}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379--390}, doi = {}, year = {2015}, }
	Venkat, Anand	PLDI '15: "Loop and Data Transformations ..." Loop and Data Transformations for Sparse Matrix Code Anand Venkat, Mary Hall, and Michelle Strout (University of Utah, USA; Colorado State University, USA) This paper introduces three new compiler transformations for representing and transforming sparse matrix computations and their data representations. In cooperation with run-time inspection, our compiler derives transformed matrix representations and associated transformed code to implement a variety of representations targeting different architecture platforms. This systematic approach to combining code and data transformations on sparse computations, which extends a polyhedral transformation and code generation framework, permits the compiler to compose these transformations with other transformations to generate code that is on average within 5% and often exceeds manually-tuned, high-performance sparse matrix libraries CUSP and OSKI. Additionally, the compiler-generated inspector codes are on average 1.5 faster than OSKI and perform comparably to CUSP, respectively. @InProceedings{PLDI15p521, author = {Anand Venkat and Mary Hall and Michelle Strout}, title = {Loop and Data Transformations for Sparse Matrix Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {521--532}, doi = {}, year = {2015}, }
	Vijaykeerthy, Deepak	PLDI '15: "Efficient Synthesis of Probabilistic ..." Efficient Synthesis of Probabilistic Programs Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy (Microsoft Research, India; IIT Delhi, India) We show how to automatically synthesize probabilistic programs from real-world datasets. Such a synthesis is feasible due to a combination of two techniques: (1) We borrow the idea of ``sketching'' from synthesis of deterministic programs, and allow the programmer to write a skeleton program with ``holes''. Sketches enable the programmer to communicate domain-specific intuition about the structure of the desired program and prune the search space, and (2) we design an efficient Markov Chain Monte Carlo (MCMC) based synthesis algorithm to instantiate the holes in the sketch with program fragments. Our algorithm efficiently synthesizes a probabilistic program that is most consistent with the data. A core difficulty in synthesizing probabilistic programs is computing the likelihood L(P | D) of a candidate program P generating data D. We propose an approximate method to compute likelihoods using mixtures of Gaussian distributions, thereby avoiding expensive computation of integrals. The use of such approximations enables us to speed up evaluation of the likelihood of candidate programs by a factor of 1000, and makes Markov Chain Monte Carlo based search feasible. We have implemented our algorithm in a tool called PSKETCH, and our results are encouraging PSKETCH is able to automatically synthesize 16 non-trivial real-world probabilistic programs. @InProceedings{PLDI15p208, author = {Aditya V. Nori and Sherjil Ozair and Sriram K. Rajamani and Deepak Vijaykeerthy}, title = {Efficient Synthesis of Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {208--217}, doi = {}, year = {2015}, }
	Vytiniotis, Dimitrios	PLDI '15: "Diagnosing Type Errors with ..." Diagnosing Type Errors with Class Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones (Cornell University, USA; Microsoft Research, UK) Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC)--including type classes, GADTs, and type families--it is possible to identify the most likely source of the type error, rather than the first source that the inference engine trips over. To determine which are the likely error sources, we apply a simple Bayesian model to a graph representation of the typing constraints; the satisfiability or unsatisfiability of paths within the graph provides evidence for or against possible explanations. While we build on prior work on error diagnosis for simpler type systems, inference in the richer type system of Haskell requires extending the graph with new nodes. The augmentation of the graph creates challenges both for Bayesian reasoning and for ensuring termination. Using a large corpus of Haskell programs, we show that this error localization technique is practical and significantly improves accuracy over the state of the art. @InProceedings{PLDI15p12, author = {Danfeng Zhang and Andrew C. Myers and Dimitrios Vytiniotis and Simon Peyton-Jones}, title = {Diagnosing Type Errors with Class}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {12--21}, doi = {}, year = {2015}, }
	Wadler, Philip	PLDI '15: "Blame and Coercion: Together ..." Blame and Coercion: Together Again for the First Time Jeremy Siek, Peter Thiemann, and Philip Wadler (Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK) C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types. We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work. @InProceedings{PLDI15p425, author = {Jeremy Siek and Peter Thiemann and Philip Wadler}, title = {Blame and Coercion: Together Again for the First Time}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {425--435}, doi = {}, year = {2015}, }
	Wang, Chao	PLDI '15: "Dynamic Partial Order Reduction ..." Dynamic Partial Order Reduction for Relaxed Memory Models Naling Zhang, Markus Kusano, and Chao Wang (Virginia Tech, USA) Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there is a large body of work on mitigating the scheduling nondeterminism during runtime verification, methods for soundly mitigating the store buffering nondeterminism are lacking. We propose a new dynamic partial order reduction (POR) algorithm for verifying concurrent programs under TSO and PSO. Our method relies on modeling both types of nondeterminism in a unified framework, which allows us to extend existing POR techniques to TSO and PSO without overhauling the verification algorithm. In addition to sound POR, we also propose a buffer-bounding method for more aggressively reducing the state space. We have implemented our new methods in a stateless model checking tool and demonstrated their effectiveness on a set of multithreaded C benchmarks. @InProceedings{PLDI15p250, author = {Naling Zhang and Markus Kusano and Chao Wang}, title = {Dynamic Partial Order Reduction for Relaxed Memory Models}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {250--259}, doi = {}, year = {2015}, } Video
	Wang, Xi	PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Waye, Lucas	PLDI '15: "Exploring and Enforcing Security ..." Exploring and Enforcing Security Guarantees via Program Dependence Graphs Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong (Harvard University, USA; MIT Lincoln Laboratory, USA) We present PIDGIN, a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. PIDGIN also allows developers to interactively explore the information flows in their applications to develop policies and investigate counter-examples. PIDGIN combines program dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies. PIDGIN is scalable. Generating a PDG for a 330k line Java application takes 90 seconds, and checking a policy on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing. We describe the design and implementation of PIDGIN and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities. @InProceedings{PLDI15p291, author = {Andrew Johnson and Lucas Waye and Scott Moore and Stephen Chong}, title = {Exploring and Enforcing Security Guarantees via Program Dependence Graphs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {291--302}, doi = {}, year = {2015}, }
	Weijiang, Yusheng	PLDI '15: "Tree Dependence Analysis ..." Tree Dependence Analysis Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni (Purdue University, USA) We develop a new framework for analyzing recursive methods that perform traversals over trees, called tree dependence analysis. This analysis translates dependence analysis techniques for regular programs to the irregular space, identifying the structure of dependences within a recursive method that traverses trees. We develop a dependence test that exploits the dependence structure of such programs, and can prove that several locality- and parallelism- enhancing transformations are legal. In addition, we extend our analysis with a novel path-dependent, conditional analysis to refine the dependence test and prove the legality of transformations for a wider range of algorithms. We then use these analyses to show that several common algorithms that manipulate trees recursively are amenable to several locality- and parallelism-enhancing transformations. This work shows that classical dependence analysis techniques, which have largely been confined to nested loops over array data structures, can be extended and translated to work for complex, recursive programs that operate over pointer-based data structures. @InProceedings{PLDI15p314, author = {Yusheng Weijiang and Shruthi Balakrishna and Jianqiao Liu and Milind Kulkarni}, title = {Tree Dependence Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {314--325}, doi = {}, year = {2015}, } aec-badge-pldi
	Wilcox, James R.	PLDI '15: "Automatically Improving Accuracy ..." Automatically Improving Accuracy for Floating Point Expressions Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock (University of Washington, USA) Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature provides techniques to mitigate rounding error, applying these techniques requires manually rearranging expressions and understanding the finer details of floating point arithmetic. We introduce Herbie, a tool which automatically discovers the rewrites experts perform to improve accuracy. Herbie's heuristic search estimates and localizes rounding error using sampled points (rather than static error analysis), applies a database of rules to generate improvements, takes series expansions, and combines improvements for different input regions. We evaluated Herbie on examples from a classic numerical methods textbook, and found that Herbie was able to improve accuracy on each example, some by up to 60 bits, while imposing a median performance overhead of 40%. Colleagues in machine learning have used Herbie to significantly improve the results of a clustering algorithm, and a mathematical library has accepted two patches generated using Herbie. @InProceedings{PLDI15p1, author = {Pavel Panchekha and Alex Sanchez-Stern and James R. Wilcox and Zachary Tatlock}, title = {Automatically Improving Accuracy for Floating Point Expressions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1--11}, doi = {}, year = {2015}, } aec-badge-pldi PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Woos, Doug	PLDI '15: "Verdi: A Framework for Implementing ..." Verdi: A Framework for Implementing and Formally Verifying Distributed Systems James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson (University of Washington, USA) Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi's utility, we present the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents. @InProceedings{PLDI15p357, author = {James R. Wilcox and Doug Woos and Pavel Panchekha and Zachary Tatlock and Xi Wang and Michael D. Ernst and Thomas Anderson}, title = {Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {357--368}, doi = {}, year = {2015}, } aec-badge-pldi
	Wu, Kevin	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Yew, Pen-Chung	PLDI '15: "Improving Compiler Scalability: ..." Improving Compiler Scalability: Optimizing Large Programs at Small Price Sanyam Mehta and Pen-Chung Yew (University of Minnesota, USA) Compiler scalability is a well known problem: reasoning about the application of useful optimizations over large program scopes consumes too much time and memory during compilation. This problem is exacerbated in polyhedral compilers that use powerful yet costly integer programming algorithms to compose loop optimizations. As a result, the benefits that a polyhedral compiler has to offer to programs such as real scientific applications that contain sequences of loop nests, remain impractical for the common users. In this work, we address this scalability problem in polyhedral compilers. We identify three causes of unscalability, each of which stems from large number of statements and dependences in the program scope. We propose a one-shot solution to the problem by reducing the effective number of statements and dependences as seen by the compiler. We achieve this by representing a sequence of statements in a program by a single super-statement. This set of super-statements exposes the minimum sufficient constraints to the Integer Linear Programming (ILP) solver for finding correct optimizations. We implement our approach in the PLuTo polyhedral compiler and find that it condenses the program statements and program dependences by factors of 4.7x and 6.4x, respectively, averaged over 9 hot regions (ranging from 48 to 121 statements) in 5 real applications. As a result, the improvements in time and memory requirement for compilation are 268x and 20x, respectively, over the latest version of the PLuTo compiler. The final compile times are comparable to the Intel compiler while the performance is 1.92x better on average due to the latter’s conservative approach to loop optimization. @InProceedings{PLDI15p143, author = {Sanyam Mehta and Pen-Chung Yew}, title = {Improving Compiler Scalability: Optimizing Large Programs at Small Price}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {143--152}, doi = {}, year = {2015}, }
	Zdancewic, Steve	PLDI '15: "A Formal C Memory Model Supporting ..." A Formal C Memory Model Supporting Integer-Pointer Casts Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis (Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany) The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq. @InProceedings{PLDI15p326, author = {Jeehoon Kang and Chung-Kil Hur and William Mansky and Dmitri Garbuzov and Steve Zdancewic and Viktor Vafeiadis}, title = {A Formal C Memory Model Supporting Integer-Pointer Casts}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {326--335}, doi = {}, year = {2015}, } Video Info aec-badge-pldi PLDI '15: "Type-and-Example-Directed ..." Type-and-Example-Directed Program Synthesis Peter-Michael Osera and Steve Zdancewic (University of Pennsylvania, USA) This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs. @InProceedings{PLDI15p619, author = {Peter-Michael Osera and Steve Zdancewic}, title = {Type-and-Example-Directed Program Synthesis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {619--630}, doi = {}, year = {2015}, } aec-badge-pldi
	Zhang, Danfeng	PLDI '15: "Diagnosing Type Errors with ..." Diagnosing Type Errors with Class Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones (Cornell University, USA; Microsoft Research, UK) Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC)--including type classes, GADTs, and type families--it is possible to identify the most likely source of the type error, rather than the first source that the inference engine trips over. To determine which are the likely error sources, we apply a simple Bayesian model to a graph representation of the typing constraints; the satisfiability or unsatisfiability of paths within the graph provides evidence for or against possible explanations. While we build on prior work on error diagnosis for simpler type systems, inference in the richer type system of Haskell requires extending the graph with new nodes. The augmentation of the graph creates challenges both for Bayesian reasoning and for ensuring termination. Using a large corpus of Haskell programs, we show that this error localization technique is practical and significantly improves accuracy over the state of the art. @InProceedings{PLDI15p12, author = {Danfeng Zhang and Andrew C. Myers and Dimitrios Vytiniotis and Simon Peyton-Jones}, title = {Diagnosing Type Errors with Class}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {12--21}, doi = {}, year = {2015}, }
	Zhang, Naling	PLDI '15: "Dynamic Partial Order Reduction ..." Dynamic Partial Order Reduction for Relaxed Memory Models Naling Zhang, Markus Kusano, and Chao Wang (Virginia Tech, USA) Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there is a large body of work on mitigating the scheduling nondeterminism during runtime verification, methods for soundly mitigating the store buffering nondeterminism are lacking. We propose a new dynamic partial order reduction (POR) algorithm for verifying concurrent programs under TSO and PSO. Our method relies on modeling both types of nondeterminism in a unified framework, which allows us to extend existing POR techniques to TSO and PSO without overhauling the verification algorithm. In addition to sound POR, we also propose a buffer-bounding method for more aggressively reducing the state space. We have implemented our new methods in a stateless model checking tool and demonstrated their effectiveness on a set of multithreaded C benchmarks. @InProceedings{PLDI15p250, author = {Naling Zhang and Markus Kusano and Chao Wang}, title = {Dynamic Partial Order Reduction for Relaxed Memory Models}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {250--259}, doi = {}, year = {2015}, } Video
	Zhang, Xiangyu	PLDI '15: "Light: Replay via Tightly ..." Light: Replay via Tightly Bounded Recording Peng Liu, Xiangyu Zhang, Omer Tripp, and Yunhui Zheng (Purdue University, USA; IBM Research, USA) Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependences is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependences, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them. @InProceedings{PLDI15p55, author = {Peng Liu and Xiangyu Zhang and Omer Tripp and Yunhui Zheng}, title = {Light: Replay via Tightly Bounded Recording}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {55--64}, doi = {}, year = {2015}, }
	Zhang, Yizhou	PLDI '15: "Lightweight, Flexible Object-Oriented ..." Lightweight, Flexible Object-Oriented Generics Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers (Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA) The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints; in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report. @InProceedings{PLDI15p436, author = {Yizhou Zhang and Matthew C. Loring and Guido Salvaneschi and Barbara Liskov and Andrew C. Myers}, title = {Lightweight, Flexible Object-Oriented Generics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {436--445}, doi = {}, year = {2015}, } aec-badge-pldi
	Zhang, Yuanrui	PLDI '15: "Optimizing Off-Chip Accesses ..." Optimizing Off-Chip Accesses in Multicores Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay (Pennsylvania State University, USA; Intel, USA) In a network-on-chip (NoC) based manycore architecture, an off-chip data access (main memory access) needs to travel through the on-chip network, spending considerable amount of time within the chip (in addition to the memory access latency). In addition, it contends with on-chip (cache) accesses as both use the same NoC resources. In this paper, focusing on data-parallel, multithreaded applications, we propose a compiler-based off-chip data access localization strategy, which places data elements in the memory space such that an off-chip access traverses a minimum number of links (hops) to reach the memory controller that handles this access. This brings three main benefits. First, the network latency of off-chip accesses gets reduced; second, the network latency of on-chip accesses gets reduced; and finally, the memory latency of off-chip accesses improves, due to reduced queue latencies. We present an experimental evaluation of our optimization strategy using a set of 13 multithreaded application programs under both private and shared last-level caches. The results collected emphasize the importance of optimizing the off-chip data accesses. @InProceedings{PLDI15p131, author = {Wei Ding and Xulong Tang and Mahmut Kandemir and Yuanrui Zhang and Emre Kultursay}, title = {Optimizing Off-Chip Accesses in Multicores}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {131--142}, doi = {}, year = {2015}, }
	Zhao, Qin	PLDI '15: "Helium: Lifting High-Performance ..." Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe (Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA) Highly optimized programs are prone to bit rot, where performance quickly becomes suboptimal in the face of new hardware and compiler techniques. In this paper we show how to automatically lift performance-critical stencil kernels from a stripped x86 binary and generate the corresponding code in the high-level domain-specific language Halide. Using Halide’s state-of-the-art optimizations targeting current hardware, we show that new optimized versions of these kernels can replace the originals to rejuvenate the application for newer hardware. The original optimized code for kernels in stripped binaries is nearly impossible to analyze statically. Instead, we rely on dynamic traces to regenerate the kernels. We perform buffer structure reconstruction to identify input, intermediate and output buffer shapes. We abstract from a forest of concrete dependency trees which contain absolute memory addresses to symbolic trees suitable for high-level code generation. This is done by canonicalizing trees, clustering them based on structure, inferring higher-dimensional buffer accesses and finally by solving a set of linear equations based on buffer accesses to lift them up to simple, high-level expressions. Helium can handle highly optimized, complex stencil kernels with input-dependent conditionals. We lift seven kernels from Adobe Photoshop giving a 75% performance improvement, four kernels from IrfanView, leading to 4.97× performance, and one stencil from the miniGMG multigrid benchmark netting a 4.25× improvement in performance. We manually rejuvenated Photoshop by replacing eleven of Photoshop’s filters with our lifted implementations, giving 1.12× speedup without affecting the user experience. @InProceedings{PLDI15p391, author = {Charith Mendis and Jeffrey Bosboom and Kevin Wu and Shoaib Kamil and Jonathan Ragan-Kelley and Sylvain Paris and Qin Zhao and Saman Amarasinghe}, title = {Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {391--402}, doi = {}, year = {2015}, } Info
	Zheng, Yunhui	PLDI '15: "Light: Replay via Tightly ..." Light: Replay via Tightly Bounded Recording Peng Liu, Xiangyu Zhang, Omer Tripp, and Yunhui Zheng (Purdue University, USA; IBM Research, USA) Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependences is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependences, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them. @InProceedings{PLDI15p55, author = {Peng Liu and Xiangyu Zhang and Omer Tripp and Yunhui Zheng}, title = {Light: Replay via Tightly Bounded Recording}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {55--64}, doi = {}, year = {2015}, }
	Ziv, Ofri	PLDI '15: "Composing Concurrency Control ..." Composing Concurrency Control Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv (Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India) Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, deadlock-safety, and opacity) as well as stronger versions of these properties that enable composition. We show how to compose protocols satisfying these properties so that the resulting combined protocol also satisfies these properties. Our approach generalizes well-known protocols (such as two-phase-locking and two-phase-commit) and leads to new protocols. We apply this theory to show how we can safely compose optimistic and pessimistic concurrency control. For example, we show how we can execute a transaction that accesses two objects, one controlled by an STM and another by locking. @InProceedings{PLDI15p240, author = {Ofri Ziv and Alex Aiken and Guy Golan-Gueta and G. Ramalingam and Mooly Sagiv}, title = {Composing Concurrency Control}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {240--249}, doi = {}, year = {2015}, } Video
	Zorn, Benjamin	PLDI '15: "FlashRelate: Extracting Relational ..." FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn (University of Massachusetts at Amherst, USA; Microsoft Research, USA) With hundreds of millions of users, spreadsheets are one of the most important end-user applications. Spreadsheets are easy to use and allow users great flexibility in storing data. This flexibility comes at a price: users often treat spreadsheets as a poor man's database, leading to creative solutions for storing high-dimensional data. The trouble arises when users need to answer queries with their data. Data manipulation tools make strong assumptions about data layouts and cannot read these ad-hoc databases. Converting data into the appropriate layout requires programming skills or a major investment in manual reformatting. The effect is that a vast amount of real-world data is "locked-in" to a proliferation of one-off formats. We introduce FlashRelate, a synthesis engine that lets ordinary users extract structured relational data from spreadsheets without programming. Instead, users extract data by supplying examples of output relational tuples. FlashRelate uses these examples to synthesize a program in Flare. Flare is a novel extraction language that extends regular expressions with geometric constructs. An interactive user interface on top of FlashRelate lets end users extract data by point-and-click. We demonstrate that correct Flare programs can be synthesized in seconds from a small set of examples for 43 real-world scenarios. Finally, our case study demonstrates FlashRelate's usefulness addressing the widespread problem of data trapped in corporate and government formats. @InProceedings{PLDI15p218, author = {Daniel W. Barowy and Sumit Gulwani and Ted Hart and Benjamin Zorn}, title = {FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {218--228}, doi = {}, year = {2015}, } aec-badge-pldi

200 authors

proc time: 1.05