Yue Yang's Ph.D. Research
Research Overview
I was a member of the Utah Verifier Group. My thesis research focused on modeling shared memory consistency models and verifying multithreaded programs. This work has led to two analytical frameworks, supporting both non-operational and operational specification styles. With these frameworks, a multithreaded program can be automatically and rigorously analyzed for a given shared memory platform. I have also formalized a collection of classical memory models as well as several cutting-edge industrial designs such as the Intel Itanium Memory Model and the Java Memory Model.
Constraint-based Analytical Framework
To make a memory model specification both declarative and executable, we developed a constraint-based approach for modeling and reasoning about thread behaviors. In a nutshell, our method consists of the following steps: (1) define shared memory consistency requirements as a set of axioms using predicate logic, (2) formulate a program verification problem as a constraint satisfaction problem, and (3) employ an efficient solver to find the result automatically. We have pursued this research in three different but related directions, addressing each of the above steps.
We developed a specification framework called Nemos (Non-operational yet Executable Memory Ordering Specifications). We applied this framework to formalize the Intel Itanium Memory Model as well as a collection of classical memory models, such as sequential consistency (SC), coherence, PRAM, causal consistency, and processor consistency.
Related papers:
- Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT (abstract pdf ppt)
- Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models (abstract pdf)
Related tool:
To enable a rigorous program analysis for multithreaded software, we proposed to explicitly capture both the program semantics and the thread semantics, and model correctness properties ("programmer expectations") as additional constraints. We applied this method to enable three important analyses: execution validation, race analysis, and atomicity verification.
Related paper:
- Memory-Model-Sensitive Data Race Analysis (abstract ps)
- Rigorous Concurrency Analysis of Multithreaded Programs (abstract pdf)
Related tool:
We have harnessed our framework with various solvers (finite-domain constraint solver, SAT solver, and QBF solver), developed efficient encoding method for SAT generation, and applied incremental SAT solving methods. With these techniques, we are now in a position to perform practical verification in industrial settings.
Related paper:
- QB or not QB: An Efficient Execution Verification Tool for Memory Orderings (abstract pdf)
Operational Specification Framework with Built-in Model Checking Support
To create and analyze operational memory model specifications, I designed the UMM (Uniform Memory Model) specification framework which integrates two key features to support memory model verification:
- It employs a simple and generic memory abstraction that can capture a large collection of memory models as guarded commands with a uniform notation.
- It provides built-in model checking capability to enable formal reasoning about thread behaviors.
Memory models specified in UMM have a parameterized style, meaning designers can simply redefine a few bypassing rules and visibility ordering rules to obtain an executable specification of another memory model. Coupled with a model checker, the UMM framework can exhaustively exercise a test program to cover all thread interleavings.
We applied this framework to formalize several well known memory models, such as sequential consistency, coherence, and PRAM. We also developed an alternative formal specification of the Java memory model, based on an earlier proposal by Manson and Pugh. Our experience shows that making memory models executable greatly reduces the likelihood of having overlooked corner cases.
Related papers:
- UMM: An Operational Memory Model Specification Framework with Integrated Model Checking Capability (abstract pdf)
- Specifying Java Thread Semantics Using a Uniform Memory Model (abstract pdf ppt)
- Analyzing the CRF Java Memory Model (abstract pdf ppt)
Related tool:
Publications
My complete publication list is available here.