Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2012

Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols

Radu Mateescu
  • Fonction : Auteur
  • PersonId : 834239
Wendelin Serwe
  • Fonction : Auteur
  • PersonId : 844454

Résumé

Mutual exclusion protocols are an essential building block of concurrent shared-memory systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurrent non-atomic accesses. Hence, many variants of mutual exclusion protocols exist, such as Peterson's or Dekker's well-known protocols. Although the functional correctness of these protocols has been studied extensively, relatively little attention has been paid to their non-functional aspects, such as their performance in the long run. In this paper, we report on experiments with the CADP toolbox for model checking and performance evaluation of mutual exclusion protocols using Interactive Markov Chains. Steady-state analysis provides an additional criterion for comparing protocols, which complements the verification of their functional properties. We also carefully re-examined the functional properties of these protocols, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved.
Fichier principal
Vignette du fichier
Mateescu-Serwe-12.pdf (1.16 Mo) Télécharger le fichier
Serwe-FMICS-10-v2.pdf (3.36 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre

Dates et versions

hal-00671321 , version 1 (17-02-2012)

Identifiants

Citer

Radu Mateescu, Wendelin Serwe. Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols. Science of Computer Programming, 2012, 78 (7), pp.843-861. ⟨10.1016/j.scico.2012.01.003⟩. ⟨hal-00671321⟩
532 Consultations
448 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More