research-article

Synthesizing an instruction selection rule library from semantic specifications

Authors:

Sebastian Buchwald,

Sebastian HackAuthors Info & Claims

CGO '18: Proceedings of the 2018 International Symposium on Code Generation and Optimization

Pages 300 - 313

https://doi.org/10.1145/3168821

Published: 24 February 2018 Publication History

Abstract

Instruction selection is the part of a compiler that transforms intermediate representation (IR) code into machine code. Instruction selectors build on a library of hundreds if not thousands of rules. Creating and maintaining these rules is a tedious and error-prone manual process.

In this paper, we present a fully automatic approach to create provably correct rule libraries from formal specifications of the instruction set architecture and the compiler IR. We use a hybrid approach that combines enumerative techniques with template-based counterexample-guided inductive synthesis (CEGIS). Thereby, we overcome several shortcomings of existing approaches, which were not able to handle complex instructions in a reasonable amount of time. In particular, we efficiently model memory operations.

Our tool synthesized a large part of the integer arithmetic rules for the x86 architecture within a few days where existing techniques could not deliver a substantial rule library within weeks. Using the rule library, we generate a prototype instruction selector that produces code on par with a manually-tuned instruction selector. Furthermore, using 63012 test cases generated from the rule library, we identified 29498 rules that both Clang and GCC miss.

References

[1]

R. Alur, R. Bodik, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1-s8.

[2]

Sorav Bansal and Alex Aiken. 2006. Automatic Generation of Peephole Superoptimizers. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XII). ACM, New York, NY, USA, 394-403.

Digital Library

[3]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). (2016). http://www.smt-lib.org

[4]

Gabriel Hjort Blindell. 2016. Instruction Selection: Principles, Methods, and Applications (1st ed.). Springer Publishing Company, Incorporated.

Digital Library

[5]

Sebastian Buchwald. 2015. Optgen: A Generator for Local Optimizations. Springer Berlin Heidelberg, Berlin, Heidelberg, 171-189.

[6]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337-340.

Digital Library

[7]

João Dias and Norman Ramsey. 2010. Automatically Generating Instruction Selectors Using Declarative Machine Descriptions. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10). ACM, New York, NY, USA, 403-416.

Digital Library

[8]

Dietmar Ebner, Florian Brandner, Bernhard Scholz, Andreas Krall, Peter Wiedermann, and Albrecht Kadlec. 2008. Generalized instruction selection using SSA-graphs. In Proceedings of the 2008 ACM SIGPLAN/ SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'08), Tucson, AZ, USA, June 12-13, 2008, Krisztián Flautner and John Regehr (Eds.). ACM, 31-40.

Digital Library

[9]

Erik Eckstein, Oliver Konig, and Bernhard Scholz. 2003. Code Instruction Selection Based on SSA-Graphs. In Software and Compilers for Embedded Systems, 7th International Workshop, SCOPES 2003, Vienna, Austria, September 24-26, 2003, Proceedings (Lecture Notes in Computer Science), Andreas Krall (Ed.), Vol. 2826. Springer, 49-65.

[10]

Patrice Godefroid and Ankur Taly. 2012. Automated Synthesis of Symbolic Instruction Encodings from I/O Samples. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '12). ACM, New York, NY, USA, 441-452.

Digital Library

[11]

E. Mark Gold. 1967. Language identification in the limit. Information and Control 10, 5 (1967), 447-474.

[12]

Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2011. Synthesis of Loop-free Programs. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11). ACM, New York, NY, USA, 62-73.

Digital Library

[13]

Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken. 2016. Stratified Synthesis: Automatically Learning the x86-64 Instruction Set. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '16). ACM, New York, NY, USA, 237-250.

Digital Library

[14]

Kry¿tof Hoder, Nikolaj Bjørner, and Leonardo de Moura. 2011. μZ- An Efficient Engine for Fixed Points with Constraints. Springer Berlin Heidelberg, Berlin, Heidelberg, 457-462.

[15]

Rajeev Joshi, Greg Nelson, and Keith Randall. 2002. Denali: A Goal-directed Superoptimizer. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI '02). ACM, New York, NY, USA, 304-314.

