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

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 pro-tected 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 func-tional correctness of these protocols has been studied extensively, relatively little atten-tion 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 check-ing 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