Στατικές εγγυήσεις ασφάλειας για γλώσσες με ταυτόχρονο προγραμματισμό

Abstract

Modern computers ranging from desktop PC to supercomputers have multicore processors. Multi-core processors bring more computing power into a chip and software plays an essential role in utilizing this power. Multithreaded programming is a widely used paradigm for exploiting concurrency in multicore systems. An inherent side-effect of this paradigm is non-determinism of execution, which allows for invalid execution interleavings to occur. Such interleavings cannot be easily reproduced, thereby making the development of reliable concurrent software a hard task. Data races and deadlocks are two wellknown consequences of non-deterministic execution. Informally, a data race occurs when multiple threads concurrently access the same memory location without synchronization. A set of threads reaches a deadlocked state, when each thread in that set is waiting for a lock in cyclic order. This dissertation shows that it is possible to increase the reliability of concurrent programs, by eliminating memory access violations, data races and deadlocks from multithreaded programs. In particular, we present the theory and implementation of a series of type systems and static analyses that provide absolute guarantees regarding multithreaded program execution. In the theoretical parts, we present the formal semantics of the type systems and languages and give formal soundness proofs. In the implementation parts we discuss how we integrated these formal systems in real programming languages and the challenges that we met. We also provide extensive measurements for the performance of each analysis and compare alternative techniques.

Τα σύγχρονα υπολογιστικά συστήματα από επιτραπέζιους υπολογιστές μέχρι υπερυπολογιστές φέρουν πολυπύρηνους (multicore) επεξεργαστές. Οι πολυπύρηνοι επεξεργαστές αποδίδουν περισσότερη υπολογιστική ισχύ σε ένα τσιπ και το λογισμικό διαδραματίζει καθοριστικό ρόλο στην αξιοποίηση της. Ο πολυνηματικός προγραμματισμός είναι ένα ευρέως χρησιμοποιούμενο πρότυπο προγραμματισμού για την αξιοποίηση του ταυτοχρονισμού σε πολυπύρηνα συστήματα. Μια εγγενής παρενέργεια αυτού του προτύπου είναι η μη ντετερμινιστική εκτέλεση των νημάτων, η οποία επιτρέπει να συμβούν ανεπιθύμητες νηματικές διεμπλοκές (thread interleavings). Τέτοιες διεμπλοκές δεν μπορούν να αναπαραχθούν εύκολα αφού εξαρτώνται από τον χρόνο, καθιστώντας δύσκολη την αξιόπιστη ανάπτυξη ταυτόχρονου λογισμικού. Οι συνθήκες ανταγωνισμού (data races) και τα αδιέξοδα (deadlocks) είναι δύο γνωστές συνέπειες της μη ντετερμινιστικής εκτέλεσης. Η συνθήκη ανταγωνισμού είναι μία κατάσταση κατά την οποία πολλαπλά νήματα έχουν ταυτόχρονη πρόσβαση στην ίδια θέση μνήμης χωρίς συγχρονισμό. Ένα σύνολο από νήματα φτάνει σε αδιέξοδο, όταν κάθε νήμα βρίσκεται σε αναμονή για μια κλειδαριά, η οποία είναι κλειδωμένη από κάποιο άλλο νήμα του ίδιου συνόλου. Σε αυτή την διατριβή δείχνουμε ότι είναι δυνατό να αυξηθεί η αξιοπιστία των ταυτόχρονων προγραμμάτων, με την εξάλειψη των παραβιάσεων πρόσβασης μνήμης, συνθηκών ανταγωνισμού και αδιεξόδων από πολυνηματικά προγράμματα. Συγκεκριμένα, παρουσιάζουμε την θεωρία και υλοποίηση συστημάτων τύπων (type systems) και στατικών αναλύσεων (static analyses) που παρέχουν κάποιες εγγυήσεις αξιοπιστίας σχετικά με την πολυνηματική εκτέλεση προγραμμάτων. Στα θεωρητικά τμήματα της διατριβής παρουσιάζουμε την τυπική σημασιολογία (formal semantics) των συστημάτων τύπων και των γλωσσών και δίνουμε τυπικές αποδείξεις ορθότητας. Στα πρακτικά τμήματα αναλύουμε την ενσωμάτωση των τυπικών συστημάτων που αναπτύξαμε σε πραγματικές γλώσσες προγραμματισμού και τις προκλήσεις που συναντήσαμε. Επίσης παρουσιάζουμε εκτεταμένες μετρήσεις για την απόδοση των αναλύσεων μας και τις συγκρίνουμε με εναλλακτικές τεχνικές.