Исследования
Лаборатория языковых инструментов
IMM: правильность компиляции для ослабленных моделей памяти
Фреймворк IMM упрощает подтверждение правильности компиляции из моделей памяти языка программирования (например, Promising и Weakestmo) в модели аппаратной памяти (например, x86, Power, Arm и RISC-V). Фреймворк механизирован в Coq.
Мы разрабатываем промежуточную слабую модель памяти (IMM) как способ модульной организации подтверждения правильности компиляции из параллельных языков программирования с семантикой согласованности ослабленной памяти в общепринятые многоядерные архитектуры, такие как POWER и ARM. Мы используем IMM для подтверждения правильности компиляции из различных новых моделей памяти языков программирования (в основном предназначенных для решения проблемы «значений из воздуха») в аппаратные модели памяти, такие как POWER, ARMv7, ARMv8, RISC-V и x86-TSO. Полученные результаты механизированы в Coq и, насколько нам известно, являются первыми машинно проверенными результатами проверки корректности компиляции для моделей слабее x86-TSO.
