Potential Issue in SharedMutex Implementation

[Clcanny]

I've been working with a simplified TLA+ model to verify the behavior of SharedMutex. During this process, I encountered an unexpected issue.

TLA+ Model and Configuration

---------------------------- MODULE LockModel ----------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

\* Constants
CONSTANTS NumExclusiveLockCallers, NumInlineSharedLockCallers, NumDeferredSharedLockCallers, MaxDeferredReadersAllocated

\* States
CONSTANTS Initialized, ExclusiveCountSet, DeferredSharedSlotsChecked, ZeroInlineSharedCountWaited, ExclusiveLockAcquired, ExclusiveLockReleased
CONSTANTS SharedLockAcquired, SharedLockReleased, DeferredSharedSlotSet

\* Variables
VARIABLES exclusiveCount, inlineSharedCount, deferredSharedSlots
VARIABLES exclusiveLockState, exclusiveLockCheckDeferredSharedSlotIndex
VARIABLES inlineSharedLockState, deferredSharedLockState

vars == <<exclusiveCount, inlineSharedCount, deferredSharedSlots, exclusiveLockState, exclusiveLockCheckDeferredSharedSlotIndex, inlineSharedLockState, deferredSharedLockState>>

\* TypeOK ensures the variables are of correct types
TypeOK == /\ exclusiveCount \in 0..1
          /\ inlineSharedCount \in Nat
          /\ deferredSharedSlots \in [1..MaxDeferredReadersAllocated -> BOOLEAN]
          /\ exclusiveLockState \in [1..NumExclusiveLockCallers -> {Initialized, ExclusiveCountSet, DeferredSharedSlotsChecked, ZeroInlineSharedCountWaited, ExclusiveLockAcquired, ExclusiveLockReleased}]
          /\ exclusiveLockCheckDeferredSharedSlotIndex \in [1..NumExclusiveLockCallers -> 1..MaxDeferredReadersAllocated]
          /\ inlineSharedLockState \in [1..NumInlineSharedLockCallers -> {Initialized, SharedLockAcquired, SharedLockReleased}]
          /\ deferredSharedLockState \in [1..NumDeferredSharedLockCallers -> {Initialized, DeferredSharedSlotSet, SharedLockAcquired, SharedLockReleased}]

\* Initial state
Init == /\ exclusiveCount = 0
        /\ inlineSharedCount = 0
        /\ deferredSharedSlots = [i \in 1..MaxDeferredReadersAllocated |-> FALSE]
        /\ exclusiveLockState = [i \in 1..NumExclusiveLockCallers |-> Initialized]
        /\ exclusiveLockCheckDeferredSharedSlotIndex = [i \in 1..NumExclusiveLockCallers |-> 1]
        /\ inlineSharedLockState = [i \in 1..NumInlineSharedLockCallers |-> Initialized]
        /\ deferredSharedLockState = [i \in 1..NumDeferredSharedLockCallers |-> Initialized]

\* Exclusive Lock Operations
SetExclusiveCount(caller) ==
    /\ exclusiveLockState[caller] = Initialized
    /\ exclusiveCount = 0
    /\ exclusiveCount' = 1
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveCountSet]
    /\ UNCHANGED <<inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

CheckDeferredSharedSlotsOp(caller) ==
  LET index == exclusiveLockCheckDeferredSharedSlotIndex[caller] IN
    /\ exclusiveLockState[caller] = ExclusiveCountSet
    /\ ~deferredSharedSlots[index]
    /\ IF index = MaxDeferredReadersAllocated
       THEN /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = DeferredSharedSlotsChecked]
           /\ UNCHANGED <<exclusiveLockCheckDeferredSharedSlotIndex>>
       ELSE /\ exclusiveLockCheckDeferredSharedSlotIndex' = [exclusiveLockCheckDeferredSharedSlotIndex EXCEPT ![caller] = index + 1]
           /\ UNCHANGED <<exclusiveLockState>>
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState>>

