salle C. Shannon CE4
12 juillet 2012 - 14h00
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
par Roberto Bruttomesso de ATRENTA
Abstract: Deadlock-free algorithms that ensure mutual exclusion cru- cially
depend on timing assumptions. In this paper, we describe our expe-
rience in automatically verifying mutual-exclusion and
deadlock-freedom of the Fischer and Lynch-Shavit algorithms, using the
model checker modulo theories mcmt. First, we explain how to specify
timing-based algorithms in the mcmt input language as symbolic
transition systems. Then, we show how the tool can verify all the
safety properties used by Lynch and Shavit to establish
mutual-exclusion, regardless of the num- ber of processes in the
system. Finally, we verify deadlock-freedom by following a reduction
to “safety problems with lemmata synthesis” and using acceleration to
avoid divergence. We also show how to automatically synthesize the
bounds on the waiting time of a process to enter the critical section.
