Автореферат (1149930)
Текст из файла
На правах рукописиПодкопаев Антон ВикторовичОПЕРАЦИОННЫЕ МЕТОДЫ В ПРИЛОЖЕНИИ КСЛАБЫМ МОДЕЛЯМ ПАМЯТИСпециальность 05.13.11 ––«Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей»Авторефератдиссертации на соискание учёной степеникандидата физико-математических наукСанкт-Петербург — 2018Работа выполнена на кафедре системногоПетербургского государственного университета.программированияСанкт-Научный руководитель:КОЗНОВ Дмитрий Владимирович, доктор технических наук, доцент, профессор кафедры системного программированияОфициальные оппоненты:ГЕРГЕЛЬ Виктор Павлович,доктор технических наук, профессор,Федеральное государственное автономное образовательное учреждение высшего образования «Нижегородский государственный университет им.Н.И.
Лобачевского»,директор института информационных технологий,математики и механики, заведующий кафедройпрограммной инженерииЛУКАШИН Алексей Андреевич,кандидат технических наук,Федеральное государственное автономное образовательное учреждение высшего образования«Санкт-Петербургский политехнический университет Петра Великого»,доцент кафедры «Телематика (при ЦНИИ РТК)»института прикладной математики и механикиВедущая организация:Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук (ИСП РАН)Защита состоится 17 мая 2018 г. в 15 часов на заседании диссертационного совета Д 212.232.51 на базе Санкт-Петербургского государственного университета по адресу: 198504, Санкт-Петербург, Старый Петергоф, Университетский пр.28, математико-механический факультет СПбГУ, ауд.
405.С диссертацией можно ознакомиться в библиотеке Санкт-Петербургского государственного университета по адресу: 199034, Санкт-Петербург, Университетская наб., д. 7/9, а также на сайте СПбГУ: http://spbu.ru/science/disser/.Автореферат разослан __ __________ 20__ года.Ученый секретарьдиссертационного советаД 212.232.51,д.ф.-м.н., профессорДемьянович Юрий КазимировичОбщая характеристика работыАктуальность темы. Многопоточные программы являются источникамиспецифических, трудно обнаружимых ошибок, таких как состояние гонки, взаимная блокировка и др. Эти ошибки могут воспроизводиться очень редко, например, в одном из 10 тысяч запусков программы, однако даже это может быть критично. В связи с этим необходимо иметь специализированные методы для анализа многопоточных программ.
Ключевым аспектом любого анализа программ является наличие хорошо определенной семантики языка программирования. Семантики языков программирования и систем (процессоров) с многопоточностьюназывают моделями памяти (memory model, MM).Наиболее простой и естественной моделью памяти является последовательная консистентность (sequential consistency, SC); она подразумевает, чтокаждый сценарий поведения многопоточной программы может быть полученнекоторым поочередным исполнением команд её потоков на одном ядре (процессоре).
Однако эта модель не способна описать все сценарии поведения, встречаемые на практике. Сценарии поведения, которые не могут быть описаны модельюSC, называются слабыми.Слабыми сценариями поведения обладают некоторые многопоточные программы с неблокирующей синхронизацией потоков. Это является следствием обработки программ оптимизирующими компиляторами и их исполнением на суперскалярных процессорах.
Поскольку алгоритмы на базе неблокирующей синхронизации всё чаще используются при разработке важных и высокопроизводительных систем, таких как ядро Linux и системы управления базами данных, тослабые сценарии поведения требуют тщательного изучения.Модели памяти, допускающие слабые сценарии поведения программ, называются слабыми (weak memory models).
На данный момент научное сообщество в тесном сотрудничестве с индустрией разработало и продолжает совершенствовать множество таких моделей для языков программирования и процессорных архитектур. При этом процессорные и языковые модели существенновлияют на друг друга. Так, модель процессора должна отражать сценарии поведения, наблюдаемые при запуске программ на существующих процессорах, иоставлять возможности для развития обратно совместимых архитектур. В то жевремя, языковая модель должна предоставлять разумные и удобные абстракциидля программиста, а также допускать основные компиляторные оптимизации ибыть совместимой с моделям целевых архитектур, т.е.
поддерживать эффективную трансляцию в низкоуровневый код без изменения семантики программы.Существующие модели памяти для наиболее популярных языков программирования обладают рядом недостатков. Так, известно, что модель памяти Javaнекорректна по отношению к базовым оптимизациям, а модель памяти C/С++11разрешает сценарии поведения программ, в которых появляются “значения извоздуха” (out-of-thin-air values).
Модель памяти имеет проблему “значений извоздуха”, если для программы без арифметики, в которой явным образом не3встречается некоторая константа, (например, 42) допустим сценарий поведения,в котором эта константа появляется (например, записывается в память или читается из памяти). Такие сценарии не проявляются на практике, но тот факт, чтомодель C/C++11 их допускает, не позволяет формально доказывать многие полезные свойства программ в рамках этой модели.
Наличие проблемы “значенийиз воздуха” связано с тем, что модель C/C++11 задана декларативно (аксиоматически), при этом сценарий поведения программы в рамках модели определяетсякак некоторая монолитная структура (граф), а не как последовательность действий некоторой абстрактной машины.
Это оставляет открытым вопрос об интеграции модели с остальными компонентами языка, которые в стандарте C/C++11определены операционно.Таким образом, для развития инструментов анализа многопоточных программ необходимо разработать операционные подходы к заданию слабых моделей памяти.Степень разработанности темы. С 1990-х годов велась работа по разработке семантики многопоточности с учетом слабых сценариев поведения.Формальные модели для наиболее распространенных процессорных архитектур(x86, Power, ARM) были разработаны J. Alglave, S. Ishtiaq, L. Maranget, F.
ZappaNardelli, S. Sarkar, P. Sewell и др. исследователями. Новые версии моделей продолжают появляться в связи с развитием процессорных архитектур. В частности,в 2016 и 2017 годах были представлены модели памяти для архитектур ARMv8.0и ARMv8.3. В 1995 году была стандартизована слабая модель памяти для языкаJava; в дальнейшем модель существенно менялась вплоть до 2005 года. В 2011году появилась аксиоматическая модель памяти для языков C/C++.В 2017 году исследователи J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis иD.
Dreyer представили обещающую модель памяти (promising memory model,Promise), которая является перспективным решением проблемы задания семантики для языка с многопоточностью. Авторы доказали, что модель допускаетбольшинство необходимых оптимизаций, а также показали корректность эффективных схем компиляции в архитектуры x86 и Power.
Открытым остался вопросо корректности компиляции в архитектуру ARM.Целью данной работы является исследование применимости операционных подходов для описания реалистичных моделей памяти и анализа многопоточных программ на примере языков C/C++.Для достижения поставленной цели были сформулированы следующиезадачи.1. Разработать операционную модель памяти С/С++11, свободную от проблемы “значений из воздуха”.2. Доказать корректность эффективной схемы компиляции из существенного подмножества обещающей модели в операционную модель памятиARMv8 POP.43.
Доказать корректность эффективной схемы компиляции из существенного подмножества обещающей модели в аксиоматическую модель памяти ARMv8.3.Постановка цели и задач исследования соответствует следующим пунктампаспорта специальности 05.13.11: модели, методы и алгоритмы проектированияи анализа программ и программных систем, их эквивалентных преобразований,верификации и тестирования (пункт 1); языки программирования и системы программирования, семантика программ (пункт 2); модели и методы создания программ и программных систем для параллельной и распределенной обработкиданных, языки и инструментальные средства параллельного программирования(пункт 8).Mетодология и методы исследования.
Методология исследования базируется на подходах информатики к описанию и анализу формальных семантикязыков программирования.В работе используется представление операционной семантики программы с помощью помеченной системы переходов, а также метода вычислительныхконтекстов, предложенного M. Felleisen. Для доказательств корректности компиляции используется техника прямой симуляции.
Программная реализация интерпретатора операционной модели памяти C/C++11 выполнена на языке Racketс использованием предметно-ориентированного расширения PLT/Redex.Основные положения, выносимые на защиту.1. Предложена операционная модель памяти C/С++11, для этой модели реализован интерпретатор.2. Доказана корректность компиляции из существенного подмножестваобещающей модели в операционную модель памяти ARMv8 POP.3. Доказана корректность компиляции из существенного подмножестваобещающей модели в аксиоматическую модель памяти ARMv8.3.Научная новизна результатов, полученных в рамках исследования, заключается в следующем.1.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