WaitForZeroInlineSharedCountOp(caller) ==
    /\ exclusiveLockState[caller] = DeferredSharedSlotsChecked
    /\ inlineSharedCount = 0
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockAcquired]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseExclusiveLock(caller) ==
    /\ exclusiveLockState[caller] = ExclusiveLockAcquired
    /\ exclusiveCount' = 0
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockReleased]
    /\ UNCHANGED <<inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Inline Shared Lock Operations
InlineSharedLockOp(caller) ==
    /\ inlineSharedLockState[caller] = Initialized
    /\ exclusiveCount = 0
    /\ inlineSharedCount' = inlineSharedCount + 1
    /\ inlineSharedLockState' = [inlineSharedLockState EXCEPT ![caller] = SharedLockAcquired]
    /\ UNCHANGED <<exclusiveCount, deferredSharedSlots, exclusiveLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseInlineSharedLock(caller) ==
    /\ inlineSharedLockState[caller] = SharedLockAcquired
    /\ inlineSharedCount' = inlineSharedCount - 1
    /\ inlineSharedLockState' = [inlineSharedLockState EXCEPT ![caller] = SharedLockReleased]
    /\ UNCHANGED <<exclusiveCount, deferredSharedSlots, exclusiveLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Deferred Shared Lock Operations
SetDeferredSharedSlotsOp(caller) ==
    /\ deferredSharedLockState[caller] = Initialized
    /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: ~deferredSharedSlots[j]}:
        /\ deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = TRUE]
        /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = DeferredSharedSlotSet]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

CheckZeroExclusiveCountOp(caller) ==
    /\ deferredSharedLockState[caller] = DeferredSharedSlotSet
    /\ IF exclusiveCount = 0
       THEN /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = SharedLockAcquired]
            /\ UNCHANGED deferredSharedSlots
       ELSE /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: deferredSharedSlots[j]}:
               deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = FALSE]
            /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = Initialized]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseDeferredSharedLock(caller) ==
    /\ deferredSharedLockState[caller] = SharedLockAcquired
    /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: deferredSharedSlots[j]}:
        deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = FALSE]
    /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = SharedLockReleased]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Next operation
Next == \/ \E caller \in 1..NumExclusiveLockCallers: SetExclusiveCount(caller) \/ CheckDeferredSharedSlotsOp(caller) \/ WaitForZeroInlineSharedCountOp(caller) \/ ReleaseExclusiveLock(caller)
        \/ \E caller \in 1..NumInlineSharedLockCallers: InlineSharedLockOp(caller) \/ ReleaseInlineSharedLock(caller)
        \/ \E caller \in 1..NumDeferredSharedLockCallers: SetDeferredSharedSlotsOp(caller) \/ CheckZeroExclusiveCountOp(caller) \/ ReleaseDeferredSharedLock(caller)

\* Specification
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Liveness Property
EventuallyReleased == <>(
    /\ \A caller \in 1..NumExclusiveLockCallers: exclusiveLockState[caller] = ExclusiveLockReleased
    /\ \A caller \in 1..NumInlineSharedLockCallers: inlineSharedLockState[caller] = SharedLockReleased
    /\ \A caller \in 1..NumDeferredSharedLockCallers: deferredSharedLockState[caller] = SharedLockReleased)

THEOREM SpecIsTypeOK == Spec => TypeOK
THEOREM SpecIsEventuallyReleased == Spec => EventuallyReleased

ExclusiveLockMutualExclusion == \A caller1, caller2 \in 1..NumExclusiveLockCallers:
  (exclusiveLockState[caller1] = ExclusiveLockAcquired) /\ (exclusiveLockState[caller2] = ExclusiveLockAcquired) => caller1 = caller2
THEOREM SpecIsExclusiveLockMutualExclusion == Spec => ExclusiveLockMutualExclusion

ExclusiveLockPreventsShared == \A caller \in 1..NumExclusiveLockCallers:
  exclusiveLockState[caller] = ExclusiveLockAcquired =>
    /\ \A c \in 1..NumInlineSharedLockCallers: inlineSharedLockState[c] # SharedLockAcquired
    /\ \A c \in 1..NumDeferredSharedLockCallers: deferredSharedLockState[c] # SharedLockAcquired
THEOREM SpecIsExclusiveLockPreventsShared == Spec => ExclusiveLockPreventsShared
=============================================================================

CONSTANTS
  NumExclusiveLockCallers = 3
  NumInlineSharedLockCallers = 3
  NumDeferredSharedLockCallers = 3
  MaxDeferredReadersAllocated = 5

  Initialized = Initialized
  ExclusiveCountSet = ExclusiveCountSet
  DeferredSharedSlotsChecked = DeferredSharedSlotsChecked
  ZeroInlineSharedCountWaited = ZeroInlineSharedCountWaited
  ExclusiveLockAcquired = ExclusiveLockAcquired
  ExclusiveLockReleased = ExclusiveLockReleased
  SharedLockAcquired = SharedLockAcquired
  SharedLockReleased = SharedLockReleased
  DeferredSharedSlotSet = DeferredSharedSlotSet

SPECIFICATION
  Spec

INVARIANTS
  TypeOK
  ExclusiveLockMutualExclusion
  ExclusiveLockPreventsShared

PROPERTY
  \* EventuallyReleased

When running the command tlc LockModel.tla -config LockModel.cfg -deadlock, TLC reports the following error:

Error: Invariant ExclusiveLockPreventsShared is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 2: <SetDeferredSharedSlotsOp(1) line 83, col 5 to line 87, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<DeferredSharedSlotSet, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 3: <CheckZeroExclusiveCountOp(1) line 90, col 5 to line 97, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 4: <SetExclusiveCount(1) line 38, col 5 to line 42, col 150 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 5: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 6: <SetDeferredSharedSlotsOp(2) line 83, col 5 to line 87, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, DeferredSharedSlotSet, Initialized>>
/\ deferredSharedSlots = <<TRUE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 7: <CheckZeroExclusiveCountOp(2) line 90, col 5 to line 97, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 8: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<3, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 9: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<4, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 10: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 11: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<DeferredSharedSlotsChecked, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 12: <WaitForZeroInlineSharedCountOp(1) line 56, col 5 to line 59, col 166 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<ExclusiveLockAcquired, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

845561 states generated, 123007 distinct states found, 26576 states left on queue.
The depth of the complete state graph search is 12.

Code Path Analysis

The issue seems to occur under the following conditions:

The caller attempts to acquire an exclusive lock at:

1. SharedMutex.h#L1082.
2. It checks whether all deferred readers are clear. If they are, lockExclusiveImpl returns true, indicating the exclusive lock is held: SharedMutex.h#L1262.

The problem arises because the check for deferred readers is not atomic. It's possible for a caller attempting to acquire a read lock to manipulate the deferred slots. Specifically, setting slot 2, encountering an exclusive lock, and then releasing slot 1, effectively moving slot 2 to slot 1, which might bypass applyDeferredReaders.

Uncertainty

The entire locking mechanism is quite complex for me, and I'm not certain if the TLA+ error is due to a misunderstanding on my part or if it indicates a genuine bug. I would appreciate the opportunity to discuss this further. Thank you for your attention.

[pgsohail]

I've been working with a simplified TLA+ model to verify the behavior of SharedMutex. During this process, I encountered an unexpected issue.

TLA+ Model and Configuration

---------------------------- MODULE LockModel ----------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

\* Constants
CONSTANTS NumExclusiveLockCallers, NumInlineSharedLockCallers, NumDeferredSharedLockCallers, MaxDeferredReadersAllocated

\* States
CONSTANTS Initialized, ExclusiveCountSet, DeferredSharedSlotsChecked, ZeroInlineSharedCountWaited, ExclusiveLockAcquired, ExclusiveLockReleased
CONSTANTS SharedLockAcquired, SharedLockReleased, DeferredSharedSlotSet

\* Variables
VARIABLES exclusiveCount, inlineSharedCount, deferredSharedSlots
VARIABLES exclusiveLockState, exclusiveLockCheckDeferredSharedSlotIndex
VARIABLES inlineSharedLockState, deferredSharedLockState

vars == <<exclusiveCount, inlineSharedCount, deferredSharedSlots, exclusiveLockState, exclusiveLockCheckDeferredSharedSlotIndex, inlineSharedLockState, deferredSharedLockState>>

\* TypeOK ensures the variables are of correct types
TypeOK == /\ exclusiveCount \in 0..1
          /\ inlineSharedCount \in Nat
          /\ deferredSharedSlots \in [1..MaxDeferredReadersAllocated -> BOOLEAN]
          /\ exclusiveLockState \in [1..NumExclusiveLockCallers -> {Initialized, ExclusiveCountSet, DeferredSharedSlotsChecked, ZeroInlineSharedCountWaited, ExclusiveLockAcquired, ExclusiveLockReleased}]
          /\ exclusiveLockCheckDeferredSharedSlotIndex \in [1..NumExclusiveLockCallers -> 1..MaxDeferredReadersAllocated]
          /\ inlineSharedLockState \in [1..NumInlineSharedLockCallers -> {Initialized, SharedLockAcquired, SharedLockReleased}]
          /\ deferredSharedLockState \in [1..NumDeferredSharedLockCallers -> {Initialized, DeferredSharedSlotSet, SharedLockAcquired, SharedLockReleased}]

\* Initial state
Init == /\ exclusiveCount = 0
        /\ inlineSharedCount = 0
        /\ deferredSharedSlots = [i \in 1..MaxDeferredReadersAllocated |-> FALSE]
        /\ exclusiveLockState = [i \in 1..NumExclusiveLockCallers |-> Initialized]
        /\ exclusiveLockCheckDeferredSharedSlotIndex = [i \in 1..NumExclusiveLockCallers |-> 1]
        /\ inlineSharedLockState = [i \in 1..NumInlineSharedLockCallers |-> Initialized]
        /\ deferredSharedLockState = [i \in 1..NumDeferredSharedLockCallers |-> Initialized]

\* Exclusive Lock Operations
SetExclusiveCount(caller) ==
    /\ exclusiveLockState[caller] = Initialized
    /\ exclusiveCount = 0
    /\ exclusiveCount' = 1
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveCountSet]
    /\ UNCHANGED <<inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

CheckDeferredSharedSlotsOp(caller) ==
  LET index == exclusiveLockCheckDeferredSharedSlotIndex[caller] IN
    /\ exclusiveLockState[caller] = ExclusiveCountSet
    /\ ~deferredSharedSlots[index]
    /\ IF index = MaxDeferredReadersAllocated
       THEN /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = DeferredSharedSlotsChecked]
           /\ UNCHANGED <<exclusiveLockCheckDeferredSharedSlotIndex>>
       ELSE /\ exclusiveLockCheckDeferredSharedSlotIndex' = [exclusiveLockCheckDeferredSharedSlotIndex EXCEPT ![caller] = index + 1]
           /\ UNCHANGED <<exclusiveLockState>>
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState>>

WaitForZeroInlineSharedCountOp(caller) ==
    /\ exclusiveLockState[caller] = DeferredSharedSlotsChecked
    /\ inlineSharedCount = 0
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockAcquired]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseExclusiveLock(caller) ==
    /\ exclusiveLockState[caller] = ExclusiveLockAcquired
    /\ exclusiveCount' = 0
    /\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockReleased]
    /\ UNCHANGED <<inlineSharedCount, deferredSharedSlots, inlineSharedLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Inline Shared Lock Operations
