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

В информатике логика разделения — это расширение логики Хоара , способ рассуждения о программах.Его разработали Джон К. Рейнольдс , Питер О'Хирн , Самин Иштиак и Хонсок Ян. опираясь на ранние работы Рода Берстолла . Язык утверждений логики разделения является частным случаем логики группированных импликаций (BI). Обзорная статья CACM О'Хирна описывает развитие этой темы до начала 2019 года.

Обзор

Логика разделения облегчает рассуждения о:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

мы получаем самое слабое предварительное условие для оператора, который изменяет кучу в месте $x$, и это работает для любого постусловия, а не только для того, которое аккуратно составлено с помощью разделительного союза. Эта идея была развита Янгом гораздо дальше, который использовал ${-\!\!*}$ предоставить локализованные рассуждения о мутациях в классическом алгоритме разметки графов Шорра-Уэйта . Наконец, одна из последних работ в этом направлении принадлежит Хобору и Виллару. ВОЗ нанимать не только ${-\!\!*}$ но и связующее $\cup \,\!\!\!\!\!*$который по-разному называли перекрывающимся союзом или сепишом, и который можно использовать для описания перекрывающихся структур данных: $P\cup \!\!\!\!\!*Q$ держит кучу $h$ когда $P$ и $Q$ удерживать для подкучек $h_{P}$ и $h_{Q}$ чей союз $h$, но которые, возможно, имеют непустую часть $h_{P}\cap h_{Q}$ в общем. Абстрактно, $P\cup \!\!\!\!\!*Q$ можно рассматривать как версию слитной связки логики релевантности .

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

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

${\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}\}}}$

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

Комментируя раннюю классическую работу Сьюзан Овики и Дэвида Грайса о говорит свободе вмешательства , О'Хирн , что явная проверка невмешательства не является необходимой, поскольку его система исключает вмешательство неявным образом, по природе способа доказательства. построен.

Модель логики параллельного разделения была впервые предложена Стивеном Бруксом в сопутствующей статье, опубликованной в журнале O'Hearn's. Правильность логики была сложной проблемой, и фактически контрпример Джона Рейнольдса показал несостоятельность более ранней, неопубликованной версии логики; Проблема, поднятая примером Рейнольдса, кратко описана в статье О'Хирна и более подробно в статье Брукса.

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

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

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

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

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

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

• Автоматический анализ программы. Эти инструменты обычно ищут ограниченные классы ошибок (например, ошибки безопасности памяти) или пытаются доказать их отсутствие, но не могут доказать полную правильность.
  • Текущий пример — Facebook Infer , инструмент статического анализа для Java, C и Objective-C, основанный на логике разделения и биабдукции. По состоянию на 2015 год компания Infer обнаруживала и исправляла сотни ошибок в месяц перед отправкой в ​​мобильные приложения Facebook.
  • Другие примеры включают SpaceInvader (один из первых анализаторов SL), Predator (выигравший несколько конкурсов по проверке), MemCAD (который сочетает в себе форму и числовые свойства) и SLAyer (от Microsoft Research, ориентированный на структуры данных, обнаруженные в драйверах устройств).
• Интерактивное доказательство. Доказательства проводились с использованием встраивания логики разделения в интерактивные средства доказательства теорем, такие как помощник доказательства Coq и HOL (помощник доказательства) . По сравнению с работой по анализу программ, эти инструменты требуют больше человеческих усилий, но обладают более глубокими свойствами, вплоть до функциональной корректности.
  • Доказательство файловой системы FSCQ где спецификация включает поведение при сбоях, а также нормальную работу. Эта работа получила награду за лучший доклад на Симпозиуме по принципам операционной системы 2015 года.
  • Верификация большого фрагмента системы типов Rust и некоторых ее стандартных библиотек в проекте RustBelt с использованием фреймворка Iris для логики разделения в The Coqproof Assistant .
  • Проверка реализации OpenSSL алгоритма криптографической аутентификации, используя проверяемый C
  • Верификация ключевых модулей коммерческого ядра ОС, ядра μC/OS-II, первого коммерческого упреждающего ядра, которое было проверено.
  • Другие примеры включают Ynot библиотека для помощника по корректуре Coq ; встраивание Смолфута Холфутом в HOL; Мелкозернистая логика параллельного разделения и Bedrock (библиотека Coq для низкоуровневого программирования).
• Между. Многие инструменты требуют большего вмешательства пользователя, чем программный анализ, поскольку они ожидают, что пользователь введет утверждения, такие как спецификации до / после для функций или инварианты цикла, но после этого ввода они пытаются быть полностью или почти полностью автоматическими; этот способ проверки восходит к классическим работам 1970-х годов, таким как верификатор Дж. Кинга и верификатор Стэнфордского Паскаля. Этот стиль верификатора недавно был назван автоматической активной проверкой , термин, который призван обозначить способ взаимодействия с верификатором через цикл проверки утверждений, аналогичный взаимодействию между программистом и проверкой типов.
  • Самый первый верификатор Логики Разделения, Смоллфут , находился в этой промежуточной категории. От пользователя требовалось ввести спецификации до и после, инварианты циклов и инварианты ресурсов для блокировок. Он представил метод символического выполнения, а также автоматический способ вывода аксиом фрейма. Смоллфут включил параллельную логику разделения.
  • SmallfootRG — это средство проверки сочетания логики разделения и классического метода доверия/гарантии для параллельных программ.
  • Heap Hop реализует логику разделения для передачи сообщений, следуя идеям Singularity (операционной системы) .
  • VeriFast — это современный современный инструмент промежуточной категории. Он продемонстрировал доказательства, начиная от объектно-ориентированных шаблонов и заканчивая высококонкурентными алгоритмами и системными программами.
  • Viper — это современная автоматизированная инфраструктура проверки для рассуждений на основе разрешений. В основном он состоит из языка программирования и двух механизмов проверки: одна основана на символьном выполнении, а другая — на генерации условий проверки (VCG). На базе инфраструктуры Viper появилось несколько интерфейсов для различных языков программирования: Gobra для Go, Nagini для Python, Prusti для Rust и VerCors для C, Java, OpenCL и OpenMP. Эти внешние интерфейсы переводят язык программирования внешнего интерфейса в Viper, чтобы затем использовать серверную часть проверки Viper для подтверждения правильности входной программы.
  • Язык программирования Mezzo и типы асинхронного разделения жидкостей включают идеи, связанные с CSL, в системе типов языка программирования. Идея включить разделение в систему типов уже имела более ранние примеры в разделах «Псевдонимы типов» и «Синтаксический контроль интерференции» .

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

Разрешимость и сложность

Можно показать, что проблема выполнимости для многосортированного фрагмента логики разделения без кванторов, параметризованного по типам местоположений и данных, является PSPACE-полной . Алгоритм решения этого фрагмента в DPLL(T) на основе решателях SMT был интегрирован в cvc5 . Расширяя этот результат, можно также показать, что выполнимость аналога класса Бернейса – Шенфинкеля для логики разделения с неинтерпретируемыми ячейками памяти является PSPACE-полной, тогда как проблема неразрешима с интерпретируемыми ячейками памяти (например, целыми числами) или дальнейшими изменениями кванторов.