Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://savenkov.lvk.cs.msu.su/mc/lect04.pdf Äàòà èçìåíåíèÿ: Mon Mar 19 19:51:56 2012 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:24:12 2016 Êîäèðîâêà:

4 SPIN. Promela. ()



· SPIN , · Promela:
­ ­ ­ ­ , , , .



· ; · , :
­ ( ), ­ ( );

· , ; · .











SPIN, Promela, LTL
· SPIN ­ Simple Promela INterpreter, · Promela ­ Process Meta Language, · LTL ­ Linear Temporal Logic.

h]p://spinroot.com

, ,


SPIN, Promela, LTL
· SPIN:
­ , ­ ;

· Promela:
­ , ­ ­ , ­ ­ ,



Promela SPIN a pan.c

i

v



t





· ­ ( Promela )
­ , ­ , ;

·
­ , ­ ;



·
­ ;

·
­ , ­ ( ), , , ­ : q?m ­ q , , .


Promela
:
­ , ­ , ­ .


0

1




Hello, world!
( ) ";" ,

active proctype main() { printf("Hello, world!\n") }

­

,

>spin hello.pml Hello, world! 1 process created


Hello, world!
· Promela ­ , . · , :
init { printf("Hello, world!\n") }


· ­ :
init { run main() }



Promela
· (proctype), · ­ proctype, · :
­ ,

active
­ .

run


Promela
active [2] proctype eager() { run eager(); run eager() }

stop run eager()

run eager()

,


Promela
active [2] proctype eager() { run eager(); run eager() }
3 1 4 5 7 2 6

· ?
­ run ­ , ­ run pid , 0, , ­ , 0, ­ 255.


run
proctype irun(byte x) { printf("it is me %d, %d\n",x,_pid) } init{ pid a,b; a = run irun(1); b = run irun(2); printf("I created %d and %d", a, b) }

_pid

prin . ­ 0.
pid+1

>spin irun.pml it is me 1, 1 I created 1 and 2 it is me 2, 2 3 processes created >

1 6



· :
­ () , ­ ( ), ­ ;

· : · ­ :
­ , ­ , ­ . ­ « » ( ), ­ ;


?
· , · ­ , · , · .



bool toggle = true; short cnt; active proctype A() provided (toggle == true) { L: cnt++; printf("A: cnt=%d\n", cnt); toggle = false; goto L } active proctype B() provided (toggle == false) { L: cnt--; printf("B: cnt=%d\n", cnt); toggle = true; goto L }

./spin provided.pml | more A: cnt=1 B: cnt=0 A: cnt=1 B: cnt=0 ...

, provided clause true. true.


Promela
· , · , · ­ 6 , · :
­ : , ­ : ( ) .


Promela
· 3 :
­ (printf), ­ , ­ .
,

, , «=» , 0 ()

2 < 3 ­ , x < 27 ­ , x < 27, 3 + x ­ , x != 3.


()
· ,


· , · , · .





· ( ),

· ( ).
a1 a1 a2 b1 b2 a2

()
b1 b2

b1 a1

b1 a2

b2 a1

b2 a2



· Promela ­ (expressions) C
while (x <= y) /* wait*/; y++;

Promela
(x > y) -> y = y + 1;



· :
­ skip: , , (1), ­ true: , , (1), ­ run: 0, , _pid .



· assert ()
­ , , ­ SPIN , 0 (false), ­ ().
int n; active proctype invariant() { assert(n <= 3) }

, .



int x; proctype A() { int y = 1; skip; run B(); x = 2; (x > 2 && y == 1); printf("x %d, y %d\n", x, y) }
, x , B ­ 0


run
· run Promela ; · , Promela ; · run:
­ run B() && run A() ­ , ­ !(run B()) ­ (_nr_pr >= 255), ­ run B() && (a>b) ­ , (a <= b);

· 0 ­ , .


­
mtype = { P, C }; mtype turn = P; active proctype producer() { do :: (turn == P) -> printf("Produce\n"); turn = C od } active proctype consumer() { do :: (turn == C) -> printf("Consume\n"); turn = P od }

