Read-Write Lock Pattern

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

# Example 0064: Read-Write Lock Pattern
# Multiple readers OR single writer
# Demonstrates: readers-writer lock, concurrent reads, exclusive writes

MAX_OPS = 3

action Init:
    readers = 0
    writer = False
    data = 0
    operations = 0

atomic action AcquireReadLock:
    require operations < MAX_OPS
    # Can read if no writer
    require not writer

    readers = readers + 1

atomic action ReleaseReadLock:
    require readers > 0

    readers = readers - 1
    operations = operations + 1

atomic action AcquireWriteLock:
    require operations < MAX_OPS
    # Can write if no readers and no writer
    require readers == 0 and not writer

    writer = True

atomic action ReleaseWriteLock:
    require writer

    writer = False
    data = data + 1
    operations = operations + 1

# Safety: no concurrent readers and writer
always assertion NoReadersWithWriter:
    if writer:
        return readers == 0
    return True

# Safety: at most one writer
always assertion SingleWriter:
    return writer == True or writer == False  # Boolean check

atomic action NoOp:
    if operations >= MAX_OPS:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 7509, queued: 0
Skipping dotfile generation. Too many Nodes: 7509
Valid Nodes: 7509 Unique states: 7509
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Mutex Pattern Distributed Lock Pattern gdoc_arrow_right_alt