PLDI 2020
41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2020)
Powered by
Conference Publishing Consulting

41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2020), June 15–20, 2020, London, UK

PLDI 2020 – Preliminary Table of Contents

Contents - Abstracts - Authors

Frontmatter

Title Page


Message from the Chairs


Committees


Sponsors


Papers

SympleGraph: Distributed Graph Processing with Precise Loop-Carried Dependency Guarantee
Youwei Zhuo, Jingji Chen, Qinyi Luo, Yanzhi Wang, Hailong Yang, Depei Qian, and Xuehai Qian
(University of Southern California, USA; Northeastern University, USA; Beihang University, China)


Article Search
OOElala: Order-of-Evaluation Based Alias Analysis for Compiler Optimization
Ankush Phulia, Vaibhav Bhagee, and Sorav Bansal
(IIT Delhi, India)


Article Search
Automatic Generation of Efficient Sparse Tensor Format Conversion Routines
Stephen Chou, Fredrik Kjolstad, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; Stanford University, USA)


Article Search
Scalable Validation of Binary Lifters
Sandeep Dasgupta, Sushant Dinesh, Vikram S. Adve, Christopher W. Fletcher, and Deepan Venkatesh
(University of Illinois at Urbana-Champaign, USA)


Article Search
The Essence of Bluespec: A Core Language for Rule-Based Hardware Design
Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Xxx Arvind
(Massachusetts Institute of Technology, USA)


Article Search
Decidable Verification under a Causally Consistent Shared Memory
Ori Lahav and Udi Boker
(Tel Aviv University, Israel; IDC Herzliya, Israel)


Article Search
Data-Driven Inference of Representation Invariants
Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker
(Princeton University, USA; University of California at Los Angeles, USA)
A representation invariant is a property that holds of all values of abstract type produced by a module. Representation invariants play important roles in software engineering and program verification. In this paper, we develop a counterexample-driven algorithm for inferring a representation invariant that is sufficient to imply a desired specification for a module. The key novelty is a type-directed notion of visible inductiveness, which ensures that the algorithm makes progress toward its goal as it alternates between weakening and strengthening candidate invariants. The algorithm is parameterized by an example-based synthesis engine and a verifier, and we prove that it is sound and complete for first-order modules over finite types, assuming that the synthesizer and verifier are as well. We implement these ideas in a tool called Hanoi, which synthesizes representation invariants for recursive data types. Hanoi not only handles invariants for first-order code, but higher-order code as well. In its back end, Hanoi uses an enumerative synthesizer called Myth and an enumerative testing tool as a verifier. Because Hanoi uses testing for verification, it is not sound, though our empirical evaluation shows that it is successful on the benchmarks we investigated.

Preprint
Towards a Verified Range Analysis for JavaScript JITs
Fraser Brown, John Renner, Andres Noetzli, Sorin Lerner, Hovav Shacham, and Deian Stefan
(Stanford University, USA; University of California at San Diego, USA; University of Texas at Austin, USA)


Article Search
Polynomial Invariant Generation for Non-deterministic Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady
(IST Austria, Austria; Shanghai Jiao Tong University, China; Ferdowsi University of Mashhad, Iran)


Article Search
Constant-Time Foundations for the New Spectre Era
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe
(University of California at San Diego, USA; Inria, France; MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain)


Article Search
Armada: Low-Effort Verification of High-Performance Concurrent Programs
Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao
(Microsoft Research, USA; University of Michigan, USA; Yale University, USA; Carnegie Mellon University, USA; Calibra, USA; Certora, USA)


Article Search
Binary Rewriting without Control Flow Recovery
Gregory J. Duck, Xiang Gao, and Abhik Roychoudhury
(National University of Singapore, Singapore)


Article Search
Repairing and Mechanising the JavaScript Relaxed Memory Model
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, and Shu-yu Guo
(University of Cambridge, UK; National Research University Higher School of Economics, Russia; MPI-SWS, Germany; ENS Rennes, France; Bloomberg, USA)


