A race condition needs one exact order
A race condition is a fault that appears only when two processes run their steps in one particular order. A test usually runs the same order every time, so it misses the fault.
SPIN is a model checker that tries every order and prints the one that breaks the program.
By the end of this lesson
Note
I can find a race between two processes in a trace.
Key words
| Word | What it means | Example |
|---|---|---|
| Process | a program that runs its own steps | |
| Shared variable | a value that two processes can both change | |
| Interleaving | one order in which the steps of two processes mix | |
| Race condition | a fault that depends on the order of steps | |
| Assertion | a rule the model checker tests at one point | assert(till == 20) |
| Trace | the list of steps that led to a failure |
The cells students fill in are left blank in this preview.
Two cashiers can lose money
Two cashiers each add 10 pounds to a shared till. Each one does two steps: read the till, then write what it read plus 10.
If cashier A reads, then B reads, then both write, each wrote 10. The till holds 10, not 20. One payment is lost.
Worked example: one bad order
| Step | Who | What happens | Till after |
|---|---|---|---|
| 1 | A | reads the till and sees 0 | 0 |
| 2 | B | reads the till and sees 0 | 0 |
| 3 | A | writes 0 + 10 | 10 |
| 4 | B | writes 0 + 10 | 10 |
The cells students fill in are left blank in this preview.
The number of orders grows fast
Two processes of two steps each can mix in 6 ways. Only 2 of them are safe: A finishes before B starts, or the other way round.
Add steps and the count explodes, as the table shows. A test runs one order. A model checker tries all of them.
Steps in each process and orders to try
| Steps in each process | Orders to try |
|---|---|
| 1 | 2 |
| 2 | 6 |
| 3 | 20 |
| 4 | 70 |
| 5 | 252 |
The cells students fill in are left blank in this preview.
Promela writes a process as steps
Promela is the language SPIN reads. A proctype is a process, and active [2] starts two copies of it. Each statement is one step, and the checker may switch to the other process after any step.
A statement is usually ended by a semicolon. -> means the same, so these models use it to read as "then". The table explains the file.
Worked example: the till model line by line
| Line | What it says |
|---|---|
| byte till = 0 | the shared till starts at 0 |
| byte done = 0 | counts the cashiers that have finished |
| active [2] proctype cashier() { | start two cashier processes |
| seen = till -> till = seen + 10 -> done++ | read, then write plus 10, then count one finished |
| active proctype audit() { | a third process that checks the end |
| done == 2 -> assert(till == 20) | wait until both finished, then demand 20 |
The cells students fill in are left blank in this preview.
Write the model to a file
printf '%s\n' 'byte till = 0' 'byte done = 0' 'active [2] proctype cashier() {' ' byte seen' ' seen = till -> till = seen + 10 -> done++' '}' 'active proctype audit() {' ' done == 2 -> assert(till == 20)' '}' > till.pmlShown here, not run. Create a free account to press Run and type it into your own lab’s terminal.
Check every order
spinrun till.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.
Replay the bad order
spin -t -p till.pmlShown 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 running the program many times will show a race. A race needs one exact order of steps. A normal run may pick the same order a million times. A model checker tries every order, so it finds the race in one run.