/
githubmirror
/
julia
Обзор
Документация
Войти
/
githubmirror
/
julia
Код
Запросы
0
Пакеты
0
Релизы
0
Аналитика
Безопасность
master
doc/src/devdocs/scheduler-wakeup/MCFixed.tla
17 строк
864 B
Ian Butterworth
scheduler: avoid O(nthreads) wake-storm on every `@spawn` (#61826)
06 июн 2026, 04:08
Не верифицирован
06 июн 2026, 04:08
a8f97b1
Код
Авторство
О чём код?
------------------------------- MODULE MCFixed ------------------------------- (* Concrete instance for TLC: the shipped wake-one algorithm that always scans *) (* each worker's sleep_check_state. TLC reports no deadlock and NoLostWakeup *) (* holds across the full state space. *) (* *) (* Two workers share pool B (plus a producer in A) so the model checker can *) (* exercise wake-one against multiple sleepers, including cross-pool inserts. *) EXTENDS Naturals, FiniteSets, TLC Threads == {1, 2, 3} Pool == (1 :> "A") @@ (2 :> "B") @@ (3 :> "B") Inject0 == ("A" :> 0) @@ ("B" :> 2) VARIABLES st, pc, nrun, queue, inject INSTANCE SchedulerWake =============================================================================