Article Search
Predictable Accelerator Design with Time-Sensitive Affine Types
Rachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li, Theodore Bauer, Yuwei Ye, Apurva Koti, Adrian Sampson, and Zhiru Zhang
(Cornell University, USA)


Article Search
Proving Data-Poisoning Robustness in Decision Trees
Samuel Drews, Aws Albarghouthi, and Loris D'Antoni
(University of Wisconsin-Madison, USA)


Article Search
Detecting Network Load Violations for Distributed Control Planes
Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, and Aditya Akella
(University of Wisconsin-Madison, USA; Google, USA)


Article Search
Improving Program Locality in the GC using Hotness
Albert Mingkun Yang, Erik Österlund, and Tobias Wrigstad
(Uppsala University, Sweden; Oracle, Sweden)
The hierarchical memory system with increasingly small and increasingly fast memory closer to the CPU has for long been at the heart of hiding, or mitigating the performance gap between memories and processors. To utilise this hardware, programs must be written to exhibit good object locality. In languages like C/C++, programmers can carefully plan how objects should be laid out (albeit time consuming and error-prone); for managed languages, especially ones with moving garbage collectors, a manually created optimal layout may be destroyed in the process of object relocation. For managed languages that present an abstract view of memory, the solution lies in making the garbage collector aware of object locality, and strive to achieve and maintain good locality, even in the face of multi-phased programs that exhibit different behaviour across different phases.
This paper presents a GC design that dynamically reorganises objects in the order mutators access them, and additionally strives to separate frequently and infrequently used objects in memory. This improves locality and the efficiency of hardware prefetching. Identifying frequently used objects is done at run-time, with small overhead. HCSGC also offers tunability, for shifting relocation work towards mutators, or for more or less aggressive object relocation.
The ideas are evaluated in the context of the ZGC collector on OpenJDK and yields performance improvements of 5% (tradebeans), 9% (h2) and an impressive 25–45% (JGraphT), all with 95% confidence. For SPECjbb, results are inconclusive due to a fluctuating baseline.

Article Search
A Marriage of Pointer- and Epoch-Based Reclamation
Jeehoon Kang and Jaehwang Jung
(KAIST, South Korea)


Article Search
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
Qinheping Hu, John Cyphert, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). We formulate the problem of proving that a SyGuS problem is unrealizable over a finite set of examples as one of solving a set of equations: the solution yields an overapproximation of the set of possible outputs that any term in the search space can produce on the given examples. If none of the possible outputs agrees with all of the examples, our technique has proven that the given SyGuS problem is unrealizable. We then present an algorithm for exactly solving the set of equations that result from SyGuS problems over linear integer arithmetic (LIA) and LIA with conditionals (CLIA), thereby showing that LIA and CLIA SyGuS problems over finitely many examples are decidable. We implement the proposed technique and algorithms in a tool called Nay. Nay can prove unrealizability for 70/132 existing SyGuS benchmarks, with running times comparable to those of the state-of-the-art tool Nope. Moreover, Nay can solve 11 benchmarks that Nope cannot solve.

Article Search
Inductive Sequentialization of Asynchronous Programs
Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer
(IST Austria, Austria; IRIF, France; University of Paris, France; CNRS, France; Calibra, USA)


Article Search
Compiler and Runtime Support for Continuation Marks
Matthew Flatt and R. Kent Dybvig
(University of Utah, USA; Cisco Systems, USA)
Continuation marks enable dynamic binding and context inspection in a language with proper handling of tail calls and first-class, multi-prompt, delimited continuations. The simplest and most direct use of continuation marks is to implement dynamically scoped variables, such as the current output stream or the current exception handler. Other uses include stack inspection for debugging or security checks, serialization of an in-progress computation, and run-time elision of redundant checks. By exposing continuation marks to users of a programming language, more kinds of language extensions can be implemented as libraries without further changes to the compiler. At the same time, the compiler and runtime system must provide an efficient implementation of continuation marks to ensure that library-implemented language extensions are as effective as changing the compiler. Our implementation of continuation marks for Chez Scheme (in support of Racket) makes dynamic binding and lookup constant-time and fast, preserves the performance of Chez Scheme's first-class continuations, and imposes negligible overhead on program fragments that do not use first-class continuations or marks.

