Applications of Formal Methods in Computer Architecture
This blog post samples a growing body of research which leverages formal methods techniques to solve computer architecture challenges. While certainly not exhaustive, it is meant to serve as a starting point for further reading and brainstorming.
This blog post focuses on a couple popular property classes in modern hardware verification and validation research, which aim to address the following challenges:
Given the above challenges, researchers have produced both hardware system and property formalizations to support reasoning about the implications of microarchitecture on program correctness and security. This section summarizes a handful of such formalization efforts, which underpin many of the formal verification approaches discussed later in this blog post.
To facilitate formal reasoning about concurrent program correctness, research over the past ~15 years has produced formally-specified memory consistency models (or MCMs). Simply put, MCMs specify the values that can be legally returned by shared memory loads in a concurrent program via constraints on the legal ordering and visibility of shared memory accesses. Notably, a sound high-level programming language MCM is not sufficient to ensure correct execution of a parallel program. In particular, a program is only guaranteed to run correctly if a compiler correctly translates language-level MCM primitives to assembly instructions, and if the target microarchitecture is indeed implementing the MCM specified by its ISA. Thus, MCM formalization efforts span the hardware-software stack. At the ISA-level, the following MCMs have all been formalized: x86-TSO, IBM Power, NVIDIA PTX, RISC-V RVWMO, RISC-V RVTSO, ARMv7, ARMv8 [ 30 , 31 , 32 , 33 , 28 , 29 , 34 ]. At the microarchitecture-level, the Check tools [ 51 , 52 , 53 , 54 , 55 , 57 ] provide a first-order logic DSL for specifying hardware designs, including their MCM implementation, axiomatically.
