Логика разделения

В информатике , логика разделения ^[1] является продолжением логики Хора , способ рассуждения о программах. Он был разработан Джоном К. Рейнольдсом , Питером О'Хирном , Самином Иштиаком и Хонгсоком Яном ^{[1] [2] [3] [4],} опираясь на ранние работы Рода Берстолла . ^[5] Язык утверждений логики разделения - это частный случай логики сгруппированных импликаций (BI). ^[6] В обзорной статье CACM, написанной О'Хирном, показаны изменения в данной теме до начала 2019 года. ^[7]

Обзор [ править ]

Логика разделения помогает рассуждать о:

• программы, которые манипулируют структурами данных указателей, включая скрытие информации при наличии указателей;
• «передача права собственности» (уход от аксиом семантического фрейма ); а также
• виртуальное разделение (модульное мышление) между параллельными модулями.

Логика разделения поддерживает развивающуюся область исследований, описанную Питером О'Хирном и другими как локальные рассуждения , согласно которым в спецификациях и доказательствах программного компонента упоминается только часть памяти, используемая компонентом, а не все глобальное состояние системы. Приложения включают автоматическую проверку программы (когда алгоритм проверяет правильность другого алгоритма) и автоматическое распараллеливание программного обеспечения.

Утверждения: операторы и семантика [ править ]

