A Formal Model for Microprocessor Caches

Abstract:- Contemporary processors have reached a bewildering level of complexity featuring multiple execution pipelines, out-of-order instruction issuing, speculative execution, various prediction components and cache memories. The performance of these components is sometimes not well understood. To facilitate the analysis of these components, we propose the use of formal models of these components. Hereby, we aim to lay a formal basis for reasoning on processor components and to formally proove their properties. In this paper, we develop an operational semantics of cache memories and show how it describes operational aspects of caches. Key-words:- operational semantics, microarchitecture, cache