Wolność od zakłóceń

W informatyce swoboda interferencji jest techniką dowodzenia częściowej poprawności współbieżnych programów ze wspólnymi zmiennymi . Logika Hoare'a została wprowadzona wcześniej, aby udowodnić poprawność programów sekwencyjnych. W swojej rozprawie doktorskiej (i dokumentach z niej wynikających) pod kierunkiem doradcy Davida Griesa Susan Owicki rozszerzyła tę pracę, aby zastosować ją do programów równoległych .

Programowanie współbieżne było używane od połowy lat sześćdziesiątych XX wieku do kodowania systemów operacyjnych jako zestawów współbieżnych procesów (patrz w szczególności Dijkstra.), Ale nie było formalnego mechanizmu dowodzenia poprawności. Rozumowanie na temat przeplatanych sekwencji wykonywania poszczególnych procesów było trudne, podatne na błędy i nie zwiększało skali. Swoboda ingerencji dotyczy dowodów zamiast sekwencji wykonania; jeden pokazuje, że wykonanie jednego procesu nie może kolidować z dowodem poprawności innego procesu.

Udowodniono poprawność szeregu skomplikowanych programów współbieżnych przy użyciu swobody interferencji, a wolność interferencji stanowi podstawę wielu późniejszych prac nad opracowywaniem programów współbieżnych ze wspólnymi zmiennymi i udowadnianiem ich poprawności. Artykuł Owickiego-Griesa Technika dowodu aksjomatycznego dla programów równoległych W 1977 roku otrzymałem nagrodę ACM Award za najlepszą pracę w językach i systemach programowania.

Notatka. Podobny pomysł przedstawia Lamport . Pisze: „Po napisaniu wstępnej wersji tego artykułu dowiedzieliśmy się o ostatnich pracach Owickiego”. Jego artykuł nie spotkał się z tak dużym zainteresowaniem jak Owicki-Gries, być może dlatego, że zamiast tekstu konstrukcji programistycznych, takich jak if i pętla while , użyto schematów blokowych. Lamport uogólniał Floyda , podczas gdy Owicki-Gries uogólniał metodę Hoare'a. Zasadniczo wszystkie późniejsze prace w tej dziedzinie wykorzystują tekst, a nie schematy blokowe. Kolejna różnica jest wymieniona poniżej w sekcji dotyczącej Zmienne pomocnicze .

Zasada nieingerencji Dijkstry

Edsger W. Dijkstra wprowadził zasadę nieingerencji w EWD 117, „Programowanie uważane za działalność ludzką”, napisanym około 1965 r. Zasada ta stwierdza, że: Poprawność całości można ustalić, biorąc pod uwagę tylko specyfikacje zewnętrzne ( skrócone specyfikacje w całym tekście) części, a nie ich konstrukcję wewnętrzną. Dijkstra nakreślił ogólne kroki w stosowaniu tej zasady:

1. Podaj pełną specyfikację każdej części.
2. Sprawdź, czy cały problem został rozwiązany, gdy dostępne są części programu spełniające ich specyfikacje.
3. Skonstruuj poszczególne części zgodnie z ich specyfikacjami, ale niezależnie od siebie i kontekstu, w jakim będą używane.

Podał kilka przykładów tej zasady poza programowaniem. Ale jego zastosowanie w programowaniu jest głównym problemem. Na przykład programista używający metody (podprogramu, funkcji itp.) powinien polegać tylko na jej specyfikacji, aby określić, co robi i jak ją wywołać, a nigdy na jej implementacji.

Specyfikacje programów są napisane w logice Hoare'a , wprowadzonej przez Sir Tony'ego Hoare'a , czego przykładem są specyfikacje procesów S1 i S2 :

       
                 
      {przed S1 } {przed S2 } S1 S2 {po S1 } {przed S2 }

