täkōFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915982034862080 |
|---|---|
| author | Srinivasan, Pranav Kapritsos, Manos Manerkar, Yatin A. |
| author_facet | Srinivasan, Pranav Kapritsos, Manos Manerkar, Yatin A. |
| contents | Accelerators provide large performance and energy-efficiency benefits, but can significantly change the hardware-software interface. The täkō 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äkō that captures the semantics of its operation, and we show how it enables programmers to formally reason about their täkō programs. We also prove the soundness of this ISA-level MCM by constructing a detailed täkō 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äkō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äkō using our ISA-level MCM. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_04172 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | täkōFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version) Srinivasan, Pranav Kapritsos, Manos Manerkar, Yatin A. Hardware Architecture Logic in Computer Science Accelerators provide large performance and energy-efficiency benefits, but can significantly change the hardware-software interface. The täkō 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äkō that captures the semantics of its operation, and we show how it enables programmers to formally reason about their täkō programs. We also prove the soundness of this ISA-level MCM by constructing a detailed täkō 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äkō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äkō using our ISA-level MCM. |
| title | täkōFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version) |
| topic | Hardware Architecture Logic in Computer Science |
| url | https://arxiv.org/abs/2605.04172 |