Twardość obliczeniowa „prawdziwych” programów komputerowych

Często słyszałem, jak mówiono, że nie można napisać programu do wychwytywania błędów w przeglądarce internetowej, edytorze tekstu lub systemie operacyjnym z powodu twierdzenia Rice'a: każda właściwość semantyczna dla języka pełnego Turinga jest nierozstrzygalna.

Nie jestem jednak pewien, w jakim stopniu dotyczy to rzeczywistego programu, takiego jak systemy operacyjne. Czy tego typu programy wymagają pełnej siły kompletności Turinga? Czy istnieją prostsze modele obliczeń (takie jak PR), w których można pisać te aplikacje? Jeśli tak, to w jakim stopniu umożliwia to rozstrzygalność poprawności programu?

Z pewnością możesz pisać programy, które wychwytują błędy - istnieje duża i aktywna społeczność ludzi, którzy piszą programy, które właśnie to robią. Jednak twierdzenie Rice'a powstrzymuje cię od napisania łapaczy błędów, które są zarówno solidne, jak i kompletne (tzn. Łapią wszystkie błędy pewnej klasy bez fałszywych alarmów).

To powiedziawszy, naiwne ograniczenia modelu obliczeniowego nie pomagają w znacznym stopniu poprawić praktyczności analizy programu. Powodem jest to, że można uzyskać programy, które robią „prawie to samo”, obracając pętle while

while P do 
   C

w pętle for z dużą stałą iteracji:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Teraz ten program nie potrzebuje nawet pełnej siły prymitywnej rekurencyjnej (ponieważ pętla for może zostać rozwinięta w makro w ogromną zagnieżdżoną instrukcję if-then-else), ale w większości praktycznych przypadków będzie zachowywać się tak samo jak poprzednio. Zauważ, że pomaga to w rozstrzygalności teoretycznej - program jest całkowity, więc możesz odpowiadać na pytania, uruchamiając program i sprawdzając, co się stanie. To nie jest to, czego tak naprawdę chcemy, aby uzyskać odpowiedzi szybciej niż uruchomienie programu - wprowadzone sztuczne zakończenie nie pomaga w praktyce analizie programu, ponieważ błędy występują z powodu błędów w prawdziwej logice programu, a my nie „ w ogóle tego dotknąłem.

$\epsilon_0$

Ponieważ pytałeś o poprawność programów w prawdziwych programach, takich jak systemy operacyjne, możesz być zainteresowany projektem seL4 ( czasopismo , pdf , konferencja ).

Zespół NICTA wziął mikrojądro trzeciej generacji z 8700 liniami C i 600 liniami asemblera wdrożonymi zgodnie ze abstrakcyjną specyfikacją w Haskell. Dostarczyli formalny, sprawdzony maszynowo dowód (w Isabelle / HOL), że wdrożenie jest ściśle zgodne ze specyfikacją. Dowodzi to, że ich program nie zawiera błędów.

Podobnie jak problem zatrzymania, chociaż nie można go ogólnie rozwiązać, można go rozwiązać w określonych przypadkach. W tym przypadku, chociaż nie możesz udowodnić, że dowolny kod C jest wolny od błędów, mogliby to zrobić w przypadku mikrojądra seL4.

Pytania, które zadajesz, są zupełnie inne.

Nie jestem jednak pewien, w jakim stopniu dotyczy to rzeczywistego programu, takiego jak systemy operacyjne. Czy tego typu programy wymagają pełnej siły kompletności Turinga?

Kompletowanie modelu obliczeniowego Turinga zajmuje bardzo niewiele. Na przykład różne modele z licznikami mogą symulować maszyny Turinga. Jeśli uważasz, że twoje oprogramowanie wymaga więcej niż dwóch liczników, którymi możesz dowolnie manipulować, używasz kompletnego języka Turinga. Chociaż liczby całkowite maszyny są ograniczone apriori, struktury danych alokowane na stercie zwykle nie są. Jeśli twoje oprogramowanie potrzebuje list, drzew i innych dynamicznie przydzielanych danych, używasz kompletnego języka Turinga.

Czy istnieją prostsze modele obliczeń (takie jak PR), w których można pisać te aplikacje? Jeśli tak, to w jakim stopniu umożliwia to rozstrzygalność poprawności programu?

Należy pamiętać, że nie chcemy sprawdzać arbitralnych właściwości naszego oprogramowania. Sprawdzanie bardzo specyficznych, wąskich właściwości (brak przepełnienia bufora, brak dereferencji wskaźnika zerowego, brak nieskończonych pętli itp.) Znacznie poprawia jakość i użyteczność oprogramowania. Teoretycznie takie problemy są nadal nierozstrzygalne. W praktyce skupienie się na określonych właściwościach pozwala nam odkryć strukturę w naszych programach, którą często możemy wykorzystać do rozwiązania problemu.

W szczególności możesz zmodyfikować swoje pierwotne pytanie na

Czy istnieje abstrakcja mojego oprogramowania, którą mogę efektywnie analizować w modelu niekompletnym Turinga?

Abstrakcja to model, który obejmuje zachowanie oryginalnego oprogramowania i prawdopodobnie wiele dodatkowych zachowań. Istnieją modele, takie jak maszyny z jednym licznikiem lub systemy wypychające, które nie są kompletne w Turinga i które możemy analizować. Standardowym podejściem do weryfikacji programu za pomocą zautomatyzowanych narzędzi jest zbudowanie abstrakcji w takim modelu i sprawdzenie go algorytmicznie.

Istnieją aplikacje, w których ludzie dbają o wyrafinowane właściwości swojego sprzętu lub oprogramowania. Firmy sprzętowe chcą, aby ich układy poprawnie wdrażały algorytmy arytmetyczne, firmy motoryzacyjne i awioniczne chcą certyfikowanego oprogramowania. Jeśli to takie ważne, lepiej wykorzystać (wyszkolonego) człowieka.