Spin Model Checker and Promela Architecture
T
T
h
h
e
e
S
S
p
p
i
i
n
n
M
M
o
o
d
d
e
e
l
l
C
C
h
h
e
e
c
c
k
k
e
e
r
r
:
:
P
P
a
a
r
r
t
t
I
I
Moonzoo Kim
KAIST
Hierarchy of SW Coverage Criteria
2
/60
Complete Value
Coverage
CVC
(SW) Model checking
Concolic testing
M
o
d
e
l
C
h
e
c
k
e
r
A
n
a
l
y
z
e
s
A
l
l
P
o
s
s
i
b
l
e
S
c
h
e
d
u
l
i
n
g
active type A() {byte x;
again:
x++;
goto again;
}
3
x:0
x:1
x:2
x:255
active type A() {byte x;
again:
x++;
goto again;
}
active type B() {byte y;
again:
y++;
goto again;
}
x
:
0
,
y
:
0
x
:
1
,
y
:
0
x
:
2
,
y
:
0
x
:
2
5
5
,
y
:
0
x
:
0
,
y
:
1
x
:
1
,
y
:
1
x
:
0
,
y
:
2
5
5
x
:
1
,
y
:
2
5
5
x:255,y:255
x
:
2
,
y
:
1
x
:
2
,
y
:
2
5
5
O
v
e
r
v
i
e
w
o
f
t
h
e
S
p
i
n
A
r
c
h
i
t
e
c
t
u
r
e
•
A few characteristics of Spin
•
Promela allows a finite state model only
•
Asynchronous execution
•
Interleaving semantics for concurrency
•
2-way process communication
•
Non-determinism
•
Promela provides (comparatively) rich set of constructs such as
variables and message passing, dynamic creation of processes,
etc
4
System Spec.
In Promela
Req. Spec.
In LTL
Spin
Model
Checker
pan.c
C compiler
a.out
OK
Counter
Example (s)
T
c
l
G
U
I
o
f
S
P
I
N
(
i
s
p
i
n
.
t
c
l
)
:
E
d
i
t
W
i
n
d
o
w
5
T
c
l
G
U
I
o
f
S
P
I
N
(
i
s
p
i
n
.
t
c
l
)
:
V
e
r
i
f
i
c
a
t
i
o
n
W
i
n
d
o
w
6
T
c
l
G
U
I
o
f
S
P
I
N
(
i
s
p
i
n
.
t
c
l
)
:
S
i
m
u
l
a
t
i
o
n
W
i
n
d
o
w
7
O
v
e
r
v
i
e
w
o
f
t
h
e
P
r
o
m
e
l
a
byte x;
chan ch1= [3] of {byte};active[2]
proctype A() {byte z;
printf(“x=%d\n”,x);
z=x+1;
ch1!z
}
proctype B(byte y) {byte z;
ch1?z;
}
Init {run B(2);
}
8
•
Similar to C syntax but
simplified
•
No pointer
•
No real datatype such
as float or real
•
No functions
•
Processes are
communicating with
each other using
•
Global variables
•
Message channels
•
Process can be
dynamically created
•
Scheduler executes
one process at a time
using interleaving
semantics
Global variables
(including channels)
Process (thread)
definition and
creation
Another
process
definition
System
initialization
P
r
o
c
e
s
s
C
r
e
a
t
i
o
n
E
x
a
m
p
l
e
•
run() operator creates a
process and returns a
newly created process
ID
•
There are 6 possible
outcomes due to
non-
deterministic
scheduling
•
A0.A1.B, A0.B.A1
•
A1.A0.B, A1.B.A0
•
B.A0.A1, B.A1.A0
•
In other words, process
creation may
not
immediately start
process execution
9
active[2]
proctype A() {byte x;
printf(“A%d is starting\n”);
}
proctype B() {printf(“B is starting\n”);
}
Init {run B();
}
V
a
r
i
a
b
l
e
s
a
n
d
T
y
p
e
s
•
Basic types
•
bit
•
bool
•
Byte (8 bit unsigned integer)
•
short (16 bits signed integer)
•
Int (32 bits signed integer)
•
Arrays
•
bool x[10];
•
Records
•
typedef R { bit x; byte y;}•
Default initial value of variables is 0
•
Most arithmetic (e.g.,+,-), relational (e.g. >,==) and
logical operators of C are supported
•
bitshift operators are supported too.
10
F
i
n
i
t
e
S
t
a
t
e
M
o
d
e
l
•
Promela spec generates only a finite state
model because
•
Max # of active process <= 255
•
Each process has only finite length of codes
•
Each variable is of finite datatype
•
All message channels have bounded
capability <= 255
11
B
a
s
i
c
S
t
a
t
e
m
e
n
t
s
•
Each Promela statement is either
•
executable:
•
Blocked
•
There are six types of statement
•
Assignment: always executable
•
Ex.
x=3+x
,
x=run A()
•
Print: always executable
•
Ex.
printf(“Process %d is created.\n”,_pid);
•
Assertion: always executable
•
Ex.
assert( x + y == z)
•
Expression: depends on its value
•
Ex.
x+3>0
,
0
,
1
,
2
•
Ex.
skip, true
•
Send: depends on buffer status
•
Ex.
ch1!m
is executable only if
ch1
is not full
•
Receive: depends on buffer status
•
Ex.
ch1?m
is executable only if
ch1
is not empty
12
E
x
p
r
e
s
s
i
o
n
S
t
a
t
e
m
e
n
t
s
•
An expression is also a statement
•
It is executable if it evaluates to non-zero
•
1 : always executable
•
1<2:always executable
•
x<0: executable only when x < 0
•
x-1:executable only when x !=0
•
If an expression statement in blocked, it
remains blocked until other process
changes the condition
•
an expression e is equivalent to while(!e); in C
13
a
s
s
e
r
t
S
t
a
t
e
m
e
n
t
•
assert(expr
)
•
assert is always executable
•
If expr is 0, SPIN detects this violation
•
assert is most frequently used checking
method, especially as a form of
invariance
•
ex. active proctype inv() { assert( x== 0);}–
Note that inv() is equivalent to [] (x==0) in LTL
with thanks to interleaving semantics
14
P
r
o
g
r
a
m
E
x
e
c
u
t
i
o
n
C
o
n
t
r
o
l
•
Promela provides low-level control mechanism, i.e., goto
and label as well as if and do
•
Note that
non-deterministic
selection is supported
•
else is predefined variable which becomes true if all
guards are false; false otherwise
15
proctype A() {byte x;
starting:
x= x+1;
goto
starting;
}
proctype A() {byte x;
if
::x<=0 -> x=x+1
::x==0 -> x=1
fi
}
proctype A() {byte x;
do
:: x<=0 ->x=x+1;
:: x==0 ->x=1;
::
else
->
break
od
}
int i;
for
(i : 1 .. 10) { printf("i =%d\n",i) }
C
r
i
t
i
c
a
l
S
e
c
t
i
o
n
E
x
a
m
p
l
e
16
bool lock;
byte cnt;
active[2] proctype P() {!lock -> lock=true;
cnt=cnt+1;
printf("%d is in the crt sec!\n",_pid);cnt=cnt-1;
lock=false;
}
active proctype Invariant() {assert(cnt <= 1);
}
[root@moonzoo spin_test]# ls
crit.pml
[root@moonzoo spin_test]# spin -a crit.pml
[root@moonzoo spin_test]# ls
crit.pml
pan.b pan.c pan.h pan.m pan.t
[root@moonzoo spin_test]# gcc pan.c
[root@moonzoo spin_test]# a.out
p
a
n
:
a
s
s
e
r
t
i
o
n
v
i
o
l
a
t
e
d
(
c
n
t
<
=
1
)
(
a
t
d
e
p
t
h
8
)
p
a
n
:
w
r
o
t
e
c
r
i
t
.
p
m
l
.
t
r
a
i
l
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 36 byte, depth reached 16, errors:
1
119 states, stored
47 states, matched
166 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
4.879 memory usage (Mbyte)
[root@moonzoo spin_test]# ls
a.out crit.pml
crit.pml.trail
pan.b pan.c pan.h
pan.m pan.t
C
r
i
t
i
c
a
l
S
e
c
t
i
o
n
E
x
a
m
p
l
e
(
c
o
n
t
.
)
17
[root@moonzoo spin_test]# spin -t -p crit.pml
Starting P with pid 0
Starting P with pid 1
Starting Invariant with pid 2
1: proc 1 (P) line 5 "crit.pml" (state 1) [(!(lock))]
2: proc 0 (P) line 5 "crit.pml" (state 1) [(!(lock))]
3: proc 1 (P) line 5 "crit.pml" (state 2) [lock = 1]
4: proc 1 (P) line 6 "crit.pml" (state 3) [cnt = (cnt+1)]
1 is in the crt sec!
5: proc 1 (P) line 7 "crit.pml" (state 4) [printf('%d is in the crt sec!\\n',_pid)]6: proc 0 (P) line 5 "crit.pml" (state 2) [lock = 1]
7: proc 0 (P) line 6 "crit.pml" (state 3) [cnt = (cnt+1)]
0 is in the crt sec!
8: proc 0 (P) line 7 "crit.pml" (state 4) [printf('%d is in the crt sec!\\n',_pid)]s
p
i
n
:
l
i
n
e
1
3
"
c
r
i
t
.
p
m
l
"
,
E
r
r
o
r
:
a
s
s
e
r
t
i
o
n
v
i
o
l
a
t
e
d
spin: text of failed assertion: assert((cnt<=1))
9: proc 2 (Invariant) line 13 "crit.pml" (state 1) [assert((cnt<=1))]
spin: trail ends after 9 steps
#processes: 3
lock = 1
cnt = 2
9: proc 2 (Invariant) line 14 "crit.pml" (state 2) <valid end state>
9: proc 1 (P) line 8 "crit.pml" (state 5)
9: proc 0 (P) line 8 "crit.pml" (state 5)
3 processes created
R
e
v
i
s
e
d
C
r
i
t
i
c
a
l
S
e
c
t
i
o
n
E
x
a
m
p
l
e
18
bool lock;
byte cnt;
active[2] proctype P() {a
t
o
m
i
c
{!
l
o
c
k
-
>
l
o
c
k
=
t
r
u
e
;
}
cnt=cnt+1;
printf("%d is in the crt sec!\n",_pid);cnt=cnt-1;
lock=false;
}
active proctype Invariant() {assert(cnt <= 1);
}
[root@moonzoo revised]# a.out
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 36 byte, depth reached 14, errors: 0
62 states, stored
17 states, matched
79 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
4.879 memory usage (Mbyte)
D
e
a
d
l
o
c
k
e
d
C
r
i
t
i
c
a
l
S
e
c
t
i
o
n
E
x
a
m
p
l
e
19
bool lock;
byte cnt;
active[2] proctype P() {atomic{ !lock -> lock
==
true
;}
cnt=cnt+1;
printf("%d is in the crt sec!\n",_pid);cnt=cnt-1;
lock=false;
}
active proctype Invariant() {assert(cnt <= 1);
}
[[root@moonzoo deadlocked]# a.out
p
a
n
:
i
n
v
a
l
i
d
e
n
d
s
t
a
t
e
(
a
t
d
e
p
t
h
3
)
(Spin Version 4.2.7 -- 23 June 2006)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
i
n
v
a
l
i
d
e
n
d
s
t
a
t
e
s
+
State-vector 36 byte, depth reached 4, errors:
1
5 states, stored
0 states, matched
5 transitions (= stored+matched)
2 atomic steps
hash conflicts: 0 (resolved)
4.879 memory usage (Mbyte)
D
e
a
d
l
o
c
k
e
d
C
r
i
t
i
c
a
l
S
e
c
t
i
o
n
E
x
a
m
p
l
e
(
c
o
n
t
.
)
20
[root@moonzoo deadlocked]# spin -t -p deadlocked_crit.pml
Starting P with pid 0
Starting P with pid 1
Starting Invariant with pid 2
1: proc 2 (Invariant) line 13 "deadlocked_crit.pml" (state 1)
[assert((cnt<=1))]
2: proc 2 terminates
3: proc 1 (P) line 5 "deadlocked_crit.pml" (state 1) [(!(lock))]
4: proc 0 (P) line 5 "deadlocked_crit.pml" (state 1) [(!(lock))]
s
p
i
n
:
t
r
a
i
l
e
n
d
s
a
f
t
e
r
4
s
t
e
p
s
#processes: 2
lock = 0
cnt = 0
4: proc 1 (P) line 5 "deadlocked_crit.pml" (state 2)
4: proc 0 (P) line 5 "deadlocked_crit.pml" (state 2)
3 processes created
C
o
m
m
u
n
i
c
a
t
i
o
n
U
s
i
n
g
M
e
s
s
a
g
e
C
h
a
n
n
e
l
s
•
Spin provides communications through
various types of message channels
•
Buffered or non-buffered (rendezvous comm.)
•
Various message types
•
Various message handling operators
•
Syntax
•
chan ch1 = [2] of { bit, byte};•
ch1!0,10;ch1!1,20
•
ch1?b,bt;ch1?1,bt
•
chan ch2= [0] of {bit, byte}21
Sender (1,20) (0,10) Receiver
O
p
e
r
a
t
i
o
n
s
o
n
C
h
a
n
n
e
l
s
•
B
a
s
i
c
c
h
a
n
n
e
l
i
n
q
u
i
r
y
•
len(ch)
•
empty(ch)
•
full(ch)
•
nempty(ch)
•
nfull(ch)
•
A
d
d
i
t
i
o
n
a
l
m
e
s
s
a
g
e
p
a
s
s
i
n
g
o
p
e
r
a
t
o
r
s
•
ch?[x,y]:
polling only
•
ch?<x,y>:
copy a message without removing it
•
ch!!x,y:
sorted sending (increasing order)
•
ch??5,y:
random receiving
•
ch?x(y) == ch?x,y
(for user’s understandability)
•
Be careful to use these operators inside of expressions
•
They have side-effects, which spin may not allow
22
F
a
u
l
t
y
D
a
t
a
T
r
a
n
s
f
e
r
P
r
o
t
o
c
o
l
(
p
g
2
7
,
d
a
t
a
s
w
i
t
c
h
m
o
d
e
l
p
r
o
p
o
s
e
d
a
t
1
9
8
1
a
t
B
e
l
l
l
a
b
s
)
23
m
t
y
p
e
=
{i
n
i
,
a
c
k
,
d
r
e
q
,
d
a
t
a
,
s
h
u
t
u
p
,
q
u
i
e
t
,
d
e
a
d
}
chan M = [1] of {mtype};chan W = [1] of {mtype};active proctype Mproc()
{W!ini;
/* connection */
M?ack;
/* handshake */
t
i
m
e
o
u
t
-
>
/
*
w
a
i
t
*
/
if
/* two options: */
:: W!shutup; /* start shutdown */
:: W!dreq; /* or request data */
do
:: M?data -> W!data
:: M?data-> W!shutup;
break
od
fi;
M?shutup;
W!quiet;
M?dead;
}
active proctype Wproc() {W?ini;
/* wait for ini*/
M!ack;
/* acknowledge */
do
/* 3 options: */
:: W?dreq->
/* data requested */
M!data
/* send data */
:: W?data->
/* receive data */
skip
/* no response */
:: W?shutup->
M!shutup; /* start shutdown*/
break
od;
W?quiet;
M!dead;
}
Mproc
Wproc
Channel W
Channel M
T
h
e
S
i
e
v
e
o
f
E
r
a
t
o
s
t
h
e
n
e
s
(
p
g
3
2
6
)
24
/*
The Sieve of Eratosthenes (c. 276-196 BC)
Prints all prime numbers up to MAX
*/
#define MAX 25
mtype = { number, eof };chan root = [0] of { mtype, int };init
{ int n = 2;run sieve(root, n);
do
:: (n < MAX) -> n++; root!number(n)
:: (n >= MAX) -> root!eof(0); break
od
}
proctype sieve(chan c; int prime)
{ chan child = [0] of { mtype, int };bool haschild; int n;
printf("MSC: %d is prime\n", prime);end: do
:: c?number(n) ->
if
:: (n%prime) == 0 -> printf("MSC: %d= %d*%d\n", n, prime, n/prime)
:: else ->
if
:: !haschild -> /* new prime */
haschild = true;
r
u
n
s
i
e
v
e
(
c
h
i
l
d
,
n
)
;
:: else ->
child!number(n)
fi;
fi
:: c?eof(0) -> break
od;
if
:: haschild -> child!eof(0)
:
:
e
l
s
e
fi
}
S
i
m
u
l
a
t
i
o
n
R
u
n
[moonzoo@verifier spin]$ spin sieve-of-eratosthenes.pml
MSC: 2 is prime
MSC: 3 is prime
MSC: 4 = 2*2
MSC: 5 is prime
MSC: 6 = 2*3
MSC: 8 = 2*4
MSC: 7 is prime
MSC: 9 = 3*3
MSC: 10 = 2*5
MSC: 12 = 2*6
MSC: 14 = 2*7
MSC: 11 is prime
MSC: 15 = 3*5
MSC: 13 is prime
MSC: 16 = 2*8
MSC: 18 = 2*9
MSC: 20 = 2*10
25
Delve into the details of Spin Model Checker and Promela system architecture, including SW coverage criteria, scheduling analysis, Spin architecture overview, and components like Tcl GUI. Discover the characteristics of Spin Promela, asynchronous execution, non-determinism, process communication, and more. Explore the unique features of Promela syntax, process interaction, process creation, and system initialization in a simplified C-like environment.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
The Spin Model Checker : Part I Moonzoo Kim KAIST
Hierarchy of SW Coverage Criteria Complete Value Coverage CVC (SW) Model checking Complete Path Coverage CPC Concolic testing Prime Path Coverage PPC All-DU-Paths Coverage ADUP Edge-Pair Coverage EPC All-uses Coverage AUC Complete Round Trip Coverage CRTC Edge Coverage EC All-defs Coverage ADC Simple Round Trip Coverage SRTC Node Coverage NC 2/60
Model Checker Analyzes All Possible Scheduling active type A() { byte x; again: x++; goto again; } x:0 x:1 x:2 x:255 active type A() { byte x; again: x++; goto again; } x:0,y:1 x:0,y:0 x:0,y:255 x:1,y:255 x:1,y:1 x:1,y:0 x:2,y:255 x:2,y:1 active type B() { byte y; again: y++; goto again; } x:2,y:0 x:255,y:255 x:255,y:0 3
Overview of the Spin Architecture System Spec. In Promela Spin Model Checker a.out C compiler pan.c Req. Spec. In LTL Counter Example (s) OK A few characteristics of Spin Promela allows a finite state model only Asynchronous execution Interleaving semantics for concurrency 2-way process communication Non-determinism Promela provides (comparatively) rich set of constructs such as variables and message passing, dynamic creation of processes, etc 4
Overview of the Promela Similar to C syntax but simplified No pointer No real datatype such as float or real No functions Processes are communicating with each other using Global variables Message channels Process can be dynamically created Scheduler executes one process at a time using interleaving semantics Global variables (including channels) byte x; chan ch1= [3] of {byte}; active[2] proctype A() { byte z; printf( x=%d\n ,x); z=x+1; ch1!z } Process (thread) definition and creation proctype B(byte y) { byte z; ch1?z; } Another process definition System initialization Init { } run B(2); 8
Process Creation Example active[2] proctype A() { byte x; printf( A%d is starting\n ); } run() operator creates a process and returns a newly created process ID There are 6 possible outcomes due to non- deterministic scheduling A0.A1.B, A0.B.A1 A1.A0.B, A1.B.A0 B.A0.A1, B.A1.A0 In other words, process creation may not immediately start process execution proctype B() { printf( B is starting\n ); } Init { run B(); } 9
Variables and Types Basic types bit bool Byte (8 bit unsigned integer) short (16 bits signed integer) Int (32 bits signed integer) Arrays bool x[10]; Records typedef R { bit x; byte y;} Default initial value of variables is 0 Most arithmetic (e.g.,+,-), relational (e.g. >,==) and logical operators of C are supported bitshift operators are supported too. 10
Finite State Model Promela spec generates only a finite state model because Max # of active process <= 255 Each process has only finite length of codes Each variable is of finite datatype All message channels have bounded capability <= 255 11
Basic Statements Each Promela statement is either executable: Blocked There are six types of statement Assignment: always executable Ex. x=3+x, x=run A() Print: always executable Ex. printf( Process %d is created.\n ,_pid); Assertion: always executable Ex. assert( x + y == z) Expression: depends on its value Ex. x+3>0, 0, 1, 2 Ex. skip, true Send: depends on buffer status Ex. ch1!m is executable only if ch1 is not full Receive: depends on buffer status Ex. ch1?m is executable only if ch1 is not empty 12
Expression Statements An expression is also a statement It is executable if it evaluates to non-zero 1 : always executable 1<2:always executable x<0: executable only when x < 0 x-1:executable only when x !=0 If an expression statement in blocked, it remains blocked until other process changes the condition an expression e is equivalent to while(!e); in C 13
assert Statement assert(expr) assert is always executable If expr is 0, SPIN detects this violation assert is most frequently used checking method, especially as a form of invariance ex. active proctype inv() { assert( x== 0);} Note that inv() is equivalent to [] (x==0) in LTL with thanks to interleaving semantics 14
Program Execution Control Promela provides low-level control mechanism, i.e., goto and label as well as if and do Note that non-deterministic selection is supported else is predefined variable which becomes true if all guards are false; false otherwise proctype A() { byte x; starting: x= x+1; goto starting; } proctype A() { byte x; if ::x<=0 -> x=x+1 ::x==0 -> x=1 fi } proctype A() { byte x; do :: x<=0 ->x=x+1; :: x==0 ->x=1; :: else -> break od } int i; for (i : 1 .. 10) { printf("i =%d\n",i) } 15
Critical Section Example [root@moonzoo spin_test]# ls crit.pml [root@moonzoo spin_test]# spin -a crit.pml [root@moonzoo spin_test]# ls crit.pml pan.b pan.c pan.h pan.m pan.t [root@moonzoo spin_test]# gcc pan.c [root@moonzoo spin_test]# a.out pan: assertion violated (cnt<=1) (at depth 8) pan: wrote crit.pml.trail Full statespace search for: never claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid end states + State-vector 36 byte, depth reached 16, errors: 1 119 states, stored 47 states, matched 166 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 4.879 memory usage (Mbyte) [root@moonzoo spin_test]# ls a.out crit.pml crit.pml.trail pan.b pan.c pan.h pan.m pan.t bool lock; byte cnt; active[2] proctype P() { !lock -> lock=true; cnt=cnt+1; printf("%d is in the crt sec!\n",_pid); cnt=cnt-1; lock=false; } active proctype Invariant() { assert(cnt <= 1); } 16
Critical Section Example (cont.) [root@moonzoo spin_test]# spin -t -p crit.pml Starting P with pid 0 Starting P with pid 1 Starting Invariant with pid 2 1: proc 1 (P) line 5 "crit.pml" (state 1) [(!(lock))] 2: proc 0 (P) line 5 "crit.pml" (state 1) [(!(lock))] 3: proc 1 (P) line 5 "crit.pml" (state 2) [lock = 1] 4: proc 1 (P) line 6 "crit.pml" (state 3) [cnt = (cnt+1)] 1 is in the crt sec! 5: proc 1 (P) line 7 "crit.pml" (state 4) [printf('%d is in the crt sec!\\n',_pid)] 6: proc 0 (P) line 5 "crit.pml" (state 2) [lock = 1] 7: proc 0 (P) line 6 "crit.pml" (state 3) [cnt = (cnt+1)] 0 is in the crt sec! 8: proc 0 (P) line 7 "crit.pml" (state 4) [printf('%d is in the crt sec!\\n',_pid)] spin: line 13 "crit.pml", Error: assertion violated spin: text of failed assertion: assert((cnt<=1)) 9: proc 2 (Invariant) line 13 "crit.pml" (state 1) [assert((cnt<=1))] spin: trail ends after 9 steps #processes: 3 lock = 1 cnt = 2 9: proc 2 (Invariant) line 14 "crit.pml" (state 2) <valid end state> 9: proc 1 (P) line 8 "crit.pml" (state 5) 9: proc 0 (P) line 8 "crit.pml" (state 5) 3 processes created 17
Revised Critical Section Example bool lock; byte cnt; [root@moonzoo revised]# a.out Full statespace search for: never claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid end states + active[2] proctype P() { atomic{ !lock -> lock=true;} cnt=cnt+1; printf("%d is in the crt sec!\n",_pid); cnt=cnt-1; lock=false; } State-vector 36 byte, depth reached 14, errors: 0 62 states, stored 17 states, matched 79 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) active proctype Invariant() { assert(cnt <= 1); } 4.879 memory usage (Mbyte) 18
Deadlocked Critical Section Example [[root@moonzoo deadlocked]# a.out pan: invalid end state (at depth 3) bool lock; byte cnt; (Spin Version 4.2.7 -- 23 June 2006) Warning: Search not completed + Partial Order Reduction active[2] proctype P() { atomic{ !lock -> lock==true;} cnt=cnt+1; printf("%d is in the crt sec!\n",_pid); cnt=cnt-1; lock=false; } Full statespace search for: never claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid end states + State-vector 36 byte, depth reached 4, errors: 1 5 states, stored 0 states, matched 5 transitions (= stored+matched) 2 atomic steps hash conflicts: 0 (resolved) active proctype Invariant() { assert(cnt <= 1); } 4.879 memory usage (Mbyte) 19
Deadlocked Critical Section Example (cont.) [root@moonzoo deadlocked]# spin -t -p deadlocked_crit.pml Starting P with pid 0 Starting P with pid 1 Starting Invariant with pid 2 1: proc 2 (Invariant) line 13 "deadlocked_crit.pml" (state 1) [assert((cnt<=1))] 2: proc 2 terminates 3: proc 1 (P) line 5 "deadlocked_crit.pml" (state 1) [(!(lock))] 4: proc 0 (P) line 5 "deadlocked_crit.pml" (state 1) [(!(lock))] spin: trail ends after 4 steps #processes: 2 lock = 0 cnt = 0 4: proc 1 (P) line 5 "deadlocked_crit.pml" (state 2) 4: proc 0 (P) line 5 "deadlocked_crit.pml" (state 2) 3 processes created 20
Communication Using Message Channels Spin provides communications through various types of message channels Buffered or non-buffered (rendezvous comm.) Various message types Various message handling operators Syntax chan ch1 = [2] of { bit, byte}; ch1!0,10;ch1!1,20 ch1?b,bt;ch1?1,bt chan ch2= [0] of {bit, byte} Sender (1,20) (0,10) Receiver 21
Operations on Channels Basic channel inquiry len(ch) empty(ch) full(ch) nempty(ch) nfull(ch) Additional message passing operators ch?[x,y]: polling only ch?<x,y>: copy a message without removing it ch!!x,y: sorted sending (increasing order) ch??5,y: random receiving ch?x(y) == ch?x,y (for user s understandability) Be careful to use these operators inside of expressions They have side-effects, which spin may not allow 22
Faulty Data Transfer Protocol (pg 27, data switch model proposed at 1981 at Bell labs) mtype={ini,ack, dreq,data, shutup,quiet, dead} chan M = [1] of {mtype}; chan W = [1] of {mtype}; active proctype Wproc() { W?ini; M!ack; /* wait for ini*/ /* acknowledge */ active proctype Mproc() { W!ini; M?ack; /* handshake */ /* connection */ } do :: W?dreq-> :: W?data-> :: W?shutup-> od; /* 3 options: */ /* data requested */ M!data /* send data */ /* receive data */ skip /* no response */ } timeout -> /* wait */ if /* two options: */ :: W!shutup; /* start shutdown */ :: W!dreq; /* or request data */ do :: M?data -> W!data :: M?data-> W!shutup; break od fi; M?shutup; W!quiet; M?dead; Mproc M!shutup; /* start shutdown*/ break W?quiet; M!dead; Channel W Wproc Channel M 23
The Sieve of Eratosthenes (pg 326) proctype sieve(chan c; int prime) { chan child = [0] of { mtype, int }; bool haschild; int n; printf("MSC: %d is prime\n", prime); end: do :: c?number(n) -> if :: (n%prime) == 0 -> printf("MSC: %d = %d*%d\n", n, prime, n/prime) :: else -> if :: !haschild -> /* new prime */ haschild = true; run sieve(child, n); :: else -> child!number(n) fi; fi :: c?eof(0) -> break od; if :: haschild -> child!eof(0) :: else fi } /* The Sieve of Eratosthenes (c. 276-196 BC) Prints all prime numbers up to MAX */ #define MAX 25 mtype = { number, eof }; chan root = [0] of { mtype, int }; init { int n = 2; run sieve(root, n); do :: (n < MAX) -> n++; root!number(n) :: (n >= MAX) -> root!eof(0); break od } 24
Simulation Run [moonzoo@verifier spin]$ spin sieve-of-eratosthenes.pml MSC: 2 is prime MSC: 3 is prime MSC: 4 = 2*2 MSC: 5 is prime MSC: 6 = 2*3 MSC: 8 = 2*4 MSC: 7 is prime MSC: 9 = 3*3 MSC: 10 = 2*5 MSC: 12 = 2*6 MSC: 14 = 2*7 MSC: 11 is prime MSC: 15 = 3*5 MSC: 13 is prime MSC: 16 = 2*8 MSC: 18 = 2*9 MSC: 20 = 2*10 2 3 5 7 11 13 25
