Lost update — a non-atomic read-modify-write race¶

What this teaches: how separating a read and a write into two distinct steps opens a window where another actor can slip in, making the two steps non-atomic and silently discarding an update.

The bug¶

Actor A wants to increment a shared counter. It does this in two steps:

Read the current value into a local register.
Write the register + 1 back.

Actor B does the same. If the steps interleave like this:

A_read  → A sees x=0
B_read  → B sees x=0
A_write → x becomes 1
B_write → x becomes 1   ← B's write wins, A's increment is lost

both actors incremented, but the counter ends at 1, not 2. One increment vanished.

This is the lost update or ABA problem — the root cause of countless concurrency bugs in databases, counters, inventories, and account balances.

The model¶

The state carries the shared counter x plus per-actor read registers (a_reg, b_reg) that hold a value once read and are cleared on write. The invariant says: once both actors are done, the counter must equal 2.

musil's BFS explores every interleaving of the four actions (A_read, A_write, B_read, B_write) and finds the one where both reads happen before either write.

Invariant violated: both-increments-counted
Trace:
  A_read   → a_reg=0
  B_read   → b_reg=0
  A_write  → x=1
  B_write  → x=1   ← counter should be 2

The fix¶

Make test-and-increment a single atomic action. A single action cannot be interleaved — once its guard fires, the update happens before any other action runs. See Producer–consumer for a direct follow-up on this same fix applied to a bounded buffer.

Source¶

"""A lost-update race: two non-atomic increments of a shared counter.

Each actor reads the counter, then writes back read+1, as two separate steps. musil's interleaving
sweep finds the ordering where both read the old value before either writes — so the counter ends at
1, not 2. The shortest counterexample trace is printed.

Run: python examples/lost_update.py
"""

from __future__ import annotations

from dataclasses import dataclass, replace

from musil import Action, Model, check


@dataclass(frozen=True)
class Counter:
    x: int = 0
    a_reg: int | None = None  # A's read-but-not-yet-written value
    b_reg: int | None = None
    a_done: bool = False
    b_done: bool = False


MODEL = Model(
    init=Counter(),
    actions=[
        Action("A_read", lambda s: s.a_reg is None and not s.a_done, lambda s: replace(s, a_reg=s.x)),
        Action(
            "A_write",
            lambda s: s.a_reg is not None,
            lambda s: replace(s, x=(s.a_reg or 0) + 1, a_reg=None, a_done=True),
        ),
        Action("B_read", lambda s: s.b_reg is None and not s.b_done, lambda s: replace(s, b_reg=s.x)),
        Action(
            "B_write",
            lambda s: s.b_reg is not None,
            lambda s: replace(s, x=(s.b_reg or 0) + 1, b_reg=None, b_done=True),
        ),
    ],
    invariants={"both-increments-counted": lambda s: not (s.a_done and s.b_done) or s.x == 2},
    terminal=lambda s: s.a_done and s.b_done,
)


if __name__ == "__main__":
    print(check(MODEL))

Run it¶

python examples/lost_update.py