Исследовательская группа
Лаборатория языковых инструментов
Операционная модель памяти процессора ARMv8
28 ноября
Современные процессоры обладают слабыми моделями памяти. В большинстве случаев семантика программ для таких процессоров описывается аксиоматически как набор графов с заданными свойствами. Однако, возможно и операционное описание. В докладе будет освещена операционная модель памяти процессора ARMv8 [1], обладающего очень слабой моделью памяти. Также будет показано, как можно инструментировать модель для упрощения доказательств корректности компиляции из более высокоуровневой модели [2].
Материалы к докладу:
[1] http://www.cl.cam.ac.uk/~sf502/popl16/index.html
[2] http://sf.snu.ac.kr/promise-concurrency/
Докладчик: Антон Подкопаев