Architectural envelope model

Definition

An architectural envelope model is a formal specification of a processor architecture that precisely defines the entire range of programmer-observable behaviours allowed by that architecture, for arbitrary code, without committing to any particular microarchitectural implementation choices ^[1][2].

Unlike traditional architecture documentation expressed in prose and pseudocode—which is inevitably ambiguous and lacks a tight connection to testing or verification—an architectural envelope model is mathematically rigorous, executable, and serves as a definitive reference for both hardware and software development ^[3].

Key properties

A well-formed architectural envelope model should possess several desirable properties ^[3][1]:

• Mathematically rigorous, providing a precise formal definition rather than informal prose.
• Readable and clearly structured for human comprehension.
• Sound with respect to vendor intent, capturing what architects intended the architecture to permit.
• Sound with respect to existing implementations, admitting all experimentally observable behaviour (modulo errata).
• Microarchitecturally abstract, avoiding over-commitment to particular pipeline or storage hierarchy details.
• Executable as a test oracle, able to enumerate, check, or explore the allowed behaviour of test cases.

Structure: integration of concurrency and ISA models

The defining characteristic of an architectural envelope model is the integration of a concurrency model with an ISA model ^[3][4]. For a single-threaded processor, instructions can be modelled as atomic updates to a global register and memory state. For a weakly consistent multiprocessor, this naive approach is insufficient because it would not admit all the observable behaviour of real implementations (e.g., out-of-order and speculative execution) ^[5].

The central design question is therefore: what is the interface between the concurrency model and the ISA semantics? The model must permit the full envelope of weakly consistent behaviour—including phenomena such as out-of-order loads, speculative reads, control-dependent loads, and memory reordering—while remaining as abstract as possible with respect to microarchitectural detail ^[2][5].

Components

A typical architectural envelope model, as exemplified by the work on IBM POWER, consists of ^[2][4][3]:

1. ISA model: A formal description of instruction decoding and behaviour, ideally derived from or tightly tied to vendor pseudocode. For POWER, this used a new instruction description language called Sail, with type inference to check pseudocode consistency while keeping instruction descriptions readable. Sail definitions were generated from an XML export of the vendor's Framemaker documentation ^[4].

2. Concurrency model: An operational model specifying the allowed memory and concurrency behaviour, typically expressed in an abstract microarchitectural style (for example, with a storage subsystem maintaining coherence relations as a strict partial order among memory events) ^[4][3].

3. ISA/Concurrency interface: The novel abstract structure that mediates between instruction semantics and the concurrency model, allowing all required concurrency behaviour without over-committing to implementation details ^[3].

Formal specification and execution

Architectural envelope models are typically expressed in a rigorous specification language such as Lem, which provides types and pure functions that serve as both mathematical definitions and executable programs ^[2][4]. Lem can:

• Typecheck definitions and automatically generate executable code (e.g., OCaml).
• Export to proof assistants including Coq, HOL4, and Isabelle/HOL.
• Produce typeset LaTeX output ^[2].

The mathematical definitions are compiled to executable code in a deliberately straightforward fashion without optimization, to maintain confidence that the executable faithfully represents the specification ^[5].

Use as a test oracle

A primary motivation for an architectural envelope model is to serve as a test oracle for hardware and software development ^[3][1]. The executable model allows developers to:

• Interactively explore the allowed behaviour of test cases.
• Exhaustively compute the set of all allowed behaviours for small but intricate concurrent test programs.
• Validate that the model is sound by comparing model predictions against experimentally observable hardware behaviour for a range of sequential and concurrent tests ^[2].

Typical inputs include litmus tests (parsed via a dedicated frontend) and ELF binaries (parsed via a formal ELF model frontend) ^[2].

Application to weakly consistent architectures

Architectural envelope models are especially valuable for weakly consistent multiprocessors such as ARM and IBM POWER, whose subtle programmer-visible concurrency behaviour arises from microarchitectural optimisations like out-of-order execution, speculation, and relaxed memory models ^[3][5].

Such models have been used to ^[4]:

• Discover errata in multiprocessor implementations, both pre- and post-silicon.
• Formally verify compilation schemes (e.g., proving that C/C++11 concurrency can be correctly compiled to POWER).
• Support operating-system kernel concurrency primitive development.

Limitations

The envelope model approach involves trade-offs. Finding all executions of concurrent programs is combinatorially challenging, so such tools are best suited as references for small-but-intricate test programs—such as those used in hardware testing and in implementations of OS synchronisation primitives and concurrent data structures—rather than as emulators for production-scale code ^[5].

Additionally, such models may have scope limitations: for example, they may handle only non-write-through cacheable coherent memory, omit exceptions and interrupts, floating point, instruction-cache effects, or supervisor features including page table manipulation ^[5]. The focus is on architectural completeness rather than performance modelling.