Doctoral thesis (Dissertations and theses)
On the Verification of Programs on Relaxed Memory Models
Linden, Alexander
2013
 

Files


Full Text
thesis.pdf
Publisher postprint (1.38 MB)
Download

All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
relaxed memory models; verification; model-checking; total store order; partial store order; fence insertion; finite automata
Abstract :
[en] Classical model-checking tools verify concurrent programs under the traditional "Sequential Consistency" (SC) memory model, in which all accesses to the shared memory are immediately visible globally, and where model-checking consists in verifying a given property when exploring the state space of a program. However, modern multi-core processor architectures implement relaxed memory models, such as "Total Store Order" (TSO), "Partial Store Order" (PSO), or an extension with locks such as "x86-TSO", which allow stores to be delayed in various ways and thus introduce many more possible executions, and hence errors, than those present in SC. Of course, one can force a program executed in the context of a relaxed memory system to behave exactly as in SC by adding synchronization operations after every memory access. But this totally defeats the performance advantage that is precisely the motivation for implementing relaxed memory models instead of SC. Thus, when moving a program to an architecture implementing a relaxed memory model (which includes most current multi-core processors), it is essential to have tools to help the programmer check if correctness (e.g. a safety property) is preserved and, if not, to minimally introduce the necessary synchronization operations. The proposed verification approach uses an operational store-buffer-based semantics of the chosen relaxed memory models and proceeds by using finite automata for symbolically representing the possible contents of the buffers. Store, load, commit and other synchronization 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, and that it is compatible with partial-order reduction techniques. 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 even check designs that may contain cycles. This verification approach then serves as a basis to a memory fence insertion algorithm that finds how to preserve the correctness of a program when it is moved from SC to TSO or PSO. Its starting point is a program that is correct for the sequential consistency memory model (with respect to a given safety property), but that might be incorrect under TSO or PSO. This program is then analyzed for the chosen relaxed memory model and when errors are found (a violated safety property), 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.
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)
Language :
English
Title :
On the Verification of Programs on Relaxed Memory Models
Defense date :
05 December 2013
Institution :
ULiège - Université de Liège
Degree :
Doctorat en Sciences, orientation Informatique
Promotor :
Wolper, Pierre  ;  Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore)
President :
Gribomont, Pascal ;  Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore)
Jury member :
Vechev, Martin
Boigelot, Bernard  ;  Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science
Raskin, Jean-François
Bouajjani, Ahmed
Available on ORBi :
since 24 November 2013

Statistics


Number of views
173 (24 by ULiège)
Number of downloads
450 (9 by ULiège)

Bibliography


Similar publications



Contact ORBi