|Ph.D Student||Meshman Yuri|
|Subject||Extrapolation and Synthesis for Relaxed Memory Models|
|Department||Department of Computer Science||Supervisor||Professor Eran Yahav|
|Full Thesis text|
In modern architectures memory operations may be reordered and executed non-atomically. Consistency is guaranteed for single thread execution, but not across threads, making it hard to reason about program correctness. Both software and hardware Relaxed Memory Models are defined to capture the possible execution behaviors where consistency is not guaranteed. Each Relaxed Memory Model poses its own challenges to successful program verification, and, in
cases where verification fails, poses its own challenges to automatic synthesis of program
Our work covers Intel's x-86 TSO and PSO hardware buffered memory models, as well as the C? software memory model. We explore such abstraction techniques
as Predicate Abstraction and Numerical Abstract Domains, to deal with both finite-state and infinite-state domains. In addition, we explore techniques to automatically synthesize program
corrections when verification fails. The program corrections, are either memory fences or
memory order parameters for memory operations, in accordance with the Relaxed Memory Model.
Where possible, we utilize the proof of program correctness from the more intuitive SC domain, extrapolating it to alleviate the complexity of proving program correctness under the Relaxed Memory Model. In addition, we show how to apply the approach of proof extrapolation from a simple to a more complex domain in domains other than Relaxed Memory Model.
We show that our techniques can synthesize fences in challenging concurrent algorithms such as the Ticket mutual exclusion algorithm, and several versions of Work Stealing Queues, and that they can synthesize, memory order parameters for algorithms such as RCU.