Утверждения логики разделения описывают «состояния», состоящие из хранилища и кучи , примерно соответствующие состоянию локальных (или выделенных стеком ) переменных и динамически выделяемых объектов в распространенных языках программирования, таких как C и Java . Хранилище - это функция, отображающая переменные в значения. Куча - это частичная функция, отображающая адреса памяти в значения. Две кучи и не пересекаются (обозначаются ), если их домены не перекрываются (т. Е. Для каждого адреса памяти хотя бы один из${\ displaystyle s}$${\ displaystyle h}$${\ displaystyle h}$${\ displaystyle h '}$${\ displaystyle h \, \ bot \, h '}$${\ displaystyle \ ell}$${\ Displaystyle ч (\ ell)}$и не определено).${\ displaystyle h '(\ ell)}$

Логика позволяет доказывать суждения о форме , где - хранилище, является кучей и является утверждением для данного хранилища и кучи. Разделение логических утверждений (обозначенные как , , ) содержат стандартные логические связки и, кроме того, , , , и , где и являются выражениями.${\ displaystyle s, h \ models P}$${\ displaystyle s}$${\ displaystyle h}$${\ displaystyle P}$${\ displaystyle P}$${\displaystyle Q}$${\displaystyle R}$${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle e\mapsto e'}$${\displaystyle P\ast Q}$${\displaystyle P{-\!\!\ast }\,Q}$${\displaystyle e}$${\displaystyle e'}$

• Константа утверждает, что куча пуста , т. Е. Когда не определено для всех адресов.${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }$${\displaystyle h}$
• Бинарный оператор принимает адрес и значение и утверждает, что куча определена ровно в одном месте, сопоставляя данный адрес с заданным значением. Т.е. когда (где обозначает значение выражения, вычисленное в магазине ), иначе не определено.${\displaystyle \mapsto }$${\displaystyle s,h\models e\mapsto e'}$${\displaystyle h([\![e]\!]_{s})=[\![e']\!]_{s}}$${\displaystyle [\![e]\!]_{s}}$${\displaystyle e}$${\displaystyle s}$${\displaystyle h}$
• Бинарный оператор (произносится как звезда или разделяющая конъюнкция ) утверждает, что куча может быть разделена на две непересекающиеся части, где выполняются два ее аргумента, соответственно. Т.е. когда существуют такие что и и и .${\displaystyle \ast }$${\displaystyle s,h\models P\ast Q}$${\displaystyle h_{1},h_{2}}$${\displaystyle h_{1}\,\bot \,h_{2}}$${\displaystyle h=h_{1}\cup h_{2}}$${\displaystyle s,h_{1}\models P}$${\displaystyle s,h_{2}\models Q}$
• Бинарный оператор (произносится как « волшебная палочка» или « разделяющая импликация» ) утверждает, что расширение кучи непересекающейся частью, удовлетворяющей своему первому аргументу, приводит к получению кучи, удовлетворяющей второму аргументу. Т.е. ,. when для каждой такой кучи , также выполняется.${\displaystyle -\!\!\ast }$${\displaystyle s,h\models P-\!\!\ast \,Q}$${\displaystyle h'\,\bot \,h}$${\displaystyle s,h'\models P}$${\displaystyle s,h\cup h'\models Q}$

Операторы и имеют общие свойства с классическими операторами конъюнкции и импликации . Их можно комбинировать с помощью правила вывода, аналогичного modus ponens.${\displaystyle \ast }$${\displaystyle -\!\!\ast }$

${\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}$

и они образуют примыкание , т. е. тогда и только тогда, когда для ; точнее, сопряженными операторами являются и .${\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}$${\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}$${\displaystyle h\,\bot \,h'}$${\displaystyle \_\ast Q}$${\displaystyle Q-\!\!\ast \,\_}$

Рассуждения о программах: тройки и правила доказательства [ править ]

В логике разделения тройки Хоара имеют несколько иное значение, чем в логике Хоара . Тройка утверждает, что если программа выполняется из начального состояния, удовлетворяющего предварительному условию, тогда программа не пойдет неправильно (например, будет иметь неопределенное поведение), а если она завершится, то конечное состояние будет удовлетворять постусловию . По сути, во время своего выполнения он может обращаться только к тем ячейкам памяти, существование которых утверждается в предварительном условии или которые были выделены им самим.${\displaystyle \{P\}\ C\ \{Q\}}$${\displaystyle C}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle C}$${\displaystyle C}$

В дополнение к стандартным правилам из логики Хоара, логика разделения поддерживает следующее очень важное правило:

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$

Это известно как фреймовое правило (названное в честь проблемы фрейма ) и допускает локальные рассуждения. В нем говорится, что программа, которая безопасно выполняется в небольшом состоянии (удовлетворение ), может также выполняться в любом более крупном состоянии (удовлетворение ) и что ее выполнение не повлияет на дополнительную часть состояния (и поэтому останется истинным в постусловии). Сторона состояние навязывает это, не указав , что ни один из переменных , модифицированных свободной в , то есть ни один из них не в «свободной переменной» набор из .${\displaystyle P}$${\displaystyle P\ast R}$${\displaystyle R}$${\displaystyle C}$${\displaystyle R}$${\displaystyle {\mathsf {fv}}}$${\displaystyle R}$

Совместное использование [ править ]

Логика разделения приводит к простым доказательствам манипулирования указателями для структур данных, которые демонстрируют регулярные шаблоны совместного использования, которые можно описать просто с помощью разделяющих союзов; примеры включают односвязные и двусвязные списки и разновидности деревьев. Графы, группы DAG и другие структуры данных с более общим разделением сложнее как для формального, так и для неформального доказательства. Тем не менее, логика разделения успешно применялась к рассуждениям о программах с общим разделением.

В своей статье POPL'01 ^[3] О'Хирн и Иштиак объяснили, как связку волшебной палочки можно использовать для рассуждения при наличии разделения, по крайней мере, в принципе. Например, в тройном${\displaystyle {-\!\!*}}$

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ [x]=42\ \{P\}}$

мы получаем самое слабое предусловие для оператора, который изменяет кучу в определенном месте , и это работает для любого постусловия, а не только для того, которое аккуратно выложено с помощью разделяющего конъюнкции. Эта идея была значительно продвинута Янгом, который использовал локализованные рассуждения о мутациях в классическом алгоритме маркировки графов Шорра-Уэйта . ^[8] Наконец, один из самых последних работ в этом направлении является то , что Hobor и Виара, ^[9] , которые используют не только также соединительно , но который по- разному называют перекрытием конъюнкции или sepish, ^[10] , и которые могут быть использованы для описания перекрывающихся структур данных: удерживает кучу, когда и${\displaystyle x}$${\displaystyle {-\!\!*}}$${\displaystyle {-\!\!*}}$${\displaystyle \cup \,\!\!\!\!\!*}$${\displaystyle P\cup \!\!\!\!\!*Q}$${\displaystyle h}$${\displaystyle P}$${\displaystyle Q}$справедливы для подкучков и чье объединение есть , но которые, возможно, имеют непустую общую часть . Абстрактно его можно рассматривать как версию логики слияния логики релевантности .${\displaystyle h_{P}}$${\displaystyle h_{Q}}$${\displaystyle h}$${\displaystyle h_{P}\cap h_{Q}}$${\displaystyle P\cup \!\!\!\!\!*Q}$

