JetBrains Research — наука, меняющая мир

Гарантии прогресса в слабых моделях памяти

Доказательства свойств прогресса (liveness) многопоточных программ часто опираются на "справедливость" планировщика, то есть гарантию того, что каждый активный поток рано или поздно будет выбран для исполнения. Однако при исполнении в слабых моделях памяти этого требования оказывается недостаточно; в частности, для обеспечения завершения необходимо накладывать дополнительное условие "справедливости по памяти". В докладе мы рассмотрим, как введение такого условия меняет определения распространённых моделей. Кроме того, мы покажем, что для декларативных моделей справедливость по памяти определяется единообразно, и используем полученное определение для доказательства завершения спинлоков.

Докладчик: Егор Намаконов

Семинар пройдет онлайн 30 ноября в 17:30, ссылка Google meet: https://meet.google.com/myu-dhmz-gvu