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 automati- cally synthesize the bounds on the waiting time of a process to enter the critical section.
Automated analysis of parametric timing based mutual exclusion protocols / R. Bruttomesso, A. Carioni, S. Ghilardi, S. Ranise - In: NASA formal methods : 4th international symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012 : proceedings / [a cura di] A. E. Goodloe, S. Person. - Berlin : Springer, 2012 Apr. - ISBN 9783642288906. - pp. 279-294 (( Intervento presentato al 4. convegno NASA Formal Methods Symposium tenutosi a Norfolk nel 2012 [10.1007/978-3-642-28891-3_28].
Automated analysis of parametric timing based mutual exclusion protocols
S. GhilardiPenultimo
;
2012
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 automati- cally synthesize the bounds on the waiting time of a process to enter the critical section.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.