t\"{a}k\={o}Formal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)

TL;DR

This paper introduces a formal memory consistency model for the t"{a}kf0 programmable memory hierarchy, enabling programmers to reason about its behavior and verify implementation correctness.

Contribution

It develops and proves the soundness of an ISA-level memory consistency model for t"{a}kf0, facilitating formal reasoning and verification of programmable memory hierarchies.

Findings

The ISA-level MCM accurately captures t"{a}kf0 semantics.

Verification confirms all implementation executions adhere to the MCM.

Insights into microarchitectural modeling applicable to hardware verification.

Abstract

Accelerators provide large performance and energy-efficiency benefits, but can significantly change the hardware-software interface. The t\"{a}k\={o} programmable memory hierarchy accelerates data movement by enabling programmers to run user-defined callback functions triggered by cache misses, evictions, and writebacks. However, it also leads to drastically increased complexity and counterintuitive outcomes. In response, we develop an ISA-level memory consistency model (MCM) for t\"{a}k\={o} that captures the semantics of its operation, and we show how it enables programmers to formally reason about their t\"{a}k\={o} programs. We also prove the soundness of this ISA-level MCM by constructing a detailed t\"{a}k\={o} implementation model and verifying that all executions of the implementation model are allowed by our ISA-level MCM. Along the way, we discover useful insights about microarchitectural modeling and verification that are applicable to hardware in general. This is the extended version of the ISCA 2026 paper "t\"{a}k\={o}Formal: Enabling Robust Software for Programmable Memory Hierarchies". This version adds material on additional litmus tests to Section V to further explore the programmability of t\"{a}k\={o} using our ISA-level MCM.