Диссертация (1149932)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Санкт-Петербургский государственный университетНа правах рукописиПодкопаев Антон ВикторовичОПЕРАЦИОННЫЕ МЕТОДЫ В ПРИЛОЖЕНИИ К СЛАБЫММОДЕЛЯМ ПАМЯТИСпециальность 05.13.11 —«Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей»Диссертация на соискание учёной степеникандидата физико-математических наукНаучный руководитель:доктор технических наук, доцент, профессор кафедры системногопрограммированияКОЗНОВ Дмитрий ВладимировичСанкт-Петербург — 20182СодержаниеСтр.Введение . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Глава 1. Обзор предметной области . . . . . . . . . . . . . . . . .1.1 Модели памяти и слабые сценарии поведения . . . . . . .1.2 Требования к моделям памяти . . . . . . . . . . . . . . . .1.2.1 Корректность компиляторных оптимизаций . . . .1.2.2 Наличие эффективной схемы компиляции . . . . .1.2.3 Гарантии программисту . .

. . . . . . . . . . . . .1.3 Существующие модели памяти языков программирования1.3.1 Виды моделей памяти . . . . . . . . . . . . . . . . .1.3.2 Модель памяти Java . . . . . . . . . . . . . . . . . .1.3.3 Модель памяти C/C++ . . . . . . . . . . . . . . . .1.3.4 Теоретические модели памяти . . . . . . . . .

. . .1.4 Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . .............6................................................121214151719202121243032Глава 2. Операционная модель памяти C/C++11 . . . . . . . . . . .2.1 Основные понятия . . . . . . . . . . . . .

. . . . . . . . . . . .2.1.1 Память и базовый фронт . . . . . . . . . . . . . . . . .2.1.2 Синхронизация потоков . . . . . . . . . . . . . . . . .2.1.3 Операционные буфера . . . . . . . . . . . . . . . . . .2.1.4 Спекулятивное исполнение . . . . . . . . .

. . . . . . .2.1.5 sc-инструкции . . . . . . . . . . . . . . . . . . . . . .2.1.6 Неатомарные обращения . . . . . . . . . . . . . . . . .2.1.7 Потребляющие чтения . . . . . . . . . . . . . . . . . .2.1.8 Соединение потоков . . . . . . . . . . . . . . . . . . .2.1.9 Расслабленные обращения и синхронизация . . . . .

.2.2 Формальное описание модели . . . . . . . . . . . . . . . . . .2.2.1 Синтаксис языка модели и базовые правила редукции .2.2.2 Представление памяти и фронтов . . . . . . . . . . . .2.2.3 Высвобождающие и приобретающие обращения . . .2.2.4 sc-инструкции . . . . . .

. . . . . . . . . . . . . . . .2.2.5 Неатомарные обращения . . . . . . . . . . . . . . . . ....................................................33333335363739404142434646485051523Стр.2.2.62.32.4Потребляющие чтения . . . . . . . . . . . . . . . . . . . . . 542.2.7 Расслабленные обращения . . . .

. . . . . . . . . . .2.2.8 Отложенные операции и спекулятивное исполнение .Интерпретация и тестирование модели . . . . . . . . . . . .2.3.1 “Лакмусовые” тесты . . . . . . . . . . . . . . . . . .2.3.2 Проверка модели на примере RCU-структуры . . . .Выводы . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . .........................555658596268Глава 3. Корректность компиляции из обещающей модели воперационную модель ARMv8 POP . . . . . . . . . . .3.1 Мотивация доказательства корректности компиляции . . .3.2 Описание моделей на примерах . . . .

. . . . . . . . . . .3.2.1 Модель ARMv8 POP . . . . . . . . . . . . . . . . .3.2.2 Абстрактная подсистема памяти: POP . . . . . . . .3.2.3 Обещающая модель . . . . . . . . . . . . . . . . . .3.3 Основные идеи доказательства корректности компиляции .3.4 Формальное определение модели ARMv8 POP . . . . . . .3.5 Формальное определение обещающей модели . .

. . . . .3.6 Промежуточная машина ARM+τ . . . . . . . . . . . . . . .3.6.1 Свойства подсистемы памяти модели ARMv8 POP3.6.2 Модель ARMv8 POP и метки времени . . . . . . . .3.6.3 Определение машины ARM+τ . . . . . . . . . . . .3.6.4 Симуляция модели ARMv8 POP . . . . . . . . . . .3.6.5 Фронты машины ARM+τ .

. . . . . . . . . . . . . .3.7 Доказательство корректности компиляции . . . . . . . . .3.8 Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . ......................................................................................69697071737882859295969899102104106111Глава 4. Корректность компиляции из обещающей модели ваксиоматическую модель ARMv8.3 . .

. . . . . . . . .4.1 Модель ARMv8.3 . . . . . . . . . . . . . . . . . . . . . .4.2 Структура доказательства корректности компиляции . .4.3 Обход ARM-согласованного сценария . . . . . . . . . . .4.4 Аналоги фронтов для ARM-согласованного сценария . .4.5 Доказательство корректности компиляции .

. . . . . . ...............................112113116117121122......4Стр.4.6Выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124Заключение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126Список сокращений и условных обозначений . . . . . . . .

. . . . . . . . 127Список литературы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128Список рисунков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140Список таблиц . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . 142Приложение А. Каталог тестов для модели C/C++11 . .А.1 Буферизация записи, SB . . . . . . . . . . . . . . .А.2 Буферизация чтения, LB . . . . . . . . . . . . . .А.3 Передача сообщения, MP . . . . . . . . . . . . . .А.4 Корректность повторного чтения, CoRR . . . . . .А.5 Независимые чтения независимых записей, IRIWА.6 Зависимость запись-чтение, WRC . . . . . . . . .А.7 “Значения из воздуха”, OOTA . .

