We have developed a constraint-based approach for specifying thread
semantics and reasoning about multithreaded programs.
In a nutshell, our method consists of the following steps:
(1) Define shared memory consistency requirements as a set of axioms;
(2) Formulate a program verification problem as a constraint satisfaction
problem;
(3) Employ an efficient solver (constraint solver, SAT solver, or QBF
solver) to find the result automatically.
We have pursued this research in three different but related directions,
addressing each of the above steps:
(1) Specifying a memory model;
(2) Modeling program properties for multithreaded software;
(3) Improving the efficiency and scalability of the solving method.
To make a memory model specification both declarative and executable, we
developed a framework called Nemos (Non-operational yet Executable Memory
Ordering Specifications). We have applied this framework to formalize the
Intel Itanium memory ordering rules as well as a collection of "classical"
memory models, such as sequential consistency (SC), coherence, PRAM, causal
consistency, and processor consistency.
To enable a rigorous program analysis, we developed a method that
precisely captures both the program semantics (including thread-local
data/control dependence) and the memory model semantics, and models
correctness properties ("programmer expectations") as additional
constraints. We further applied this method to enable three important
analyses: execution validation, race analysis, and atomicity verification.
We have formalized SC for a Java-like source language, which should be
useful for the JMM community since race conditions in Java will be defined
using SC executions.
Related papers and software tools are available at
http://www.cs.utah.edu/~yyang. We invite you to visit our web site to find
out more information.
Your comments will be greatly appreciated!
- Jason
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:57 EDT