11.1 Purpose of This Chapter

This chapter defines the architectural invariants of EmulatR.

An architectural invariant is a rule that:

Must always hold true

Is independent of implementation details

Cannot be violated by optimization

Defines correctness, not performance

If an invariant is violated, the emulator is architecturally incorrect, even if it appears to work.

These invariants apply across:

Single-CPU and SMP systems

PAL and non-PAL execution

All pipeline stages

All device and MMIO interactions

11.2 Execution and Pipeline Invariants

11.2.1 Precise Execution

All exceptions are precise

When an exception is delivered:

All prior instructions have completed

No later instruction has modified architectural state

No instruction partially commits

There are no imprecise exceptions in EmulatR.

11.2.2 Single Commit Point

Architectural state commits only in Writeback

No instruction updates architectural state earlier

Speculative results are never visible

This applies to:

Registers

Condition codes

Memory visibility

11.2.3 EX Stage Authority

All instruction semantics execute in EX stage

Memory operations occur in EX via MBox

Other pipeline stages perform bookkeeping only

No architectural work occurs outside EX.

11.2.4 No Speculation Across Serialization Points

No speculative instruction may execute past:

WMB

EXCB

TRAPB

CALL_PAL

HW_REI

Serialization points are absolute.

11.3 Memory Model Invariants

11.3.1 Weak Ordering by Default

Memory is weakly ordered

Loads and stores may reorder

Stores may be deferred

Visibility is not guaranteed without barriers

No implicit ordering exists.

11.3.2 Explicit Ordering Only

Ordering is enforced only by:

MB / WMB

EXCB / TRAPB

PAL entry / exit

Certain MMIO semantics

Any code relying on implicit ordering is incorrect.

11.3.3 MMIO Strong Ordering

MMIO accesses are strongly ordered

MMIO accesses are synchronous

MMIO accesses are never buffered

MMIO accesses are never speculative

MMIO correctness overrides performance.

11.4 Load-Locked / Store-Conditional (LL/SC) Invariants

11.4.1 Reservation Model

LL/SC uses reservations, not locks

Reservations are:

Per-CPU

Cache-line granular

Optimistic

Non-blocking

No mutex semantics exist.

11.4.2 Reservation Lifetime

A CPU may hold at most one reservation

Reservations are cleared on:

Any store to the cache line

Any store by the same CPU

MB / EXCB where required

PAL entry or exit

Exception or interrupt delivery

Context switch

Reservations never survive privilege boundaries.

11.4.3 Store-Conditional Semantics

ST*_C must:

Succeed only if reservation is valid

Fail otherwise

Clear reservation regardless of outcome

No retries are implicit.

11.5 Privilege and PAL Invariants

11.5.1 Absolute Privileged Boundary

Execution is either PAL or non-PAL

There is no intermediate privilege state

Privilege cannot be escalated incrementally

11.5.2 Single Entry / Single Exit

CALL_PAL is the only entry into PAL

HW_REI is the only exit from PAL

Any other path is illegal and must fault.

11.5.3 Complete State Restoration

PAL entry captures full architectural state

HW_REI restores full architectural state

No partial restoration is permitted

No PAL state leaks into non-PAL execution

11.6 Exception and Interrupt Invariants

11.6.1 Classification

Faults are synchronous

Traps are synchronous but post-commit

Interrupts are asynchronous

Each follows distinct delivery rules.

11.6.2 Priority and Isolation

Only one exception or interrupt is delivered at a time

Exceptions are prioritized deterministically

Interrupts are maskable and deferrable

Faults affect only the current CPU

11.6.3 PAL-Mediated Delivery

All exceptions and interrupts enter PAL

No exception bypasses PAL

PAL is the sole authority for dispatch

11.7 SMP Invariants

11.7.1 True Symmetry

All CPUs are peers

No CPU has implicit authority

No global CPU lock exists

11.7.2 Per-CPU Independence

Each CPU has independent:

Pipeline

Registers

TLBs

Write buffers

Reservations

PAL state

No CPU directly mutates another CPU’s private state.

11.7.3 Shared Memory, Explicit Coordination

GuestMemory is shared

Visibility is not immediate

Coordination occurs only through:

Barriers

IPIs

PAL operations

11.8 Device and MMIO Invariants

11.8.1 Asynchronous Devices

Devices operate asynchronously

CPU never blocks on device execution

Completion is interrupt-driven or polled

11.8.2 Synchronous MMIO

MMIO access is synchronous

Side effects occur immediately

MMIO is strongly ordered

11.8.3 DMA Rules

DMA operates on GuestMemory

DMA obeys access permissions

DMA completion does not imply ordering without barriers

11.9 Debugging and Observability Invariants

11.9.1 Determinism

Given the same inputs, execution is deterministic

SMP ordering differences are intentional and observable

No hidden timing dependencies exist

11.9.2 Traceability

Every architectural event is traceable:

Exceptions

Interrupts

Barriers

PAL transitions

Reservation changes

MMIO accesses

If it cannot be traced, it cannot be trusted.

11.10 Invariant Violations

Any violation of an architectural invariant indicates:

A design bug, or

An implementation defect

Performance, convenience, or simplicity never justify violating an invariant.

11.11 Summary

Architectural invariants define what EmulatR is.

Key guarantees:

Precise execution

Explicit ordering

Absolute privilege separation

Deterministic SMP behavior

Correct atomic semantics

Strong MMIO correctness

PAL-mediated control

Full observability

These invariants are the foundation on which all future features must stand.

Where This Chapter Fits

This chapter should be treated as:

A correctness checklist

A validation guide

A regression test oracle

A contributor contract

Chapter 11 - Architectural Invariants