Исследовательская группа

Лаборатория языковых инструментов

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

December 7

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

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

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

Материалы