טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentMeshman Yuri
SubjectExtrapolation and Synthesis for Relaxed Memory Models
DepartmentDepartment of Computer Science
Supervisor Professor Eran Yahav
Full Thesis textFull thesis text - English Version


Abstract


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

corrections.


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.