Article Search
Securing Smart Contract with Runtime Validation
Ao Li, Jemin Andrew Choi, and Fan Long
(University of Toronto, Canada)


Article Search
Type-Directed Scheduling of Streaming Accelerators
David Durst, Matthew Feldman, Dillon Huff, David Akeley, Ross Daly, Gilbert Louis Bernstein, Marco Patrignani, Kayvon Fatahalian, and Pat Hanrahan
(Stanford University, USA; University of California at Los Angeles, USA; University of California at Berkeley, USA; CISPA, Germany)


Article Search
HipHop.js: (A)Synchronous Reactive Web Programming
Gérard Berry and Manuel Serrano
(Collège de France, France; Inria, France)
We present HipHop.js, a synchronous reactive language that adds synchronous concurrency and preemption to JavaScript. Inspired from Esterel, HipHop.js simplifies the programming of non-trivial temporal behaviors as found in complex web interfaces or IoT controllers and the cooperation between synchronous and asynchronous activities. HipHop.js is compiled into plain sequential JavaScript and executes on unmodified runtime environments. We use three examples to present and discuss HipHop.js: a simple web login form to introduce the language and show how it differs from JavaScript, and two real life examples, a medical prescription pillbox and an interactive music system that show why concurrency and preemption help programming such temporal applications.

Article Search Info
Validating SMT Solvers via Semantic Fusion
Dominik Winterer, Chengyu Zhang, and Zhendong Su
(ETH Zurich, Switzerland; East China Normal University, China)


Article Search
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu
(Columbia University, USA)


Article Search
CARAT: A Case for Virtual Memory through Compiler- and Runtime-Based Address Translation
Brian Suchy, Simone Campanoni, Nikos Hardavellas, and Peter Dinda
(Northwestern University, USA)


Article Search
Multi-modal Synthesis of Regular Expressions
Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, and Isil Dillig
(University of Texas at Austin, USA; University of Michigan at Ann Arbor, USA)
In this paper, we propose a multi-modal synthesis technique for automatically constructing regular expressions (regexes) from a combination of examples and natural language. Using multiple modalities is useful in this context because natural language alone is often highly ambiguous, whereas examples in isolation are often not sufficient for conveying user intent. Our proposed technique first parses the English description into a so-called hierarchical sketch that guides our programming-by-example (PBE) engine. Since the hierarchical sketch captures crucial hints, the PBE engine can leverage this information to both prioritize the search as well as make useful deductions for pruning the search space.
We have implemented the proposed technique in a tool called Regel and evaluate it on over three hundred regexes. Our evaluation shows that Regel achieves 80

Article Search
Automated Derivation of Parametric Data Movement Lower Bounds for Affine Programs
Auguste Olivry, Julien Langou, Louis-Noël Pouchet, P. Sadayappan, and Fabrice Rastello
(Inria, France; University of Colorado at Denver, USA; Colorado State University, USA; University of Utah, USA)


Article Search
Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities
Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis
(International Computer Science Institute, USA; University of Sydney, Australia; University of Malta, Malta; University of Athens, Greece)


Article Search
Crafty: Efficient, HTM-Compatible Persistent Transactions
Kaan Genç, Michael D. Bond, and Guoqing Harry Xu
(Ohio State University, USA; University of California at Los Angeles, USA)


Article Search
Zippy LL(1) Parsing with Derivatives
Romain Edelmann, Jad Hamza, and Viktor Kunčak
(EPFL, Switzerland)
In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.

Article Search
SmartTrack: Efficient Predictive Race Detection
Jake Roemer, Kaan Genç, and Michael D. Bond
(Ohio State University, USA)


