City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Weak memory models
Saint Petersburg / spring 2020, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

Современные компиляторы и процессоры являются оптимизирующими. Из-за этого поведение многопоточных программ не может быть полностью описано моделью памяти последовательной консистентности [Lamport:TC79], т.е. как поочередное исполение потоков на одном процессоре (ядре). Модели памяти, описывающие такое поведение программ, называются слабыми. Слабыми являются модели памяти как процессорных архитектур (x86, Power, ARM, SPARC, DEC Alpha), так и для языков программирования (C/C++, Java, OCaml).

Первая лекция курса начнется с рассмотрения примеров слабого поведения программ. Далее будут обсуждены требования к языковым и процессорным моделям памяти, а также особенности и недостатки существующих моделей.

Вторая лекция курса посвящена декларативным (аксиоматическим) моделям памяти. Будет рассмотрены соответствующий формализм и существующие декларативные модели (x86-TSO [Sewell-al:CACM10], C/C++11 MM [Batty-al:POPL11], ARMv8.3 MM [Pulte-al:POPL18], OCaml MM [Dolan-al:PLDI18], JavaScript MM), а также проблема доказательства корректности компиляции между ними.

В третьей лекции будет рассмотрена обещающая модель памяти (Promising semantics, [Kang-al:POPL17]), являющаяся перспективной попыткой решить проблемы C/C++11 MM.

Четвертая лекция посвящена доказательству корректности компиляции из обещающей модели памяти в модели памяти процессорных архитектур с использованием промежуточной модели памяти (IMM) [Podkopaev-al:POPL19].