Deadlock-free algorithms that ensure mutual exclusion crucially depend on timing assumptions. In this paper, we describe our experience 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 number 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. © 2012 Springer-Verlag.

Automated analysis of parametric timing-based mutual exclusion algorithms / Bruttomesso, R.; Carioni, A.; Ghilardi, S.; Ranise, S.. - 7226:(2012), pp. 279-294. ((Intervento presentato al convegno 4th NASA Formal Methods Symposium, NFM 2012 tenutosi a Norfolk, VA, usa nel 2012 [10.1007/978-3-642-28891-3_28].

Automated analysis of parametric timing-based mutual exclusion algorithms

Ranise S.
2012-01-01

Abstract

Deadlock-free algorithms that ensure mutual exclusion crucially depend on timing assumptions. In this paper, we describe our experience 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 number 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. © 2012 Springer-Verlag.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-642-28890-6
978-3-642-28891-3
Bruttomesso, R.; Carioni, A.; Ghilardi, S.; Ranise, S.
Automated analysis of parametric timing-based mutual exclusion algorithms / Bruttomesso, R.; Carioni, A.; Ghilardi, S.; Ranise, S.. - 7226:(2012), pp. 279-294. ((Intervento presentato al convegno 4th NASA Formal Methods Symposium, NFM 2012 tenutosi a Norfolk, VA, usa nel 2012 [10.1007/978-3-642-28891-3_28].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/332987
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact