An Operational Semantics of Cache Coherent Multicore Architectures

Abstract

This paper presents a formal semantics of multicore architectures with private cache, shared memory, and instantaneous inter-core communications. The purpose of the semantics is to provide an operational understanding of how low-level read and write operations interact with caches and main memory. The semantics is based on an abstract model of cache coherence and allows formal reasoning over parallel programs that execute on any given number of cores. We prove correctness properties expressed as invariants for the preservation of program order, data-race free execution of low-level operations, and no access to stale data.