|
|
 |
Έρχεται ο Εξολοθρευτής
|
|
|
|
|
|
|
Το 1936, ο Alan Turing ―ο μαθηματικός που υπήρξε ένας από τους θεμελιωτές της επιστήμης των υπολογιστών― έδειξε ότι είναι αδύνατη η κατασκευή ενός αλγορίθμου ο οποίος θα αποδεικνύει ότι κάθε δεδομένο πρόγραμμα ολοκληρώνει πάντοτε την εκτέλεσή του. Η ουσία του επιχειρήματός του ήταν ότι ένας τέτοιος αλγόριθμος μπορεί πάντα να αποτύχει αν, αναλύοντας τον εαυτό του, βρει ότι αδυνατεί να σταματήσει. «Οδηγεί σε λογικό παράδοξο», σημειώνει ο David Schmidt, καθηγητής της επιστήμης των υπολογιστών στο Πολιτειακό Πανεπιστήμιο του Κάνσας. Σε πρακτικό επίπεδο, η ανικανότητα για «τερματισμό», όπως λέγεται στη διάλεκτο των υπολογιστών, είναι οικεία σε κάθε χρήστη του λειτουργικού συστήματος Windows ο οποίος πίεσε το ENTER και έμεινε να ατενίζει επ’ αόριστον το εικονίδιο της κλεψύδρας που υποδεικνύει ότι το πρόγραμμα επαναλαμβάνει κάποιον ατέρμονα βρόχο στις ίδιες γραμμές κώδικα.
Η τρέχουσα έκδοση του λειτουργικού συστήματος της Microsoft, γνωστή ως XP, είναι πιο σταθερή από τις προηγούμενες. Ωστόσο, κατασκευαστές εκτυπωτών, συσκευών αναπαραγωγής MP3 και άλλων περιφερειακών συνεχίζουν να γράφουν προβληματικό λογισμικό «οδήγησης», το οποίο επιτρέπει στο περιφερειακό να αλληλεπιδρά με το λειτουργικό σύστημα. Έτσι, οι χρήστες των XP δεν έχασαν δυστυχώς την εξοικείωσή τους με τις παγωμένες κλεψύδρες. Το ερευνητικό τμήμα τής Microsoft έκανε πρόσφατα κάποιες προσπάθειες να αντιμετωπίσει την εδώ και καιρό υποβόσκουσα αίσθηση απογοήτευσης εστιάζοντας σε εργαλεία τα οποία ελέγχουν τα προγράμματα οδήγησης για την απουσία σφαλμάτων.
Το ερευνητικό τμήμα τής Microsoft δεν έχει καταφέρει ακόμα να αντικρούσει τον Turing, ξεκίνησε ωστόσο να παρουσιάζει εργασίες σε συνέδρια για ένα εργαλείο το οποίο ονομάζει Terminator· αυτό προσπαθεί να αποδείξει ότι ένα πρόγραμμα οδήγησης θα ολοκληρώσει τη δουλειά του. «Εξαιτίας του φαντάσματος του Turing, οι επιστήμονες των υπολογιστών δεν κατάφεραν ποτέ μέχρι τώρα να κατασκευάσουν ένα πρακτικό αυτοματοποιημένο εργαλείο επαλήθευσης του τερματισμού μεγάλων προγραμμάτων», ισχυρίζεται ο Byron Cook, θεωρητικός της επιστήμης των υπολογιστών στο Εργαστήριο Έρευνας της Microsoft στο Καίμπριτζ της Αγγλίας, ο οποίος ορίστηκε επί κεφαλής του προγράμματος. «Ο Turing απέδειξε ότι το πρόβλημα είναι μη αποφασίσιμο και, υπό κάποια έννοια, αυτό τρόμαξε τον κόσμο», υποστηρίζει.
Συνδυάζοντας πολλές προηγούμενες τεχνικές από την αυτοματοποιημένη ανάλυση προγραμμάτων, το Terminator δημιουργεί μια πεπερασμένη αναπαράσταση του άπειρου αριθμού καταστάσεων τις οποίες θα μπορούσε να καταλάβει ένας οδηγός συσκευής κατά την εκτέλεση ενός προγράμματος. Κατόπιν προσπαθεί να καταλήξει σε ένα λογικό επιχείρημα που να δείχνει ότι το λογισμικό θα ολοκληρώσει την εργασία του. Αυτό το επιτυγχάνει συνδυάζοντας πολλές «συναρτήσεις κατάταξης», οι οποίες μετρούν το πόσο έχει προχωρήσει ένας οδηγός συσκευής στους βρόχους ενός προγράμματος, δηλαδή σε ακολουθίες εντολών οι οποίες εκτελούνται συνεχώς μέχρι να ικανοποιηθεί μια συγκεκριμένη συνθήκη. Το Terminator ξεκινάει με ένα αρχικό, μάλλον αδύναμο επιχείρημα, το οποίο βελτιώνει συνεχώς με βάση τις πληροφορίες που αποκόμισε από προηγούμενες αποτυχημένες προσπάθειες να δημιουργήσει μια απόδειξη (ένα επαρκώς ισχυρό επιχείρημα). Η διαδικασία μπορεί να απαιτήσει ώρες σε έναν ισχυρό υπολογιστή μέχρις ότου, αν όλα πάνε καλά, να δημιουργηθεί μια απόδειξη η οποία δείχνει ότι καμία διαδρομή εκτέλεσης του προγράμματος οδήγησης δεν θα προκαλέσει το τρομερό φαινόμενο της παγωμένης κλεψύδρας.
Το Terminator, που λειτουργεί μόνο 9 μήνες και ακόμα δεν έχει διανεμηθεί στους εξωτερικούς κατασκευαστές οδηγών συσκευών για τα Windows, έχει ανακαλύψει κάποια σφάλματα τερματισμού στην έκδοση Vista των Windows (που πρόκειται να κυκλοφορήσει σε λίγο) καθώς προσπαθούσε να καταλήξει σε μια απόδειξη. Ο Cook προβλέπει ότι το Terminator θα είναι τελικά σε θέση να βρίσκει αποδείξεις για το 99,9% της τάξης των προγραμμάτων που ολοκληρώνουν την εκτέλεσή τους. (Φυσικά, κάποια προγράμματα έχουν σχεδιαστεί για να εκτελούνται συνεχώς.) Ο Turing, ωστόσο, μπορεί ακόμα να αναπαύεται εν ειρήνη. «Πάντα θα υπάρχει μια είσοδος για το Terminator για την οποία δεν μπορείς να αποδείξεις αν τερματίζεται», λέει ο Cook. «Αλλά αν καταφέρεις να κάνεις το Terminator να λειτουργεί για κάθε πρόγραμμα στον πραγματικό κόσμο, τότε τα υπόλοιπα είναι απλώς λόγια.»
Ο Patrick Cousot, της École Normale Supérieure στο Παρίσι, πρωτοπόρος στη μαθηματική ανάλυση προγραμμάτων, επισμαίνει ότι το Terminator θα μπορεί να λειτουργήσει για ένα περιορισμένο σύνολο καλά ορισμένων εφαρμογών. «Αμφιβάλλω, για παράδειγμα, ότι το πρόγραμμα θα είναι σε θέση να χειριστεί δύσκολα προβλήματα τερματισμού» ―αυτά που χειρίζονται αριθμούς κινητής υποδιαστολής ή προγράμματα εκτελούμενα την ίδια στιγμή. Ο Cook δεν διαφωνεί, και λέει ότι σκοπεύει να αναπτύξει μεθόδους απόδειξης τερματισμού και για τέτοιου είδους προγράμματα. Ωστόσο, η εύρεση ενός τρόπου που να εξασφαλίζει ότι τα πιο σύνθετα προγράμματα δεν «παγώνουν» αποτελεί τόσο δύσκολη πρόκληση ώστε ο Cook πιστεύει πως πιθανόν να χρειαστεί να αφιερώσει σε αυτή την έρευνα το υπόλοιπο της καριέρας του.
|
|
|
|
|
|
