Denali: a goal-directed superoptimizer

By Rajeev Joshi, Greg Nelson, Keith H. Randall. 2002

199 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Hardware and Architecture, Optimization & Training

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Hardware and Architecture

In Optimization & Training

Citations in the corpus

CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis (2022, background): “Previous work (Joshi et al., 2002; Panchekha et al., 2015; Cheung et al., 2013) leverages domain-specific language to restrict the search space; however, this limits the applicability of synthesized programs.”
Contrastive Code Representation Learning (2020, background): “Yet, crowdsourcing equivalent programs from GitHub is difﬁcult as verifying equivalence is un-decidable (Joshi et al., 2002; Bansal and Aiken, 2006) and approximate veriﬁcation is costly and runs untrusted code (Massalin, 1987).”
Pioneer: verifying code integrity and enforcing untampered code execution on legacy systems (2005, methodology): “Promising research directions to achieve a proof of optimality are tools such as Denali [15] or superopt [10] that automatically generate the most optimal code sequence for basic code blocks in a program.”
SWATT: softWare-based attestation for embedded devices (2004, methodology): “Joshi, Nelson and Randall propose a superoptimizer, Denali, that uses an automatic theorem prover to generate a nearly mathematically optimal straight line machine code sequence, that evaluates a given set of expressions using the minimal possible instruction count on a given architecture [8].”
Oracle-guided component-based program synthesis (2010, methodology): “…Program Synthesis Susmit Jha Sumit Gulwani Sanjit A. Seshia Ashish Tiwari UC Berkeley Microsoft Research UC Berkeley SRI International jha@eecs.berkeley.edu sumitg@microsoft.com sseshia@eecs.berkeley.edu tiwari@csl.sri.com ABSTRACT We present a novel approach to automatic synthesis of…”
Program Synthesis (2017, methodology): “The control structure of the program may be restricted to a user-provided looping template [135], a partial program with holes [132], straight-line programs [8, 47, 63, 87, 109], or a guarded statement set with control flow at the very top [43].”
Synthesis of loop-free programs (2011, methodology): “In this paper, we demonstrate how to semi-automate the discovery of small, but intricate, bitvector programs using the currently available formal veri.cation technology.”
Component-based synthesis for complex APIs (2017, methodology): “The DENALI tool for super-optimization performs graph reachability analysis to generate more efficient, but semantically equivalent code [23].”
Stochastic superoptimization (2012, methodology): “Denali [11], and the more recent Equality Saturation technique [18], attempt to gain scalability by only considering programs that are known to be equal to the input program.”
Simplify: a theorem prover for program checking (2005, methodology): “This method was used in the Denali superoptimizer [Joshi et al. 2002], which uses Simplify-like techniques to generate provably optimal machine code.”
Compiler validation via equivalence modulo inputs (2014, unknown): “Extending work on super-optimization [3, 11, 15], in particular Denali [11], Tate et al. introduce the Peggy optimization and translation validation framework for JVM based on equality saturation [25].”
Automatic performance tuning of sparse matrix kernels (2003, methodology): “, substitute exhaustive search in Massalin’s superoptimizer with an automated theorem prover in their Denali superoptimizer [181].”
A Conversational Paradigm for Program Synthesis (2022, background): “Previous work (Joshi et al., 2002; Panchekha et al., 2015; Cheung et al., 2013) leverages domain-specific language to restrict the search space; however, this limits the applicability of the synthesized programs.”
Equality saturation: a new approach to optimization (2009, methodology): “Denali represents the computations performed in the basic block as an expression graph, and applies axioms to create an E-graph data structure representing the various ways of computing the values in the basic block.”