From b9ff75209d6aaf814e1024dfe714570d80a796af Mon Sep 17 00:00:00 2001 From: Alastair Reid Date: Sat, 22 Jun 2024 15:13:13 +0100 Subject: [PATCH] wip --- _papers/dutertre:smt:2015.md | 16 +++++++++ _papers/mosier:sandp:2023.md | 12 +++++-- _papers/sasnauskas:arxiv:2018.md | 27 ++++++++++++++ _staging/10.1007:978-3-030-29436-6_22.md | 31 ++++++++++++++++ _staging/10.1007:978-3-319-21668-3_10.md | 29 +++++++++++++++ _staging/10.1007:978-3-319-96145-3_15.md | 34 ++++++++++++++++++ _staging/10.1007:978-3-642-54013-4_12.md | 23 ++++++++++++ _staging/10.1007:978-3-662-54577-5_18.md | 28 +++++++++++++++ _staging/10.1007:s00236-017-0294-5.md | 38 ++++++++++++++++++++ _staging/10.1145:1706299.1706345.md | 37 +++++++++++++++++++ _staging/10.1145:1707801.1706345.md | 39 ++++++++++++++++++++ _staging/10.1145:1993316.1993532.md | 37 +++++++++++++++++++ _staging/10.1145:1993498.1993532.md | 35 ++++++++++++++++++ _staging/10.1145:2451116.2451150.md | 34 ++++++++++++++++++ _staging/10.1145:2490301.2451150.md | 36 +++++++++++++++++++ _staging/10.1145:2499368.2451150.md | 36 +++++++++++++++++++ _staging/10.1145:2737924.2737965.md | 36 +++++++++++++++++++ _staging/10.1145:2813885.2737965.md | 38 ++++++++++++++++++++ _staging/10.1145:2837614.2837666.md | 40 +++++++++++++++++++++ _staging/10.1145:2872362.2872387.md | 40 +++++++++++++++++++++ _staging/10.1145:2914770.2837666.md | 42 ++++++++++++++++++++++ _staging/10.1145:2954679.2872387.md | 42 ++++++++++++++++++++++ _staging/10.1145:2980024.2872387.md | 42 ++++++++++++++++++++++ _staging/10.1145:2983990.2984006.md | 36 +++++++++++++++++++ _staging/10.1145:3022671.2984006.md | 38 ++++++++++++++++++++ _staging/10.1145:3062341.3062372.md | 34 ++++++++++++++++++ _staging/10.1145:3140587.3062372.md | 36 +++++++++++++++++++ _staging/10.1145:3368826.3377927.md | 36 +++++++++++++++++++ _staging/10.1145:3371080.md | 46 ++++++++++++++++++++++++ _staging/10.1145:3428245.md | 39 ++++++++++++++++++++ _staging/10.1145:3453483.3454030.md | 37 +++++++++++++++++++ _staging/10.1145:3563334.md | 40 +++++++++++++++++++++ _staging/10.1145:3649837.md | 36 +++++++++++++++++++ _staging/10.1145:364995.365000.md | 29 +++++++++++++++ _staging/10.1145:502874.502885.md | 29 +++++++++++++++ _staging/10.1145:502949.502885.md | 31 ++++++++++++++++ _staging/6679385.md | 29 +++++++++++++++ 37 files changed, 1266 insertions(+), 2 deletions(-) create mode 100644 _papers/dutertre:smt:2015.md create mode 100644 _papers/sasnauskas:arxiv:2018.md create mode 100644 _staging/10.1007:978-3-030-29436-6_22.md create mode 100644 _staging/10.1007:978-3-319-21668-3_10.md create mode 100644 _staging/10.1007:978-3-319-96145-3_15.md create mode 100644 _staging/10.1007:978-3-642-54013-4_12.md create mode 100644 _staging/10.1007:978-3-662-54577-5_18.md create mode 100644 _staging/10.1007:s00236-017-0294-5.md create mode 100644 _staging/10.1145:1706299.1706345.md create mode 100644 _staging/10.1145:1707801.1706345.md create mode 100644 _staging/10.1145:1993316.1993532.md create mode 100644 _staging/10.1145:1993498.1993532.md create mode 100644 _staging/10.1145:2451116.2451150.md create mode 100644 _staging/10.1145:2490301.2451150.md create mode 100644 _staging/10.1145:2499368.2451150.md create mode 100644 _staging/10.1145:2737924.2737965.md create mode 100644 _staging/10.1145:2813885.2737965.md create mode 100644 _staging/10.1145:2837614.2837666.md create mode 100644 _staging/10.1145:2872362.2872387.md create mode 100644 _staging/10.1145:2914770.2837666.md create mode 100644 _staging/10.1145:2954679.2872387.md create mode 100644 _staging/10.1145:2980024.2872387.md create mode 100644 _staging/10.1145:2983990.2984006.md create mode 100644 _staging/10.1145:3022671.2984006.md create mode 100644 _staging/10.1145:3062341.3062372.md create mode 100644 _staging/10.1145:3140587.3062372.md create mode 100644 _staging/10.1145:3368826.3377927.md create mode 100644 _staging/10.1145:3371080.md create mode 100644 _staging/10.1145:3428245.md create mode 100644 _staging/10.1145:3453483.3454030.md create mode 100644 _staging/10.1145:3563334.md create mode 100644 _staging/10.1145:3649837.md create mode 100644 _staging/10.1145:364995.365000.md create mode 100644 _staging/10.1145:502874.502885.md create mode 100644 _staging/10.1145:502949.502885.md create mode 100644 _staging/6679385.md diff --git a/_papers/dutertre:smt:2015.md b/_papers/dutertre:smt:2015.md new file mode 100644 index 0000000..2e067a8 --- /dev/null +++ b/_papers/dutertre:smt:2015.md @@ -0,0 +1,16 @@ +--- +ENTRYTYPE: inproceedings +added: 2024-06-16 +authors: +- Bruno Dutertre +booktitle: 13th International Workshop on Satisfiability Modulo Theories (SMT 2015) +layout: paper +month: July +read: false +readings: [] +title: Solving Exists/Forall Problems With Yices +year: 2015 +notes: +papers: +--- +{% include links.html %} diff --git a/_papers/mosier:sandp:2023.md b/_papers/mosier:sandp:2023.md index cc5ddfd..06e7c83 100644 --- a/_papers/mosier:sandp:2023.md +++ b/_papers/mosier:sandp:2023.md @@ -14,8 +14,9 @@ eprinttype: arXiv journal: CoRR layout: paper link: https://doi.org/10.48550/arXiv.2309.05174 -read: false -readings: [] +read: true +readings: +- 2023-12-01 timestamp: Fri, 15 Sep 2023 12:26:52 +0200 title: 'Serberus: Protecting Cryptographic Code from Spectres at Compile-Time' url: https://doi.org/10.48550/arXiv.2309.05174 @@ -27,4 +28,11 @@ notes: - speculative execution papers: --- + +Serberus is a mitigation against [speculative execution] attacks +implemented as an extension of LLVM. +It relies on the use of Intel Architecture CET features to +constrain speculative branches. + + {% include links.html %} diff --git a/_papers/sasnauskas:arxiv:2018.md b/_papers/sasnauskas:arxiv:2018.md new file mode 100644 index 0000000..4160adb --- /dev/null +++ b/_papers/sasnauskas:arxiv:2018.md @@ -0,0 +1,27 @@ +--- +ENTRYTYPE: misc +added: 2024-06-16 +archiveprefix: arXiv +authors: +- Raimondas Sasnauskas +- Yang Chen +- Peter Collingbourne +- Jeroen Ketema +- Gratian Lup +- Jubi Taneja +- John Regehr +eprint: '1711.04422' +layout: paper +primaryclass: id=\textquotesingle cs.PL\textquotesingle full\_name=\textquotesingle Programming Languages\textquotesingle is\_active=True alt\_name=None + in\_archive=\textquotesingle cs\textquotesingle is\_general=False description=\textquotesingle Covers programming language semantics, language features, + programming approaches (such as object-oriented programming, functional programming, logic programming). Also includes material on compilers oriented + towards programming languages; other material on compilers may be more appropriate in Architecture (AR). Roughly includes material in ACM Subject Classes + D.1 and D.3.\textquotesingle +read: false +readings: [] +title: 'Souper: A Synthesizing Superoptimizer' +year: 2018 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:978-3-030-29436-6_22.md b/_staging/10.1007:978-3-030-29436-6_22.md new file mode 100644 index 0000000..9a6b6db --- /dev/null +++ b/_staging/10.1007:978-3-030-29436-6_22.md @@ -0,0 +1,31 @@ +--- +ENTRYTYPE: inproceedings +abstract: Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used + directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas with parametric + bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification. + While this logic is undecidable, this approach can still solve many formulas by capitalizing on advances in SMT solving for non-linear arithmetic and + universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width + independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrites. +added: 2024-06-22 +address: Cham +authors: +- Aina Niemetz +- Mathias Preiner +- Andrew Reynolds +- Yoni Zohar +- Clark Barrett +- Cesare Tinelli +booktitle: Automated Deduction - CADE 27 +editor: Fontaine, Pascal +isbn: 978-3-030-29436-6 +layout: paper +pages: 366-384 +publisher: Springer International Publishing +read: false +readings: [] +title: Towards Bit-Width-Independent Proofs in SMT Solvers +year: 2019 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:978-3-319-21668-3_10.md b/_staging/10.1007:978-3-319-21668-3_10.md new file mode 100644 index 0000000..85bcb6e --- /dev/null +++ b/_staging/10.1007:978-3-319-21668-3_10.md @@ -0,0 +1,29 @@ +--- +ENTRYTYPE: inproceedings +abstract: Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies + the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis + (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program \textbackslash \textdollar \textbackslash \textdollar + \textbackslash backslashmathtt \textbackslash Prog\textbackslash \textbackslash \textdollar \textbackslash \textdollar that is correct for S. The synthesizer + repeatedly checks if there exists a counterexample input c such that the execution of \textbackslash \textdollar \textbackslash \textdollar \textbackslash + backslashmathtt \textbackslash Prog\textbackslash \textbackslash \textdollar \textbackslash \textdollar is incorrect on c. If so, the synthesizer enlarges + S to include c, and picks a program from the program space that is correct for the new set S. +added: 2024-06-22 +address: Cham +authors: +- Rajeev Alur +- Pavol {\v C}erný +- Arjun Radhakrishna +booktitle: Computer Aided Verification +editor: Kroening, Daniel and P{\u a}s{\u a}reanu, Corina S. +isbn: 978-3-319-21668-3 +layout: paper +pages: 163-179 +publisher: Springer International Publishing +read: false +readings: [] +title: Synthesis Through Unification +year: 2015 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:978-3-319-96145-3_15.md b/_staging/10.1007:978-3-319-96145-3_15.md new file mode 100644 index 0000000..168a001 --- /dev/null +++ b/_staging/10.1007:978-3-319-96145-3_15.md @@ -0,0 +1,34 @@ +--- +ENTRYTYPE: inproceedings +abstract: Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution + space, and tools often require a user-provided syntactic restriction of the search space. We propose a new approach to program synthesis that combines + the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying + on user guidance. We call this approach CEGIS(\textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal \textbackslash T\textbackslash + \textbackslash \textdollar \textbackslash \textdollar T), where \textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal + \textbackslash T\textbackslash \textbackslash \textdollar \textbackslash \textdollar Tis a first-order theory. In this paper, we focus on one particular + challenge for program synthesizers, namely the generation of programs that require non-trivial constants. This is a fundamentally difficult task for state-of-the-art + synthesizers. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate + the practical value of CEGIS(\textbackslash \textdollar \textbackslash \textdollar \textbackslash backslashmathcal \textbackslash T\textbackslash \textbackslash + \textdollar \textbackslash \textdollar T) by automatically synthesizing programs for a set of intricate benchmarks. +added: 2024-06-22 +address: Cham +authors: +- Alessandro Abate +- Cristina David +- Pascal Kesseli +- Daniel Kroening +- Elizabeth Polgreen +booktitle: Computer Aided Verification +editor: Chockler, Hana and Weissenbacher, Georg +isbn: 978-3-319-96145-3 +layout: paper +pages: 270-288 +publisher: Springer International Publishing +read: false +readings: [] +title: Counterexample Guided Inductive Synthesis Modulo Theories +year: 2018 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:978-3-642-54013-4_12.md b/_staging/10.1007:978-3-642-54013-4_12.md new file mode 100644 index 0000000..6e9031c --- /dev/null +++ b/_staging/10.1007:978-3-642-54013-4_12.md @@ -0,0 +1,23 @@ +--- +ENTRYTYPE: inproceedings +abstract: Compiler optimizations play an increasingly important role in code generation. This is especially true with the advent of resourcelimited mobile + devices. We rely on compiler optimizations to improve performance, reduce code size, and reduce power consumption of our programs. +added: 2024-06-22 +address: Berlin, Heidelberg +authors: +- Nuno P. Lopes +- José Monteiro +booktitle: Verification, Model Checking, and Abstract Interpretation +editor: McMillan, Kenneth L. and Rival, Xavier +isbn: 978-3-642-54013-4 +layout: paper +pages: 203-221 +publisher: Springer Berlin Heidelberg +read: false +readings: [] +title: Weakest Precondition Synthesis for Compiler Optimizations +year: 2014 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:978-3-662-54577-5_18.md b/_staging/10.1007:978-3-662-54577-5_18.md new file mode 100644 index 0000000..a3aec7f --- /dev/null +++ b/_staging/10.1007:978-3-662-54577-5_18.md @@ -0,0 +1,28 @@ +--- +ENTRYTYPE: inproceedings +abstract: Given a semantic constraint specified by a logical formula, and a syntactic constraint specified by a context-free grammar, the Syntax-Guided + Synthesis (SyGuS) problem is to find an expression that satisfies both the syntactic and semantic constraints. An enumerative approach to solve this problem + is to systematically generate all expressions from the syntactic space with some pruning, and has proved to be surprisingly competitive in the newly started + competition of SyGuS solvers. It performs well on small to medium sized benchmarks, produces succinct expressions, and has the ability to generalize from + input-output examples. However, its performance degrades drastically with the size of the smallest solution. To overcome this limitation, in this paper + we propose an alternative approach to solve SyGuS instances. +added: 2024-06-22 +address: Berlin, Heidelberg +authors: +- Rajeev Alur +- Arjun Radhakrishna +- Abhishek Udupa +booktitle: Tools and Algorithms for the Construction and Analysis of Systems +editor: Legay, Axel and Margaria, Tiziana +isbn: 978-3-662-54577-5 +layout: paper +pages: 319-336 +publisher: Springer Berlin Heidelberg +read: false +readings: [] +title: Scaling Enumerative Program Synthesis via Divide and Conquer +year: 2017 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1007:s00236-017-0294-5.md b/_staging/10.1007:s00236-017-0294-5.md new file mode 100644 index 0000000..90bbb1d --- /dev/null +++ b/_staging/10.1007:s00236-017-0294-5.md @@ -0,0 +1,38 @@ +--- +ENTRYTYPE: article +abstract: Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis + methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive + synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional + machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively + querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical + characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants + where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning + algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension + studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of + formal inductive synthesis. +added: 2024-06-22 +address: Berlin, Heidelberg +authors: +- Susmit Jha +- Sanjit A. Seshia +doi: 10.1007/s00236-017-0294-5 +issn: 0001-5903 +issue_date: November 2017 +journal: Acta Inf. +layout: paper +link: https://doi.org/10.1007/s00236-017-0294-5 +month: nov +number: '7' +numpages: '34' +pages: 693-726 +publisher: Springer-Verlag +read: false +readings: [] +title: A theory of formal synthesis via inductive learning +url: https://doi.org/10.1007/s00236-017-0294-5 +volume: '54' +year: 2017 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:1706299.1706345.md b/_staging/10.1145:1706299.1706345.md new file mode 100644 index 0000000..cc43771 --- /dev/null +++ b/_staging/10.1145:1706299.1706345.md @@ -0,0 +1,37 @@ +--- +ENTRYTYPE: inproceedings +abstract: We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have + been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs + us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation + validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.We + present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our + own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging + type errors.Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing + concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations + from expensive-to-run super-optimizers. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Ross Tate +- Michael Stepp +- Sorin Lerner +booktitle: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages +doi: 10.1145/1706299.1706345 +isbn: '9781605584799' +keywords: proof generalization, explanation-based learning, compiler optimization +layout: paper +link: https://doi.org/10.1145/1706299.1706345 +location: Madrid, Spain +numpages: '14' +pages: 389-402 +publisher: Association for Computing Machinery +read: false +readings: [] +series: POPL '10 +title: Generating compiler optimizations from proofs +url: https://doi.org/10.1145/1706299.1706345 +year: 2010 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:1707801.1706345.md b/_staging/10.1145:1707801.1706345.md new file mode 100644 index 0000000..44e5b5b --- /dev/null +++ b/_staging/10.1145:1707801.1706345.md @@ -0,0 +1,39 @@ +--- +ENTRYTYPE: article +abstract: We present an automated technique for generating compiler optimizations from examples of concrete programs before and after improvements have + been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs + us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation + validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable optimization rules.We + present a category-theoretic formalization of our proof generalization technique. This abstraction makes our technique applicable to logics besides our + own. In particular, we demonstrate how our technique can also be used to learn query optimizations for relational databases or to aid programmers in debugging + type errors.Finally, we show experimentally that our technique enables programmers to train a compiler with application-specific optimizations by providing + concrete examples of original programs and the desired transformed programs. We also show how it enables a compiler to learn efficient-to-run optimizations + from expensive-to-run super-optimizers. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Ross Tate +- Michael Stepp +- Sorin Lerner +doi: 10.1145/1707801.1706345 +issn: 0362-1340 +issue_date: January 2010 +journal: SIGPLAN Not. +keywords: proof generalization, explanation-based learning, compiler optimization +layout: paper +link: https://doi.org/10.1145/1707801.1706345 +month: jan +number: '1' +numpages: '14' +pages: 389-402 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Generating compiler optimizations from proofs +url: https://doi.org/10.1145/1707801.1706345 +volume: '45' +year: 2010 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:1993316.1993532.md b/_staging/10.1145:1993316.1993532.md new file mode 100644 index 0000000..6f52a6b --- /dev/null +++ b/_staging/10.1145:1993316.1993532.md @@ -0,0 +1,37 @@ +--- +ENTRYTYPE: article +abstract: Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three + years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested + was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the + results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates + programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code + bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Xuejun Yang +- Yang Chen +- Eric Eide +- John Regehr +doi: 10.1145/1993316.1993532 +issn: 0362-1340 +issue_date: June 2011 +journal: SIGPLAN Not. +keywords: random testing, random program generation, compiler testing, compiler defect, automated testing +layout: paper +link: https://doi.org/10.1145/1993316.1993532 +month: jun +number: '6' +numpages: '12' +pages: 283-294 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Finding and understanding bugs in C compilers +url: https://doi.org/10.1145/1993316.1993532 +volume: '46' +year: 2011 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:1993498.1993532.md b/_staging/10.1145:1993498.1993532.md new file mode 100644 index 0000000..5d7979b --- /dev/null +++ b/_staging/10.1145:1993498.1993532.md @@ -0,0 +1,35 @@ +--- +ENTRYTYPE: inproceedings +abstract: Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three + years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested + was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the + results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates + programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code + bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Xuejun Yang +- Yang Chen +- Eric Eide +- John Regehr +booktitle: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation +doi: 10.1145/1993498.1993532 +isbn: '9781450306638' +keywords: random testing, random program generation, compiler testing, compiler defect, automated testing +layout: paper +link: https://doi.org/10.1145/1993498.1993532 +location: San Jose, California, USA +numpages: '12' +pages: 283-294 +publisher: Association for Computing Machinery +read: false +readings: [] +series: PLDI '11 +title: Finding and understanding bugs in C compilers +url: https://doi.org/10.1145/1993498.1993532 +year: 2011 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2451116.2451150.md b/_staging/10.1145:2451116.2451150.md new file mode 100644 index 0000000..0d78c26 --- /dev/null +++ b/_staging/10.1145:2451116.2451150.md @@ -0,0 +1,34 @@ +--- +ENTRYTYPE: inproceedings +abstract: We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness + and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler is used to rapidly explore the space of all + possible programs to find one that is an optimization of a given target program. Although our method sacrifices completeness, the scope of programs we + are able to consider, and the resulting quality of the programs that we produce, far exceed those of existing superoptimizers. Beginning from binaries + compiled by llvm -O0 for 64-bit x86, our prototype implementation, STOKE, is able to produce programs which either match or outperform the code produced + by gcc -O3, icc -O3, and in some cases, expert handwritten assembly. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Eric Schkufza +- Rahul Sharma +- Alex Aiken +booktitle: Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems +doi: 10.1145/2451116.2451150 +isbn: '9781450318709' +keywords: 64-bit, binary, markov chain monte carlo, mcmc, smt, stochastic search, superoptimization, x86, x86-64 +layout: paper +link: https://doi.org/10.1145/2451116.2451150 +location: Houston, Texas, USA +numpages: '12' +pages: 305-316 +publisher: Association for Computing Machinery +read: false +readings: [] +series: ASPLOS '13 +title: Stochastic superoptimization +url: https://doi.org/10.1145/2451116.2451150 +year: 2013 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2490301.2451150.md b/_staging/10.1145:2490301.2451150.md new file mode 100644 index 0000000..cbf1f6d --- /dev/null +++ b/_staging/10.1145:2490301.2451150.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: article +abstract: We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness + and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler is used to rapidly explore the space of all + possible programs to find one that is an optimization of a given target program. Although our method sacrifices completeness, the scope of programs we + are able to consider, and the resulting quality of the programs that we produce, far exceed those of existing superoptimizers. Beginning from binaries + compiled by llvm -O0 for 64-bit x86, our prototype implementation, STOKE, is able to produce programs which either match or outperform the code produced + by gcc -O3, icc -O3, and in some cases, expert handwritten assembly. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Eric Schkufza +- Rahul Sharma +- Alex Aiken +doi: 10.1145/2490301.2451150 +issn: 0163-5964 +issue_date: March 2013 +journal: SIGARCH Comput. Archit. News +keywords: 64-bit, binary, markov chain monte carlo, mcmc, smt, stochastic search, superoptimization, x86, x86-64 +layout: paper +link: https://doi.org/10.1145/2490301.2451150 +month: mar +number: '1' +numpages: '12' +pages: 305-316 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Stochastic superoptimization +url: https://doi.org/10.1145/2490301.2451150 +volume: '41' +year: 2013 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2499368.2451150.md b/_staging/10.1145:2499368.2451150.md new file mode 100644 index 0000000..2e8d460 --- /dev/null +++ b/_staging/10.1145:2499368.2451150.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: article +abstract: We formulate the loop-free binary superoptimization task as a stochastic search problem. The competing constraints of transformation correctness + and performance improvement are encoded as terms in a cost function, and a Markov Chain Monte Carlo sampler is used to rapidly explore the space of all + possible programs to find one that is an optimization of a given target program. Although our method sacrifices completeness, the scope of programs we + are able to consider, and the resulting quality of the programs that we produce, far exceed those of existing superoptimizers. Beginning from binaries + compiled by llvm -O0 for 64-bit x86, our prototype implementation, STOKE, is able to produce programs which either match or outperform the code produced + by gcc -O3, icc -O3, and in some cases, expert handwritten assembly. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Eric Schkufza +- Rahul Sharma +- Alex Aiken +doi: 10.1145/2499368.2451150 +issn: 0362-1340 +issue_date: April 2013 +journal: SIGPLAN Not. +keywords: 64-bit, binary, markov chain monte carlo, mcmc, smt, stochastic search, superoptimization, x86, x86-64 +layout: paper +link: https://doi.org/10.1145/2499368.2451150 +month: mar +number: '4' +numpages: '12' +pages: 305-316 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Stochastic superoptimization +url: https://doi.org/10.1145/2499368.2451150 +volume: '48' +year: 2013 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2737924.2737965.md b/_staging/10.1145:2737924.2737965.md new file mode 100644 index 0000000..3b29c8a --- /dev/null +++ b/_staging/10.1145:2737924.2737965.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: inproceedings +abstract: Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the + efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together + they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either + proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion + in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures--but largely hides--the detailed + semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, + found that eight of them were wrong. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Nuno P. Lopes +- David Menendez +- Santosh Nagarakatte +- John Regehr +booktitle: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation +doi: 10.1145/2737924.2737965 +isbn: '9781450334686' +keywords: Peephole Optimization, Compiler Verification, Alive +layout: paper +link: https://doi.org/10.1145/2737924.2737965 +location: Portland, OR, USA +numpages: '11' +pages: 22-32 +publisher: Association for Computing Machinery +read: false +readings: [] +series: PLDI '15 +title: Provably correct peephole optimizations with alive +url: https://doi.org/10.1145/2737924.2737965 +year: 2015 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2813885.2737965.md b/_staging/10.1145:2813885.2737965.md new file mode 100644 index 0000000..3798a25 --- /dev/null +++ b/_staging/10.1145:2813885.2737965.md @@ -0,0 +1,38 @@ +--- +ENTRYTYPE: article +abstract: Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the + efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together + they represent a persistent source of bugs. This paper presents Alive, a domain-specific language for writing optimizations and for automatically either + proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion + in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures--but largely hides--the detailed + semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, + found that eight of them were wrong. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Nuno P. Lopes +- David Menendez +- Santosh Nagarakatte +- John Regehr +doi: 10.1145/2813885.2737965 +issn: 0362-1340 +issue_date: June 2015 +journal: SIGPLAN Not. +keywords: Peephole Optimization, Compiler Verification, Alive +layout: paper +link: https://doi.org/10.1145/2813885.2737965 +month: jun +number: '6' +numpages: '11' +pages: 22-32 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Provably correct peephole optimizations with alive +url: https://doi.org/10.1145/2813885.2737965 +volume: '50' +year: 2015 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2837614.2837666.md b/_staging/10.1145:2837614.2837666.md new file mode 100644 index 0000000..d30d5ce --- /dev/null +++ b/_staging/10.1145:2837614.2837666.md @@ -0,0 +1,40 @@ +--- +ENTRYTYPE: inproceedings +abstract: Many advanced programming tools--for both end-users and expert developers--rely on program synthesis to automatically generate implementations + from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms because they require synthesized programs to + be not only correct, but also optimal with respect to a desired cost metric, such as program size. Finding these optimal solutions efficiently requires + domain-specific search strategies, but existing synthesizers hard-code the strategy, making them difficult to reuse. This paper presents metasketches, + a general framework for specifying and solving optimal synthesis problems. metasketches make the search strategy a part of the problem definition by specifying + a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. + A global optimizing search coordinates the activities of local searches, informing them of the costs of potentially-optimal solutions as they explore + different regions of the candidate space in parallel. The local searches execute an incremental form of counterexample-guided inductive synthesis to incorporate + information sent from the global search. We present Synapse, an implementation of these algorithms, and show that it effectively solves optimal synthesis + problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly + controlling the search strategy, and we show that Synapse solves classic synthesis problems that state-of-the-art tools cannot. +added: 2024-06-22 +address: New York, NY, USA +authors: +- James Bornholt +- Emina Torlak +- Dan Grossman +- Luis Ceze +booktitle: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages +doi: 10.1145/2837614.2837666 +isbn: '9781450335492' +keywords: Program synthesis +layout: paper +link: https://doi.org/10.1145/2837614.2837666 +location: St. Petersburg, FL, USA +numpages: '14' +pages: 775-788 +publisher: Association for Computing Machinery +read: false +readings: [] +series: POPL '16 +title: Optimizing synthesis with metasketches +url: https://doi.org/10.1145/2837614.2837666 +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2872362.2872387.md b/_staging/10.1145:2872362.2872387.md new file mode 100644 index 0000000..f5534f8 --- /dev/null +++ b/_staging/10.1145:2872362.2872387.md @@ -0,0 +1,40 @@ +--- +ENTRYTYPE: inproceedings +abstract: Developing a code optimizer is challenging, especially for new, idiosyncratic ISAs. Superoptimization can, in principle, discover machine-specific + optimizations automatically by searching the space of all instruction sequences. If we can increase the size of code fragments a superoptimizer can optimize, + we will be able to discover more optimizations. We develop LENS, a search algorithm that increases the size of code a superoptimizer can synthesize by + rapidly pruning away invalid candidate programs. Pruning is achieved by selectively refining the abstraction under which candidates are considered equivalent, + only in the promising part of the candidate space. LENS also uses a bidirectional search strategy to prune the candidate space from both forward and backward + directions. These pruning strategies allow LENS to solve twice as many benchmarks as existing enumerative search algorithms, while LENS is about 11-times + faster.Additionally, we increase the effective size of the superoptimized fragments by relaxing the correctness condition using contexts (surrounding + code). Finally, we combine LENS with complementary search techniques into a cooperative superoptimizer, which exploits the stochastic search to make random + jumps in a large candidate space, and a symbolic (SAT-solver-based) search to synthesize arbitrary constants. While existing superoptimizers consistently + solve 9-16 out of 32 benchmarks, the cooperative superoptimizer solves 29 benchmarks. It can synthesize code fragments that are up to 82\% faster than + code generated by gcc -O3 from WiBench and MiBench. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Phitchaya Mangpo Phothilimthana +- Aditya Thakur +- Rastislav Bodik +- Dinakar Dhurjati +booktitle: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems +doi: 10.1145/2872362.2872387 +isbn: '9781450340915' +keywords: SMT, program synthesis, superoptimization +layout: paper +link: https://doi.org/10.1145/2872362.2872387 +location: Atlanta, Georgia, USA +numpages: '14' +pages: 297-310 +publisher: Association for Computing Machinery +read: false +readings: [] +series: ASPLOS '16 +title: Scaling up Superoptimization +url: https://doi.org/10.1145/2872362.2872387 +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2914770.2837666.md b/_staging/10.1145:2914770.2837666.md new file mode 100644 index 0000000..4c72233 --- /dev/null +++ b/_staging/10.1145:2914770.2837666.md @@ -0,0 +1,42 @@ +--- +ENTRYTYPE: article +abstract: Many advanced programming tools--for both end-users and expert developers--rely on program synthesis to automatically generate implementations + from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms because they require synthesized programs to + be not only correct, but also optimal with respect to a desired cost metric, such as program size. Finding these optimal solutions efficiently requires + domain-specific search strategies, but existing synthesizers hard-code the strategy, making them difficult to reuse. This paper presents metasketches, + a general framework for specifying and solving optimal synthesis problems. metasketches make the search strategy a part of the problem definition by specifying + a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. + A global optimizing search coordinates the activities of local searches, informing them of the costs of potentially-optimal solutions as they explore + different regions of the candidate space in parallel. The local searches execute an incremental form of counterexample-guided inductive synthesis to incorporate + information sent from the global search. We present Synapse, an implementation of these algorithms, and show that it effectively solves optimal synthesis + problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly + controlling the search strategy, and we show that Synapse solves classic synthesis problems that state-of-the-art tools cannot. +added: 2024-06-22 +address: New York, NY, USA +authors: +- James Bornholt +- Emina Torlak +- Dan Grossman +- Luis Ceze +doi: 10.1145/2914770.2837666 +issn: 0362-1340 +issue_date: January 2016 +journal: SIGPLAN Not. +keywords: Program synthesis +layout: paper +link: https://doi.org/10.1145/2914770.2837666 +month: jan +number: '1' +numpages: '14' +pages: 775-788 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Optimizing synthesis with metasketches +url: https://doi.org/10.1145/2914770.2837666 +volume: '51' +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2954679.2872387.md b/_staging/10.1145:2954679.2872387.md new file mode 100644 index 0000000..e18540b --- /dev/null +++ b/_staging/10.1145:2954679.2872387.md @@ -0,0 +1,42 @@ +--- +ENTRYTYPE: article +abstract: Developing a code optimizer is challenging, especially for new, idiosyncratic ISAs. Superoptimization can, in principle, discover machine-specific + optimizations automatically by searching the space of all instruction sequences. If we can increase the size of code fragments a superoptimizer can optimize, + we will be able to discover more optimizations. We develop LENS, a search algorithm that increases the size of code a superoptimizer can synthesize by + rapidly pruning away invalid candidate programs. Pruning is achieved by selectively refining the abstraction under which candidates are considered equivalent, + only in the promising part of the candidate space. LENS also uses a bidirectional search strategy to prune the candidate space from both forward and backward + directions. These pruning strategies allow LENS to solve twice as many benchmarks as existing enumerative search algorithms, while LENS is about 11-times + faster.Additionally, we increase the effective size of the superoptimized fragments by relaxing the correctness condition using contexts (surrounding + code). Finally, we combine LENS with complementary search techniques into a cooperative superoptimizer, which exploits the stochastic search to make random + jumps in a large candidate space, and a symbolic (SAT-solver-based) search to synthesize arbitrary constants. While existing superoptimizers consistently + solve 9-16 out of 32 benchmarks, the cooperative superoptimizer solves 29 benchmarks. It can synthesize code fragments that are up to 82\% faster than + code generated by gcc -O3 from WiBench and MiBench. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Phitchaya Mangpo Phothilimthana +- Aditya Thakur +- Rastislav Bodik +- Dinakar Dhurjati +doi: 10.1145/2954679.2872387 +issn: 0362-1340 +issue_date: April 2016 +journal: SIGPLAN Not. +keywords: SMT, program synthesis, superoptimization +layout: paper +link: https://doi.org/10.1145/2954679.2872387 +month: mar +number: '4' +numpages: '14' +pages: 297-310 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Scaling up Superoptimization +url: https://doi.org/10.1145/2954679.2872387 +volume: '51' +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2980024.2872387.md b/_staging/10.1145:2980024.2872387.md new file mode 100644 index 0000000..c7b88cc --- /dev/null +++ b/_staging/10.1145:2980024.2872387.md @@ -0,0 +1,42 @@ +--- +ENTRYTYPE: article +abstract: Developing a code optimizer is challenging, especially for new, idiosyncratic ISAs. Superoptimization can, in principle, discover machine-specific + optimizations automatically by searching the space of all instruction sequences. If we can increase the size of code fragments a superoptimizer can optimize, + we will be able to discover more optimizations. We develop LENS, a search algorithm that increases the size of code a superoptimizer can synthesize by + rapidly pruning away invalid candidate programs. Pruning is achieved by selectively refining the abstraction under which candidates are considered equivalent, + only in the promising part of the candidate space. LENS also uses a bidirectional search strategy to prune the candidate space from both forward and backward + directions. These pruning strategies allow LENS to solve twice as many benchmarks as existing enumerative search algorithms, while LENS is about 11-times + faster.Additionally, we increase the effective size of the superoptimized fragments by relaxing the correctness condition using contexts (surrounding + code). Finally, we combine LENS with complementary search techniques into a cooperative superoptimizer, which exploits the stochastic search to make random + jumps in a large candidate space, and a symbolic (SAT-solver-based) search to synthesize arbitrary constants. While existing superoptimizers consistently + solve 9-16 out of 32 benchmarks, the cooperative superoptimizer solves 29 benchmarks. It can synthesize code fragments that are up to 82\% faster than + code generated by gcc -O3 from WiBench and MiBench. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Phitchaya Mangpo Phothilimthana +- Aditya Thakur +- Rastislav Bodik +- Dinakar Dhurjati +doi: 10.1145/2980024.2872387 +issn: 0163-5964 +issue_date: May 2016 +journal: SIGARCH Comput. Archit. News +keywords: SMT, program synthesis, superoptimization +layout: paper +link: https://doi.org/10.1145/2980024.2872387 +month: mar +number: '2' +numpages: '14' +pages: 297-310 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Scaling up Superoptimization +url: https://doi.org/10.1145/2980024.2872387 +volume: '44' +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:2983990.2984006.md b/_staging/10.1145:2983990.2984006.md new file mode 100644 index 0000000..deabd3b --- /dev/null +++ b/_staging/10.1145:2983990.2984006.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: inproceedings +abstract: 'Machine-code synthesis is the problem of searching for an instruction sequence that implements a semantic specification, given as a formula in + quantifier-free bit-vector logic (QFBV). Instruction sets like Intel''s IA-32 have around 43,000 unique instruction schemas; this huge instruction pool, + along with the exponential cost inherent in enumerative synthesis, results in an enormous search space for a machine-code synthesizer: even for relatively + small specifications, the synthesizer might take several hours or days to find an implementation. In this paper, we present several improvements to the + algorithms used in a state-of-the-art machine-code synthesizer McSynth. In addition to a novel pruning heuristic, our improvements incorporate a number + of ideas known from the literature, which we adapt in novel ways for the purpose of speeding up machine-code synthesis. Our experiments for Intel''s IA-32 + instruction set show that our improvements enable synthesis of code for 12 out of 14 formulas on which McSynth times out, speeding up the synthesis time + by at least 1981X, and for the remaining formulas, speeds up synthesis by 3X.' +added: 2024-06-22 +address: New York, NY, USA +authors: +- Venkatesh Srinivasan +- Tushar Sharma +- Thomas Reps +booktitle: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications +doi: 10.1145/2983990.2984006 +isbn: '9781450344449' +keywords: pruning heuristics, move-to-front heuristic, flow independence, flattening deep terms, Machine-code synthesis, IA-32 instruction set +layout: paper +link: https://doi.org/10.1145/2983990.2984006 +location: Amsterdam, Netherlands +numpages: '16' +pages: 165-180 +publisher: Association for Computing Machinery +read: false +readings: [] +series: OOPSLA 2016 +title: Speeding up machine-code synthesis +url: https://doi.org/10.1145/2983990.2984006 +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3022671.2984006.md b/_staging/10.1145:3022671.2984006.md new file mode 100644 index 0000000..6e85992 --- /dev/null +++ b/_staging/10.1145:3022671.2984006.md @@ -0,0 +1,38 @@ +--- +ENTRYTYPE: article +abstract: 'Machine-code synthesis is the problem of searching for an instruction sequence that implements a semantic specification, given as a formula in + quantifier-free bit-vector logic (QFBV). Instruction sets like Intel''s IA-32 have around 43,000 unique instruction schemas; this huge instruction pool, + along with the exponential cost inherent in enumerative synthesis, results in an enormous search space for a machine-code synthesizer: even for relatively + small specifications, the synthesizer might take several hours or days to find an implementation. In this paper, we present several improvements to the + algorithms used in a state-of-the-art machine-code synthesizer McSynth. In addition to a novel pruning heuristic, our improvements incorporate a number + of ideas known from the literature, which we adapt in novel ways for the purpose of speeding up machine-code synthesis. Our experiments for Intel''s IA-32 + instruction set show that our improvements enable synthesis of code for 12 out of 14 formulas on which McSynth times out, speeding up the synthesis time + by at least 1981X, and for the remaining formulas, speeds up synthesis by 3X.' +added: 2024-06-22 +address: New York, NY, USA +authors: +- Venkatesh Srinivasan +- Tushar Sharma +- Thomas Reps +doi: 10.1145/3022671.2984006 +issn: 0362-1340 +issue_date: October 2016 +journal: SIGPLAN Not. +keywords: pruning heuristics, move-to-front heuristic, flow independence, flattening deep terms, Machine-code synthesis, IA-32 instruction set +layout: paper +link: https://doi.org/10.1145/3022671.2984006 +month: oct +number: '10' +numpages: '16' +pages: 165-180 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Speeding up machine-code synthesis +url: https://doi.org/10.1145/3022671.2984006 +volume: '51' +year: 2016 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3062341.3062372.md b/_staging/10.1145:3062341.3062372.md new file mode 100644 index 0000000..f4f0cfe --- /dev/null +++ b/_staging/10.1145:3062341.3062372.md @@ -0,0 +1,34 @@ +--- +ENTRYTYPE: inproceedings +abstract: Peephole optimizations are a common source of compiler bugs. Compiler developers typically transform an incorrect peephole optimization into a + valid one by strengthening the precondition. This process is challenging and tedious. This paper proposes Alive-Infer, a data-driven approach that infers + preconditions for peephole optimizations expressed in Alive. Alive-Infer generates positive and negative examples for an optimization, enumerates predicates + on-demand, and learns a set of predicates that separate the positive and negative examples. Alive-Infer repeats this process until it finds a precondition + that ensures the validity of the optimization. Alive-Infer reports both a weakest precondition and a set of succinct partial preconditions to the developer. + Our prototype generates preconditions that are weaker than LLVM's preconditions for 73 optimizations in the Alive suite. We also demonstrate the applicability + of this technique to generalize 54 optimization patterns generated by Souper, an LLVM IR-based superoptimizer. +added: 2024-06-22 +address: New York, NY, USA +authors: +- David Menendez +- Santosh Nagarakatte +booktitle: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation +doi: 10.1145/3062341.3062372 +isbn: '9781450349888' +keywords: Alive, Compilers, Inference, Learning +layout: paper +link: https://doi.org/10.1145/3062341.3062372 +location: Barcelona, Spain +numpages: '15' +pages: 49-63 +publisher: Association for Computing Machinery +read: false +readings: [] +series: PLDI 2017 +title: 'Alive-Infer: data-driven precondition inference for peephole optimizations in LLVM' +url: https://doi.org/10.1145/3062341.3062372 +year: 2017 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3140587.3062372.md b/_staging/10.1145:3140587.3062372.md new file mode 100644 index 0000000..3cbc7cb --- /dev/null +++ b/_staging/10.1145:3140587.3062372.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: article +abstract: Peephole optimizations are a common source of compiler bugs. Compiler developers typically transform an incorrect peephole optimization into a + valid one by strengthening the precondition. This process is challenging and tedious. This paper proposes Alive-Infer, a data-driven approach that infers + preconditions for peephole optimizations expressed in Alive. Alive-Infer generates positive and negative examples for an optimization, enumerates predicates + on-demand, and learns a set of predicates that separate the positive and negative examples. Alive-Infer repeats this process until it finds a precondition + that ensures the validity of the optimization. Alive-Infer reports both a weakest precondition and a set of succinct partial preconditions to the developer. + Our prototype generates preconditions that are weaker than LLVM's preconditions for 73 optimizations in the Alive suite. We also demonstrate the applicability + of this technique to generalize 54 optimization patterns generated by Souper, an LLVM IR-based superoptimizer. +added: 2024-06-22 +address: New York, NY, USA +authors: +- David Menendez +- Santosh Nagarakatte +doi: 10.1145/3140587.3062372 +issn: 0362-1340 +issue_date: June 2017 +journal: SIGPLAN Not. +keywords: Alive, Compilers, Inference, Learning +layout: paper +link: https://doi.org/10.1145/3140587.3062372 +month: jun +number: '6' +numpages: '15' +pages: 49-63 +publisher: Association for Computing Machinery +read: false +readings: [] +title: 'Alive-Infer: data-driven precondition inference for peephole optimizations in LLVM' +url: https://doi.org/10.1145/3140587.3062372 +volume: '52' +year: 2017 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3368826.3377927.md b/_staging/10.1145:3368826.3377927.md new file mode 100644 index 0000000..6aa8186 --- /dev/null +++ b/_staging/10.1145:3368826.3377927.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: inproceedings +abstract: Static analyses compute properties of programs that are true in all executions, and compilers use these properties to justify optimizations such + as dead code elimination. Each static analysis in a compiler should be as precise as possible while remaining sound and being sufficiently fast. Unsound + static analyses typically lead to miscompilations, whereas imprecisions typically lead to missed optimizations. Neither kind of bug is easy to track down. Our + research uses formal methods to help compiler developers create better static analyses. Our contribution is the design and evaluation of several algorithms + for computing sound and maximally precise static analysis results using an SMT solver. These methods are too slow to use at compile time, but they can + be used offline to find soundness and precision errors in a production compiler such as LLVM. We found no new soundness bugs in LLVM, but we can discover + previously-fixed soundness errors that we re-introduced into the code base. We identified many imprecisions in LLVM's static analyses, some of which have + been fixed as a result of our work. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Jubi Taneja +- Zhengyang Liu +- John Regehr +booktitle: Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization +doi: 10.1145/3368826.3377927 +isbn: '9781450370479' +keywords: Soundness, Precision, Dataflow analysis +layout: paper +link: https://doi.org/10.1145/3368826.3377927 +location: San Diego, CA, USA +numpages: '13' +pages: 81-93 +publisher: Association for Computing Machinery +read: false +readings: [] +series: CGO 2020 +title: Testing static analyses for precision and soundness +url: https://doi.org/10.1145/3368826.3377927 +year: 2020 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3371080.md b/_staging/10.1145:3371080.md new file mode 100644 index 0000000..03dd90e --- /dev/null +++ b/_staging/10.1145:3371080.md @@ -0,0 +1,46 @@ +--- +ENTRYTYPE: article +abstract: 'We consider the problem of type-directed component-based synthesis where, given a set of (typed) components and a query type, the goal is to + synthesize a term that inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries + of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for Java do scale, but only apply + to monomorphic data and components: polymorphic data and components infinitely explode the size of the graph that must be searched, rendering synthesis + intractable. We introduce type-guided abstraction refinement (TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and + components. Our key insight is that we can overcome the explosion by building a graph over abstract types which represent a potentially unbounded set + of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that uses proofs + of untypeability of ill-typed candidates to iteratively refine the abstraction until a well-typed result is found. We have implemented TYGAR in H+, a + tool that takes as input a set of Haskell libraries and a query type, and returns a Haskell term that uses functions from the provided libraries to implement + the query type. Our support for polymorphism allows H+ to work with higher-order functions and type classes, and enables more precise queries due to parametricity. + We have evaluated H+ on 44 queries using a set of popular Haskell libraries with a total of 291 components. H+ returns an interesting solution within + the first five results for 32 out of 44 queries. Our results show that TYGAR allows H+ to rapidly return well-typed terms, with the median time to first + solution of just 1.4 seconds. Moreover, we observe that gains from iterative refinement over exhaustive enumeration are more pronounced on harder queries.' +added: 2024-06-22 +address: New York, NY, USA +articleno: '12' +authors: +- Zheng Guo +- Michael James +- David Justo +- Jiaxiao Zhou +- Ziteng Wang +- Ranjit Jhala +- Nadia Polikarpova +doi: 10.1145/3371080 +issue_date: January 2020 +journal: Proc. ACM Program. Lang. +keywords: Abstract Interpretation, Program Synthesis, Type Systems +layout: paper +link: https://doi.org/10.1145/3371080 +month: dec +number: POPL +numpages: '28' +publisher: Association for Computing Machinery +read: false +readings: [] +title: Program synthesis by type-guided abstraction refinement +url: https://doi.org/10.1145/3371080 +volume: '4' +year: 2019 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3428245.md b/_staging/10.1145:3428245.md new file mode 100644 index 0000000..fbf0191 --- /dev/null +++ b/_staging/10.1145:3428245.md @@ -0,0 +1,39 @@ +--- +ENTRYTYPE: article +abstract: 'Superoptimization is a compilation strategy that uses search to improve code quality, rather than relying on a canned sequence of transformations, + as traditional optimizing compilers do. This search can be seen as a program synthesis problem: from unoptimized code serving as a specification, the + synthesis procedure attempts to create a more efficient implementation. An important family of synthesis algorithms works by enumerating candidates and + then successively checking if each refines the specification, using an SMT solver. The contribution of this paper is a pruning technique which reduces + the enumerative search space using fast dataflow-based techniques to discard synthesis candidates that contain symbolic constants and uninstantiated instructions. + We demonstrate the effectiveness of this technique by improving the runtime of an enumerative synthesis procedure in the Souper superoptimizer for the + LLVM intermediate representation. The techniques presented in this paper eliminate 65\% of the solver calls made by Souper, making it 2.32x faster (14.54 + hours vs 33.76 hours baseline, on a large multicore) at solving all 269,113 synthesis problems that Souper encounters when optimizing the C and C++ programs + from SPEC CPU 2017.' +added: 2024-06-22 +address: New York, NY, USA +articleno: '177' +authors: +- Manasij Mukherjee +- Pranav Kant +- Zhengyang Liu +- John Regehr +doi: 10.1145/3428245 +issue_date: November 2020 +journal: Proc. ACM Program. Lang. +keywords: abstract interpretation, program synthesis, pruning, superoptimization +layout: paper +link: https://doi.org/10.1145/3428245 +month: nov +number: OOPSLA +numpages: '24' +publisher: Association for Computing Machinery +read: false +readings: [] +title: Dataflow-based pruning for speeding up superoptimization +url: https://doi.org/10.1145/3428245 +volume: '4' +year: 2020 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3453483.3454030.md b/_staging/10.1145:3453483.3454030.md new file mode 100644 index 0000000..f6a1cf7 --- /dev/null +++ b/_staging/10.1145:3453483.3454030.md @@ -0,0 +1,37 @@ +--- +ENTRYTYPE: inproceedings +abstract: 'We designed, implemented, and deployed Alive2: a bounded translation validation tool for the LLVM compiler''s intermediate representation (IR). + It limits resource consumption by, for example, unrolling loops up to some bound, which means there are circumstances in which it misses bugs. Alive2 + is designed to avoid false alarms, is fully automatic through the use of an SMT solver, and requires no changes to LLVM. By running Alive2 over LLVM''s + unit test suite, we discovered and reported 47 new bugs, 28 of which have been fixed already. Moreover, our work has led to eight patches to the LLVM + Language Reference-the definitive description of the semantics of its IR-and we have participated in numerous discussions with the goal of clarifying + ambiguities and fixing errors in these semantics. Alive2 is open source and we also made it available on the web, where it has active users from the LLVM + community.' +added: 2024-06-22 +address: New York, NY, USA +authors: +- Nuno P. Lopes +- Juneyoung Lee +- Chung-Kil Hur +- Zhengyang Liu +- John Regehr +booktitle: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation +doi: 10.1145/3453483.3454030 +isbn: '9781450383912' +keywords: Translation Validation, IR Semantics, Compilers, Automatic Software Verification +layout: paper +link: https://doi.org/10.1145/3453483.3454030 +location: Virtual, Canada +numpages: '15' +pages: 65-79 +publisher: Association for Computing Machinery +read: false +readings: [] +series: PLDI 2021 +title: 'Alive2: bounded translation validation for LLVM' +url: https://doi.org/10.1145/3453483.3454030 +year: 2021 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3563334.md b/_staging/10.1145:3563334.md new file mode 100644 index 0000000..cc8ddc2 --- /dev/null +++ b/_staging/10.1145:3563334.md @@ -0,0 +1,40 @@ +--- +ENTRYTYPE: article +abstract: This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers + in a fashion similar to the way yacc automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides + specifications of (i) the concrete semantics of a given operation op, (ii) the abstract domain A to be used by the analyzer, and (iii) the semantics of + a domain-specific language L in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for op in abstract + domain A, expressed in L (an "L-transformer for op over A"). Moreover, the abstract transformer obtained is a most-precise L-transformer for op over A; + that is, there is no other L-transformer for op over A that is strictly more precise. We implemented our method in a tool called AMURTH. We used AMURTH + to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, + when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, + which demonstrates the risk of using manually created transformers. +added: 2024-06-22 +address: New York, NY, USA +articleno: '171' +authors: +- Pankaj Kumar Kalita +- Sujit Kumar Muduli +- Loris D'Antoni +- Thomas Reps +- Subhajit Roy +doi: 10.1145/3563334 +issue_date: October 2022 +journal: Proc. ACM Program. Lang. +keywords: DSL, abstract transformer, program synthesis +layout: paper +link: https://doi.org/10.1145/3563334 +month: oct +number: OOPSLA2 +numpages: '29' +publisher: Association for Computing Machinery +read: false +readings: [] +title: Synthesizing abstract transformers +url: https://doi.org/10.1145/3563334 +volume: '6' +year: 2022 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:3649837.md b/_staging/10.1145:3649837.md new file mode 100644 index 0000000..426fe4d --- /dev/null +++ b/_staging/10.1145:3649837.md @@ -0,0 +1,36 @@ +--- +ENTRYTYPE: article +abstract: Optimizing compilers rely on peephole optimizations to simplify combinations of instructions and remove redundant instructions. Typically, + a new peephole optimization is added when a compiler developer notices an optimization opportunity--a collection of dependent instructions that can + be improved--and manually derives a more general rewrite rule that optimizes not only the original code, but also other, similar collections of instructions. In + this paper, we present Hydra, a tool that automates the process of generalizing peephole optimizations using a collection of techniques centered on + program synthesis. One of the most important problems we have solved is finding a version of each optimization that is independent of the bitwidths + of the optimization's inputs (when this version exists). We show that Hydra can generalize 75\% of the ungeneralized missed peephole optimizations + that LLVM developers have posted to the LLVM project's issue tracker. All of Hydra's generalized peephole optimizations have been formally verified, + and furthermore we can automatically turn them into C++ code that is suitable for inclusion in an LLVM pass. +added: 2024-06-22 +address: New York, NY, USA +articleno: '120' +authors: +- Manasij Mukherjee +- John Regehr +doi: 10.1145/3649837 +issue_date: April 2024 +journal: Proc. ACM Program. Lang. +keywords: alive2, generalization, hydra, llvm, peephole optimization, program synthesis, souper, superoptimization +layout: paper +link: https://doi.org/10.1145/3649837 +month: apr +number: OOPSLA1 +numpages: '29' +publisher: Association for Computing Machinery +read: false +readings: [] +title: 'Hydra: Generalizing Peephole Optimizations with Program Synthesis' +url: https://doi.org/10.1145/3649837 +volume: '8' +year: 2024 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:364995.365000.md b/_staging/10.1145:364995.365000.md new file mode 100644 index 0000000..e5c11bd --- /dev/null +++ b/_staging/10.1145:364995.365000.md @@ -0,0 +1,29 @@ +--- +ENTRYTYPE: article +abstract: Redundant instructions may be discarded during the final stage of compilation by using a simple optimizing technique called peephole optimization. + The method is described and examples are given. +added: 2024-06-22 +address: New York, NY, USA +authors: +- W. M. McKeeman +doi: 10.1145/364995.365000 +issn: 0001-0782 +issue_date: July 1965 +journal: Communications of the ACM +layout: paper +link: https://doi.org/10.1145/364995.365000 +month: jul +number: '7' +numpages: '2' +pages: 443-444 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Peephole optimization +url: https://doi.org/10.1145/364995.365000 +volume: '8' +year: 1965 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:502874.502885.md b/_staging/10.1145:502874.502885.md new file mode 100644 index 0000000..34b5ea5 --- /dev/null +++ b/_staging/10.1145:502874.502885.md @@ -0,0 +1,29 @@ +--- +ENTRYTYPE: inproceedings +abstract: This paper describes a system that automatically generates peephole optimizations. A general peephole optimizer driven by a machine description + produces optimizations at compile-compile time for a fast, pattern-directed, compile-time optimizer. They form part of a compiler that simplifies retargeting + by substituting peephole optimization for case analysis. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Jack W. Davidson +- Christopher W. Fraser +booktitle: Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction +doi: 10.1145/502874.502885 +isbn: 0897911393 +layout: paper +link: https://doi.org/10.1145/502874.502885 +location: Montreal, Canada +numpages: '6' +pages: 111-116 +publisher: Association for Computing Machinery +read: false +readings: [] +series: SIGPLAN '84 +title: Automatic generation of peephole optimizations +url: https://doi.org/10.1145/502874.502885 +year: 1984 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/10.1145:502949.502885.md b/_staging/10.1145:502949.502885.md new file mode 100644 index 0000000..5384625 --- /dev/null +++ b/_staging/10.1145:502949.502885.md @@ -0,0 +1,31 @@ +--- +ENTRYTYPE: article +abstract: This paper describes a system that automatically generates peephole optimizations. A general peephole optimizer driven by a machine description + produces optimizations at compile-compile time for a fast, pattern-directed, compile-time optimizer. They form part of a compiler that simplifies retargeting + by substituting peephole optimization for case analysis. +added: 2024-06-22 +address: New York, NY, USA +authors: +- Jack W. Davidson +- Christopher W. Fraser +doi: 10.1145/502949.502885 +issn: 0362-1340 +issue_date: June 1984 +journal: SIGPLAN Not. +layout: paper +link: https://doi.org/10.1145/502949.502885 +month: jun +number: '6' +numpages: '6' +pages: 111-116 +publisher: Association for Computing Machinery +read: false +readings: [] +title: Automatic generation of peephole optimizations +url: https://doi.org/10.1145/502949.502885 +volume: '19' +year: 1984 +notes: +papers: +--- +{% include links.html %} diff --git a/_staging/6679385.md b/_staging/6679385.md new file mode 100644 index 0000000..07b0d2a --- /dev/null +++ b/_staging/6679385.md @@ -0,0 +1,29 @@ +--- +ENTRYTYPE: inproceedings +added: 2024-06-22 +authors: +- Rajeev Alur +- Rastislav Bodik +- Garvit Juniwal +- Milo M. K. Martin +- Mukund Raghothaman +- Sanjit A. Seshia +- Rishabh Singh +- Armando Solar-Lezama +- Emina Torlak +- Abhishek Udupa +booktitle: 2013 Formal Methods in Computer-Aided Design +doi: 10.1109/FMCAD.2013.6679385 +keywords: Grammar;Syntactics;Heuristic algorithms;Concrete;Search problems;Libraries;Production +layout: paper +number: '' +pages: 1-8 +read: false +readings: [] +title: Syntax-guided synthesis +volume: '' +year: 2013 +notes: +papers: +--- +{% include links.html %}