| 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 nonoperational 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 nonoperational 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 nonoperational 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. |
