[PDF] assess the role of the international court of justice in protecting human rights
[PDF] assessment in education
[PDF] assessment in education pdf
[PDF] assessment in spanish
[PDF] assessment in the classroom
[PDF] assessment meaning
[PDF] assessment pro
[PDF] assessment strategies
[PDF] assessment synonym
[PDF] assessment test
[PDF] assessment tools
[PDF] asset acquisition accounting entries
[PDF] asset fractionalization
[PDF] asset monetization blockchain
[PDF] asset securitization pdf
Formal Specification of the x86
Instruction Set ArchitectureDissertation
zur Erlangung des Grades
Doktor der Ingenieurswissenschaften (Dr.-Ing.)
Ulan Degenbaev
Saarbrücken, Februar 2012brought to you by COREView metadata, citation and similar papers at core.ac.ukprovided by Scientific documents from the Saarland University,
ii
Tag des Kolloquiums: 6. Februar 2012
Dekan: Prof. Dr. Holger Hermanns
Vorsitzender des Prüfungsausschusses: Prof. Dr. Sebastian Hack
1. Berichterstatter: Prof. Dr. Wolfgang J. Paul
2. Berichterstatter: Dr. habil. Peter-Michael Seidel
Akademischer Mitarbeiter: Dr. Art Tevs
ohne Benutzung anderer als der angegebenen Hilfsmittel angefertigt habe. Die aus anderen Quellen oder indirekt übernommenen Daten und Konzepte sind unter Angabe der Quelle gekennzeichnet. Die Arbeit wurde bisher weder im In- noch im Ausland in
Saarbrücken, im Februar 2012iii
iv
Abstract
In this thesis we formally specify the x86 instruction set architecture (ISA) by develop- ing 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 pro- viding 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: mem- ory 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 pro- cessor. In order to make instruction semantics specification readable and compact, we design a new domain-specific language. The language has intuitive syntax for defining registers and instructions, so that any programmer should be able to understand the specifica- tion. Although our language is external and not embedded into a formal proof system, the language is based on the same principles as embedded, monadic domain-specific languages. Thus, it is possible to translate specifications from our language to formal proof systems.
Zusammenfassung
In dieser Arbeit spezifizieren wir den x86-Befehlssatz durch die Definition einer ab- strakten Maschine, die das Verhalten eines modernen Computers mit mehreren x86- Prozessoren modeliert. Unser Modell bietet eine formale Interpretation der Prozes- sorherstellerdokumentationen, die über Tausend Seiten von informellen Spezifikatio- nen enthalten. Wir zeigen, wie das Problem der Befehlssatz-Formalisierung in zwei einfachere Prob- leme zerlegt werden kann: Spezifikation von dem Speichermodell und Spezifikation von klassischen "Total Store Ordering" Speichermodells mit Caches, Translation-Lookaside
Buffers, Memory Fences und Locks.
Um die Maschinenbefehlsemantikspezifikation lesbar und kompakt zu machen, entwer- Definition von Registern und Maschinenbefehlen, so dass jeder Programmierer in der Lage sein sollte, die Spezifikation zu verstehen. Obwohl unsere Sprache nicht in ein nen aus unserer Sprache in ein formales Beweissystem zu übertragen.v vi
Acknowledgments
I would like to thank my supervisor Professor Wolfgang Paul for the guidance and en- couragement. I owe my graditute to many people in the Verisoft XT group for valuable suggestions, stimulating discussions, and friendly atmosphere. Special thanks to Christian Müller, Ernie Cohen, Eyad Alkassar, Mark A. Hillebrant, and Norbert Schirmer.vii viii
CONTENTS
1 Introduction1
1.1 Motivation
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 The Problem
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Related Work
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.4 Methodology
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.5 Scope of the model
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.6 Outline
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
I Abstract Machine
13
2 Notation15
2.1 Relations
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.2 Functions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Conventions for memory accesses
. . . . . . . . . . . . . . . . . . . . . . 17
3 Model Overview
19
3.1 Instruction execution
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Abstract x86 machine
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
4 Environment27
5 Cache29
5.1 MOESI protocol
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5.2 Memory types
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5.3 Cache model
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6 Store Buffer37
6.1 Forwarding and writing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6.2 Transitions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
7 Load Buffers41
7.1 Loading code
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.2 Loading data
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.3 Flushing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ix
8 Translation-Lookaside Buffer45
8.1 Page Tables
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
8.2 Creating and dropping walks
. . . . . . . . . . . . . . . . . . . . . . . . . 48
8.3 Extending walks
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
8.4 Loading translations into the Core
. . . . . . . . . . . . . . . . . . . . . . 50
8.5 Flushing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
9 Core53
9.1 Core configuration
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
9.2 Overview of transitions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
9.3 Instruction border
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
9.4 RESET, INIT, HALT
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
9.5 Memory accesses
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
9.6 Fetch and decode
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
9.7 Execution
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
9.8 VMEXIT
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
9.9 Serializing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
9.10 Jump to interrupt service routine
. . . . . . . . . . . . . . . . . . . . . . . 72
10 Local APIC77
10.1 Maskable interrupts
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
10.2 INIT, NMI, SIPI
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
10.3 Interprocessor interrupts
. . . . . . . . . . . . . . . . . . . . . . . . . . . 83
10.4 Miscellaneous
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
10.5 Register accesses
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
10.6 IPI Delivery
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
II Inside Processor Core
95
11 DSL Syntax and Semantics
97
11.1 Source Code Structure
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
11.2 Types
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
11.3 Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
11.4 Expressions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
11.5 Functions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
11.6 Actions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
11.7 Instructions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
12 Registers113
12.1 General-Purpose Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . 113
12.2 Control Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
12.3 Segment Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
12.4 Descriptor Table Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . 120
12.5 Task Register
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
12.6 Virtualization Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
12.7 Instruction Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
12.8 Memory Type Registers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
12.9 Fast System Call
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
12.10 APIC Base Address
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 x
12.11 Time-Stamp Counters. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
13 Architecture129
13.1 Operating Modes
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
13.2 Exceptions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
13.3 Address spaces
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
13.4 Memory System Interface
. . . . . . . . . . . . . . . . . . . . . . . . . . . 134
13.5 Reading and Writing the Virtual Memory
. . . . . . . . . . . . . . . . . . 136
13.6 Page Tables
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
13.7 Segment Descriptors
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
13.8 Gate Descriptors
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
13.9 Descriptor Tables
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
13.10 Protection
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
13.11 Privilege Level Change
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
13.12 Segmentation Translation
. . . . . . . . . . . . . . . . . . . . . . . . . . . 152
13.13 Segment Register Access
. . . . . . . . . . . . . . . . . . . . . . . . . . . 154
13.14 Task State Segment
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
14 Instruction Fetch and Decode
161
14.1 Instruction Format
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
14.2 Opcode
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
14.3 Prefixes
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
14.4 ModRM byte
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
14.5 SIB byte
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
14.6 Displacement
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
14.7 Immediate Operand
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
14.8 Opcode Table
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
14.9 Instruction Fetch
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
14.10 Operand Width
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172
14.11 Memory Operand Address Width
. . . . . . . . . . . . . . . . . . . . . . . 173
14.12 Memory Operand Address
. . . . . . . . . . . . . . . . . . . . . . . . . . . 174
14.13 Operand Decode
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
15 Stack and Stack Operations
179
15.1 Inner Stack
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180
16 Far Control Transfer
183
16.1 Far Jump
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
16.2 Far Procedure Call
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
16.3 Control Transfer to an Interrupt Handler
. . . . . . . . . . . . . . . . . . 193
16.4 Far Return
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195
16.5 Task Switch
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198
17 Virtualization199
17.1 Guest State Save Area - VMCB SSA
. . . . . . . . . . . . . . . . . . . . . 200
17.2 Guest Control Area - VMCB CA
. . . . . . . . . . . . . . . . . . . . . . . 203
17.3 Injected Events and Virtual Interrupts
. . . . . . . . . . . . . . . . . . . . 209
17.4 Host State Save Area
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
18 Instructions213xi
19 Conclusion217
19.1 Validating the model
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
III Appendix
219
A Move Instructions
221
B Arithmetic Instructions
227
B.1 Addition
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
B.2 Subtraction
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229
B.3 Comparison
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
B.4 Multiplication
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232
B.5 Division
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
C Logic Instructions
237
D Bit String Instructions
241
D.1 Bit Test and Set
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241
D.2 Bit Search
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
D.3 Bit String Conversions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245
D.4 Shifts
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
D.5 Rotations
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250
E Instructions for Binary Coded Decimals
253
F Flag Instructions
257
G Stack Instructions
261
H Near Control Transfer Instructions
267
I Far Control Transfer Instructions
271
I.1 Fast System Call Instructions
. . . . . . . . . . . . . . . . . . . . . . . . . 271
I.2 Far JMP and CALL instructions
. . . . . . . . . . . . . . . . . . . . . . . . 276
I.3 Software Interrupt Instructions
. . . . . . . . . . . . . . . . . . . . . . . . 278
I.4 Return Instructions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278
J String Instructions
281
K Input/Output Instructions
285
L Segmentation Instructions
289
L.1 Load SR and GPR from Memory
. . . . . . . . . . . . . . . . . . . . . . . 289
L.2 SWAPGS
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290
L.3 Task Register Access
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290
L.4 Descriptor Table Register Access
. . . . . . . . . . . . . . . . . . . . . . . 291
M Protection Instructions
295
N CR and MSR Access Instructions
297
N.1 Control Register Access
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 297 xii N.2 Model Specific Register Access. . . . . . . . . . . . . . . . . . . . . . . . 300
O Memory Management Instructions
303
O.1 TLB Invalidation
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303
O.2 Memory Fences
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304
O.3 Cache Invalidation
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 305
P Virtualization Instructions
307
P.1 Run Guest
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307
P.2 Exit Guest
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311
P.3 Save and Restore Guest Extended State
. . . . . . . . . . . . . . . . . . . 313
P.4 Exit Codes
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315
Q Miscellaneous Instructions
319
R Operand Read and Write
321
S Page Table Entries
325 xiii
xiv
CHAPTER
ONEINTRODUCTION
1.1 Motivation
In the first Quarter of 2011, the x86 processors comprised about99:9%of the personal computer market and66:4%of the server market [Cor11a,Cor11b]. Even though these processors are ubiquitous, there is still no publicly available, rigorous description of how they execute instructions. Official vendor documentation is written in informal prose, that is often ambiguous or inconsistent. A programmer who wishes to write low-level software has to spend a vast amount of time interpreting the huge vendor documents, experimenting with the real hardware, and collecting bits of the low-level programming folklore. After finishing the software, the programmer is left with the only option to ensure software correctness: testing. Two recent technological advances have highlighted the need for formal specification of the processor behaviour. The first is proliferation of multiprocessor computers. It is difficult to write correct concurrent programs when the programmer does not know how exactly the memory accesses from one processor are observed by another proces- sor. Testing cannot catch subtle concurrency bugs which are triggered by a specific interleaving of memory accesses. This interleaving might occur once in every million executions of the program because the highly-optimized processors reorder memory ac- cesses in practically unpredictable way. This means that the programmer has to prove the correctness of a concurrent program for all possible interleavings. Such proofs cannot exists without precise description of how a processor issues and reorders the memory accesses. The second advance is virtualization. Cloud and web hosting providers have embraced this technology because it allows to run several independent operating systems on a single server. Each operating system has an illusion that it fully controls the server, but in reality there is a so-called hypervisor program running on the server and providing a virtual hardware environment for an operating system. Using the processor"s virtualiza- tion capabilities, the hypervisor can choose which instructions of the operating system are to be executed natively by the processor and which instructions are to be emulated by the hypervisor. Having formal specification of the instructions would help to prove1 that the hypervisor emulates them correctly. Even more important concern is security of the hypervisor. Since an operating system is free to run any code, including mali- cious or invalid code, the hypervisor has to ensure that such code can never escape the virtual environment. Malicious code might try to exploit obscure, poorly documented effects of an instruction. The hypervisor has to be programmed to handle such effects. Only with rigorous specification of the instructions, one can hope to prove the absence of loopholes in the hypervisor. We could list a dozen of other reasons for why formal specification of the x86 instruc- tions is a good thing. However, the two arguments above were our main motivation when we started formalizing the instructions as part of the Verisoft XT project on
Microsoft
®Hyper-V™hypervisor verification in 2007. This thesis summarizes our ef- forts and answers the following question: "Is is possible to develop a useful formal specification of the modern x86 instruction set architecture?"
1.2 The Problem
Instruction set architecture (ISA) is an interface between a processor and software. In other words, an ISA is a high-level processor description that provides enough infor- mation for a programmer to write and reason about low-level software. Ideally an ISA would hide as much of processor implementation as possible. Thus, specifying an ISA is a fine art of balancing between being too loose and too strict. A too loose specification makes it impossible for a programmer to prove certain properties of software. A too strict specification precludes performance optimizations in the processor hardware. An
ISA defines
the processor registers and the meaning of each bit in a register; the memory model, i.e. how memory accesses are reordered; interrupts and interrupt handling; the data structures shared between the processor and software, such as descriptor tables, page tables, control blocks, etc. the instruction opcodes and operands; the instruction semantics, i.e. the effects of instruction execution. Processor vendors prefer to specify the x86 architecture in informal prose as it requires considerably less effort than formal specification and it allows them to be vague in certain places in order to leave a room for future hardware optimizations [ Int09 Adv07quotesdbs_dbs8.pdfusesText_14
[PDF] x86 Instruction Encoding