@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 = "Publisher Copyright: {\textcopyright} 2019 Association for Computing Machinery. All rights reserved.; 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",
}