Paper published in a book (Scientific congresses and symposiums)
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Linden, Alexander; Wolper, Pierre
2011In Model Checking Software , 18th International SPIN Workshop
Peer reviewed
 

Files


Full Text
LW SPIN2011.pdf
Author postprint (333.32 kB)
Download

The original publication is available at www.springerlink.com


All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
model-cheking; relaxed memory models; finite automata; memory fence insertion
Abstract :
[en] This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers, and its extension x86-TSO, which in addition allows synchronization and lock operations. The proposed approach uses a previously developed verification tool that uses finite automata to symbolically represent the possible contents of the store buffers. Its starting point is a program that is correct for the usual sequential consistency memory model, but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (with respect to safety properties), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen. An advantage of our technique is that the underlying symbolic verification tool makes a full exploration possible even for cyclic programs, which makes our approach broadly applicable. The method has been tested with an experimental implementation and can effectively handle a series of classical examples.
Disciplines :
Computer science
Author, co-author :
Linden, Alexander ;  Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Dép. d'électric., électron. et informat. (Inst.Montefiore)
Wolper, Pierre  ;  Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > informatique
Language :
English
Title :
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Publication date :
July 2011
Event name :
Model Checking Software , 18th International SPIN Workshop
Event place :
Cliff Lodge, Snowbird, Utah, United States
Event date :
July 14-15, 2011
Audience :
International
Main work title :
Model Checking Software , 18th International SPIN Workshop
Publisher :
Springer, Berlin, Germany
ISBN/EAN :
978-3-642-22305-1
Collection name :
Lecture Notes in Computer Science, vol. 6823
Pages :
144-160
Peer reviewed :
Peer reviewed
Available on ORBi :
since 23 May 2011

Statistics


Number of views
264 (57 by ULiège)
Number of downloads
304 (4 by ULiège)

Scopus citations®
 
25
Scopus citations®
without self-citations
24
OpenCitations
 
21

Bibliography


Similar publications



Contact ORBi