Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8

Watch a 24-minute conference presentation from POPL 2018 exploring the evolution and simplification of ARM's memory model architecture. Dive into how ARM's concurrency model transitioned from non-multicopy-atomic to multicopy-atomic in ARMv8, examining the technical motivations and practical benefits behind this architectural shift. Learn about two formal concurrency models - an operational model that simplifies the Flowing model, and an axiomatic model from the revised ARMv8 specification - developed through collaboration between academic researchers and ARM engineers. Understand how these models were proven equivalent and integrated into an executable exploration tool with web interface, demonstrated through real-world examples including a Linux kernel lock implementation analysis. Gain insights into relaxed memory models, semantics, and the intersection of theoretical computer science and practical hardware architecture design.