Article Search
From Folklore to Fact: Comparing Implementations of Stacks and Continuations
Kavon Farvardin and John Reppy
(University of Chicago, USA)


Article Search
PMEvo: Portable Inference of Port Mappings for Out-of-Order Processors by Evolutionary Optimization
Fabian Ritter and Sebastian Hack
(Saarland University, Germany)


Article Search
Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting
DongKwon Lee, Woosuk Lee, Hakjoo Oh, and Kwangkeun Yi
(Seoul National University, South Korea; Hanyang University, South Korea; Korea University, South Korea)


Article Search
Typilus: Neural Type Hints
Miltiadis Allamanis, Earl T. Barr, Soline Ducousso, and Zheng Gao
(Microsoft Research, n.n.; University College London, UK; ENSTA Paris, France)


Article Search
Adaptive Low-Overhead Scheduling for Periodic and Reactive Intermittent Execution
Kiwan Maeng and Brandon Lucia
(Carnegie Mellon University, USA)
Batteryless energy-harvesting devices eliminate the need in batteries for deployed sensor systems, enabling longer lifetime and easier maintenance. However, such devices cannot support an event-driven execution model (e.g., periodic or reactive execution), restricting the use cases and hampering real-world deployment. Without knowing exactly how much energy can be harvested in the future, robustly scheduling periodic and reactive workloads is challenging. We introduce CatNap, an event-driven energy-harvesting system with a new programming model that asks the programmer to express a subset of the code that is time-critical. CatNap isolates and reserves energy for the time-critical code, reliably executing it on schedule while deferring execution of the rest of the code. CatNap degrades execution quality when a decrease in the incoming power renders it impossible to maintain its schedule. Our evaluation on a real energy-harvesting setup shows that CatNap works well with end-to-end, real-world deployment settings. CatNap reliably runs periodic events when a prior system misses the deadline by 7.3x and supports reactive applications with a 100% success rate when a prior work shows less than a 2% success rate.

Article Search
Blended, Precise Semantic Program Embeddings
Ke Wang and Zhendong Su
(Visa Research, n.n.; ETH Zurich, Switzerland)
Learning neural program embeddings is key to utilizing deep neural networks in program languages research --- precise and efficient program representations enable the application of deep models to a wide range of program analysis tasks. Existing approaches predominately learn to embed programs from their source code, and, as a result, they do not capture deep, precise program semantics. On the other hand, models learned from runtime information critically depend on the quality of program executions, thus leading to trained models with highly variant quality. This paper tackles these inherent weaknesses of prior approaches by introducing a new deep neural network, Liger, which learns program representations from a mixture of symbolic and concrete execution traces. We have evaluated Liger on two tasks: method name prediction and semantics classification. Results show that Liger is significantly more accurate than the state-of-the-art static model code2seq in predicting method names, and requires on average around 10x fewer executions covering nearly 4x fewer paths than the state-of-the-art dynamic model DYPRO in both tasks. Liger offers a new, interesting design point in the space of neural program embeddings and opens up this new direction for exploration.

Article Search
PMThreads: Persistent Memory Threads Harnessing Versioned Shadow Copies
Zhenwei Wu, Kai Lu, Andrew Nisbet, Wenzhe Zhang, and Mikel Luján
(National University of Defense Technology, China; University of Manchester, UK)


Article Search
Semantic Code Search via Equational Reasoning
Varot Premtoon, James Koppel, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)


Article Search
Proving Almost-Sure Termination by Omega-Regular Decomposition
Jianhui Chen and Fei He
(Tsinghua University, China)
Almost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. Our approach automatically decomposes the runs of the probabilistic program into a finite union of ω-regular subsets and then proves almost-sure termination of each subset based on the notion of localized ranking supermartingales. Compared to the lexicographic methods and the compositional methods, our approach does not require a lexicographic order over the ranking supermartingales as well as the so-called unaffecting condition. Thus it has high generality. We present the algorithm of our approach and prove its soundness, as well as its relative completeness. We show that our approach can be applied to some hard cases and the evaluation on the benchmarks of previous works shows the significant efficiency of our approach.

