*************************************************
 **       The Algebraic Specification of          **
 ** Multi-core and Multi-threaded Microprocessors **
  *************************************************

-Sean Handley, Swansea University, UK (2006-2007)

[Head]
- Abstract
- Signed Declarations
- Contents

[Body]
- Analysis
  - Modern Microprocessors
    - Architecture Principles and Wisdom
      - Make the common case fast
      - Principle of locality
      - Instruction level parallelism
    - Latency and Throughput
      - Amdahl's Law
      - The CPU Performance Equation
    - RISC
    - Superscalar
    - Pipelining
    - Parallelism
    - Multi-core & Multi-threading
  - Algebraic Specification
    - Formal Concepts
      - Algebras
      - Sorts and Axioms
    - Maude
      - Common uses
        - Specifying number systems, protocols,
          software, hardware
      - Principle of Reduction
      - Program Correctness
-Design  
  - How to use Maude to model a microprocessor
    - The binary number system
      - The hexadecimal system
    - Memory and registers
    - Machine words, half-words, bytes, double-words
      instruction formats
    - Modelling progress with streams and an iterated
      map
    - Instruction sets
    - Pipelining
      - Pipeline stages
      - Predictive branching and hazards
    - Superscalar
    - Multicore
    - Multi-threading
    - Writing example programs using this system
  - How to convert Maude output into a more intuitive
    format
    - Parsing Maude output in Java
    - Producing basic animated illustration of execution
-Implementation
  - Programmer's Model of a CPU
  - Pipelined Model
  - Multi-core Model
  - Superscalar Model
  - Multi-threaded Model
  - Example Programs
  - Parsed Output
  - Animated Output
- Thoughts and Conclusions
- Evaluation

[Tail]
- Bibliography
- Appendix A - Case Studies
  - The MIPS processor
  - The Intel Core Duo
  - Hyperthreaded Pentium 4
- Appendix B - Source Code