Συστήματα Τύπων Με Γραμμικά Δικαιώματα Πρόσβασης

Abstract

Σκοπός της εργασίας είναι η μελέτη των συστημάτων τύπων με γραμμικά δικαιώματα πρόσβασης και η εφαρμογή τους για την ασφάλεια τύπων σε δύο γλώσσες προγραμματισμού. Η πρώτη είναι μια ακολουθιακή γλώσσα με αναφορές, ισχυρή ανάθεση (strong update) και ρητή αποδέσμευση, όπου το σύστημα τύπων εγγυάται την ασφάλεια της πρόσβασης στη μνήμη. Η δεύτερη είναι μια γλώσσα ταυτόχρονου προγραμματισμού, όπου το σύστημα τύπων εγγυάται αφενός την ασφάλεια της πρόσβασης στη μνήμη, αφετέρου την απουσία συνθηκών ανταγωνισμού (data races).Στο πλαίσιο της εργασίας, αρχικά τροποποιήθηκε η γλώσσα let! ώστε να υποστηρίζει γραμμικά δικαιώματα πρόσβασης (linear capabilities). Η γλώσσα let!, όπως και η τροποποίησή της, είναι συναρτησιακές γλώσσες με ισχυρό σύστημα τύπων που υποστηρίζουν αναφορές. Η εισαγωγή των αναφορών σε γλώσσες με ισχυρό σύστημα τύπων δημιουργεί πρόβλημα, αφού λόγω του aliasing δεν μπορούν να γίνουν ασφαλώς η ισχυρή ανάθεση (strong update) και η αποδέσμευση της μνήμης. Στη γλώσσαlet! ο έλεγχος του aliasing γίνεται αντιμετωπίζοντας τις αναφορές με γραμμικό τρόπο, ενώ η έκφραση του let! επιτρέπει ελεγχόμενη μετατροπή των linear τιμών σε unrestricted. Στην ακολουθιακή γλώσσα που παρουσιάζεται σε αυτήν την εργασία τα γραμμικά αντικείμενα που ελέγχουν το aliasing είναι ταδικαιώματα πρόσβασης. Επεκτείνοντας τη γλώσσα ώστε να υποστηρίζει ταυτόχρονο προγραμματισμό, τα ίδια δικαιώματα πρόσβασης μπορούν να χρησιμοποιηθούν για την αποφυγή των συνθηκών ανταγωνισμού.Για την ακολουθιακή και την ταυτόχρονη γλώσσα παρουσιάζονται η σύνταξή τους, το σύστημα τύπων τους και η λειτουργική σημασιολογία τους. Επίσης, έχουν κατασκευαστεί και για τις δύο ελεγκτές τύπων και διερμηνείς.