In the following code sample, a Sender and a Receiver exchange --for an undetermined amount of time-- a number of packets. Each message, sent by the Sender, contains either 0 or 1 and a sequence number. Whenever the Receiver a message, it checks whether it is new and in such case it sends back to the Sender an acknowledgment. Upon receiving an ACK, the Sender sends a message with new content.
In this model, whenever a message is sent, the message can either be lost, sent twice or sent normally.
mtype = { MESSAGE, ACK };
chan sender2receiver = [2] of { mtype, bit, int };
chan receiver2sender = [2] of { mtype, bit, int };
inline unreliable_send(channel, type, tag, seqno) {
bool loss = false;
bool duplicate = true;
if
:: channel!type(tag, seqno);
if
:: channel!type(tag, seqno);
:: duplicate = false;
fi
:: loss = true;
fi
}
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no) ->
receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
active proctype Receiver () {
bit in_bit, old_bit;
int seq_no;
do
:: sender2receiver?MESSAGE(in_bit, seq_no) ->
if
:: in_bit != old_bit ->
printf("received: %d\n", seq_no);
old_bit = in_bit;
:: else ->
skip;
fi;
unreliable_send(receiver2sender, ACK, in_bit, 0);
od;
}
In the previous model, the loss of a packet causes a deadlock.
To solve this issue, the lecturer discussed several approaches.
One of these approaches, is to make the Sender relentless, so that it keeps sending out a message up until when it is effectively delivered to the Receiver and its corresponding ack is correctly received by the Sender. i.e.:
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
Although in practice this approach seems to work, meaning that simulating the model no longer results in a deadlock, the lecturer warned us that it would still fail a step of formal verification because there exits at least one unlucky execution path in which at some point all messages are lost, no matter how much one insists in sending the same message again.
The lecturer invited us to think how we could use Spin to find one of the execution traces for which the proposed approach fails. Since we did not cover LTL model checking yet, the solution should be based on assert or labels.
The idea behind the protocol is that Sender and Receiver keep exchanging new messages for an infinite amount of time.
One can verify whether the proposed solution effectively respects this specification by means of progress labels.
Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
In this model, the progress-state is the one in which we establish that a message was both correctly sent and acknowledged, so our progress-state is the one immediately after we realize this fact.
Thus, we edit the Sender code as follows, and add a progress: label after in_bit == out_bit ->:
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
progress:
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
We can then formally verify the model as follows:
~$ spin -a -DNP test.pml
~$ gcc -DNP pan.c -o run
~$ ./run -l -bfs
or, alternatively, with the following one-liner:
~$ spin -search -l test.pml
As expected, spin finds a non-progress cycle:
pan:1: non-progress cycle (at depth 16)
pan: wrote test.pml.trail
(Spin Version 6.4.7 -- 19 August 2017)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 88 byte, depth reached 41, errors: 1
21 states, stored
0 states, matched
21 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector + overhead))
0.287 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
pan: elapsed time 0 seconds
We can now simulate the counter-example and show the print the offending execution trace:
~$ spin -p -l -g -t test.pml
starting claim 2
spin: couldn't find claim 2 (ignored)
using statement merging
2: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
Sender(0):loss = 0
2: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
Sender(0):duplicate = 1
Sender(0):loss = 0
4: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
6: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
8: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
10: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
12: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
Receiver(1):loss = 0
12: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
Receiver(1):duplicate = 1
Receiver(1):loss = 0
14: proc 1 (Receiver:1) test.pml:10 (state 11) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0]
16: proc 1 (Receiver:1) test.pml:12 (state 12) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
<<<<<START OF CYCLE>>>>>
18: proc 0 (Sender:1) test.pml:12 (state 4) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
20: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
22: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
24: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
26: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
26: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
28: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
30: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):loss = 0
30: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):duplicate = 1
Sender(0):loss = 0
32: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
34: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
36: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
38: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
40: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
40: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
42: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
spin: trail ends after 42 steps
#processes: 2
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
42: proc 1 (Receiver:1) test.pml:43 (state 20)
Receiver(1):loss = 1
42: proc 0 (Sender:1) test.pml:11 (state 6)
2 processes created