Город: Санкт-Петербург Новосибирск Казань Язык: Русский English

Слабые модели памяти
Санкт-Петербург / весна 2020, посмотреть все семестры

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

Современные компиляторы и процессоры являются оптимизирующими. Из-за этого поведение многопоточных программ не может быть полностью описано моделью памяти последовательной консистентности [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].