Article Search
FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates
(University of Edinburgh, UK; Imperial College London, UK)
ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types.
Type inference for unrestricted System F-style polymorphism is undecidable in general. Nevertheless, the literature abounds with a range of proposals to bridge the gap between ML and System F.
We put forth a new proposal, FreezeML, a conservative extension of ML with two new features. First, let- and lambda-binders may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. FreezeML is equipped with type-preserving translations back and forth between System F and admits a type inference algorithm, an extension of algorithm W, that is sound and complete and which yields principal types.

Article Search
Debugging and Detecting Numerical Errors in Computation with Posits
Sangeeta Chowdhary, Jay P. Lim, and Santosh Nagarakatte
(Rutgers University, USA)


Article Search
Type Error Feedback via Analytic Program Repair
Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, and Ranjit Jhala
(University of California at San Diego, USA; University of Michigan, USA)


Article Search
λESI: Exact Inference for Higher-Order Probabilistic Programs
Timon Gehr, Samuel Steffen, and Martin Vechev
(ETH Zurich, Switzerland)


Article Search
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev
(ETH Zurich, Switzerland)


Article Search
CacheQuery: Learning Replacement Policies from Hardware Caches
Pepe Vila, Pierre Ganty, Marco Guarnieri, and Boris Köpf
(IMDEA Software Institute, Spain; Microsoft Research, n.n.)


Article Search
Reactive Probabilistic Programming
Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin
(IBM Research, n.n.; Massachusetts Institute of Technology, USA; Ecole Normale Superieure, n.n.)


Article Search
Promising 2.0: Global Optimizations in Relaxed Memory Concurrency
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis
(Seoul National University, South Korea; National Research University Higher School of Economics, Russia; MPI-SWS, Germany; IIT Delhi, India; Tel Aviv University, Israel)


Article Search
On the Principles of Differentiable Quantum Programming Languages
Shaopeng Zhu, Shih-Han Hung, Shouvanik Chakrabarti, and Xiaodi Wu
(University of Maryland, USA)
Variational Quantum Circuits (VQCs), or the so-called quantum neural-networks, are predicted to be one of the most important near-term quantum applications, not only because of their similar promises as classical neural-networks, but also because of their feasibility on near-term noisy intermediate-size quantum (NISQ) machines. The need for gradient information in the training procedure of VQC applications has stimulated the development of auto-differentiation techniques for quantum circuits. We propose the first formalization of this technique, not only in the context of quantum circuits but also for imperative quantum programs (e.g., with controls), inspired by the success of differentiable programming languages in classical machine learning. In particular, we overcome a few unique difficulties caused by exotic quantum features (such as quantum no-cloning) and provide a rigorous formulation of differentiation applied to bounded-loop imperative quantum programs, its code-transformation rules, as well as a sound logic to reason about their correctness. Moreover, we have implemented our code transformation in OCaml and demonstrated the resource-efficiency of our scheme both analytically and empirically. We also conduct a case study of training a VQC instance with controls, which shows the advantage of our scheme over existing auto-differentiation for quantum circuits without controls.

Article Search
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock
(University of Washington, USA; Certora, n.n.; MPI-SWS, Germany)


Article Search
Responsive Parallelism with Futures and State
Stefan K. Muller, Kyle Singer, Noah Goldstein, Umut A. Acar, Kunal Agrawal, and I-Ting Angelina Lee
(Carnegie Mellon University, USA; Washington University at St. Louis, USA)


Article Search
Gillian: Parametric Symbolic Execution for All
José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner
(Instituto Superior Técnico, Portugal; Imperial College London, UK; Mathematical Institute SASA, n.n.)


