WikiDer > Логика разделения - Википедия
В Информатика, логика разделения[1] является продолжением Логика Хоара, способ рассуждать о программах. Джон С. Рейнольдс, Питер О'Хирн, Самин Иштиак и Хонгсок Ян,[1][2][3][4] опираясь на ранние работы Род Берстолл.[5] Язык утверждений логики разделения - это частный случай логика сгруппированных выводов (BI).[6] В обзорной статье CACM, написанной О'Хирном, показаны изменения в данной теме до начала 2019 года.[7]
Обзор
Логика разделения облегчает рассуждение о:
- программы, которые манипулируют структурами данных указателей, включая скрытие информации при наличии указателей;
- «передача права собственности» (избегание семантической рамки аксиомы); и
- виртуальное разделение (модульное мышление) между параллельными модулями.
Логика разделения поддерживает развивающуюся область исследований, описанную Питер О'Хирн и другие как местная аргументация, при этом в спецификациях и доказательствах программного компонента упоминается только часть памяти, используемая компонентом, а не все глобальное состояние системы. Приложения включают автоматизированные проверка программы (где алгоритм проверяет правильность другого алгоритма) и автоматически распараллеливание программного обеспечения.
Утверждения: операторы и семантика
Утверждения логики разделения описывают «состояния», состоящие из хранить и куча, примерно соответствующее состоянию местный (или выделенный стеком) переменные и динамически распределяемый объекты в распространенных языках программирования, таких как C и Ява. Склад это функция отображение переменных в значения. Куча это частичная функция отображение адресов памяти в значения. Две кучи и находятся непересекающийся (обозначено ), если их домены не перекрываются (т. е. для каждого адреса памяти , по крайней мере, один из и не определено).
Логика позволяет обосновывать суждения вида , куда это магазин, это куча, и является утверждение над данным магазином и кучей. Утверждения логики разделения (обозначенные как , , ) содержат стандартные булевы связки и, кроме того, , , , и , куда и выражения.
- Постоянная утверждает, что куча пустой, т.е. когда не определено для всех адресов.
- Бинарный оператор принимает адрес и значение и утверждает, что куча определена ровно в одном месте, сопоставляя данный адрес с заданным значением. Т.е., когда (куда обозначает значение выражения оценивается в магазине ) и в противном случае не определено.
- Бинарный оператор (произносится звезда или же разделительный союз) утверждает, что кучу можно разделить на две непересекающийся части, в которых справедливы два его аргумента, соответственно. Т.е., когда есть такой, что и и и .
- Бинарный оператор (произносится Волшебная палочка или же разделяющее значение) утверждает, что расширение кучи непересекающейся частью, удовлетворяющей своему первому аргументу, приводит к получению кучи, удовлетворяющей второму аргументу. Т.е. когда для каждой кучи такой, что , также держит.
Операторы и разделяют некоторые свойства с классическими соединение и значение операторы. Их можно комбинировать, используя правило вывода, подобное modus ponens
и они образуют примыкание, т.е. если и только если за ; точнее, сопряженные операторы и .
Рассуждения о программах: тройки и правила доказательства
В логике разделения тройки Хоара имеют несколько иное значение, чем в Логика Хоара. Тройка утверждает, что если программа выполняется из начального состояния, удовлетворяющего предварительному условию тогда программа будет не ошибись (например, иметь неопределенное поведение), и если оно завершается, то конечное состояние будет удовлетворять постусловию . По сути, при его исполнении может иметь доступ только к ячейкам памяти, существование которых заявлено в предварительном условии или которые были выделены сам.
Помимо стандартных правил от Логика Хоара, логика разделения поддерживает следующее очень важное правило:
Это известно как фрейм правило (назван в честь проблема с рамой) и допускает локальные рассуждения. В нем говорится, что программа, которая безопасно выполняется в небольшом состоянии (удовлетворяющем ), также может выполняться в любом более крупном состоянии (удовлетворяющем ) и что его выполнение не повлияет на дополнительную часть состояния (и так останется истинным в постусловии). Дополнительное условие обеспечивает это, указывая, что ни одна из переменных, измененных происходить бесплатно в , т.е. ни один из них не входит в набор 'свободная переменная' из .
Обмен
Логика разделения приводит к простым доказательствам манипулирования указателями для структур данных, которые демонстрируют регулярные шаблоны совместного использования, которые можно описать просто с помощью разделяющих союзов; примеры включают односвязные и двусвязные списки и разновидности деревьев. Графы, группы DAG и другие структуры данных с более общим общим доступом сложнее как для формального, так и для неформального доказательства. Тем не менее, логика разделения успешно применялась к рассуждениям о программах с общим разделением.
В своей статье POPL'01[3] О'Хирн и Иштиак объяснили, как соединяется волшебная палочка. можно было бы использовать для рассуждения при наличии совместного использования, по крайней мере, в принципе.
мы получаем самое слабое предварительное условие для оператора, который изменяет кучу в местоположении , и это работает для любого постусловия, а не только для того, которое аккуратно выложено с помощью разделяющего союза. Эта идея была значительно продвинута Янгом, который использовал предоставить локальные рассуждения о мутациях в классическом Алгоритм разметки графа Шорра-Уэйта.[8] Наконец, одна из последних работ в этом направлении - это работа Хобора и Вилларда.[9] кто нанимает не только но также связующее который по-разному называли перекрывающимся соединением или сепиш,[10] и которые можно использовать для описания перекрывающихся структур данных: держит кучу когда и придерживаться кучи и чей союз , но которые, возможно, имеют непустую часть в общем. Абстрактно, можно рассматривать как версию соединительного элемента слияния логика релевантности.
Логика параллельного разделения
Логика параллельного разделения (CSL), версия логики разделения для параллельных программ, была первоначально предложена Питер О'Хирн,[11]используя правило доказательства
что позволяет независимо рассуждать о потоках, обращающихся к отдельному хранилищу. Правила доказательства О'Хирна адаптировали ранний подход Тони Хоар к рассуждениям о параллелизме,[12]замена использования ограничений области действия для обеспечения разделения рассуждением в логике разделения. В дополнение к расширению подхода Хоара для применения в присутствии указателей, выделенных из кучи, О'Хирн показал, как логика параллельного разделения может отслеживать динамическую передачу владения частями кучи между процессами; примеры в статье включают буфер передачи указателя и менеджер памяти.
Модель для параллельной логики разделения была впервые представлена Стивеном Бруксом в статье, сопутствующей О'Хирну.[13] Обоснованность логики была трудной проблемой, и на самом деле контрпример Джона Рейнольдса показал несостоятельность более ранней, неопубликованной версии логики; вопрос, поднятый примером Рейнольдса, кратко описан в статье О'Хирна и более подробно в статье Брукса.
Сначала казалось, что CSL хорошо подходит для того, что Дейкстра назвал слабо связанными процессами,[14] но, возможно, не к мелкозернистым параллельным алгоритмам со значительными помехами. Однако постепенно стало понятно, что базовый подход CSL оказывается значительно более мощным, чем предполагалось вначале, если использовать нестандартные модели логических связок и даже троек Хоара.
Была предложена абстрактная версия логики разделения, которая работает для троек Хоара, где предусловия и постусловия представляют собой формулы, интерпретируемые над произвольным частичным коммутативным моноидом вместо конкретной модели кучи.[15] Позже, путем подходящего выбора коммутативного моноида, было неожиданно обнаружено, что правила доказательства абстрактных версий логики параллельного разделения могут быть использованы для рассуждений о вмешательстве в параллельные процессы, например, путем кодирования техники надежной гарантии, которая первоначально была предложена для обоснования о вмешательстве;[16] в этой работе элементы модели рассматривались не как ресурсы, а скорее как «представления» о состоянии программы, а нестандартная интерпретация троек Хоара сопровождает нестандартное прочтение предусловий и постусловий. Наконец, принципы CSL-стиля имеют был использован для составления рассуждений об историях программ, а не о состояниях программ, чтобы предоставить модульные методы для рассуждений о мелкозернистых параллельных алгоритмах.[17]
Версии CSL были включены во многие интерактивные и полуавтоматические (или «промежуточные») инструменты проверки, как описано в следующем разделе. Особенно значительные усилия по проверке прилагаются к упомянутому там ядру μC / OS-II. Но, хотя шаги были сделаны,[18] на данный момент рассуждения в стиле CSL включены в сравнительно небольшое количество инструментов в категорию автоматического анализа программ (и ни один из них не упоминается в следующем разделе).
О'Хирн и Брукс - соучредители премии 2016 г. Премия Гёделя за изобретение логики параллельного разделения.[19]
Инструменты проверки и анализа программ
Инструменты для рассуждений о программах варьируются от полностью автоматических инструментов анализа программ, не требующих ввода данных пользователем, до интерактивных инструментов, в которых человек принимает непосредственное участие в процессе проверки. Было разработано много таких инструментов; следующий список включает несколько представителей в каждой категории.
- Автоматический анализ программ. Эти инструменты обычно ищут ограниченные классы ошибок (например, ошибки безопасности памяти) или пытаются доказать их отсутствие, но не могут доказать полную корректность.
- Текущий пример: Facebook Infer, инструмент статического анализа для Java, C и Цель-C на основе логики разделения и двойного похищения.[20] По состоянию на 2015 год Infer обнаруживал и исправлял сотни ошибок в месяц перед отправкой в мобильные приложения Facebook.[21]
- Другие примеры включают SpaceInvader (один из первых анализаторов SL), Хищник (который выиграл несколько проверочных соревнований), MemCAD (который сочетает в себе форму и числовые свойства) и SLAyer (из Microsoft Research, основное внимание уделяется структурам данных в драйверах устройств)
- Интерактивное доказательство. Доказательства были выполнены с использованием вложений логики разделения в интерактивные средства доказательства теорем, такие как Помощник доказательства Coq и HOL (помощник проверки). По сравнению с анализом программ, эти инструменты требуют больших человеческих усилий, но обладают более глубокими свойствами, вплоть до функциональной корректности.
- Доказательство файловой системы FSCQ[22] где спецификация включает поведение при сбоях, а также нормальную работу. Эта работа получила награду за лучшую работу на Симпозиуме по принципам операционных систем 2015 года.
- Проверка большого фрагмента Ржавчина система типов и некоторые из ее стандартных библиотек в Проект RustBelt с использованием Ирис структура для логики разделения в Помощник доказательства Coq.
- Проверка реализации OpenSSL алгоритма криптографической аутентификации,[23] использование проверяемый C
- Верификация ключевых модулей коммерческого ядра ОС, ядра μC / OS-II, первый коммерческий упреждающий ядро должно быть проверено.[24]
- Другие примеры включают У не[25] библиотека для Помощник доказательства Coq; то Холфут встраивание Smallfoot в HOL; Детализированная логика параллельного разделения, и Коренная порода (библиотека Coq для низкоуровневого программирования).
- Между. Многие инструменты требуют большего вмешательства пользователя, чем анализ программы, поскольку они ожидают, что пользователь введет утверждения, такие как предварительные / последующие спецификации для функций или инварианты цикла, но после того, как этот ввод предоставлен, они пытаются быть полностью или почти полностью автоматическими; Этот способ проверки восходит к классическим работам 1970-х годов, таким как верификатор Дж. Кинга и Стэнфордский верификатор Паскаля. Этот стиль верификатора недавно получил название автоматическая активная проверка, термин, который предназначен для обозначения способа взаимодействия с проверяющим через цикл проверки утверждений, аналогично взаимодействию между программистом и средством проверки типов.
- Самый первый верификатор логики разделения, Смолфут, находился в этой промежуточной категории. Он требовал, чтобы пользователь вводил спецификации до и после, инварианты цикла и инварианты ресурсов для блокировок. Он представил метод символического исполнения, а также автоматический способ вывода аксиом фрейма. Смоллфут включил логику параллельного разделения.
- SmallfootRG это средство проверки сочетания логики разделения и классического метода проверки / гарантии для параллельных программ.
- Куча хоп реализует логику разделения для передачи сообщений, следуя идеям в Singularity (операционная система).
- Verifast - это продвинутый текущий инструмент в промежуточной категории. Он продемонстрировал разнообразные доказательства, от объектно-ориентированных шаблонов до алгоритмов с высокой степенью параллелизма и системных программ.
- В Язык программирования Mezzo и Типы асинхронного отделения жидкости включить идеи, связанные с CSL, в систему типов для языка программирования. Идея включения разделения в систему типов уже упоминалась ранее в Типы псевдонимов и Синтаксический контроль интерференции.
Различие между интерактивными и промежуточными верификаторами не является резким. Например, Bedrock стремится к высокой степени автоматизации в том, что он называет в основном автоматической проверкой, где Verifast иногда требует аннотаций, которые напоминают тактики (небольшие программы), используемые в интерактивных верификаторах.
Рекомендации
- ^ а б Рейнольдс, Джон С. (2002). «Логика разделения: логика для общих изменяемых структур данных» (PDF). LICS.
- ^ Рейнольдс, Джон С. (1999). «Интуиционистские рассуждения об общей изменчивой структуре данных». В Дэвис, Джим; Роско, Билл; Вудкок, Джим (ред.). Millennium Perspectives in Computer Science, Proceedings of the 1999 Oxford – Microsoft Symposium in Honor of Sir Tony Hoare. Palgrave.
- ^ а б Иштиак, Самин; О'Хирн, Питер (2001). «BI как язык утверждений для изменяемых структур данных». POPL. ACM.
- ^ О'Хирн, Питер; Рейнольдс, Джон С.; Ян, Хонгсок (2001). «Местные рассуждения о программах, изменяющих структуры данных». CSL. CiteSeerX 10.1.1.29.1331.
- ^ Берстолл, Р. М. (1972). «Некоторые методы доказательства программ, изменяющих структуры данных». Машинный интеллект. 7.
- ^ О'Хирн, П. У .; Пим, Д. Дж. (Июнь 1999 г.). «Логика сгруппированных следствий». Бюллетень символической логики. 5 (2): 215–244. CiteSeerX 10.1.1.27.4742. Дои:10.2307/421090. JSTOR 421090.
- ^ О'Хирн, Питер (февраль 2019 г.). «Логика разделения». Commun. ACM. 62 (2): 86–95. Дои:10.1145/3211968. ISSN 0001-0782.
- ^ Ян, Хонгсок (2001). "Пример локального мышления в логике указателя BI: алгоритм маркировки графа Шорра-Уэйта". Труды 1-го семинара по семантике «Программный анализ» и вычислительным средам для управления памятью.
- ^ Хобор, Фома Аквинский; Виллар, Жюль (2013). «Разветвления совместного использования структур данных» (PDF). Уведомления ACM SIGPLAN. 48: 523–536. Дои:10.1145/2480359.2429131.
- ^ Гарднер, Филиппа; Маффейс, Серджио; Смит, Харет (2012). "К программной логике для Java Сценарий" (PDF). Материалы 39-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '12. С. 31–44. Дои:10.1145/2103656.2103663. HDL:10044/1/33265. ISBN 9781450310833. S2CID 9571576.
- ^ О'Хирн, Питер (2007). «Ресурсы, параллелизм и локальное мышление» (PDF). Теоретическая информатика. 375 (1–3): 271–307. Дои:10.1016 / j.tcs.2006.12.035.
- ^ Хоар, C.A.R. (1972). «К теории параллельного программирования». Операционная система. Академическая пресса.
- ^ Брукс, Стивен (2007). "Семантика логики параллельного разделения" (PDF). Теоретическая информатика. 375 (1–3): 227–270. Дои:10.1016 / j.tcs.2006.12.034.
- ^ Дейкстра, Эдсгер В. Взаимодействующие последовательные процессы (EWD-123) (PDF). Архив Э.В. Дейкстры. Центр американской истории, Техасский университет в Остине. (транскрипция) (Сентябрь 1965 г.)
- ^ Кальканьо, Криштиану; О'Хирн, Питер У .; Ян, Хонгсок (2007). "Локальное действие и логика абстрактного разделения" (PDF). 22-й ежегодный симпозиум IEEE по логике в компьютерных науках (LICS 2007). С. 366–378. CiteSeerX 10.1.1.66.6337. Дои:10.1109 / LICS.2007.30. ISBN 978-0-7695-2908-0. S2CID 1044254.
- ^ Динсдейл-Янг, Томас; Биркедал, Ларс; Гарднер, Филиппа; Паркинсон, Мэтью; Ян, Хонгсок (2013). "Взгляды" (PDF). Уведомления ACM SIGPLAN. 48: 287–300. Дои:10.1145/2480359.2429104.
- ^ Сергей, Илья; Наневский, Александар; Банерджи, Аниндья (2015). «Определение и проверка параллельных алгоритмов с историей и субъективностью» (PDF). 24-й Европейский симпозиум по программированию. arXiv:1410.0306. Bibcode:2014arXiv1410.0306S.
- ^ Гоцман Алексей; Бердин, Джош; Повар, Байрон; Сагив, Мули (2007). Анализ модульной формы резьбы (PDF). PLDI. Конспект лекций по информатике. 5403. С. 266–277. Дои:10.1007/978-3-540-93900-9_3. ISBN 978-3-540-93899-6.
- ^ https://www.eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize-
- ^ Логика разделения и двойное похищение, стр., Вывести сайт проекта.
- ^ Вывод на Facebook с открытым исходным кодом: выявление ошибок перед отправкой. С. Кальканьо, Д. Дистефано и П. О'Хирн. 11 июня 2015 г.
- ^ Использование Crash Hoare Logic для сертификации файловой системы FSCQ, Х. Чен и др., SOSP'15
- ^ Проверенная корректность и безопасность OpenSSL HMAC. Леннарт Берингер, Адам Петчер, Кэтрин К. Йе и Эндрю В. Аппель. В 24-й симпозиум по безопасности USENIX, Август 2015 г.
- ^ Фреймворк практической проверки для превентивных ядер ОС. Фэнвэй Сюй, Мин Фу, Синью Фэн, Сяоран Чжан, Хуэй Чжан и Чжаохуэй Ли: В CAV 2016: 59–79
- ^ Домашняя страница Ynot Project, Гарвардский университет, СОЕДИНЕННЫЕ ШТАТЫ АМЕРИКИ.