Ανάλυση και Μοντελοποίηση Αλγορίθμων Χρονοδρομολόγησης με Χρονισμένα Αυτόματα

Abstract

Προβλήματα χρονοδρομολόγησης απαντώνται σε πολλούς κλάδους και ένα εύρος περιπτώσεων, βρίσκοντας εφαρμογές σε πεδία που εκτείνονται από τον προγραμματισμό παραγωγής μέχρι την κατανομή των εργασιών ενός υπολογιστικού συστήματος. Άξονα αυτών αποτελεί η βέλτιστη αξιοποίηση μιας σειράς περιορισμένων πόρων (resources) στους οποίους βασίζεται η λειτουργία του εκάστοτε συστήματος προκειμένου να εκτελεστούν συγκεκριμένες εφαρμογές. Αν αντιμετωπίσουμε τέτοιες εφαρμογές ως ένα άθροισμα αλληλεξαρτώμενων δραστηριοτήτων (interdependent tasks), θα παρατηρήσουμε πως προκειμένου να εξασφαλίσουμε την αποτελεσματικότερη και «ομαλότερη» εκτέλεσή τους παράλληλα με την βέλτιστη αξιοποίηση των πόρων μας, εφαρμόζονται ορισμένες αρχές χρονοδρομολόγης που κατευθύνουν την κάθε αρμοδιότητα της εφαρμογής , με σκοπό την βέλτιστη αυτή απόδοση. Βέβαια, για κάποιες φυσικές εφαρμογές που τίθενται προς έλεγχο, είναι πολύ πιθανό να απαιτούνται προθεσμίες χρονισμού (timing deadlines) είτε για ολόκληρη την εφαρμογή (καθολικά) είτε για κάθε interdepend task ξεχωριστά. Η πρόκληση λοιπόν έγκειται στη σωστή εφαρμογή των scheduling principles ώστε να εξασφαλίζουν ότι πληρούνται όλες οι προθεσμίες χρονισμού της κάθε διεργασίας προς ανάλυση (schedulability analysis). Σκοπός λοιπόν αυτής της εργασίας αποτελεί αρχικά η μοντελοποίηση τέτοιων περιπτώσεων χρονοδρομολόγησης σε κατάλληλο simulation tool. Η μοντελοποίηση των διαφόρων scheduling scenarios πραγματοποιήθηκε στο UPPAAL (4.15) [12,24] , το οποίο αποτελεί ένα εργαλείο για modelling, validation και verification [4,21] σε συστήματα πραγματικού χρόνου με την χρήση χρονισμένων αυτομάτων [κεφ3]. Συγκεκριμένα στα μοντέλα συμπεριλήφθηκαν ποικίλα scheduling policies [κεφ1], πληθώρα χαρακτηριστικών και εξαρτήσεων για το κάθε interdependent task, δυνατότητα ανάθεσης συγκεκριμένων resource σε συγκεκριμένα tasks (bus, processor) αλλά και δυνατότητα διακοπτόμενης χρονοδρομολόγησης. Στη συνέχεια επήλθε πειραματισμός και μελέτη πάνω στα γενικά μοντέλα μεταβάλλοντας τις αρχικές τιμές των παραμέτρων, ώστε να προκύψουν ξεχωριστά και διαφορετικά σενάρια χρονοδρομολόγησης των οποίων η εγκυρότητα ελέγχθηκε μέσω του verifier του UPPAAL [12,24]. Τα συμπεράσματα αλλά και μια πιθανή μελλοντική εργασία θα παρατεθούν στο τέλος.