this is my first Q on Stack Exchange so if there's anything that's breaking guidelines please let me know.
I have a program written in Promela for a college OS and concurrent systems class. There are two processes running that increment a variable n. Our task is to write the processes and then use the verification tool in Spin to prove that it is possible for n to take on the value 4. I've had a read through all of the command line arguments and messed around but nothing strikes out to me as the "insert this modifier followed by a variable name to check all it's possible values."
byte n;
proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
init
{
run p();
run q();
}
There are several ways to do that, though as a teacher I would prefer the ltl based one, since at least it shows you understand how to use it.
Monitor Process.
This is by far the simplest, conceptually: you simply add a process that asserts that n != 4 at any time, and then check whether this assertion eventually fails or not.
byte n;
active proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
active proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
active proctype monitor()
{
do
:: true -> assert(n != 4);
od;
}
Note: the loop in the monitor process is totally unnecessary, but it makes its purpose more clear to beginners.
You can verify this program with the following one liner:
~$ spin -search -bfs buggy_01.pml
Spin finds a counter-example in zero-time:
Depth=10 States=56 Transitions=84 Memory=128.195
pan:1: assertion violated (n!=4) (at depth 19)
pan: wrote buggy_01.pml.trail
(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
+ Breadth-First Search
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 28 byte, depth reached 19, errors: 1
215 states, stored
215 nominal states (stored-atomic)
181 states, matched
396 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.011 equivalent memory usage for states (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
128.195 total actual memory usage
pan: elapsed time 0 seconds
You can actually check the execution trace that violates the assertion with:
~$ spin -t -p -g -l buggy_01.pml
The options have the following meaning:
-t: replay the .trail counter-example generated by spin -p: print all statements-g: print all global variables-l: print all local variablesThis is the output:
using statement merging
1: proc 2 (monitor:1) buggy_01.pml:27 (state 1) [(1)]
2: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
3: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))]
4: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
n = 1
5: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
q(1):countq = 1
6: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
7: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
n = 2
8: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
q(1):countq = 2
9: proc 1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))]
10: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n]
p(0):temp = 2
11: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)]
p(0):temp = 3
12: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp]
n = 3
13: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)]
p(0):countp = 1
14: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))]
15: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n]
p(0):temp = 3
16: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)]
p(0):temp = 4
17: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp]
n = 4
18: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)]
p(0):countp = 2
19: proc 0 (p:1) buggy_01.pml:9 (state 6) [((countp>=2))]
spin: buggy_01.pml:27, Error: assertion violated
spin: text of failed assertion: assert((n!=4))
20: proc 2 (monitor:1) buggy_01.pml:27 (state 2) [assert((n!=4))]
spin: trail ends after 20 steps
#processes: 3
n = 4
20: proc 2 (monitor:1) buggy_01.pml:26 (state 3)
20: proc 1 (q:1) buggy_01.pml:22 (state 9) <valid end state>
20: proc 0 (p:1) buggy_01.pml:11 (state 11) <valid end state>
3 processes created
as you can see, it reports (one) of the possible execution traces that leads to the assertion violation.
LTL.
One can think of several ltl properties that can help to verify whether n will eventually be equal to 4. One of such properties, is [] (n != 4), which reads:
starting from the initial state, in every reachable state along all outgoing paths it is always
truethatnis different from4.
The new model looks like this:
byte n;
active proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
active proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
ltl p0 { [] (n != 4) }
You verify this property pretty much in the same way as you would with the assertion. To keep this answer short, I won't copy-and-paste the whole output here, and just list the commands used:
~$ spin -search -bfs buggy_02.pml
ltl p0: [] ((n!=4))
Depth=10 States=40 Transitions=40 Memory=128.195
pan:1: assertion violated !( !((n!=4))) (at depth 15)
pan: wrote buggy_02.pml.trail
...
Full statespace search for:
never claim + (p0)
...
State-vector 28 byte, depth reached 15, errors: 1
...
~$ spin -t -p -g -l buggy_02.pml
...
If you want to guarantee that n is always eventually equal to 4, then you should look into some mutual exclusion approach to protect your critical section or, alternatively, check the documentation of d_step {}.