Article Search
A Study of the Learnability of Relational Properties
Muhammad Usman, Wenxi Wang, Marko Vasic, Kaiyuan Wang, Haris Vikalo, and Sarfraz Khurshid
(University of Texas at Austin, USA; Google, USA)


Article Search
Learning Fast and Precise Numerical Analysis
Jingxuan He, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)


Article Search
BlankIt Library Debloating: Getting What You Want Instead of Cutting What You Don’t
Chris Porter, Girish Mururu, Prithayan Barua, and Santosh Pande
(Georgia Institute of Technology, USA)


Article Search
First-Order Quantified Separators
Jason R. Koenig, Oded Padon, Neil Immerman, and Alex Aiken
(Stanford University, USA; University of Massachusetts at Amherst, USA)


Article Search
NV: An Intermediate Language for Verification of Network Control Planes
Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker
(Princeton University, USA; Microsoft Research, USA)


Article Search
Debug Information Validation for Optimized Code
Yuanbo Li, Shuo Ding, Qirun Zhang, and Davide Italiano
(Georgia Institute of Technology, USA; Apple, USA)


Article Search
Fast Graph Simplification for Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin, USA)
Many program-analysis problems can be formulated as graph-reachability problems. Interleaved Dyck language reachability. Interleaved Dyck language reachability (InterDyck-reachability) is a fundamental framework to express a wide variety of program-analysis problems over edge-labeled graphs. The InterDyck language represents an intersection of multiple matched-parenthesis languages (i.e., Dyck languages). In practice, program analyses typically leverage one Dyck language to achieve context-sensitivity, and other Dyck languages to model data dependences, such as field-sensitivity and pointer references/dereferences. In the ideal case, an InterDyck-reachability framework should model multiple Dyck languages simultaneously.
Unfortunately, precise InterDyck-reachability is undecidable. Any practical solution must over-approximate the exact answer. In the literature, a lot of work has been proposed to over-approximate the InterDyck-reachability formulation. This paper offers a new perspective on improving both the precision and the scalability of InterDyck-reachability: we aim to simplify the underlying input graph G. Our key insight is based on the observation that if an edge is not contributing to any InterDyck-path, we can safely eliminate it from G. Our technique is orthogonal to the InterDyck-reachability formulation, and can serve as a pre-processing step with any over-approximating approaches for InterDyck-reachability. We have applied our graph simplification algorithm to pre-processing the graphs from a recent InterDyck-reachability-based taint analysis for Android. Our evaluation on three popular InterDyck-reachability algorithms yields promising results. In particular, our graph-simplification method improves both the scalability and precision of all three InterDyck-reachability algorithms, sometimes dramatically.

Article Search
Behavioral Simulation for Smart Contracts
Sidi Mohamed Beillahi, Gabriela Ciocarlie, Michael Emmi, and Constantin Enea
(University of Paris Diderot, France; SRI International, n.n.)


Article Search
EVA: An Encrypted Vector Arithmetic Language and Compiler for Efficient Homomorphic Computation
Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, and Madan Musuvathi
(University of Texas at Austin, USA; EPFL, Switzerland; Microsoft Research, n.n.)


Article Search
LLHD: A Multi-level Intermediate Representation for Hardware Description Languages
Fabian Schuiki, Andreas Kurth, Tobias Grosser, and Luca Benini
(ETH Zurich, Switzerland)


Article Search
Question Selection for Interactive Program Synthesis
Ruyi Ji, Jingjing Liang, Yingfei Xiong, Lu Zhang, and Zhenjiang Hu
(Peking University, China)
Interactive program synthesis aims to solve the ambiguity in specifications, and selecting the proper question to minimize the rounds of interactions is critical to the performance of interactive program synthesis. In this paper we address this question selection problem and propose two algorithms. SampleSy approximates a state-of-the-art strategy proposed for optimal decision tree and has a short response time to enable interaction. EpsSy further reduces the rounds of interactions by approximating SampleSy with a bounded error rate. To implement the two algorithms, we further propose VSampler, an approach to sampling programs from a probabilistic context-free grammar based on version space algebra. The evaluation shows the effectiveness of both algorithms.

