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

Современные процессоры обладают слабыми моделями памяти. В большинстве случаев семантика программ для таких процессоров описывается аксиоматически как набор графов с заданными свойствами. Однако, возможно и операционное описание. В докладе будет освещена операционная модель памяти процессора ARMv8 [1], обладающего очень слабой моделью памяти. Также будет показано, как можно инструментировать модель для упрощения доказательств корректности компиляции из более высокоуровневой модели [2].

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

[1] http://www.cl.cam.ac.uk/~sf502/popl16/index.html

[2] http://sf.snu.ac.kr/promise-concurrency/

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