Parallel Assembly Synthesis

Published in International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'24), 2024

Download paper here
Recommended Citation Jingmei Hu, Stephen Chong, Margo Seltzer. 2024. Logic-Based Program Synthesis and Transformation. LOPSTR 2024. DOI:https://doi.org/10.1007/978-3-031-71294-4_1.

Abstract

Program synthesis offers an attractive alternative to the intricate and tedious process of writing assembly programs manually. Assembly program synthesis automatically generates implementations, given a high-level formal specification and a machine description. However, its limited scalability prevents widespread adoption. Automatic parallelization improves program synthesis in general, but parallelizing assembly synthesis is nontrivial as the realities that data are untyped and all state is global lead to an enormous search space and prevent straightforward decomposition into separable sub-problems that can be run in parallel. We present PASSES, a Parallel Assembly Synthesis System Exploiting Subspaces. PASSES uses five heuristics to transform an original assembly synthesis problem into a set of sub-problems; it runs multiple synthesis sub-problems in parallel and constructs the final result by combining them. We evaluate PASSES on 26 general bit manipulation assembly programming problems and 140 machine-dependent use cases from two operating systems. Compared to an existing assembly synthesis tool and a state-of-the-art parallel SMT solver, all five heuristics in PASSES significantly improve assembly synthesis scalability.