![](data:image/svg+xml;charset=utf-8,<svg width="640" height="640" style="background-color:%2344badc;font-family:Nunito,sans-serif" viewBox="0 0 100 100" preserveAspectRatio="xMidYMid meet" xmlns="http://www.w3.org/2000/svg">
<text font-size="30" x="50%" y="50%" dy="5" fill="white" dominant-baseline="middle" text-anchor="middle">A4</text>
</svg>)
Я для себя выделяю два типа модел чекинга: stateful и stateless.
С первым все понятно: храним состояния явно, не посещаем их повторно.
Со вторым интереснее. Состояния не хранятся явно, поэтому нужны техники, которые позволили бы не посещать повторные состояния. Даже не состояния, а целые траектории.
Есть POR, но для рантайма эти техники сложны - нужно статически анализировать программу. Знать, что поток предпримет в будущем.
Поэтому есть другая крутая техника, специально для stateless runtime-а - DPOR.
https://users.soe.ucsc.edu/~cormac/papers/popl05.pdf
Ее суть - это наблюдение, что две траектории могут привести в один стейт. Какие траектории обладают таким свойством? А те, в которых действия независимы - т.е. неформально - конечное состояние не зависит от порядка применения этих действий.
Чтобы эту инфу трекать прямо в рантайме, DPOR не анализирует ничего сразу же - он трекает точки динамически. Т.е. запускает как попало программу, и по дороге делает бэктрекинг: берет потенциальное действие из текущего стейта, и находит действие в прошлом, с которым это действие зависимо. Только такие нам и интересны. Дальше запоминает это, и позже (обход дфс) попытается "свапнуть" действия. Пример - лоад и стор одного атомика.
Реализация такой техники - это векторные часы. Прямо как в тсане!
Самое крутое, что это не теоретическая забава. Ее реально применяют, например Rust по мотивам написал чекер (loom), который еще и слабые атомики поддерживает (векторные часы же!):
https://github.com/tokio-rs/loom
А вот реальное применение loom - тестирование планировщика из tokio:
https://tokio.rs/blog/2019-10-scheduler/
#dpor #rust #loom #model_checking #scheduler #tokio
С первым все понятно: храним состояния явно, не посещаем их повторно.
Со вторым интереснее. Состояния не хранятся явно, поэтому нужны техники, которые позволили бы не посещать повторные состояния. Даже не состояния, а целые траектории.
Есть POR, но для рантайма эти техники сложны - нужно статически анализировать программу. Знать, что поток предпримет в будущем.
Поэтому есть другая крутая техника, специально для stateless runtime-а - DPOR.
https://users.soe.ucsc.edu/~cormac/papers/popl05.pdf
Ее суть - это наблюдение, что две траектории могут привести в один стейт. Какие траектории обладают таким свойством? А те, в которых действия независимы - т.е. неформально - конечное состояние не зависит от порядка применения этих действий.
Чтобы эту инфу трекать прямо в рантайме, DPOR не анализирует ничего сразу же - он трекает точки динамически. Т.е. запускает как попало программу, и по дороге делает бэктрекинг: берет потенциальное действие из текущего стейта, и находит действие в прошлом, с которым это действие зависимо. Только такие нам и интересны. Дальше запоминает это, и позже (обход дфс) попытается "свапнуть" действия. Пример - лоад и стор одного атомика.
Реализация такой техники - это векторные часы. Прямо как в тсане!
Самое крутое, что это не теоретическая забава. Ее реально применяют, например Rust по мотивам написал чекер (loom), который еще и слабые атомики поддерживает (векторные часы же!):
https://github.com/tokio-rs/loom
А вот реальное применение loom - тестирование планировщика из tokio:
https://tokio.rs/blog/2019-10-scheduler/
#dpor #rust #loom #model_checking #scheduler #tokio