Reference : An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/65125
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
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 > Services administratifs généraux > Vice-Recteur à la Recherche - Informatique (parallélisme et banques de données) >]
Sep-2010
Lecture Notes in Computer Science
Springer
Model Checking Software , 17th International SPIN Workshop, Proceedings
212-226
Yes
International
0302-9743
1611-3349
Berlin
Germany
17th International SPIN Workshop
September 29-30, 2010
Enschede
Netherlands
[en] model-cheking ; relaxed memory models ; finite automata
[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.
Researchers
http://hdl.handle.net/2268/65125
10.1007/978-3-642-16164-3_16
http://www.springerlink.com/content/e13un22154g5p72h/
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
LW SPIN2010.pdfAuthor postprint196.8 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.