Analysis of the Suzuki-Kasami algorithm with SAL model checkers

We report on a case study in which SAL model checkers have been used to analyze the Suzuki-Kasami distributed mutual exclusion algorithm with respect to the mutual exclusion property and the lockout freedom property. SAL includes five different model checkers. In the case study, we have used two model checkers SMC (symbolic model checker) and infBMC (infinite bounded model checker). SMC has concluded that a finite-state model of the algorithm has the mutual exclusion property, but has found a counterexample to the lockout freedom property. The counterexample has led to one possible modification that makes the algorithm lockout free. We have also used infBMC to prove that an infinite-state model of the algorithm has the mutual exclusion property by k-induction.