Technical Report PHD-2017-04

TR#:PHD-2017-04
Class:PHD
Title: Extrapolation and Synthesis for Relaxed Memory Models
Authors: Yuri Meshman
Supervisors: Eran Yahav
PDFCurrently accessibly only within the Technion network
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++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, 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.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2017/PHD/PHD-2017-04), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the PHD technical reports of 2017
To the main CS technical reports page

Computer science department, Technion
admin