Znaczenie: Jeśli wykonanie Si w stanie, w którym warunek wstępny pre-Si jest prawdziwy, kończy się, to po zakończeniu warunek końcowy post-Si jest prawdziwy.

Rozważmy teraz programowanie współbieżne ze wspólnymi zmiennymi. Specyfikacje dwóch (lub więcej) procesów S1 i S2 są podane w kategoriach ich warunków wstępnych i końcowych, i zakładamy, że podane są implementacje S1 i S2 , które spełniają ich specyfikacje. Ale podczas równoległego wykonywania ich implementacji, ponieważ współdzielą one zmienne, może wystąpić sytuacja wyścigu ; jeden proces zmienia wspólną zmienną na wartość, która nie jest przewidziana w dowodzie drugiego procesu, więc drugi proces nie działa zgodnie z zamierzeniami.

Tym samym zasada nieingerencji Dijkstry zostaje naruszona.

W swojej rozprawie doktorskiej z 1975 r. z informatyki na Cornell University , napisanej pod kierunkiem doradcy Davida Griesa , Susan Owicki rozwinęła pojęcie wolności ingerencji . Jeżeli procesy S1 i S2 spełniają warunki wolności od zakłóceń, to ich równoległa realizacja będzie przebiegać zgodnie z planem. Dijkstra nazwał tę pracę pierwszym znaczącym krokiem w kierunku zastosowania logiki Hoare'a do współbieżnych procesów. Aby uprościć dyskusje, ograniczamy uwagę tylko do dwóch równoczesnych procesów, chociaż Owicki-Gries pozwala na więcej.

Swoboda ingerencji w zakresie konturów dowodu

Owicki-Gries przedstawił zarys dowodu potrójnego {P}S{Q } Hoare'a . Zawiera wszystkie szczegóły potrzebne do udowodnienia poprawności {P}S{Q } przy użyciu aksjomatów i reguł wnioskowania logiki Hoare'a . (Ta praca wykorzystuje instrukcję przypisania x: = e , instrukcje if-then i if-then-else oraz pętlę while .) Hoare nawiązywał do zarysów dowodów w swojej wczesnej pracy; dla wolności ingerencji musiało to zostać sformalizowane.

Zarys dowodu dla {P}S{Q } zaczyna się od warunku wstępnego P i kończy na warunku końcowym Q . Dwie asercje w nawiasach klamrowych { i } pojawiające się obok siebie wskazują, że pierwsza musi implikować drugą.

Przykład: Zarys dowodu dla {P} S {Q }, gdzie S to: x : = a; jeśli e to S1 inaczej S2

  
  
  
  
  
                 
                 
        
                 
                 
  
   {P } {P1[x/a] } x : = za; {P1 } jeśli e to {P1 ∧ e } S1 {Q1 } inaczej {P1 ∧ ¬ e } S2 {Q1 } {Q1 } {Q }

P ⇒ P1[x/a] musi być zachowane, gdzie P1[x/a] oznacza P1 z każdym wystąpieniem x zastąpionym przez a . (W tym przykładzie S1 i S2 to podstawowe instrukcje, takie jak instrukcja przypisania, instrukcja skip lub instrukcja oczekiwania ).

Każde stwierdzenie T w zarysie dowodu jest poprzedzone warunkiem wstępnym pre-T , po którym następuje warunek końcowy post-T , a {pre-T}T{post-T } musi być możliwe do udowodnienia przy użyciu pewnego aksjomatu lub reguły wnioskowania logiki Hoare'a. Tak więc schemat dowodu zawiera wszystkie informacje niezbędne do udowodnienia, że ​​{P}S{Q } jest poprawne.

Rozważmy teraz dwa równoległe procesy S1 i S2 oraz ich specyfikacje:

       
                 
      {przed S1 } {przed S2 } S1 S2 {po S1 } {po S2 }

