A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

DRANK

From FSLA Complete Formal Semantics of x86-64 User-Level Instruction Set ArchitectureSandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu PLDI'19, ACM. 2019. To appearAbstract. 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.PDF, Semantics, PLDI'19, BIB