# Optimistic Locking Pattern

> Optimistic locking with version numbers: a runnable model of concurrent read-modify-write updates using compare-and-set, checked for lost updates.

Canonical: https://fizzbee.io/design/patterns/optimistic-locking/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-01-04-optimistic-locking


Version-based concurrency control

**Demonstrates:** optimistic locking, version numbers, CAS

```fizz
# Example 0069: Optimistic Locking Pattern
# Version-based concurrency control
# Demonstrates: optimistic locking, version numbers, CAS

action Init:
    value = 0
    version = 0
    txn1_read_version = None
    txn1_new_value = None
    txn2_read_version = None
    txn2_new_value = None
    commits = 0

atomic action Txn1Read:
    require txn1_read_version == None

    txn1_read_version = version
    txn1_new_value = value + 1

atomic action Txn1Commit:
    require txn1_read_version != None
    require commits < 2

    # CAS: commit only if version unchanged
    if version == txn1_read_version:
        value = txn1_new_value
        version = version + 1
        commits = commits + 1

atomic action Txn2Read:
    require txn2_read_version == None

    txn2_read_version = version
    txn2_new_value = value + 10

atomic action Txn2Commit:
    require txn2_read_version != None
    require commits < 2

    # CAS: commit only if version unchanged
    if version == txn2_read_version:
        value = txn2_new_value
        version = version + 1
        commits = commits + 1

# Retry failed transaction
atomic action Txn2Retry:
    require txn2_read_version != None

    # Retry if version changed (CAS would fail)
    if version != txn2_read_version:
        txn2_read_version = version
        txn2_new_value = value + 10

# Safety: version increments with each commit
always assertion VersionMatches:
    return version == commits

# Safety: no lost updates (both can't commit if concurrent)
always assertion NoLostUpdates:
    if commits == 2:
        # Version should be 2, meaning sequential commits
        return version == 2
    return True

atomic action NoOp:
    if commits >= 2:
        pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 26, queued: 0
Valid Nodes: 26 Unique states: 26
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-01-04-optimistic-locking)

## Language features used

[Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/)