( 1) ­ 0, (op"on sequence)

(guard)


­
mtype = { P, C }; mtype turn = P; active proctype producer() { do :: (turn == P) -> printf("Produce\n"); turn = C od } active proctype consumer() { do :: (turn == C) -> printf("Consume\n"); turn = P od }

-uN ­

./spin -u14 pc.pml Produce Consume Produce Consume ------------depth-limit (-u14 steps) reached #processes: 2 turn = C 14: proc 1 (consumer) line 17 "pc.pml" (state 3) 14: proc 0 (producer) line 6 "pc.pml" (state 4) 2 processes created


if
active proctype consumer() { do :: (turn == C) -> printf("Consume \n"); turn = P od } } fi; goto again active proctype consumer() { again: if :: (turn == C) -> printf("Consume\n"); turn = P

· break ­ do, · :: else ­ , · ­
wait: if :: (turn == P) -> ... :: else -> goto wait fi (turn == P) ->...


(turn == P);...


:
bool busy; byte mutex; proctype P(bit i) { (!busy) -> busy = true; mutex++; printf(P%d in critical section\n",i); mutex--; busy = false } active proctype invariant() { assert(mutex <= 1) } init { atomic { run P(0); run P(1)} }

, , , : (!busy) busy = true P



> ./spin -a mutex.pml > gcc -DSAFETY -o pan pan.c > ./pan pan: assertion violated (mutex<=1) (at depth 10) pan: wrote mutex.pml.trail (Spin Version 5.1.4 -- 27 January 2008) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 24 byte, depth reached 19, errors: 1 73 states, stored 32 states, matched 105 transitions (= stored+matched) 1 atomic steps hash conflicts: 0 (resolved) 2.501 memory usage (Mbyte) pan: elapsed time 0 seconds



./spin -t -p mutex.pml Starting invariant with pid 0 Starting :init: with pid 1 Starting P with pid 2 1: proc 1 (:init:) line 14 "mutex.pml" (state 1) [(run P(0))] Starting P with pid 3 2: proc 1 (:init:) line 14 "mutex.pml" (state 2) [(run P(1))] 3: proc 3 (P) line 4 "mutex.pml" (state 1) [(!(busy))] 4: proc 2 (P) line 4 "mutex.pml" (state 1) [(!(busy))] 5: proc 3 (P) line 4 "mutex.pml" (state 2) [busy = 1] 6: proc 3 (P) line 5 "mutex.pml" (state 3) [mutex = (mutex+1)] P1 in critical section 7: proc 3 (P) line 6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)] 8: proc 2 (P) line 4 "mutex.pml" (state 2) [busy = 1] 9: proc 2 (P) line 5 "mutex.pml" (state 3) [mutex = (mutex+1)] P0 in critical section 10: proc 2 (P) line 6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)] spin: line 11 "mutex.pml", Error: assertion violated spin: text of failed assertion: assert((mutex<=1)) 11: proc 0 (invariant) line 11 "mutex.pml" (state 1) [assert((mutex<=1))] spin: trail ends after 11 steps #processes: 4 busy = 1 mutex = 2 11: proc 3 (P) line 7 "mutex.pml" (state 5) 11: proc 2 (P) line 7 "mutex.pml" (state 5) 11: proc 1 (:init:) line 15 "mutex.pml" (state 4) 11: proc 0 (invariant) line 12 "mutex.pml" (state 2) 4 processes created



( )
bit x,y; byte mutex; active proctype A() { x = 1; (y == 0) -> mutex++; printf("%d\n", _pid); mutex--; x = 0; } active proctype invariant() { assert(mutex != 2) }

/
active proctype B() { y = 1; (x == 0) -> mutex++; printf("%d\n",_pid); mutex--; y=0 }

!(y == 0) , B ­



> ./spin -a mutex2.pml > gcc -DSAFETY -o pan pan.c > ./pan pan: invalid end state (at depth 3) pan: wrote mutex2.pml.trail (Spin Version 5.1.4 -- 27 January 2008) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim assertion violations cycle checks invalid end states - (none specified) + - (disabled by -DSAFETY) +

State-vector 20 byte, depth reached 16, errors: 1 23 states, stored 3 states, matched 26 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 2.501 memory usage (Mbyte) pan: elapsed time 0 seconds



( )
bit x,y; byte mutex; active proctype A() { x = 1; (y == 0) -> mutex++; printf("%d\n", _pid); mutex--; x = 0; } active proctype invariant() { assert(mutex != 2) }

active proctype B() { y = 1; (x == 0) -> mutex++; printf("%d\n",_pid); mutex--; y=0 }

, (deadlock, invalid endstate)



