A lock admits one process at a time
A lock makes sure only one process at a time is in the part of a program that changes shared data. That promise is called mutual exclusion.
A lock that looks right can still fail in one order of steps. SPIN checks every order, so you find out before the program runs.
By the end of this lesson
Note
I can write a lock and have SPIN report no errors.
Key words
| Word | What it means |
|---|---|
| Critical section | the steps that must not run in two processes at once |
| Mutual exclusion | at most one process in the critical section |
| Lock | a shared value that decides who may enter |
| Deadlock | every process waits for another, so none can move |
| Atomic step | a step that nothing can interrupt |
| Flag | a shared true or false value a process sets to show it wants in |
The cells students fill in are left blank in this preview.
Checking then setting is not a lock
The obvious lock is: look at the other process's flag, and if it is down, put your own flag up. Each process does this as two separate steps.
SPIN can switch between those two steps. Both processes see the other flag down, both put theirs up, and both walk in.
Write the check-then-set lock
printf '%s\n' 'bool flag[2]' 'byte inside' 'active [2] proctype p() {' ' (flag[1 - _pid] == false) -> flag[_pid] = true -> inside++ -> assert(inside == 1) -> inside-- -> flag[_pid] = false' '}' > checkfirst.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check every order
spinrun checkfirst.pml | grep -E 'pan:1|errors'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Worked example: the file line by line
| Part | What it says |
|---|---|
| bool flag[2] | one flag for each of the two processes |
| _pid | the number of this process, 0 or 1 |
| (flag[1 - _pid] == false) | wait until the other flag is down |
| flag[_pid] = true | put my flag up |
| inside++ -> assert(inside == 1) | enter, and demand that I am alone |
The cells students fill in are left blank in this preview.
Peterson's lock uses two flags and a turn
Peterson's algorithm is a classic lock for two processes. First put your flag up. Then set turn to the other process: you politely give them the next go. Then wait until the other flag is down or the turn is yours.
Putting the flag up first closes the gap. Setting the turn breaks a tie when both want in.
Write Peterson's lock
printf '%s\n' 'bool flag[2]' 'byte turn' 'byte inside' 'active [2] proctype p() {' ' flag[_pid] = true -> turn = 1 - _pid -> (flag[1 - _pid] == false || turn == _pid) -> inside++ -> assert(inside == 1) -> inside-- -> flag[_pid] = false' '}' > peterson.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check Peterson's lock
spinrun peterson.pml | grep -E 'pan:1|errors'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A safe lock can still get stuck
Mutual exclusion is a promise about what never happens. A lock can keep it and still be useless, if both processes wait for ever.
Put the flag up, then wait for the other flag to go down, and leave out the turn. Both flags go up, and both wait for the other. SPIN calls the stuck state an invalid end state.
Write a lock without a turn
printf '%s\n' 'bool flag[2]' 'byte inside' 'active [2] proctype p() {' ' flag[_pid] = true -> (flag[1 - _pid] == false) -> inside++ -> assert(inside == 1) -> inside-- -> flag[_pid] = false' '}' > stuck.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check for a deadlock
spinrun stuck.pml | grep -E 'pan:1|errors'Shown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
A common mistake
Warning
Many people think a lock is good once SPIN finds no assertion failure. A lock that never lets anybody in also passes that test. A good check asks two things: nobody is ever in together, and everybody who wants in gets in.