[PLDI24] SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)

Описание: SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques (Video, PLDI 2024)
Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, and Peter J. Stuckey
(Complutense University of Madrid, Spain; Monash University, Australia; Complutense University of Madrid, Spain; Monash University, Australia; Complutense University of Madrid, Spain; Monash University, Australia)

Abstract: Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed, and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named SuperStack, which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.

Article: https://doi.org/10.1145/3656435

Supplementary archive: https://doi.org/10.5281/zenodo.10801691 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)

ORCID: https://orcid.org/0000-0003-0048-0705, https://orcid.org/0000-0002-6666-514X, https://orcid.org/0000-0003-2109-8863, https://orcid.org/0000-0002-4535-2902, https://orcid.org/0000-0002-0501-9830, https://orcid.org/0000-0003-2186-0459

Video Tags: Superoptimization, Program Synthesis, SAT, EVM, WebAssembly, pldi24main-p416-p, doi:10.1145/3656435, doi:10.5281/zenodo.10801691, orcid:0000-0003-0048-0705, orcid:0000-0002-6666-514X, orcid:0000-0003-2109-8863, orcid:0000-0002-4535-2902, orcid:0000-0002-0501-9830, orcid:0000-0003-2186-0459, Artifacts Available, Artifacts Evaluated — Reusable

Presentation at the PLDI 2024 conference, June 24–28, 2024, https://pldi24.sigplan.org/
Sponsored by ACM SIGPLAN,