Udowodnienie, że działają one odpowiednio równolegle, będzie wymagało ich ograniczenia w następujący sposób. Każde wyrażenie E w S1 lub S2 może odnosić się co najwyżej do jednej zmiennej y , która może być zmieniona przez inny proces podczas obliczania E , a E może odnosić się do y co najwyżej raz. Podobne ograniczenie dotyczy instrukcji przypisania x: = E .

W tej konwencji jedyną niepodzielną akcją musi być odwołanie do pamięci. Załóżmy na przykład, że proces S1 odwołuje się do zmiennej y, podczas gdy S2 zmienia y . Wartość, S1 dla y , musi być wartością przed lub po zmianie S2 y , a nie jakąś fałszywą wartością pośrednią.

Definicja bez zakłóceń

Ważną innowacją Owickiego-Griesa było zdefiniowanie, co to znaczy, że zdanie T nie koliduje z dowodem { P}S{Q }. Jeśli wykonanie T nie może sfalsyfikować żadnego twierdzenia podanego w zarysie dowodu {P}S{Q }, to dowód ten zachowuje ważność nawet w obliczu równoczesnego wykonania S i T .

Definicja . Stwierdzenie T z warunkiem wstępnym pre-T nie koliduje z dowodem {P}S{Q }, jeśli spełnione są dwa warunki:

(1) {Q ∧ pre-T} T {Q } (2) Niech S' będzie dowolną instrukcją wewnątrz S , ale nie wewnątrz instrukcji await (patrz późniejsza sekcja). Następnie {pre-S' ∧ pre-T} T {pre-S' }.

Przeczytaj ostatnią trójkę Hoare'a w ten sposób: Jeśli stan jest taki, że można wykonać zarówno T , jak i S' , to wykonanie T nie będzie fałszować pre-S' .

Definicja . Zarysy dowodu dla {P1}S1{Q1 } i {P2}S2{Q2 } są wolne od interferencji, jeśli spełnione są następujące warunki. Niech T będzie instrukcją await lub przypisaniem (która nie pojawia się w await ) procesu S1 . Wtedy T nie koliduje z dowodem {P2}S2{Q2 }. Podobnie dla T procesu S2 i {P1}S1{Q1 }.

Instrukcje zaczynają się i czekają

Wprowadzono dwie instrukcje dotyczące współbieżności. Wykonanie instrukcji cobegin S1 // S2 coend wykonuje równolegle S1 i S2 . Kończy się, gdy zarówno S1 , jak i S2 zostaną zakończone.

Wykonanie instrukcji await await B then S jest opóźniane do momentu spełnienia warunku B. Następnie instrukcja S jest wykonywana jako niepodzielna akcja — ocena B jest częścią tej niepodzielnej akcji. Jeśli dwa procesy czekają na ten sam warunek B , gdy stanie się on prawdziwy, jeden z nich kontynuuje oczekiwanie, podczas gdy drugi kontynuuje.

Instrukcja oczekiwania nie może być wydajnie zaimplementowana i nie proponuje się jej wstawienia do języka programowania. Zapewnia raczej sposób reprezentowania kilku standardowych prymitywów, takich jak semafory — najpierw wyraź operacje semaforowe jako await s , a następnie zastosuj techniki opisane tutaj.

Reguły wnioskowania dla await i cobegin to:

czekaj {P ∧ B} S {Q} / {P} czekaj B , a następnie S {Q} cobegin
{P1} S1 {Q1}, {P2} S2 {Q2} wolny od interferencji / {P1∧P2} cobegin S1// koniec S2 {Q1∧Q2}

Zmienne pomocnicze

Zmienna pomocnicza nie występuje w programie, ale jest wprowadzana w dowodzie poprawności, aby uprościć lub nawet umożliwić rozumowanie. Zmienne pomocnicze są używane tylko w przypisaniach do zmiennych pomocniczych, więc ich wprowadzenie nie zmienia programu dla żadnego wejścia ani nie wpływa na wartości zmiennych programu. Zazwyczaj są one używane jako liczniki programów lub do rejestrowania historii obliczeń.

Definicja . Niech AV będzie zbiorem zmiennych, które pojawiają się w S' tylko w przypisaniach x: = E , gdzie x jest w AV . Wtedy AV jest zmienną pomocniczą złożoną dla S' .

Ponieważ zestaw AV zmiennych pomocniczych jest używany tylko w przypisaniach do zmiennych w AV , usunięcie wszystkich przypisań do nich nie zmienia poprawności programu i mamy regułę wnioskowania eliminacji AV :

   {P} S' {Q} / {P} S {Q}

AV jest zmienną pomocniczą złożoną dla S' . Zmienne w AV nie występują w P lub Q . S uzyskuje się z S' przez usunięcie wszystkich przypisań do zmiennych w AV .

Zamiast używać zmiennych pomocniczych, można wprowadzić licznik programu do systemu dowodowego, ale to zwiększa złożoność systemu dowodowego.

Uwaga: Apt omawia logikę Owickiego-Griesa w kontekście twierdzeń rekurencyjnych , czyli twierdzeń efektywnie obliczalnych . Udowadnia, że ​​wszystkie twierdzenia w zarysie dowodu mogą być rekurencyjne, ale nie ma to już miejsca, jeśli zmienne pomocnicze są używane tylko jako liczniki programu, a nie do rejestrowania historii obliczeń. Lamport w swojej podobnej pracy używa twierdzeń dotyczących pozycji tokenów zamiast zmiennych pomocniczych, gdzie token na krawędzi schematu blokowego jest podobny do licznika programu. Nie ma pojęcia zmiennej historii. Wskazuje to, że podejście Owickiego-Griesa i Lamporta nie jest równoważne, gdy ogranicza się je do twierdzeń rekurencyjnych.

Zakleszczenie i zakończenie

Owicki-Gries zajmuje się głównie poprawnością częściową: {P} S {Q } oznacza: Jeśli S wykonywane w stanie, w którym P jest prawdziwe, kończy się, to Q jest prawdziwe dla stanu po zakończeniu. Jednak Owicki-Gries podaje również kilka praktycznych technik, które wykorzystują informacje uzyskane z częściowego dowodu poprawności w celu uzyskania innych właściwości poprawności, w tym wolności od impasu, zakończenia programu i wzajemnego wykluczania.

Program jest w impasie , jeśli wszystkie procesy, które nie zostały zakończone, wykonują instrukcje oczekiwania i żaden nie może kontynuować, ponieważ ich warunki oczekiwania są fałszywe. Owicki-Gries zapewnia warunki, w których impas nie może wystąpić.

Owicki-Gries przedstawia regułę wnioskowania o całkowitej poprawności pętli while . Wykorzystuje funkcję związaną, która maleje z każdą iteracją i jest dodatnia, o ile warunek pętli jest prawdziwy. Apt i wsp. pokazują, że ta nowa reguła wnioskowania nie spełnia wymogów wolności ingerencji. Fakt, że funkcja związana jest dodatnia, o ile warunek pętli jest prawdziwy, nie został uwzględniony w teście interferencji. Pokazują dwa sposoby naprawienia tego błędu.

Prosty przykład

       
       

       
        Rozważmy instrukcję: {x=0} cobegin await true then x: = x+1 // wait true then x: = x+2 coend {x=3}

Zarys dowodu na to:

       
       
       
       
     
       
       
       
       
     

{x=0} S: początek {x=0} {x=0 ∨ x=2} S1: czekaj wtedy prawda x : = x+1 {Q1: x=1 ∨ x=3} // {x=0 } {x=0 ∨ x=1} S2: czekaj prawda wtedy x : = x+2 {Q2: x=2 ∨ x=3} coend {(x=1 ∨ x=3) ∧ (x=2 ∨ x =3)} {x=3}

Udowodnienie, że S1 nie koliduje z dowodem S2 , wymaga udowodnienia dwóch trójek Hoare'a:

(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}

Warunek wstępny (1) redukuje się do x=0 , a warunek wstępny (2) redukuje się do x=2 . Z tego łatwo zauważyć, że te trójki Hoare'a się trzymają. Potrzebne są dwie podobne trójki Hoare'a, aby pokazać, że S2 nie koliduje z dowodem S1 .

Załóżmy, że S1 zostanie zmienione z instrukcji await na przypisanie x: = x+1 . Wtedy schemat dowodu nie spełnia wymagań, ponieważ przypisanie zawiera dwa wystąpienia zmiennej wspólnej x . Rzeczywiście, wartość x po wykonaniu instrukcji cobegin może wynosić 2 lub 3.

Załóżmy , że S1 zostanie zmieniona na instrukcję await await true then x: = x+2 , więc jest taka sama jak S2 . Po wykonaniu S x powinno wynosić 4. Aby to udowodnić , ponieważ oba przypisania są takie same, potrzebne są dwie zmienne pomocnicze, jedna wskazująca, czy S1 zostało wykonane; drugi, czy S2 zostało wykonane. Czytelnikowi pozostawiamy zmianę w zarysie dowodu.

Przykłady formalnie udowodnionych programów współbieżnych

A. Findpos . Napisz program, który znajdzie pierwszy dodatni element tablicy (jeśli taki istnieje). Jeden proces sprawdza wszystkie elementy tablicy na parzystych pozycjach tablicy i kończy działanie, gdy znajdzie wartość dodatnią lub gdy nie zostanie znaleziona żadna. Podobnie drugi proces sprawdza elementy tablicy w nieparzystych pozycjach tablicy. Zatem ten przykład dotyczy while . Nie ma również oczekiwania .

Ten przykład pochodzi od Barry'ego K. Rosena. Rozwiązanie w Owicki-Gries, wraz z programem, konspektem dowodu i omówieniem wolności ingerencji, zajmuje mniej niż dwie strony. Wolność od zakłóceń jest dość łatwa do sprawdzenia, ponieważ istnieje tylko jedna wspólna zmienna. W przeciwieństwie do tego artykuł Rosena wykorzystuje Findpos jako pojedynczy, działający przykład w tym 24-stronicowym artykule.

Zarys obu procesów w środowisku ogólnym:

     
     
     
     
  
     
     
     
     

cobegin producent: ... czekaj na wejście < N następnie pomiń ; dodaj: b[w mod N]:= następna wartość; znak: w: = w +1; ... // konsument: ... czekaj na wejście-wyjście > 0, a następnie pomiń ; usuń:
        ta wartość:= b[out mod N]; znacznik: out: = out+1; koedukacja ...

B. Problem konsumenta/producenta z ograniczonym buforem . Proces producenta generuje wartości i umieszcza je w ograniczonym buforze b o rozmiarze N ; proces konsumencki je usuwa. Postępują według zmiennych stawek. Producent musi czekać, jeśli bufor b jest pełny; konsument musi czekać, jeśli bufor b jest pusty. W Owicki-Gries pokazano rozwiązanie w środowisku ogólnym; jest następnie osadzony w programie, który kopiuje tablicę c[1..M] do tablicy d[1..M] .

Ten przykład ilustruje zasadę ograniczania sprawdzania kolizji do minimum: umieść jak najwięcej w twierdzeniu, które jest niezmiennie prawdziwe wszędzie w obu procesach. W tym przypadku asercja jest definicją ograniczonego bufora i granic zmiennych, które wskazują, ile wartości zostało dodanych i usuniętych z bufora. Oprócz samego bufora b , dwie wspólne zmienne rejestrują liczbę wejść wartości dodanych do bufora i liczbę usuniętych z bufora.

C. Implementacja semaforów . W swoim artykule na temat systemu wieloprogramowego THE Dijkstra wprowadza semafor sem jako prymityw synchronizacji: sem jest zmienną całkowitą, do której można się odwoływać tylko na dwa sposoby, pokazane poniżej; każdy jest niepodzielną operacją:

1. P(sem) : Zmniejsz sem o 1. Jeśli teraz sem < 0 , wstrzymaj proces i umieść go na liście zawieszonych procesów powiązanych z sem .

2. V(sem) : Zwiększ sem o 1. Jeśli teraz sem ≤ 0 , usuń jeden z procesów z listy zawieszonych procesów związanych z sem , aby jego dynamiczny postęp był znowu dozwolony.

Implementacja P i V przy użyciu instrukcji await to:

      
          
              
                
          
          
                


      
          
              
                 
                                   
                             P(sem): czekaj prawda, a następnie rozpocznij sem: = sem-1; jeśli sem < 0 to w[ten proces]: = prawdziwy koniec ; czekaj ¬w[ten proces] , a następnie pomiń V(sem): czekaj prawda, a następnie rozpocznij sem: = sem+1; jeśli sem ≤ 0 to zacznij wybierać p takie , że w[ p ]; w [ p ]:
                  = koniec fałszywego końca
          

Tutaj w jest tablicą procesów, które czekają, ponieważ zostały zawieszone; początkowo w[p] = false dla każdego procesu p . Można zmienić implementację, aby zawsze budzić najdłużej zawieszony proces.

D. Odśmiecanie w locie . Podczas letniej szkoły Marktoberdorf w 1975 r. Dijkstra omówił wyrzucanie elementów bezużytecznych w locie jako ćwiczenie w zrozumieniu równoległości. Struktura danych używana w konwencjonalnej implementacji LISP-a jest grafem skierowanym, w którym każdy węzeł ma co najwyżej dwie wychodzące krawędzie, z których jednej może brakować: wychodzącą lewą krawędź i wychodzącą prawą krawędź. Wszystkie węzły grafu muszą być osiągalne ze znanego korzenia. Zmiana węzła może spowodować nieosiągalne węzły, których nie można już używać i są nazywane śmieciami . Garbage collector on-the-fly ma dwa procesy: sam program i Garbage Collector, którego zadaniem jest identyfikowanie węzłów śmieci i umieszczanie ich na wolnej liście, aby można było ich ponownie użyć.

Gries uważał, że wolność ingerencji może zostać wykorzystana do udowodnienia, że ​​​​śmieciarz w locie ma rację. Z pomocą Dijkstry i Hoare'a był w stanie wygłosić prezentację na zakończenie Szkoły Letniej, co zaowocowało artykułem w CACM.

E. Weryfikacja rozwiązania czytników/pisarzy z semaforami . Courtois i inni używają semaforów, aby przedstawić dwie wersje problemu czytelników/pisarzy, bez dowodu. Operacje zapisu blokują zarówno odczyt, jak i zapis, ale operacje odczytu mogą odbywać się równolegle. Owicki dostarcza dowód.

F. Petersona , rozwiązanie dwuprocesowego problemu wzajemnego wykluczania, został opublikowany przez Petersona w dwustronicowym artykule. Schneider i Andrews dostarczają dowód poprawności.

Zależności od swobody interferencji

Poniższy obraz, autorstwa Ilyi Sergey, przedstawia przepływ pomysłów, które zostały zaimplementowane w logice zajmującej się współbieżnością. U podstaw leży wolność od zakłóceń. Plik CSL-Family-Tree (PDF) zawiera odniesienia. Poniżej podsumowujemy najważniejsze postępy.

• Niezawodna gwarancja . 1981. Wolność ingerencji nie jest kompozycyjna. Cliff Jones odzyskuje kompozycję poprzez abstrakcję interferencji w dwóch nowych predykatach w specyfikacji: warunek zależności rejestruje, jaką ingerencję wątek musi tolerować, a warunek gwarancji określa górną granicę interferencji, jaką wątek może wyrządzić swoim siostrzanym wątkom . Xu i inni zauważają, że Rely-Guarantee to przeformułowanie wolności ingerencji; ujawnienie związku między tymi dwiema metodami, jak mówią, oferuje głębokie zrozumienie weryfikacji wspólnych programów zmiennych.
• CSL . 2004. Logika separacji obsługuje rozumowanie lokalne, w którym specyfikacje i dowody komponentu programu wspominają tylko o części pamięci używanej przez komponent. Współbieżna logika separacji (CSL) została pierwotnie zaproponowana przez Petera O'Hearna , cytujemy z: „metoda Owickiego-Griesa polega na jawnym sprawdzaniu braku interferencji między komponentami programu, podczas gdy nasz system wyklucza interferencje w sposób niejawny, z natury sposobu, w jaki konstruowane są dowody”.
• Wyprowadzanie programów współbieżnych . 2005-2007. Feijen i van Gasteren pokazują, jak wykorzystać Owicki-Gries do projektowania programów współbieżnych, ale brak teorii postępu oznacza, że ​​projektami kierują się wyłącznie wymogi bezpieczeństwa . Dongol, Goldson, Mooij i Hayes rozszerzyli tę pracę o „logikę postępu” opartą na języku Unity Chandy'ego i Misry , uformowaną tak, aby pasowała do modelu programowania sekwencyjnego. Dongel i Goldson opisują swoją logikę postępu. Goldson i Dongol pokazują, w jaki sposób ta logika jest wykorzystywana do usprawnienia procesu projektowania programów za pomocą Algorytm Dekkera dla dwóch procesów jako przykład. Dongol i Mooij przedstawiają więcej technik wyprowadzania programów, na przykładzie algorytmu wzajemnego wykluczania Petersona . Dongol i Mooij pokazują, jak zmniejszyć narzut obliczeniowy w formalnych dowodach i wyprowadzeniach oraz ponownie wyprowadzić algorytm Dekkera, prowadząc do kilku nowych i prostszych wariantów algorytmu. Mooij bada reguły obliczeniowe dla relacji prowadzących do Unity . Wreszcie Dongol i Hayes dostarczają teoretycznych podstaw i udowadniają poprawność logiki procesu.
• OGRA . 2015. Lahav i Vafeiadis wzmacniają kontrolę wolności zakłóceń, aby stworzyć (cytujemy ze streszczenia) „OGRA, logikę programu, która jest odpowiednia do rozumowania na temat programów we fragmencie uwalniania-nabywania modelu pamięci C11”. Podają kilka przykładów jego użycia, w tym implementację prymitywów synchronizacji RCU.
• Programowanie kwantowe . 2108. Ying i wsp. rozszerzają wolność zakłóceń na programowanie kwantowe. Trudności, z którymi się borykają, obejmują przeplatający się niedeterminizm: niedeterminizm obejmujący pomiary kwantowe i niedeterminizm wprowadzony przez równoległość występującą w tym samym czasie. Autorzy formalnie weryfikują równoległy algorytm kwantowy Bravyi-Gosseta-Königa rozwiązujący problem algebry liniowej, dając, jak mówią, po raz pierwszy bezwarunkowy dowód na kwantową przewagę obliczeniową.
• POG . 2020. Raad i wsp. przedstawiają POG (Persistent Owicki-Gries), pierwszą logikę programu do wnioskowania o technologiach pamięci nieulotnej, w szczególności Intel-x86.

Teksty omawiające wolność ingerencji

• On A Method of Multiprogramming , 1999. Van Gasteren i Feijen omawiają formalny rozwój programów współbieżnych całkowicie na idei wolności od zakłóceń.
• On Current Programming , 1997. Schneider wykorzystuje wolność od zakłóceń jako główne narzędzie w opracowywaniu i sprawdzaniu programów współbieżnych. Podano połączenie z logiką temporalną, więc można udowodnić dowolne właściwości bezpieczeństwa i żywotności. Predykaty kontrolne eliminują potrzebę stosowania zmiennych pomocniczych do wnioskowania o licznikach programu.
• Verification of Sequential and Concurrent Programs , 1991, 2009. Ten pierwszy tekst obejmujący weryfikację ustrukturyzowanych programów współbieżnych, autorstwa Apt i in ., doczekał się kilku wydań na przestrzeni kilkudziesięciu lat.
• Concurrency Verification: Introduction to Compositional and Non-Compositional Methods , 2112. De Roever i in. zapewniają systematyczne i obszerne wprowadzenie do kompozycyjnych i niekompozycyjnych metod dowodzenia do weryfikacji programów współbieżnych w oparciu o stan

Implementacje wolności ingerencji

• 1999: Nipkow i Nieto przedstawiają pierwszą formalizację wolności ingerencji i jej kompozycyjną wersję, metodę polegania na gwarancji, w dowodzie twierdzeń: Isabelle/HOL.
• 2005: Praca doktorska Ábraháma zapewnia sposób udowodnienia poprawności wielowątkowych programów Java w trzech krokach: (1) opatrz adnotacją program w celu utworzenia zarysu dowodu, (2) użyj ich narzędzia Verger do automatycznego stworzenia warunków weryfikacji oraz (3) użyj twierdzenia Prover PVS do interaktywnego udowodnienia warunków weryfikacji.
• 2017: Denissen informuje o implementacji Owicki-Gries w „gotowym do weryfikacji” języku programowania Dafny . Denissen zwraca uwagę na łatwość użycia Dafny i jego rozszerzenie, co sprawia, że ​​jest on niezwykle przydatny podczas nauczania uczniów o wolności od zakłóceń. Jego prostota i intuicyjność przewyższają wadę polegającą na braku kompozycji. Wymienia około dwudziestu instytucji, które uczą wolności ingerencji.
• 2017: Amani i wsp. łączą podejście Hoare-Parallel, formalizacji Owicki-Gries w Isabelle/HOL dla prostego języka while, oraz SIMPL, ogólnego języka osadzonego w Isabelle/HOL, aby umożliwić formalne rozumowanie w programach C.
• 2022: Dalvandi i wsp. wprowadzają pierwsze dedukcyjne środowisko weryfikacji w Isabelle / HOL dla programów o słabej pamięci podobnych do C11, opierając się na kodowaniu Owickiego-Griesa przez Nipkowa i Nieto w dowodzie twierdzenia Isabelle.
• 2022: Ta strona internetowa opisuje weryfikator Civl dla programów równoległych i zawiera instrukcje dotyczące instalowania go na komputerze. Jest zbudowany na Boogie, weryfikatorze programów sekwencyjnych. Kragl i inni opisują, w jaki sposób w Civl osiąga się wolność od zakłóceń, używając ich nowego idiomu specyfikacji, niezmienników wydajności . Można również użyć specyfikacji w stylu polegania na gwarancji. Civl oferuje połączenie typowania liniowego i logiki, które umożliwia ekonomiczne i lokalne rozumowanie dotyczące rozłączności (jak logika separacji). Civl to pierwszy system, który oferuje udoskonalone rozumowanie w ustrukturyzowanych programach współbieżnych.
• 2022. Esen i Rümmer opracowali TRICERA, zautomatyzowane narzędzie do weryfikacji programów C o otwartym kodzie źródłowym. Opiera się na koncepcji ograniczonych klauzul Horna i obsługuje programy działające na stercie z wykorzystaniem teorii stert. Dostępny jest interfejs sieciowy do wypróbowania go online. Aby obsłużyć współbieżność, TRICERA używa wariantu reguł dowodu Owickiego-Griesa, z jawnymi zmiennymi dodawanymi w celu reprezentowania czasu i zegarów.