diff options
Diffstat (limited to 'design/68578/spinbit.tla')
| -rw-r--r-- | design/68578/spinbit.tla | 533 |
1 files changed, 533 insertions, 0 deletions
diff --git a/design/68578/spinbit.tla b/design/68578/spinbit.tla new file mode 100644 index 0000000..3023b20 --- /dev/null +++ b/design/68578/spinbit.tla @@ -0,0 +1,533 @@ +------------------------------ MODULE spinbit ------------------------------ +EXTENDS TLC, Integers, Sequences, FiniteSets + +CONSTANT NumThreads +CONSTANT NumAcquires +CONSTANT NumSpins \* performance tunable "spin" +CONSTANT WakeAny \* reduce state space: wake any of the sleepers +CONSTANT NULL \* [ model value ] + +ASSUME NumThreads >= 1 +ASSUME NumAcquires >= 0 +ASSUME NumSpins >= 0 +ASSUME WakeAny \in BOOLEAN + +Threads == 1..NumThreads + +(* --algorithm spinbit + +variables + + \* logical owner + owner = NULL; + + \* lock state, stored in l.key word + l_key_locked = FALSE; \* bit 0 + l_key_sleeping = FALSE; \* bit 1 + l_key_spinning = FALSE; \* bit 63 + + \* local variables + v_locked = [t \in Threads |-> FALSE]; + v_sleeping = [t \in Threads |-> FALSE]; + v_spinning = [t \in Threads |-> FALSE]; + v8_locked = [t \in Threads |-> FALSE]; + v8_sleeping = [t \in Threads |-> FALSE]; + weSpin = [t \in Threads |-> FALSE]; + i = [t \in Threads |-> 0]; + + \* OS state + sleepers = {}; + + \* + acquisitions = 0; + + \* performance tunables + spin = NumSpins; + +define + + TypeInvariant == + /\ owner \in Threads \union {NULL} + /\ l_key_locked \in BOOLEAN + /\ l_key_sleeping \in BOOLEAN + /\ l_key_spinning \in BOOLEAN + /\ \A t \in Threads: v_locked[t] \in BOOLEAN + /\ \A t \in Threads: v_sleeping[t] \in BOOLEAN + /\ \A t \in Threads: v_spinning[t] \in BOOLEAN + /\ \A t \in Threads: v8_locked[t] \in BOOLEAN + /\ \A t \in Threads: v8_sleeping[t] \in BOOLEAN + /\ \A t \in Threads: weSpin[t] \in BOOLEAN + /\ \A t \in Threads: i[t] \in Nat + /\ sleepers \subseteq Threads + /\ acquisitions \in Nat + + NoLostWakeups == + (Cardinality(sleepers) > 0) ~> (Cardinality(sleepers) = 0) + + HaveAcquisitions == + <>[](acquisitions >= NumAcquires) + +end define; + +\* This is a lock, so if a process dies while holding it the rest of the simulation +\* won't be able to make progress. We need "fair process" so the threads don't die. +fair process thread \in Threads +begin + NonCriticalSection: + if acquisitions >= NumAcquires then + goto Done; + end if; + + SpeculativeGrab: + \* v8 = atomic.Xchg8(k8, mutexLocked) + v8_locked[self] := l_key_locked; + v8_sleeping[self] := l_key_sleeping; + l_key_locked := TRUE; + l_key_sleeping := FALSE; + SpeculativeGrabCheck: + if v8_locked[self] = FALSE then + if v8_sleeping[self] = TRUE then + \* atomic.Or8(k8, mutexSleeping) + l_key_sleeping := TRUE; + end if; + goto Locked; + else + \* var v uintptr = mutexLocked + v_locked[self] := TRUE; + v_sleeping[self] := FALSE; + v_spinning[self] := FALSE; + weSpin[self] := FALSE; + end if; + + EnterSlowPath: + i[self] := 0; + + TryAcquire: + if v_locked[self] = TRUE then + goto SetSleepBit + else + if weSpin[self] then + \* next := (v &^ mutexSpinning) | mutexLocked | mutexSleeping + \* if atomic.Casuintptr(&l.key, v, next) { + if v_locked[self] = l_key_locked + /\ v_sleeping[self] = l_key_sleeping + /\ v_spinning[self] = l_key_spinning then + l_key_locked := TRUE; + l_key_sleeping := TRUE; + l_key_spinning := FALSE; + goto Locked; + end if; + else + \* prev8 := atomic.Xchg8(k8, mutexLocked|mutexSleeping) + \* if prev8&mutexLocked == 0 { + if l_key_locked = FALSE then + l_key_locked := TRUE; + l_key_sleeping := TRUE; + goto Locked; + else + l_key_locked := TRUE; + l_key_sleeping := TRUE; + end if; + end if; + end if; + TryAcquireLoop: + \* v = atomic.Loaduintptr(&l.key) + v_locked[self] := l_key_locked; + v_sleeping[self] := l_key_sleeping; + v_spinning[self] := l_key_spinning; + goto TryAcquire; + + SetSleepBit: + \* atomic.Or8(k8, mutexSleeping) + if v_sleeping[self] = FALSE then + l_key_sleeping := TRUE; + v_sleeping[self] := TRUE; + end if; + + SetSpinBit: + \* if !weSpin && atomic.Xchg8(key8Upper(&l.key), mutexSpinning>>((goarch.PtrSize-1)*8)) == 0 { + if weSpin[self] = FALSE then + weSpin[self] := (l_key_spinning = FALSE); + l_key_spinning := TRUE; + end if; + + DoSpin: + if weSpin[self] = TRUE then + if i[self] < spin then + \* procyield(active_spin_cnt) + \* v = atomic.Loaduintptr(&l.key) + v_locked[self] := l_key_locked; + v_sleeping[self] := l_key_sleeping; + v_spinning[self] := l_key_spinning; + goto TryAcquire; + else + weSpin[self] := FALSE; + \* atomic.Xchg8(key8Upper(&l.key), 0) + l_key_spinning := FALSE; + end if; + end if; + + Sleep: + \* v = atomic.Loaduintptr(&l.key) + v_locked[self] := l_key_locked; + v_sleeping[self] := l_key_sleeping; + v_spinning[self] := l_key_spinning; + Futex: + if v_locked[self] = FALSE then + goto TryAcquire; + else + \* futexsleep(k32, uint32(v|mutexSleeping), -1) + if l_key_locked = v_locked[self] + /\ l_key_sleeping = TRUE then + sleepers := sleepers \union {self}; + end if; + end if; + + Sleeping: + await self \notin sleepers; + i[self] := 0; + \* v = atomic.Loaduintptr(&l.key) + v_locked[self] := l_key_locked; + v_sleeping[self] := l_key_sleeping; + v_spinning[self] := l_key_spinning; + goto TryAcquire; + + Locked: + owner := self; + CriticalSection: + acquisitions := acquisitions + 1; + Unlock: + owner := NULL; + \* prev8 := atomic.Xchg8(key8(&l.key), 0) + v8_locked[self] := l_key_locked; + v8_sleeping[self] := l_key_sleeping; + l_key_locked := FALSE; + l_key_sleeping := FALSE; + if v8_sleeping[self] = TRUE then + goto Wakeup; + else + goto NonCriticalSection; + end if; + + Wakeup: + \* v := atomic.Loaduintptr(&l.key) + v_locked[self] := l_key_locked; + v_sleeping[self] := l_key_sleeping; + v_spinning[self] := l_key_spinning; + Wake2: + if v_spinning[self] = FALSE then + if Cardinality(sleepers) > 0 then + if WakeAny then + with other = CHOOSE other \in sleepers: TRUE do + sleepers := sleepers \ {other}; + end with; + else + with other \in sleepers do + sleepers := sleepers \ {other}; + end with; + end if; + end if; + end if; + goto NonCriticalSection; + +end process; + +end algorithm; *) +\* BEGIN TRANSLATION (chksum(pcal) = "a993096" /\ chksum(tla) = "41bbe278") +VARIABLES owner, l_key_locked, l_key_sleeping, l_key_spinning, v_locked, + v_sleeping, v_spinning, v8_locked, v8_sleeping, weSpin, i, sleepers, + acquisitions, spin, pc + +(* define statement *) +TypeInvariant == + /\ owner \in Threads \union {NULL} + /\ l_key_locked \in BOOLEAN + /\ l_key_sleeping \in BOOLEAN + /\ l_key_spinning \in BOOLEAN + /\ \A t \in Threads: v_locked[t] \in BOOLEAN + /\ \A t \in Threads: v_sleeping[t] \in BOOLEAN + /\ \A t \in Threads: v_spinning[t] \in BOOLEAN + /\ \A t \in Threads: v8_locked[t] \in BOOLEAN + /\ \A t \in Threads: v8_sleeping[t] \in BOOLEAN + /\ \A t \in Threads: weSpin[t] \in BOOLEAN + /\ \A t \in Threads: i[t] \in Nat + /\ sleepers \subseteq Threads + /\ acquisitions \in Nat + +NoLostWakeups == + (Cardinality(sleepers) > 0) ~> (Cardinality(sleepers) = 0) + +HaveAcquisitions == + <>[](acquisitions >= NumAcquires) + + +vars == << owner, l_key_locked, l_key_sleeping, l_key_spinning, v_locked, + v_sleeping, v_spinning, v8_locked, v8_sleeping, weSpin, i, + sleepers, acquisitions, spin, pc >> + +ProcSet == (Threads) + +Init == (* Global variables *) + /\ owner = NULL + /\ l_key_locked = FALSE + /\ l_key_sleeping = FALSE + /\ l_key_spinning = FALSE + /\ v_locked = [t \in Threads |-> FALSE] + /\ v_sleeping = [t \in Threads |-> FALSE] + /\ v_spinning = [t \in Threads |-> FALSE] + /\ v8_locked = [t \in Threads |-> FALSE] + /\ v8_sleeping = [t \in Threads |-> FALSE] + /\ weSpin = [t \in Threads |-> FALSE] + /\ i = [t \in Threads |-> 0] + /\ sleepers = {} + /\ acquisitions = 0 + /\ spin = NumSpins + /\ pc = [self \in ProcSet |-> "NonCriticalSection"] + +NonCriticalSection(self) == /\ pc[self] = "NonCriticalSection" + /\ IF acquisitions >= NumAcquires + THEN /\ pc' = [pc EXCEPT ![self] = "Done"] + ELSE /\ pc' = [pc EXCEPT ![self] = "SpeculativeGrab"] + /\ UNCHANGED << owner, l_key_locked, + l_key_sleeping, l_key_spinning, + v_locked, v_sleeping, v_spinning, + v8_locked, v8_sleeping, weSpin, i, + sleepers, acquisitions, spin >> + +SpeculativeGrab(self) == /\ pc[self] = "SpeculativeGrab" + /\ v8_locked' = [v8_locked EXCEPT ![self] = l_key_locked] + /\ v8_sleeping' = [v8_sleeping EXCEPT ![self] = l_key_sleeping] + /\ l_key_locked' = TRUE + /\ l_key_sleeping' = FALSE + /\ pc' = [pc EXCEPT ![self] = "SpeculativeGrabCheck"] + /\ UNCHANGED << owner, l_key_spinning, v_locked, + v_sleeping, v_spinning, weSpin, i, + sleepers, acquisitions, spin >> + +SpeculativeGrabCheck(self) == /\ pc[self] = "SpeculativeGrabCheck" + /\ IF v8_locked[self] = FALSE + THEN /\ IF v8_sleeping[self] = TRUE + THEN /\ l_key_sleeping' = TRUE + ELSE /\ TRUE + /\ UNCHANGED l_key_sleeping + /\ pc' = [pc EXCEPT ![self] = "Locked"] + /\ UNCHANGED << v_locked, v_sleeping, + v_spinning, weSpin >> + ELSE /\ v_locked' = [v_locked EXCEPT ![self] = TRUE] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = FALSE] + /\ v_spinning' = [v_spinning EXCEPT ![self] = FALSE] + /\ weSpin' = [weSpin EXCEPT ![self] = FALSE] + /\ pc' = [pc EXCEPT ![self] = "EnterSlowPath"] + /\ UNCHANGED l_key_sleeping + /\ UNCHANGED << owner, l_key_locked, + l_key_spinning, v8_locked, + v8_sleeping, i, sleepers, + acquisitions, spin >> + +EnterSlowPath(self) == /\ pc[self] = "EnterSlowPath" + /\ i' = [i EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "TryAcquire"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v_locked, v_sleeping, + v_spinning, v8_locked, v8_sleeping, + weSpin, sleepers, acquisitions, spin >> + +TryAcquire(self) == /\ pc[self] = "TryAcquire" + /\ IF v_locked[self] = TRUE + THEN /\ pc' = [pc EXCEPT ![self] = "SetSleepBit"] + /\ UNCHANGED << l_key_locked, l_key_sleeping, + l_key_spinning >> + ELSE /\ IF weSpin[self] + THEN /\ IF v_locked[self] = l_key_locked + /\ v_sleeping[self] = l_key_sleeping + /\ v_spinning[self] = l_key_spinning + THEN /\ l_key_locked' = TRUE + /\ l_key_sleeping' = TRUE + /\ l_key_spinning' = FALSE + /\ pc' = [pc EXCEPT ![self] = "Locked"] + ELSE /\ pc' = [pc EXCEPT ![self] = "TryAcquireLoop"] + /\ UNCHANGED << l_key_locked, + l_key_sleeping, + l_key_spinning >> + ELSE /\ IF l_key_locked = FALSE + THEN /\ l_key_locked' = TRUE + /\ l_key_sleeping' = TRUE + /\ pc' = [pc EXCEPT ![self] = "Locked"] + ELSE /\ l_key_locked' = TRUE + /\ l_key_sleeping' = TRUE + /\ pc' = [pc EXCEPT ![self] = "TryAcquireLoop"] + /\ UNCHANGED l_key_spinning + /\ UNCHANGED << owner, v_locked, v_sleeping, v_spinning, + v8_locked, v8_sleeping, weSpin, i, + sleepers, acquisitions, spin >> + +TryAcquireLoop(self) == /\ pc[self] = "TryAcquireLoop" + /\ v_locked' = [v_locked EXCEPT ![self] = l_key_locked] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = l_key_sleeping] + /\ v_spinning' = [v_spinning EXCEPT ![self] = l_key_spinning] + /\ pc' = [pc EXCEPT ![self] = "TryAcquire"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v8_locked, v8_sleeping, + weSpin, i, sleepers, acquisitions, + spin >> + +SetSleepBit(self) == /\ pc[self] = "SetSleepBit" + /\ IF v_sleeping[self] = FALSE + THEN /\ l_key_sleeping' = TRUE + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = TRUE] + ELSE /\ TRUE + /\ UNCHANGED << l_key_sleeping, v_sleeping >> + /\ pc' = [pc EXCEPT ![self] = "SetSpinBit"] + /\ UNCHANGED << owner, l_key_locked, l_key_spinning, + v_locked, v_spinning, v8_locked, + v8_sleeping, weSpin, i, sleepers, + acquisitions, spin >> + +SetSpinBit(self) == /\ pc[self] = "SetSpinBit" + /\ IF weSpin[self] = FALSE + THEN /\ weSpin' = [weSpin EXCEPT ![self] = (l_key_spinning = FALSE)] + /\ l_key_spinning' = TRUE + ELSE /\ TRUE + /\ UNCHANGED << l_key_spinning, weSpin >> + /\ pc' = [pc EXCEPT ![self] = "DoSpin"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + v_locked, v_sleeping, v_spinning, + v8_locked, v8_sleeping, i, sleepers, + acquisitions, spin >> + +DoSpin(self) == /\ pc[self] = "DoSpin" + /\ IF weSpin[self] = TRUE + THEN /\ IF i[self] < spin + THEN /\ v_locked' = [v_locked EXCEPT ![self] = l_key_locked] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = l_key_sleeping] + /\ v_spinning' = [v_spinning EXCEPT ![self] = l_key_spinning] + /\ pc' = [pc EXCEPT ![self] = "TryAcquire"] + /\ UNCHANGED << l_key_spinning, weSpin >> + ELSE /\ weSpin' = [weSpin EXCEPT ![self] = FALSE] + /\ l_key_spinning' = FALSE + /\ pc' = [pc EXCEPT ![self] = "Sleep"] + /\ UNCHANGED << v_locked, v_sleeping, + v_spinning >> + ELSE /\ pc' = [pc EXCEPT ![self] = "Sleep"] + /\ UNCHANGED << l_key_spinning, v_locked, + v_sleeping, v_spinning, weSpin >> + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, v8_locked, + v8_sleeping, i, sleepers, acquisitions, spin >> + +Sleep(self) == /\ pc[self] = "Sleep" + /\ v_locked' = [v_locked EXCEPT ![self] = l_key_locked] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = l_key_sleeping] + /\ v_spinning' = [v_spinning EXCEPT ![self] = l_key_spinning] + /\ pc' = [pc EXCEPT ![self] = "Futex"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v8_locked, v8_sleeping, weSpin, + i, sleepers, acquisitions, spin >> + +Futex(self) == /\ pc[self] = "Futex" + /\ IF v_locked[self] = FALSE + THEN /\ pc' = [pc EXCEPT ![self] = "TryAcquire"] + /\ UNCHANGED sleepers + ELSE /\ IF l_key_locked = v_locked[self] + /\ l_key_sleeping = TRUE + THEN /\ sleepers' = (sleepers \union {self}) + ELSE /\ TRUE + /\ UNCHANGED sleepers + /\ pc' = [pc EXCEPT ![self] = "Sleeping"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v_locked, v_sleeping, + v_spinning, v8_locked, v8_sleeping, weSpin, i, + acquisitions, spin >> + +Sleeping(self) == /\ pc[self] = "Sleeping" + /\ self \notin sleepers + /\ i' = [i EXCEPT ![self] = 0] + /\ v_locked' = [v_locked EXCEPT ![self] = l_key_locked] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = l_key_sleeping] + /\ v_spinning' = [v_spinning EXCEPT ![self] = l_key_spinning] + /\ pc' = [pc EXCEPT ![self] = "TryAcquire"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v8_locked, v8_sleeping, + weSpin, sleepers, acquisitions, spin >> + +Locked(self) == /\ pc[self] = "Locked" + /\ owner' = self + /\ pc' = [pc EXCEPT ![self] = "CriticalSection"] + /\ UNCHANGED << l_key_locked, l_key_sleeping, l_key_spinning, + v_locked, v_sleeping, v_spinning, v8_locked, + v8_sleeping, weSpin, i, sleepers, acquisitions, + spin >> + +CriticalSection(self) == /\ pc[self] = "CriticalSection" + /\ acquisitions' = acquisitions + 1 + /\ pc' = [pc EXCEPT ![self] = "Unlock"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v_locked, v_sleeping, + v_spinning, v8_locked, v8_sleeping, + weSpin, i, sleepers, spin >> + +Unlock(self) == /\ pc[self] = "Unlock" + /\ owner' = NULL + /\ v8_locked' = [v8_locked EXCEPT ![self] = l_key_locked] + /\ v8_sleeping' = [v8_sleeping EXCEPT ![self] = l_key_sleeping] + /\ l_key_locked' = FALSE + /\ l_key_sleeping' = FALSE + /\ IF v8_sleeping'[self] = TRUE + THEN /\ pc' = [pc EXCEPT ![self] = "Wakeup"] + ELSE /\ pc' = [pc EXCEPT ![self] = "NonCriticalSection"] + /\ UNCHANGED << l_key_spinning, v_locked, v_sleeping, + v_spinning, weSpin, i, sleepers, acquisitions, + spin >> + +Wakeup(self) == /\ pc[self] = "Wakeup" + /\ v_locked' = [v_locked EXCEPT ![self] = l_key_locked] + /\ v_sleeping' = [v_sleeping EXCEPT ![self] = l_key_sleeping] + /\ v_spinning' = [v_spinning EXCEPT ![self] = l_key_spinning] + /\ pc' = [pc EXCEPT ![self] = "Wake2"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v8_locked, v8_sleeping, weSpin, + i, sleepers, acquisitions, spin >> + +Wake2(self) == /\ pc[self] = "Wake2" + /\ IF v_spinning[self] = FALSE + THEN /\ IF Cardinality(sleepers) > 0 + THEN /\ IF WakeAny + THEN /\ LET other == CHOOSE other \in sleepers: TRUE IN + sleepers' = sleepers \ {other} + ELSE /\ \E other \in sleepers: + sleepers' = sleepers \ {other} + ELSE /\ TRUE + /\ UNCHANGED sleepers + ELSE /\ TRUE + /\ UNCHANGED sleepers + /\ pc' = [pc EXCEPT ![self] = "NonCriticalSection"] + /\ UNCHANGED << owner, l_key_locked, l_key_sleeping, + l_key_spinning, v_locked, v_sleeping, + v_spinning, v8_locked, v8_sleeping, weSpin, i, + acquisitions, spin >> + +thread(self) == NonCriticalSection(self) \/ SpeculativeGrab(self) + \/ SpeculativeGrabCheck(self) \/ EnterSlowPath(self) + \/ TryAcquire(self) \/ TryAcquireLoop(self) + \/ SetSleepBit(self) \/ SetSpinBit(self) \/ DoSpin(self) + \/ Sleep(self) \/ Futex(self) \/ Sleeping(self) + \/ Locked(self) \/ CriticalSection(self) \/ Unlock(self) + \/ Wakeup(self) \/ Wake2(self) + +(* Allow infinite stuttering to prevent deadlock on termination. *) +Terminating == /\ \A self \in ProcSet: pc[self] = "Done" + /\ UNCHANGED vars + +Next == (\E self \in Threads: thread(self)) + \/ Terminating + +Spec == /\ Init /\ [][Next]_vars + /\ \A self \in Threads : WF_vars(thread(self)) + +Termination == <>(\A self \in ProcSet: pc[self] = "Done") + +\* END TRANSLATION + +============================================================================= +\* Modification History +\* Last modified Tue Oct 01 13:18:42 PDT 2024 by rhysh +\* Created Tue Sep 17 12:10:43 PDT 2024 by rhysh |