The Taub Faculty of Computer Science Events and Talks

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.