JetBrains Research — наука, меняющая мир

Семинар по операционной модели памяти процессора ARMv8

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

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

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

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

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

28.11.2016, 17:15, Мат-Мех, ауд. 3248.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28