Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Extrapolation and Synthesis for Relaxed Memory Models
event speaker icon
Yuri Meshman (Ph.D. Thesis Seminar)
event date icon
Wednesday, 17.08.2016, 14:00
event location icon
Taub 601
event speaker icon
Advisor: Prof. E. Yahav
In modern architectures memory operations may be reordered and executed non-atomically. Consistency is guarantied for single thread execution, but not across threads. Both software and hardware Relaxed Memory Models are defined to capture the possible execution behaviors. 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++RMM 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, if verification fails, according to the relaxed memory model, we explore techniques to automatically synthesize program correction in the form of either memory fences or memory order parameters to memory operations. We show that our techniques can synthesize fences in challenging concurrent algorithms such as Ticket mutual exclusion algorithm, and several versions of Work Stealing Queues. As well as, how to synthesize memory order parameters for algorithms such as RCU.