Replication Package for Artifact： Data-Driven Inference of Representation Invariants
作者: Miltner, Anders and Padhi, Saswat and Millstein, Todd and Walker, David
关键词: Abstract Data Types, Logical Relations, Type-Directed Synthesis
Abstract
This archive contains the code and benchmarks for the paper Data-Driven Inference of Representation Invariants.
Instructions for installation and build, instructions for reproduction of the results, and a description of the structure of the repository, are all available in the file $/README.pdf.
Replication Package for Article： Type Error Feedback via Analytic Program Repair
作者: Sakkas, Georgios and Endres, Madeline and Cosman, Benjamin and Weimer, Westley and Jhala, Ranjit
关键词: Machine Learning, Program Repair, Program Synthesis, Type Error Feedback
Abstract
The artifact contains all the necessary code and data in order to reproduce the results from the paper "Type Error Feedback via Analytic Program Repair" as appeared in PLDI 2020. Instructions for installing and running the artifact can be found in the provided README file.
Szalinski： A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
作者: Nandi, Chandrakana and Willsey, Max and Anderson, Adam and Wilcox, James R. and Darulova, Eva and Grossman, Dan and Tatlock, Zachary
关键词: CAD, Compiler Optimization, Computational Geometry, Synthesis
Abstract
Paper pldi20main-p471-p
Goals of the artifact
In our paper, we evaluated the following about Szalinski (Section 7):
End-to-End: we ran Szalinski on the flat CSG outputs of a mesh decompiler (Reincarnate). The results are in
Table 2.Scalability: we evaluated Szalinski on a large dataset of models scraped from a popular online repository (Thingiverse). The results are in
Figure 14(first three box plots).Sensitivity: we evaluated the usefulness of Szalinski's two main features: CAD rewrites and Inverse Transformations. The results are in
Figure 14(last two box plots).
In support of these results, this artifact reproduces Table 2 and Figure 14. In addition, it also generates the output programs in Figure 15 that are used in the case studies.
This document contains the following parts:
System requirements
- How to run Szalinski
- Reproducing Table 2 (takes < 5 minutes)
- Reproducing Figure 14 (takes approx. 1.5 hour)
- Reproducing Figure 15 (takes < 5 minutes)
Validation
- Reusability
- How to set up Szalinski on a different machine (this is also how we set up the VM we submitted for PLDI 2020 AEC)
Description of the code and how to modify it
Notes and remarks
System requirements
- Specs of the machine where we ran the VM: Intel i7-8700K (12 threads @ 4.7GHz), 32GiB RAM
Running the tools
Reproducing Table 2
Navigate to the directory that contains the Makefile and type make out/aec-table2/table2.csv. This should take about 3 minutes. This will reproduce Table 2 from the paper. To view the content of the table, type cat out/aec-table2/table2.csv | column -t -s, and compare the numbers with Table 2 in the paper.
NOTE: - We suspect that different versions of OpenSCAD use different triangulation algorithms for compiling to mesh which can affect the numbers in the #Tri column.
Reproducing Figure 14
We have included in the repo the 2,127 examples from Thingiverse that we evaluated on in the paper. The remainder of the 12,939 scraped from Thingiverse were either malformed or used features not supported by Szalinski. The script (scripts/scrape-thingiverse.sh) scrapes models under the customizable category, from the first 500 pages.
NOTE: Running this part takes about an hour. We recommend first reproducing Figure 15 and Table 2, both of which take much less time.
Navigate to the directory that contains the Makefile and type make out/fig14.pdf. Open the generated file in a pdf viewer and compare with Figure 14 in the paper.
Reproducing Figure 15 programs
Navigate to the directory that contains the Makefile and type make aec-fig15. This should take less than a minute. Then look in the out/aec-fig15 directory. The optimized programs generated by Szalinski are in the files with extensions normal.csexp.opt. There should be 6 such files. Open them and compare the content with the programs listed in Figure 15 of the paper.
NOTE: - The programs in the paper are sugared and represented more compactly for space. - MapI found in the artifact results corresponds to Tabulate in the paper. - When comparing the results generated by the artifact to the programs in Figure 15 of the paper, it is most important to check that the high-level structure in terms of Fold and MapI synthesized by the artifact matches that reported in the paper.
Validation
Section 6 of our paper describes Szalinski's validation process. We use OpenSCAD to compile CSG programs to meshes and use CGAL to compute the Hausdorff distance between two meshes.
To validate the programs in Figure 15, run make out/aec-fig15/hausdorff. This should terminate in less than 3 minutes. It should show you the names of the 6 examples in Figure 15 and the corresponding Hausdorff distances which are close to zero.
We have also validated all our other results reported in the paper. However, our experience indicates that OpenSCAD's compilation step is often very slow. Therefore, the other commands mentioned in the instruction for reproducing the results do not perform validation by default.
You can validate any example from our evaluation by typing: make out/dir_name/example_name.normal.diff, where dir_name can be aec-table2, aec_fig15 or thingiverse, and example_name is the name of whatever example you choose. Then open the generated .diff file and check that the Hausdorff distance is within some epsilon of 0.
NOTE: For many example, CGAL crashes or is slow at computing the Hausdorff distance. For these, we recommend a manual validation if you are interested. In order to validate an example, type the following: make out/dir_name/example_name.diff.scad. You can open the generated .scad file in OpenSCAD (already installed in the VM). In OpenSCAD, click on the Render button (the second button from the right) in the toolbar. You should either see nothing rendered or some residual thin walls that are artifacts of rounding error prevalent in OpenSCAD.
Reusability
Here we provide instructions on how to start using Szalinski including installation and changing the rules and features of the Caddy language.
Setup instructions
Following are the steps for setting up Szalinski from scratch on a machine that runs Ubuntu 19.10.
Install rust. Type
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | shin the terminal and follow the subsequent instructions. The version we used is1.41.0. Seehttps://www.rust-lang.org/tools/installfor more information.Make sure you configure your current shell by typing:
source $HOME/.cargo/env(the Rust installation will prompt you to do this).Install make by typing:
sudo apt-get install makeInstall g++ by typing:
sudo apt-get install g++Install jq by typing:
sudo apt-get install jqInstall CGAL by typing
sudo apt-get install libcgal-devInstall OpenSCAD by typing
sudo apt-get install openscadInstall git by typing
sudo apt install gitInstall pip by typing
sudo apt install python3-pipand then installnumpyby typingpip3 install numpyandmatplotlibby typingpip3 install matplotlibWe have made a github release for the PLDI AEC from where you can get the source.
Navigate to the project directory where the
Makefileis and run the tool as described above.
Changing Caddy and modifying the rules
The Caddy language is defined in
cad.rsin thesrcdirectory. A simple feature you can add is support for a new primitive or new transformations. You can also change the costs of various language constructs. The definition of thecostfunction starts at line267.As we described in the paper, to verify the correctness of Szalinski, we evaluate Caddy programs to flat Core Caddy and pretty print to CSG. This code is in
eval.rs.solve.rsandpermute.rscontains code that solves for first and second degree polynomials in Cartesian and Spherical coordinates, and performs partitioning and permutations of lists.The rewrites rules are in
rules.rs. Syntactic rewrites are written using therw!macro. Each rewrite has a name, a left hand side, and a right hand side. You can add / remove rules to see how that affects the final Caddy output of Szalinski. For example, if you comment out the rules for inverse transformations, they will not be propagated and eliminated, and therefore the quality of Szalinski's output will not be as good.
Notes and remarks
Szalinski is implemented in Rust. As mentioned in Section 6 of the paper, it uses OpenSCAD to compile CSG programs to triangular meshes, and CGAL to compute the Hausdorff distance between two meshes.
Replication Package for Article： Compiler and Runtime Support for Continuation Marks
作者: Flatt, Matthew and Dybvig, R. Kent
关键词: context inspection, Dynamic binding
Abstract
The artifact contains the full source code for Racket and Chez Scheme and variants as described in the paper, and it provides benchmarks that can be used to support the following claims:
The implementation of continuation marks is compatible with a high-performance implementation of first-class, delimited continuations.
Compiler and runtime support for continuation marks can improve the performance of applications.
Specific optimizations described in the paper improve the performance of continuation marks and applications that use them.
Artifact for Article： Crafty： Efficient, HTM-Compatible Persistent Transactions
作者: Gen\c{c
关键词: Crafty, non-volatile memory, persistent memory, persistent transactions
Abstract
The artifact contains the source code of our implementation, including the microbenchmarks we evaluated and the code required to generate the graphs seen in the paper. It also contains a Docker image that includes all requirements for building and running the code. Using the Docker image is optional but highly recommended. A README file detailing how to reproduce our results is included.
Replication Package for Article： From Folklore to Fact： Comparing Implementations of Stacks and Continuations
作者: Farvardin, Kavon and Reppy, John
关键词: Call stacks, Compilers, Concurrency, Continuations, Functional Programming
Abstract
This artifact contains all materials needed to reproduce or extend the results of this work. It includes the raw data and plots corresponding to the results presented in the paper, the full source code of Manticore \& LLVM (plus the benchmark programs and plotting scripts), a Docker image that contains the entire system pre-built, and an extensive README that describes how to build and run our benchmark suite to replicate the experiments in the paper.
Typilus： neural type hints
作者: Allamanis, Miltiadis and Barr, Earl T. and Ducousso, Soline and Gao, Zheng
关键词: deep learning, graph neural networks, meta-learning, structured learning, type inference
Abstract
Type inference over partial contexts in dynamically typed languages is challenging. In this work, we present a graph neural network model that predicts types by probabilistically reasoning over a program’s structure, names, and patterns. The network uses deep similarity learning to learn a TypeSpace — a continuous relaxation of the discrete space of types — and how to embed the type properties of a symbol (i.e. identifier) into it. Importantly, our model can employ one-shot learning to predict an open vocabulary of types, including rare and user-defined ones. We realise our approach in Typilus for Python that combines the TypeSpace with an optional type checker. We show that Typilus accurately predicts types. Typilus confidently predicts types for 70% of all annotatable symbols; when it predicts a type, that type optionally type checks 95% of the time. Typilus can also find incorrect type annotations; two important and popular open source libraries, fairseq and allennlp, accepted our pull requests that fixed the annotation errors Typilus discovered.
Learning nonlinear loop invariants with gated continuous logic networks
作者: Yao, Jianan and Ryan, Gabriel and Wong, Justin and Jana, Suman and Gu, Ronghui
关键词: Continuous Logic Networks, Loop Invariant Inference, Program Verification
Abstract
Verifying real-world programs often requires inferring loop invariants with nonlinear constraints. This is especially true in programs that perform many numerical operations, such as control systems for avionics or industrial plants. Recently, data-driven methods for loop invariant inference have shown promise, especially on linear loop invariants. However, applying data-driven inference to nonlinear loop invariants is challenging due to the large numbers of and large magnitudes of high-order terms, the potential for overfitting on a small number of samples, and the large space of possible nonlinear inequality bounds. In this paper, we introduce a new neural architecture for general SMT learning, the Gated Continuous Logic Network (G-CLN), and apply it to nonlinear loop invariant learning. G-CLNs extend the Continuous Logic Network (CLN) architecture with gating units and dropout, which allow the model to robustly learn general invariants over large numbers of terms. To address overfitting that arises from finite program sampling, we introduce fractional sampling—a sound relaxation of loop semantics to continuous functions that facilitates unbounded sampling on the real domain. We additionally design a new CLN activation function, the Piecewise Biased Quadratic Unit (PBQU), for naturally learning tight inequality bounds. We incorporate these methods into a nonlinear loop invariant inference system that can learn general nonlinear loop invariants. We evaluate our system on a benchmark of nonlinear loop invariants and show it solves 26 out of 27 problems, 3 more than prior work, with an average runtime of 53.3 seconds. We further demonstrate the generic learning ability of G-CLNs by solving all 124 problems in the linear Code2Inv benchmark. We also perform a quantitative stability evaluation and show G-CLNs have a convergence rate of 97.5% on quadratic problems, a 39.2% improvement over CLN models.
Blended, precise semantic program embeddings
作者: Wang, Ke and Su, Zhendong
关键词: Attention Network, Semantic Program Embedding, Static and Dynamic Program Features
Abstract
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.
Towards a Verified Range Analysis for JavaScript JITs： Artifact
作者: Brown, Fraser and Renner, John and N"{o
关键词: verification
Abstract
Artifact for "Towards a Verified Range Analysis for JavaScript JITS"
Binary rewriting without control flow recovery
作者: Duck, Gregory J. and Gao, Xiang and Roychoudhury, Abhik
关键词: binary instrumentation, binary patching, binary repair, instruction eviction, instruction punning, memory management, static binary rewriting
Abstract
Static binary rewriting has many important applications in software security and systems, such as hardening, repair, patching, instrumentation, and debugging. While many different static binary rewriting tools have been proposed, most rely on recovering control flow information from the input binary. The recovery step is necessary since the rewriting process may move instructions, meaning that the set of jump targets in the rewritten binary needs to be adjusted accordingly. Since the static recovery of control flow information is a hard problem in general, most tools rely on a set of simplifying heuristics or assumptions, such as specific compilers, specific source languages, or binary file meta information. However, the reliance on assumptions or heuristics tends to scale poorly in practice, and most state-of-the-art static binary rewriting tools cannot handle very large/complex programs such as web browsers. In this paper we present E9Patch, a tool that can statically rewrite x86_64 binaries without any knowledge of control flow information. To do so, E9Patch develops a suite of binary rewriting methodologies—such as instruction punning, padding, and eviction—that can insert jumps to trampolines without the need to move other instructions. Since this preserves the set of jump targets, the need for control flow recovery and related heuristics is eliminated. As such, E9Patch is robust by design, and can scale to very large (>100MB) stripped binaries including the Google Chrome and FireFox web browsers. We also evaluate the effectiveness of E9Patch against realistic applications such as binary instrumentation, hardening and repair.
Replication Package for article： BlankIt Library Debloating： Getting What You Want Instead of Cutting What You Don’t
作者: Porter, Chris and Mururu, Girish and Barua, Prithayan and Pande, Santosh
关键词: software debloating
Abstract
These are the docker containers to reproduce the main results of the paper.
Mechanized proofs accompanying paper： Verifying Concurrent Search Structure Templates
作者: Krishna, Siddharth and Patel, Nisarg and Shasha, Dennis and Wies, Thomas
关键词: concurrent search structures, Coq, functional correctness, Grasshopper, Iris, mechanized proofs, memory safety
Abstract
Our artifact consists of two parts: the proofs of template algorithms, to be verified by Iris/Coq, and the proofs of implementations, to be verified by GRASShopper.
Replication Package for Article “Armada： Low-Effort Verification of High-Performance Concurrent Programs”
作者: Lorch, Jacob R. and Chen, Yixuan and Kapritsos, Manos and Parno, Bryan and Qadeer, Shaz and Sharma, Upamanyu and Wilcox, James R. and Zhao, Xueyuan
关键词: refinement, weak memory models, x86-TSO
Abstract
This artifact contains the materials necessary for replication of the paper "Armada: Low-Effort Verification of High-Performance Concurrent Programs". It contains a Docker image containing the source code, executables, external dependencies, and examples. It also contains documentation of the artifact and a description of the Armada language.
Coq proofs for： Decidable Verification under a Causally Consistent Shared Memory
作者: Lahav, Ori and Boker, Udi
关键词: causal consistency, concurrency, Coq, decidability, release/acquire, shared-memory, verification, weak memory models, well-structured transition systems
Abstract
The artifact consists of the Coq development accompanying the paper. The main result is the equivalence between loSRA (called SRAL in the Coq development) and opSRA (called SRAG in the Coq development) that is given in Lemmas 5.15 and 5.16 in the paper. This final result is included in "SRAL_SRAG.v".
Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact)
作者: Kragl, Bernhard and Enea, Constantin and Henzinger, Thomas A. and Mutluergil, Suha Orhun and Qadeer, Shaz
关键词: abstraction, asynchrony, concurrency, induction, invariants, layers, movers, reduction, refinement, verification
Abstract
Inductive sequentialization is implemented as an extension of the CIVL verifier. This implementation and all examples listed in Table 1 of the paper are part of the open-source project Boogie. This artifact is for long-term archiving purposes and contains a snapshot of Boogie version 2.6.4. Since the project is under active development, we recommend to obtain the most recent version from https://github.com/boogie-org/boogie.
For further information and instructions, see the included README.md file.
The essence of Bluespec： a core language for rule-based hardware design
作者: Bourgeat, Thomas and Pit-Claudel, Cl'{e
关键词: Compiler Correctness, Hardware Description Language, Semantics
Abstract
The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits. Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design. In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies. Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits. We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.
Replication Package for Paper： LLHD： A Multi-level Intermediate Representation for Hardware Description Languages
作者: Schuiki, Fabian and Kurth, Andreas and Grosser, Tobias and Benini, Luca
关键词: domain-specific languages, hardware, language design, language implementation, new programming models or languages, parallelism
Abstract
A Docker image with the necessary toolchains pre-installed and source codes pre-loaded to reproduce the main results of the LLHD paper, and to serve as a starting point for individual exploration.
Replication Package for： On the Principles of Differentiable Quantum Programming Languages
作者: Zhu, Shaopeng and Hung, Shih-Han and Chakrabarti, Shouvanik and Wu, Xiaodi
关键词: autodifferentiation, differentiable programming, quantum computing, quantum machine learning, quantum programming languages
Abstract
The artifact includes two parts: (1) A parser and compiler that implements the rules for autodifferentiaton; (2) A simulation that demonstrates the advantage of differentiating quantum programs with control flow. Classical simulation of quantum programs is used in this part for evaluation.
silq-artifact
作者: Bichsel, Benjamin and Baader, Maximilian and Gehr, Timon and Vechev, Martin
关键词: Quantum Language, Semantics, Uncomputation
Abstract
Artifact for PLDI'20 paper "Silq: A High-level Quantum Programming Language with Safe Uncomputation and Intuitive Semantics".
Replication Package for Article： Improving Program Locality in the GC using Hotness
作者: Yang, Albert Mingkun and "{O
关键词: garbage collection, load barrier, openjdk, program locality
Abstract
It includes our implementation, benchmarks used, and scripts for running benchmarks and collecting/visualizing results.
Implementation and Benchmark suite for Article： A Marriage of Pointer- and Epoch-Based Reclamation
作者: Kang, Jeehoon and Jung, Jaehwang
关键词: epoch-based reclamation, garbage collection, hazard pointer, pointer-based reclamation, safe memory reclamation
Abstract
A Marriage of Pointer- and Epoch-Based Reclamation
This is the artifact for
Jeehoon Kang and Jaehwang Jung, A Marriage of Pointer- and Epoch-Based Reclamation, PLDI 2020.
The latest developments are on https://github.com/kaist-cp/pebr-benchmark.
Summary
On Ubuntu 18.04,
sudo apt install build-essential python3-pip
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
pip3 install --user pandas plotnine
python3 bench.py
python3 plot.pyDependencies
- Linux >= 4.14 for
MEMBARRIER_CMD_PRIVATE_EXPEDITEDandMEMBARRIER_CMD_REGISTER_PRIVATE_EXPEDITED, used in the implementation of PEBR.- IMPORTANT: Docker disables this feature by default. To enable, please use
--security-opt seccomp:unconfinedoption when launching Docker.
- IMPORTANT: Docker disables this feature by default. To enable, please use
rustupfor building the implementation of NR, EBR, PEBR and data structures- Rust requires GCC for linking in Linux.
- Python >= 3.6, pandas and plotnine for benchmark runner and plotting scripts
Usage
To build the benchmark,
git submodule update --init --recursive # not needed if you got the archived source code
cargo build --release # remove --release for debug buildTo run a single test,
./target/release/pebr-benchmark -d <data structure> -m <reclamation scheme> -t <threads>where
- data structure: HList, HMList, HHSList, HashMap, NMTree, BonsaiTree
- reclamation scheme: NR, EBR, PEBR
For detailed usage information,
./target/release/pebr-benchmark -hTo run the entire benchmark,
python3 bench.pyThis takes several hours and creates raw CSV data under ./results/.
To generate plots,
python3 plot.pyThis creates plots presented in the paper under ./results/.
Debug
We used ./sanitize.sh to debug our implementation. This script runs the benchmark with LLVM address sanitizer for Rust and uses parameters that impose high stress on PEBR by triggering more frequent ejection.
Note that sanitizer may report memory leaks when used against -m EBR. This is because of a minor bug in original Crossbeam but it doesn't affect performance of our benchmark.
Project structure
./crossbeam-pebris the fork of Crossbeam that implements PEBR. The main implementation of PEBR lies under./crossbeam-pebr/crossbeam-epoch../crossbeam-ebris the original Crossbeam source code../srccontains the benchmark driver (./src/main.rs) and the implementation of data structures based on PEBR (./src/pebr/) and original Crossbeam (./src/ebr/).
Results
./paper-results contains the raw results and graphs used in the paper.
Note
On Windows, the benchmark uses the default memory allocator instead of jemalloc since the Rust library for jemalloc does not support Windows.
The benchmark run by
./sanitize.shwill generate inaccurate memory usage report since it uses the default memory allocator instead of jemalloc. The memory tracker relies on jemalloc's functionalities which doesn't keep track of allocations by the default allocator.
CARAT： a case for virtual memory through compiler- and runtime-based address translation
作者: Suchy, Brian and Campanoni, Simone and Hardavellas, Nikos and Dinda, Peter
关键词: memory management, virtual memory
Abstract
Virtual memory is a critical abstraction in modern computer systems. Its common model, paging, is currently seeing considerable innovation, yet its implementations continue to be co-designs between power-hungry/latency-adding hardware (e.g., TLBs, pagewalk caches, pagewalkers, etc) and software (the OS kernel). We make a case for a new model for virtual memory, compiler- and runtime-based address translation (CARAT), which instead is a co-design between the compiler and the OS kernel. CARAT can operate without any hardware support, although it could also be retrofitted into a traditional paging model, and could leverage simpler hardware support. CARAT uses compile-time transformations and optimizations combined with tightly-coupled runtime/kernel interaction to generate programs that run efficiently in a physical address space, but nonetheless allow the kernel to maintain protection and dynamically manage physical memory similar to what is possible using traditional virtual memory. We argue for the feasibility of CARAT through an empirical study of application characteristics and kernel behavior, as well as through the design, implementation, and performance evaluation of a CARAT prototype. Because our prototype works at the IR level (in particular, via LLVM bitcode), it can be applied to most C and C++ programs with minimal or no restrictions.
Repairing and mechanising the JavaScript relaxed memory model
作者: Watt, Conrad and Pulte, Christopher and Podkopaev, Anton and Barbier, Guillaume and Dolan, Stephen and Flur, Shaked and Pichon-Pharabod, Jean and Guo, Shu-yu
关键词: ARMv8, Alloy, Coq, Web worker, weak memory
Abstract
Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the JavaScript specification defines an axiomatic relaxed memory model to describe their behaviour. While this model is heavily based on the C/C++11 model, it diverges in some key areas. JavaScript chooses to give a well-defined semantics to data-races, unlike the “undefined behaviour” of C/C++11. Moreover, the JavaScript model is mixed-size. This means that its accesses are not to discrete locations, but to (possibly overlapping) ranges of bytes. We show that the model, in violation of the design intention, does not support a compilation scheme to ARMv8 which is used in practice. We propose a correction, which also incorporates a previously proposed fix for a failure of the model to provide Sequential Consistency of Data-Race-Free programs (SC-DRF), an important correctness condition. We use model checking, in Alloy, to generate small counter-examples for these deficiencies, and investigate our correction. To accomplish this, we also develop a mixed-size extension to the existing ARMv8 axiomatic model. Guided by our Alloy experimentation, we mechanise (in Coq) the JavaScript model (corrected and uncorrected), our ARMv8 model, and, for the corrected JavaScript model, a “model-internal” SC-DRF proof and a compilation scheme correctness proof to ARMv8. In addition, we investigate a non-mixed-size subset of the corrected JavaScript model, and give proofs of compilation correctness for this subset to x86-TSO, Power, RISC-V, ARMv7, and (again) ARMv8, via the Intermediate Memory Model (IMM). As a result of our work, the JavaScript standards body (ECMA TC39) will include fixes for both issues in an upcoming edition of the specification.
Replication Package for Article： Promising 2.0： Global Optimizations in Relaxed Memory Concurrency
作者: Lee, Sung-Hwan and Cho, Minki and Podkopaev, Anton and Chakraborty, Soham and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor
关键词: Compiler Optimizations, Operational Semantics, Relaxed Memory Concurrency
Abstract
The artifact is a Coq development of the paper Promising 2.0: Global Optimizations and Relaxed Memory Concurrency. It includes (i) a Coq development of Promising 2.0 memory model and (ii) compilation correctness proof of Promising 2.0 to IMM. See README.md for more detail.
NVTraverse： in NVRAM data structures, the destination is more important than the journey
作者: Friedman, Michal and Ben-David, Naama and Wei, Yuanhao and Blelloch, Guy E. and Petrank, Erez
关键词: Concurrent Data Structures, Lock-free, Non-blocking, Non-volatile Memory
Abstract
The recent availability of fast, dense, byte-addressable non-volatile memory has led to increasing interest in the problem of designing durable data structures that can recover from system crashes. However, designing durable concurrent data structures that are correct and efficient has proven to be very difficult, leading to many inefficient or incorrect algorithms. In this paper, we present a general transformation that takes a lock-free data structure from a general class called traversal data structure (that we formally define) and automatically transforms it into an implementation of the data structure for the NVRAM setting that is provably durably linearizable and highly efficient. The transformation hinges on the observation that many data structure operations begin with a traversal phase that does not need to be persisted, and thus we only begin persisting when the traversal reaches its destination. We demonstrate the transformation’s efficiency through extensive measurements on a system with Intel’s recently released Optane DC persistent memory, showing that it can outperform competitors on many workloads.
Replication Package for Article： Predictable Accelerator Design with Time-Sensitive Affine types
作者: Nigam, Rachit and Atapattu, Sachille and Thomas, Samuel and Li, Zhijing and Bauer, Theodore and Ye, Yuwei and Koti, Apurva and Sampson, Adrian and Zhang, Zhiru
关键词: affine types, high-level synthesis
Abstract
Contains the following repositories: - Dahlia (v0.0.1): The reference compiler built for the paper. - Dahlia-evaluation: The data and the evaluation scripts. - Dahlia-spatial-comparison: Repository to reproduce Dahlia's Spatial evaluation. - Polyphemus: Server framework used to run FPGA experiments on AWS.
Replication Package for Article： Type-Directed Scheduling of Streaming Accelerators
作者: Durst, David and Feldman, Matthew and Huff, Dillon and Akeley, David and Daly, Ross and Bernstein, Gilbert Louis and Patrignani, Marco and Fatahalian, Kayvon and Hanrahan, Pat
关键词: FPGAs, hardware description languages, image processing, scheduling, space-time types
Abstract
This is the artifact for the PLDI 2020 paper "Type-Directed Scheduling of Streaming Accelerators". The artifact is a virtual machine that supports the claims, including reproducing the results, of the submission version of the paper. Please go to https://aetherling.org for the latest version of the code.
Virtual Machine for paper “FreezeML： Complete and Easy Type Inference for First-Class Polymorphism”
作者: Emrich, Frank and Lindley, Sam and Stolarek, Jan and Cheney, James and Coates, Jonathan
关键词: first-class polymorphism, impredicative types, type inference
Abstract
The artifact is a virtual machine that contains an implementation of the FreezeML system described in the paper. The artifact also contains a collection of examples presented in the paper so that the results can be easily reproduced.
Securing smart contract with runtime validation
作者: Li, Ao and Choi, Jemin Andrew and Long, Fan
关键词: compiler, runtime validation, smart contract
Abstract
We present Solythesis, a source to source Solidity compiler which takes a smart contract code and a user specified invariant as the input and produces an instrumented contract that rejects all transactions that violate the invariant. The design of Solythesis is driven by our observation that the consensus protocol and the storage layer are the primary and the secondary performance bottlenecks of Ethereum, respectively. Solythesis operates with our novel delta update and delta check techniques to minimize the overhead caused by the instrumented storage access statements. Our experimental results validate our hypothesis that the overhead of runtime validation, which is often too expensive for other domains, is in fact negligible for smart contracts. The CPU overhead of Solythesis is only 0.1% on average for our 23 benchmark contracts.
Ethainter： A Smart Contract Security Analyzer for Composite Vulnerabilities
作者: Brent, Lexi and Grech, Neville and Lagouvardos, Sifis and Scholz, Bernhard and Smaragdakis, Yannis
关键词: Program Analysis, Smart Contracts
Abstract
The artifact is composed of: - A decompiler (modified Gigahorse) - Ethainter implementation - Data for recreating experiments
Behavioral simulation for smart contracts
作者: Beillahi, Sidi Mohamed and Ciocarlie, Gabriela and Emmi, Michael and Enea, Constantin
关键词: Blockchain, Refinement, Simulation, Smart contracts
Abstract
While smart contracts have the potential to revolutionize many important applications like banking, trade, and supply-chain, their reliable deployment begs for rigorous formal verification. Since most smart contracts are not annotated with formal specifications, general verification of functional properties is impeded. In this work, we propose an automated approach to verify unannotated smart contracts against specifications ascribed to a few manually-annotated contracts. In particular, we propose a notion of behavioral refinement, which implies inheritance of functional properties. Furthermore, we propose an automated approach to inductive proof, by synthesizing simulation relations on the states of related contracts. Empirically, we demonstrate that behavioral simulations can be synthesized automatically for several ubiquitous classes like tokens, auctions, and escrow, thus enabling the verification of unannotated contracts against functional specifications.
Multi-modal synthesis of regular expressions
作者: Chen, Qiaochu and Wang, Xinyu and Ye, Xi and Durrett, Greg and Dillig, Isil
关键词: Program Synthesis, Programming by Example, Programming by Natural Languages, Regular Expression
Abstract
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 % accuracy whereas the NLP-only and PBE-only baselines achieve 43 % and 26 % respectively. We also compare our proposed PBE engine against an adaptation of AlphaRegex, a state-of-the-art regex synthesis tool, and show that our proposed PBE engine is an order of magnitude faster, even if we adapt the search algorithm of AlphaRegex to leverage the sketch. Finally, we conduct a user study involving 20 participants and show that users are twice as likely to successfully come up with the desired regex using Regel compared to without it.
Lobster - Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting
作者: Lee, DongKwon and Lee, Woosuk and Oh, Hakjoo and Yi, Kwangkeun
关键词: Homomorphic encryption circuit, Program synthesis, Term rewriting
Abstract
Lobster optimizes homomorphic encryption circuit using aggressive rewrite rules automatically learned by program synthesis technique.
Polca： a tool for learning cache replacement policies as automata models
作者: Vila, Pepe and Ganty, Pierre and Guarnieri, Marco and K"{o
关键词: automata, cache, cachequery, learning, learnlib, program synthesis, replacement policy, sketch
Abstract
Polca implements the automata interface to LearnLib for automatically learning cache replacement policies. It can be connected to CacheQuery for directly interacting with hardware caches. It also contains the learned models, instructions to generate them, and the templates (and results) for (from) the program synthesis evaluation.
Replication package for： HipHop.js： (A)Synchronous Reactive Web Programming
作者: Berry, G'{e
关键词: JavaScript, Reactive Programming, Synchronous Programming, Web Programming
Abstract
Our artifact consists of:
The current HipHop.js implementation, which you can either download fully constructed in the docker file available from the PLDI artifact site (see Part 1 below) or entirely rebuild from the public Hop/HipHop sources files (see Part 3) if you find the 1.3 GB docker file too big or if you want to do it yourself. Once the docker image is downloaded or built, you can validate it by running the standard HipHop implementation test suite (see Part 4).
The implementation and step-by-step simulation of our Lisinopril medical prescription application described in the paper (Part 2 below). The main Lisinopril HipHop reactive module is exacly the one in the paper. The complete source files can be accessed within the docker image or dowloaded from the web.
EVA： an encrypted vector arithmetic language and compiler for efficient homomorphic computation
作者: Dathathri, Roshan and Kostova, Blagovesta and Saarikivi, Olli and Dai, Wei and Laine, Kim and Musuvathi, Madan
关键词: Homomorphic encryption, compiler, neural networks, privacy-preserving machine learning
Abstract
Fully-Homomorphic Encryption (FHE) offers powerful capabilities by enabling secure offloading of both storage and computation, and recent innovations in schemes and implementations have made it all the more attractive. At the same time, FHE is notoriously hard to use with a very constrained programming model, a very unusual performance profile, and many cryptographic constraints. Existing compilers for FHE either target simpler but less efficient FHE schemes or only support specific domains where they can rely on expert-provided high-level runtimes to hide complications. This paper presents a new FHE language called Encrypted Vector Arithmetic (EVA), which includes an optimizing compiler that generates correct and secure FHE programs, while hiding all the complexities of the target FHE scheme. Bolstered by our optimizing compiler, programmers can develop efficient general-purpose FHE applications directly in EVA. For example, we have developed image processing applications using EVA, with a very few lines of code. EVA is designed to also work as an intermediate representation that can be a target for compiling higher-level domain-specific languages. To demonstrate this, we have re-targeted CHET, an existing domain-specific compiler for neural network inference, onto EVA. Due to the novel optimizations in EVA, its programs are on average 5.3\texttimes{
Real arithmetic package and code to check floating point precision
作者: Boehm, Hans-J.
关键词: accuracy checking, comparison, decidability, floating point, real numbers
Abstract
Source code and instructions to run the floating point accuracy test described in the paper. This includes the real arithmetic package, with the described comparison support, and an updated version of the previously described underlying recursive reals package (which diverges on exact comparison of equal real numbers). The real arithmetic package is very similar to that currently used by Google's Android calculator.
Responsive Parallelism with Futures and State - Software Artifact
作者: Muller, Stefan K. and Singer, Kyle and Goldstein, Noah and Acar, Umut A. and Agrawal, Kunal and Lee, I-Ting Angelina
关键词: futures, Interactive Cilk, priority inversion, responsiveness, task parallelism, type systems
Abstract
This artifact contains a prototype of the I-Cilk runtime for scheduling parallel code with task priorities, a C++ type system for preventing priority inversions, and benchmarks using both of the former. The artifact demonstrates the practicality of the type system in implementing performant parallel code that uses task priorities. The prototype I-Cilk runtime is in the interactive-cilk directory, with the type system located in interactive-cilk/include/cilk/cilk_priority.h.
SympleGraph： distributed graph processing with precise loop-carried dependency guarantee
作者: Zhuo, Youwei and Chen, Jingji and Luo, Qinyi and Wang, Yanzhi and Yang, Hailong and Qian, Depei and Qian, Xuehai
关键词: big data, compilers, graph algorithms, graph analytics
Abstract
Graph analytics is an important way to understand relationships in real-world applications. At the age of big data, graphs have grown to billions of edges. This motivates distributed graph processing. Graph processing frameworks ask programmers to specify graph computations in user- defined functions (UDFs) of graph-oriented programming model. Due to the nature of distributed execution, current frameworks cannot precisely enforce the semantics of UDFs, leading to unnecessary computation and communication. In essence, there exists a gap between programming model and runtime execution. This paper proposes SympleGraph, a novel distributed graph processing framework that precisely enforces loop-carried dependency, i.e., when a condition is satisfied by a neighbor, all following neighbors can be skipped. SympleGraph instruments the UDFs to express the loop-carried dependency, then the distributed execution framework enforces the precise semantics by performing dependency propagation dynamically. Enforcing loop-carried dependency requires the sequential processing of the neighbors of each vertex distributed in different nodes. Therefore, the major challenge is to enable sufficient parallelism to achieve high performance. We propose to use circulant scheduling in the framework to allow different machines to process disjoint sets of edges/vertices in parallel while satisfying the sequential requirement. It achieves a good trade-off between precise semantics and parallelism. The significant speedups in most graphs and algorithms indicate that the benefits of eliminating unnecessary computation and communication overshadow the reduced parallelism. Communication efficiency is further optimized by 1) selectively propagating dependency for large-degree vertices to increase net benefits; 2) double buffering to hide communication latency. In a 16-node cluster, SympleGraph outperforms the state-of-the-art system Gemini and D-Galois on average by 1.42\texttimes{
PMEvo： portable inference of port mappings for out-of-order processors by evolutionary optimization
作者: Ritter, Fabian and Hack, Sebastian
关键词: evolutionary algorithm, port mapping, processor reverse engineering
Abstract
Achieving peak performance in a computer system requires optimizations in every layer of the system, be it hardware or software. A detailed understanding of the underlying hardware, and especially the processor, is crucial to optimize software. One key criterion for the performance of a processor is its ability to exploit instruction-level parallelism. This ability is determined by the port mapping of the processor, which describes the execution units of the processor for each instruction. Processor manufacturers usually do not share the port mappings of their microarchitectures. While approaches to automatically infer port mappings from experiments exist, they are based on processor-specific hardware performance counters that are not available on every platform. We present PMEvo, a framework to automatically infer port mappings solely based on the measurement of the execution time of short instruction sequences. PMEvo uses an evolutionary algorithm that evaluates the fitness of candidate mappings with an analytical throughput model formulated as a linear program. Our prototype implementation infers a port mapping for Intel’s Skylake architecture that predicts measured instruction throughput with an accuracy that is competitive to existing work. Furthermore, it finds port mappings for AMD’s Zen+ architecture and the ARM Cortex-A72 architecture, which are out of scope of existing techniques.
PMThreads： Persistent Memory Threads Harnessing Versioned Shadow Copies (Artifact)
作者: Wu, Zhenwei and Lu, Kai and Nisbet, Andrew and Zhang, Wenzhe and Luj'{a
关键词: memory persistence, non-volatile memory
Abstract
This is the artifact for the paper "PMThreads: Persistent Memory Threads Harnessing Versioned Shadow Copies", which is set to be published in PLDI 2020. The artifact contains code, and a Dockerfile for assembling a Docker image with all required dependencies to run the code and reproduce the paper results.
SCAF： A Speculation-Aware Collaborative Dependence Analysis Framework
作者: Apostolakis, Sotiris and Xu, Ziyang and Tan, Zujun and Chan, Greg and Campanoni, Simone and August, David I.
关键词: compilers, program analysis, speculation
Abstract
Artifact archive for the artifact evaluation of the PLDI 2020 paper, titled "SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework". It contains a Dockerfile along with relevant to this paper software to create a docker image used to reproduce the evaluation results presented in this PLDI 2020 paper.
Artifact for “Scalable Validation of Binary Lifters”
作者: Dasgupta, Sandeep and Dinesh, Sushant and Venkatesh, Deepan and Adve, Vikram S. and Fletcher, Christopher W.
关键词: compiler-optimization, detecting-bugs, evaluation, formal-semantics, graph-matching, language-semantics, llvm-ir, mcsema, pldi, reproducing-bugs, reverse-engineering, symbolic-execution-engine, symbolic-summaries, translation-validation, validation, verification-conditions, verification-queries, virtualbox, x86-64
Abstract
Snapshot of peer-evaluated artifact corresponding to the published conference paper [1].
[1] Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S. Adve, and Christopher W. Fletcher 2020. Scalable Validation of Binary Lifters. In Proceedings of the 2020 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM. https://doi.org/10.1145/3385412.3385964
Polynomial invariant generation for non-deterministic recursive programs
作者: Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar and Goharshady, Ehsan Kafshdar
关键词: Invariant generation, Polynomial programs, Positivstellensaetze
Abstract
We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set. On the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previous complete method (Kapur, ACA 2004) is doubly-exponential. Even when restricted to linear invariants, the best previous complexity for complete invariant generation is exponential (Colon et al, CAV 2003). On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. We demonstrate the applicability of our approach by providing experimental results on several academic benchmarks. To the best of our knowledge, the only previous invariant generation method that provides completeness guarantees for invariants consisting of polynomial inequalities is (Kapur, ACA 2004), which relies on quantifier elimination and cannot even handle toy programs such as our running example.
Artifact for “Templates and Recurrences： Better Together”
作者: Breck, Jason and Cyphert, John and Kincaid, Zachary and Reps, Thomas
关键词: Invariant generation, Recurrence relation
Abstract
This is the artifact for the PLDI 2020 paper, "Templates and Recurrences: Better Together." The artifact is a virtual machine in OVA (Open Virtualization Archive) format. Its operating system is Ubuntu 18. The virtual machine contains an installation of the CHORA static analysis tool, which is the implementation of the technique described by the associated paper. The virtual machine also contains the benchmark programs that were used in the experiments of the associated paper, along with a script that is designed to replicate the paper's experimental results. The virtual machine has a user account with name "chorauser" and password "chorapassword", and allows login via graphical user interface, or via SSH on port 22.
Artifact for Article： First-Order Quantified Separators
作者: Koenig, Jason R. and Padon, Oded and Immerman, Neil and Aiken, Alex
关键词: first-order logic, invariant inference, software verification
Abstract
This artifact contains implementations of the separation algorithm from Section 5, the IC3/PDR implementation from Section 6.3, and the evaluation data from Section 7. This artifact can be used to both reproduce the results of the article as well as run these algorithms on novel distributed protocols.
Validating SMT solvers via semantic fusion
作者: Winterer, Dominik and Zhang, Chengyu and Su, Zhendong
关键词: Fuzz testing, SMT solvers, Semantic fusion
Abstract
We introduce Semantic Fusion, a general, effective methodology for validating Satisfiability Modulo Theory (SMT) solvers. Our key idea is to fuse two existing equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas into a new formula that combines the structures of its ancestors in a novel manner and preserves the satisfiability by construction. This fused formula is then used for validating SMT solvers. We realized Semantic Fusion as YinYang, a practical SMT solver testing tool. During four months of extensive testing, YinYang has found 45 confirmed, unique bugs in the default arithmetic and string solvers of Z3 and CVC4, the two state-of-the-art SMT solvers. Among these, 41 have already been fixed by the developers. The majority (29/45) of these bugs expose critical soundness issues. Our bug reports and testing effort have been well-appreciated by SMT solver developers.
PositDebug Artifact： Debugging and Detecting Numerical Errors in Computation with Posits
作者: Chowdhary, Sangeeta and Lim, Jay P. and Nagarakatte, Santosh
关键词: cancellation, CORDIC, floating point, FPSanitizer, numerical errors, PositDebug, posits
Abstract
This artifact contains a shadow execution framework for finding numerical errors in applications using both posits and floating point. The prototype for posits is called PositDebug and the prototype for floating point programs is called FPSsanitizer.
Efficient Predictive Race Detection
作者: Roemer, Jake and Gen\c{c
关键词: Data race detection, dynamic predictive analysis
Abstract
This is the artifact submitted for the Artifact Evaluation process for the PLDI 2020 paper "SmartTrack: Efficient Predictive Race Detection" by Jake Roemer, Kaan Gen\c{c
Replication Package for Article： Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs
作者: Qin, Boqin and Chen, Yilun and Yu, Zeming and Song, Linhai and Zhang, Yiying
关键词: Bug Study, Concurrency Bug, Memory Bug, Rust
Abstract
The artifact is to support the data in our paper with programs. It contains five directories related to the corresponding sections in the paper. section-2-background-and-related-work contains scripts and raw data to plot Fig. 1 and Fig. 2. section-4-unsafe-usages contains a bench testing for safe and unsafe code, and a script to count unsafe statistics. section-5-memory-safety-issues contains the fix commits of our studied memory bugs, and our reproduced memory bugs. section-6-thread-safety-issues contains the fix commits of our studied blocking and non-blocking bugs, our reproduced blocking and non-blocking bugs, and the code to count cases where locks are manually dropped. section-7-bug-detection contains our detection tools for use-after-free and double-lock.
Fast graph simplification for interleaved Dyck-reachability
作者: Li, Yuanbo and Zhang, Qirun and Reps, Thomas
关键词: CFL-Reachability, Static Analysis
Abstract
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.
Artifact： Static Analysis of Enterprise Applications： Frameworks and Caches, the Elephants in the Room
作者: Antoniadis, Anastasios and Filippakis, Nikos and Krishnan, Paddy and Ramesh, Raghavendra and Allen, Nicholas and Smaragdakis, Yannis
关键词: Java EE, points-to analysis, static analysis
Abstract
This artifact contains the evaluation benchmarks for the paper "Static Analysis of Java Enterprise Applications: Frameworks and Caches, the Elephants in the Room" , accepted in the Programming Language Design and Implementation Conference (PLDI'20).
Link to paper preprint
Abstract:
Enterprise applications are a major success domain of Java, and Java
is the default setting for much modern static analysis research. It
would stand to reason that high-quality static analysis of Java
enterprise applications would be commonplace, but this is far from
true. Major analysis frameworks feature virtually no support for
enterprise applications and offer analyses that are woefully
incomplete and vastly imprecise, when at all scalable.
In this work, we present two techniques for drastically enhancing
the completeness and precision of static analysis for Java
enterprise applications. The first technique identifies
domain-specific concepts underlying all enterprise application
frameworks, captures them in an extensible, declarative form, and
achieves modeling of components and entry points in a largely
framework-independent way. The second technique offers precision and
scalability via a sound-modulo-analysis modeling of standard data
structures.
In realistic enterprise applications (an order of magnitude larger than
prior benchmarks in the literature) our techniques achieve high degrees of
completeness (on average more than 4x higher than conventional techniques) and
speedups of about 6x compared to the most precise conventional analysis, with
higher precision on multiple metrics. The result is JackEE, an
enterprise analysis framework that can offer precise, high-completeness
static modeling of realistic enterprise applications.
Automated derivation of parametric data movement lower bounds for affine programs
作者: Olivry, Auguste and Langou, Julien and Pouchet, Louis-No"{e
关键词: Affine programs, Data access complexity, I/O lower bounds, Static analysis
Abstract
Researchers and practitioners have for long worked on improving the computational complexity of algorithms, focusing on reducing the number of operations needed to perform a computation. However the hardware trend nowadays clearly shows a higher performance and energy cost for data movements than computations: quality algorithms have to minimize data movements as much as possible. The theoretical operational complexity of an algorithm is a function of the total number of operations that must be executed, regardless of the order in which they will actually be executed. But theoretical data movement (or, I/O) complexity is fundamentally different: one must consider all possible legal schedules of the operations to determine the minimal number of data movements achievable, a major theoretical challenge. I/O complexity has been studied via complex manual proofs, e.g., refined from Ω(n3/√S) for matrix-multiply on a cache size S by Hong & Kung to 2n3/√S by Smith et al. While asymptotic complexity may be sufficient to compare I/O potential between broadly different algorithms, the accuracy of the reasoning depends on the tightness of these I/O lower bounds. Precisely, exposing constants is essential to enable precise comparison between different algorithms: for example the 2n3/√S lower bound allows to demonstrate the optimality of panel-panel tiling for matrix-multiplication. We present the first static analysis to automatically derive non-asymptotic parametric expressions of data movement lower bounds with scaling constants, for arbitrary affine computations. Our approach is fully automatic, assisting algorithm designers to reason about I/O complexity and make educated decisions about algorithmic alternatives.
Automatic generation of efficient sparse tensor format conversion routines
作者: Chou, Stephen and Kjolstad, Fredrik and Amarasinghe, Saman
关键词: attribute query language, coordinate remapping notation, sparse tensor algebra, sparse tensor assembly, sparse tensor conversion, sparse tensor formats
Abstract
This paper shows how to generate code that efficiently converts sparse tensors between disparate storage formats (data layouts) such as CSR, DIA, ELL, and many others. We decompose sparse tensor conversion into three logical phases: coordinate remapping, analysis, and assembly. We then develop a language that precisely describes how different formats group together and order a tensor’s nonzeros in memory. This lets a compiler emit code that performs complex remappings of nonzeros when converting between formats. We also develop a query language that can extract statistics about sparse tensors, and we show how to emit efficient analysis code that computes such queries. Finally, we define an abstract interface that captures how data structures for storing a tensor can be efficiently assembled given specific statistics about the tensor. Disparate formats can implement this common interface, thus letting a compiler emit optimized sparse tensor conversion code for arbitrary combinations of many formats without hard-coding for any specific combination. Our evaluation shows that the technique generates sparse tensor conversion routines with performance between 1.00 and 2.01\texttimes{
Replication package for OOElala： Order-of-Evaluation Based Alias Analysis for Compiler Optimization
作者: Phulia, Ankush and Bhagee, Vaibhav and Bansal, Sorav
关键词: Alias Analysis, Clang, Compiler Optimization, LLVM, Polybench, SPEC CPU 2017, Undefined behaviour
Abstract
This artifact contains the implementation for the algorithm described in the paper, OOElala: Order-of-Evaluation Based Alias Analysis for Compiler Optimization, accepted at PLDI 2020.
Terminology
- We use
OOElala,ooelalaandclang-unseqinterchangeably to refer to the tool/binary which we have implemented and produced as a part of this work. <artifact-home>refers to/home/$USER/ooelala-project
Structure of the artifact
This artifact directory is structured into the following subdirectories, each of which is described subsequently:
- litmus_tests - This directory contains the implementation of the two examples, which have been introduced in Section 1.1 of the paper, to spearhead the discussion about the key idea of the paper. The makefile is used to run these two examples, as described in detail in the later sections.
- array_min_max - This subdirectory contains the code, for the first example, on the left of the figure.
- nested_loop - This subdirectory contains the code for an example, which isolates the kernel initialization code described in the second image on the right. The implementation captures the basic idea for the SPEC 2017 example, as discussed in section 1.1 of the paper.
- ooelala - This directory contains the source code for our tool, OOELala, which has been implemented over clang/llvm 8.0.0.
- src - This sub-directory contains the source code for the optimizing compiler implementation which includes the AST analysis to identify the must-not-alias predicates and the Alias Analysis which utilises the must-not-alias information to enable further optimisations. This has been added as a sub-module and the specific implementation details can be found in the commit history and commit messages of this sub-module.
- ubsan - This sub-directory contains the source code for the implementation of the UB Sanitizer which uses the must-not-alias predicates generated after the AST analysis to implement the runtime checks. This has been added as a sub-module and the specific implementation details can be found in the commit history and commit messages of this sub-module.
- spec - This directory contains the resources which we use to run the SPEC CPU 2017 benchmarks, with clang and OOELala.
- configs - This subdirectory contains the config files
clang-unseq.cfgandclang.cfg, which are used when we build and run the SPEC CPU 2017 suite with OOELala and clang respectively. Additionally, this directory also contains config filesclang-ubsan.cfgandclang-ubsan-unseq.cfg, which are used to specify that SPEC should be built and run with clang and OOELala respectively, with UB Sanitizer checks enabled and no optimisations. - makefiles - This subdirectory contains the makefiles, which are used to compile and run specific SPEC benchmarks or generate object/LLVM files for some specific source files, in some specific benchmarks. These have been used to identify the patterns discussed in figure 2 of the paper. For running these on SPEC refrate inputs refer to
Readme.mdin the subdirectory. - scripts - This subdirectory contains the scripts which are used to build and run the SPEC 2017 benchmarks and generate the performance numbers presented in table 6 of the paper. This also contains the post processing python script which is used to generate the summary of the aliasing stats, which are presented in Table 5 of the paper. The list of scripts and their functionality is described in the Readme.md file present in this subdirectory.
- configs - This subdirectory contains the config files
- polybench - This directory contains the resources which we use to run the Polybench benchmark suite, with clang and OOELala
- common - This subdirectory contains the Polybench header file which needs to be included in the benchmarks.
- scripts - This subdirectory contains the scripts used to build and run the Polybench benchmarks to obtain the speedups listed in Table 4 of the paper. Comparisons between various compilers have been drawn.
- selected_benchmarks - This represents the selected subset of benchmarks which we have annotated with custom
RESTRICTmacro predicates (corresponding toCANT_ALIASused in the paper), used to provide the additional aliasing information, but in no way modifying the behaviour of the program
- sample_outputs - This directory contains a set of sample outputs which are obtained on running the SPEC CPU 2017 and the polybench benchmarks. These can be used by the developers to verify the output format
- spec - This contains the results and stats obtained for a sample run of SPEC CPU 2017, with clang and clang-unseq
- polybench - This contains the results and stats obtained for a sample run of Polybench, with clang and clang-unseq
- CANT_ALIAS.md - This is a tutorial which discusses the CANT_ALIAS predicate described in the paper. It outlines the use of the macro and the subtleties associated with that.
Artifact for “Effective function merging in the SSA form”
作者: Rocha, Rodrigo C. O. and Petoumenos, Pavlos and Wang, Zheng and Cole, Murray and Leather, Hugh
关键词: code size, compiler optimization, function merging, link-time optimization, LTO
Abstract
This artifact includes a modified version of the open-source LLVM compiler framework. It includes a prototype implementation of our novel function merging technique, called SalSSA. It also includes an implementation of the state-of-the-art function merging technique. This artifact also provides Makefile scripts to run spec2006 using these function merging techniques and scripts to compare them.
Proving almost-sure termination by omega-regular decomposition
作者: Chen, Jianhui and He, Fei
关键词: Almost-Sure Termination, Omega-Regular Languages, Probabilistic Programs, Ranking Supermartingales
Abstract
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.
lpsi-artifact
作者: Gehr, Timon and Steffen, Samuel and Vechev, Martin
关键词: Exact, Higher-order, Probabilistic Programming
Abstract
Artifact for PLDI'20 paper "λPSI: Exact Inference for Higher-Order Probabilistic Programs".
Replication package for Article： Reactive Probabilistic Programming
作者: Baudart, Guillaume and Mandel, Louis and Atkinson, Eric and Sherman, Benjamin and Pouzet, Marc and Carbin, Michael
关键词: Benchmark, Compiler, Delayed sampling, Inference, Probabilistic programming, Runtime, Sequential Monte Carlo, Synchronous programming
Abstract
This is the artifact of the PLDI 2020 paper Reactive Probabilistic Programming by Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. The archive contains - pldi2020.pdf: Paper with appendices - README.md: Details on how the code is linked to the paper and how to run the code and the benchmarks - ProbZelus-PLDI20.ova: Linux image in the Open Virtualization Format with the ProbZelus compiler and benchmarks - LICENSE.txt: ProbZelus license.
The artifact can be used to check the implementation of the algorithms presented in the paper and to reproduce the evaluation.
Pitchfork-Angr
作者: Cauligi, Sunjay and Disselkoen, Craig and Gleissenthall, Klaus v. and Tullsen, Dean and Stefan, Deian and Rezk, Tamara and Barthe, Gilles
关键词: spectre, speculative execution, static analysis, symbolic execution
Abstract
Pitchfork is a static analysis tool, built on angr (https://github.com/angr/angr), which performs speculative symbolic execution. That is, it not only executes the "correct" or "sequential" paths of a program, but also the "mispredicted" or "speculative" paths, subject to some speculation window size. Pitchfork finds paths where secret data is used in either address calculations or branch conditions (and thus leaked), even speculatively - these paths represent Spectre vulnerabilities. Pitchfork covers Spectre v1, Spectre v1.1, and Spectre v4.
Gillian, Part I： A Multi-language Platform for Symbolic Execution
作者: Fragoso Santos, Jos'{e
关键词: bounded verification, bug-finding, C, JavaScript, parametric semantics, Symbolic execution
Abstract
This artifact contains the Gillian platform, as it was for the submission of the corresponding PLDI'20 paper.
Note: This artifact is licensed under the GNU General Public License v3.0 and can only be used for academic purposes. The Gillian platform itself is not licensed under the same license.
Efficient handling of string-number conversion
作者: Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Chen, Yu-Fang and Diep, Bui Phi and Dolby, Julian and Jank\r{u
关键词: Automata, Formal Verification, String Solver
Abstract
String-number conversion is an important class of constraints needed for the symbolic execution of string-manipulating programs. In particular solving string constraints with string-number conversion is necessary for the analysis of scripting languages such as JavaScript and Python, where string-number conversion is a part of the definition of the core semantics of these languages. However, solving this type of constraint is very challenging for the state-of-the-art solvers. We propose in this paper an approach that can efficiently support both string-number conversion and other common types of string constraints. Experimental results show that it significantly outperforms other state-of-the-art tools on benchmarks that involves string-number conversion.
Software Artifact for NV： An Intermediate Language for Verification of Network Control Planes
作者: Giannarakis, Nick and Loehr, Devon and Beckett, Ryan and Walker, David
关键词: intermediate verification language, network simulation, network verification, static analysis
Abstract
The artifact contains a VirtualBox VM image with the source code and the binary for the NV framework (the simulator, SMT verifier, etc.). Also included is a modified version of Batfish that can translate router configurations to NV source files.
Detecting network load violations for distributed control planes
作者: Subramanian, Kausik and Abhashkumar, Anubhavnidhi and D’Antoni, Loris and Akella, Aditya
关键词: Abstract Representation, Fault Tolerance, Quantitative Verification, Routing Protocols
Abstract
One of the major challenges faced by network operators pertains to whether their network can meet input traffic demand, avoid overload, and satisfy service-level agreements. Automatically verifying if no network links are overloaded is complicated—requires modeling frequent network failures, complex routing and load-balancing technologies, and evolving traffic requirements. We present QARC, a distributed control plane abstraction that can automatically verify whether a control plane may cause link-load violations under failures. QARC is fully automatic and can help operators program networks that are more resilient to failures and upgrade the network to avoid violations. We apply QARC to real datacenter and ISP networks and find interesting cases of load violations. QARC can detect violations in under an hour.
Compiler-directed soft error resilience for lightweight GPU register file protection
作者: Kim, Hongjune and Zeng, Jianping and Liu, Qingrui and Abdel-Majeed, Mohammad and Lee, Jaejin and Jung, Changhee
关键词: ECC, GPU, Resilience
Abstract
This paper presents Penny, a compiler-directed resilience scheme for protecting GPU register files (RF) against soft errors. Penny replaces the conventional error correction code (ECC) based RF protection by using less expensive error detection code (EDC) along with idempotence based recovery. Compared to the ECC protection, Penny can achieve either the same level of RF resilience yet with significantly lower hardware costs or stronger resilience using the same ECC due to its ability to detect multi-bit errors when it is used solely for detection. In particular, to address the lack of store buffers in GPUs, which causes both checkpoint storage overwriting and the high cost of checkpointing stores, Penny provides several compiler optimizations such as storage coloring and checkpoint pruning. Across 25 benchmarks, Penny causes only ≈3% run-time overhead on average.
Adaptive low-overhead scheduling for periodic and reactive intermittent execution
作者: Maeng, Kiwan and Lucia, Brandon
关键词: energy-harvesting, intermittent computing
Abstract
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.
Faster general parsing through context-free memoization
作者: Herman, Grzegorz
关键词: Earley, GLL, GLR, context-free, generalized parsing, memoization
Abstract
We present a novel parsing algorithm for all context-free languages. The algorithm features a clean mathematical formulation: parsing is expressed as a series of standard operations on regular languages and relations. Parsing complexity w.r.t. input length matches the state of the art: it is worst-case cubic, quadratic for unambiguous grammars, and linear for LR-regular grammars. What distinguishes our approach is that parsing can be implemented using only immutable, acyclic data structures. We also propose a parsing optimization technique called context-free memoization. It allows handling an overwhelming majority of input symbols using a simple stack and a lookup table, similarly to the operation of a deterministic LR(1) parser. This allows our proof-of-concept implementation to outperform the best current implementations of common generalized parsing algorithms (Earley, GLR, and GLL). Tested on a large Java source corpus, parsing is 3–5 times faster, while recognition—35 times faster.
Zippy LL(1) parsing with derivatives
作者: Edelmann, Romain and Hamza, Jad and Kun\v{c
关键词: Derivatives, Formal proof, LL(1), Parsing, Zipper
Abstract
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.
Debug information validation for optimized code
作者: Li, Yuanbo and Ding, Shuo and Zhang, Qirun and Italiano, Davide
关键词: Debug Information, Optimizing Compilers
Abstract
Almost all modern production software is compiled with optimization. Debugging optimized code is a desirable functionality. For example, developers usually perform post-mortem debugging on the coredumps produced by software crashes. Designing reliable debugging techniques for optimized code has been well-studied in the past. However, little is known about the correctness of the debug information generated by optimizing compilers when debugging optimized code. Optimizing compilers emit debug information (e.g., DWARF information) to support source code debuggers. Wrong debug information causes debuggers to either crash or to display wrong variable values. Existing debugger validation techniques only focus on testing the interactive aspect of debuggers for dynamic languages (i.e., with unoptimized code). Validating debug information for optimized code raises some unique challenges: (1) many breakpoints cannot be reached by debuggers due to code optimization; and (2) inspecting some arbitrary variables such as uninitialized variables introduces undefined behaviors. This paper presents the first generic framework for systematically testing debug information with optimized code. We introduce a novel concept called actionable program. An actionable program P⟨ s, v⟩ contains a program location s and a variable v to inspect. Our key insight is that in both the unoptimized program P⟨ s,v⟩ and the optimized program P⟨ s,v⟩′, debuggers should be able to stop at the program location s and inspect the value of the variable v without any undefined behaviors. Our framework generates actionable programs and does systematic testing by comparing the debugger output of P⟨ s, v⟩′ and the actual value of v at line s in P⟨ s, v⟩. We have applied our framework to two mainstream optimizing C compilers (i.e., GCC and LLVM). Our framework has led to 47 confirmed bug reports, 11 of which have already been fixed. Moreover, in three days, our technique has found 2 confirmed bugs in the Rust compiler. The results have demonstrated the effectiveness and generality of our framework.
Yogo
作者: Premtoon, Varot and Koppel, James and Solar-Lezama, Armando
关键词: code search, equational reasoning
Abstract
Docker container with an executable copy of Yogo, and source code for the Haskell portion (frontend)
Proving data-poisoning robustness in decision trees
作者: Drews, Samuel and Albarghouthi, Aws and D’Antoni, Loris
关键词: Abstract Interpretation, Adversarial Machine Learning, Decision Trees, Poisoning, Robustness
Abstract
Machine learning models are brittle, and small changes in the training data can result in different predictions. We study the problem of proving that a prediction is robust to data poisoning, where an attacker can inject a number of malicious elements into the training set to influence the learned model. We target decision-tree models, a popular and simple class of machine learning models that underlies many complex learning techniques. We present a sound verification technique based on abstract interpretation and implement it in a tool called Antidote. Antidote abstractly trains decision trees for an intractably large space of possible poisoned datasets. Due to the soundness of our abstraction, Antidote can produce proofs that, for a given input, the corresponding prediction would not have changed had the training set been tampered with or not. We demonstrate the effectiveness of Antidote on a number of popular datasets.
Replication Package for Article： A Study of the Learnability of Relational Properties： Model Counting Meets Machine Learning (MCML) - PLDI 2020
作者: Usman, Muhammad and Wang, Wenxi and Vasic, Marko and Wang, Kaiyuan and Vikalo, Haris and Khurshid, Sarfraz
关键词: Alloy, ApproxMC, machine learning, model counting, ProjMC, Relational Properties, SAT solving
Abstract
The artifact contains datasets and code which were used to compute results for this paper (A Study of the Learnability of Relational Properties: Model Counting Meets Machine Learning (MCML) - PLDI 2020). Detailed instructions can be found in README.txt file.
Reproduction Package for Article： Learning Fast and Precise Numerical Analysis
作者: He, Jingxuan and Singh, Gagandeep and P"{u
关键词: Abstract interpretation, Machine learning, Numerical domains, Performance optimization.
Abstract
This material is the artifact for paper "Learning Fast and Precise Numerical Analysis" at PLDI 2020. It contains raw data for main experiments, benchmarks, full source code, and scripts for reproducing main experiments.
Artifact for article： Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
作者: Hu, Qinheping and Cyphert, John and D’Antoni, Loris and Reps, Thomas
关键词: program synthesis, syntax guided synthesis, unrealizability
Abstract
This artifact contains Nay, a synthesizer which can prove unrealizability of unrealizable SyGuS problems. For detail can be found in this paper:https://arxiv.org/abs/2004.00878
Artifact for paper “Question Selection for Interactive Program Synthesis”
作者: Ji, Ruyi and Liang, Jingjing and Xiong, Yingfei and Zhang, Lu and Hu, Zhenjiang
关键词: Interaction, Program Synthesis
Abstract
This artifact is comprised of the appendix, source code and experiment scripts of paper "Question Selection for Interactive Program Synthesis". Readers can use them to reproduce the experiment results listed in our paper.
DryadSynth： Release as PLDI 2020 Artifact： Reconciling Enumerative and Deductive Program Synthesis
作者: Huang, Kangjing and Qiu, Xiaokang and Shen, Peiyuan and Wang, Yanjun
关键词: deductive synthesis, divide-and-conquer, enumerative synthesis, syntax-guided synthesis
Abstract
DryadSynth: A syntax-guided synthesizer
评论
