Finding your first deadlock and livelock with the Spin model checker

Date: 2015-04-07

Updated: 2020-10-27, when I wrote this article and retested everything.

Exercises in agreement

Jump to the setup instructions below if you haven’t installed spin or my helper scripts (spinsafe, spinlive, spinltl, and spinplay).

Download agreepair.pml (or view it on GitHub). This Promela code models a pair of processes that should eventually agree to have the same x value, which can be any integer from 0 to 5. It doesn’t quite work though. Using Spin, perhaps you can fix it!

Exercise 1: Verify the program’s safety properties

Exercise 1.a. What is the deadlock (aka invalid end state) that you find?

Exercise 1.b. How can the deadlock be fixed?
Make the fix and verify that no deadlocks exist.

Exercise 2: Verify the program’s LTL properties

Exercise 2.a. Verify the LTL claim named close_enough.
Instructions: Uncomment the claim by changing #if 0 to #if 1 near the end of the file.

This should succeed if the deadlock was fixed in the previous exercise.

Exercise 2.b. Verify the LTL claim named exactly_equal.
Instructions: Same as before, but change #if 1 back to #if 0, and change #elif 0 to #elif 1.

This should fail, but we’ll fix it in the next exercise.

Exercise 3: Verify the program’s other liveness properties

Exercise 3.a. What is the livelock (aka non-progress cycle) that you find?

Exercise 3.b. How can the livelock be fixed without adding an atomic block? Remove the livelock and verify that no other livelocks exist.

Setting up Spin

We will use stow as a maintainable way of installing files as a normal user in ~/local/bin. Follow these instructions to install it and configure your system accordingly.

Install helper scripts

I wrote some scripts for checking safety properties (spinsafe), liveness properties (spinlive), LTL properties (spinltl), and replaying a trace (spinplay). They handle the spin invocation, compile the verifier, run the verifier, and remove temporary files (review it on GitHub). The scripts also try to give helpful context and advice to avoid common pitfalls.

To install, run the following commands:

mkdir -p ~/local/stow/$release_name/bin
cd ~/local/stow/$release_name/bin
curl "$release_name/{spinsafe,spinlive,spinltl,spinplay}" -o "#1"
chmod 0755 spinsafe spinlive spinltl spinplay
cd ~/local/stow
stow $release_name

For completeness, the individual files are: spinsafe, spinlive, spinltl, spinplay

Install Spin

Ideally you can obtain spin (which comes with ispin) through a Linux package manager:

Otherwise, run the following to install in your ~/local/ directory:

mkdir -p ~/local/src
cd ~/local/src
git clone $release_name
cd $release_name
make -C Src
mkdir -p ~/local/stow/$release_name/bin
install --mode 0755 -T Src/spin ~/local/stow/$release_name/bin/spin
install --mode 0755 -T optional_gui/ispin.tcl ~/local/stow/$release_name/bin/ispin
cd ~/local/stow
stow $release_name

Install Vim settings

If you use Vim, the following will set up indentation and syntax for Promela (the language of Spin models).

mkdir -p ~/.vim/indent ~/.vim/syntax
curl https:// -o ~/.vim/indent/promela.vim
curl https:// -o ~/.vim/syntax/promela.vim
echo 'autocmd BufNewFile,BufRead *.pml set ft=promela sw=2 ts=2' >> ~/.vim/filetype.vim

If you don’t have a ~/.vimrc already, this will make it:

cat > ~/.vimrc <<"HERE_DOCUMENT"
set nocompatible
set expandtab
filetype on
filetype plugin indent on
syntax enable

If you have no idea what’s going on with this editor: