A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
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.
Wed 26 Jun
|10:00 - 10:20|
|10:20 - 10:40|
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram AdveUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-ChampaignLink to publication DOI Pre-print Media Attached
|10:40 - 11:00|
Li ZhouDepartment of Computer Science and Technology, Tsinghua University, Nengkun YuUniversity of Technology Sydney, Australia, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.Media Attached