TY  - THES
T1  - Formal specification of the x86 instruction set architecture
A1  - Degenbaev,Ulan
Y1  - 2012/03/09
N2  - In this thesis we specify the x86 instruction set architecture (ISA) by developing an abstract machine that models the behaviour of a modern computer with multiple x86 processors. Our model enables reasoning about low-level system software by providing formal interpretation of thousand pages of the processor vendor documentation written in informal prose. We show how to reduce the problem of ISA formalization to two simpler problems: memory model specification and instruction semantics specification. We solve the former problem by extending the classical Total Store Ordering memory model with caches, translation-lookaside buffers, memory fences, locks, and other features of the x86 processor. For the latter problem we design a new domain-specific language which makes instruction semantics specification readable and compact.

KW  - AMD x86-64
KW  - Prozessor
KW  - Formalisierung
KW  - Programmiersprache
KW  - Speicher <Informatik>
KW  - Cache-Speicher
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2012/4707
ER  -