Digital Library

[16]

Donald E. Knuth. 2005. The Art of Computer Programming, Volume 4, Fascicle 3: Generating All Combinations and Partitions. Addison-Wesley Professional.

Digital Library

[17]

David Ryan Koes and Seth Copen Goldstein. 2008. Near-optimal instruction selection on DAGs. In Sixth International Symposium on Code Generation and Optimization (CGO 2008), April 5-9, 2008, Boston, MA, USA, Mary Lou Soffa and Evelyn Duesterwald (Eds.). ACM, 45-54.

Digital Library

[18]

Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA. IEEE Computer Society, 75s88.

Digital Library

[19]

libFirm Website 2017. Firm s Optimization and Machine Code Generation. (2017). http://libfirm.org

[20]

LLVM Website 2017. The LLVM Compiler Infrastructure Project. (2017). http://llvm.org

[21]

Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably Correct Peephole Optimizations with Alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '15). ACM, New York, NY, USA, 22-32.

Digital Library

[22]

Henry Massalin. 1987. Superoptimizer: A Look at the Smallest Program. In Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems (ASPLOS II). IEEE Computer Society Press, Los Alamitos, CA, USA, 122-126.

Digital Library

[23]

Michael Paleczny, Christopher A. Vick, and Cliff Click. 2001. The Java HotSpot Server Compiler. In Proceedings of the 1st Java Virtual Machine Research and Technology Symposium, April 23-24, 2001, Monterey, CA, USA, Saul Wold (Ed.). USENIX. http://www.usenix.org/publications/library/proceedings/jvm01/paleczny.html

Digital Library

[24]

Philipp Rümmer and Thomas Wahl. 2010. An SMT-LIB Theory of Binary Floating-Point Arithmetic. In Informal proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, Edinburgh, Scotland.

[25]

Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic Superoptimization. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '13). ACM, New York, NY, USA, 305-316.

Digital Library

[26]

Ehud Y. Shapiro. 1983. Algorithmic Program Debugging. MIT Press, Cambridge, MA, USA.

Digital Library

[27]

Carsten Sinz, Stephan Falke, and Florian Merz. 2010. A Precise Memory Model for Low-level Bounded Model Checking. In Proceedings of the 5th International Conference on Systems Software Verification (SSV'10). USENIX Association, Berkeley, CA, USA, 1-9.

Digital Library

[28]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XII). ACM, New York, NY, USA, 404-415.

Digital Library

[29]

Venkatesh Srinivasan and Thomas Reps. 2015. Synthesis of Machine Code from Semantics. SIGPLAN Not. 50, 6 (June 2015), 596-607.

Digital Library

[30]

Venkatesh Srinivasan, Tushar Sharma, and Thomas Reps. 2016. Speeding Up Machine-code Synthesis. SIGPLAN Not. 51, 10 (Oct. 2016), 165-180.

Digital Library

[31]

SyGuS-COMP 2017. SyGuS-COMP 2017. (2017). http://www.sygus.org/SyGuS-COMP2017.html

[32]

Henry S. Warren Jr. 2012. Hacker's Delight (2nd ed.). Addison-Wesley Professional.

Digital Library

Cited By

Li YYang QCi YTian EDe V(2024)SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program ExecutionProceedings of the 61st ACM/IEEE Design Automation Conference10.1145/3649329.3655958(1-6)Online publication date: 23-Jun-2024
https://dl.acm.org/doi/10.1145/3649329.3655958
Zhou HHan QShi HZhang YYao JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Boost Linear Algebra Computation Performance via Efficient VNNI UtilizationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651333(149-163)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651333
Kothari ANoor AXu MUddin HBaronia DBaziotis SAdve VMendis CSengupta STsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware ArchitecturesProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640385(514-529)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640385
Show More Cited By

Index Terms

Synthesizing an instruction selection rule library from semantic specifications
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Retargetable compilers

Recommendations

Vector instruction selection for digital signal processors using program synthesis
ASPLOS '22: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems

Instruction selection, whereby input code represented in an intermediate representation is translated into executable instructions from the target platform, is often the most target-dependent component in optimizing compilers. Current approaches include ...
Generalized instruction selection using SSA-graphs
LCTES '08: Proceedings of the 2008 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems

