Real engineers, when faced with complex design problems build and analyze prototypes to reduce the risk of implementing a flawed design. Can the same be done with software also? How can we show if the system meets its design requirements? It is hard to devise all the possible test cases especially for concurrent software.
One of the most powerful formal methods is model checking. In principle model checking generates all possible states of a program and checks that the correctness specifications hold in each state. Model checking is challenging because the model should describe the system in sufficient detail and yet the model must be sufficiently simple so that the model checker can perform the verification within the reasonable limits of time and memory.
In this blog post I will model the Peterson’s algorithm and verify the mutual exclusion property. We will use Spin model checker. Spin accepts design specification in the verification language Promela. Promela is not an implementation language but a systems description language. The emphasis in the language is on the modelling of process synchronization and coordination, and not on computation.
/** Model specified using Promela for Peterson's algorithm **/Correctness claims are specified in the syntax of standard Linear Temporal Logic – a logic which is built for reasoning about things that change over time. Mutual exclusion can be expressed using the temporal operator for always – [].
/* condition for mutual exclusion */
#define mutex (critical <= 1)
/* flag value is 1 when the process wants to enter CS */
/* turn holds the ID of the process whose turn it is */
bool flag[2], turn;
/* number of processes in the critical section */
byte critical = 0;
/* instantiating two processes */
active [2] proctype process()
{
/* process identifiers start from 0 */
pid i = _pid;
pid j = 1 - _pid;
/* do statement*/
do
/* only one choice for execution */
:: /* process wants to enter CS */
flag[i] = true;
/* but asks other process to go ahead */
turn = j;
/* wait until the other process is not interested, */
/* or it is his own turn */
/* process is blocked until the statement is true */
!(flag[j] && turn == j);
/* critical section */
critical++;
critical--;
/* end of critical section */
flag[i] = false;
od;
}
For verification, the negation of the LTL formula is added with the -a argument (verification mode) and -f argument (fairness condition of contention manager) to the Spin command which generates the C source code for the model checker. The file is compiled with the -DSAFETY argument so that it is optimized for checking safety properties. Absence of an example on executing pan will indicate that the property is not violated.
$ spin -a -f '![]mutex' peterson.pmlFortunately there is no ‘Model Checking for Dummies’ book as of now. To get started on this subject, I would suggest that you read the chapter on ‘Verification by Model Checking’ in the book Logic in Computer Science followed by the manual of the appropriate model checker.
$ gcc -DSAFETY -o pan pan.c
$ ./pan
