A complete formal semantics of x86-64 user-level instruction set architecture
| Autor: | Grigore Rosu, Daejun Park, Sandeep Dasgupta, Vikram Adve, Theodoros Kasampalis |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Programming language
Computer science Formal semantics (linguistics) 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.file_format Mnemonic computer.software_genre 01 natural sciences Instruction set Test case 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Test suite x86 Executable Hardware_CONTROLSTRUCTURESANDMICROPROGRAMMING computer |
| Zdroj: | PLDI |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|