@inproceedings{be899ed5968a4142bcfa4a97f965817e,
title = "A complete formal semantics of x86-64 user-level instruction set architecture",
abstract = "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.",
keywords = "Formal Semantics, ISA specification, X86-64",
author = "Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Adve, \{Vikram S.\} and Grigore Ro{\c s}u",
note = "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.; 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 ; Conference date: 22-06-2019 Through 26-06-2019",
year = "2019",
month = jun,
day = "8",
doi = "10.1145/3314221.3314601",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "1133--1148",
editor = "McKinley, \{Kathryn S.\} and Kathleen Fisher",
booktitle = "PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation",
address = "United States",
}