Город: Санкт-Петербург Новосибирск Казань Язык: Русский 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].

Дата и время Название Место Материалы
22 марта
11:15–12:45
Лекция 1. Слабые модели памяти: почему и кому нужно, лекция ПОМИ РАН Нет
22 марта
13:00–14:30
Лекция 2. Декларативные модели памяти, лекция ПОМИ РАН Нет
29 марта
11:15–12:45
Лекция 3. Обещающая семантика, лекция ПОМИ РАН Нет
29 марта
13:00–14:30
Лекция 4. Корректность компиляции для слабых моделей памяти, лекция ПОМИ РАН Нет