. . . . . . . . .А.8 Независимые записи, WR . . . . . . . . . . . . . .А.9 Спекулятивное исполнение, SE . . . . . . . . . . .А.10 ARM-weak . . . . . . . . . . . . . . . . . . . . . .А.11 Блокировки . . . . . . . . . . . . . . . . . . . . . .........................................................................................................................143143144147150150151153153154156156Приложение Б. Правила переходов и вспомогательные функциимашины ARMv8 POP . . .

. . . . . . . . . . . . . . . . . 158Приложение В. Доказательство вспомогательных лемм о симуляциимодели ARM+τ . . . . . . . . . . . . . . . . . . . . . . .В.1 Базовые леммы . . . . . . . . . . . . . . . . . . . . . . . . . . . . .В.2 Сертификация . . . . .

. . . . . . . . . . . . . . . . . . . . . . . .В.2.1 Структура доказательства теоремы о сертификации . . . .В.2.2 Описание вспомогательного отношения . . . . . . . . . .В.2.3 Доказательство лемм и теоремы о сертификации . . . . .......1631631691691711735Стр.Приложение Г. Представление программ . . . . . . . . . . . . . . . . . . 179Г.1Г.2Г.3Помеченная система переходов . . . . . . . .

. . . . . . . . . . . . . 179Предзапуски . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180Связь между системой переходов и предзапусками . . . . . . . . . . 182Приложение Д. Доказательство леммы о шаге симуляцииобещающей модели и обхода сценария ARMv8.3 . . . . . 1846ВведениеАктуальность темы. Многопоточные программы являются источникамиспецифических, трудно обнаружимых ошибок, таких как состояние гонки, взаимная блокировка и др. Эти ошибки могут воспроизводиться очень редко, например,в одном из 10 тысяч запусков программы, однако даже это может быть критично.В связи с этим необходимо иметь специализированные методы для анализа многопоточных программ.

Ключевым аспектом любого анализа программ являетсяналичие хорошо определенной семантики языка программирования. Семантикиязыков программирования и систем (процессоров) с многопоточностью называютмоделями памяти (memory model, MM).Наиболее простой и естественной моделью памяти является последовательная консистентность (sequential consistency, SC) [1]; она подразумевает, что каждый сценарий поведения многопоточной программы может быть получен некоторым поочередным исполнением команд её потоков на одном ядре (процессоре).Однако эта модель не способна описать все сценарии поведения, встречаемые напрактике.

Сценарии поведения, которые не могут быть описаны моделью SC, называются слабыми.Слабыми сценариями поведения обладают некоторые многопоточные программы с неблокирующей синхронизацией потоков. Это является следствием обработки программ оптимизирующими компиляторами и их исполнением на суперскалярных процессорах. Поскольку алгоритмы на базе неблокирующей синхронизации всё чаще используются при разработке важных и высокопроизводительных систем, таких как ядро Linux и системы управления базами данных, тослабые сценарии поведения требуют тщательного изучения.Модели памяти, допускающие слабые сценарии поведения программ, называются слабыми (weak memory models) [2].

На данный момент научное сообщество в тесном сотрудничестве с индустрией разработало и продолжает совершенствовать множество таких моделей для языков программирования и процессорных архитектур. При этом процессорные и языковые модели существенно влияют на друг друга. Так, модель процессора должна отражать сценарии поведения,наблюдаемые при запуске программ на существующих процессорах, и оставлятьвозможности для развития обратно совместимых архитектур. В то же время, языковая модель должна предоставлять разумные и удобные абстракции для программиста, а также допускать основные компиляторные оптимизации и быть совме-7стимой с моделям целевых архитектур, т.е.

поддерживать эффективную трансляцию в низкоуровневый код без изменения семантики программы.Существующие модели памяти для наиболее популярных языков программирования обладают рядом недостатков. Так, известно, что модель памятиJava [3] некорректна по отношению к базовым оптимизациям, а модель памяти C/С++11 [4] разрешает сценарии поведения программ, в которых появляются“значения из воздуха” (out-of-thin-air values) [5]. Модель памяти имеет проблему“значений из воздуха”, если для программы без арифметики, в которой явнымобразом не встречается некоторая константа, (например, 42) допустим сценарийповедения, в котором эта константа появляется (например, записывается в памятьили читается из памяти). Такие сценарии не проявляются на практике, но тот факт,что модель C/C++11 их допускает, не позволяет формально доказывать многие полезные свойства программ в рамках этой модели.

Наличие проблемы “значений извоздуха” связано с тем, что модель C/C++11 задана декларативно (аксиоматически), при этом сценарий поведения программы в рамках модели определяется какнекоторая монолитная структура (граф), а не как последовательность действийнекоторой абстрактной машины. Это оставляет открытым вопрос об интеграциимодели с остальными компонентами языка, которые в стандарте C/C++11 определены операционно.Таким образом, для развития инструментов анализа многопоточных программ необходимо разработать операционные подходы к заданию слабых моделей памяти.Степень разработанности темы. С 1990-х годов велась работа по разработке семантики многопоточности с учетом слабых сценариев поведения. Формальные модели для наиболее распространенных процессорных архитектур (x86,Power, ARM) были разработаны J.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов диссертации