Artifact for “Modular Information Flow through Ownership”
作者: Crichton, Will and Patrignani, Marco and Agrawala, Maneesh and Hanrahan, Pat
关键词: information flow, modular program analysis, rust
Abstract
This is a Docker image that contains the codebase and evaluation scripts for our PLDI 2022 paper “Modular Information Flow Through Ownership”.
Replication package for “ANOSY： Approximated Knowledge Synthesis with Refinement Types for Declassification”
作者: Guria, Sankha Narayan and Vazou, Niki and Guarnieri, Marco and Parker, James
关键词: knowledge-based privacy, program synthesis, program verification, refinement types
Abstract
The artifact is a Docker image that contains all of the source code, benchmarks, and experiment harnesses used in the development of the paper (set-up and ready to run). The README contains instructions to reproduce results from the paper, as well as pointers for how to use, extend or modify the tool and benchmarks.
Hardening attack surfaces with formally proven binary format parsers
作者: Swamy, Nikhil and Ramananandro, Tahina and Rastogi, Aseem and Spiridonova, Irina and Ni, Haobin and Malloy, Dmitry and Vazquez, Juan and Tang, Michael and Cardona, Omar and Gupta, Arti
关键词: Formal proofs, Network formats, Parser generators
Abstract
With an eye toward performance, interoperability, or legacy concerns, low-level system software often must parse binary encoded data formats. Few tools are available for this task, especially since the formats involve a mixture of arithmetic and data dependence, beyond what can be handled by typical parser generators. As such, parsers are written by hand in languages like C, with inevitable errors leading to security vulnerabilities.
Addressing this need, we present EverParse3D, a parser generator for binary message formats that yields performant C code backed by fully automated formal proofs of memory safety, arithmetic safety, functional correctness, and even double-fetch freedom to prevent certain kinds of time-of-check/time-of-use errors. This allows systems developers to specify their message formats declaratively and to integrate correct-by-construction C code into their applications, eliminating several classes of bugs.
EverParse3D has been in use in the Windows kernel for the past year. Applied primarily to the Hyper-V network virtualization stack, the formats of nearly 100 different messages spanning four protocols have been specified in EverParse3D and the resulting formally proven parsers have replaced prior handwritten code. We report on our experience in detail.
Reproduction Package for Article “P4BID： Information Flow Control in P4”
作者: Grewal, Karuna and D’Antoni, Loris and Hsu, Justin
关键词: IFC, P4
Abstract
The artifact contains the main Readme.txt describing how to reproduce the evaluation presented in the paper using the baseline original P4c compiler and its IFC extension.
Artifact for “Turning Manual Concurrent Memory Reclamation into Automatic Reference Counting”
作者: Anderson, Daniel and Blelloch, Guy E. and Wei, Yuanhao
关键词: automatic memory reclamation, concurrency, lock-free, smart pointers
Abstract
This artifact contains our code and experiments as they were at the time of submission, and hence, at the time that they were validated by the artifact evaluation comittee. The latest version of our code can always be obtained from here. If you wish to build on our code for your own research, we highly recommend obtaining the latest version.
Note that this artifact does not contain the commercial just::threads library, which we compare with in Figure 13 of our paper, due to copyright. This artifact is still able to plot Figure 13, but without the line for just::threads.
[PLDI’22 Artifact] #132 Low-Latency, High-Throughput Garbage Collection
作者: Zhao, Wenyu and Blackburn, Stephen M. and McKinley, Kathryn S.
关键词: Garbage collection, Reference counting
Abstract
Artifact for PLDI 2022 paper: Low-Latency, High-Throughput Garbage Collection
Please check https://github.com/wenyuzhao/lxr-pldi-2022-artifact/blob/main/README.md for instructions on building and evaluating the artifact.
Please refer to https://github.com/wenyuzhao/mmtk-core/tree/lxr for the latest implementation.
Mako – A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters
作者: Ma, Haoran and Liu, Shi and Wang, Chenxi and Qiao, Yifan and Bond, Michael D. and Blackburn, Stephen M. and Kim, Miryung and Xu, Guoqing Harry
关键词: Disaggregation, Garbage Collection
Abstract
Mako contains the following three components:
- the Linux kernel with functionalities required by Mako - kernel
- the CPU-server Java Virtual Machine - Mako-CPU
- the Memory-server Java Virtual Machine - Mako-Memory
CPAM (Compressed Parallel Augmented Maps), an implementation of “PaC-Trees： Supporting Parallel and Compressed Purely-Functional Collections”
作者: Dhulipala, Laxman and Blelloch, Guy E. and Gu, Yan and Sun, Yihan
关键词: parallel data structures, purely-functional data structures, space-efficient data structures
Abstract
CPAM (Compressed Parallel Augmented Maps) is a parallel C++ library providing an implementation of the PaC-tree data structure, which is used to provide an interface for augmented maps that supports blocking of the nodes and applying user-defined compression schemes on the underlying data. CPAM’s interface is an extension of the interface from the PAM (Parallel Augmented Maps) library. CPAM is designed for maintaining ordered map data structures on potentially large and compressed datasets while efficiently answering queries (e.g., range queries) and performing dynamic updates on the data.
In the experiments, we use the interface in four examples: an inverted index, interval-queries, 2d range-queries, and graph processing. This artifact provides a self-contained docker image, includes examples and scripts for running the main experiments reported in the paper. It has also been designed to make it easy to try many other scenarios (e.g., different sizes, different datasets, different numbers of cores, and other operations described in the paper, but not reported in the experiments).
More details, examples, and discussion can be found in our paper.
Reproduction package of “Type-Directed Program Synthesis for RESTful APIs”
作者: Guo, Zheng and Cao, David and Tjong, Davin and Yang, Jean and Schlesinger, Cole and Polikarpova, Nadia
关键词: Program Synthesis, RESTful API, Type Inference
Abstract
This package includes a VMware virtual machine to reproduce results reported in the paper “Type-Directed Program Synthesis for RESTful APIs”.
Research Artifact for PLDI’22 Paper： Visualization Question Answering Using Introspective Program Synthesis
作者: Chen, Yanju and Yan, Xifeng and Feng, Yu
关键词: Machine Learning, Program Synthesis
Abstract
Research Artifact for PLDI’22 Paper: Visualization Question Answering Using Introspective Program Synthesis
WebRobot： web robotic process automation using interactive programming-by-demonstration
作者: Dong, Rui and Huang, Zhicheng and Lam, Ian Iong and Chen, Yan and Wang, Xinyu
关键词: Human-in-the-loop, Program Synthesis, Programming by Demonstration, Rewrite-based Synthesis, Robotic Process Automation, Web Automation
Abstract
It is imperative to democratize robotic process automation (RPA), as RPA has become a main driver of the digital transformation but is still technically very demanding to construct, especially for non-experts. In this paper, we study how to automate an important class of RPA tasks, dubbed web RPA, which are concerned with constructing software bots that automate interactions across data and a web browser. Our main contributions are twofold. First, we develop a formal foundation which allows semantically reasoning about web RPA programs and formulate its synthesis problem in a principled manner. Second, we propose a web RPA program synthesis algorithm based on a new idea called speculative rewriting. This leads to a novel speculate-and-validate methodology in the context of rewrite-based program synthesis, which has also shown to be both theoretically simple and practically efficient for synthesizing programs from demonstrations. We have built these ideas in a new interactive synthesizer called WebRobot and evaluate it on 76 web RPA benchmarks. Our results show that WebRobot automated a majority of them effectively. Furthermore, we show that WebRobot compares favorably with a conventional rewrite-based synthesis baseline implemented using egg. Finally, we conduct a small user study demonstrating WebRobot is also usable.
Reproduction Package for Synthesizing Analytical SQL Queries from Computation Demonstration
作者: Zhou, Xiangyu and Bodik, Rastislav and Cheung, Alvin and Wang, Chenglong
关键词: Program Synthesis, Query by Demonstration
Abstract
In this artifact, we included implementations of an analytical query synthesizer that uses enumerative synthesis algorithm and provenance abstraction for pruning the search space. In addition, we included the implementation of baselines synthesizers that use value abstraction, and type abstraction for experiments. Running the experimental scripts reproduces graph results in Synthesizing Analytical SQL Queries from Computation Demonstration. We also included 80 real-world benchmarks on solving analytical SQL problems with synthesizer.
Replication Package for Article： “Finding Typing Compiler Bugs”
作者: Chaliasos, Stefanos and Sotiropoulos, Thodoris and Spinellis, Diomidis and Gervais, Arthur and Livshits, Benjamin and Mitropoulos, Dimitris
关键词: compiler bugs, compiler testing, Groovy, Java, Kotlin, static typing
Abstract
The purpose of this artifact is to reproduce the results presented in the PLDI 2022 paper titled “Finding Typing Compiler Bugs”. The artifact contains the instructions, tool, and scripts to re-run the evaluation described in the paper. The artifact has the following structure:
- scripts/: This directory contains the scripts needed to re-run the experiments presented in our paper.
- data/: This is the directory that contains the precomputed results of our evaluation.
- database/bug_schema.sql: This is the database schema that contains the bugs discovered by our approach.
- database/bugdb.sqlite3: This is the sqlite3 database file corresponding to our bug database.
- database/bugs.json: This JSON file contains the bugs of database/bugdb.sqlite.
- hephaestus/: Contains the source code of the tool (provided as a git submodule) used for testing the compilers of Java, Kotlin, and Groovy. The name of our tool is Hephaestus.
- installation_scripts/: Contains helper scripts used to install all dependencies (e.g., compiler versions from SDKMAN).
- figures/: This directory will be used to save figure 8 of the paper.
- Dockerfile: The Dockerfile used to create a Docker image of our artifact. This image contains all data and dependencies.
IRDL： An IR Definition Language for SSA Compilers - PLDI 2022 Artifact Evaluation
作者: Fehr, Mathieu and Niu, Jeff and Riddle, River and Amini, Mehdi and Su, Zhendong and Grosser, Tobias
关键词: Compilers, Intermediate Representation, MLIR
Abstract
The artifact provides: * A python tool to extract an IRDL representation of the 28 dialects available in MLIR. Each dialect can be extracted in two variants: (1) contains constraints that can currently be enforced by our IRDL implementation, (2) contains additional IRDL constraints that demonstate the full expressiveness of IRDL. The reader can manually inspect the IRDL file of each dialect to get a visual impression of the IRDL files for typical MLIR dialects. * Scripts to reproduce all plots (except Figure 3) from the evaluation section of the paper. In particular, Figure 3 is not reproduced * An implementation of the key language constructs of IRDL for MLIR, which can be registered at runtime and supports the following constructs: * Definition of dialects * Operations with operands, results, and constraint variables * Types * The following type constraints: Any, AnyOf, equality constraint, base constraint, parametric constraint
Coq Development for the article Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency
作者: Cho, Minki and Lee, Sung-Hwan and Lee, Dongjae and Hur, Chung-Kil and Lahav, Ori
关键词: Compiler Optimizations, Operational Semantics, Relaxed Memory Concurrency
Abstract
This artifact contains Coq development of the promising semantics model extended with non-atomic accesses, the SEQ model and its soundness theorem, and the certified optimizer.
Artifact Package for “Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?”
作者: Choi, Wonhyuk and Finkbeiner, Bernd and Piskac, Ruzica and Santolucito, Mark
关键词: Program Synthesis, Reactive Synthesis, Syntax-Guided Synthesis
Abstract
Instructions to download and run the tool temos, the artifact for the paper “Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?”
Software Artifact for “Recursion Synthesis with Unrealizability Witnesses” Paper
作者: Farzan, Azadeh and Lette, Danya and Nicolet, Victor
关键词: Abstraction, Functional Programming, Invariants, Program Synthesis, Recursion, Unrealizability
Abstract
This software artifact is provided to support the experimental claims made in the PLDI’22 paper Recursion Synthesis with Unrealizability Witnesses. All the results given in the paper are reproducible modulo experimental error. The artifact also contains a reusable version of Synduce, the tool implementing the synthesis algorithms presented in the paper.
Reproduction package for “Synthesizing Input Grammars”： A Replication Study
作者: Bendrissou, Bachir and Gopinath, Rahul and Zeller, Andreas
关键词: glade, grammar mining, replication
Abstract
This is a virtual box image that contains all experiments necessary to reproduce the results of the paper “Synthesizing Input Grammars”: A Replication Study.
Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model (The Artifact)
作者: Ahrens, Willow and Kjolstad, Fredrik and Amarasinghe, Saman
关键词: Asymptotic Analysis, Automatic Scheduling, Compilers, Conjunctive Query Containment, Query Optimization, Sparse Tensors
Abstract
An artifact to replicate the results of “Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model”, Willow Ahrens, Fredrik Kjolstad, and Saman Amarasinghe. PLDI 2022.
DISTAL： the distributed tensor algebra compiler
作者: Yadav, Rohan and Aiken, Alex and Kjolstad, Fredrik
关键词: Compilers, Distributed Systems, High Performance Computing
Abstract
We introduce DISTAL, a compiler for dense tensor algebra that targets modern distributed and heterogeneous systems. DISTAL lets users independently describe how tensors and computation map onto target machines through separate format and scheduling languages. The combination of choices for data and computation distribution creates a large design space that includes many algorithms from both the past (e.g., Cannon’s algorithm) and the present (e.g., COSMA). DISTAL compiles a tensor algebra domain specific language to a distributed task-based runtime system and supports nodes with multi-core CPUs and multiple GPUs. Code generated by is competitive with optimized codes for matrix multiply on 256 nodes of the Lassen supercomputer and outperforms existing systems by between 1.8x to 3.7x (with a 45.7x outlier) on higher order tensor operations.
Reproduction Package for “All You Need Is Superword-Level Parallelism： Systematic Control-Flow Vectorization with SLP”
作者: Chen, Yishen and Mendis, Charith and Amarasinghe, Saman
关键词: Compiler, Optimization, SIMD, Vectorization
Abstract
Artifact to reproduce the result in the paper.
Replication Package for Warping Cache Simulation of Polyhedral Programs
作者: Morelli, Canberk and Reineke, Jan
关键词: cache model, cache simulation, data independence, performance analysis, simulation
Abstract
This is the artifact of the conference paper “Warping Cache Simulation of Polyhedral Programs” at PLDI 2022.
The artifact structure is as follows: - benchmark: The PolyBench benchmark that is used in our experiments. - data: The data we obtained from our experiments (data/existing) which are presented in our paper as plots. The data that you will reproduce will also be available here (data/reproduced). - haystack-artifact: The artifact provided by the related work HayStack. - plots: The plots you will generate (plots/from-existing-data and plots/from-reproduced-data). - scripts: The scripts for repeating our experiments and generating our figures. - warping-cache-simulation: The source code of our cache simulation tool. - d4-7.tar.gz: DineroIV package, used only if the ftp server used in haystack-artifact/Dockerfile is down. - Dockerfile: File to build our Docker image, which will be used to repeat our experiments and generate our plots. - README.md: This file. We suggest using a “markdown capable” viewer to read the file. - paper-submission-version.pdf: The submission version of our accepted paper.
Please refer to the README.md for more information.
Certified mergeable replicated data types
作者: Soundarapandian, Vimala and Kamath, Adharsh and Nagar, Kartik and Sivaramakrishnan, KC
关键词: Automated verification, Eventual consistency, MRDTs, Replication-aware simulation
Abstract
Replicated data types (RDTs) are data structures that permit concurrent modification of multiple, potentially geo-distributed, replicas without coordination between them. RDTs are designed in such a way that conflicting operations are eventually deterministically reconciled ensuring convergence. Constructing correct RDTs remains a difficult endeavour due to the complexity of reasoning about independently evolving states of the replicas. With the focus on the correctness of RDTs (and rightly so), existing approaches to RDTs are less efficient compared to their sequential counterparts in terms of the time and space complexity of local operations. This is unfortunate since RDTs are often used in a local-first setting where the local operations far outweigh remote communication. This paper presents PEEPUL, a pragmatic approach to building and verifying efficient RDTs. To make reasoning about correctness easier, we cast RDTs in the mould of the distributed version control system, and equip it with a three-way merge function for reconciling conflicting versions. Further, we go beyond just verifying convergence, and provide a methodology to verify arbitrarily complex specifications. We develop a replication-aware simulation relation to relate RDT specifications to their efficient purely functional implementations. We implement PEEPUL as an F* library that discharges proof obligations to an SMT solver. The verified efficient RDTs are extracted as OCaml code and used in Irmin, a distributed database built on the principles of Git.
Hamband： RDMA replicated data types
作者: Houshmand, Farzin and Saberlatibari, Javad and Lesani, Mohsen
关键词: Operational Semantics, RDMA, WRDT
Abstract
Data centers are increasingly equipped with RDMAs. These network interfaces mark the advent of a new distributed system model where a node can directly access the remote memory of another. They have enabled microsecond-scale replicated services. The underlying replication protocols of these systems execute all operations under strong consistency. However, strong consistency can hinder response time and availability, and recent replication models have turned to a hybrid of strong and relaxed consistency. This paper presents RDMA well-coordinated replicated data types, the first hybrid replicated data types for the RDMA network model. It presents a novel operational semantics for these data types that considers three distinct categories of methods and captures their required coordination, and formally proves that they preserve convergence and integrity. It implements these semantics in a system called Hamband that leverages direct remote accesses to efficiently implement the required coordination protocols. The empirical evaluation shows that Hamband outperforms the throughput of existing message-based and strongly consistent implementations by more than 17x and 2.7x respectively.
RunTime-assisted convergence in replicated data types
作者: Kaki, Gowtham and Prahladan, Prasanth and Lewchenko, Nicholas V.
关键词: CRDT, Causal Consistency, Concurrent Revisions, Convergence, Decentralized Systems, MRDT, Replication, Runtime
Abstract
We propose a runtime-assisted approach to enforce convergence in distributed executions of replicated data types. The key distinguishing aspect of our approach is that it guarantees convergence unconditionally – without requiring data type operations to satisfy algebraic laws such as commutativity and idempotence. Consequently, programmers are no longer obligated to prove convergence on a per-type basis. Moreover, our approach lets sequential data types be reused in a distributed setting by extending their implementations rather than refactoring them. The novel component of our approach is a distributed runtime that orchestrates well-formed executions that are guaranteed to converge. Despite the utilization of a runtime, our approach comes at no additional cost of latency and availability. Instead, we introduce a novel tradeoff against a metric called staleness, which roughly corresponds to the time taken for replicas to converge. We implement our approach in a system called Quark and conduct a thorough evaluation of its tradeoffs.
Artifact For “Adore： Atomic Distributed Objects with Certified Reconfiguration”
作者: Honor'{e
关键词: consensus protocols, Coq, distributed systems, formal verification, reconfiguration, refinement
Abstract
This is the Coq implementation of the Adore model, safety proof, and refinement described in the paper. It also includes an executable instantiation of the abstract model using OCaml extraction. Refer to the README for build instructions and additional details.
CycleQ
作者: Jones, Eddie and Ong, C.-H. Luke and Ramsay, Steven
关键词: cyclic proofs, equational reasoning, program verification
Abstract
CycleQ is an efficient basis for automatic equation reasoning with cyclic proofs, rather than traditional induction, that is aimed at verifying the behaviour of functional programs. Specifically, the tool is implemented as a plugin for GHC.
Finding the Dwarf： Recovering Precise Types from WebAssembly Binaries
作者: Lehmann, Daniel and Pradel, Michael
关键词: DWARF, WebAssembly, corpus, dataset, debugging information, machine learning, neural networks, reverse engineering, type prediction, type recovery
Abstract
The increasing popularity of WebAssembly creates a demand for understanding and reverse engineering WebAssembly binaries. Recovering high-level function types is an important part of this process. One method to recover types is data-flow analysis, but it is complex to implement and may require manual heuristics when logical constraints fall short. In contrast, this paper presents SnowWhite, a learning-based approach for recovering precise, high-level parameter and return types for WebAssembly functions. It improves over prior work on learning-based type recovery by representing the types-to-predict in an expressive type language, which can describe a large number of complex types, instead of the fixed, and usually small type vocabulary used previously. Thus, recovery of a single type is no longer a classification task but sequence prediction, for which we build on the success of neural sequence-to-sequence models. We evaluate SnowWhite on a new, large-scale dataset of 6.3 million type samples extracted from 300,905 WebAssembly object files. The results show the type language is expressive, precisely describing 1,225 types instead the 7 to 35 types considered in previous learning-based approaches. Despite this expressiveness, our type recovery has high accuracy, exactly matching 44.5% (75.2%) of all parameter types and 57.7% (80.5%) of all return types within the top-1 (top-5) predictions.
Abstract interpretation repair
作者: Bruni, Roberto and Giacobazzi, Roberto and Gori, Roberta and Ranzato, Francesco
关键词: CEGAR, abstract interpretation, local completeness, program analysis, program verification
Abstract
Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials (Artifact)
作者: \v{Z
关键词: Cost analysis, Differential cost analysis, Potential functions, Relational reasoning
Abstract
The artifact contains a prototype tool for differential cost analysis of numerical C programs with polynomial arithmetic and possibly with non-determinism. Given two programs together with their input sets, the tool computes an upper bound on the maximal difference in cost usage between the two programs on any initial variable valuation that is contained in both input sets. Cost may take both positive and negative values, and we assume that each program has a special variable “cost” that is initialized to 0 and that is updated whenever cost is incurred in the program. It could be used to track program runtime, memory usage, the number of object allocations, or any other program property of interest that could be tracked by a program variable.
The artifact is provided both as a docker image and as a zip of all source files. The reason for providing both is that, in our experimental evaluation, we use Gurobi for linear programming (LP) which is licensed and is free only for academic use. Thus, we cannot install Gurobi in our docker image but replace it with the GLPK solver. GLPK allows reproducing our experimental results with slightly longer runtimes (details are provided in README). To reproduce our reported experimental results with Gurobi, one needs to build the tool from source files and instructions for doing so are provided in README.
A Flexible Type System for Fearless Concurrency： Accompanying Artifact
作者: Milano, Mae and Turcotti, Julia and Myers, Andrew C.
关键词: aliasing, compiler, concurrency, coq, linear types, ocaml, regions, type systems
Abstract
An implementation of a type-checker (with efficient proof search/inference) for the language described in the PLDI 2022 paper “A Flexible Type System for Fearless Concurrency,” available with DOI 10.1145/3519939.3523443 at the The ACM DL in June of 2022. Includes an accompanying virtual machine, with all dependencies installed, capable of building the type checker.
Data race examples
作者: Chabbi, Milind and Ramanathan, Murali Krishna
关键词: data races, dynamic analysis, golang
Abstract
Examples of the data races discussed in the PLDI 22 paper titled “A Real World Study of Data Races in Golang”
Replication Package for Article： Checking Robustness to Weak Persistency Models
作者: Gorjiara, Hamed and Luo, Weiyu and Lee, Alex and Xu, Guoqing Harry and Demsky, Brian
关键词: Crash Consistency Bugs, Jaaru, Persistency Bugs, Persistent Memory Model Checker, PMDK, PSan, RECIPE, Robustness Violations
Abstract
This artifact contains a vagrant repository that downloads and compiles the source code for PSan(a plugin for Jaaru), its companion compiler pass, and benchmarks. The artifact enables users to reproduce the bugs that are found by PSan in PMDK and RECIPE (Table 2
Artifact for PLDI’22 paper “Sound Sequentialization for Concurrent Program Verification”
作者: Farzan, Azadeh and Klumpp, Dominik and Podelski, Andreas
关键词: Concurrency, Partial Order Reduction, Sequentialization
Abstract
This artifact for the PLDI’22 paper “Sound Sequentialization for Concurrent Program Verification” consists of a docker image that contains source code for the evaluated verifiers, compiled binaries of the verifiers, benchmark programs to compare the verifiers, and the raw evaluation results that form the basis for the discussion in the paper.
OpTuner Artifact
作者: Briggs, Ian and Panchekha, Pavel
关键词: accuracy, floating point, ILP, optimization
Abstract
Instructions and a virtual machine image to verify the claims in the paper “Choosing Math Function Implementations for Speed and Accuracy”
Artifact for： Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming (PLDI 2022)
作者: Beutner, Raven and Ong, C.-H. Luke and Zaiser, Fabian
关键词: abstract interpretation, Bayesian inference, interval arithmetic, operational semantics, probabilistic programming, symbolic execution, type system, verification
Abstract
This is the artifact for “Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming” (PLDI 2022). It contains the implementation of the GuBPI tool, which can compute Guaranteed Bounds for Posterior Inference. It also includes the benchmarks from the paper and scripts to reproduce the reported data. For convenience, Docker images are also provided to allow for quick experimentation.
Artifact for Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
作者: Aanjaneya, Mridul and Lim, Jay P. and Nagarakatte, Santosh
关键词: Correct rounded elementary functions, progressive polynomials, RLIBM, RLIBM-PROG
Abstract
We present the artifact for the paper, “Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries.” We describe the list of claims made by the paper, evaluation instructions, and instructions on how to use RLIBM-PROG. To ease the installation effort, we provide a docker image with all but one required softwares installed already (with instructions on how to build the remaining required software in the docker image). Additionally, we provide complete instructions to manually install the artifact on Ubuntu 20.04.
A typed continuation-passing translation for lexical effect handlers
作者: Schuster, Philipp and Brachth"{a
关键词: continuation-passing style, lexical effect handlers
Abstract
Effect handlers are a language feature which enjoys popularity in academia and
is also gaining traction in industry. Programs use abstract effect operations
and handlers provide meaning to them in a delimited scope. Each effect operation
is handled by the dynamically closest handler. Using an effect operation outside
of a matching handler is meaningless and results in an error. A type-and-effect
system prevents such errors from happening.
Lexical effect handlers are a recent variant of effect handlers with a number of
attractive properties. Just as with traditional effect handlers, programs use
effect operations and handlers give meaning to them. But unlike with traditional
effect handlers, the connection between effect operations and their handler is
lexical. Consequently, they typically have different type-and-effect systems.
The semantics of lexical effect handlers as well as their implementations use
multi-prompt delimited control. They rely on the generation of fresh labels at
runtime, which associate effect operations with their handlers. This use of
labels and multi-prompt delimited control is theoretically and practically
unsatisfactory.
Our main result is that typed lexical effect handlers do not need the full power
of multi-prompt delimited control. We present the first CPS translation for
lexical effect handlers to pure System F. It preserves well-typedness and
simulates the traditional operational semantics. Importantly, it does so without
requiring runtime labels. The CPS translation can be used to study the semantics
of lexical effect handlers as well as as an implementation technique.
Deep and Shallow Types for Gradual Languages
作者: Greenman, Ben
关键词: complete monitoring, gradual typing, migratory typing, type enforcement strategies
Abstract
Data, analysis scripts, and source code.
Implementation of the KMT framework in OCaml
作者: Greenberg, Michael and Beckett, Ryan and Campbell, Eric
关键词: algebraic models, functors, kleene algebra, modules, program equivalence, tracing semantics, verification
Abstract
Kleene algebra modulo theories (KMT) is a framework for deriving concrete Kleene algebras with tests (KATs)—an algebraic framework for While-like programs with decidable program equivalence.
More plainly: KMT is a framework for building simple programming languages with structured control (if, while, etc.) where we can algorithmically decide whether or not two programs are equivalent. You can use equivalence to verify programs. If a is a nice property to have after running your program, then if p;a == p, you know that p satisfies a. Kleene algebra with tests subsumes Hoare logic: if a;p;~b == 0 then all runs starting from a either diverge or end with b, i.e., that equation corresponds to the partial correctness specification {a
Semantic soundness for language interoperability
作者: Patterson, Daniel and Mushtak, Noble and Wagner, Andrew and Ahmed, Amal
关键词: language interoperability, logical relations, semantics, type soundness
Abstract
Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate features can frustrate interoperability, as invariants from one language can easily be violated in the other. In their seminal 2007 paper, Matthews and Findler proposed a multi-language construction that augments the interoperating languages with a pair of boundaries that allow code from one language to be embedded in the other. While this technique has been widely applied, their syntactic source-level interoperability doesn’t reflect practical implementations, where the behavior of interaction is only defined after compilation to a common target, and any safety must be ensured by target invariants or inserted target-level “glue code.” In this paper, we present a novel framework for the design and verification of sound language interoperability that follows an interoperation-after-compilation strategy. Language designers specify what data can be converted between types of the two languages via a convertibility relation τA ∼ τB (“τA is convertible to τB”) and specify target-level glue code implementing the conversions. Then, by giving a semantic model of source-language types as sets of target-language terms, they can establish not only the meaning of the source types, but also soundness of conversions: i.e., whenever τA ∼ τB, the corresponding pair of conversions (glue code) convert target terms that behave like τA to target terms that behave like τB, and vice versa. With this, they can prove semantic type soundness for the entire system. We illustrate our framework via a series of case studies that demonstrate how our semantic interoperation-after-compilation approach allows us both to account for complex differences in language semantics and make efficiency trade-offs based on particularities of compilers or targets.
Artifact for PLDI 2022 Paper： Quartz： Superoptimization of Quantum Circuits
作者: Xu, Mingkuan and Li, Zikun and Padon, Oded and Lin, Sina and Pointing, Jessica and Hirth, Auguste and Ma, Henry and Palsberg, Jens and Aiken, Alex and Acar, Umut A. and Jia, Zhihao
关键词: quantum computing, superoptimization
Abstract
Quartz is a quantum circuit optimizer that automatically generates and verifies circuit transformations for an arbitrary quantum gate set. To optimize an input quantum circuit, Quartz uses these auto-generated circuit transformations to construct a search space of functionally equivalent quantum circuits. Quartz uses a cost-based search algorithm to explore the space and discovers highly optimized quantum circuits.
Quartz is open-source and developed on GitHub: https://github.com/quantum-compiler/quartz.
This artifact supports the PLDI 2022 paper about Quartz, and contains the implementation and scripts used to obtain the results reported in the paper. See also the extended version of the paper at https://arxiv.org/abs/2204.09033.
Artifact for PLDI 2022 paper Giallar： Push-button Verification for the Qiskit Quantum Compiler
作者: Tao, Runzhou and Shi, Yunong and Yao, Jianan and Li, Xupeng and Javadi-Abhari, Ali and Cross, Andrew W. and Chong, Frederic T. and Gu, Ronghui
关键词: automated verification, compiler verification, quantum computing
Abstract
The artifact contains the docker image file needed to reproduce the results presented in the paper.
Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra
作者: Peng, Yuxiang and Ying, Mingsheng and Wu, Xiaodi
关键词: compiler optimization, non-idempotent Kleene algebra, normal form theorem, quantum Hoare logic
Abstract
We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.
Reproduction Package for Article “PyLSE： A Pulse-Transfer Level Language for Superconductor Electronics”
作者: Christensen, Michael and Tzimpragos, Georgios and Kringen, Harlan and Volk, Jennifer and Sherwood, Timothy and Hardekopf, Ben
关键词: hardware description language, superconductor electronics, timed automata
Abstract
PyLSE is a Python-embedded pulse-transfer level language for the design and simulation of superconductor electronics (SCE). The purpose of PyLSE is to make it easier to create precise and composable models of the basic SCE cells (i.e. gates), use these models to create larger systems, quickly get up and running in the built-in simulation framework, and finally prove various properties about these cells and systems using a state-of-the-art model checker. This artifact will show you how to do so, as well as show you how to get the results in the tables and figures found in the evaluation section of our paper.
Reproducing package for Bind the Gap： Compiling Software to Hardware FFT Accelerators
作者: Woodruff, Jackson and Armengol-Estap'{e
关键词: Compiler, FFT, Hardware Accelerator
Abstract
#FACC Artifact Evaluation
This set of instructions is split into several sections. First, we cover the generic build process. We then cover steps required to reproduce each figure. The main directory is FACC. Other sub-directories should be used as refered to in the README.
Exocompilation for Productive Programming of Hardware Accelerators
作者: Ikarashi, Yuka and Bernstein, Gilbert Louis and Reinking, Alex and Genc, Hasan and Ragan-Kelley, Jonathan
关键词: Code optimization, Computer architecture, High performance computing, Language design
Abstract
This artifact consists of a Docker image capable of reproducing our AVX-512 benchmarks on compatible hardware (e.g. Skylake-X or Tiger Lake). To use the latest Exo system for practical development, we refer readers to our GitHub repository at: https://github.com/ChezJrk/exo and our Python package at: https://pypi.org/project/exo-lang/
Reproduction Package for ‘PDL： A High-Level Hardware Design Language for Pipelined Processors’
作者: Zagieboylo, Drew and Sherk, Charles and Suh, Gookwon Edward and Myers, Andrew C.
关键词: Computer Architecture, Language Design
Abstract
A Docker container which can be used to recreate the results from the PLDI ’22 paper, PDL: A High-Level Hardware Design Language for Pipelined Processors.
This includes:
- The source code of the PDL compiler and its test suite
- A simulator for the baseline Chisel processor used in our evaluation
- The PDL programs describing the RISC-V architectures described in our evaluation
- A build system to generate the CPI results reported in the paper for the above architectures
Software-hardware codesign for efficient in-memory regular pattern matching
作者: Kong, Lingkun and Yu, Qixuan and Chattopadhyay, Agnishom and Le Glaunec, Alexis and Huang, Yi and Mamouras, Konstantinos and Yang, Kaiyuan
关键词: automata theory, computer architecture
Abstract
Regular pattern matching is used in numerous application domains, including text processing, bioinformatics, and network security. Patterns are typically expressed with an extended syntax of regular expressions. This syntax includes the computationally challenging construct of bounded repetition or counting, which describes the repetition of a pattern a fixed number of times. We develop a specialized in-memory hardware architecture that integrates counter and bit vector modules into a state-of-the-art in-memory NFA accelerator. The design is inspired by the theoretical model of nondeterministic counter automata (NCA). A key feature of our approach is that we statically analyze regular expressions to determine bounds on the amount of memory needed for the occurrences of bounded repetition. The results of this analysis are used by a regex-to-hardware compiler in order to make an appropriate selection of counter or bit vector modules. We evaluate our hardware implementation using a simulator based on circuit parameters collected by SPICE simulation in TSMC 28nm CMOS process. We find that the use of counter and bit vector modules outperforms unfolding solutions by orders of magnitude. Experiments concerning realistic workloads show up to 76% energy reduction and 58% area reduction in comparison to CAMA, a recently proposed in-memory NFA accelerator.
Artifact of “Deoptless： Speculation with Dispatched On-Stack Replacement and Specialized Continuations”
作者: Fl"{u
关键词: virtual machine
Abstract
This is the artifact to accompany our PLDI 2022 submission on “Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations”. The artifact consists of a virtual machine for the R language, called \v{R
Karp： a language for NP reductions
作者: Zhang, Chenhao and Hartline, Jason D. and Dimoulas, Christos
关键词: domain-specific language, reduction, solver-aided program- ming, teaching and learning theoretical computer science
Abstract
In CS theory courses, NP reductions are a notorious source of pain for students and instructors alike. Invariably, students use pen and paper to write down reductions that “work” in many but not all cases. When instructors observe that a student’s reduction deviates from the expected one, they have to manually compute a counterexample that exposes the mistake. In other words, NP reductions are subtle yet, most of the time, unimplemented programs. And for a good reason: there exists no language tailored to NP reductions.
We introduce Karp, a language for programming and testing NP reductions. Karp combines an array of programming languages techniques: language-oriented programming and macros, solver-aided languages, property testing, higher-order contracts and gradual typing. To validate the correctness of Karp, we prove that its core is well-defined. To validate its pragmatics, we demonstrate that it is expressive and performant enough to handle a diverse set of reduction exercises from a popular algorithms textbook. Finally, we report the results from a preliminary user study with Karp.
WARio： Efficient Code Generation for Intermittent Computing - PLDI 2022 Artifact
作者: Kortbeek, Vito and Ghosh, Souradip and Hester, Josiah and Campanoni, Simone and Pawe\l{
关键词: ARM, battery-free, compiler-support, embedded, intermittent computing, mixed-memory architecture, non-volatile memory, PLDI
Abstract
This is the PLDI 2022 artifact for WARio, a compiler-support runtime for intermittently-powered platforms with non-volatile main memory.
This artifact is separated into three downloadable objects: * docker.zip, which holds all the Dockerfiles and prebuilt Docker containers. * code.zip, which holds all the source code (also available at: https://github.com/TUDSSL/WARio) * README.md, a markdown file containing more details about this artifact and how to evaluate it properly.
The docker containers can go through all the steps required to reproduce WARio, from building WARio and its dependencies to generating the figures and tables presented in the paper (and more).
For more information, please download the README.md file in this artifact.
Accompanying GitHub repository: https://github.com/TUDSSL/WARio
Supporting grants: NWO: P15-06 NSF: CNS-1850496, CNS-2145584, CCF-1908488, CNS-1763743
Compass： Strong and Compositional Library Specifications in Relaxed Memory Separation Logic (Artifact)
作者: Dang, Hoang-Hai and Jung, Jaehwang and Choi, Jaemin and Nguyen, Duc-Than and Mansky, William and Kang, Jeehoon and Dreyer, Derek
关键词: C11, Coq, Iris, Linearizabliity, Logical Atomicity, Relaxed Memory, Separation Logic
Abstract
This contains a snapshot of the Compass development.
More updated information can be found at https://plv.mpi-sws.org/compass/.
Artifact and Appendix of ‘Diaframe： Automated Verification of Fine-Grained Concurrent Programs in Iris’
作者: Mulder, Ike and Krebbers, Robbert and Geuvers, Herman
关键词: Coq, fine-grained concurrency, Iris, proof automation, Separation logic
Abstract
This is the artifact for the PLDI ‘22 paper ’Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris’. It contains the Diaframe source code, a VM containing a compiled version of this source code, the appendix for the paper, and instructions for evaluation.
Artifact for “Islaris： Verification of Machine Code Against Authoritative ISA Semantics”
作者: Sammler, Michael and Hammond, Angus and Lepigre, Rodolphe and Campbell, Brian and Pichon-Pharabod, Jean and Dreyer, Derek and Garg, Deepak and Sewell, Peter
关键词: Arm, assembly, Coq, Iris, Isla, proof automation, RISC-V, Sail, separation logic, verification
Abstract
This is the artifact for the PLDI’22 paper “Islaris: Verification of Machine Code Against Authoritative ISA Semantics”. It contains the Coq development for the paper.
RustHornBelt： A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code, Artifact
作者: Matsushita, Yusuke and Denis, Xavier and Jourdan, Jacques-Henri and Dreyer, Derek
关键词: Coq mechanization, Iris, Rust, semi-automated verification, separation logic, Why3
Abstract
It is the artifact for the PLDI 2022 paper “RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code”. It contains the Coq mechanization of RustHornBelt’s type-spec system and its semantic soundness proof, as well as the benchmarks that evaluate RustHornBelt’s specs using a semi-automated Rust verifier Creusot.
Efficient approximations for cache-conscious data placement
作者: Ahmadi, Ali and Daliri, Majid and Goharshady, Amir Kafshdar and Pavlogiannis, Andreas
关键词: approximation, cache management, cache misses, data placement, parameterization, treewidth
Abstract
There is a huge and growing gap between the speed of accesses to data stored in main memory vs cache. Thus, cache misses account for a significant portion of runtime overhead in virtually every program and minimizing them has been an active research topic for decades. The primary and most classical formal model for this problem is that of Cache-conscious Data Placement (CDP): given a commutative cache with constant capacity k and a sequence Σ of accesses to data elements, the goal is to map each data element to a cache line such that the total number of cache misses over Σ is minimized. Note that we are considering an offline single-threaded setting in which Σ is known a priori. CDP has been widely studied since the 1990s. In POPL 2002, Petrank and Rawitz proved a notoriously strong hardness result: They showed that for every k ≥ 3, CDP is not only NP-hard but also hard-to-approximate within any non-trivial factor unless P=NP. As such, all subsequent works gave up on theoretical improvements and instead focused on heuristic algorithms with no theoretical guarantees. In this work, we present the first-ever positive theoretical result for CDP. The fundamental idea behind our approach is that real-world instances of the problem have specific structural properties that can be exploited to obtain efficient algorithms with strong approximation guarantees. Specifically, the access graphs corresponding to many real-world access sequences are sparse and tree-like. This was already well-known in the community but has only been used to design heuristics without guarantees. In contrast, we provide fixed-parameter tractable algorithms that provably approximate the optimal number of cache misses within any factor 1 + є, assuming that the access graph of a specific degree dє is sparse, i.e. sparser real-world instances lead to tighter approximations. Our theoretical results are accompanied by an experimental evaluation in which our approach outperforms past heuristics over small caches with a handful of lines. However, the approach cannot currently handle large real-world caches and making it scalable in practice is a direction for future work.
Artifact： FreeTensor： A Free-form DSL with Holistic Optimizations for Irregular Tensor Programs
作者: Tang, Shizhi and Zhai, Jidong and Wang, Haojie and Jiang, Lin and Zheng, Liyan and Yuan, Zhenhao and Zhang, Chen
关键词: DSL, optimizing compilers, tensor computing
Abstract
Artifact for PLDI ’22 paper “FreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programs”. The tensor compiler described in the paper is included, and the performance number can be reproduced.
Lasagne： A Static Binary Translator for Weak Memory Model Architectures
作者: Rocha, Rodrigo C. O. and Sprokholt, Dennis and Fink, Martin and Gouicem, Redha and Spink, Tom and Chakraborty, Soham and Bhatotia, Pramod
关键词: LLVM, Memory Model, Static Binary Translation
Abstract
Artifact for the paper titled “Lasagne: A Static Binary Translator for Weak Memory Model Architectures” published in the Conference on Programming Language Design and Implementation, 2022. It contains the automated proofs presented in the paper as well as the software for the Lasagne system and its evaluation.
Artifact of “Verifying Optimizations of Concurrent Programs in the Promising Semantics”
作者: Zha, Junpeng and Liang, Hongjin and Feng, Xinyu
关键词: Code optimizations, Concurrency, Coq, Verification, Weak memory models
Abstract
This is the artifact of PLDI22-paper984 “Verifying Optimizations of Concurrent Programs in the Promising Semantics”. We package our artifact (mechanized proof of the verification framework introduced in our paper in the Coq) in the virtual machine VirtualBox-6.1.32 as pldi22-paper984.ova. Detailed descriptions of the artifact can be found in the README.txt.
Artifact for “Relational Compilation for Performance-Critical Applications”
作者: Pit-Claudel, Cl'{e
关键词: compilation, theorem proving, verification
Abstract
A virtual machine submitted to PLDI 2022’s artifact evaluation committee.
Artifact for Article `Formally Verified Lifting of C-compiled x86-64 Binaries’
作者: Verbeek, Freek and Bockenek, Joshua and Fu, Zhoulai and Ravindran, Binoy
关键词: binary verification, disassembly, formal methods
Abstract
This artifact accompanies the PLDI’22 article `Formally Verified Lifting of C-compiled x86-64 Binaries’. It can be used to disassemble x86-64 binaries and export proofs of correctness to the Isabelle/HOL theorem prover.
Leapfrog： Certified Equivalence for Protocol Parsers
作者: Doenges, Ryan and Kapp'{e
关键词: automata, certified parsers, Coq, equivalence, foundational verification, network protocol parsers, P4
Abstract
This is the artifact accompanying the paper “Leapfrog: Certified Equivalence for Protocol Parsers”, to appear at PLDI 2022. See the README.md file for more details and installation instructions.
Artifact for Computing Correctly with Inductive Relations
作者: Paraskevopoulou, Zoe and Eline, Aaron and Lampropoulos, Leonidas
关键词: Coq, Inductive relations, QuickChick
Abstract
VM containing ready-to-build experiments for the paper.
Interpreter-guided differential JIT compiler unit testing
作者: Polito, Guillermo and Ducasse, St'{e
关键词: JIT compilers, concolic testing, interpreters, virtual machine
Abstract
Modern language implementations using Virtual Machines feature diverse execution engines such as byte-code interpreters and machine-code dynamic translators, a.k.a. JIT compilers. Validating such engines requires not only validating each in isolation, but also that they are functionally equivalent. Tests should be duplicated for each execution engine, exercising the same execution paths on each of them.
In this paper, we present a novel automated testing ap- proach for virtual machines featuring byte-code interpreters. Our solution uses concolic meta-interpretation: it applies concolic testing to a byte-code interpreter to explore all pos- sible execution interpreter paths and obtain a list of concrete values that explore such paths. We then use such values to apply differential testing on the VM interpreter and JIT compiler. This solution is based on two insights: (1) both the interpreter and compiler implement the same language semantics and (2) interpreters are simple executable specifications of those semantics and thus promising targets to (meta-) interpretation using concolic testing. We validated it on 4 different compilers of the open-source Pharo Virtual Machine and found 468 differences between them, produced by 91 different causes, organized in 6 different categories.
Landmarks and regions： a robust approach to data extraction
作者: Parthasarathy, Suresh and Pattanaik, Lincy and Khatry, Anirudh and Iyer, Arun and Radhakrishna, Arjun and Rajamani, Sriram K. and Raza, Mohammad
关键词: Data extraction, Landmarks and regions, Program synthesis, Semi-structured data
Abstract
We propose a new approach to extracting data items or field values from semi-structured documents. Examples of such problems include extracting passenger name, departure time
and departure airport from a travel itinerary, or extracting price of an item from a purchase receipt. Traditional approaches to data extraction use machine learning or program synthesis to process the whole document to extract the desired fields. Such approaches are not robust to for-
mat changes in the document, and the extraction process typically fails even if changes are made to parts of the document that are unrelated to the desired fields of interest. We propose a new approach to data extraction based on the concepts of landmarks and regions. Humans routinely use
landmarks in manual processing of documents to zoom in and focus their attention on small regions of interest in the document. Inspired by this human intuition, we use the notion of landmarks in program synthesis to automatically synthesize extraction programs that first extract a small region
of interest, and then automatically extract the desired value from the region in a subsequent step. We have implemented our landmark based extraction approach in a tool LRSyn, and show extensive
valuation on documents in HTML as well as scanned images of invoices and receipts. Our results
show that the our approach is robust to various types of format changes that routinely happen in real-world settings
Odin： on-demand instrumentation with on-the-fly recompilation
作者: Wang, Mingzhe and Liang, Jie and Zhou, Chijin and Wu, Zhiyong and Xu, Xinyi and Jiang, Yu
关键词: Instrumentation, On-the-Fly Recompilation
Abstract
Instrumentation is vital to fuzzing. It provides fuzzing directions and helps detect covert bugs, yet its overhead greatly reduces the fuzzing throughput. To reduce the overhead, compilers compromise instrumentation correctness for better optimization, or seek convoluted runtime support to remove unused probes during fuzzing.
In this paper, we propose Odin, an on-demand instrumentation framework to instrument C/C++ programs correctly and flexibly. When instrumentation requirement changes during fuzzing, Odin first locates the changed code fragment, then re-instruments, re-optimizes, and re-compiles the small fragment on-the-fly. Consequently, with a minuscule compilation overhead, the runtime overhead of unused probes is reduced. Its architecture ensures correctness in instrumentation, optimized code generation, and low latency in recompilation. Experiments show that Odin delivers the performance of compiler-based static instrumentation while retaining the flexibility of binary-based dynamic instrumentation. When applied to coverage instrumentation, Odin reduces the coverage collection overhead by 3\texttimes{
Reproduction Package for ‘Quickstrom： Property-based acceptance testing with LTL specifications’
作者: O’Connor, Liam and Wickstr"{o
关键词: programming, property-based testing, results, software, web applications
Abstract
This artifact contains the software, source code, and experimental results for the paper ‘Quickstrom: Property-based acceptance testing with LTL specifications’ at PLDI 2022. See README.TXT for more details.
评论
