Αποδειξη Ορθοτητας Συλλεκτη Σκουπιδιων Αντιγραφης

Abstract

Η διαχείριση της μνήμης που έχει εκχωρηθεί σε ένα πρόγραμμα αποτελεί πολύ σημαντικό κομμάτι του προγράμματος. Με την έννοια της διαχείρισης της μνήμης εννοούμε όλες τις απαραίτητες ενέργειες που πρέπει να γίνουν για να διασφαλιστεί ότι όλα τα αντικείμενα της μνήμης των οποίων ο χρόνος ζωής έχει παρέλθει θα πρέπει να αφαιρεθούν και η μνήμη την οποία καταλάμβαναν να αποδοθεί ελεύθερη προς χρήση. Η διαχείριση αυτή μπορεί να γίνει είτε από τον ίδιον τον προγραμματιστή, πράγμα που συμβαίνει σε γλώσσες όπως η C και η Pascal, είτε από μια διαδικασία η οποία ονομάζεται συλλέκτης σκουπιδιών όπως στις συναρτησιακές γλώσσες προγραμματισμού αλλά και σε ευρέως χρησιμοποιούμενες γλώσσες όπως η Java αλλά και η C#.Η διαχείριση της μνήμης από τον ίδιον τον προγραμματιστή έχει κάποια σημαντικά μειονεκτήματα όπως ο χρόνος που θα πρέπει να αφιερώσει κατά τη γραφή του πηγαίου κώδικα για να υλοποιήσει την διαχείριση αυτή, ο κώδικας θα γίνει δυσκολότερος στην συντήρησή του αλλά και πιθανώς θα υπάρξουν και λάθη στον κώδικα τα οποία θα οδηγήσουν σε σημαντικές δυσλειτουργίες του προγράμματος. Η διαδικασία της συλλογής σκουπιδιών πραγματοποιείται κατά την ώρα εκτέλεσης του προγράμματος. Την διαδικασία αυτή αναλαμβάνει το ίδιο το πρόγραμμα και ο προγραμματιστής δεν αναμιγνύεται.Σκοπός της εργασίας αυτής είναι η απόδειξη της ορθότητας της λειτουργίας ενός τέτοιου συλλέκτη σκουπιδιών. Γίνεται εύκολα αντιληπτό πως μια δυσλειτουργία ενός συλλέκτη σκουπιδιών μιας γλώσσας αυτόματα θα περνούσε σε όλα τα προγράμματα που θα παράγονταν από την γλώσσα αυτήν. Ο συλλέκτης σκουπιδιών που επιλέχτηκε για απόδειξη είναι ο semi-space garbage collector.Για την απόδειξη δημιουργήθηκε ένας συλλέκτης σκουπιδιών semi-space σε γλώσσα ANSI C και χρησιμοποιήθηκαν τα εργαλεία Caduceus και Frama-c.