Formalizing Shared Memory Consistency Models for Program Analysis
Abstract
Shared memory consistency models are critical for system correctness but difficult to analyze. The increasing popularity of
multithreaded programming also creates a new challenge in how to help programmers reason about thread executions against the
underlying memory consistency rules.
This dissertation addresses the problem of formally specifying memory models to support program analysis. Two analytical
frameworks are established to support both operational and non-operational specification styles. These frameworks are applied
to formalize a wide range of memory consistency designs, including classical, industrial processor level, and language level memory
models.
We first present an operational style specification framework called UMM, which supports a generic memory abstraction and
provides built-in model checking capability. Then we present Nemos, a non-operational specification framework that uses higher
order predicate logic to capture memory ordering constraints in a declarative and compositional fashion. After imposing the
consistency rules on a symbolic program execution, the validity of the execution can be automatically checked through constraint
solving or SAT solving. This method makes a memory model executable, a powerful feature lacking in previous non-operational
methods. Furthermore, a constraint-based approach is applied to specify control/data dependence and to capture
"programmer expectations". By combining the constraints of program properties
and language semantics, memory-model-sensitive program analysis can be automated. Three concrete applications of this approach are
proposed, including execution validation, race detection and atomicity verification.