Instruction selection is a well-studied compiler phase that translates the compiler's intermediate representation of programs to a sequence of target-dependent machine instructions optimizing for various compiler objectives (e.g. speed and space). Most ...
A Study on Instruction-set Selection Using Multi-application Based Application Specific Instruction-set Processors
VLSID '13: Proceedings of the 2013 26th International Conference on VLSI Design and 2013 12th International Conference on Embedded Systems

Efficiency in embedded systems is paramount to achieve high performance while consuming less area and power. Processors in embedded systems have to be designed carefully to achieve such design constraints. Application Specific Instruction set Processors ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CGO '18: Proceedings of the 2018 International Symposium on Code Generation and Optimization

February 2018

377 pages

ISBN:9781450356176

DOI:10.1145/3179541

General Chairs:
Jens Knoop
Vienna University of Technology, Austria
,
Markus Schordan
Lawrence Livermore National Laboratory, USA
,
Program Chairs:
Teresa Johnson
Google, USA
,
Michael O'Boyle
University of Edinburgh, UK

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication Notes

Badge change: Article originally badged under Version 1.0 guidelines https://www.acm.org/publications/policies/artifact-review-badging

Publication History

Published: 24 February 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Deutsche Forschungsgemeinschaft

Conference

CGO '18

Sponsor:

CGO '18: 16th Annual IEEE/ACM International Symposium on Code Generation and Optimization

February 24 - 28, 2018

Vienna, Austria

Acceptance Rates

Overall Acceptance Rate 312 of 1,061 submissions, 29%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
302
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)7

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li YYang QCi YTian EDe V(2024)SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program ExecutionProceedings of the 61st ACM/IEEE Design Automation Conference10.1145/3649329.3655958(1-6)Online publication date: 23-Jun-2024
https://dl.acm.org/doi/10.1145/3649329.3655958
Zhou HHan QShi HZhang YYao JTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Boost Linear Algebra Computation Performance via Efficient VNNI UtilizationProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651333(149-163)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651333
Kothari ANoor AXu MUddin HBaronia DBaziotis SAdve VMendis CSengupta STsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware ArchitecturesProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640385(514-529)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640385
VanHattum APardeshi MFallin CSampson ABrown FTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Lightweight, Modular Verification for WebAssembly-to-Native Instruction SelectionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624862(231-248)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3617232.3624862
Root AAhmad MSharlet DAdams AKamil SRagan-Kelley JAamodt TSwift MJerger N(2023)Fast Instruction Selection for Fast Digital Signal ProcessingProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 410.1145/3623278.3624768(125-137)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3623278.3624768
Pal ASaiki BTjoa RRichey CZhu AFlatt OWillsey MTatlock ZNandi C(2023)Equality Saturation Theory Exploration à la CarteProceedings of the ACM on Programming Languages10.1145/36228347:OOPSLA2(1034-1062)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622834
Liou JAwan MHofmeyr SForrest SWu C(2022)Understanding the Power of Evolutionary Computation for GPU Code Optimization2022 IEEE International Symposium on Workload Characterization (IISWC)10.1109/IISWC55918.2022.00025(185-198)Online publication date: Nov-2022
https://doi.org/10.1109/IISWC55918.2022.00025
Cavalcante TBessa ILima Filho ECordeiro L(2022)Formal synthesis of non-fragile state-feedback digital controllers considering performance requirements for step responseScientific Reports10.1038/s41598-022-19284-412:1Online publication date: 14-Sep-2022
https://doi.org/10.1038/s41598-022-19284-4
Nandi CWillsey MZhu AWang YSaiki BAnderson ASchulz AGrossman DTatlock Z(2021)Rewrite rule inference using equality saturationProceedings of the ACM on Programming Languages10.1145/34854965:OOPSLA(1-28)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485496
Chen YMendis CCarbin MAmarasinghe SSherwood TBerger EKozyrakis C(2021)VeGen: a vectorizer generator for SIMD and beyondProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446692(902-914)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446692
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents