Jan 13, 2025
I came across a fascinating and surprising aspect of a seemingly simple concurrent program when run on a model checker. Consider this:
If we run P and Q concurrently, with ‘n’ initialized to zero, what would the value of ‘n’ be when the two processes finish executing their statements?
I thought the final value of ‘n’ would be between 10 and 20. What do you think? Take a guess.
I came across this in Ben-Ari’s book on the SPIN model checker [1]. He said he was shocked to find out that the final value could be as low as 2. I was shocked as well—the outcome completely defied my intuition.
To see this in action, we could write a simple program in SPIN and claim that there is a computation where the value is 2. We can obtain this computation automatically by adding the assertion assertion (n > 2) at the end of the program and running a verification. SPIN searches the state space, looking for counterexamples.
Here is the program followed by the trai