InlineSharedLockOp(caller) ==
    /\ inlineSharedLockState[caller] = Initialized
    /\ exclusiveCount = 0
    /\ inlineSharedCount' = inlineSharedCount + 1
    /\ inlineSharedLockState' = [inlineSharedLockState EXCEPT ![caller] = SharedLockAcquired]
    /\ UNCHANGED <<exclusiveCount, deferredSharedSlots, exclusiveLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseInlineSharedLock(caller) ==
    /\ inlineSharedLockState[caller] = SharedLockAcquired
    /\ inlineSharedCount' = inlineSharedCount - 1
    /\ inlineSharedLockState' = [inlineSharedLockState EXCEPT ![caller] = SharedLockReleased]
    /\ UNCHANGED <<exclusiveCount, deferredSharedSlots, exclusiveLockState, deferredSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Deferred Shared Lock Operations
SetDeferredSharedSlotsOp(caller) ==
    /\ deferredSharedLockState[caller] = Initialized
    /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: ~deferredSharedSlots[j]}:
        /\ deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = TRUE]
        /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = DeferredSharedSlotSet]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

CheckZeroExclusiveCountOp(caller) ==
    /\ deferredSharedLockState[caller] = DeferredSharedSlotSet
    /\ IF exclusiveCount = 0
       THEN /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = SharedLockAcquired]
            /\ UNCHANGED deferredSharedSlots
       ELSE /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: deferredSharedSlots[j]}:
               deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = FALSE]
            /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = Initialized]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

ReleaseDeferredSharedLock(caller) ==
    /\ deferredSharedLockState[caller] = SharedLockAcquired
    /\ \E i \in {j \in 1..MaxDeferredReadersAllocated: deferredSharedSlots[j]}:
        deferredSharedSlots' = [deferredSharedSlots EXCEPT ![i] = FALSE]
    /\ deferredSharedLockState' = [deferredSharedLockState EXCEPT ![caller] = SharedLockReleased]
    /\ UNCHANGED <<exclusiveCount, inlineSharedCount, exclusiveLockState, inlineSharedLockState, exclusiveLockCheckDeferredSharedSlotIndex>>

\* Next operation
Next == \/ \E caller \in 1..NumExclusiveLockCallers: SetExclusiveCount(caller) \/ CheckDeferredSharedSlotsOp(caller) \/ WaitForZeroInlineSharedCountOp(caller) \/ ReleaseExclusiveLock(caller)
        \/ \E caller \in 1..NumInlineSharedLockCallers: InlineSharedLockOp(caller) \/ ReleaseInlineSharedLock(caller)
        \/ \E caller \in 1..NumDeferredSharedLockCallers: SetDeferredSharedSlotsOp(caller) \/ CheckZeroExclusiveCountOp(caller) \/ ReleaseDeferredSharedLock(caller)

\* Specification
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Liveness Property
EventuallyReleased == <>(
    /\ \A caller \in 1..NumExclusiveLockCallers: exclusiveLockState[caller] = ExclusiveLockReleased
    /\ \A caller \in 1..NumInlineSharedLockCallers: inlineSharedLockState[caller] = SharedLockReleased
    /\ \A caller \in 1..NumDeferredSharedLockCallers: deferredSharedLockState[caller] = SharedLockReleased)

THEOREM SpecIsTypeOK == Spec => TypeOK
THEOREM SpecIsEventuallyReleased == Spec => EventuallyReleased

ExclusiveLockMutualExclusion == \A caller1, caller2 \in 1..NumExclusiveLockCallers:
  (exclusiveLockState[caller1] = ExclusiveLockAcquired) /\ (exclusiveLockState[caller2] = ExclusiveLockAcquired) => caller1 = caller2
THEOREM SpecIsExclusiveLockMutualExclusion == Spec => ExclusiveLockMutualExclusion

ExclusiveLockPreventsShared == \A caller \in 1..NumExclusiveLockCallers:
  exclusiveLockState[caller] = ExclusiveLockAcquired =>
    /\ \A c \in 1..NumInlineSharedLockCallers: inlineSharedLockState[c] # SharedLockAcquired
    /\ \A c \in 1..NumDeferredSharedLockCallers: deferredSharedLockState[c] # SharedLockAcquired
THEOREM SpecIsExclusiveLockPreventsShared == Spec => ExclusiveLockPreventsShared
=============================================================================

