arXiv:2601.02653 · v3

Prophecy Variables, Program Analysis, Binding Times, and Staged Compilation in the BuildIt System

首次提交 2026-01-06 10:06

版本更新 2026-11-12 02:27

雷达观测 2026-11-13 14:16

摘要

BuildIt is a lightweight C++ library system for implementing domain specific languages (DSLs) and compilers through multi-stage execution. It uses partial evaluation to generate optimized code without requiring parsers, explicit intermediate representations (IRs), or custom code generators. History variables and forward execution support analyses of past computation, but optimizations such as data movement, operator fusion, and binding-time analysis also require information about future execution. We introduce prophecy variables into BuildIt to predict future program behavior and guide code generation. Repeated first-stage execution refines predictions until they satisfy the program's checks, extending BuildIt's existing reexecution machinery with little additional complexity. This approach obtains information typically computed by backwards dataflow analyses over an explicit IR while preserving BuildIt's lightweight implementation model. The cost of first-stage reexecution can be amortized over repeated executions of the generated code. We formalize the mechanism and mechanize its guarantees in Lean 4. We demonstrate prophecy variables in three applications: selective CPU-GPU data movement, neural-network operator fusion, and automatic binding-time analysis. These applications achieve performance improvements of up to 5.5x while simplifying the programming interface.