A complete formal semantics of x86-64 user-level instruction set architecture

Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram Sadanand Adve, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsKathryn S. McKinley, Kathleen Fisher
PublisherAssociation for Computing Machinery
Pages1133-1148
Number of pages16
ISBN (Electronic)9781450367127
DOIs
StatePublished - Jun 8 2019
Event40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States
Duration: Jun 22 2019Jun 26 2019

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
CountryUnited States
CityPhoenix
Period6/22/196/26/19

Fingerprint

Semantics
Testing

Keywords

  • Formal Semantics
  • ISA specification
  • X86-64

ASJC Scopus subject areas

  • Software

Cite this

Dasgupta, S., Park, D., Kasampalis, T., Adve, V. S., & Rosu, G. (2019). A complete formal semantics of x86-64 user-level instruction set architecture. In K. S. McKinley, & K. Fisher (Eds.), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 1133-1148). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3314221.3314601

A complete formal semantics of x86-64 user-level instruction set architecture. / Dasgupta, Sandeep; Park, Daejun; Kasampalis, Theodoros; Adve, Vikram Sadanand; Rosu, Grigore.

PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ed. / Kathryn S. McKinley; Kathleen Fisher. Association for Computing Machinery, 2019. p. 1133-1148 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Dasgupta, S, Park, D, Kasampalis, T, Adve, VS & Rosu, G 2019, A complete formal semantics of x86-64 user-level instruction set architecture. in KS McKinley & K Fisher (eds), PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery, pp. 1133-1148, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, United States, 6/22/19. https://doi.org/10.1145/3314221.3314601
Dasgupta S, Park D, Kasampalis T, Adve VS, Rosu G. A complete formal semantics of x86-64 user-level instruction set architecture. In McKinley KS, Fisher K, editors, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery. 2019. p. 1133-1148. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/3314221.3314601
Dasgupta, Sandeep ; Park, Daejun ; Kasampalis, Theodoros ; Adve, Vikram Sadanand ; Rosu, Grigore. / A complete formal semantics of x86-64 user-level instruction set architecture. PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. editor / Kathryn S. McKinley ; Kathleen Fisher. Association for Computing Machinery, 2019. pp. 1133-1148 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).
@inproceedings{be899ed5968a4142bcfa4a97f965817e,
title = "A complete formal semantics of x86-64 user-level instruction set architecture",
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.",
keywords = "Formal Semantics, ISA specification, X86-64",
author = "Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Adve, {Vikram Sadanand} and Grigore Rosu",
year = "2019",
month = "6",
day = "8",
doi = "10.1145/3314221.3314601",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "1133--1148",
editor = "McKinley, {Kathryn S.} and Kathleen Fisher",
booktitle = "PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation",

}

TY - GEN

T1 - A complete formal semantics of x86-64 user-level instruction set architecture

AU - Dasgupta, Sandeep

AU - Park, Daejun

AU - Kasampalis, Theodoros

AU - Adve, Vikram Sadanand

AU - Rosu, Grigore

PY - 2019/6/8

Y1 - 2019/6/8

N2 - 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.

AB - 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.

KW - Formal Semantics

KW - ISA specification

KW - X86-64

UR - http://www.scopus.com/inward/record.url?scp=85067669165&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85067669165&partnerID=8YFLogxK

U2 - 10.1145/3314221.3314601

DO - 10.1145/3314221.3314601

M3 - Conference contribution

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 1133

EP - 1148

BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - McKinley, Kathryn S.

A2 - Fisher, Kathleen

PB - Association for Computing Machinery

ER -