Potential Issue in SharedMutex Implementation

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

```tla
---------------------------- 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 == <>

\* 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 <>

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

WaitForZeroInlineSharedCountOp(caller) ==
/\ exclusiveLockState[caller] = DeferredSharedSlotsChecked
/\ inlineSharedCount = 0
/\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockAcquired]
/\ UNCHANGED <>

ReleaseExclusiveLock(caller) ==
/\ exclusiveLockState[caller] = ExclusiveLockAcquired
/\ exclusiveCount' = 0
/\ exclusiveLockState' = [exclusiveLockState EXCEPT ![caller] = ExclusiveLockReleased]
/\ UNCHANGED <>

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

ReleaseInlineSharedLock(caller) ==
/\ inlineSharedLockState[caller] = SharedLockAcquired
/\ inlineSharedCount' = inlineSharedCount - 1
/\ inlineSharedLockState' = [inlineSharedLockState EXCEPT ![caller] = SharedLockReleased]
/\ UNCHANGED <>

\* 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 <>

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 <>

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 <>

\* 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
=============================================================================
```

```cfg
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:

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

State 2:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 3:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 0

State 4:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<1, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 5:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 6:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 7:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<2, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 8:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<3, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 9:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<4, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 10:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 11:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ inlineSharedCount = 0
/\ exclusiveCount = 1

State 12:
/\ inlineSharedLockState = <>
/\ exclusiveLockCheckDeferredSharedSlotIndex = <<5, 1, 1>>
/\ exclusiveLockState = <>
/\ deferredSharedLockState = <>
/\ deferredSharedSlots = <>
/\ 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](https://github.com/facebook/folly/blob/b59f99e724af79721190cf8d06be62b10c72f8e9/folly/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](https://github.com/facebook/folly/blob/b59f99e724af79721190cf8d06be62b10c72f8e9/folly/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.