3.9 · Shared-state interleavings

The same updates can differ when reads and writes interleave.

Writing each read and write as a separate step lets one finite schedule expose a lost update while a serialized schedule preserves both changes.

Guiding question

What disappears when two updates read the same shared balance before either finishes?

Separate each transaction read from its later write
Recognize a write computed from a stale shared value
Enumerate the exact step order of a finite schedule
Compare a lost-update result with a serialized result

The deposit adds 10 and the withdrawal subtracts 20. In the first schedule, both operations read 100. The deposit writes 110, but the withdrawal still computes from its earlier read and writes 80. The later write replaces the deposit result, so the final balance does not contain both changes.

The second schedule lets the deposit read and write before the withdrawal reads. The withdrawal therefore sees 110 and writes 90. These programs enumerate two already chosen finite schedules. They do not create threads or a serializer, and they do not establish the result of every possible interleaving.

Lispex · SICP sourceScheme-compatible SICP syntax executed by the Lispex SICP profile.

(begin
  (define balance 100)
  (define deposit-read balance)
  (define withdraw-read balance)
  (define deposit-write (+ deposit-read 10))
  (set! balance deposit-write)
  (define withdraw-write (- withdraw-read 20))
  (set! balance withdraw-write)
  (list (list 'deposit 'read deposit-read)
        (list 'withdraw 'read withdraw-read)
        (list 'deposit 'write deposit-write)
        (list 'withdraw 'write withdraw-write)
        (list 'final balance)))

Lispex learning runtimeLispex SICP profile 1.0.0

Loading Lispex SICP runtime

Lispex · SICP source461 / 1,048,576 UTF-8 bytes

Examples

Result—

Output: —
Value: —
Diagnostic: —

Visible execution0 / 0 trace events

This browser result is not a Lispex Vouch record or authority.wasm —

Expected observation

The first program returns ((deposit read 100) (withdraw read 100) (deposit write 110) (withdraw write 80) (final 80)). The serialized program returns ((deposit read 100) (deposit write 110) (withdraw read 110) (withdraw write 90) (final 90)).

Trace focus

Follow the two initial balance reads before either assignment in the first run, then locate the writes of 110 and 80. In the second run, the withdrawal read follows the write of 110. The bounded traces describe only these two explicit schedules.

Try it yourself

Change the program before you read the hint.

In the first schedule, place the withdrawal write before the deposit write. Predict the final balance and name the update that is then lost.

Show one hint

Both writes were computed from 100, so the write that occurs last determines the final balance.