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

From FSL
Revision as of 22:27, 5 April 2019 by Dpark69 (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu
PLDI'19, ACM, pp 1133-1148. 2019
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.
PDF, Slides(PDF), Semantics, DOI, PLDI'19, BIB

Personal tools
Namespaces

Variants
Actions
Navigation