С 17 марта 2020 г. для ресурсов (учебные, научные, материалы конференций, статьи из периодических изданий, авторефераты диссертаций, диссертации) ЭБ СПбПУ, обеспечивающих образовательный процесс, установлен особый режим использования. Обращаем внимание, что ВКР/НД не относятся к этой категории.

Детальная информация

Название: О корректности компиляции подмножества обещающей модели памяти в аксиоматическую модель ARMv8.3 // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Сер.: Информатика. Телекоммуникации. Управление: научное издание. – 2017. – Т. 10, № 4
Авторы: Подкопаев Антон Викторович; Лахав Ори; Вафеядис Виктор
Организация: Санкт-Петербургский государственный университет телекоммуникаций имени профессора М. А. Бонч-Бруевича; Тель-Авивский университет; Институт имени Макса Планка
Выходные сведения: Санкт-Петербург: Изд-во Политехн. ун-та, 2017
Коллекция: Общая коллекция
Тематика: Вычислительная техника; Языки программирования; корректность компиляции; аксиоматические модели; модели памяти (вычислительная техника); семантика; многопоточные программы; compilation correctness; axiomatic models; memory models (computer engineering); semantics; multithreaded programs
УДК: 004.43
ББК: 32.973-018.1
Тип документа: Статья, доклад
Язык: Русский
DOI: 10.18721/JCSTCS.10405
Права доступа: Свободный доступ из сети Интернет (чтение, печать, копирование)

Разрешенные действия: Прочитать

Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети

Группа: Анонимные пользователи

Сеть: Интернет

Аннотация

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

A "promising" memory model is an auspicious solution to the problem of defining semantics for an imperative language with concurrency, such as C/C++ or Java. An essential requirement for such a memory model is the existence of an effective and correct compilation scheme from the language to its target platforms. There are compilation correctness proofs from the promising model to x86 and Power as well as to an operational model ARMv8 POP. This paper presents such proof for an axiomatic memory model for ARMv8.3. In the proof, we use a new method of execution traversal, which might be used in other compilation correctness proofs for the promising memory model.

Права на использование объекта хранения

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все Прочитать Печать Загрузить
Интернет Авторизованные пользователи Прочитать Печать Загрузить
-> Интернет Анонимные пользователи Прочитать

Статистика использования

stat Количество обращений: 101
За последние 30 дней: 2
Подробная статистика