Σφυρηλάτηση και αναζήτηση που αποδεικνύει την αξία της
Το πρόβλημα με το παλιό κόλπο
Κάθε σοβαρό σύστημα λογισμικού έχει μερικά κομμάτια κώδικα που έχουν πολύ μεγαλύτερη σημασία από ό,τι υποδηλώνει το μέγεθός τους. Ένας βρόχος που εκτελείται εκατομμύρια φορές. Μια πράξη bit σε μια διαδρομή συμπίεσης. Μια μικρή ρουτίνα πινάκων. Ένας πυρήνας αριθμητικής υπολοίπων. Το είδος του κώδικα που φαίνεται ακίνδυνο στην αναθεώρηση και μετά αποφασίζει ήσυχα τον λογαριασμό ενέργειας, τον προϋπολογισμό καθυστέρησης ή τον αριθμό των μηχανημάτων που πρέπει να αγοράσετε. Πολύ δημοκρατικό το λογισμικό. Μια μικροσκοπική συνάρτηση μπορεί να χαλάσει τη συνάντηση για όλους.
Ιστορικά, αυτοί οι πυρήνες βελτιώνονται από ανθρώπους. Ένας ανώτερος μηχανικός θυμάται ένα κόλπο από μια εργασία. Κάποιος ψάχνει μια παλιά ανάρτηση σε φόρουμ. Γράφεται μια σουίτα συγκριτικής αξιολόγησης. Δοκιμάζονται μερικοί υποψήφιοι. Ο ταχύτερος κερδίζει αν εξακολουθεί να φαίνεται σωστός. Στη συνέχεια, ο οργανισμός τον παγώνει, γιατί το να τον ξαναγγίξεις μοιάζει με το να τρυπάς έναν κοιμισμένο μετασχηματιστή με πιρούνι.
Το Forge είναι έρευνα για μια καλύτερη εκδοχή αυτής της διαδικασίας. Είναι μια μηχανή σύνθεσης προγραμμάτων για μικρές, κρίσιμες υλοποιήσεις: δώστε της μια τυποποιημένη προδιαγραφή και ιδιότητες, αφήστε την να αναζητήσει υποψήφια προγράμματα, να μετρήσει και να συγκρίνει ανταλλάγματα, να επαληθεύσει ισοδυναμία και στη συνέχεια να μεταφέρει την ανακαλυφθείσα υλοποίηση σε στόχους που έχουν σημασία. Η σημαντική λέξη δεν είναι η αναζήτηση. Η σημαντική λέξη είναι ακόμα. Πρέπει ακόμα να είναι σωστό.
Γι' αυτό το Forge ζει στην έρευνα. Δεν είναι ένα δημόσιο κουμπί προϊόντος όπου κάποιος πληκτρολογεί κάντο πιο γρήγορο και λαμβάνει ένα θαύμα. Είναι ένας πάγκος εργασίας σύνθεσης για πειράματα συνεργατών, ανακάλυψη πυρήνων και έρευνα για το πόσο μακριά μπορεί να φτάσει η αυτοματοποιημένη αναζήτηση όταν συνδέεται με επαλήθευση αντί για θέατρο συγκριτικής αξιολόγησης.
Μια προδιαγραφή είναι η γραμμή εκκίνησης
Η βελτιστοποίηση χωρίς προδιαγραφή είναι απλώς τζόγος με ωραιότερα ονόματα μεταβλητών. Τη στιγμή που εμφανίζεται ένας έξυπνος υποψήφιος, η ομάδα πρέπει να γνωρίζει τι υποτίθεται ότι διατηρεί. Χειρίζεται κάθε είσοδο ή μόνο τις φιλικές από τη συγκριτική αξιολόγηση; Σέβεται τη συμπεριφορά υπερχείλισης; Είναι η αλγεβρική ταυτότητα έγκυρη υπό την αναπαράσταση που χρησιμοποιείται στην πραγματικότητα; Διατηρεί την ίδια σημασιολογία όταν μεταφέρεται σε διαφορετικό backend;
Το Forge ξεκινά από τυποποιημένες εκφράσεις και ιδιότητες επειδή η αναζήτηση χρειάζεται ένα όριο. Το όριο ορίζει τι θεωρείται ισοδύναμο. Χωρίς αυτό, η μηχανή μπορεί να βρει κάτι εκπληκτικά γρήγορο διαγράφοντας τη μισή δουλειά. Οι υπολογιστές είναι εξαιρετικοί στην κακόβουλη συμμόρφωση όταν η σύμβαση είναι ασαφής.
Η πλευρά της αναζήτησης είναι σκόπιμα πληθυντική. Η απαριθμητική αναζήτηση είναι χρήσιμη όταν ο χώρος είναι αρκετά μικρός για να καλυφθεί. Το CEGIS είναι χρήσιμο όταν τα αντιπαραδείγματα μπορούν να καθοδηγήσουν τη βελτίωση. Ο γενετικός προγραμματισμός και το MCTS εξερευνούν διαφορετικά. Η αναζήτηση με καθοδήγηση μηχανικής μάθησης μπορεί να μάθει μοντέλα κόστους και να δώσει προτεραιότητα σε υποσχόμενες περιοχές. Κανένα από αυτά δεν είναι καθολικά το καλύτερο. Αυτό δεν είναι αδυναμία. Έτσι συμπεριφέρεται η αναζήτηση στον πραγματικό κόσμο. Αν ένα σφυρί έλυνε κάθε πυρήνα, τα κουτιά εργαλείων θα ήταν πολύ βαρετά και οι κατασκευαστές υλικού θα ήταν άνεργοι.
Το ερευνητικό ερώτημα είναι πώς να συνδυαστούν αυτές οι μηχανές με αρκετή πίεση απόδειξης ώστε το αποτέλεσμα να μην είναι απλώς έξυπνο. Ένας συντεθειμένος πυρήνας πρέπει να επιβιώσει τόσο από τη συγκριτική αξιολόγηση της ευτυχούς διαδρομής όσο και από τον επαληθευτή της δυσμενούς διαδρομής. Διαφορετικά, η βελτίωση δεν είναι μηχανική. Είναι ένα μαγικό κόλπο με κόστος συντήρησης.
Ο επαληθευτής είναι ο ενήλικας στο δωμάτιο
Το Forge χρησιμοποιεί μια στοίβα επαλήθευσης, επειδή κανένας έλεγχος από μόνος του δεν αρκεί για κάθε τομέα. Τα γρήγορα παραδείγματα είναι φθηνά και χρήσιμα. Οι δοκιμές ιδιοτήτων εντοπίζουν ευρείες κατηγορίες σφαλμάτων και συμπυκνώνουν τα αντιπαραδείγματα σε κάτι που μπορεί να διαβάσει ένας άνθρωπος. Οι λύτες SMT, όπως οι Z3 και CVC5, μπορούν να αποδείξουν ισοδυναμία όπου η κωδικοποίηση είναι επιλύσιμη. Ο εξαντλητικός έλεγχος είναι πρακτικός για μικρούς τομείς. Ο κορεσμός ισοδυναμίας με E-graph δίνει μια άλλη διαδρομή μέσω της αλγεβρικής ισοδυναμίας.
Η στοίβα έχει σημασία επειδή οι πυρήνες αποτυγχάνουν με ενοχλητικούς τρόπους. Ένας υποψήφιος μπορεί να περάσει κάθε συνηθισμένο σημείο αναφοράς και παρόλα αυτά να είναι λάθος σε μια ακραία περίπτωση. Μπορεί να είναι σωστός για προσημασμένες εισόδους και λάθος για μη προσημασμένες. Μπορεί να είναι σωστός σε ένα μαθηματικό πεδίο και λάθος αφού η επιλεγμένη αναπαράσταση υπερχειλίσει. Μπορεί να είναι σωστός πριν από τη μετατροπή και διακριτικά λάθος μετά από μια απόφαση επιλογής εντολών. Ο επαληθευτής υπάρχει επειδή η αισιοδοξία δεν είναι στρατηγική δοκιμών. Ελέγξαμε. Επανειλημμένα. Παραμένει αλήθεια.
Υπάρχει επίσης ένας πρακτικός λόγος να διατηρηθούν αρκετές διαδρομές απόδειξης. Οι τυπικές μέθοδοι είναι ισχυρές, αλλά δεν είναι δωρεάν. Κάποιες κωδικοποιήσεις υπερβαίνουν το χρονικό όριο. Κάποιοι τομείς είναι πολύ μεγάλοι για εξαντλητικό έλεγχο. Κάποιες ιδιότητες είναι ευκολότερο να δοκιμαστούν πιθανοτικά πρώτα και να αποδειχθούν αργότερα. Το Forge αντιμετωπίζει την επαλήθευση ως χωνί, όχι ως τελετουργικό αγνότητας. Οι φθηνοί έλεγχοι απορρίπτουν τον προφανή παραλογισμό. Οι ισχυρότεροι έλεγχοι προστατεύουν τον τελικό υποψήφιο.
Το γρήγορο δεν είναι ένας αριθμός
Η δουλειά για τις επιδόσεις γίνεται γελοία όταν επιτρέπεται σε μία μετρική να κυριαρχεί σε κάθε συζήτηση. Η καθυστέρηση έχει σημασία. Ο αριθμός των πράξεων έχει σημασία. Η χρήση μνήμης έχει σημασία. Η πίεση καταχωρητών έχει σημασία. Ο χρόνος μεταγλώττισης μερικές φορές έχει σημασία. Η φορητότητα έχει σημασία όταν ο ίδιος πυρήνας πρέπει να ζήσει σε περισσότερα από ένα backends. Ένας υποψήφιος που κερδίζει σε καθυστέρηση καίγοντας καταχωρητές σαν μικρή φωτιά μπορεί να είναι λάθος για τον πραγματικό στόχο. Ένας υποψήφιος που είναι μικρός αλλά αργός μπορεί να είναι χρήσιμος κάπου αλλού. Το πλαίσιο παραμένει αήττητο.
Το Forge επομένως πλαισιώνει τη βελτιστοποίηση ως πρόβλημα Pareto. Η μηχανή μπορεί να αναζητήσει σε πολλούς στόχους αντί να προσποιείται ότι υπάρχει ένα καθολικό σκορ που παραδίδεται από ένα πολύ σίγουρο υπολογιστικό φύλλο. Η χρήσιμη έξοδος δεν είναι πάντα ο μοναδικός ταχύτερος υποψήφιος. Μερικές φορές είναι μια οικογένεια υποψηφίων με ορατούς συμβιβασμούς, ώστε ένας μηχανικός να μπορεί να επιλέξει αυτόν που ταιριάζει στον περιορισμό ανάπτυξης.
Γι' αυτό επίσης δεν μου αρέσουν οι γυμνοί ισχυρισμοί επιτάχυνσης σε αναρτήσεις ιστολογίου. Η σελίδα έρευνας μπορεί να περιγράφει εσωτερικές προσδοκίες και πειραματικούς στόχους, αλλά οι δημόσιοι ισχυρισμοί χρειάζονται φρέσκες εκτελέσεις, τρέχον υλικό, τρέχουσες σημαίες μεταγλωττιστή και ακριβές πλαίσιο φόρτου εργασίας. Διαφορετικά, ο αριθμός γίνεται ενθύμιο. Τα ενθύμια είναι ωραία. Δεν είναι αρχιτεκτονική.
Ο ειλικρινής ισχυρισμός είναι ούτως ή άλλως ισχυρότερος: το Forge αφορά το να κάνει την αναζήτηση αναπαράξιμη, συγκρίσιμη και ελέγξιμη. Όταν ένας υποψήφιος κερδίζει, θα πρέπει να ξέρουμε ποιον στόχο κέρδισε, ποιους υποψηφίους νίκησε, ποιος επαληθευτής τον αποδέχτηκε και σε ποιο backend απευθύνεται. Αυτό είναι πολύ πιο χρήσιμο από έναν αριθμό που αιωρείται σε μια παρουσίαση και φαίνεται ακριβός.
Η μετατροπή είναι εκεί όπου οι αποδείξεις δοκιμάζονται
Μια ανακάλυψη που γίνεται από το σύστημα είναι χρήσιμη μόνο αν επιβιώσει μέχρι να φτάσει σε πραγματικούς στόχους. Η έρευνα του Forge καλύπτει τη μεταγλώττιση σε backends όπως x86-64, RISC-V, WASM, διαδρομές GPU μέσω Vulkan, C και Verilog. Αυτή η λίστα στόχων δεν είναι διακόσμηση. Κάθε backend έχει τους δικούς του περιορισμούς, σχήματα εντολών, συμπεριφορά μνήμης και τρόπους αποτυχίας. Η ίδια προδιαγραφή πρέπει να διατηρήσει το νόημά της ενώ η υλοποίηση γίνεται κάτι που ο στόχος μπορεί πραγματικά να εκτελέσει.
Εδώ είναι που η σύνθεση συνδέεται με το υπόλοιπο stack του Dweve. Το Core θέλει αποδοτικούς εσωτερικούς βρόχους. Το Numerus ενδιαφέρεται για ντετερμινιστικούς αριθμητικούς πυρήνες. Το BitWeave θέλει δυαδικές πράξεις διανυσμάτων και πινάκων που δεν σπαταλούν την CPU. Το Kera ενδιαφέρεται για τη μεταγλώττιση γράφων υπολογισμού σε πραγματικό υλικό. Το Forge μπορεί να τροφοδοτήσει αυτά τα επίπεδα μόνο αν η παραγόμενη υλοποίηση είναι κάτι περισσότερο από γρήγορη. Πρέπει να είναι ισοδύναμη, αρκετά φορητή για τον επιλεγμένο στόχο και επιθεωρήσιμη όταν κάτι αλλάζει.
Τι σημαίνει αυτό για τις ομάδες
Για μια ομάδα, η ενδιαφέρουσα αλλαγή δεν είναι ότι μια μηχανή μπορεί να ανακαλύψει έναν ταχύτερο πυρήνα. Είναι ότι η εργασία με πυρήνες εξαρτάται λιγότερο από τη λαϊκή σοφία. Αντί ένας ειδικός να θυμάται το σωστό κόλπο, η διαδικασία γίνεται: δήλωσε τη σύμβαση, εξερεύνησε τον χώρο, μέτρησε τους υποψήφιους, απόδειξε την ισοδυναμία, καταγράψε τον συμβιβασμό και δημιούργησε τον κώδικα για τον στόχο. Οι άνθρωποι εξακολουθούν να αποφασίζουν. Απλώς σταματούν να κάνουν όλη την ανακάλυψη με το χέρι.
Αυτό έχει σημασία για τις λειτουργίες επειδή το χρέος απόδοσης είναι ακριβό με τρόπο που οι οργανισμοί συχνά κρύβουν. Ένας αργός πυρήνας γίνεται περισσότεροι διακομιστές. Περισσότεροι διακομιστές γίνονται περισσότερο κόστος, περισσότερη ενέργεια, μεγαλύτερη πολυπλοκότητα ανάπτυξης και περισσότερος θόρυβος στον σχεδιασμό. Μια λάθος βελτιστοποίηση γίνεται περιστατικά. Ένα σωστό αλλά ατεκμηρίωτο κόλπο γίνεται μελλοντικός κίνδυνος μετανάστευσης. Το Forge είναι έρευνα για τη μείωση αυτού του σωρού από αποφευκτέα προβλήματα.
Υπάρχει και μια πολιτισμική αλλαγή. Η χειροκίνητη εργασία απόδοσης συχνά επιβραβεύει τους ηρωισμούς. Κάποιος εξαφανίζεται στη σπηλιά και επιστρέφει με ένα έξυπνο κόλπο σε επίπεδο bit. Όλοι χειροκροτούν, κανείς δεν το καταλαβαίνει πλήρως και η εταιρεία έχει αποκτήσει ένα μικρό ιερό αντικείμενο. Το Forge ωθεί τη διαδικασία προς τα αποδεικτικά στοιχεία: εδώ είναι η προδιαγραφή, εδώ είναι η διαδρομή αναζήτησης, εδώ είναι οι απορριφθέντες υποψήφιοι, εδώ είναι ο επαληθευτής, εδώ είναι το επιλεγμένο backend. Λιγότερη μυθολογία. Περισσότερες αποδείξεις.
Πού η δουλειά είναι ακόμα δύσκολη
Τίποτα από αυτά δεν κάνει τη σύνθεση εύκολη. Οι προδιαγραφές είναι δύσκολες. Αν η προδιαγραφή είναι λάθος, η μηχανή μπορεί πιστά να ανακαλύψει το λάθος πράγμα. Οι χώροι αναζήτησης μπορούν να εκραγούν. Οι επιλυτές μπορούν να εξαντλήσουν τον χρόνο. Τα μοντέλα κόστους μπορούν να παραπλανήσουν. Τα backends μπορούν να αποκαλύψουν λεπτομέρειες που η αφηρημένη έκφραση δεν ενδιαφερόταν. Η επαλήθευση μπορεί να είναι ισχυρή σε έναν τομέα και άβολη σε έναν άλλο. Όποιος πουλά τη σύνθεση προγραμμάτων ως μηχάνημα αυτόματης πώλησης για βέλτιστο κώδικα είτε παραλείπει τα δύσκολα μέρη είτε χρεώνει επιπλέον για την απογοήτευση.
Το Forge είναι ενδιαφέρον ακριβώς επειδή αντιμετωπίζει αυτά τα δύσκολα μέρη άμεσα. Συνδυάζει πολλές στρατηγικές αναζήτησης. Κρατά την επαλήθευση κοντά. Αντιμετωπίζει τους στόχους ως συμβιβασμούς. Στοχεύει σε πραγματικά backends. Παραμένει ερευνητικό πρόγραμμα επειδή μαθαίνουμε ακόμα πού βρίσκεται το όριο μεταξύ αυτόματης ανακάλυψης, ανθρώπινης κρίσης, περιορισμών των επιλυτών και πραγματικότητας ανάπτυξης.
Αυτό το όριο αξίζει να εξερευνηθεί. Η βιομηχανία λογισμικού έχει πάρα πολλούς μικρούς θερμούς βρόχους, πάρα πολύ διπλότυπη λαϊκή σοφία για την απόδοση και πάρα πολλές βελτιστοποιήσεις που κανείς δεν θέλει να ξαναγγίξει. Αν το Forge μπορεί να μετατρέψει έστω και μέρος αυτής της δουλειάς σε μια επαναλήψιμη διαδικασία αποδεικτικών στοιχείων, το αποτέλεσμα δεν είναι απλώς ταχύτερος κώδικας. Είναι πιο ήρεμος κώδικας. Ο πιο ήρεμος κώδικας υποτιμάται, κυρίως από ανθρώπους που δεν έχουν δεχτεί κλήση στις 02:17.
Τι χρειάζεται ένα καλό τρέξιμο του Forge
Ένα σοβαρό πείραμα με το Forge ξεκινά πριν τρέξει η μηχανή. Η ομάδα πρέπει να φέρει έναν πραγματικό πυρήνα, όχι ένα αόριστο παράπονο για τις επιδόσεις. Χρειάζεται αντιπροσωπευτικά δεδομένα εισόδου, γνωστές ακραίες περιπτώσεις, στοχευμένο υλικό, τρέχοντα σημεία αναφοράς και τον επιχειρηματικό λόγο για τον οποίο έχει σημασία αυτός ο πυρήνας. Διαφορετικά, η μηχανή σύνθεσης μπορεί να ξοδέψει πολύ χρόνο λύνοντας ένα πρόβλημα που κανείς στην πραγματικότητα δεν έχει. Τα ερευνητικά εργαλεία δεν είναι άτρωτα στα σκουπίδια στην είσοδο. Απλώς κάνουν τα σκουπίδια πιο ακριβά στην επιθεώρηση.
Η πιο χρήσιμη είσοδος είναι ένα μικρό, ευκρινές συμβόλαιο. Τι υποτίθεται ότι υπολογίζει η συνάρτηση; Ποιοι αλγεβρικοί νόμοι έχουν σημασία; Ποια συμπεριφορά υπερχείλισης είναι σκόπιμη; Ποια εύρη τιμών είναι αδύνατα εξ ορισμού και ποια απλώς δεν εμφανίστηκαν στην τελευταία δοκιμή; Ποιες έξοδοι ανέχονται προσέγγιση και ποιες όχι; Μια ομάδα που δεν μπορεί να απαντήσει σε αυτές τις ερωτήσεις πιθανότατα δεν έχει ακόμη πρόβλημα βελτιστοποίησης. Έχει πρόβλημα αποσαφήνισης προϊόντος που φοράει καπέλο μεταγλωττιστή.
Ένα καλό τρέξιμο χρειάζεται επίσης μια στοχευμένη στάση. Το x86-64 και το RISC-V δεν είναι το ίδιο. Το WASM έχει διαφορετικούς περιορισμούς. Οι διαδρομές GPU Vulkan ενδιαφέρονται για σχήματα και μετακίνηση μνήμης. Το Verilog εγείρει ερωτήματα υλικού που οι συνηθισμένες ομάδες εφαρμογών σπάνια απολαμβάνουν πριν από τον καφέ. Το Forge μπορεί να εξερευνήσει τη μεταγλώττιση για συγκεκριμένους στόχους, αλλά δεν μπορεί να αποφασίσει οργανωτικές προτεραιότητες. Αν η φορητότητα έχει μεγαλύτερη σημασία από την ταχύτητα σε έναν στόχο, πείτε το. Αν η καθυστέρηση υπερτερεί της μνήμης, πείτε το. Αν η πίεση καταχωρητών είναι το πρακτικό όριο, πείτε το κι αυτό. Η μηχανή είναι ισχυρή, όχι διόρατη.
Η έξοδος θα πρέπει να αντιμετωπίζεται σαν ένα πακέτο αποδεικτικών στοιχείων. Υποψήφιος, στόχος, διαδρομή απόδειξης, αντιπαραδείγματα που απορρίφθηκαν, παρασκηνιακό σύστημα, πλαίσιο σημείων αναφοράς και ανοιχτές επιφυλάξεις. Αυτό το πακέτο είναι που επιτρέπει στους ανθρώπους να πάρουν μια συνετή απόφαση. Μερικές φορές η νικητήρια κίνηση είναι να υιοθετηθεί ο υποψήφιος. Μερικές φορές είναι να κρατηθεί ο παλιός πυρήνας επειδή ο συμβιβασμός στη φορητότητα δεν αξίζει τον κόπο. Μερικές φορές η ανακάλυψη είναι ότι η προδιαγραφή ήταν πολύ χαλαρή. Και τα τρία αποτελέσματα είναι χρήσιμα. Μόνο ένα από αυτά φαίνεται συναρπαστικό σε μια επίδειξη, γι' αυτό οι επιδείξεις είναι φτωχό υποκατάστατο της μηχανικής.
Το μάθημα
Το μάθημα του Forge είναι απλό: οι επιδόσεις δεν πρέπει να ξεπερνούν την απόδειξη. Η αναζήτηση είναι ισχυρή, αλλά μια μηχανή αναζήτησης χωρίς επαλήθευση είναι απλώς ένας πολύ ενεργητικός τρόπος να δημιουργήσεις σφάλματα. Η επαλήθευση είναι ισχυρή, αλλά χωρίς αναζήτηση περιμένει από τους ανθρώπους να φέρουν υποψηφίους. Το Forge συνδυάζει τα δύο και αναρωτιέται ποιους πυρήνες μπορούμε να ανακαλύψουμε όταν επιτρέπεται στη μηχανή να εξερευνά, αλλά δεν της επιτρέπεται να ψεύδεται.
Αυτή είναι η έρευνα που αξίζει να γίνει. Τυποποιημένες προδιαγραφές, αναζήτηση υποψηφίων, διοχετεύσεις απόδειξης, στόχοι Pareto και μεταγλώττιση για συγκεκριμένους στόχους. Όχι μαγεία. Όχι συντομεύσεις προϊόντος. Ένας τρόπος να φτιάξεις καλύτερο μικρό κώδικα με συνημμένα αποδεικτικά στοιχεία.