Arrow Research search
Back to LOPSTR

LOPSTR 2024

Parallel Assembly Synthesis

Conference Paper Synthesis and Transformation Formal Methods ยท Logic in Computer Science

Abstract

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.

Authors

Keywords

No keywords are indexed for this paper.

Context

Venue
International Symposium on Logic-Based Program Synthesis and Transformation
Archive span
1990-2025
Indexed papers
560
Paper id
952350859106538666
v2026.09.13