CONSTANTS
  NumExclusiveLockCallers = 3
  NumInlineSharedLockCallers = 3
  NumDeferredSharedLockCallers = 3
  MaxDeferredReadersAllocated = 5

  Initialized = Initialized
  ExclusiveCountSet = ExclusiveCountSet
  DeferredSharedSlotsChecked = DeferredSharedSlotsChecked
  ZeroInlineSharedCountWaited = ZeroInlineSharedCountWaited
  ExclusiveLockAcquired = ExclusiveLockAcquired
  ExclusiveLockReleased = ExclusiveLockReleased
  SharedLockAcquired = SharedLockAcquired
  SharedLockReleased = SharedLockReleased
  DeferredSharedSlotSet = DeferredSharedSlotSet

SPECIFICATION
  Spec

INVARIANTS
  TypeOK
  ExclusiveLockMutualExclusion
  ExclusiveLockPreventsShared

PROPERTY
  \* EventuallyReleased

When running the command tlc LockModel.tla -config LockModel.cfg -deadlock, TLC reports the following error:

Error: Invariant ExclusiveLockPreventsShared is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 2: <SetDeferredSharedSlotsOp(1) line 83, col 5 to line 87, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<DeferredSharedSlotSet, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 3: <CheckZeroExclusiveCountOp(1) line 90, col 5 to line 97, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<Initialized, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 4: <SetExclusiveCount(1) line 38, col 5 to line 42, col 150 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 5: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<FALSE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 6: <SetDeferredSharedSlotsOp(2) line 83, col 5 to line 87, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, DeferredSharedSlotSet, Initialized>>
/\ deferredSharedSlots = <<TRUE, TRUE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 7: <CheckZeroExclusiveCountOp(2) line 90, col 5 to line 97, col 140 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 8: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<3, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 9: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<4, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 10: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<ExclusiveCountSet, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 11: <CheckDeferredSharedSlotsOp(1) line 46, col 5 to line 53, col 123 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<DeferredSharedSlotsChecked, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 12: <WaitForZeroInlineSharedCountOp(1) line 56, col 5 to line 59, col 166 of module LockModel>
/\ inlineSharedLockState = <<Initialized, Initialized, Initialized>>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <<ExclusiveLockAcquired, Initialized, Initialized>>
/\ deferredSharedLockState = <<SharedLockAcquired, Initialized, Initialized>>
/\ deferredSharedSlots = <<TRUE, FALSE, FALSE, FALSE, FALSE>>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

845561 states generated, 123007 distinct states found, 26576 states left on queue.
The depth of the complete state graph search is 12.

Code Path Analysis

The issue seems to occur under the following conditions:

The caller attempts to acquire an exclusive lock at:

1. SharedMutex.h#L1082.
2. It checks whether all deferred readers are clear. If they are, lockExclusiveImpl returns true, indicating the exclusive lock is held: SharedMutex.h#L1262.

The problem arises because the check for deferred readers is not atomic. It's possible for a caller attempting to acquire a read lock to manipulate the deferred slots. Specifically, setting slot 2, encountering an exclusive lock, and then releasing slot 1, effectively moving slot 2 to slot 1, which might bypass applyDeferredReaders.

Uncertainty

The entire locking mechanism is quite complex for me, and I'm not certain if the TLA+ error is due to a misunderstanding on my part or if it indicates a genuine bug. I would appreciate the opportunity to discuss this further. Thank you for your attention.

Thanks for bringing this up! I reviewed the TLA+ model, and there are a few areas that might be causing the unexpected behavior:

Refactor the Init Action: Start by confirming that all variables are properly initialized according to your intended starting state. Any deviation might cause issues during the state exploration.

Review State Transitions: Revisit the Next action, ensuring that each operation transition correctly reflects the real-world behavior of the mutex. Pay attention to the order of operations and conditions.

Run TLC Model Checker: Use different configurations in TLC to identify potential pitfalls. Carefully analyze any counterexamples it generates, as these can guide you towards the root cause of the problem.