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

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

Локальная свобода от гонок

March 5

Современные компиляторы и аппаратные архитектуры производят агрессивные оптимизации кода. Эффекты этих оптимизаций не влияют на семантику однопоточных программ, однако в многопоточной среде могут приводить к неожиданным поведениям.Модели памяти, в которых можно наблюдать такие поведения, называются слабыми.Рассуждать о программах, имеющих слабые поведения, может быть затруднительно для рядовых разработчиков. По этой причине многие слабые модели памяти предоставляют так называемую DRF гарантию (data-race free guarantee). DRF гарантия означает, что если программа не имеет гонок в SC модели памяти, то она не имеет слабых поведений в данной модели памяти.К сожалению, такое определение DRF гарантии глобально: одна единственная гонка в программе полностью нарушает гарантию. В докладе будет рассмотрена более сильная локальная DRF гарантия (local data-race free guarantee), а также модель памяти, которая предоставляет данную гарантию.

Материалы к докладу:

Stephen Dolan, KC Sivaramakrishnan, Anil Madhavapeddy. Bounding Data Races in Space and Time // PLDI 2018.

Докладчик: Евгений Моисеенко