spin
Herramienta de verificación formal de aplicaciones de software multihilo. Para usar SPIN, se describe el comportamiento concurrente del software en un lenguaje especializado llamado PROMELA [PROcess MEta LAnguage].
Un ejemplo de uso con dos procesos que intentan adquirir dos cerrojos (lockA y lockB), pero en orden diferente
$ nano deadlock.pml
/* deadlock.pml */
bool lockA = false;
bool lockB = false;
active proctype Proceso1() {
/* Intenta adquirir A y luego B */
(lockA == false) -> lockA = true;
(lockB == false) -> lockB = true;
/* Sección crítica */
lockB = false;
lockA = false;
}
active proctype Proceso2() {
/* Intenta adquirir B y luego A (orden inverso -> potencial deadlock) */
(lockB == false) -> lockB = true;
(lockA == false) -> lockA = true;
/* Sección crítica */
lockA = false;
lockB = false;
}
$ spin deadlock.pml
$ gcc -o pan pan.c
$ spin -a deadlock.pml
$ gcc -o pan pan.c
$ ./pan
$ spin -t -p deadlock.pml
$ spin -p deadlock.pml
$ spin -g deadlock.pml