Логика параллельного разделения [ править ]

Параллельная Разделение логики (CSL), версия логики разделения для параллельных программ, первоначально был предложен Питером O'Hearn , ^[11] с использованием доказательства правила

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

что позволяет независимо рассуждать о потоках, обращающихся к отдельному хранилищу. Правила доказательства О'Хирна адаптировали ранний подход Тони Хоара к рассуждениям о параллелизме ^[12], заменив использование ограничений области видимости для обеспечения разделения рассуждениями в логике разделения. В дополнение к расширению подхода Хоара для применения в присутствии указателей, выделенных в куче, О'Хирн показал, как логика параллельного разделения может отслеживать динамическую передачу владения частями кучи между процессами; Примеры в статье включают буфер передачи указателя и диспетчер памяти .

Модель для параллельной логики разделения была впервые представлена ​​Стивеном Бруксом в статье, сопутствующей О'Хирну. ^[13] Надежность логики была сложной проблемой, и на самом деле контрпример Джона Рейнольдса показал несостоятельность более ранней, неопубликованной версии логики; вопрос, поднятый примером Рейнольдса, кратко описан в статье О'Хирна и более подробно в статье Брукса.

Сначала казалось, что CSL хорошо подходит для того, что Дейкстра назвал слабо связанными процессами ^[14], но, возможно, не для мелкозернистых параллельных алгоритмов со значительными помехами. Однако постепенно стало понятно, что базовый подход CSL был значительно более мощным, чем предполагалось вначале, если использовать нестандартные модели логических связок и даже троек Хоара.

Была предложена абстрактная версия логики разделения, которая работает для троек Хоара, где предусловия и постусловия представляют собой формулы, интерпретируемые над произвольным частичным коммутативным моноидом вместо конкретной модели кучи. ^[15] Позже, путем подходящего выбора коммутативного моноида, было неожиданно обнаружено, что правила доказательства абстрактных версий логики параллельного разделения могут быть использованы для рассуждений о вмешательстве в параллельные процессы, например, путем кодирования техники надежной гарантии, которая изначально была предложил рассуждать о вмешательстве; ^[16]в этой работе элементы модели рассматривались не как ресурсы, а как «представления» о состоянии программы, а нестандартное прочтение предусловий и постусловий сопровождает нестандартная интерпретация троек Хоара. Наконец, принципы стиля CSL были использованы для составления рассуждений об историях программ, а не о состояниях программ, чтобы предоставить модульные методы для рассуждений о мелкозернистых параллельных алгоритмах. ^[17]

Версии CSL были включены во многие интерактивные и полуавтоматические (или «промежуточные») инструменты проверки, как описано в следующем разделе. Особенно значительные усилия по проверке связаны с упомянутым там ядром μC / OS-II. Но, хотя шаги были предприняты, ^[18] на данный момент рассуждения в стиле CSL включены в сравнительно небольшое количество инструментов в категории автоматического анализа программ (и ни один из них не упоминается в следующем разделе).

О'Хирн и Брукс - соучредители премии Гёделя 2016 года за изобретение логики параллельного разделения. ^[19]

Инструменты проверки и анализа программ [ править ]

Инструменты для рассуждений о программах варьируются от полностью автоматических инструментов анализа программ, не требующих ввода данных пользователем, до интерактивных инструментов, в которых человек принимает непосредственное участие в процессе проверки. Было разработано много таких инструментов; следующий список включает несколько представителей в каждой категории.

