# Formalizing Memory Accesses and Interrupts

## TL;DR

This paper introduces a formal model for understanding and verifying the complex hardware and software interactions involved in memory accesses and interrupts in modern heterogeneous multicore systems.

## Contribution

It presents a formal framework for modeling address spaces and resources, enabling verification of system invariants across diverse hardware platforms.

## Key findings

- Formal model captures complex memory access pathways.
- Model helps verify correct configuration of hardware resources.
- Applicable to real-world heterogeneous multicore systems.

## Abstract

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.