Автореферат (1149930), страница 4
Текст из файла (страница 4)
Для любого корректного сценария поведения G в модели ARMv8.3 существует обход ⟨W init , W init ⟩ →∗TC ⟨E, W ⟩, где W init — множество инициализи13рующих записей сценария G, E — все события сценария G, W — все событиязаписи сценария G.Используя данную теорему для построения операционного исполненияпрограммы в модели ARMv8.3, автор работы доказывает, что обещающая модель может симулировать сценарии поведения модели ARMv8.3.В заключении приведены основные результаты работы.1.
Разработана операционная модель памяти C/C++11. Данная модель допускает такие же сценарии поведения, что и модель C/С++11 на большинстве тестов, приведенных в литературе, но не обладает сценариямиповедения со “значениями из воздуха”. В отличие от обещающей модели, предлагаемая модель является запускаемой, что упрощает разработку средств анализа программ для неё. Недостатком модели является то,она накладывает синтаксические ограничения на поведения программ.2.
Доказана корректность компиляции из существенного подмножестваобещающей модели в операционную модель памяти ARMv8 POP.3. Доказана корректность компиляции из существенного подмножестваобещающей модели в аксиоматическую модель памяти ARMv8.3.В рамках рекомендации по применению результатов работы в индустрии и научных исследованиях указывается, что модель памяти промышленного языка программирования должна быть лишена сценариев поведения, имеющих “значения из воздуха”, а также либо быть представленной в операционнойформе, либо иметь эквивалентный операционный аналог. Последнее позволяетреализовать интерпретатор модели и выполнять отладку программ в рамках модели.Также были определены перспективы дальнейшей разработки тематики, основным из которых является разработка обобщенной аксиоматической модели памяти для процессорных архитектур, которая будет определена для синтаксиса модели C/C++11 и окажется строгим надмножеством существующих моделей памяти x86, Power и ARM, а также для которой будет применим предложенный метод доказательства корректности компиляции из обещающей моделипамяти.
Это позволит свести дальнейшие доказательства корректности компиляции из обещающей модели к доказательству корректности компиляции в обобщенную аксиоматическую модель, что сводится к рассуждениям об ацикличности и вложенности путей на графах. Кроме того, актуальной является задача разработки эффективной программной логики на базе логики многопоточного разделения (concurrent separation logic) для операционного аналога модели памятиC/С++11 и обещающей модели памяти. Такая логика позволит формально доказывать в рамках моделей сложные свойства программ, такие как соответствиеспецификации.14Публикации автора по теме диссертацииНиже приведён перечень публикаций, где были представлены основныерезультаты данной диссертационной работы.Статьи из “Перечня рецензируемых научных изданий, в которых должныбыть опубликованы основные научные результаты диссертаций на соискание ученой степени кандидата наук, на соискание ученой степени докторанаук”, сформированного согласно требованиям, установленным Министерством образования и науки Российской Федерации1.
Подкопаев, А. В. О корректности компиляции подмножества обещающей модели памяти в аксиоматическую модель ARMv8.3 / А.В. Подкопаев, О. Лахав, В. Вафеядис // Научно-технические ведомости СПбГПУ. Информатика,Телекоммуникации. Управление. — 2017. — Т. 10, № 4. — C. 51–69.2. Подкопаев, А. В. Обещающая компиляция в ARMv8.3 / А.В. Подкопаев, О.Лахав, В. Вафеядис // Труды ИСП РАН. — 2017. — Т. 29, № 5. — C. 149–164.Статьи в изданиях, входящих в базы цитирования Web of Science и Scopus3. Podkopaev, A. Promising compilation to ARMv8 POP / A. Podkopaev, O. Lahav,V.
Vafeiadis // 31st European Conference on Object-Oriented Programming(ECOOP 17), Leibniz International Proceedings in Informatics (LIPIcs). — 2017.— P. 22:1–22:28.Статьи в других изданиях4. Подкопаев, А. В. Обещающая компиляция в ARMv8 / А.В. Подкопаев, О.Лахав, В. Вафеядис // Языки программирования и компиляторы. Труды конференции. Ростов-на-Дону, Россия. — 2017. — C. 223–226.5. Podkopaev, A. Operational Aspects of C/C++ Concurrency / A. Podkopaev, I.Sergey, A.
Nanevski [Электронный ресурс]. — URL: http://arxiv.org/abs/1606.01400 (дата обращения: 14.11.2017).15Подкопаев Антон ВикторовичОПЕРАЦИОННЫЕ МЕТОДЫ В ПРИЛОЖЕНИИ К СЛАБЫМ МОДЕЛЯМ ПАМЯТИАвтореф. дис. на соискание ученой степени канд. физ.-мат. наукПодписано в печать. .. Заказ №Формат 60×90/16. Усл.
печ. л. 1. Тираж 100 экз.Типография.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
