Université de Liège Réseau des Bibliothèques

BICTEL/e - ULg
Serveur institutionnel des thèses de doctorat



Nouvelles thèses
dans BICTEL/e - ULg
  • Lambert, Justine - Implication de la Transition Epithélio-Mésenchymateuse dans la coagulation et les étapes précoces de la dissémination métastatique.
  • Donati, Kim - Impact des modulations du microenvironnement et de la niche prémétastatique dans l’émergence des métastases pulmonaires.
  • Jeunehomme, Olivier - Temporal compression of events in episodic memory/La compression temporelle des événements en mémoire épisodique
Présentation Recherche thèse Dépôt thèse Accès
gestionnaires
 
Page de résumé pour ULgetd-12032013-215858

Auteur : Linden, Alexander
URN : ULgetd-12032013-215858
Langue : Anglais/English
Titre : On the Verification of Programs on Relaxed Memory Models
Intitulé du diplôme : Doctorat en sciences (orientation informatique)
Département : FSA - Département d'électricité, électronique et informatique
Jury :
Nom : Titre :
Gribomont, Pascal Président du jury/Committee Chair
Wolper, Pierre Promoteur/Director
Mots-clés :
  • fence insertion
  • verification
  • model-checking
  • relaxed memory models
  • finite automata
  • total store order
  • partial store order
Date de soutenance : 2013-12-05
Type d'accès : Public/Internet
Résumé :

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.

Autre version : http://hdl.handle.net/2268/158670
Fichiers :
Nom du fichier Taille Temps de chargement évalué (HH:MI:SS)
Modem 56K ADSL
[Public/Internet] thesis.pdf 1.38 Mb 00:03:16 00:00:07

Bien que le maximum ait été fait pour que les droits des ayants-droits soient respectés, si un de ceux-ci constatait qu'une oeuvre sur laquelle il a des droits a été utilisée dans BICTEL/e ULg sans son autorisation explicite, il est invité à prendre contact le plus rapidement possible avec la Direction du Réseau des Bibliothèques.


Parcourir BICTEL/e par Auteur|Département | Rechercher dans BICTEL/e


© Réseau des Bibliothèques de l'ULg, Grande traverse, 12 B37 4000 LIEGE