Παραλληλοποίηση των Dynamic Partial Order Reduction Αλγορίθμων στον Concuerror

Abstract

Ο έλεγχος και η επαλήθευση των ταυτόχρονων προγραμμάτων είναι μία πολύπλοκη εργασία. Λόγω του μη ντετερμινιστικού τρόπου με τον οποίο δουλεύει ο scheduler ενός συστήματος, μπορεί μόνο μερικά interleavings από διεργασίες να οδηγούν σε σφάλματα και συνεπώς, για να ελεγχθεί η ορθότητα ενός προγράμματος, πρέπει να εξεταστούν όλα τα πιθανά interleavings. Ο αριθμός, όμως, αυτών των interleavings είναι εκθετικός ως προς το μέγεθος του προγράμματος και τον αριθμό των νημάτων. Η πιο αποτελεσματική μέθοδος για να λυθεί αυτό το πρόβλημα είναι το stateless model checking με τη χρήση αναγωγής σε δυναμικές σχέσεις μερική διάταξης (Dynamic Partial Order Reduction ή DPOR). Καθώς τα παράλληλα συστήματα επεξεργασίας έχουν γίνει το κυρίαρχο πρότυπο των σύγχρονων υπολογιστικών συστημάτων, η παραλληλοποίηση των διαφόρων DPOR αλγορίθμων είναι αναγκαία για την κλιμάκωση αυτών των αλγορίθμων στους σύγχρονους υπολογιστές. Αυτή η διπλωματική εργασία ασχολείται με τη παραλληλοποίηση του Concuerror, ενός stateless model checking εργαλείου που χρησιμοποιεί διάφορους DPOR αλγόριθμους για να ελέγξει ταυτόχρονα προγράμματα γραμμένα σε Erlang. Συγκεκριμένα, εστιάσαμε στο να σχεδιάσουμε παράλληλες εκδοχές για τα τους δύο βασικούς αλγορίθμους του Concuerror: τον source-DPOR και τον optimal-DPOR και στο να καταστήσουμε εφικτή την παράλληλη εξερεύνηση διαφορετικών interleavings απο τον Concuerror. Επίσης, αξιο- λογήσαμε την επιτάχυνση και την κλιμακωσιμότητα των υλοποιήσεων μας σε διάφορα benchmarks που χρησιμοποιούνται ευρέως για την αξιολόγηση DPOR αλγορίθμων. Συ- γκεκριμένα, η υλοποίηση μας επιτυγχάνει σημαντική επιτάχυνση και καταφέρνει να δια- τηρήσει κλιμακωσιμότητα για 32 παράλληλους schedulers.