  The hardware/software boundary in modern heterogeneous multicore computers is
increasingly complex, and diverse across different platforms. A single memory
access by a core or DMA engine traverses multiple hardware translation and
caching steps, and the destination memory cell or register often appears at
different physical addresses for different cores. Interrupts pass through a
complex topology of interrupt controllers and remappers before delivery to one
or more cores, each with specific constraints on their configurations. System
software must not only correctly understand the specific hardware at hand, but
also configure it appropriately at runtime. We propose a formal model of
address spaces and resources in a system that allows us to express and verify
invariants of the system's runtime configuration, and illustrate (and motivate)
it with several real platforms we have encountered in the process of OS
implementation.
