195251, Санкт-Петербург,
Политехническая ул., 29, НИК, к. В.3.17
+7 (812) 552-6216 (с 10 до 17.30 )
infocom@spbstu.ru

Вафеядис Виктор

Подкопаев А.В., Лахав О., Вафеядис В.

О корректности компиляции подмножествa обещающей модели памяти в аксиоматическую модель ARMv8.3

Опубликовано в разделе «Программное обеспечение вычислительных, телекоммуникационных и управляющих систем»

«Обещающая» модель памяти является перспективным решением проблемы задания семантики многопоточности в контексте императивных языков программирования, таких как С/C++ и Java. Естественным требованием, которое ставится перед моделью памяти языка программирования, является наличие эффективной и корректной схемы компиляции для распространенных процессорных архитектур. Ранее для обещающей модели была показана корректность компиляции в архитектуры x86, Power и для операционной модели памяти ARMv8 POP. В статье приведено доказательство корректности компиляции в аксиоматическую модель ARMv8.3. В доказательстве использован новый метод обхода исполнений аксиоматических моделей памяти. Этот метод является более общим, чем использованные ранее подходы, и может использоваться в последующих доказательствах корректности компиляции из обещающей модели памяти.

Ссылка при цитировании: Подкопаев А.В., Лахав О., Вафеядис В. О корректности компиляции подмножествa обещающей модели памяти в аксиоматическую модель ARMv8.3 // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 2017. Т. 10. № 4. С. 51–69. DOI: 10.18721/JCSTCS.10405

Просмотров: 393 Комментариев: 0