Verified optimizations for functional languages

Abstract

Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq's extraction plugin to obtain a program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language can render source-level verification useless. A verified compiler is a compiler whose output provably preserves thesemantics of the source language. CertiCoq is a verified compiler, currently under development, for Coq's specification language, Gallina. CertiCoq targets Clight, a subset of the C language, that can be compiled with the CompCert verified compiler to obtain a certified executable, bridging the gap between the formally verified source program and the compiled target program. In this thesis, I present the implementation and verification of CertiCoq's optimizing middle-end pipeline. CertiCoq's middle end consists of seven different transformations and is responsible for efficiently compiling an untyped purely functional intermediate language to a subset of the same language, which can be readily compiled to a first-order, low-level intermediate language. CertiCoq's middle-end pipeline performs crucial optimizations for functional languages including closure conversion, uncurrying, shrink-reduction and inlining. It advances the state of the art of verified optimizing compilers for functional languages by implementing more efficient closure-allocation strategies. For proving CertiCoq correct, I develop a framework based on thetechnique of logical relations, making novel technical contributions. I extend logical relations with notions of relational preconditions and postconditions that facilitate reasoning about the resource consumption of programs simultaneously with functional correctness. I demonstrate how this enables reasoning about preservation of non-terminating behaviors, which is not supported by traditional logical relations. Moreover, I develop a novel, lightweight technique that allows logical-relation proofs to be composed in order to obtain a top-level compositional compiler correctness theorem. This technique is used to obtain a separate compilation theorem that guarantees that programs compiled separately through CertiCoq using different sets of optimizations can be safely linked at the target level. Lastly, I use the framework to prove that CertiCoq's closure conversion is not only functionally correct but also safe for time and space, meaning that it is guaranteed to preserve the asymptotic time and space complexity of the source program.

Το σύστημα Coq είναι ένα από τα πιο διαδεδομένα συστήματα μηχανικών αποδείξεων. Επιτρέπει στους χρήστες να γράφουν συναρτησιακά προγράμματα, να εκφράζουν τυπικές προδιαγραφές για αυτά, και στη συνέχεια να τις αποδεικνύουν μέσω μιας διαλογικής διεπαφής. Τα προγράμματα που είναι γραμμένα σε Coq μπορούν να εξαχθούν σε μία από τις γλώσσες OCaml, Haskell, ή Scheme και στην συνέχεια να μεταγλωττιστούν και να εκτελεστούν. Όταν το πρόγραμμα Coq συνοδεύεται από μια μηχανική απόδειξη ορθότητας, τότε το πρόγραμμα που εξάγεται πρόκειται για ένα πιστοποιημένο πρόγραμμα. Ωστόσο, σφάλματα τόσο στο πρόγραμμα εξαγωγής όσο και στους μεταγλωττιστές μπορούν να δημιουργήσουν σημασιολογικές διαφορές μεταξύτου τελικού εκτελέσιμου και του αρχικού προγράμματος, με αποτέλεσμα οι αποδεδειγμένες ιδιότητες να μην ισχύουν για τον τελικό κώδικα. Προκειμένου να επιτευχθεί πιστοποίηση του προγράμματος απο άκρη σε άκρη, χρειάζεται ο τελικός κώδικας να παράγεται μέσω μιας πιστοποιημένης διαδικασίας μεταγλώττισης. Επιπλέον, είναι σύνηθες κάποια προγράμματα να μεταγλωττίζονται ξεχωριστά (π.χ. βιβλιοθήκες). Είναι σημαντικό λοιπόν οι αποδείξεις ορθότητας μεταγλώττισης που αφορούν κάθε πρόγραμμα ξεχωριστά, να μπορούν να συντεθούν σε μια απόδειξη που αφορά το τελικό πρόγραμμα μετά τη σύνδεση. Αυτό είναι ένα γνωστό πρόβλημα στην βιβλιογραφία επαλήθευσης μεταγλωττιστών που αυξάνει σημαντικά την πολυπλοκότητα των αποδείξεων. Σε αυτή τη διατριβή παρουσιάζεται υλοποίηση και πιστοποίηση του μέσου τμήματος του μεταγλωττιστή CertiCoq, ενός μηχανικά επαληθευμένου μεταγλωττιστή για την γλώσσα Coq. Ο μεταγλωττιστής όπως και οι αποδείξεις είναι γραμμένα στην Coq. Το μέσο τμήμα αποτελείται από 7 μετασχηματισμούς προγραμμάτων (closure conversion, lambda lifting, inlining, shrink reduction, hoisting, uncurrying, dead parameter elimination) πάνω σε μια συναρτησιακή ενδιάμεση αναπαράσταση που βασίζεται στην Α-κανονική μορφή. Οι μετασχηματισμοί αυτοί μετατρέπουν τις συναρτήσεις υψηλής τάξης σε συναρτήσεις πρώτης τάξης. Έτσι, το πρόγραμμα μπορεί να μεταφραστεί άμεσα σε μια γλώσσα χαμηλού επιπέδου. Οι μετασχηματισμοί εκτελούν επίσης βελτιστοποιήσεις που είναι κρίσιμες για την αποδοτικότητα τουτελικού προγράμματος. Προκειμένου να αποδειχτεί η ορθότητα των μετασχηματισμών αναπτύσσεται ένα νέο πλαίσιο που βασίζεται στην τεχνική των λογικών σχέσεων. Το πλαίσιο δίνει τη δυνατότητα σε αποδείξεις ορθής μεταγλώττισης προγραμμάτων που έχουν μεταγλωττιστεί ξεχωριστά να συντεθούν σε έναμια απόδειξη ορθής μεταγλώττισης που αφορά το τελικό πρόγραμμα μετά τη σύνδεση. Αυτό μπορεί να γίνει ακόμα και αν εσωτερικά οι μεταγλωττιστές που χρησιμοποιούνται για την ξεχωριστή μεταγλώττιση χρησιμοποιούν διαφορετικούς μετασχηματισμούς. Ωστόσο, επιβάλλεται ο επιπλέον περιορισμός ότι οι μεταγλωττιστές χρησιμοποιούν τις ίδιες ενδιάμεσες αναπαραστάσεις. Η διατριβή δείχνει πως μια γνωστή τεχνική μπορεί να χρησιμοποιηθεί για να λύσει ένα δύσκολο πρόβλημα στην βιβλιογραφία, για το οποίο οι προηγούμενες τεχνικές που θα μπορούσαν να εφαρμοστούν θα αύξαναν σημαντικά την πολυπλοκότητα. Το πλαίσιο χρησιμοποιείται επίσης για να αποδειχτεί ότι η μετατροπή κλεισίματος συναρτήσεων (closure conversion) του μεταγλωττιστή διατηρεί την χωρική και χρονική ασυμπτωτική πολυπλοκότητα του προγράμματος. Αυτό είναι ιδιαιτέρως σημαντικό καθώς έχει βρεθεί ότι συγκεκριμένες υλοποιήσεις του μετασχηματισμού μπορούν να προκαλέσουν διαρροές μνήμης, αλλάζοντας την χωρική ασυμπτωτική πολυπλοκότητα των προγραμμάτων.