A Pipelined Multi-Core Machine with Operating System Support: Hardware Implementation and Correctness Proof (Lecture Notes in Computer Science, 9999)

Preface
Contents
1 Introductory Material
	1.1 So What?
		1.1.1 The Element of Chance in Multi-Core Programming
		1.1.2 Standards and Verification in Classical Architecture versus SystemArchitecture
	1.2 Overview
	1.3 Basics
		1.3.1 Sets, Cross Products and Sequences
		1.3.2 Boolean Operators
		1.3.3 Binary and Two’s Complement Numbers
		1.3.4 Memory
2 On Hierarchical Hardware Design
	2.1 Syntax
		2.1.1 Buses
		2.1.2 I/O Buses
		2.1.3 Basic Hardware Units
		2.1.4 Subunit Declarations
		2.1.5 Composite Hardware Units
		2.1.6 Implicit Labels and Types in Hardware Schematics
		2.1.7 Size Parameters
		2.1.8 Recursive Constructions
		2.1.9 Global Naming
		2.1.10 Paths, Cycles and Depth
	2.2 Semantics
		2.2.1 Values of Input Signals
		2.2.2 Configurations
		2.2.3 Hardware Computations
		2.2.4 Circuit Evaluation
		2.2.5 Values of Buses and Outputs of Units
		2.2.6 Updating Configurations
		2.2.7 Streamlining Notation
	2.3 Modular Reasoning
		2.3.1 Tracking Paths
		2.3.2 Evaluating Circuits
		2.3.3 The Easy Common Case
		2.3.4 Cycles of Buses Between Units
		2.3.5 Updating Configurations
	2.4 Expressions and Assignments as Syntactic Sugar
		2.4.1 Syntax
		2.4.2 Implementation
		2.4.3 Semantics
3 Hardware Library
	3.1 Circuit Library
		3.1.1 Basic Circuits
		3.1.2 Arithmetic Circuits
		3.1.3 Branch Condition Evaluation Unit
	3.2 Control Automata
	3.3 Random Access Memory (RAM)
		3.3.1 Basic Design
		3.3.2 Read Only Memory (ROM)
		3.3.3 R-W-RAM
		3.3.4 R-RW-RAM
		3.3.5 Two port ROM
		3.3.6 bw-R-RW-RAM
		3.3.7 bw-R-RW-RAM-ROM
		3.3.8 GPR-RAM
		3.3.9 SPR-RAM
		3.3.10 R-RW-SPR RAM
	3.4 Register Control
		3.4.1 Set-Clear Flip-Flop
		3.4.2 Stabilizer Latch
	3.5 Control of Tri-State Buses
		3.5.1 Justifying the Operating Conditions
		3.5.2 Controlling Tri-State Buses
		3.5.3 Arbitration
		3.5.4 Combined Arbiter and Tri-State Bus
	3.6 Exercises
4 Basic Processor Design
	4.1 MIPS ISA
		4.1.1 Instruction Tables
		4.1.2 Configuration and Instruction Fields
		4.1.3 Instruction Decoding
		4.1.4 Reading out Data from Register Files
		4.1.5 Moves
		4.1.6 ALU-operations
		4.1.7 Shift Unit Operations
		4.1.8 Branch and Jump
		4.1.9 Memory Operations
		4.1.10 ISA Summary
		4.1.11 Software Conditions
	4.2 A Sequential Processor Design
		4.2.1 Hardware Configurations and Simulation Relation
		4.2.2 Memory Embedding
		4.2.3 Overview of the Hardware
		4.2.4 Initialization and Instruction Fetch
		4.2.5 Straight Forward Constructions
		4.2.6 Data Accesses
		4.2.7 Absence of Cycles
	4.3 Repackaging the Induction Step
		4.3.1 Numbers and Correctness of Circuit Stages
		4.3.2 Use of Signals for Instruction Execution
5 Pipelining
	5.1 General Concepts
		5.1.1 ISA, Circuit Stages and Software Conditions
		5.1.2 Cost Effectiveness of Pipelining
		5.1.3 Notation
	5.2 Basic Pipelined Processor
		5.2.1 Pipeline Registers
		5.2.3 Scheduling Functions
		5.2.4 Delayed PC
		5.2.5 Correctness Statement and Additional Software Condition
		5.2.6 Intuition
		5.2.7 Software Conditions
		5.2.8 Correctness Proof
	5.3 Forwarding
		5.3.1 Forwarding Circuits
		5.3.2 Correctness
	5.4 Stalling
		5.4.1 Stall Engine with Hazard Signals
		5.4.2 Correctness and Liveness
		5.4.3 Proof Summary
	5.5 Final Remark: Getting Rid of Software Conditions
6 Cache Memory Systems
	6.1 Reviewing A Concrete Example
		6.1.1 Construction
		6.1.2 Memory Abstraction
	6.2 Specification
		6.2.1 Signals of the Processor Interface
		6.2.2 Protocol
		6.2.3 Operating Conditions for the CMS
		6.2.4 External Access Sequence
		6.2.5 Sequential Consistency
		6.2.6 Ordering External Accesses by their End Cycle
		6.2.7 Liveness
	6.3 Using a Cache Memory System in a Single Pipeline
		6.3.1 Connecting Interfaces
		6.3.2 Stability of Inputs of Accesses
		6.3.3 Relating Update Enable Signals and Ends of Accesses
		6.3.4 Software Conditions and Main Induction Hypothesis
		6.3.5 External Accesses to the Data Cache Ending in the Current Cycle
		6.3.6 Induction Step
		6.3.7 Proof Summary
	6.4 Exercises
	6.5 Errata
7 Interrupt Mechanism
	7.1 Specification
		7.1.1 Special Purpose Registers Revisited
		7.1.2 Types of Interrupts
		7.1.3 MIPS ISA with Interrupts
		7.1.4 Specification of Most Internal Interrupt Event Signals
		7.1.5 Instruction and Data Accesses Revisited
	7.2 Sequential Implementation
		7.2.1 PC Environment
		7.2.2 Cause Processing Environment
		7.2.3 Accesses and Write Signals
		7.2.4 Special Purpose Register File
		7.2.5 Software Conditions and Correctness
	7.3 Pipelining a Processor With Interrupts
	7.4 Stalling, Rollback and Pipe Drain
		7.4.1 Stall Engine and Scheduling Functions with Rollbacks and Stabilized Full Bits
		7.4.2 Properties of the New Stall Engine
		7.4.3 Liveness and Correctness in the Presence of Rollback
		7.4.4 Pipelining Signals
		7.4.5 Sampling the External Interrupt Signal
	7.5 Pipelining and Forwarding
		7.5.1 Data Paths
		7.5.2 Forwarding Data
		7.5.3 Connecting the new Rollback Engine
		7.5.4 Program Counter Environment
		7.5.5 Write and Clock Enable Signals
		7.5.6 Connecting the Cache Memory System
		7.5.7 Stability of the Instruction Memory Address
	7.6 Stating Processor Correctness
		7.6.1 Software Condition for Self Modifying Code
		7.6.2 A New Induction Hypothesis
	7.7 Properties of Liveness
		7.7.1 Properties needed for Correctness
		7.7.2 Towards the Liveness Proof
	7.8 Proving Processor Correctness
		7.8.1 Induction Scheme
		7.8.2 Induction Step of the Inner Induction
		7.8.3 Correctness of Memory Update
		7.8.4 Pipeline Correctness with Rollback Request
		7.8.5 Pipeline Correctness without Rollback Request
	7.9 Completing the Liveness Proof
	7.10 Proof Summary
	7.11 Exercises
8 Self Modification, Instruction Buffer and Nondeterministic ISA
	8.1 ISA
		8.1.1 Nondeterminism, Oracle Inputs and Stepping Functions
		8.1.2 Guard Conditions and Software Conditions
		8.1.3 Configurations, Instruction Buffer and Guard Conditions
		8.1.4 Instruction Execution
	8.2 Hardware correctness
		8.2.1 Inputs for Processor Steps
		8.2.2 Stepping Function
		8.2.3 Software Condition and Stating Processor Correctness
		8.2.4 Properties of pseq
		8.2.5 Induction Step
		8.2.6 Correctness of Memory Update
		8.2.7 Pipeline Correctness
	8.3 Liveness and Guard condition
	8.4 A Simple Instruction Buffer Reduction Theorem
	8.5 Summary
		8.5.1 ISA
		8.5.2 Specifying Processor Correctness
		8.5.3 Correctness Proof
	8.6 Exercises
9 Memory Management Units
	9.1 Walks and ISA MMU
		9.1.1 Page Tables
		9.1.2 Walks
		9.1.3 TLBs
		9.1.4 Translation Requests
	9.2 ISA
		9.2.1 Configuration
		9.2.2 TLB Steps
		9.2.3 Instruction Buffer Steps
		9.2.4 Processor Steps
	9.3 MMU Construction
		9.3.1 TLB
		9.3.2 Walking Unit and MMU
		9.3.3 Correctness
	9.4 Pipelined Processor with MMUs
		9.4.1 Instruction Address
		9.4.2 Connecting MMUs to the Pipeline
		9.4.3 Caches
		9.4.4 Forwarding
		9.4.5 PC Environment
		9.4.6 Interrupts and Cause Pipe
		9.4.7 Stall Engine
	9.5 Correctness
		9.5.1 Stability of Inputs of Accesses
		9.5.2 Sequential Order and Local Sequential Index of CMS steps
		9.5.3 Relating Update Enable Signals and Ends of Accesses
		9.5.4 Inputs for Processor Steps
		9.5.5 Stepping Function
		9.5.6 Induction Hypothesis
		9.5.7 Correctness for Components Outside the Pipeline
		9.5.8 Correctness for Pipeline Registers
		9.5.9 Proof Summary
