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:

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:

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). Teller1 based its calculation on values that were out of date at the point they were sent to the database.