A complete formal semantics of x86-64 user-level instruction set architecture
A complete formal semantics of x86-64 user-level instruction set architecture
复制标题
x86-64用户级指令集架构的完整形式语义
DOI：
10.1145/3314221.3314601
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Grigore Roşu
中科院分区：
文献类型：
--
作者：
Sandeep Dasgupta;D. Park;T. Kasampalis;Vikram S. Adve;Grigore Roşu
迄今为止，我们介绍了X86-64的最完整和经过彻底测试的正式语义。我们的语义忠实地正式化了X86-64 Haswell指令集体系结构的所有未剥夺的，连续的用户级指令。这将总计3155个指令变体，对应于774 mnemonics。语义是完全可执行的，并且已经针对7,000多个指令级测试用例和GCC酷刑测试套件进行了测试。这种广泛的测试获得了回报，揭示了X86-64参考手册和其他现有语义的错误。我们还说明了语义在不同的正式分析中的潜在应用，并讨论了它如何对处理器验证有用。
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.
影响因子：
1.8
作者：
Armstrong, Alasdair;Bauereiss, Thomas;Sewell, Peter
通讯作者：
Sewell, Peter