15.10.2009

Środowisko specyfikacyjno-weryfikacyjne
dla optymalizatorów generujących dowody

Budowa kompilatorów i ich poprawność jest jedną z najstarszych dziedzin badań informatyki. W rezultacie tych badań wykrystalizowały się dwie kategorie metod formalnych implementacji poprawnych kompilatorów: kompilatory certyfikowane i kompilatory certyfikujące. Implementacja kompilatora certyfikowanego polega na implementacji samego kompilatora oraz dostarczeniu dwóch dowodów matematycznych demonstrujących poprawność algorytmu kompilatora oraz poprawność implementacji tego algorytmu w konkretnej architekturze maszyny, która wykonuje program kompilatora. Implementacja kompilatora certyfikującego polega na wyposażeniu programu kompilatora w dodatkowy moduł certyfikujący, który po zakończeniu konkretnej translacji przejmuje jej program źródłowy oraz program docelowy jako swoje dane wejściowe i generuje dowód formalny poprawności translacji. Dowód taki zwany jest certyfikatem translacji. W tym kontekście należy dalej rozróżnić między podejściami metod formalnych do tego, czym jest dowód formalny poprawności translacji. Implementacje kompilatorów oparte na metodzie translation validation (TV) odwzorowują programy na ich semantyczne abstrakcje, które służą jako dane wejściowe dla dedykowanego narzędzia zwanego abstraction validator. Model checker jest przykładem takiego narzędzia. W ramach mojej prezentacji przedstawię implementację nowatorskiej metody formalnej certyfikowania translacji, foundational translation validation (FTV), którą opisałem w mojej pracy doktorskiej. Metoda ta opiera się na implementacji kompilatora certyfikującego oraz formalizacji środowiska specyfikacyjno-weryfikacyjnego w logice wyższego rzędu (HOL) przy pomocy narzędzia theorem prover. Moduł certyfikujący kompilatora odwzorowuje programy na ich syntaktyczne reprezentacje w HOL oraz generuje dowód matematyczny, który demonstruje poprawność danej translacji. Zaletą metody FTV w porównaniu do metody TV jest formalizacja czytelnego kontraktu translacji, który zawiera formalne definicje semantyki programów źródłowych i docelowych oraz predykatu poprawności translacji, oraz możliwość certyfikowania całych sekwencji transformacji programów, które mają miejsce w fazie optymalizacji kompilatora.