Certyfikowany kompilator i optymalizacje w Coq / Agda

Interesują mnie sprawdzone kompilatory sformalizowane w teorii typów Martina-Löfa, tj. Coq / Agda. W tej chwili napisałem przykład małej zabawki. Dzięki temu mogę udowodnić, że moje optymalizacje są prawidłowe. Na przykład można wyeliminować dodawanie zerowe, tzn. Wyrażenia takie jak „x + 0”.

Czy istnieją optymalizacje, które są trudne do przeprowadzenia przy użyciu zwykłego kompilatora, który byłby dobrym przykładem? Czy można udowodnić pewne właściwości programu, które pozwalają na optymalizacje, których nie można wykonać za pomocą zwykłego kompilatora? (tj. bez wnioskowania, które jest możliwe przy twierdzeniu twierdzenia)

Byłbym zainteresowany pomysłami lub przykładami, a także referencjami na ten temat.

Powiązane pytanie: Dowody poprawności kompilatora

edit: Jak ładnie ujął to Tsuyoshi w komentarzach: Szukam technik optymalizacji, które są trudne do wdrożenia, jeśli kompilator jest napisany w (powiedzmy) C, ale łatwiejsze do wdrożenia, jeśli kompilator jest napisany w (powiedzmy) Coq. Gdy Agda kompiluje się do C (przez haskell), możliwe jest robienie wszystkiego, co jest możliwe w Agdzie również w C. Prawdopodobnie jedyną korzyścią z twierdzeń takich jak Coq / Agda jest to, że można zweryfikować kompilator i optymalizacje.

edit2: Zgodnie z sugestią Vijay DI napisz, co przeczytałem do tej pory. Skoncentrowałem się głównie na Xavier Leroy i projekcie CompCert w INRIA (wydaje mi się, że 80-stronicowy artykuł to dobra lektura). Drugim zainteresowaniem były prace Antona Setzera nad programami interaktywnymi. Pomyślałem, że być może jego praca mogłaby zostać wykorzystana do udowodnienia właściwości programów IO i bisimulacji programów IO. Dzięki za wzmiankę o Sewell. Słyszałem jego przemówienie „Opowieści z dżungli” w ICFP i przeczytałem może 2-3 jego artykuły. Ale nie spojrzałem konkretnie na jego prace i prace jego współautorów.
Nie dowiedziałem się jeszcze, od czego zacząć, ani szukać artykułów na temat optymalizacji kompilatorów; np. które optymalizacje byłyby interesujące w kontekście zweryfikowanego kompilatora.

ten artykuł autorstwa Yvesa Bertota, Benjamina Gr´egoire'a i Xaviera Leroya buduje optymalizujący kompilator dla języka podobnego do C oparty wyłącznie na specyfikacji Coq. niektóre z tych technologii jest najwyraźniej wykorzystywane w kompilator CompCert C .

Ustrukturyzowane podejście do sprawdzania optymalizacji kompilatora na podstawie analizy przepływu danych

bierze pod uwagę poprawność dwóch optymalizacji, stałej propagacji (CP) i wspólnej eliminacji podwyrażeń (CSE), sekcja 4. Te optymalizacje są bardziej zaawansowane niż te, które są powiązane z kompilatorami nie opartymi na Coq dla tego samego języka. patrz np. ta tabela porównawcza w porównaniu do gcc. (kompilator oparty na Coq jest prawdopodobnie wolniejszy w kompilacji, chociaż jest to rzadko wspominane!)

Oryginalny aspekt ConCert polega na tym, że większość kompilatora jest napisana bezpośrednio w języku specyfikacji Coq, w czysto funkcjonalnym stylu. Kompilator wykonywalny jest uzyskiwany przez automatyczną ekstrakcję kodu Caml z tej specyfikacji.

jednak na końcu artykułu zauważają, że istnieją pewne optymalizacje kompilatorów w prawdziwych kompilatorach, których nie można modelować w ich ramach.

ulepszona optymalizacja nie jest tu jedynym czynnikiem branym pod uwagę, innym aspektem jest to, że logika optymalizacji kompilatora może podlegać subtelnym defektom szczególnie ze względu na jej złożony charakter. z biegiem lat okazało się, że gcc ma błędy w licznych procedurach logiki optymalizacyjnej. np. błąd gcc?

Czy mogę udowodnić pewne właściwości (które z pewnością są przechowywane) dla programu (np. Podprogram nie jest uruchamiany i nigdy nie może się wywołać), które umożliwiają przeprowadzenie optymalizacji, które zwykle nie są możliwe.

Jest to równoważne z rozszerzeniem sprawdzania typu, aby zapewnić optymalizatorowi niektóre właściwości programu. Uważam, że Tsuyoshi Ito ma rację i możesz być trochę wprowadzony w błąd co do Coq. Jest to świetne narzędzie do dostarczania kompilatora bezbłędnego, ale w opisanym przypadku nie zapewnia większej mocy analizom statycznym.

Jedyne, co mogę myśleć o wzmocnieniu analiz statycznych za pomocą Coq, to ​​wyposażyć swój język w twierdzenia zawierające niektóre pisemne dowody. - Jeśli sam kompilator zostałby przetłumaczony na język obejmujący wtapianie do dynamicznego sprawdzania typów, a jeśli dowody napisane przez użytkownika byłyby przekształcalne w funkcje, wówczas możliwe byłoby zastosowanie tych funkcji jako wstępnie wymaganych właściwości dla niektórych podtypów lub optymalizacji. - To rzeczywiście zapewniłoby więcej mocy kompilatorowi.

Jednak, o ile widzę, byłoby to raczej przydatne do wzmocnienia podtypów. - Trudno jest programiście wiedzieć, jaka właściwość w jakim miejscu byłaby pomocna dla optymalizatora.