Сборники трудов ИСП РАН


Обещающая компиляция в ARMv8.3

Подкопаев А.В. (СПбГУ, Санкт-Петербург, Россия; JetBrains Research, Санкт-Петербург, Россия)
Лахав О. (ТАУ, Тель-Авив, Израиль)
Вафеядис В. (ИМП, Кайзерслаутерн, Германия)

Аннотация

Поведение многопоточных программ не может быть промоделировано попеременным последовательным исполнением различных потоков на одном вычислительном узле. На данный момент полное и корректное описание поведения многопоточных программ является открытой теоретической проблемой. Одним из перспективных  решений этой проблемы является „обещающая“ модель памяти. Для того, чтобы некоторая модель могла быть использована в стандарте некоторого промышленного языка программирования, должна быть доказана корректность компиляции из этой модели в модель памяти целевой процессорной архитектуры. Данная статья представляет доказательство корректности компиляции из подмножества обещающей модели в модели памяти процессора  ARMv8.3. Главной идеей доказательства является введение промежуточного операционного варианта модели ARMv8.3, поведение которого может быть симулировано обещающей моделью.

Ключевые слова

многопоточность; корректность компиляции; слабые модели памяти

Издание

Труды Института системного программирования РАН, том 29, вып. 5, 2017, стр. 149-164.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(5)-9

Полный текст статьи в формате pdf Вернуться к содержанию тома