Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection

“Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection” by Ross Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark Barrett, and Pat Hanrahan. In Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), (Nina Narodytska and Philipp Rümmer, eds.), Oct. 2024, pp. 8-17. Prague, Czech Republic.

Abstract

Compiling programs to an instruction set architecture (ISA) requires a set of rewrite rules that map patterns consisting of compiler instructions to patterns consisting of ISA instructions. We synthesize such rules by constructing SMT queries, whose solutions represent two functionally equivalent programs. These two programs are interpreted as an instruction selection rewrite rule. Existing work is limited to single-instruction ISA patterns, whereas our solution does not have that restriction. Furthermore, we address inefficiencies of existing work by developing two optimized algorithms. The first only generates unique rules by preventing synthesis of duplicate and composite rules. The second only generates lowest-cost rules by preventing synthesis of higher-cost rules. We evaluate our algorithms on multiple ISAs. Without our optimizations, the vast majority of synthesized rewrite rules are either duplicates, composites, or higher cost. Our optimizations result in synthesis speed-ups of up to 768x and 4004x for the two algorithms.

BibTeX entry:

@inproceedings{DDT+24,
   author = {Ross Daly and Caleb Donovick and Caleb Terrill and Jackson
	Melchert and Priyanka Raina and Clark Barrett and Pat Hanrahan},
   editor = {Nina Narodytska and Philipp R{\"u}mmer},
   title = {Efficiently Synthesizing Lowest Cost Rewrite Rules for
	Instruction Selection},
   booktitle = {Proceedings of the {\it 24^{th}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '24)},
   pages = {8--17},
   publisher = {TU Wien Academic Press},
   month = oct,
   year = {2024},
   doi = {10.34727/2024/isbn.978-3-85448-065-5_7},
   note = {Prague, Czech Republic},
   url = {https://repositum.tuwien.at/handle/20.500.12708/200774}
}

(This webpage was created with bibtex2web.)