10 Store Buffers
	10.1 Specification of Store Buffers
	10.2 Extending ISA
		10.2.1 Processor Steps
		10.2.2 Store Buffer Steps
		10.2.3 Instruction Buffer and MMU Steps
	10.3 Store Buffer Construction
		10.3.1 Basic Queue with Forwarding
		10.3.2 Improved Queue Design
	10.4 Pipelined Processor with Store Buffer
		10.4.1 Draining Instructions
		10.4.2 Arbitration and Control
		10.4.3 Connecting the Data Paths
		10.4.4 Computing the Busy Signal
		10.4.5 Stability of Inputs
	10.5 Correctness
		10.5.1 Definition of Stepping Function
		10.5.2 Simulation Relation
		10.5.3 Managing the Induction Step
		10.5.4 Induction Step
		10.5.5 Preparations
		10.5.6 Correctness for Components Outside the Pipeline
		10.5.7 Correctness for Pipeline Registers
		10.5.8 Proof Summary
	10.6 A Simple Store Buffer Reduction Theorem
	10.7 Exercises
11 Multi-Core Processors
	11.1 Defining Basic Multi-Core ISA
	11.2 Local ISA Configurations and Computations
	11.3 Hardware
		11.3.1 Connecting Processors to the Cache Memory System
	11.4 Correctness
		11.4.1 Straight Forward Generalizations of Arguments for Single CoreProcessors
		11.4.2 Liveness and Committed
		11.4.3 Sampling Signals from Outside the Pipeline
		11.4.4 Ordering Instructions by the Cycle they Pass The Memory Stage
		11.4.5 Software Conditions and Correctness Statement
		11.4.6 Induction Step
		11.4.7 Numbering Accesses to Data Ports
	11.5 Instruction Buffer Reduction
	11.6 Exercises
12 Advanced Programmable Interrupt Controllers (APICs)
	12.1 Specification
		12.1.1 Processor Steps
		12.1.2 Store Buffer Steps
		12.1.3 MMU and Instruction Buffer Steps
		12.1.4 SIPI Steps
		12.1.5 IPI Delivery Steps
		12.1.6 Initial Configuration
	12.2 Construction
		12.2.1 Interrupt Bus
		12.2.2 Interface of Local APIC
		12.2.3 Construction of Local APIC
		12.2.4 Placing the APICs on the Interrupt Bus
		12.2.5 Cause Pipe and Stalling
		12.2.6 Memory Operations to the APIC
	12.3 Correctness
		12.3.1 Stepping Function
		12.3.2 Software Conditions
		12.3.3 Induction Hypothesis
		12.3.4 Scheduling Diagram for APIC
		12.3.5 Induction Step
		12.3.6 Correctness of Store Buffers
		12.3.7 Validity
		12.3.8 Correctness of ICR
		12.3.9 Correctness of IRR
		12.3.10 Correctness of ISR
		12.3.11 Remaining Registers
		12.3.12 Correctness of Components outside the Pipeline
		12.3.13 Correctness of Pipeline
		12.3.14 Summary
	12.4 Exercises
13 Adding a Disk
	13.1 Hardware Disk as a Basic Unit
	13.2 Connecting the Disk with the Processors
		13.2.1 Operating Conditions of the Device Bus
	13.3 ISA
	13.4 Correctness
		13.4.1 Stepping Function
		13.4.2 Software Condition for Disk
		13.4.3 Induction Hypothesis
		13.4.4 Induction Step
		13.4.5 Validity
		13.4.6 Operating Condition of Disk
		13.4.7 Disk Correctness
		13.4.8 Correctness of Non-Pipelined Components
		13.4.9 Correctness of the Pipeline
	13.5 Exercises
14 I/O APIC
	14.1 Specification of I/O APIC
		14.1.1 I/O APIC Steps
		14.1.2 EOI Mechanism and the Local APIC
	14.2 Construction
		14.2.1 Local APIC Revisited
		14.2.2 I/O APIC
		14.2.3 Connecting Everything
	14.3 Correctness Proof
		14.3.1 Stepping Function
		14.3.2 Software Conditions
		14.3.3 Induction Hypothesis
		14.3.4 Induction Step
		14.3.5 Validity
		14.3.6 Correctness of the EOI Pending Register
		14.3.7 Correctness of the Redirection Register
		14.3.8 Correctness of Non-Pipelined Components
		14.3.9 Correctness of Pipelined Registers
	14.4 Exercises
References