135.50K

Category:

electronics

SPIN Examples

1. SPIN Examples

Flavio Lerda
Carnegie Mellon University
SPIN Examples
SPIN Examples
Bug Catching
1
15-398

2. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
Bug Catching
2
15-398

3. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
Bug Catching
3
15-398

4. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
flag0=1
Bug Catching
4
15-398

5. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
flag0=1
turn=0
Bug Catching
5
15-398

6. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
flag0=1
turn=0
flag1 == 0 || turn == 1
Bug Catching
6
15-398

7. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
flag0=1
turn=0
flag1 == 0 || turn == 1
flag1 != 0 && turn != 1
Bug Catching
7
15-398

8. Mutual Exclusion

9. Mutual Exclusion

10. Mutual Exclusion

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion
• Peterson’s solution to the mutual exclusion
problem
flag0=1
turn=0
flag0=0
flag1 == 0 || turn == 1
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
10
15-398

11. Mutual Exclusion

12. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
proctype mutex0() {
flag0=1
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
12
15-398

13. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
proctype mutex0() {
flag0=1
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
13
15-398

14. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag0=1
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
14
15-398

15. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag[0] = 1;
flag0=1
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
15
15-398

16. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag[0] = 1;
flag0=1
turn = 0;
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
16
15-398

17. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag[0] = 1;
flag0=1
turn = 0;
(flag[1] == 0 || turn == 0);
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
17
15-398

18. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag[0] = 1;
flag0=1
turn = 0;
(flag[1] == 0 || turn == 0);
/* critical section */
turn=0
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
18
15-398

19. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
flag[0] = 1;
flag0=1
turn = 0;
(flag[1] == 0 || turn == 0);
/* critical section */
turn=0
flag[0] = 0;
flag0=0
flag1 == 0 || turn == 1
}
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
19
15-398

20. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn;
bool flag[2];
proctype mutex0() {
again:
flag[0] = 1;
flag0=1
turn = 0;
(flag[1] == 0 || turn == 0);
/* critical section */
turn=0
flag[0] = 0;
goto again;
}
flag0=0
flag1 == 0 || turn == 1
flag1 != 0 && turn != 1
Critical
Section
Bug Catching
20
15-398

21. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn, flag[2];
Active process:
automatically creates instances of processes
active [2] proctype user()
{
assert(_pid == 0 || __pid == 1);
_pid:
Identifier of the process
again:
flag[_pid] = 1;
assert:
turn = _pid;
Checks that there are only
(flag[1 - _pid] == 0 || turn == 1 - _pid);
at most two instances with
identifiers 0 and 1
/* critical section */
flag[_pid] = 0;
goto again;
}
Bug Catching
21
15-398

22. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn, flag[2];
byte ncrit;
ncrit:
Counts the number of
Process in the critical section
active [2] proctype user()
{
assert(_pid == 0 || __pid == 1);
again:
flag[_pid] = 1;
turn = _pid;
(flag[1 - _pid] == 0 || turn == 1 - _pid);
ncrit++;
assert(ncrit == 1); /* critical section */
ncrit--;
assert:
Checks that there are always
at most one process in the
critical section
flag[_pid] = 0;
goto again;
}
Bug Catching
22
15-398

23. Mutual Exclusion in SPIN

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Mutual Exclusion in SPIN
bool turn, flag[2];
LTL Properties:
bool critical[2];
[] (critial[0] || critical[1])
active [2] proctype user()
{
[] <> (critical[0])
[] <> (critical[1])
assert(_pid == 0 || __pid == 1);
again:
flag[_pid] = 1;
turn = _pid;
(flag[1 - _pid] == 0 || turn == 1 - _pid);
critical[_pid] = 1;
/* critical section */
critical[_pid] = 0;
flag[_pid] = 0;
goto again;
}
Bug Catching
23
[] (critical[0] ->
(critial[0] U
(!critical[0] &&
((!critical[0] &&
!critical[1]) U critical[1]))))
[] (critical[1] ->
(critial[1] U
(!critical[1] &&
((!critical[1] &&
!critical[0]) U critical[0]))))
15-398

24. Alternating Bit Protocol

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Alternating Bit Protocol
• Two processes want to communicate
• They want acknowledge of received
messages
• Sending window of one message
• Each message is identified by one bit
• Alternating values of the identifier
Bug Catching
24
15-398

25. Alternating Bit Protocol

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Alternating Bit Protocol
Sender
Receiver
msg0
ack0
msg1
ack1
msg0
ack0
msg1
Bug Catching
25
15-398

26. Alternating Bit Protocol

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Alternating Bit Protocol
Sender
Receiver
msg0
ack1
msg0
ack0
Bug Catching
26
15-398

27. Alternating Bit Protocol

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Alternating Bit Protocol
Sender
Receiver
msg0
msg0
ack0
msg1
ack1
Bug Catching
27
15-398

28. Sender Process

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Sender Process
active proctype Sender()
{
do
::
if
:: receiver?msg0;
:: skip
fi;
do
:: sender?ack0 -> break
:: sender?ack1
:: timeout ->
if
:: receiver!msg0;
:: skip
fi;
od;
::
if
:: receiver?msg1;
:: skip
fi;
do
:: sender?ack1 -> break
:: sender?ack0
:: timeout ->
if
:: receiver!msg1;
:: skip
fi;
od;
od;
}
Bug Catching
28
15-398

29. Receiver Process

Flavio Lerda
Carnegie Mellon University
SPIN Examples
Receiver Process
active proctype Receiver()
{
do
::
do
:: receiver?msg0 ->
sender!ack0; break;
:: receiver?msg1 ->
server!ack1
od
mtype = { msg0, msg1, ack0, ack1 }
chan sender = [1] of { mtype };
chan receiver = [1] of { mtype };
do
:: receiver?msg1 ->
sender!ack1; break;
:: receiver?msg0 ->
server!ack0
od
od
}
Bug Catching
29
15-398

English Русский Rules