Свобода вмешательства
Метод параллельной проверки программ

В информатике свобода от помех — это метод доказательства частичной корректности параллельных программ с общими переменными. Логика Хоара была введена ранее для доказательства корректности последовательных программ. В своей докторской диссертации [1] (и работах, вытекающих из нее [ 2] [3] ) под руководством Дэвида Грайса Сьюзан Овицки распространила эту работу на параллельные программы.

Параллельное программирование использовалось с середины 1960-х годов для кодирования операционных систем как наборов параллельных процессов (см., в частности, Дейкстру. [4] ), но формального механизма для доказательства корректности не существовало. Рассуждения о чередующихся последовательностях выполнения отдельных процессов были сложными, подверженными ошибкам и не масштабировались. Свобода от помех применяется к доказательствам , а не к последовательностям выполнения; один показывает, что выполнение одного процесса не может мешать доказательству корректности другого процесса.

Целый ряд сложных параллельных программ были доказаны корректными с использованием свободы от помех, и свобода от помех обеспечивает основу для большей части последующей работы по разработке параллельных программ с общими переменными и доказательству их корректности. Статья Оуики-Гриса « Аксиоматическая техника доказательства для параллельных программ» [2] получила премию ACM Award 1977 года за лучшую статью в области языков и систем программирования. [5] [6]

Примечание. Лампорт [7] представляет похожую идею. Он пишет: «После написания первоначальной версии этой статьи мы узнали о недавней работе Оуики. [1] [2] «Его статья не привлекла столько внимания, как статья Оуики-Гриса, возможно, потому, что в ней использовались блок-схемы вместо текста программных конструкций, таких как оператор if и цикл while . Лампорт обобщал метод Флойда [8] , в то время как Оуики-Гриса обобщал метод Хоара. [9] По сути, все последующие работы в этой области используют текст, а не блок-схемы. Другое различие упоминается ниже в разделе о вспомогательных переменных.

Принцип невмешательства Дейкстры

Эдсгер В. Дейкстра ввел принцип невмешательства в EWD 117, «Программирование как человеческая деятельность», написанном около 1965 года. [10] Этот принцип гласит, что: Правильность целого может быть установлена, принимая во внимание только внешние спецификации (сокращенные спецификации по всему тексту) частей, а не их внутреннюю конструкцию. Дейкстра изложил общие шаги по использованию этого принципа:

  1. Дайте полную спецификацию каждой отдельной детали.
  2. Убедитесь, что проблема решена в целом, когда доступны части программы, соответствующие их спецификациям.
  3. Сконструируйте отдельные детали так, чтобы они соответствовали их спецификациям, но независимо друг от друга и от контекста, в котором они будут использоваться.

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

Спецификации программ написаны в логике Хоара , введенной сэром Тони Хоаром [9], как показано в спецификациях процессов S1 и S2 :

  {до S1 } {до S2 } S1 S2 {после S1 } {до S2 }     
                 
     

Значение: Если выполнение Si в состоянии, в котором предварительное условие pre-Si является истинным, завершается, то по завершении постусловие post-Si является истинным.

Теперь рассмотрим параллельное программирование с общими переменными. Спецификации двух (или более) процессов S1 и S2 даны в терминах их предварительных и постусловий, и мы предполагаем, что даны реализации S1 и S2 , которые удовлетворяют их спецификациям. Но при параллельном выполнении их реализаций, поскольку они совместно используют переменные, может возникнуть состояние гонки ; один процесс изменяет общую переменную на значение, которое не ожидается в доказательстве другого процесса, поэтому другой процесс не работает так, как предполагалось.

Таким образом, нарушается принцип невмешательства Дейкстры.

В своей докторской диссертации 1975 года [1] по информатике , Корнелльский университет , написанной под руководством Дэвида Грайса , Сьюзен Овицки разработала понятие свободы помех . Если процессы S1 и S2 удовлетворяют свободе помех, то их параллельное выполнение будет работать так, как и планировалось. Дейкстра назвал эту работу первым значительным шагом на пути к применению логики Хоара к параллельным процессам. [11] Для упрощения обсуждений мы ограничиваем внимание только двумя параллельными процессами, хотя Овицки-Грис [2] [3] допускает больше.

Свобода вмешательства в плане доказательств

Оуки-Грайс [2] [3] представил схему доказательства для тройки Хоара {P}S{Q }. Она содержит все детали, необходимые для доказательства корректности {P}S{Q } с использованием аксиом и правил вывода логики Хоара . (В этой работе используются оператор присваивания x: = e , операторы if-then и if-then-else , а также цикл while .) Хоар ссылался на схемы доказательства в своей ранней работе; для свободы от помех ее нужно было формализовать.

Схема доказательства для {P}S{Q } начинается с предусловия P и заканчивается постусловием Q. Два утверждения в фигурных скобках { и }, появляющиеся рядом друг с другом, указывают, что первое должно подразумевать второе.

Пример: Схема доказательства для {P} S {Q }, где S это:
x : = a; если e , то S1 , иначе S2

  {P } {P1[x/a] } x : = a; {P1 } если e , то {P1 ∧ e } S1 {Q1 } иначе {P1 ∧ ¬ e } S2 {Q1 } {Q1 } {Q }
  
  
  
  
                 
                 
        
                 
                 
  
  