> ./spin -t -p mutex2.pml Starting A with pid 0 Starting B with pid 1 Starting invariant with pid 2 1: proc 2 (invariant) line 25 "mutex2.pml" =2))] 2: proc 2 terminates 3: proc 1 (B) line 16 "mutex2.pml" (state 4: proc 0 (A) line 6 "mutex2.pml" (state spin: trail ends after 4 steps #processes: 2 x=1 y=1 mutex = 0 4: proc 1 (B) line 17 "mutex2.pml" (state 4: proc 0 (A) line 7 "mutex2.pml" (state 3 processes created >

(state 1)

[assert((mutex!

1) 1)

[y = 1] [x = 1]

2) 2)


(1981)
mtype bool byte mtype = {A_Turn, B_Turn}; x,y; mutex; turn = A_Turn;

/ ?

active proctype A() { x = true; turn = B_Turn; (!y || turn == A_Turn) -> mutex++; /*critical section*/ mutex--; x = false; } active proctype invariant() { assert(mutex <= 1) }

active proctype B() { y = true; turn = A_Turn; (!x || turn == B_Turn) -> mutex++; /*critical section*/ mutex--; y = false; }


(1981)
?
byte turn[2]; byte mutex; active [2] proctype P() { bit i = _pid; L: turn[i] = 1; turn[i] = turn[i+1]; (turn[1-i] == 0) || (turn[i] < turn[1-i]) -> mutex++; assert(mutex == 1); mutex--; turn[i] = 0; goto L; }



i = 255?

, 255 i?


Promela
· : · : · : · :
x++, x--, x = x + 1, x = run P(); (x), (1), run P(), skip, true, else, timeout; printf("x = %d\n", x);

assert(1+1 == 2), assert(false); · : q!m;

· :

q?m;


Promela

s2r sender r2s receiver

s2r!msg s2r?msg r2s!ack

r2s?ack

! ­ , ?



· (/ ), · :
­ (), ­ (, );



· :


chan x = [10] of {int, short, bit};
; 0 ( )



· :
a c «»

chan chan chan chan

a; c = [0] of {bit}; toR = [2] of {mtype, bit, chan}; line[2] = [1] of {mtype, record};





mtype
(mtype = message type)

· ( 255), · mtype: 6
mtype = {foo, bar}; mtype = {ack, msg, err, interrupt};

· mtype:
, 0 mtype a; mtype b = foo; 0



· : ch!expr1,...,expr
­ expri ; ­ , ; · : ch?const1 var1,...,constn varn ­ vari . ; ­ consti ; ­ , .
n



· :
#define ack 5 chan ch = [N] of {int, bit}; bit seqno; ch!ack,0; ch?ack,seqno : ch!ack(0); ch?ack(seqno)




· , , · , , · , .
q!m1 q!m2 q!m3
m3 m2 m1

q?m1 q?m2 q?m3



· 0: · «»; · ; · , ; · .
q!m1 q!m2 q!m3 q?m1 q?m2 q?m3

chan ch = [0] of {mtype};


:
mtype = { P, V }; chan sema = [0] of { mtype }; active proctype semaphore() { L: } active [5] proctype user() { L: /*non-critical*/ sema?P -> /*critical*/ sema!V; goto L; } sema!P -> sema?V; goto L

?V

!P



· len(q) ­ , · empty(q) ­ true, q , · full(q) ­ true, q , · nempty(q) ­ !empty(q) ( ), · nfull(q) ­ !full(q) ( ).



· q?[n,m,p]
­ , ­ true, q?m,n,p , n,m,p q;

?

· q?



­ , q?n,m,p; n,m,p , q?n,m,p, q;

· q?n(m,p)



­ (.. q?n,m,p), ­ .



· , ­ .
chan x = [3] of { chan }; active proctype A() { chan a; x?a; a!x } active proctype B() { chan b = [2] of { chan }; x!b; b?x; 0 }

, A B B x B , b !


,

:

· q!!n,m,p · q??n,m,p

­ q!n,m,p, n,m,p , n,m,p; ­ q?n,m,p, ( ).
> ./spin sorted.pml 2 5 1 process created >

init { chan q = [3] of {int}; int x; q!!5; q!!2; q?x->printf("%d\n",x); q?x->printf("%d\n",x) }


Promela
bit bool byte chan mtype pid short int unsigned 0..2n 1 0..1 false..true 0..255 1..255 1..255 1..255 215..215 1 231..231 1 bit turn = 1; bool flag = true; byte cnt; chan q; mtype msg; pid p; short s = 100; int x = 1; unsigned u : 3;

3 , 0..7

· ( , ) ; · ; · .


Promela
Promela , . , .



: byte a[27]; bit flags[4] = 1;

· , · 0.
: typedef record { short f1; byte f2 = 4; } record rr; ff.f1 = 5;
0



typedef array {byte b[4];} array a[4]; a[3].b[2] = 1;


#define ab(x,y) a[x].b[y] ab(x,y) = ab(2,3) + ab(3,2);

( #define, #if, #ifdef, #ifndef, #include)



· (int); · .
mtype = active { byte short chan mtype a x x p = = = = {foo, bar}; proctype tryme() x; y = 1024; a,b; p;

­ ­

}

a + b; 257; y; y/8



· :
­ ( ), ­ ( )
· (. ) , · . active proctype main() { int x, y; { int y, z; x++; y++; z++ }; }

, y z !

printf("y=%d, z=%d\n", y, z);



· 5 :
­ ( inline), ­ (atomic, d_step), ­ (if..fi, do..od), ­ escape ({...}unless {...}). ­ (";"), , goto,


­ cpp
· , · :
­
#define MAXQ 2 chan q=[MAXQ] of {mtype,chan};

(: spin ­DMAXQ=2 ...) #define RESET(a)\ ­ ­
#define LOSSY 1 ... #ifdef LOSSY active proctype D() #endif

atomic {a[0] = 0; a[1] = 0} #if 0 COMMENTS #endif


­ cpp
· :
­ , ­ ,

· :
­ mtype , ­ ( P),

· inline .


inline
· , · , · ­ .
#define swap(a,b) tmp = a;\ a = b;\ b = tmp #endif inline tmp a= b= } swap(a,b){ = a; b; tmp



if ::guard ::guard :: ::guard fi
1 2 n

-> stmnt -> stmnt -> stmnt

1.1 2.1 n.1

;stmnt ;stmnt ;stmnt

1.2 2.2 n.2

;stmnt ;stmnt ;stmnt

1.3 2.3 n.3

; ; ;

· if , , · , , · , if , · .


if
/* x y*/ if :: x >= y -> m = x :: x <= y -> m = y fi if :: :: :: :: fi (n%2 (n >= (n%3 else != 0) -> n = 0 0) -> n = n-2 == 0) -> n = 3 /* -> skip */

/* if :: :: :: :: fi

0..3*/ n n n n = = = = 0 1 2 3

,

LTS


else
C
if(x <= y) x = y ­ x; y++;

Promela
if ::(x <= y) -> x = y ­ x :: else fi; y++

· , else , , · .. if .



· else ­ true, , · timeout ­ true, , · _ ­ , , , · _pid ­ , · _nr_pr ­ .


do
do ::guard ::guard :: ::guard do
1 2 n

-> stmnt -> stmnt -> stmnt

1.1 2.1 n.1

;stmnt ;stmnt ;stmnt

1.2 2.2 n.2

;stmnt ;stmnt ;stmnt

1.3 2.3 n.3

; ; ;

· , · , if, · break goto.


do
· , (a==b)
do ::(a == b) -> break; ::else -> skip od
L: if ::( a== b) -> skip else goto L fi

(a == b)
·


Alterna"ng Bit Protocol
(Bartle] ., 1969)
· , ; · ; · , ; · , , ; · , , .


eval()
x ,

ch!msg(12) ch?msg(eval(x))

, x 12


Promela
mtype = {msg, ack}; chan s_r = [2] of {mtype, bit}; chan r_s = [2] of {mtype, bit}; active proctype sender() { bit seqno; do :: s_r!msg,seqno -> if :: r_s?ack,eval(seqno) -> seqno = 1 - seqno; :: r_s?ack,eval(1-seqno) fi od } active proctype receiver() { bit expect, seqno; do :: s_r?msg,seqno -> r_s!ack,seqno; if :: seqno == expect; expect = 1 - expect ::else fi od

msg(0) msg(1)

ack(0) ack(1)









>./spin -u20 -c abp.pml proc 0 = sender proc 1 = receiver q\p 0 1 1 s_r!msg,0 1 . s_r?msg,0 2 . r_s!ack,0 2 r_s?ack,0 1 s_r!msg,1 1 . s_r?msg,1 2 . r_s!ack,1 2 r_s?ack,1 ------------depth-limit (-u20 steps) reached ------------final state: ------------#processes: 2 queue 1 (s_r): queue 2 (r_s): 20: proc 1 (receiver) line 19 "abp.pml" (state 7) 20: proc 0 (sender) line 7 "abp.pml" (state 7) 2 processes created >

20



>./spin -a abp.pml > gcc -o pan pan.c >./pan (Spin Version 5.1.4 -- 27 January 2008) + Partial Order Reduction Full statespace search for: never claim assertion violations acceptance cycles invalid end states - (none specified) + - (not selected) +

?

?

State-vector 44 byte, depth reached 13, errors: 0 14 states, stored 1 states, matched 15 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 2.501 unreached in line (1 of unreached in line (1 of memory usage (Mbyte) proctype sender 15, state 10, "-end-" 10 states) proctype receiver 27, state 10, "-end-" 10 states)



( )


xspin


SPIN («» )



· :
­ pan.c:
· DCHECK ­ · DVERBOSE DSDUMP ­ · DBFS ­ ( )

­ pan:
· d ­ (state ­ )

· :
­ spin:
· o1 ­ , · o2 ­ , · o3 ­

­ pan.c:
· DNOREDUCE ­


:
· (int x = 1) ; · (run) ­ ,
­ ac"ve , ­ , end ;

· , , (LIFO); · ­ .


!
· ?