INRIA Grenoble - Rhône-Alpes / VASY (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
2010 - 2011
5,300 lines of LNT
300 lines of MCL
500 lines of SVL
up to 1.6 billion states and 2.7 billion transitions
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.).
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 experminental measures
published in the literature.
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
INRIA Grenoble - Rhône-Alpes / VASY project-team
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|