Должно выполняться условие P ⇒ P1[x/a] , где P1[x/a] обозначает P1 , где каждое вхождение x заменено на a . (В этом примере S1 и S2 являются базовыми операторами, такими как оператор присваивания, skip или await .)

Каждому утверждению T в схеме доказательства предшествует предусловие pre-T и за ним следует постусловие post-T , и {pre-T}T{post-T } должно быть доказуемо с использованием некоторой аксиомы или правила вывода логики Хоара. Таким образом, схема доказательства содержит всю информацию, необходимую для доказательства того, что {P}S{Q } является правильным.

Теперь рассмотрим два процесса S1 и S2 , выполняемых параллельно, и их характеристики:

  {до S1 } {до S2 } S1 S2 {после S1 } {после S2 }     
                 
     

Доказательство того, что они работают параллельно, потребует ограничения их следующим образом. Каждое выражение E в S1 или S2 может ссылаться не более чем на одну переменную y , которая может быть изменена другим процессом во время вычисления E , и E может ссылаться на y не более одного раза. Аналогичное ограничение действует для операторов присваивания x: = E .

При таком соглашении единственным неделимым действием должна быть ссылка на память. Например, предположим, что процесс S1 ссылается на переменную y, в то время как S2 изменяет y . Значение, которое S1 получает для y, должно быть значением до или после того, как S2 изменяет y , а не каким-то ложным промежуточным значением.

Определение помехоустойчивости

Важным нововведением Овицки-Гриса было определение того, что означает, что утверждение T не мешает доказательству { P}S{Q }. Если выполнение T не может опровергнуть ни одно утверждение, данное в схеме доказательства {P}S{Q }, то это доказательство все еще остается в силе даже при одновременном выполнении S и T .

Определение . Утверждение T с предусловием pre-T не мешает доказательству {P}S{Q }, если выполняются два условия:

