To illustrate the power of SPIN let's have a look at an example. First we start with an extremely simple case and gradually increase the complexity. Let there be a multiprocessor system with two processors communicating via shared RAM and an interrupt signal. One directional communication is enough for our purposes.
The protocol is based on a simple idea: the sender writes information into a predefined location in the shared RAM and then asserts an interrupt which activates the receiver. The interrupt will be cleared after the receiver used up the data. Sender will wait for a low interrupt line to give time for the reader to consume the previously sent data.
A model for the protocol written in the promela language could be like this:
unsigned interrupt:1 = 0;
byte data; // represents shared RAM
proctype wr(byte d)
{
interrupt == 0 -> // wait for interrupt line to go low
data = d; // write data into shared RAM
interrupt = 1; // assert interrupt
}
active proctype rd()
{
do // loop forever
:: interrupt == 1 -> // activated by interrupt
// ... use up data
interrupt = 0; // quit interrupt
od
}
init
{
// start a process to send data
run wr(1);
}
To use SPIN in interpreter or simulator mode type in the following:
spin -p filenameA possible output could be:
Starting rd with pid 0
0: proc - (:root:) creates proc 0 (rd)
Starting :init: with pid 1
0: proc - (:root:) creates proc 1 (:init:)
Starting wr with pid 2
1: proc 1 (:init:) creates proc 2 (wr)
1: proc 1 (:init:) line 22 "stop" (state 1) [(run wr(1))]
2: proc 2 (wr) line 6 "stop" (state 1) [((interrupt==0))]
3: proc 2 (wr) line 7 "stop" (state 2) [data = d]
4: proc 2 (wr) line 8 "stop" (state 3) [interrupt = 1]
5: proc 0 (rd) line 13 "stop" (state 3) [((interrupt==1))]
6: proc 0 (rd) line 15 "stop" (state 2) [interrupt = 0]
6: proc 2 (wr) terminates
6: proc 1 (:init:) terminates
7: proc 0 (rd) line 17 "stop" (state 4) [.(goto)]
timeout
#processes: 1
interrupt = 0
data = 1
7: proc 0 (rd) line 13 "stop" (state 3)
3 processes created
Here we can see, that the wr process was able to start up because the interrupt line was 0. It first writes the information into the shared RAM data and then asserts the interrupt signal to wake up the receiver. The other side is activated by the interrupt signal. First it uses the data (the actual code is just indicated by ...), and then cleares the interrupt. The communication was successful.
To make the example a bit more realistic, we allow two concurrent processes to send information using the same algorithm. We also have to add some code to enable us to detect possible information loss or duplication. Whenever the receiver gets the new information it will remeber the fact using an array.
Here is the modified model
unsigned interrupt:1;
byte data; // represents shared RAM
byte rec [2]; // records arrival of data
proctype wr(byte d)
{
interrupt == 0 -> // wait for the interrupt line to go low
data = d; // write data into shared RAM
interrupt = 1; // assert interrupt
}
active proctype rd()
{
do // loop forever
:: interrupt == 1 -> // activated by interrupt
rec[data] = 1; // use up data, remember it
interrupt = 0; // quit interrupt
od
}
init
{
// start two processes to send data
run wr(0);
run wr(1);
// wait for the dust to settle
timeout ->
assert(rec[0] == 1 && rec[1] == 1);
}
Here two processes try to send data concurrently so there is a chance for race condition. The receiver will use the data as index into the rec array to mark the arrival of info. The init process can get to the last line only after there is no other activity possible in the model. By this time both messages should have arrived. Should any of them be missing, the assert statement would catch it.
On possible output of the SPIN simulator is:
Starting rd with pid 0
0: proc - (:root:) creates proc 0 (rd)
Starting :init: with pid 1
0: proc - (:root:) creates proc 1 (:init:)
Starting wr with pid 2
1: proc 1 (:init:) creates proc 2 (wr)
1: proc 1 (:init:) line 25 "stop" (state 1) [(run wr(0))]
Starting wr with pid 3
2: proc 1 (:init:) creates proc 3 (wr)
2: proc 1 (:init:) line 26 "stop" (state 2) [(run wr(1))]
3: proc 3 (wr) line 8 "stop" (state 1) [((interrupt==0))]
4: proc 3 (wr) line 9 "stop" (state 2) [data = d]
5: proc 3 (wr) line 10 "stop" (state 3) [interrupt = 1]
5: proc 3 (wr) terminates
6: proc 0 (rd) line 15 "stop" (state 4) [((interrupt==1))]
7: proc 0 (rd) line 17 "stop" (state 2) [rec[data] = 1]
8: proc 0 (rd) line 18 "stop" (state 3) [interrupt = 0]
9: proc 0 (rd) line 20 "stop" (state 5) [.(goto)]
10: proc 2 (wr) line 8 "stop" (state 1) [((interrupt==0))]
11: proc 2 (wr) line 9 "stop" (state 2) [data = d]
12: proc 2 (wr) line 10 "stop" (state 3) [interrupt = 1]
12: proc 2 (wr) terminates
13: proc 0 (rd) line 15 "stop" (state 4) [((interrupt==1))]
14: proc 0 (rd) line 17 "stop" (state 2) [rec[data] = 1]
15: proc 0 (rd) line 18 "stop" (state 3) [interrupt = 0]
16: proc 0 (rd) line 20 "stop" (state 5) [.(goto)]
timeout
17: proc 1 (:init:) line 28 "stop" (state 3) [(timeout)]
18: proc 1 (:init:) line 29 "stop" (state 4) [assert(((rec[0]==1)&&(rec[1]==1)))]
18: proc 1 (:init:) terminates
timeout
#processes: 1
interrupt = 0
data = 0
rec[0] = 1
rec[1] = 1
18: proc 0 (rd) line 15 "stop" (state 4)
4 processes created
Here one of the senders completes sending the message, then the reader reads it. The second sender will see the interrupt line go low so it can procede with sending a different value (so that we can recognize it) which will be read eventually by the reader. The communication succeeds. If we keep on re-running the simulator it will produce different runs. It is caused by the simulator making arbitrary scheduling decisions whenever the opporunity arises. In some runs the assertion gets violated, i.e. a message gets lost.
Let's see, what went wrong in the following run!
Starting rd with pid 0
0: proc - (:root:) creates proc 0 (rd)
Starting :init: with pid 1
0: proc - (:root:) creates proc 1 (:init:)
Starting wr with pid 2
1: proc 1 (:init:) creates proc 2 (wr)
1: proc 1 (:init:) line 25 "stop" (state 1) [(run wr(0))]
2: proc 2 (wr) line 8 "stop" (state 1) [((interrupt==0))]
Starting wr with pid 3
3: proc 1 (:init:) creates proc 3 (wr)
3: proc 1 (:init:) line 26 "stop" (state 2) [(run wr(1))]
4: proc 2 (wr) line 9 "stop" (state 2) [data = d]
5: proc 3 (wr) line 8 "stop" (state 1) [((interrupt==0))]
6: proc 3 (wr) line 9 "stop" (state 2) [data = d]
7: proc 2 (wr) line 10 "stop" (state 3) [interrupt = 1]
8: proc 0 (rd) line 15 "stop" (state 4) [((interrupt==1))]
9: proc 0 (rd) line 17 "stop" (state 2) [rec[data] = 1]
10: proc 3 (wr) line 10 "stop" (state 3) [interrupt = 1]
11: proc 0 (rd) line 18 "stop" (state 3) [interrupt = 0]
11: proc 3 (wr) terminates
11: proc 2 (wr) terminates
12: proc 0 (rd) line 20 "stop" (state 5) [.(goto)]
timeout
13: proc 1 (:init:) line 28 "stop" (state 3) [(timeout)]
spin: line 29 "stop", Error: assertion violated
spin: text of failed assertion: assert(((rec[0]==1)&&(rec[1]==1)))
#processes: 2
interrupt = 0
data = 1
rec[0] = 0
rec[1] = 1
14: proc 1 (:init:) line 29 "stop" (state 4)
14: proc 0 (rd) line 15 "stop" (state 4)
4 processes created
Here we can see the first writer starting up and actually copying the data into the shared RAM but before it would assert the interrupt, the second writer already has seen that the interrupt is low. Then the second writer proceeds (maybe because it has higher priority?) eventually overwriting the first data - before it was read! The protocol has lost a message!
After considering what caused the error, we might try to remedy the situation by restricting concurrency via interrupt disables on the sender's CPU. This can be modelled by the atomic keyword in Promela. It disables concurrency, once the opening '{' is entered, no other process has the chance to run, until the the closing '}'.
The model looks like this after the necessary modifications:
unsigned interrupt:1;
byte data; // represents shared RAM
byte rec [2]; // records arrival of data
proctype wr(byte d)
{
atomic {
interrupt == 0 -> // wait for interrupt line to go low
data = d; // write data into shared RAM
interrupt = 1; // assert interrupt
}
}
active proctype rd()
{
end: do // loop forever
:: interrupt == 1 -> // activated by interrupt
rec[data] = 1; // use up data, remember it
interrupt = 0; // quit interrupt
od
}
init
{
// start two processes to send data
run wr(0);
run wr(1);
// wait for the dust to settle
timeout ->
assert(rec[0] == 1 && rec[1] == 1);
}
Now we can run again the SPIN simulator and watch for failure. We won't see a message loss for a even after many runs. Does it mean, that we now know that the design is good? No, it only makes it probable. And if we keep on simulating for a longer time than it will be even more probable, but never certain.
To be certain, we need an other tool. We can ask SPIN to create a verifier based on our Promela model. It will exercise our model in every possible way and will detect if there is any way to violate the specifications. I could do it mentally in every imaginable way, but SPIN has frequently proven that my imagination is not always enough to find possible problems.
To create a verifier issue the commandspin -a filename
It will create a file, named pan.c, which needs to be compiled and linked into an executable program. This program is the verifier of our model. After running the program it declares the assertion in the model has never failed. It was interleaving the execution of the receiver and the two senders in every possible way to reach this conclusion.
What does this exactly mean? What did we prove? Well, we proved that the current design can send exactly two one byte messages, the message '0' and the message '1' without loosing it. This is not exactly what we were looking for. We want to know if messages can be lost or duplicated even if the system runs forever without regard of the message content. Of course the message size should not matter either. It would be relatively easy to change the model to send infinitely many messages, and we still could prove it correct at a cost of higher complexity. As far as the message conent is concerned, all we needed is the capability to distinguish the two messages, so '0' and '1' were fine to that end. Experience with SPIN shows that design problems typically show up within a few steps after system startup, so even this limited verification probably caught all the problems.
Let's have an other look at our achievement. To discover a bug like this would have meant to observe the system for an extended time under heavy load, possibly with program modification to automatically detect the problem.
Note: the Promela model describes two concurrently running processes using the same method to send information to the receiver. It also models a single process, sending two messages one after the other, as a special case.