What: | Lecture |
When: | Sunday, 11 October 2020, 22:00–00:00 |
Where: | Конференция в zoom, Онлайн |
Использование компиляторных и процессорных оптимизаций приводит к тому, что современные языки программирования не гарантируют модель памяти последовательной консистентности (sequential consistency, SC, [Lamport:TC79]) для многопоточных программ. Вместо этого, такие языки обладают слабыми моделями памяти, допускающими больше возможных результатов исполнения программ. Такие модели памяти балансируют между производительностью, как следствие свободы, предоставляемой компилятору и процессору, и гарантиями на разумность
поведения программы, предоставляемыми программисту.
В этом докладе вводятся слабые модели памяти, рассматриваются требования к моделям памяти языков программирования, а также обсуждаются достоинства и недостатки моделей, используемых в индустрии (C/C++11 [Batty-al:POPL11] и Java [Manson-al:POPL05]). Далее рассматриваются новые модели памяти (RC11 [Lahav-al:PLDI17], MRD [Paviotti-al:ESOP20], Promising 1.0 [Kang-al:POPL17], Promising 2.0 [Hwan-al:PLDI20], Weakestmo [Chakraborty-Vafeiadis:POPL19]), призванные решить упомянутые недостатки. В заключении обсуждается то, как стоит подходить к выбору и/или модификации модели памяти для языка программирования или виртуальной машины.
Целевая аудитория:
интересующиеся низкоуровневым многопоточным программированием;
разработчики языков и виртуальных машин.
Основные идеи доклада:
Модели памяти популярных языков (C/C++ и Java) имеют существенные недостатки.
Существуют модели без них, но с разными компромиссами.
Предлагается способ подбора или модификации модели памяти под требования языка и/или виртуальной машины.