TY - GEN
T1 - A complete formal semantics of x86-64 user-level instruction set architecture
AU - Dasgupta, Sandeep
AU - Park, Daejun
AU - Kasampalis, Theodoros
AU - Adve, Vikram S.
AU - Roşu, Grigore
N1 - Funding Information:
We thank the K team, for their technical support throughout the project, and the Strata developers, for promptly confirming our reported bugs and answering all our questions in great detail. We thank our shepherd, June Andronick, for her diligence and helpful guidance in responding to the reviewers' comments. We are grateful to Alastair Reid and Matthew Fernandez for their invaluable feedback. The work presented in this paper was supported in part by the Office of Naval Research under contract number N00014-17-1-2996, NSF CNS 1619275, and DARPA Sub HRL 17090-181687 US.
Publisher Copyright:
© 2019 Association for Computing Machinery. All rights reserved.
PY - 2019/6/8
Y1 - 2019/6/8
N2 - We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics. We also illustrate potential applications of our semantics in different formal analyses, and discuss how it can be useful for processor verification.
AB - We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics. We also illustrate potential applications of our semantics in different formal analyses, and discuss how it can be useful for processor verification.
KW - Formal Semantics
KW - ISA specification
KW - X86-64
UR - http://www.scopus.com/inward/record.url?scp=85067669165&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85067669165&partnerID=8YFLogxK
U2 - 10.1145/3314221.3314601
DO - 10.1145/3314221.3314601
M3 - Conference contribution
AN - SCOPUS:85067669165
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 1133
EP - 1148
BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - McKinley, Kathryn S.
A2 - Fisher, Kathleen
PB - Association for Computing Machinery
T2 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
Y2 - 22 June 2019 through 26 June 2019
ER -