• Автоматический анализ программ. Эти инструменты обычно ищут ограниченные классы ошибок (например, ошибки безопасности памяти) или пытаются доказать их отсутствие, но не могут доказать полную корректность.
  • Текущий пример - Facebook Infer , инструмент статического анализа для Java, C и Objective-C, основанный на логике разделения и двойном абдукции. ^[20] По состоянию на 2015 год, Infer обнаруживал сотни ошибок в месяц и исправлял их разработчиками перед отправкой в ​​мобильные приложения Facebook ^[21]
  • Другие примеры включают SpaceInvader (один из первых анализаторов SL), Predator (который выиграл несколько соревнований по проверке), MemCAD (который сочетает форму и числовые свойства) и SLAyer (из Microsoft Research, ориентированный на структуры данных, обнаруженные в драйверах устройств).
• Интерактивное доказательство. Доказательства были выполнены с использованием вложений логики разделения в интерактивные средства доказательства теорем, такие как помощник по доказательству Coq и HOL (помощник по доказательству) . По сравнению с работой по анализу программ, эти инструменты требуют больших человеческих усилий, но обладают более глубокими свойствами, вплоть до функциональной корректности.
  • Доказательство файловой системы FSCQ ^[22], где спецификация включает поведение при сбоях, а также нормальную работу. Эта работа получила награду за лучшую работу на Симпозиуме по принципам операционных систем 2015 года.
  • Верификация большого фрагмента системы типов Rust и некоторых ее стандартных библиотек в проекте RustBelt с использованием фреймворка Iris для логики разделения в помощнике доказательства Coq .
  • Проверка реализации OpenSSL алгоритма криптографической аутентификации ^{[23] с} использованием проверяемого языка C
  • Проверка ключевых модулей коммерческого ядра ОС, ядра μC / OS-II, первого коммерческого упреждающего ядра, которое было проверено. ^[24]
  • Другие примеры включают библиотеку Ynot ^[25] для помощника доказательства Coq ; Holfoot вложения Smallfoot в HOL; Подробная логика параллельного разделения и Bedrock (библиотека Coq для низкоуровневого программирования).
• Между. Многие инструменты требуют большего вмешательства пользователя, чем анализ программы, поскольку они ожидают, что пользователь введет утверждения, такие как предварительные / последующие спецификации для функций или инварианты цикла, но после этого ввода они пытаются быть полностью или почти полностью автоматическими; Этот способ проверки восходит к классическим работам 1970-х годов, таким как верификатор Дж. Кинга и Стэнфордский верификатор Паскаля. Этот стиль верификатора недавно был назван автоматической активной верификацией , термин, который предназначен для обозначения способа взаимодействия с верификатором через цикл assert-check, аналогичный взаимодействию между программистом и проверкой типов.
  • Самый первый верификатор логики разделения, Смоллфут , находился в этой промежуточной категории. Это требовало, чтобы пользователь вводил спецификации до / после, инварианты цикла и инварианты ресурсов для блокировок. Он представил метод символического исполнения, а также автоматический способ вывода аксиом фрейма. Смоллфут включил логику параллельного разделения.
  • SmallfootRG - это средство проверки сочетания логики разделения и классического метода полагаться / гарантировать для параллельных программ.
  • Heap Hop реализует логику разделения для передачи сообщений, следуя идеям Singularity (операционная система) .
  • Verifast - это продвинутый текущий инструмент в промежуточной категории. Он продемонстрировал различные доказательства, начиная от объектно-ориентированных шаблонов и заканчивая алгоритмами с высокой степенью параллелизма и системными программами.
  • Язык программирования Mezzo и типы асинхронного разделения жидкости включают идеи, связанные с CSL в системе типов для языка программирования. Идея включения разделения в систему типов уже упоминалась в предыдущих примерах в статьях «Псевдонимы» и « Синтаксическое управление помехами» .

Различие между интерактивными и промежуточными верификаторами не является резким. Например, Bedrock стремится к высокой степени автоматизации в том, что он называет в основном автоматической проверкой, где Verifast иногда требует аннотаций, которые напоминают тактики (небольшие программы), используемые в интерактивных верификаторах.

Ссылки [ править ]