Reference : A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/91581
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
English
Linden, Alexander mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Dép. d'électric., électron. et informat. (Inst.Montefiore) >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > informatique > >]
Jul-2011
Lecture Notes in Computer Science
Springer
Model Checking Software , 18th International SPIN Workshop, Proceedings
144-160
Yes
International
0302-9743
1611-3349
Berlin
Germany
Model Checking Software , 18th International SPIN Workshop
July 14-15, 2011
Cliff Lodge, Snowbird, Utah
USA
[en] model-cheking ; relaxed memory models ; finite automata ; memory fence insertion
[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.
Researchers
http://hdl.handle.net/2268/91581
10.1007/978-3-642-22306-8_10
http://link.springer.com/chapter/10.1007/978-3-642-22306-8_10
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
LW SPIN2011.pdfAuthor postprint325.51 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.