About the race sample
The race sample is in Bank-race.mon. It implements Get and Set events, and corresponding Response events. A teller can find the value of an account, perform some modification and then set the new account value. To take money from one account, the protocol is as follows:
1. Send a Get event to obtain the current value of the account.
2. Wait for a GetResponse event that contains the current value.
3. Compute the new account value.
4. Send a Set event to set the new account value.
5. Wait for a SetResponse event.
This works well when a single transfer occurs at a time. However, there is a bug because between the time that teller 1 obtains an account value and the time that teller 1 sets the new account value, teller 2 can obtain the account value, compute a new value, and set a new account value. The following time line demonstrates this:
Time | Teller 1 | Teller 2 | Bank Database |
0 (setup) | Transfer 50 from A to B | | A: 100 B: 100 C: 100 |
| Get A, Get B | | |
| A=100, B=100 | | |
| Sleep 1 second | | |
0.5 | | Transfer 25 from B to C | |
| | Get B, Get C | |
| | B=100, C=100 | |
| | newB=75, newC=125 | |
| | Set B, Set C | |
| | | A: 100, B: 75, C: 125 |
1.0 | newA=50, newB = 150 | | |
| Set A, Set B | | |
| | | A: 50, B: 150, C: 125 |
B's account should have 100 + 50 – 25 = 125. But it ends up with 150 because teller 1 overwrites teller 2's value for B's account (75). Teller 1 based its calculation on values that were out of date at the point they were sent to the database.