Database of Case Studies Achieved Using CADP

Mutual Exclusion Protocols

Organisation: INRIA Grenoble - Rhône-Alpes / VASY (FRANCE)

Method: LNT
MCL
SVL

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed Algorithms.

Period: 2010 - 2011

Size: 5,300 lines of LNT
300 lines of MCL
500 lines of SVL
up to 1.6 billion states and 2.7 billion transitions

Description: Mutual exclusion protocols are an essential building block of concurrent systems to ensure proper use of shared resources in the presence of concurrent accesses. Many variants of mutual exclusion protocols exist for shared memory, 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 performance aspects.

VASY undertook a study of these protocols, by considering a set of 27 mutual exclusion protocols for up to sixteen processes with a shared memory and coherent caches. Each protocol was specified in LNT using a set of generic modules to describe shared variables and the overall architecture. Then, the LNT specifications were extended compositionally with Markov delays modelling the latencies of read/write accesses on shared variables, so as to obtain the Interactive Markov Chain (IMC) corresponding to each protocol.

Functional verification was carried out by considering the following properties: mutual exclusion, livelock and starvation freedom, independent progress, and unbounded overtaking. These properties were expressed as MCL formulas: the first property belongs to the alternation-free fragment of modal mu-calculus, whilst the last four properties are of alternation depth two, requiring the use of the infinite looping operator of MCL (which can be checked in linear-time). Finally, using the performance evaluation tools of CADP, the steady-state throughputs of the critical section accesses were computed, by varying several parameters (relative speeds of processes, ratio between the time spent in critical and non-critical sections, etc.).

Conclusions: This study made it possible to compare the protocols according to their efficiency (steady-state throughputs). It was observed that symmetric protocols are more robust when the difference in execution speed between processes is large, which confirms the importance of the symmetry requirement originally formulated by Dijkstra. The quantitative results corroborated those of functional verification: the presence of (asymmetric) starvation of processes, detected using temporal formulas, was clearly reflected in their steady-state throughputs. The results also correspond to experimental measures published in the literature.

Publications: [Mateescu-Serwe-10] Radu Mateescu and Wendelin Serwe. "A Study of Shared-Memory Mutual Exclusion Protocols using CADP". Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2010, Lecture Notes in Computer Science vol. 6371, pages 180-197. Springer Verlag, September 2010.
Available on-line from http://cadp.inria.fr/publications/Mateescu-Serwe-10.html

[Mateescu-Serwe-13] Radu Mateescu and Wendelin Serwe. "Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols". Science of Computer Programming, 2013.
Available on-line from http://cadp.inria.fr/publications/Mateescu-Serwe-13.html

Contact:
Wendelin Serwe
INRIA Grenoble - Rhône-Alpes / VASY project-team
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
FRANCE
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
Email: Wendelin.Serwe@inria.fr
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page