(1) {Q ∧ pre-T} T {Q }
(2) Пусть S' будет любым оператором внутри S , но не внутри оператора await (см. следующий раздел). Тогда {pre-S' ∧ pre-T} T {pre-S' }.

Прочитайте последнюю тройку Хоара следующим образом: если состояние таково, что могут быть выполнены как T , так и S' , то выполнение T не приведет к фальсификации pre-S' .

Определение . Схемы доказательства для {P1}S1{Q1 } и {P2}S2{Q2 } свободны от помех, если выполняется следующее. Пусть T — оператор await или присваивания (который не появляется в await ) процесса S1 . Тогда T не мешает доказательству {P2}S2{Q2 }. Аналогично для T процесса S2 и {P1}S1{Q1 }.

Заявления начинаются и ждут

Для решения проблемы параллелизма были введены два оператора. Выполнение оператора cobegin S1 // S2 coend выполняет S1 и S2 параллельно. Он завершается, когда оба S1 и S2 завершаются.

Выполнение оператора await await B then S откладывается до тех пор, пока условие B не станет истинным. Затем оператор S выполняется как неделимое действие — оценка B является частью этого неделимого действия. Если два процесса ожидают одного и того же условия B , когда оно становится истинным, один из них продолжает ждать, пока другой продолжает.

Оператор await не может быть реализован эффективно и не предлагается для вставки в язык программирования. Вместо этого он предоставляет средства представления нескольких стандартных примитивов, таких как семафоры — сначала выразите операции семафора как await s , а затем примените описанные здесь методы.

Правила вывода для await и cobegin следующие:

ждать
⁠{П ∧ Б} С {Q}/{P} ждем B , затем S {Q}⁠

cobegin ⁠
{P1} S1 {Q1}, {P2} S2 {Q2}
без помех/{P1∧P2} cobegin S1//S2 coend {Q1∧Q2}⁠

Вспомогательные переменные

Вспомогательная переменная не встречается в программе, но вводится в доказательство корректности, чтобы упростить рассуждения — или даже сделать их возможными. Вспомогательные переменные используются только при присвоении вспомогательных переменных, поэтому их введение не изменяет программу для каких-либо входных данных и не влияет на значения переменных программы. Обычно они используются либо как счетчики программ, либо для записи истории вычислений.

Определение . Пусть AV — набор переменных, которые появляются в S' только в назначениях x: = E , где x находится в AV . Тогда AV — вспомогательный набор переменных для S' .

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

  ⁠{П} С' {Q}/{П} С {Q}⁠

AV — это вспомогательный набор переменных для S' . Переменные в AV не встречаются в P или Q. S получается из S' путем удаления всех назначений переменным в AV .

Вместо использования вспомогательных переменных можно ввести в систему доказательства программный счетчик, но это усложнит систему доказательства.

Примечание: Апт [12] обсуждает логику Овицки-Гриса в контексте рекурсивных утверждений, то есть эффективно вычислимых утверждений. Он доказывает, что все утверждения в схемах доказательств могут быть рекурсивными, но это уже не так, если вспомогательные переменные используются только как счетчики программ, а не для записи истории вычислений. Лампорт в своей похожей работе [7] использует утверждения о позициях токенов вместо вспомогательных переменных, где токен на краю потоковой диаграммы сродни счетчику программ. Понятие переменной истории отсутствует. Это указывает на то, что подходы Овицки-Гриса и Лампорта не эквивалентны, когда ограничиваются рекурсивными утверждениями.

Тупик и прекращение

Овицки-Грайс [2] [3] в основном занимается частичной корректностью: {P} S {Q } означает: если S, выполненное в состоянии, в котором P истинно, завершается, то Q истинно для состояния по завершении. Однако Овицки-Грайс также приводит некоторые практические методы, которые используют информацию, полученную из доказательства частичной корректности, для вывода других свойств корректности, включая свободу от тупика, завершение программы и взаимное исключение.

Программа находится в тупике, если все процессы, которые не были завершены, выполняют операторы await и ни один из них не может продолжить работу, поскольку их условия await ложны. Оуики-Грайс предоставляет условия, при которых тупик не может возникнуть.

Овицки-Грайс представляет правило вывода для полной корректности цикла while . Оно использует связанную функцию, которая уменьшается с каждой итерацией и положительна, пока условие цикла истинно. Апт и др . [13] показывают, что это новое правило вывода не удовлетворяет свободе помех. Тот факт, что связанная функция положительна, пока условие цикла истинно, не был включен в тест на помехи. Они показывают два способа исправления этой ошибки.

Простой пример

Рассмотрим выражение:
       {x=0}
       cobegin await true then x: = x+1
                  // await true then x: = x+2
       coend
        {x=3}

Схема доказательства:

{х=0}
S: cobegin {x=0} {x=0 ∨ x=2} S1: await true then x : = x+1 {Q1: x=1 ∨ x=3} // {x=0} {x=0 ∨ x=1} S2: await true then x : = x+2 {Q2: x=2 ∨ x=3} coend
       
       
       
       
     
       
       
       
       
     
{(х=1 ∨ х=3) ∧ (х=2 ∨ х=3)}
{х=3}

Доказательство того, что S1 не мешает доказательству S2, требует доказательства двух троек Хоара:

(1) {(x=0 ∨ x=2) ∧ (x=0 ∨ x=1} S1 {x=0 ∨ x=1}
(2) {(x=0 ∨ x=2) ∧ (x=2 ∨ x=3} S1 {x=2 ∨ x=3}

Предварительное условие (1) сводится к x=0 , а предварительное условие (2) сводится к x=2 . Из этого легко видеть, что эти тройки Хоара выполняются. Для того, чтобы показать, что S2 не мешает доказательству S1 , требуются две подобные тройки Хоара .

Предположим, что S1 изменен с оператора await на присваивание x: = x+1 . Тогда схема доказательства не удовлетворяет требованиям, поскольку присваивание содержит два вхождения общей переменной x . Действительно, значение x после выполнения оператора cobegin может быть 2 или 3.

Предположим, что S1 изменен на оператор await await true then x: = x+2 , поэтому он такой же, как S2 . После выполнения S , x должен быть равен 4. Чтобы доказать это, поскольку два присваивания одинаковы, нужны две вспомогательные переменные: одна для указания того, был ли выполнен S1 ; другая — был ли выполнен S2 . Мы оставляем изменение в схеме доказательства читателю.

Примеры формально доказанных параллельных программ

A. Findpos . Напишите программу, которая находит первый положительный элемент массива (если он есть). Один процесс проверяет все элементы массива на четных позициях массива и завершается, когда находит положительное значение или когда ничего не найдено. Аналогично, другой процесс проверяет элементы массива на нечетных позициях массива. Таким образом, этот пример имеет дело с циклами while . Он также не имеет операторов await .

Этот пример взят из работы Барри К. Розена. [14] Решение в Owicki-Gries, [2] полное с программой, планом доказательства и обсуждением свободы помех, занимает менее двух страниц. Свободу помех довольно легко проверить, поскольку есть только одна общая переменная. Напротив, статья Розена [14] использует Findpos как единственный, работающий пример в этой 24-страничной статье.

Схема обоих процессов в общей среде:

cobegin производитель: ... ожидание in-out < N затем пропуск ; добавить: b[in mod N]:= следующее значение; markin: in: = in+1; ... // потребитель: ... ожидание in-out > 0 затем пропуск ; удалить: это значение:= b[out mod N]; markout: out: = out+1;
     
     
     
     
  
     
     
     
       
     
коенд
...

B. Проблема потребителя/производителя с ограниченным буфером . Процесс-производитель генерирует значения и помещает их в ограниченный буфер b размером N ; процесс-потребитель удаляет их. Они выполняются с переменной скоростью. Производитель должен ждать, если буфер b полон; потребитель должен ждать, если буфер b пуст. В Овицки-Гриесе [2] показано решение в общей среде; затем оно встраивается в программу, которая копирует массив c[1..M] в массив d[1..M] .

Этот пример демонстрирует принцип сведения проверок помех к минимуму: поместите как можно больше в утверждение, которое инвариантно истинно везде в обоих процессах. В этом случае утверждение является определением ограниченного буфера и границ переменных, которые указывают, сколько значений было добавлено в буфер и удалено из него. Помимо самого буфера b , две общие переменные записывают количество значений , добавленных в буфер, и количество удаленных из буфера.

C. Реализация семафоров . В своей статье о системе мультипрограммирования THE [4] Дейкстра представляет семафор sem как примитив синхронизации: sem — это целочисленная переменная, на которую можно ссылаться только двумя способами, показанными ниже; каждый из них является неделимой операцией:

1. P(sem) : Уменьшить sem на 1. Если теперь sem < 0 , приостановить процесс и поместить его в список приостановленных процессов, связанных с sem .

2. V(sem) : Увеличить sem на 1. Если теперь sem ≤ 0 , удалить один из процессов из списка приостановленных процессов, связанных с sem , чтобы его динамическое выполнение снова стало допустимым.

Реализация P и V с использованием операторов await выглядит следующим образом:

P(sem): ожидание true затем начало sem: = sem-1; если sem < 0 тогда w[этот процесс]: = true конец ; ожидание ¬w[этот процесс] затем пропуск
      
          
              
                
          
          
                

V(sem): ожидание true затем начало sem: = sem+1; если sem ≤ 0 , то начало выбрать p так , чтобы w[ p ]; w[ p ]: = false конец конец
      
          
              
                 
                                   
                            
                 
          

Здесь w — массив процессов, которые ждут, поскольку они были приостановлены; изначально w[p] = false для каждого процесса p . Можно изменить реализацию, чтобы всегда пробуждать самый долго приостановленный процесс.

D. Сборка мусора «на лету» . На летней школе в Марктобердорфе в 1975 году Дейкстра обсуждал сборщик мусора «на лету» как упражнение по пониманию параллелизма. Структура данных, используемая в обычной реализации LISP, представляет собой направленный граф, в котором каждый узел имеет не более двух исходящих ребер, каждое из которых может отсутствовать: исходящее левое ребро и исходящее правое ребро. Все узлы графа должны быть достижимы из известного корня. Изменение узла может привести к появлению недоступных узлов, которые больше не могут использоваться и называются мусором . Сборщик мусора «на лету» имеет два процесса: саму программу и сборщик мусора, задача которого — идентифицировать мусорные узлы и помещать их в свободный список, чтобы их можно было использовать снова.

Грайс чувствовал, что свободу вмешательства можно использовать для доказательства правильности сборщика мусора на лету. С помощью Дейкстры и Хоара он смог сделать презентацию в конце Летней школы, которая вылилась в статью в CACM. [15]

E. Проверка решения читатели/писатели с помощью семафоров . Куртуа и др. [16] используют семафоры, чтобы дать две версии проблемы читатели/писатели, без доказательства. Операции записи блокируют как чтение, так и запись, но операции чтения могут выполняться параллельно. Овицки [17] приводит доказательство.

Алгоритм Ф. Петерсона , решение проблемы взаимного исключения двух процессов, был опубликован Петерсоном в двухстраничной статье. [18] Шнайдер и Эндрюс приводят доказательство корректности. [19]

Зависимости от свободы вмешательства

Изображение ниже, Ильи Сергея, изображает поток идей, которые были реализованы в логике, которая имеет дело с параллелизмом. В корне лежит свобода от помех. Файл CSL-Family-Tree (PDF)содержит ссылки. Ниже мы суммируем основные достижения.

Исторический график логики программы для свободы от помех
Исторический график логики программы для свободы от помех
  • Rely-Guarantee . 1981. Свобода от помех не является композиционной. Клифф Джонс [20] [21] восстанавливает композиционность, абстрагируя помехи в два новых предиката в спецификации: условие Rely записывает, какие помехи поток должен быть в состоянии выдержать, а условие Guarantee устанавливает верхнюю границу помех, которые поток может нанести своим родственным потокам. Сюй и др . [22] отмечают, что Rely-Guarantee — это переформулировка свободы от помех; они говорят, что выявление связи между этими двумя методами дает глубокое понимание проверки программ с общими переменными.
  • CSL . 2004. Логика разделения поддерживает локальные рассуждения, посредством которых спецификации и доказательства программного компонента упоминают только часть памяти, используемую компонентом. Логика параллельного разделения (CSL) была первоначально предложена Питером О'Хирном , [23] [24] Мы цитируем: [23] «метод Оуки-Грайса [2] включает явную проверку отсутствия помех между компонентами программы, в то время как наша система исключает помехи неявным образом, по природе способа, которым строятся доказательства».
  • Вывод параллельных программ . 2005-2007. Фейен и ван Гастерен [25] показывают, как использовать Оуики-Гриса для проектирования параллельных программ, но отсутствие теории прогресса означает, что проекты обусловлены только требованиями безопасности . Донгол, Голдсон, Муидж и Хейс расширили эту работу, включив «логику прогресса», основанную на языке Чанди и Мисры Unity , сформированном для соответствия модели последовательного программирования. Донгель и Голдсон [26] описывают свою логику прогресса. Голдсон и Донгол [27] показывают, как эта логика используется для улучшения процесса проектирования программ, используя в качестве примера алгоритм Деккера для двух процессов. Донгол и Муидж [28] представляют больше методов для вывода программ, используя в качестве одного из примеров алгоритм взаимного исключения Петерсона . Донгол и Муидж [29] показывают, как сократить вычислительные издержки в формальных доказательствах и выводах и снова вывести алгоритм Деккера, что приводит к некоторым новым и более простым вариантам алгоритма. Муидж [30] изучает вычислительные правила для отношения «приводит к» Unity . Наконец, Донгол и Хейс [31] предоставляют теоретическую основу и доказывают обоснованность логики процесса.
  • OGRA . 2015. Лахав и Вафейадис усиливают проверку свободы вмешательства, чтобы создать (цитируем из аннотации) «OGRA, программную логику, которая является надежной для рассуждений о программах во фрагменте освобождения-получения модели памяти C11». Они приводят несколько примеров ее использования, включая реализацию примитивов синхронизации RCU. [32]
  • Квантовое программирование . 2018. Ин и др. [33] распространяют свободу помех на квантовое программирование. Трудности, с которыми они сталкиваются, включают переплетенный недетерминизм: недетерминизм, включающий квантовые измерения, и недетерминизм, введенный параллелизмом, происходящим в одно и то же время. Авторы формально проверяют параллельный квантовый алгоритм Бравого-Госсета-Кёнига, решающий задачу линейной алгебры, давая, как они говорят, впервые безусловное доказательство вычислительного квантового преимущества.
  • POG . 2020. Раад и др. представляют POG (Persistent Owicki-Gries), первую программную логику для рассуждений о технологиях энергонезависимой памяти, в частности Intel-x86. [34]

Тексты, в которых обсуждается свобода вмешательства

  • О методе мультипрограммирования , 1999. [25] Ван Гастерен и Фейен обсуждают формальную разработку параллельных программ исключительно на основе идеи свободы от помех.
  • On Current Programming , 1997. [35] Шнайдер использует свободу от помех как основной инструмент при разработке и доказательстве параллельных программ. Дается связь с темпоральной логикой, поэтому могут быть доказаны произвольные свойства безопасности и жизнеспособности. Управляющие предикаты устраняют необходимость во вспомогательных переменных для рассуждений о счетчиках программ.
  • Проверка последовательных и параллельных программ , 1991, [36] 2009. [37] Этот первый текст, посвященный проверке структурированных параллельных программ, написанный Аптом и др ., выдержал несколько изданий за несколько десятилетий.
  • Проверка параллельности: введение в композиционные и некомпозиционные методы , 2112. [38] Де Роевер и др. предоставляют систематическое и всестороннее введение в композиционные и некомпозиционные методы доказательства для проверки параллельных программ на основе состояний.

Реализации свободы вмешательства

  • 1999: Нипков и Нието представляют первую формализацию свободы вмешательства и ее композиционную версию, метод «rely-gurantee», в программе для доказательства теорем: Isabelle/HOL. [39] [40]
  • 2005: Кандидатская диссертация Абрахама предлагает способ доказательства корректности многопоточных программ на Java в три этапа: (1) аннотирование программы для создания схемы доказательства, (2) использование их инструмента Verger для автоматического создания условий проверки и (3) использование средства доказательства теорем PVS для интерактивного доказательства условий проверки. [41] [42]
  • 2017: Дениссен [43] сообщает о реализации Овицки-Гриса в «готовом к проверке» языке программирования Dafny . [44] Дениссен отмечает простоту использования Dafny и его расширения, что делает его чрезвычайно подходящим для обучения студентов свободе вмешательства. Его простота и интуитивность перевешивают недостаток некомпозиционности. Он перечисляет около двадцати учреждений, которые обучают свободе вмешательства.
  • 2017: Амани и др. объединяют подходы Hoare-Parallel, формализацию Owicki-Gries в Isabelle/HOL для простого while-языка, и SIMPL, универсального языка, встроенного в Isabelle/HOL, для обеспечения формального рассуждения в программах на языке C. [45]
  • 2022: Далванди и др. представляют первую среду дедуктивной проверки в Isabelle/HOL для программ со слабой памятью типа C11, основанную на кодировании Нипкова и Нието Овицки-Гриса в доказательстве теоремы Изабеллы. [46]
  • 2022: На этой веб-странице [47] описывается верификатор Civl для параллельных программ и даются инструкции по его установке на ваш компьютер. Он построен на основе Boogie, верификатора для последовательных программ. Крагл и др. [48] описывают, как в Civl достигается свобода от помех с помощью их новой идиомы спецификации yield invariants . Можно также использовать спецификации в стиле Rely-Guarantee. Civl предлагает комбинацию линейной типизации и логики, которая позволяет экономично и локально рассуждать о непересекаемости (например, логике разделения). Civl — первая система, которая предлагает уточненные рассуждения для структурированных параллельных программ.
  • 2022. Эсен и Рюммер разработали TRICERA, [49] автоматизированный инструмент проверки с открытым исходным кодом для программ на языке C. Он основан на концепции ограниченных предложений Хорна и обрабатывает программы, работающие в куче, используя теорию куч. Доступен веб-интерфейс для его онлайн-тестирования. Для обработки параллелизма TRICERA использует вариант правил доказательства Овицки-Гриса с явными переменными, добавляемыми для представления времени и часов.

Ссылки

  1. ^ abc Owicki, Susan S. (август 1975). Методы аксиоматического доказательства для параллельных программ (диссертация на степень доктора философии). Корнелльский университет. hdl :1813/6393 . Получено 01.07.2022 .
  2. ^ abcdefghi Овицки, Сьюзен ; Грис, Дэвид (25 июня 1976 г.). "Метод аксиоматического доказательства для параллельных программ I". Acta Informatica . 6 (4). Берлин: Springer (Германия): 319– 340. doi :10.1007/BF00268134. S2CID  206773583.
  3. ^ abcd Овицки, Сьюзен ; Грайс, Дэвид (май 1976). «Проверка свойств параллельных программ: аксиоматический подход». Сообщения ACM . 19 (5): 279– 285. doi : 10.1145/360051.360224 . S2CID  9099351.
  4. ^ ab Dijkstra, EW (1968), «Структура мультипрограммной системы „THE“», Communications of the ACM , 11 (5): 341– 346, doi : 10.1145/363095.363143 , S2CID  2021311
  5. ^ "Susan S Owicki". Awards.acm.org . Получено 2022-07-01 .
  6. ^ "Дэвид Грайс". Awards.acm.org . Получено 01.07.2022 .
  7. ^ ab Lamport, Leslie (март 1977 г.). «Доказательство корректности многопроцессных программ». IEEE Transactions on Software Engineering . SE-3 (2): 125– 143. doi :10.1109/TSE.1977.229904. S2CID  9985552.
  8. ^ Флойд, Роберт В. (1967). «Присвоение значений программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты компьютерной науки. Труды симпозиума по прикладной математике. Том 19. Американское математическое общество. С.  19–32 . ISBN 0821867288.
  9. ^ ab Hoare, CAR (октябрь 1969). "Аксиоматическая основа компьютерного программирования". Communications of the ACM . 12 (10): 576– 580. doi : 10.1145/363235.363259 . S2CID  207726175.
  10. ^ "Программирование как человеческая деятельность" (PDF) . Архив Э. В. Дейкстры . Техасский университет.
  11. ^ Дейкстра, Эдсгер В. (1982). "EWD 554: Персональное резюме теории Гриса-Овицкого". Избранные труды по вычислениям: Персональная точка зрения . Монографии по информатике. Springer-Verlag. С.  188–199 . ISBN 0387906525.
  12. ^ Апт, Кшиштоф Р. (июнь 1981 г.). «Рекурсивные утверждения и параллельные программы». Acta Informatica . 15 (3): 219– 232. doi :10.1007/BF00289262. S2CID  42470032.
  13. ^ Апт, Кшиштоф Р.; де Бур, Фрэнк С.; Ольдерог, Эрнст-Рюдигер (1990). «Доказательство завершения параллельных программ». В Грис, Д.; Фейен, WHJ; ван Гастерен, AJM; Мисра, Дж. (ред.). Красота – это наш бизнес. Монографии по информатике. Нью-Йорк: Springer Verlag. стр.  0–6 . doi : 10.1007/978-1-4612-4476-9. ISBN 978-1-4612-8792-6. S2CID  24379938.
  14. ^ ab Rosen, Barry K (1976). «Корректность параллельных программ: подход Чёрча-Россера». Теоретическая информатика . 2 (2): 183– 207. doi : 10.1016/0304-3975(76)90032-3 .
  15. ^ Грайс, Дэвид (декабрь 1977 г.). «Упражнение по доказательству корректности параллельных программ». Сообщения ACM . 20 (12): 921– 930. doi : 10.1145/359897.359903 . S2CID  3202388.
  16. ^ Куртуа, П. Дж.; Хейманс, Ф.; Парнас, Д. Л. (октябрь 1971 г.). «Одновременное управление с помощью «читателей» и «писателей»». Сообщения ACM . 14 (10): 667– 668. doi : 10.1145/362759.362813 . S2CID  7540747.
  17. ^ Овицки, Сьюзен (август 1977 г.). Проверка параллельных программ с разделяемыми классами данных (PDF) (Технический отчет). Лаборатория цифровых систем, Стэнфордский университет. 147 . Получено 2022-07-08 .
  18. ^ Петерсон, Гэри Л. (июнь 1981 г.). «Мифы о проблеме взаимного исключения». IPL . 12 (3): 115– 116. doi :10.1016/0020-0190(81)90106-X.
  19. ^ Шнайдер, Фред Б .; Эндрюс, Грегори Р. (1986). «Концепции параллельного программирования». В JW Bakker; WP de Roever; G. Rozenberg (ред.). Современные тенденции в параллелизме . Конспект лекций по информатике. Том 224. Нордвейкерхаут, Нидерланды: Springer Verlag . С.  669–716 . doi :10.1007/BFb0027049. ISBN 978-3-540-16488-3.
  20. ^ Джонс, К. Б. (июнь 1981 г.). Методы разработки компьютерных программ, включая понятие помех (PDF) (диссертация на степень доктора философии). Оксфордский университет.
  21. ^ Джонс, Клифф Б. (1983). REA Mason (ред.). Спецификация и проектирование (параллельных) программ . 9-й Всемирный компьютерный конгресс IFIP (Обработка информации 83). North-Holland/IFIP. стр.  321–332 . ISBN 0444867295.
  22. ^ Сюй, Цивэнь; де Ровер, Виллем-Пол; Хе, Цзифэн (1997). «Метод Rely-Guarantee для проверки параллельных программ с разделяемыми переменными». Формальные аспекты вычислений . 9 (2): 149– 174. doi : 10.1007/BF01211617 . S2CID  12148448.
  23. ^ ab O'Hearn, Peter W. (2004-09-03). "Ресурсы, параллелизм и локальные рассуждения". В P. Gardner; N. Yoshida (ред.). CONCUR 2004 -- Теория параллелизма . CONCUR 2004. Лондон, Великобритания: Springer Verlag Berlin, Heidelberg. стр.  49–67 . doi :10.1007/b100113. ISBN 978-3-540-28644-8. Получено 2022-07-06 .
  24. ^ О'Херн, Питер (2007). "Ресурсы, параллелизм и локальные рассуждения" (PDF) . Теоретическая информатика . 375 ( 1– 3): 271– 307. doi : 10.1016/j.tcs.2006.12.035 .
  25. ^ аб Ван Гастерен, AJM; Фейен, WHJ (1999). Грис, Дэвид ; Шнайдер, Фред Б. (ред.). Об одном методе мультипрограммирования . Монографии по информатике. Springer-Verlag New York Inc. с. 370. дои : 10.1007/978-1-4757-3126-2. ISBN 978-1-4757-3126-2. S2CID  13607884.
  26. ^ Донгол, Брижеш; Голдсон, Дуг (2006) [12 января 2005 г.]. «Расширение теории Овицкого и Грайса с помощью логики прогресса». Логические методы в информатике . 2. Центр прямой научной коммуникации (CCSD). arXiv : cs/0512012v3 . doi :10.2168/lmcs-2(1:6)2006. S2CID  302420.
  27. ^ Голдсон, Дуг; Донгол, Бриджеш (январь 2005 г.). «Проектирование параллельных программ в расширенной теории Оуки и Грайса». В работе Майка Аткинсона; Фрэнка Дене (ред.). CATS '05: Proc 2005 Australasian Symp on Theory of Computing . Том 41. Australian Computer Society, Inc., стр.  41–50 .
  28. ^ Dongol, Brijesh; Mooij, Arjan J (июль 2006 г.). «Прогресс в получении параллельных программ: подчеркивание роли стабильных охранников». В Tarmo Uustalu (ред.). MPC'06: Proc. 8th Int. Conf. on Mathematics of Program Construction . Vol. 41. Курессааре , Эстония : Springer Verlag , Берлин, Гейдельберг. стр.  14–161 . doi :10.1007/11783596_11.
  29. ^ Донгол, Бриджеш; Муидж, Арджан Дж (2008). «Оптимизация основанных на прогрессе выводов параллельных программ». Формальные аспекты вычислений . 20 (2): 141– 160. doi : 10.1007/s00165-007-0037-4 . S2CID  7024064.
  30. ^ Mooij, Arjan J. (ноябрь 2007 г.). «Расчет и составление свойств прогресса в терминах отношения «приводит к». В Michael Butler; Michael G. Hinchey; María M. Larrondo-Petrie (ред.). ICFEM'07: Proc. Formal Engineering Methods 9th Int. Conf. on Formal Methods and Software Engineering . Boca Raton, Florida: Springer Verlag , Berlin, Heidelberg. стр.  366–386 . ISBN 978-3540766483.
  31. ^ Донгол, Бриджеш; Хейс, Ян (апрель 2007 г.). Семантика трассировки для теории Оуики-Грайса, интегрированная с логикой прогресса из UNITY (PDF) (Технический отчет). Университет Квинсленда . SSE-2007-02.
  32. ^ Lahav, Ori; Vafeiadis, Viktor (2015). «Рассуждения Овицкого-Гриса для моделей со слабой памятью». В Halldórsson, M.; Iwama, K.; Kobayashi, N.; Speckmann, B. (ред.). Автоматы, языки и программирование. ICALP 2015. ICALP 2015. Lecture Notes in Computer Science. Vol. 9135. Berlin, Heidelberg: Springer. pp.  311– 323. doi :10.1007/978-3-662-47666-6_25.
  33. ^ Инь, Миншэн; Чжоу, Ли; Ли, Янцзя (2018). «Рассуждения о параллельных квантовых программах». arXiv : 1810.11334 [cs.LO].
  34. ^ Раад, Азалия; Лахав, Ори; Вафейадис, Виктор (13 ноября 2020 г.). «Постоянное рассуждение Овицкого-Гриса: программная логика для рассуждений о постоянных программах на Intel-x86». Труды ACM по языкам программирования . Том 4. ACM . С.  1–28 . doi : 10.1145/3428219 . hdl : 10044/1/97398 .
  35. ^ Шнайдер, Фред Б. (1997). Грайс, Дэвид ; Шнайдер, Фред Б. (ред.). О параллельном программировании . Graduate Texts in Computer Science. Springer-Verlag New York Inc. doi :10.1007/978-1-4612-1830-2. ISBN 978-1-4612-1830-2. S2CID  9980317.
  36. ^ Апт, Кшиштоф Р.; Ольдерог, Эрнст-Рюдигер (1991). Грайс, Дэвид (ред.). Верификация последовательных и параллельных программ . Тексты по информатике. Шпрингер-Верлаг Германия.
  37. ^ Apt, Krzysztof R.; Boer, Frank S.; Olderog, Ernst-Rüdiger (2009). Gries, David ; Schneider, Fred B. (ред.). Verification of Sequential and Concurrent Programs. Texts in Computer Science (3-е изд.). Springer-Verlag London. стр. 502. Bibcode :2009vscp.book.....A. doi :10.1007/978-1-84882-745-5. ISBN 978-1-84882-744-8.
  38. ^ де Ровер, Виллем-Поль; де Бур, Виллем-Поль; Ханнеман, Ульрих; Хуман, Йозеф; Лахнех, Ясин; Поэль, Маннес; Цвирс, Иов (2012). Абрамский С. (ред.). Проверка параллелизма: введение в композиционные и некомпозиционные методы . Кембриджские трактаты по теоретической информатике. Издательство Кембриджского университета, США. п. 800. ISBN 978-0521169325.
  39. ^ Nieto, Leonor Prensa (2002-01-31). Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL (PhD диссертация). Technischen Universitaet Muenchen. стр. 198. Получено 2022-07-05 .
  40. ^ Нипков, Тобиас; Нието, Леонор Пренса (1999-03-22). "Owicki/Gries in Isabelle/HOL". В JP Finance (ред.). Фундаментальные подходы к программной инженерии . FASE 1999. Конспект лекций по информатике. Том 1577. Берлин-Гейдельберг: Springer Verlag . С.  188–203 . doi : 10.1007/978-3-540-49020-3_13 . ISBN 978-3-540-49020-3.
  41. ^ Абрахам, Эрика (2005-01-20). Система доказательств утверждений для многопоточной Java - теория и поддержка инструментов (диссертация). Universiteit Leiden. стр. 220. hdl :1887/584. ISBN 9090189084. Получено 2022-07-05 .
  42. ^ Абрахам, Эрика; Бур, Франк, С., де; Ровер, Виллем-Пол, де; Мартин, Штеффен (2005-02-25). "Система доказательств на основе утверждений для многопоточной Java". Теоретическая информатика . 331 ( 2–3 ). Elsevier : 251–290 . doi : 10.1016/j.tcs.2004.09.019 .{{cite journal}}: CS1 maint: несколько имен: список авторов ( ссылка )
  43. ^ Denissen, PEJG (ноябрь 2017 г.). Расширение Dafny для параллелизма: верификация программ в стиле Овицкого-Гриса для верификатора программ Dafny (магистерская диссертация). Технический университет Эйндховена.
  44. ^ "Язык программирования Dafny" . Получено 20 июля 2022 г. .
  45. ^ Amani, S.; Andronick, J.; Bortin, M.; Lewis, C.; Rizkallah, C.; Tuong, J. (16 января 2017 г.). Yves Bertot; Viktor Vafeiadid (ред.). COMPLX: структура проверки для параллельных императивных программ. CPP 2017: Proc 6th ACM SIGPLAN Conference on Certified Programs and Proof. Париж, Франция: ACM . стр.  138–150 . doi :10.1145/3018610.3018627. ISBN 978-1-4503-4705-1.
  46. ^ Далванди, Садег; Донгол, Бриджеш; Доэрти, Саймон; Верхайм, Хайке (февраль 2022 г.). «Интеграция моделей памяти Овицкого–Гриса для C11-стиля в Isabelle/HOL». Журнал автоматизированного рассуждения . 66 : 141– 171. arXiv : 2004.02983 . doi : 10.1007/s10817-021-09610-2 . S2CID  215238874.
  47. ^ "Civl: Верификатор для параллельных программ" . Получено 2022-07-22 .
  48. ^ Крагл, Бернхард; Кадир, Шаз; Хензингер, Томас А. (2020). «Уточнение для структурированных параллельных программ». В S. Lahiri; C. Wang (ред.). CAV 2020: Computer Aided Verification . Lecture Notes in Computer Science. Vol. 12224. Springer Verlag . doi : 10.1007/978-3-030-53288-8_14 . ISBN 978-3-030-53288-8.
  49. ^ Эсен, Зафер; Рюммер, Филипп (октябрь 2022 г.). «TRICERA Verifying C Programs Using the Theory of Heaps» (Проверка программ на языке C с использованием теории куч). В A. Griggio; N. Rungta (ред.). Proc. 22nd Conf. on Formal Methods in Computer-Aided Design – FMCAD 2022. TU Wien Academic Press. стр.  360–391 . doi : 10.34727/2022/isbn.978-3-85448-053-2_45 .
Взято с "https://en.wikipedia.org/w/index.php?title=Interference_freedom&oldid=1241387975"