A Study of Shared-Memory Mutual Exclusion Protocols using CADP

Radu Mateescu 1 Wendelin Serwe 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Mutual exclusion protocols are an essential building block of concurrent 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 in the shared-memory setting, 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 nonfunctional aspects, such as their performance in the long run. In this paper, we report on experiments with the 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, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved.
Liste complète des métadonnées

Littérature citée [43 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00532897
Contributeur : Christine Mckinty <>
Soumis le : jeudi 4 novembre 2010 - 16:40:27
Dernière modification le : mercredi 11 avril 2018 - 01:52:15
Document(s) archivé(s) le : samedi 5 février 2011 - 03:05:39

Fichier

mateescu_serwe.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00532897, version 1

Citation

Radu Mateescu, Wendelin Serwe. A Study of Shared-Memory Mutual Exclusion Protocols using CADP. 15th International Workshop on Formal Methods for Industrial Critical Systems '2010, Sep 2010, Antwerp, Belgium. 2010. 〈inria-00532897〉

Partager

Métriques

Consultations de la notice

265

Téléchargements de fichiers

121