Article Search Info
Static Analysis of Java Enterprise Applications: Frameworks and Caches, the Elephants in the Room
Anastasios Antoniadis, Nikos Filippakis, Paddy Krishnan, Raghavendra Ramesh, Nicholas Allen, and Yannis Smaragdakis
(University of Athens, Greece; CERN, Switzerland; Oracle Labs, Australia; ConsenSys, Australia)


Article Search
Reconciling Enumerative and Deductive Program Synthesis
Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, and Yanjun Wang
(Purdue University, USA)
Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability.
In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms.

Article Search Archive submitted (1 MB) Info
SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework
Sotiris Apostolakis, Ziyang Xu, Zujun Tan, Greg Chan, Simone Campanoni, and David I. August
(Princeton University, USA; Northwestern University, USA)
Program analysis determines the potential dataflow and control flow relationships among instructions so that compiler optimizations can respect these relationships to transform code correctly. Since many of these relationships rarely or never occur, speculative optimizations assert they do not exist while optimizing the code. To preserve correctness, speculative optimizations add validation checks to activate recovery code when these assertions prove untrue. This approach results in many missed opportunities because program analysis and thus other optimizations remain unaware of the full impact of these dynamically-enforced speculative assertions. To address this problem, this paper presents SCAF, a Speculation-aware Collaborative dependence Analysis Framework. SCAF learns of available speculative assertions via profiling, computes their full impact on memory dependence analysis, and makes this resulting information available for all code optimizations. SCAF is modular (adding new analysis modules is easy) and collaborative (modules cooperate to produce a result more precise than the confluence of all individual results). Relative to the best prior speculation-aware dependence analysis technique, by computing the full impact of speculation on memory dependence analysis, SCAF dramatically reduces the need for expensive-to-validate memory speculation in the hot loops of all 16 evaluated C/C++ SPEC benchmarks.

Article Search
Verifying Concurrent Search Structure Templates
Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies
(Microsoft Research, USA; New York University, USA)


Article Search
Effective Function Merging in the SSA Form
Rodrigo C. O. Rocha, Pavlos Petoumenos, Zheng Wang, Murray Cole, and Hugh Leather
(University of Edinburgh, UK; University of Leeds, UK)


Article Search
NVTraverse: In NVRAM Data Structures, the Destination Is More Important Than the Journey
Naama Ben-David, Guy E. Blelloch, Michal Friedman, Erez Petrank, and Yuanhao Wei
(Carnegie Mellon University, USA; Technion, Israel)


Article Search
Faster General Parsing through Context-Free Memoization
Grzegorz Herman
(Jagiellonian University, Poland)


Article Search
Compiler-Directed Soft Error Resilience for Lightweight GPU Register File Protection
Hongjune Kim, Jianping Zeng, Qingrui Liu, Mohammad Rajab Abdel-Majeed, Jaejin Lee, and Changhee Jung
(Seoul National University, South Korea; Purdue University, USA; Virginia Tech, USA; University of Jordan, Jordan)


Article Search
Efficient Handling of String-Number Conversion
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janků, Hsin-Hung Lin, Lukáš Holík, and Wei-Cheng Wu
(Uppsala University, Sweden; Academia Sinica, Taiwan; IBM Research, USA; Brno University of Technology, Czechia; University of Southern California, USA)


Article Search
Templates and Recurrences: Better Together
Jason Breck, John Cyphert, Zachary Kincaid, and Thomas Reps
(University of Wisconsin-Madison, USA; Princeton University, USA)


Article Search
Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs
Boqin Qin, Yilun Chen, Zeming Yu, Linhai Song, and Yiying Zhang
(Pennsylvania State University, USA; Purdue University, USA; University of California at San Diego, USA)


Article Search
Towards an API for the Real Numbers
Hans-J. Boehm
(Google, n.n.)


Article Search

proc time: 3.1