Συστηματικός Έλεγχος Ορθότητας Του Read-copy-update Υπό Ακολουθιακά Συνεπή Και Ασθενή Μοντέλα Μνήμης

Abstract

Ο συστηματικός έλεγχος ορθότητας και η επαλήθευση παράλληλων προγραμμάτων,παρουσιάζουν σημαντικές δυσκολίες. Ας θεωρήσουμε, για παράδειγμα,μια βιβλιοθήκη προγραμμάτων που χρησιμοποιείται για το συγχρονισμό μεταξύ διεργασιών,ή για τον έλεγχο πρόσβασης σε κάποιες κοινές μεταξύ διαφόρωννημάτων δομές δεδομένων. Κατά την κατασκευή μιας συστηματικής διαδικασίας ελέγχουγια μία τέτοια βιβλιοθήκη, πρέπει να ληφθούν υπ' όψιν: οι πολλοίπιθανοί τρόποι με τους οποίους τα νήματα-πελάτες έχουν πρόσβασηστη βιβλιοθήκη, οι διαφορετικοί τρόποι με τους οποίους τα νήματακαι η βιβλιοθήκη αλληλεπιδρούν, καθώς και οποιεσδήποτε επιπτώσειςοφείλονται στο ασθενές μοντέλο μνήμης (weak memory model) που χρησιμοποιείταιαπό τους σύγχρονους μικροεπεξεργαστές.Ο σκοπός της διπλωματικής αυτής εργασίας είναι ο συστηματικός έλεγχοςορθότητας της βιβλιοθήκης Read-Copy-Update, ενός μηχανισμού συγχρονισμούπου χρησιμοποιείται ευρέως στον πυρήνα του λειτουργικού συστήματος Linux.Για το σκοπό αυτό, χρησιμοποιήθηκε το Nidhugg, ένα εργαλείο ελέγχου μοντέλουχωρίς αποθήκευση της κατάστασης (stateless model checking tool) για C/pthreads προγράμματα,το οποίο ενσωματώνει επεκτάσεις για τη μελέτητων επιπτώσεων διαφόρων ασθενών μοντέλων μνήμης, όπως TSO, PSO και POWER.Κατασκευάσαμε μία μη-φορμαλιστική, αλλά πλήρη λίστα προδιαγραφών για τοRead-Copy-Update, καθώς και μία κατάλληλη συλλογή προγραμμάτων που στοχεύουνστον συστηματικό έλεγχό του. Στην εργασία αυτή, παρουσιάζουμε την πρώτη μηχανικήεπαλήθευση της ιδιότητας της "Περιόδου Χάριτος" (Grace-Period guarantee) του RCU,χρησιμοποιώντας το Tree RCU, το οποίο αποτελεί την κύρια υλοποίηση που χρησιμοποιείταιστον πυρήνα του Linux.Επιπρόσθετα, αναπαρηγάγαμε ένα γνωστόσφάλμα (bug) στον πυρήνα χρησιμοποιώντας το Nidhugg, ενώ αντίθετα, δείξαμε ότιένα προηγουμένως αναφερόμενο ως bug, στην πραγματικότητα δεν αποτελεί bug.Τέλος, ελέγχθηκαν επίσης κάποιες ακόμη ιδιότητες του Tree RCU και του Tiny RCU.