Paper published in a journal (Scientific congresses and symposiums)
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
Linden, Alexander; Wolper, Pierre
2010In Lecture Notes in Computer Science, p. 212-226
Peer reviewed
 

Files


Full Text
LW SPIN2010.pdf
Author postprint (201.53 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
Abstract :
[en] This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers. The proposed approach proceeds by using finite automata to symbolically represent the possible contents of the store buffers. Store, load and commit operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach.
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 > Services administratifs généraux > Vice-Recteur à la Recherche - Informatique (parallélisme et banques de données)
Language :
English
Title :
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
Publication date :
September 2010
Event name :
17th International SPIN Workshop
Event place :
Enschede, Netherlands
Event date :
September 29-30, 2010
Audience :
International
Journal title :
Lecture Notes in Computer Science
ISSN :
0302-9743
eISSN :
1611-3349
Publisher :
Springer, Berlin, Germany
Special issue title :
Model Checking Software , 17th International SPIN Workshop, Proceedings
Pages :
212-226
Peer reviewed :
Peer reviewed
Available on ORBi :
since 02 July 2010

Statistics


Number of views
308 (84 by ULiège)
Number of downloads
255 (31 by ULiège)

Scopus citations®
 
30
Scopus citations®
without self-citations
28
OpenCitations
 
28

Bibliography


Similar publications



Contact ORBi