On compilation correctness for a subset of a promising memory model to the ARMv8.3 memory model

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