Исследовательская группа

Лаборатория языковых инструментов

Корректность компиляции из "обещающей" модели в модель ARMv8

February 27

Доклад посвящен доказательству корректности компиляции для подмножества "обещающей" семантики Kang el al. в модель процессора ARMv8 Flur et al.

Докладчик: Антон Подкопаев.

Материалы к докладу:

J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. A promising semantics for relaxed-memory concurrency. POPL 2017.

S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget, W. Deacon, and P. Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. POPL 2016.