Από DistrSys

Πίνακας περιεχομένων 1 Περιγραφή Μοντέλου Ασύγχρονων Συστημάτων 1.1 1. Αυτόματα Εισόδου/Εξόδου(Ι/Ο) 1.1.1 Υπογραφή Ι/Ο αυτόματου 1.1.2 Παραδείγματα Ι/Ο αυτομάτων 1.2 2. Λειτουργιές πάνω σε αυτόματα 1.2.1 Σύνθεση 1.2.2 Απόκρυψη 1.3 3. Δικαιοσύνη 1.4 4. Είσοδοι και έξοδοι για προβλήματα 1.5 5. Ιδιότητες και μέθοδοι αποδείξεων 1.5.1 Αμετάβλητοι ισχυρισμοί 1.5.2 Ιδιότητες ίχνους 1.6 6. Μετρικές πολυπλοκότητας 2 Περιγραφή Μοντέλου Ασύγχρονου Δικτύου 2.1 1. Συστήματα Αποστολής/Λήψης(Send/Receive) 2.1.1 Διαδικασίες 2.1.2 Κανάλια Αποστολής/Λήψης 2.1.3 Αξιόπιστο κανάλι FIFO. 2.1.4 Αξιόπιστο κανάλι με αλλαγή σειράς. 2.1.5 Κανάλια με αποτυχίες 2.1.6 Ασύγχρονα συστήματα αποστολής λήψης(send/receive) 2.1.7 Ιδιότητες των συστημάτων αποστολής/λήψης με αξιόπιστα κανάλια FIFO 2.1.8 Μετρικές πολυπλοκότητας

Περιγραφή Μοντέλου Ασύγχρονων Συστημάτων

Το κεφάλαιο αυτό κάνει μια εισαγωγή ενός τυπικού μοντέλου για τον ασύγχρονο υπολογισμό: Το μοντέλο του αυτόματου εισόδου/εξόδου(Ι/Ο)

Πρόκειται για ένα πολύ γενικό μοντέλο κατάλληλο για την περιγραφή σχεδόν οποιουδήποτε τύπου ασύγχρονου ταυτόχρονου συστήματος συμπεριλαμβανομένων αυτών που θα μελετήσουμε παρακάτω: 1. Ασύγχρονα συστήματα κοινής μνήμης 2. Ασύγχρονα συστήματα δικτύου

Το αυτόματο εισόδου/εξόδου(Ι/Ο)έχει μικρή δομή και γι' αυτό χρησιμοποιείται για την μοντελοποίηση πολλών διαφορετικών τύπων κατανεμημένων συστημάτων. Προσθέτοντας επιπλέον δομές στο βασικό μοντέλο μπορούμε να περιγράψουμε συγκεκριμένους τύπους ασύγχρονων συστημάτων. Το μοντέλο προσφέρει έναν συγκεκριμένο τρόπο για να περιγράψουμε και να συζητήσουμε για τα στοιχεία του συστήματος (π.χ διαδικασίες ή κανάλια επικοινωνίας) που επικοινωνούν μεταξύ τους και που λειτουργούν σε αυθαίρετες σχετικές ταχύτητες.

Συνεχίζοντας θα ορίσουμε το αυτόματο και την εκτέλεση του και θα αναφερθούμε στις λειτουργίες Σύνθεσης που αναφέρεται στο πως συνδυάζουμε αυτόματα για να φτιάξουμε ένα μεγαλύτερο αυτόματο καθώς και στην έννοια της Δικαιοσύνης(fairness) που ουσιαστικά εγγυάται ότι δεν θα απαγορεύεται επ' άπειρον στα στοιχεία του αυτόματου να εκτελούν κάποια βήματα κατά τους γύρους εκτέλεσης.

1. Αυτόματα Εισόδου/Εξόδου(Ι/Ο)

Ένα Ι/Ο αυτόματο μοντελοποιεί ένα στοιχείο ενός κατανεμημένου συστήματος που αλληλεπιδρά με άλλα στοιχεία του συστήματος. Είναι ένας απλός τύπος μηχανής καταστάσεων στην οποία η μεταβάσεις συνδέονται με ονομαζόμενες ενέργειες. Οι δράσεις ταξινομούνται ως είσοδος, έξοδος ή εσωτερική. Οι είσοδοι και έξοδοι χρησιμοποιούνται για την επικοινωνία με του αυτόματου με το περιβάλλον, ενώ η εσωτερικές ενέργειες είναι ορατές μόνο στο ίδιο το αυτόματο. Οι ενέργειες εισόδου δεν είναι υπό τον έλεγχο του αυτόματου - απλώς φθάνουν από το εξωτερικό - ενώ το αυτόματο το ίδιο καθορίζει ποια ενεργεία εξόδου και εσωτερική θα πρέπει να εκτελείται. Ένα παράδειγμα ενός τυπικού I / O αυτόματου είναι μια διαδικασία σε ένα ασύγχρονο κατανεμημένο σύστημα. Η διασύνδεση μιας τυπικής διαδικασία αυτομάτου με το περιβάλλον του απεικονίζεται στο σχήμα 8.1.

Σχήμα 8.1: Μια διαδικασία Ι/Ο αυτόματου

Το αυτόματο P_i σχεδιάζεται ως ένας κύκλο, με εισερχόμενα βέλη που επισημαίνονται με τις ενέργειες εισόδου και τα εξερχόμενα βέλη που επισημαίνονται με τις ενέργειες εξόδου. Εσωτερικές ενέργειες δεν εμφανίζονται. Η απεικονιζόμενο αυτόματο λαμβάνει εισόδους της μορφής init(v)_i από τον έξω κόσμο, τα οποία υποτίθεται ότι αναπαριστούν την λήψη μιας τιμής εισόδου v. Αποστέλλει εξόδους της μορφής decide(v)_i, που αναπαριστούν μια απόφαση v. Για να καταλήξει σε απόφαση, η διεργασία P_i μπορεί να θέλει να επικοινωνήσει με άλλες διαδικασίες χρησιμοποιώντας ένα σύστημα μηνυμάτων. Η Διεπαφή του με το σύστημα μηνυμάτων αποτελείται ενέργειες εξόδου της μορφής send(m)_i,j, το οποίο αντιπροσωπεύει τη διαδικασία P_i που στέλνει ένα μήνυμα με το περιεχόμενο m στην διεργασία P_j , και ενέργειες εισόδου της μορφής receive(m)_j,i, που αντιπροσωπεύει τη διαδικασία P_i να λαμβάνει ένα μήνυμα με το περιεχόμενο m από τη διαδικασία P_j. Όταν το αυτόματο εκτελεί οποιαδήποτε από τις αναφερόμενες ενέργειες (ή οποιαδήποτε εσωτερική ενέργεια), μπορεί επίσης να αλλάξει κατάσταση.

Ένα άλλο παράδειγμα ενός τυπικού I / O αυτόματου είναι ένα FIFO κανάλι μηνυμάτων. Ένα τυπικό αυτόματο καναλιού, που ονομάζεται C_i,j, παρουσιάζεται στο σχήμα 8.2

Σχήμα 8.2: Ένα Ι/Ο αυτόματο καναλιού

Οι ενέργειες εισόδου είναι της μορφής send(m)_i,j, και οι ενέργειες εξόδου είναι της μορφής receive(m)_i,j. Με τον συνήθη τρόπο περιγραφής ενός κατανεμημένου συστήματος χρησιμοποιώντας Ι/Ο αυτόματα , μια συλλογή από αυτόματα διαδικασίας και αυτόματα καναλιού συντίθενται ,ταιριάζοντας τις εξόδους του ενός με τις εισόδου με ίδιο όνομα άλλων αυτομάτων. Έτσι μια send(m)_i,j έξοδος που εκτελείται από μια διαδικασία P_i αναγνωρίζεται με μια send_i,jείσοδο απο το κανάλι C_i,j. Το σημαντικό σημείο είναι οτι οι διαφορές ενέργειες εκτελούνται μια κάθε φορά, με απρόβλεπτη σειρά -σε αντίθεση με τα σύγχρονα συστήματα που όλες οι διεργασίες στέλνουν και λαμβάνουν μηνύματα ταυτόχρονα σε κάθε γύρο υπολογισμού.

Υπογραφή Ι/Ο αυτόματου

Θεωρούμε ένα καθολικό σύνολο ενεργειών.

Μια υπογραφή S είναι μια τριάδα που αποτελείται από τρία ξένα σύνολα ενεργειών: τις ενέργειες εισόδου, in(S), τις ενέργειες εξόδου, out(S), και τις εσωτερικές ενέργειες, int(S) Ορίζουμε τις εξωτερικές ενέργειες ως ext(S)= in(S)∪out(S), τις τοπικά ελεγχόμενες ενέργειες local(S)= out(S)∪int(S)και ως acts(S) όλες της ενέργειες του S. Η εξωτερική υπογραφή, extsig(S) ορίζεται ως η υπογραφή (in(S),out(s),∅).Συχνά θα αναφερόμαστε σε αυτή ως εξωτερική διεπαφή

'Ενα Ι/Ο αυτόματο A, που ονομάζεται επίσης και αυτόματο αποτελείται από 5 στοιχεία:'

• sig(A),μια υπογραφή

• states(A),ενα ( όχι απαραίτητα πεπερασμένο) σύνολο καταστάσεων

• starts(A),ενα μη κενό υποσύνολο του states(A) γνωστό ως αρχικές καταστάσεις

• trans(A), μια σχέση μετάβασης καταστάσεων όπου trans(A)⊆states(A)x acts(sig(A))x states(A), πρέπει να έχει την ιδιότητα ότι για κάθε κατάσταση s και κάθε ενεργεία εισόδου π υπάρχει μια μετάβαση (s,π,s')∈trans(A)

• tasks(A), ένας καταμερισμός της εργασίας, ο οποίος είναι μια σχέση ισοδυναμίας πάνω στο σύνολο local(sig(A)) που έχει το πολύ αριθμήσιμα πολλές κλάσεις ισοδυναμίας

Χρησιμοποιούμε τον όρο acts(A) ως συναίρεση για το acts(sig(A)) και παρομοίως in(A) κτλ. Λέμε ότι το Α είναι κλειστό αν δεν έχει καθόλου εισόδους , δηλ αν in(A)=∅.

Το σύνολο των καταστάσεων δεν χρειάζεται να είναι πεπερασμένο. Αυτή η γενίκευση είναι σημαντική , αφού μας επιτρέπει την μοντελοποίηση συστημάτων που έχουν απεριόριστες δομές δεδομένων όπως οι μετρητές και οι απεριορίστου μεγέθους ουρές. Επιτρέπουμε όπως και στην σύγχρονη περίπτωση, πολλαπλές αρχικές καταστάσεις ώστε να ενσωματώνουμε κάποια πληροφορία εισόδου σε αυτές.

Καλούμε ένα στοιχείο (s,π,s') του trans(A) μια μετάβαση ή βήμα του Α. Η μετάβαση (s,π,s') καλείται μετάβαση εισόδου , μετάβαση εξόδου κτλ ανάλογα αν η ενέργεια π είναι ενέργεια εισόδου , ενέργεια εξόδου κτλ. Διαφορετικά από το σύγχρονο μοντέλο οι μεταβάσεις δεν σχετίζονται απαραίτητα με την λήψη κάποιου μηνύματος αλλά μπορούν να σχετίζονται με αυθαίρετες ενέργειες. Αν για μια συγκεκριμένη κατάσταση s και μια συγκεκριμένη ενέργεια π, το A έχει κάποια μετάβαση της μορφής (s,π,s') τότε λέμε ότι η π ενεργοποιείται στην s. Αφού κάθε ενέργεια εισόδου απαιτείται να ενεργοποιείται σε κάθε κατάσταση, τα αυτόματα ονομάζονται ενεργοποιημένα λογω εισόδου(input-enabled) . Η σημασια της ενεργοποιησης είναι οτι το αυτόματο δεν μπορεί αυθαίρετα να εμποδίζει τις ενέργειες εισόδου να συμβούν. Δηλαδή, για παράδειγμα μια διαδικασία πρέπει να είναι προετοιμασμένη να αντιμετωπίσει οποιαδήποτε τιμή μηνύματος όταν φτάνει ένα μήνυμα. Λέμε ότι μια κατάσταση s είναι ήρεμη αν οι μόνες ενέργειες που ενεργοποιούνται σε αυτή είναι ενέργειες εισόδου. Ίσως φαίνεται ότι η ιδιότητα ενεργοποίησης λόγω εισόδου είναι πολύ ισχυρός περιορισμός για να εφαρμοστεί σε ένα γενικό μοντέλο, γιατί πολλά στοιχειά του συστήματος είναι σχεδιασμένα να δέχονται συγκεκριμένες εισόδους σε συγκεκριμένες στιγμές. Όμως υπάρχουν άλλοι τρόποι να μοντελοποιηθούν αυτοί οι περιορισμοί στο περιβάλλον, χωρίς την απαίτηση το περιβάλλον να μην εκτελέσει την είσοδο. Αντ’ αυτού αν θέλουμε μπορούμε να εισάγουμε ένα μήνυμα λάθους όταν αντιμετωπίζουμε μια μη επιθυμητή είσοδο.

Η ιδιότητα ενεργοποίησης λογω εισόδου έχει δυο σημαντικά πλεονεκτήματα:

1.Επειδή μια σημαντική πηγή σφαλμάτων στην ανάπτυξη στοιχείων του συστήματος είναι η αδυναμία να ορίσουμε την αντίδραση του στοιχείου σε μια απροσδόκητη είσοδο, η χρήση ενός μοντέλου που λαμβάνει υπόψη τις αυθαίρετες εισόδους βοηθάει στην εξάλειψη τέτοιων σφαλμάτων.

2.Η χρήση της ενεργοποίησης λογω εισόδου κάνει την θεωρία του μοντέλου να λειτουργεί σωστά, συγκεκριμένα αυτή η ιδιότητα μας δίνει την δυνατότητα να χρησιμοποιούμε άπλες έννοιες εξωτερικών συμπεριφορών για ένα αυτόματο βασισμένες σε ακολουθίες εξωτερικών ενεργειών.

Το 5ο στοιχείο στον ορισμό του αυτόματου, ο καταμερισμός των εργασιών tasks(A), θα πρέπει να θεωρηθεί ως μια αφηρημένη περιγραφή των "εργασιών" ή "νημάτων έλεγχου" μέσα στο αυτόματο. Αυτό το τμήμα χρησιμοποιείται για να ορίσει τις συνθήκες δικαιοσύνης κατά την εκτέλεση του αυτομάτου- τις συνθήκες που ορίζουν ότι το αυτόματο πρέπει να συνεχίσει κατά την εκτέλεση του να δίνει δίκαιους γύρους σε κάθε εργασία του. Αυτό είναι χρήσιμο όταν μοντελοποιούμε ένα στοιχειό συστήματος που κάνει παραπάνω από μια δουλειές. Είναι επίσης χρήσιμο όταν αρκετά αυτόματα συντίθενται για να δημιουργήσουν ένα μεγαλύτερο αυτόματο που αναπαριστά ολόκληρο το σύστημα. Άλλη μια χρήση του είναι όταν μοντελοποιούμε ασύγχρονους αλγορίθμους κοινής μνήμης. Θα αναφερόμαστε στις κλάσεις του τμήματος "εργασιών" ως εργασίες tasks.

Όταν λέμε ότι μια εργασία C ενεργοποιείται σε μια κατάσταση s , αυτός είναι ένας σύντομος τρόπος να πούμε ότι κάποια ενέργεια στην C ενεργοποιείται στην s.

Παραδείγματα Ι/Ο αυτομάτων

Στις περισσότερες περίγραφες αυτομάτων Ι/Ο, η σχέση μετάβασης περιγράφεται με έναν τρόπο που αποκαλείται precondition-effect. Με αυτόν τον τρόπο συγκεντρώνονται όλες οι μεταβάσεις που περιλαμβάνουν κάθε τύπο ενέργειας σε ξεχωριστά τμήματα κώδικα. Ο κώδικας αυτός περιγράφει τις συνθήκες υπό τις οποίες μια ενέργεια επιτρέπεται να λάβει χώρα. Έπειτα περιγράφει τις αλλαγές που συμβαίνουν ως αποτέλεσμα της ενέργειας με την μορφή ενός απλού προγράμματος που εφαρμόζεται στην s για να αποδώσει την s'. Όλο το τμήμα κώδικα εκτελείται αδιαίρετα, ως μια μοναδική μετάβαση. Με αυτή την μορφή προκύπτει ένας πιο συνοπτικός κώδικας γιατί οι μεταβάσεις που περιλαμβάνουν κάθε ενέργειας περιλαμβάνουν μόνο μια μικρή αναλογία τις κατάστασης. Τα προγράμματα που είναι γραμμένα έτσι χρησιμοποιούν πολύ απλές δομές έλεγχου. Αυτό κάνει τη μετάφραση από πρόγραμμα σε Ι/Ο αυτόματο διαφανή, που σημαίνει ότι είναι ευκολότερο να επιχειρηματολογήσουμε με τυπικό τρόπο για τα αυτόματα.

Παράδειγμα 1 -- Ι/Ο αυτόματο καναλιού

Ως ένα παράδειγμα αυτόματου Ι/Ο, θεωρείστε ένα αυτόματο καναλιού επικοινωνίας C_i,j. Έστω Μ ένα καθορισμένο αλφάβητο μηνύματος. Πρώτα δίνουμε την υπογραφή ,sig(C_i,j). Εδώ και εκεί χρησιμοποιούμε την σύμβαση ότι αν δεν αναφέρουμε ένα στοιχείο υπογραφής(συνήθως, τις εσωτερικές ενέργειες),τότε το σύνολο των ενεργειών είναι κενό.

Υπογραφη:

Εισοδος: 
  send(m)i,j, m∈M                   

Εξοδος: 
  receive(m)i,j, m∈M


Οι καταστάσεις, states(Ci,j), και οι αρχικές καταστάσεις, start(Ci,j), 
περιγράφονται πολύ βολικά  με την μορφή μιας λίστας μεταβλητών κατάστασης και τις αρχικές τους τιμές. 
Οπως στις σύγχρονες ρυθμισεις.

Καταστάσεις:

queue, Μια FIFO ουρα των στοιχείν του Μ, αρχικά κενή

Οι μεταβάσεις του Ci,j περιγράφονται από τον ακόλουθο κώδικα:

Μεταβάσεις:

 send(m)i,j
    Αποτέλεσμα: 
         Προσθεσε το m στην queue

 receive(m)i,j
    Προυπόθεση: 
         το m ειναι πρώτο στην queue
    Αποτέλεσμα: 
         αφαίρεσε το πρώτο στοιχειο της queue

Εργασιες:

{receive(m)i,j : m∈M}

Ο κώδικας θα πρεπει να ειναι αυτο-εξηγούμενος: η ενέργεια send επιτρεπεται να συμβει οποτεδήποτε και έχει σαν αποτέλεσμα την Ο κώδικας θα πρέπει να είναι αυτο-εξηγούμενος: η ενέργεια send επιτρέπεται να συμβεί οποτεδήποτε και έχει σαν αποτέλεσμα την προσθήκη του μηνύματος στο τέλος της queue, ενώ η ενέργεια receive μπορεί να συμβεί όταν το μήνυμα είναι στο επάνω μέρος της queue και έχει το αποτέλεσμα ότι το αφαιρει.

Ο καταμερισμός της εργασίας, tasks(C_i,j) ομαδοποιεί όλες τις ενέργειες receive σε ένα μοναδικό τμήμα. Η λειτουργιά της λήψης μηνυμάτων θεωρείται σαν μοναδική εργασία

Παράδειγμα 2 -- Ι/Ο αυτόματο διαδικασίας

Ως δεύτερο παράδειγμα ενός Ι/Ο αυτόματου θεωρείστε ένα αυτόματο διαδικασίας P_i. Αυτό το αυτόματο έχει την εξωτερική διεπαφη που περιγράφεται παρακάτω. Εδώ, το V είναι ένα καθορισμένο σύνολο τιμών, null είναι μια ειδική τιμή που δεν ανήκει στο V, και f είναι μια καθορισμένη συνάρτηση f:Vⁿ ->V.

Υπογραφή :

Είσοδος:
 init(v)i, v∈V
 receive(v)j,i, v∈V, 1 ≤ j ≤ n, j≠i

Έξοδος:
 decide(v)i, v∈V
 send(v)i,j, v∈V, 1 ≤ j ≤ n, j≠i


Οι καταστάσεις και οι αρχικές καταστάσεις είναι ως ακολούθως:


Καταστάσεις:
 val, ένα διάνυσμα με δεικτες {1,...,n} των στοιχείων του V ∪{null}, όλα αρχικά null


Ακολουθούν οι μεταβάσεις:


Μεταβάσεις:

init(v)i, v∈V
   Αποτέλεσμα: 
       val(i):=v


send(v)i,j, v∈V
   Προϋπόθεση: 
       val(i)=v
   Αποτέλεσμα: 
       κανένα


receive(v)j,i, v∈V
   Αποτελεσμα: 
       val(j):=v


decide(v)i, v∈V
   Προϋπόθεση:
       για όλα τα j, 1 ≤ j ≤ n:
          val(j)≠null
       v = f(val(1),…,val(n))
   Αποτέλεσμα:
       κανένα

Εργασίες:

Για κάθε j≠i:
{send(v)i,j: v∈V}

{decide(v)i: v∈V}

Έτσι η ενέργεια init κάνει το P_i να γεμίζει την καθορισμένη τιμή στην θέση της στο διάνυσμα val, ενώ η ενέργεια receive προκαλεί το γέμισμα σε άλλη θέση. Αυτές οι τιμές μπορούν να ανανεωθούν άπειρο αριθμό φόρων μέσω πολλαπλών ενεργειών init ή receive. To P_i έχει δικαίωμα να στείλει την τιμή του όσες φορές θέλει σε οπουδήποτε κανάλι. Το P_i μπορεί επίσης να αποφασίσει όσες φορές θέλει, βασιζόμενο σε νέες εφαρμογές της f στο διάνυσμα του.

Ο καταμερισμός της εργασίας, tasks(P_i), περιέχει n εργασίες: μια για όλες τις ενέργειες send_i,j για κάθε j≠i και μια για όλες τις ενέργειες decide. Έτσι η αποστολή σε κάθε κανάλι θεωρείται μια μοναδική ενιαία εργασία, όπως είναι η αναφορά των αποφάσεων.

Τώρα θα περιγράψουμε πως εκτελείται ένα Ι/Ο αυτόματο Α. Ένα τμήμα εκτέλεσης του Α είναι μια πεπερασμένη ακολουθία s₀,π₁,s₁,π₂,…,π_r,s_r, ή μια μη άπειρη ακολουθία s₀,π₁,s₁,π₂,…,π_r,s_r,…, καταστάσεων και ενεργειών του Α εναλλάξ τέτοια ώστε (s_k,π_k+1,s_k+1) είναι μια μετάβαση του Α για κάθε k≥0. Παρατηρείστε ότι αν η ακολουθία είναι πεπερασμένη πρέπει να τελειώνει με μια κατάσταση. Ένα τμήμα εκτέλεσης που ξεκινά με μια αρχική κατάσταση λέγεται εκτέλεση. Συμβολίζουμε το σύνολο των εκτελέσεων του Α με execs(A). Μια κατάσταση λέγεται προσεγγίσιμη αν είναι η τελική κατάσταση μιας πεπερασμένης εκτέλεσης του Α.

Αν α είναι ένα πεπερασμένο τμήμα εκτέλεσης του Α και α’ είναι οποιοδήποτε τμήμα εκτέλεσης του Α που ξεκινά με την τελευταία κατάσταση του α , τότε αναπαριστούμε με αα’ την ακολουθία που προκύπτει από την ένωση των α και α’, εξαλείφοντας το αντίγραφο της τελευταίας κατάστασης του α. Δηλαδή κρατάμε μόνο μια φορά αυτή την κατάσταση. Προφανώς η ακολουθία αα’ είναι επίσης ένα τμήμα εκτέλεσης του Α.

Μερικές φορές μας ενδιαφέρει μόνο η εξωτερική συμπεριφορά ενός αυτόματου. Έτσι το ίχνος μια εκτέλεσης α του Α που δηλώνεται ως trace(α) είναι η υπακολουθία της α που αποτελείται μόνο από τις εξωτερικές ενέργειες . Λέμε ότι η β είναι ένα ίχνος του Α αν η β είναι το ίχνος μιας εκτέλεσης του Α. Αναπαριστούμε το σύνολο των ιχνών του Α ως traces(A).

Παράδειγμα 3 -- Εκτελέσεις

Οι παρακάτω είναι 3 εκτελέσεις του αυτόματου C_i,j που περιγράφτηκε στο Παράδειγμα 1( υποθέτοντας ότι το αλφάβητο μηνυμάτων Μ ισούται με το σύνολο {1,2}). Εδώ υποδεικνύουμε τις καταστάσεις βάζοντας τις ακολουθίες που είναι στην queue σε αγκύλες , το λ δηλώνει την κενή ακολουθία

[λ],send(1)_i,j, [1],receive(1)_i,j,[λ]send(2)_i,j,[2],receive(2)_i,j,[λ]

[λ],send(1)_i,j, [1],receive(1)_i,j,[λ]send(2)_i,j,[2]

[λ],send(1)_i,j, [1], send(1)_i,j,[11], send(1)_i,j,[111],…

Οι 2 τελευταίες επιτρέπονται αν και περιέχουν μηνύματα που στέλνονται αλλά δεν λαμβάνονται ποτέ. Αυτό γίνεται γιατί μέχρι τώρα δεν έχουμε θέσει κανένα περιορισμό στις εκτελέσεις λέγοντας ότι οι ενέργειες που ενεργοποιούνται πρέπει να συμβούν. Παρακάτω θα εισάγουμε τις απαιτήσεις της δικαιοσύνης που θα μας επιτρέπουν να εκφράζουμε τέτοιους περιορισμούς

2. Λειτουργιές πάνω σε αυτόματα

Εδώ θα ορίσουμε την λειτουργιά της σύνθεσης και την λειτουργιά της απόκρυψης των ενεργειών εξόδου για τα Ι/Ο αυτόματα.

Σύνθεση

Η λειτουργιά της σύνθεσης επιτρέπει σε ένα αυτόματο που αναπαριστά ένα σύνθετο σύστημα να κατασκευαστεί συνθέτοντας αυτόματα που αναπαριστούν ατομικά στοιχειά συστήματος. Η σύνθεση αναγνωρίζει ενέργειες με την ιδία ονομασία σε διαφορετικά στοιχειώδη αυτόματα. Όταν ένα στοιχείο εκτελεί ένα βήμα που περιέχει την π, το ίδιο κάνουν και όλα τα στοιχειώδη αυτόματα που έχουν την π στις υπόγραφες τους.

Περιορισμοί σύνθεσης αυτομάτων

Ορίζουμε ότι μια μετρήσιμη συλλογή υπογραφών {S_i}_i∈I είναι συμβατή αν για ολα τα i,j∈I, i≠j ισχύουν τα ακόλουθα:

1. int(Si) ∩acts(Sj)=∅

Επεξήγηση: Αφού οι εσωτερικές ενέργειες ενός αυτόματου Α πρέπει να είναι απαρατήρητες από οποιοδήποτε αυτόματο Β δεν επιτρέπεται η σύνθεση των Α και Β αν οι εσωτερικές ενέργειες του Α δεν είναι ανεξάρτητες από τις ενέργειες του Β.(Αλλιώς η εκτέλεση μιας εσωτερικής ενέργειας του Α θα ωθούσε το Β να κάνει ένα βήμα).

2. out(Si) ∩ out(Sj)=∅

Επεξήγηση: Για να έχει η σύνθεση καλές ιδιότητες όπως θα δούμε παρακάτω θέτουμε την σύμβαση ότι το πολύ ένα στοιχειώδες αυτόματο ελέγχει την απόδοση κάθε δεδομένης ενέργειας, δηλαδή δεν επιτρέπεται η σύνθεση των Α και Β αν τα σύνολα των ενεργειών εξόδου τους δεν είναι ανεξάρτητα.

3. Καμία ενέργεια δεν περιέχεται σε άπειρα πολλά σύνολα acts(Si)

Επεξήγηση: Αποκλείεται η πιθανότητα σύνθεσης μιας μετρήσιμα άπειρης συλλογής αυτομάτων. Απαιτούμε κάθε ενέργεια να είναι ενέργεια μόνο πεπερασμένα πολλών στοιχειωδών αυτομάτων( αυτός ειδικά ο περιορισμός χρειάζεται διότι το θεώρημα που θα αναφέρουμε παρακάτω δεν θα ισχύει διαφορετικά)

Λέμε ότι μια συλλογή από αυτόματα είναι συμβατή αν οι υπογραφές τους είναι συμβατές.

ΕΡΩΤΗΣΗ: Γιατί να μην αποκλείσουμε απλώς τα απείρως πολλά αυτόματα (αφού εξάλλου τα υλικά συστήματα είναι πεπερασμένα);;;

ΑΠΑΝΤΗΣΗ: Ο λόγος για την άπειρη σύνθεση είναι ότι τα Ι/Ο αυτόματα χρησιμοποιούνται για να μοντελοποιήσουν λογικά σύστημα εκτός από υλικά συστήματα. Ένα λογικό σύστημα μπορεί να αποτελείται από μεγάλο αριθμό λογικών στοιχείων που θα πρέπει να εφαρμοστούν σε ένα υλικό σύστημα με λιγότερα στοιχειά. Για την ακρίβεια, κάποια λογικά συστήματα επιτρέπουν την δημιουργία στοιχείων κατά την διάρκεια μιας άπειρης εκτέλεσης (π.χ τα συστήματα βάσεων δεδομένων μπορεί να επιτρέπουν την δημιουργία νέων στιγμιότυπων μεταβάσεων ενώ το σύστημα εκτελείται). Ο τρόπος για να μοντελοποιήσουμε την δημιουργία στοιχείων χρησιμοποιώντας Ι/Ο αυτόματα είναι να φανταστούμε ότι όλα τα πιθανά στοιχειά που μπορούν να δημιουργηθούν είναι παρόντα από την αρχή αλλά έχουν κάποιες ειδικές ενέργειες εισόδου αφύπνισης (wakeup) που τα αφυπνίζουν την στιγμή που υποτίθεται ότι δημιουργούνται. Με αυτό το κόλπο ο χειριστής της συνηθισμένης σύνθεσης είναι επαρκής για την περιγραφή του τρόπου αλληλεπίδρασης των δυναμικά δημιουργούμενων στοιχείων με το υπόλοιπο σύστημα. Επομένως είναι απαραίτητο απείρως πολλά στοιχεία να συνδυάζονται.

Όταν συνθέτουμε μια συλλογή από αυτόματα , οι ενέργειες εξόδου των επιμέρους στοιχείων γίνονται ενέργειες εξόδου της σύνθεσης, οι εσωτερικές ενέργειες των στοιχείων γίνονται εσωτερικές ενέργειες της σύνθεσης , και οι ενέργειες που είναι είσοδοι σε κάποια στοιχεία αλλά δεν είναι ταυτόχρονα και έξοδοι κανενός στοιχείου γίνονται οι ενέργειες εισόδου της σύνθεσης.

Τυπικά, η σύνθεση S= Π_i∈I S_i μιας μετρήσιμης συμβατής συλλογής υπογραφών {S_i}_i∈I ορίζεται ως η υπογραφή με

• out(S) = ∪_i∈I out(S_i)

• int(S) = ∪_i∈I int(S_i)

• in(S) = ∪_i∈I in(S_i) - ∪_i∈I out(S_i)

Έτσι, η σύνθεση A= Π_i∈I A_i μιας μετρήσιμης συμβατής συλλογής Ι/Ο αυτομάτων {A_i}_i∈I είναι το αυτόματο όπως ορίζεται παρακάτω:

• sig(A)=Π_i∈I sig(A_i)

• states(A)=Π_i∈I states(A_i)

• start(A)=Π_i∈I start(A_i)

• trans(A) είναι το σύνολο των τριάδων (s,π,s') τέτοιων ώστε, για κάθε i∈I, αν π ∈ acts(Ai), τότε (si,π,si')∈ trans(A_i) αλλιώς s_i=s_i'

• tasks(A)=∪_i∈I tasks(A_i)

Έτσι, οι καταστάσεις και οι αρχικές καταστάσεις του αυτόματου που αποτελεί την σύνθεση είναι διανύσματα καταστάσεων και αρχικών καταστάσεων των στοιχειωδών αυτομάτων. Οι μεταβάσεις της σύνθεσης ανακτώνται επιτρέποντας σε όλα τα στοιχειώδη αυτόματα που έχουν μια συγκεκριμένη ενέργεια π στις υπογραφές τους να συμμετέχουν ταυτόχρονα στα βήματα που αφορούν την π, ενώ όλα τα υπόλοιπα αυτόματα δεν κάνουν τίποτα. Ο καταμερισμός της εργασίας των τοπικά ελεγχόμενων ενεργειών της σύνθεσης σχηματίζεται από την ένωση των καταμερισμών εργασίας των στοιχειωδών αυτομάτων , δηλαδή κάθε κλάση ισοδυναμίας κάθε στοιχειώδους αυτόματου γίνεται μια κλάση ισοδυναμίας της σύνθεσης. Αυτό σημαίνει ότι η δομή των εργασιών των στοιχειωδών αυτομάτων διατηρείται όταν τα αυτόματα συντίθενται. Παρατηρείστε ότι αφού τα αυτόματα Αi ενεργοποιούνται λογω εισόδου(input-enabled), το ίδιο και η σύνθεση. Συνεπώς η σύνθεση Π_i∈I A_i είναι πράγματι ένα Ι/Ο αυτόματο.

Όταν το Ι είναι ένα πεπερασμένο σύνολο μερικές φορές χρησιμοποιούμε το σύμβολο x για να δηλώσουμε την σύνθεση. Για παράδειγμα, αν Ι={1,...,n} μερικές φορές αναπαριστούμε το Π_i∈I A_i ως Α₁ x...x A_n.

Παρατηρήστε ότι μια ενέργεια π που είναι έξοδος ενός στοιχείου και είσοδος ενός άλλου κατατάσσεται ως ενέργεια εξόδου στην σύνθεση και όχι ως εσωτερική ενέργεια. Αυτό γίνεται επειδή θέλουμε να επιτρέπουμε την πιθανότητα επιπλέον επικοινωνίας χρησιμοποιώντας την π. Για παράδειγμα , υποθέστε ότι το αυτόματο Α έχει την π ως ενέργεια εξόδου ενώ τα αυτόματα Β και C την έχουν ως ενέργεια εισόδου. Έτσι η π είναι κατ' ουσία ενέργεια μετάδοσης από το Α στα Β και C στην σύνθεση ΑxBxC των τριών αυτομάτων. Θα θέλαμε να σκαφτόμαστε με πιο σπονδυλωτό τρόπο για την σύνθεση , πρώτα να κατασκευάζαμε την ΑxΒ και μετά να συνθέταμε το αποτέλεσμα με το C. Συμφωνά με τον ορισμό που έχουμε δώσει στην σύνθεση η μορφή Α x B x C είναι ισοδύναμη με την (Α x B)x C, το αποτέλεσμα της σύνθεσης πρώτα των Α και Β και μετά η σύνθεση του αποτελέσματος αυτού με το C. Όμως αν το π είχε καταταχτεί ως εσωτερική στην σύνθεση Α x Β τότε δεν θα είχαμε αυτή την δυνατότητα: η σύνθεση Α x Β δεν θα μπορούσε να συντεθεί με το C, αφού θα παραβιαζόταν ο πρώτος κανόνας συμβατικότητας. Υπάρχει η δυνατότητα να αποκρύψουμε ενέργειες που χρησιμοποιούνται για την επικοινωνία των στοιχείων, και έτσι τις εμποδίζουμε να χρησιμοποιηθούν για περαιτέρω επικοινωνία. Αυτό γίνεται με την λειτουργιά της απόκρυψης επιπρόσθετα με την λειτουργιά της σύνθεσης.

Παράδειγμα 4 -- Σύνθεση αυτομάτων

Σκεφτείτε ένα σταθερό σύνολο δεικτών Ι = {1, ... , n} και έστω Α η σύνθεση όλων των αυτομάτων διαδικασίας P_i, i∈I, από το Παράδειγμα 2 και όλων των αυτομάτων καναλιού C_i,j, i, j ∈I, από το Παράδειγμα 1. Για να τα συνθέσουμε πρέπει να υποθέσουμε ότι το αλφάβητο μηνυμάτων Μ για τα αυτόματα καναλιού περιέχει το σύνολο τιμών V για τα αυτόματα διαδικασίας.

Το Σχήμα 8.3 παρουσιάζει την αρχιτεκτονική για την ειδική περίπτωση όπου n=3.

Σχήμα 8.1: Σύνθεση των Pi και των Ci,j

Η προκύπτουσα σύνθεση είναι ένα ενιαίο αυτόματο που αντιπροσωπεύει ένα κατανεμημένο σύστημα. Η κατάσταση του συστήματος αποτελείται από μια κατάσταση για κάθε διαδικασία (καθεμία ένα διάνυσμα τιμών, ένα για κάθε διαδικασία), συν μια κατάσταση για κάθε κανάλι (καθένα μια ουρά μηνυμάτων προς μεταφορά). Κάθε μετάβαση του συστήματος περιλαμβάνει ένα από τα ακόλουθα:

1. Μια ενεργεία εισόδου init(v)_i, που τοποθετεί μια τιμή στην μεταβλητή val(i) του P_i, την val(i)_i²

2. Μια ενέργεια εξόδου send(v)_i,j μέσω της όποιας η τιμή val(i) του P_i τοποθετείται στο κανάλι C_i,j

3. Μια ενέργεια εξόδου (v)_i,j , μέσω της οποίας το πρώτο μήνυμα στο C_i,j αφαιρείται και ταυτόχρονα τοποθετείται στην μεταβλητή val(i)_j του P_j

4. Μια ενέργεια εξόδου decide(v)_i , μέσω της οποίας το P_i ανακοινώνει την τρέχουσα υπολογισμένη τιμή του.

Ένα δείγμα ίχνους αυτής της σύνθεσης για n=2 όπου το σύνολο τίμων V είναι το N και η f είναι πρόσθεση, είναι

init(2)₁,init(1)₂,send(2)_1,2,receive(2)_1,2,send(1)_2,1,receive(1)_2,1,init(4)₁,init(0)₂,decide(5)₁,decide(2)₂

Στην μοναδική κατάσταση συστήματος που είναι προσεγγίσιμη χρησιμοποιώντας αυτό το ίχνος, το P₁ έχει διάνυσμα val το (4,1) και το P₂ έχει διάνυσμα val το (2,0), και τα δυο κανάλια είναι κενά. Φυσικά υπάρχουν πολλά άλλα ίχνη που μπορούν να προκύψουν κατά την εκτέλεση αυτού του σύνθετου συστήματος.

Κλείνοντας αυτή την υποενότητα θα αναφερθούμε σε 3 βασικά αποτελέσματα που σχετίζουν τις εκτελέσεις και τα ίχνη μιας σύνθεσης με αυτά των επιμέρους αυτομάτων. Το πρώτο λέει ότι μια εκτέλεση ή ένα ίχνος μιας σύνθεσης έχει σκοπό την απόδοση των εκτελέσεων ή ιχνών των στοιχειωδών αυτομάτων. Δεδομένης μια εκτέλεσης , α=s₀,π₁,s₁,...,του Α, έστω α|Α_i η ακολουθία που προκύπτει από την διαγραφή κάθε ζεύγους π_r,s_r για το οποίο η π_r δεν είναι ενέργεια του A_i και την αντικατάσταση κάθε εναπομείναντος s_r με το (s_r)_i, δηλαδή το κομμάτι της κατάστασης s_r του αυτόματου Α_i. Επίσης δεδομένου ενός ίχνους β του Α(ή πιο γενικά, οποιασδήποτε ακολουθίας ενεργειών), έστω β|Α_i η υπακολουθια του β που αποτελείται από όλες τις ενέργειες του A_i μέσα στο β. Επίσης χρησιμοποιούμε την θεώρηση | για να αναπαραστήσουμε την επακολουθία μιας ακολουθίας ενεργειών β που αποτελείται από όλες τις ενέργειες σε ένα δεδομένο σύνολο στο β.

Θεώρημα 1. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτόματων και έστω Α=Π_i∈IA_i

1. Αν α ∈ execs(A), τότε α|Α_i ∈ execs(A_i) για κάθε i∈I.

2. Αν β ∈ traces(A), τότε β|Α_i ∈ traces(A_i) για κάθε i∈I

Απόδειξη. Η απόδειξη αφήνεται ως άσκηση.

Τα επόμενα δυο είναι αντίστροφα του Θεωρήματος 1. Το επόμενο θεώρημα λέει ότι υπό συγκεκριμένες συνθήκες, οι εκτελέσεις των στοιχειωδών αυτομάτων μπορούν να ενωθούν μαζί για να σχηματίσουν μια εκτέλεση της σύνθεσης.

Θεώρημα 2. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτομάτων και έστω Α=Π_i∈IA_i. Υποθέστε ότι α_i είναι μια εκτέλεση του A_i, για κάθε i∈I' και υποθέστε ότι β είναι μια ακολουθία ενεργειών μέσα στο σύνολο ext(A) τέτοια ώστε β|Α_i= trace(α_i) για κάθε i∈I. Τότε υπάρχει μια εκτέλεση α του τέτοια ώστε b=trace(α) και α_i=α|Α_i για κάθε i∈I.

Απόδειξη. Η απόδειξη αφήνεται ως άσκηση.

Το τελευταίο θεώρημα λέει ότι τα ίχνη των στοιχειωδών αυτομάτων μπορούν επίσης να ενωθούν μαζί για να σχηματίσουν ένα ίχνος της εκτέλεσης.

Θεώρημα 3. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτομάτων και έστω Α=Π_i∈IA_i. Υποθέστε ότι β είναι μια ακολουθία ενεργειών μέσα στο σύνολο ext(A). Αν β|Α_i ∈ traces(A_i) για κάθε i∈I', τότε β ∈ traces(A).

Απόδειξη. Η απόδειξη αφήνεται ως άσκηση.

Το Θεώρημα 3 συνεπάγεται ότι για να δείξουμε ότι μια ακολουθία είναι ένα ίχνος ενός συστήματος, αρκεί να δείξουμε ότι η προβολή του σε κάθε ατομικό στοιχειώδες σύστημα είναι ένα ίχνος αυτού του στοιχειώδους συστήματος.

Απόκρυψη

Τώρα θα ορίσουμε μια λειτουργιά η όποια υποκρύπτει τις ενέργειες εξόδου ενός Ι/Ο αυτόματου επανακατατασσοντας τες ως εσωτερικές ενέργειες. Αυτό τις εμποδίζει να χρησιμοποιηθούν για περεταίρω επικοινωνία και σημαίνει ότι δεν συμπεριλαμβάνονται πλέον σε ίχνη. Πρώτα ορίζουμε την λειτουργιά της απόκρυψης για τις υπογραφές: Αν S είναι μια υπογραφή και Φ ⊆ out(S), τότε hide_Φ(S) ορίζεται ως η νέα υπογραφή S' , όπου in(S' )=in(S), out(S' )=out(S)-Φ, και int(S' )=int(S)∪ Φ. Η λειτουργιά της απόκρυψης για τα Ι/Ο αυτόματα είναι εύκολο να οριστεί τώρα:

Αν Α είναι ένα αυτόματο και Φ ⊆ out(Α), τότε hide_Φ(Α) είναι το αυτόματο Α' που προκύπτει από το Α αντικαθιστώντας την sig(A) με την sig(A')=hide_Φ(sig(A)).

3. Δικαιοσύνη

Σε κατανεμημένα συστήματα μας ενδιαφέρουν εκείνες οι εκτελέσεις μιας σύνθεσης στις οποίες σε όλα τα στοιχεία δίνονται δίκαιοι γύροι για να εκτελέσουν βήματα. Θα ορίσουμε μια κατάλληλη έννοια της δικαιοσύνης για τα αυτόματα Ι/Ο.

Θυμηθείτε ότι κάθε Ι/Ο αυτόματο είναι εξοπλισμένο με ένα τμήμα των τοπικά ελεγχόμενων ενεργειών του, κάθε κλάση ισοδυναμίας σε αυτό το τμήμα αναπαριστά κάποιες εργασίες που πρέπει να εκτελέσει το αυτόματο. Η έννοια της δικαιοσύνης είναι ότι κάθε εργασία λαμβάνει άπειρα πολλές ευκαιρίες να εκτελέσει μια από τις ενέργειες της.

Τυπικά, ένα τμήμα εκτέλεσης α ενός Ι/Ο αυτόματου Α λέγεται ότι είναι δίκαιο αν ισχύουν οι ακόλουθες συνθήκες για κάθε κλάση C του tasks(A):

1. Αν το α είναι πεπερασμένο, τότε η C δεν ενεργοποιείται στην τελική κατάσταση του α.

2. Αν το α είναι άπειρο, τότε το α περιέχει απείρως πολλά συμβάντα από την C η απείρως πολλές καταστάσεις στις οποίες η C δεν ενεργοποιείται.

Εδώ και εκεί, χρησιμοποιούμε τον όρο γεγονός για να δηλώσουμε την εμφάνιση μιας ενέργειας σε μια ακολουθία, για παράδειγμα, μια εκτέλεση ή ένα ίχνος. Μπορούμε να αντιληφτούμε τον ορισμό της δικαιοσύνης λέγοντας ότι απείρως συχνά σε κάθε εργασία (κλάση ισοδυναμίας) C δίνεται ένας γύρος. Όποτε συμβαίνει αυτό είτε μια ενέργεια του C εκτελείται είτε καμία ενέργεια από την C δεν θα μπορέσει να εκτελεστεί αφού δεν ενεργοποιείται. Μπορούμε να σκεφτούμε μια πεπερασμένη δίκαιη εκτέλεση ως μια εκτέλεση στο τέλος της οποίας το αυτόματο δίνει επαναλαμβανόμενα γύρους σε όλες τις εργασίες με σειρά round robin, άλλα ποτέ δεν επιτυγχάνει την εκτέλεση κάποιας ενέργειας αφού καμία δεν ενεργοποιείται στην τελική κατάσταση.

Δηλώνουμε το σύνολο των δικαίων εκτελέσεων του Α ως fairexecs(A). Λέμε ότι το β είναι ένα δίκαιο ίχνος του Α αν το β είναι το ίχνος μιας δίκαιης εκτέλεσης του Α, και δηλώνουμε το σύνολο των δίκαιων ιχνών του Α ως fairtraces(A).

Παράδειγμα 5 -- Δικαιοσύνη

Στο Παράδειγμα 3 η πρώτη εκτέλεση που δίνεται είναι δίκαιη, επειδή καμία ενέργεια receive δεν ενεργοποιείται στην τελική κατάσταση. Η δεύτερη εκτέλεση δεν είναι δίκαιη, διότι είναι πεπερασμένη και μια ενέργεια receive ενεργοποιείται στην τελική κατάσταση. Η τρίτη επίσης δεν είναι δίκαιη διότι είναι άπειρη , δεν περιέχει κανένα συμβάν receive και έχει ενέργειες receive ενεργοποιούνται σε κάθε σημείο μετά το πρώτο βήμα.

''Παράδειγμα 6 -- Δικαιοσύνη'

Για να επεξηγήσουμε περαιτέρω τον ορισμό της δικαιοσύνης , θεωρείστε το ακόλουθο Ι/Ο αυτόματο ρολογιού , που αναπαριστά ένα διακριτό ρολόι.

Αυτόματο Ρολογιού:

Υπογραφή:

Είσοδος: 
  request

Εσωτερική:
  tick

Έξοδος:
  clock(t), t∈N


Καταστάσεις:

counter ∈N, αρχικά 0

flag, boolean μεταβλητη, αρχικα false


Μεταβάσεις:

tick
  Προϋπόθεση: 
    true''
  Αποτέλεσμα:
    counter := counter+1

clock(t)
  Προϋπόθεση:
    flag = true
    counter = t
  Αποτέλεσμα: 
    flag := false

request
  Αποτέλεσμα: 
    flag := true


Εργασίες:

{tick}

{clock(t): tEN}

Το αυτόματο ρολογιού απλώς κάνει tick για πάντα αυξάνοντας έναν μετρητή. Επιπλέον αν μια αίτηση φτάσει , το ρολόι απατάει (σε ένα ξεχωριστό βήμα) με την τρέχουσα τιμή του μετρητή. Ακολουθεί μια ακολουθία εναργειών σε μια δίκαιη εκτέλεση του ρολογιού:

tick, tick, tick,...

Η επομένη είναι μια ακολουθία ενεργειών μιας εκτέλεσης που δεν είναι δίκαιη:

tick, tick, tick

Για την ακρίβεια το Ρολόι δεν έχει καμία πεπερασμένη δίκαιη εκτέλεση , αφού η tick ενεργοποιείται πάντα. Αυτή που ακολουθεί είναι δίκαιη:

tick, tick, request, tick, tick, clock(4), tick, tick,…,

Αφού από την στιγμή που το ρολόι έχει απαντήσει σε μια μοναδική αίτηση, δεν ενεργοποιούνται περαιτέρω ενέργειες clock. Τέλος αυτή η εκτέλεση δεν είναι δίκαιη:

tick, tick, request, tick, tick, tick,…,

επειδή μετά την αίτηση η εργασία clock παραμένει ενεργοποιημένη αλλά καμία ενέργεια clock δεν συμβαίνει ποτέ

Μπορούμε να αποδείξουμε τα ανάλογα των θεωρημάτων 1-3

Θεώρημα 4. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτομάτων και έστω Α=Π_i∈IA_i

1. Αν α ∈ fairexecs(A), τότε α|Α_i ∈ fairexecs(A_i) για κάθε i∈I.

2. Αν β ∈ fairtraces(A), τότε β|Α_i ∈ fairtraces(A_i) για κάθε i∈I

Θεώρημα 5. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτομάτων και έστω Α=Π_i∈IA_i. Υποθέστε ότι αi είναι μια δίκαιη εκτέλεση του A_i, για κάθε i∈I και υποθέστε ότι β είναι μια ακολουθία ενεργειών μέσα στο σύνολο ext(A) τέτοια ώστε β|Α_i= trace(α_i) για κάθε i∈I. Τότε υπάρχει μια δίκαιη εκτέλεση α του Α τέτοια ώστε b=trace(α) και α_i=α|Α_i για κάθε i∈I.

Θεώρημα 6. Έστω {Α_i}_i∈I μια συμβατή συλλογή αυτομάτων και έστω Α=Π_i∈IA_i. Υποθέστε ότι β είναι μια ακολουθία ενεργειών μέσα στο σύνολο ext(A). Αν β|Α_i ∈ fairtraces(A_i) για κάθε i∈I, τότε β ∈ fairtraces(A).

Αποδείξεις Οι αποδείξεις αφήνονται για εξάσκηση.

Παράδειγμα 7-- Δικαιοσύνη

Θεωρούμε την δίκαιη εκτέλεση του συστήματος των 3 διαδικασιών και 3 καναλιών του παραδείγματος 4. Σε κάθε δίκαιη εκτέλεση , κάθε μήνυμα που αποστέλλεται κάποια στιγμή λαμβάνεται . Επίσης , σε κάθε δίκαιη εκτέλεση που περιέχει τουλάχιστον ένα συμβάν initi_i για κάθε i, κάθε διαδικασία στέλνει απείρως πολλά μηνύματα σε κάθε άλλη διαδικασία και κάθε διαδικασία εκτελεί απείρως πολλά βήματα decide. Από την άλλη μεριά σε κάθε δίκαιη εκτέλεση που δεν περιέχει τουλάχιστον ένα συμβάν init για κάθε διαδικασία , καμία διαδικασία δεν εκτελεί ποτέ ένα βήμα decide. Σημειώστε ότι η δικαιοσύνη δεν έχει απαιτήσεις για να συμβεί η init- το πλήθος των συμβάντων init_i που εμπλέκουν κάθε p_i μπορεί να είναι πεπερασμένο (πιθανώς 0) ή άπειρο.

Το Θεώρημα που ακολουθεί λέει ότι κάθε πεπερασμένη εκτέλεση (ή ίχνος) μπορεί να επεκταθεί σε μια δίκαιη εκτέλεση (ή ίχνος)

Θεώρημα 7. Έστω Α το οποιοδήποτε Ι/Ο αυτόματο.

1. Αν α είναι μια πεπερασμένη εκτέλεση του Α, τότε υπάρχει μια δίκαιη εκτέλεση του Α που αρχίζει με την α.

2. Αν β είναι ένα πεπερασμένο ίχνος του Α, τότε υπάρχει ένα δίκαιο ίχνος του Α που ξεκινά με το β

3. Αν α είναι μια πεπερασμένη εκτέλεση του Α και β είναι μια (πεπερασμένη ή άπειρη) ακολουθία εναργειών εισόδου του Α, τότε υπάρχει μια δίκαιη εκτέλεση α α’ του Α τέτοια ώστε η ακολουθία των εναργειών εισόδου στην α’ είναι ακριβώς β.

4. Αν β είναι ένα πεπερασμένο ίχνος του Α και β’ είναι οποιαδήποτε (πεπερασμένη ή άπειρη) ακολουθία εναργειών εισόδου του Α ,τότε υπάρχει μια δίκαιη εκτέλεση α α’ του Α τέτοια ώστε trace(a)=β και ,η ακολουθία των ενεργειών εισόδου στην α’ να είναι ακριβώς β’.

Η απόδειξη αφήνεται για εξάσκηση.

4. Είσοδοι και έξοδοι για προβλήματα

Τα προβλήματα που επιλύονται με Ι/Ο αυτόματα έχουν κάποιο τύπο εισόδου και εξόδου. Πρέπει να τα μοντελοποιήσουμε κάπως. Στο σύγχρονο μοντέλο γενικά μοντελοποιήσαμε τέτοια είσοδο και έξοδο με την βοήθεια ειδικών μεταβλητών κατάστασης, υποθέτοντας ότι οι είσοδοι χτίζονται μέσα σε ορισμένες μεταβλητές στις αρχικές καταστάσεις και ότι η έξοδοι εμφανίζονται σε ορισμένες μεταβλητές μιας εγγραφής. Μπορούμε να κάνουμε το ίδιο και στο ασύγχρονο σύστημα. Ωστόσο αφού τα Ι/Ο αυτόματα μπορούν να έχουν ενέργειες εισόδου και εξόδου , είναι πιο φυσικό να μοντελοποιήσουμε εισόδους και εξόδους των συστημάτων άμεσα με τις ενέργειες εισόδου και εξόδου.

5. Ιδιότητες και μέθοδοι αποδείξεων

Θα περιγράψουμε κάποιους τύπους ιδιοτήτων που αποδεικνύονται για τα ασύγχρονα συστήματα όπως και κάποιες μεθόδους που χρησιμοποιούνται για να τις αποδείξουμε.

Αμετάβλητοι ισχυρισμοί

Ο πιο θεμελιώδης τύπος ιδιότητας που αποδεικνύεται είναι ένας αμετάβλητος ισχυρισμός, η απλώς αμετάβλητος για συντομία. Ορίζουμε τον αμετάβλητο ισχυρισμό ενός αυτόματου Α ότι είναι οποιαδήποτε ιδιότητα όλων των προσεγγίσιμων καταστάσεων του Α που είναι αληθής. Οι αμετάβλητοι αποδεικνύονται τυπικά με επαγωγή στον αριθμό των βημάτων σε μια εκτέλεση που οδηγεί στις επιθυμητή κατάσταση. Πιο γενικά, υπάρχει πιθανότητα να αποδεικνύουμε αμετάβλητους έναν κάθε φορά, χρησιμοποιώντας αμετάβλητους που αποδειχτήκαν πιο πριν όταν μεταφέρουν επακόλουθες επαγωγικές αποδείξεις. Τους αμετάβλητους ισχυρισμούς τους χρησιμοποιήσαμε για την απόδειξη ιδιοτήτων και σε συγχρόνους αλγορίθμους. Όταν έχουμε σύγχρονα συστήματα οι αμετάβλητοι ισχυρισμοί αποδεικνύονται για τις καταστάσεις του συστήματος μετά από έναν αυθαίρετο αριθμό γύρων. Αντίθετα στα ασύγχρονα συστήματα, αποδεικνύονται αμετάβλητοι ισχυρισμοί για τις καταστάσεις συστήματος μετά από έναν αυθαίρετο αριθμό βημάτων. Αφού η ποσότητα επιχειρημάτων είναι πολύ μικρότερη για τους ασύγχρονους αλγορίθμους , τα επιχειρήματα είναι τυπικά μακρύτερα, πιο περιγραφικά και πιο δύσκολα.

Ιδιότητες ίχνους

Ένα Ι/Ο αυτόματο μπορεί να θεωρηθεί ως ένα ως ένα μαύρο κουτί από την οπτική γωνία του χρηστή. Το μόνο που βλέπει είναι τα ίχνη των εκτελέσεων (ή δικαίων εκτελέσεων) του αυτόματων. Μερικές από τις ιδιότητες που αποδεικνύονται για τα Ι/Ο αυτόματα είναι φυσικά καταταγμένες ως ιδιότητες των ιχνών τους ή των δικαίων ιχνών του.

Τυπικά , μια ιδιότητα ίχνους P αποτελείται από τα ακόλουθα:

• sig(P), μια υπογραφή που δεν περιέχει εσωτερικές ενέργειες
• traces(P), ένα σύνολο (πεπερασμένων ή άπειρων ακολουθιών ) των ενεργειών στο σύνολο acts(sig(P))

Δηλαδή, μια ιδιότητα ίχνους χαρακτηρίζει και μια εξωτερική διεπαφή και ένα σύνολο (δηλαδή μια ιδιότητα) ακολουθιών που παρατηρούνται σε αυτή την διεπαφη. Γραφούμε ότι acts(P) σαν συντομία του acts(sig(P)), και παρομοίως in(P) κλτ.

Ο ισχυρισμός ότι ένα Ι/Ο αυτόματο Α ικανοποιεί μια ιδιότητα ίχνους P μπορεί να σημαίνει οποιοδήποτε από τα 2(τουλάχιστον ) διαφορετικά πράγματα:

1. extsig(A)= sig(P) και traces(A) ⊆ traces(P)

2. extsig(A)= sig(P) και fairtraces(A)⊆ traces(P)

Σε οποιαδήποτε περίπτωση , η διαισθητική ιδέα είναι ότι κάθε εξωτερική συμπεριφορά που μπορεί να παραχθεί από το Α είναι επιτρεπόμενη από την ιδιότητα P. Σημειώστε ότι το αντίθετο δεν είναι απαραίτητο –ότι κάθε ίχνος του P μπορεί πράγματι να εκτεθεί από το Α. Ωστόσο η δεδομένη δήλωση ένταξης δεν είναι τετριμμένη: το γεγονός ότι το Α είναι ενεργοποιούμενο λογω εισόδου διασφαλίζει ότι το fairtraces(A)(συνεπώς και traces(A)) περιέχει μια απάντηση από το Α σε κάθε δυνατή ακολουθία ενεργειών εισόδου. Αν fairtraces(A) ⊆ traces(P), τότε όλες οι προκύπτουσες ακολουθίες πρέπει να περιλαμβάνονται στην ιδιότητα P.

Θα εξηγήσουμε τι εννοούμε με τον ορό ότι ένα αυτόματο ικανοποίει μια ιδιότητα ίχνους με ένα παράδειγμα.

Παράδειγμα 8--Αυτόματα και ιδιότητες ίχνους

Θεωρείστε αυτόματα και ιδιότητες ίχνους με σύνολο εισόδου{0} και σύνολο εξόδου{1,2}. Πρώτα υποθέστε ότι traces(P) είναι το σύνολο των ακολουθιών πάνω στο {0,1,2} που περιλαμβάνουν τουλάχιστον ένα 1. Τότε fairtraces(A) ⊆ traces(P) σημαίνει ότι σε κάθε δίκαιη εκτέλεση , το Α πρέπει να βγάλει ως έξοδο τουλάχιστο ν ένα 1. Είναι εύκολο να σχεδιάσουμε ένα Ι/Ο αυτόματο για το οποίο αυτή είναι η περίπτωση.- για παράδειγμα, μπορεί να περιλαμβάνει μια εργασία της οποίας όλη η ευθύνη είναι να παραγιέ έξοδο 1. Η συνθήκη δικαιοσύνης χρησιμοποιείται για να διασφαλίσει ότι αυτή η εργασία πράγματι έχει την ευκαιρία να βγάλει την εξοδο1. Από την άλλη δεν υπάρχει κανένα αυτόματο Α για το οποίο traces(A) ⊆ traces(P), διότι το traces(A) πάντα περιλαμβάνει πάντα το κενό string λ, το οποίο δεν περιέχει ένα 1. Τώρα υποθέστε ότι το traces(P) είναι το σύνολο των ακολουθιών πάνω στο {0,1,2} που περιλαμβάνει τουλάχιστον ένα 0. Σε αυτή την περίπτωση , δεν υπάρχει κανένα Ι/Ο αυτόματο Α(με την δοσμένη εξωτερική διεπαφη) για το οποίο fairtraces(A)⊆ traces(P), διότι το fairtraces(A) πρέπει να περιέχει κάποια ακολουθία που δεν περιλαμβάνει καμία είσοδο.

Ορίζουμε μια λειτουργιά σύνθεσης για τις ιδιότητες ίχνους. Λέμε ότι μια μετρήσιμη συλλογή ιδιοτήτων ίχνους{P_i}_i∈I είναι συμβατή αν οι υπόγραφες τους είναι συμβατές. Τότε η σύνθεση P=Π_i∈IP_i είναι η ιδιότητα ίχνους τέτοια ώστε:

• sig(P)= Π_i∈Isig(P_i)

• traces(P) είναι το σύνολο των ακολουθιών β των εξωτερικών ενεργειών του P τέτοιο ώστε β|acts(P_i)∈ traces(P_i) για όλα τα i∈I.

6. Μετρικές πολυπλοκότητας

Αν και το μοντέλο Ι/Ο αυτομάτου είναι ασύγχρονο , έχει μια φυσική έννοια της χρονικής πολυπλοκότητας. Για ένα δοσμένο αυτόματο Α, ορίζουμε άνω χρονικά όρια για κάθε υποσύνολο των κλάσεων ισοδυναμίας στον καταμερισμό της εργασίας tasks(A). Συγκεκριμένα για κάθε εργασία C, μπορούμε να ορίσουμε ένα όριο upperc, το οποίο μπορεί να είναι είτε ένας θετικός πραγματικός αριθμός είτε το άπειρο ∞.Τότε για κάθε δίκαιη εκτέλεση α του Α, ένας πραγματικά εκτιμώμενος χρόνος μπορεί να σχετιστεί με κάθε συμβάν του α, που υπόκειται στις παρακάτω συνθήκες:

1. Οι χρόνοι είναι μονότονοι μη φθίνοντες στο α

2. Αν το α είναι άπειρο , τότε οι χρόνοι προσεγγίζουν το ∞

3. Από κάθε σημείο μέσα στο α, μια εργασία C μπορεί να ενεργοποιηθεί για χρόνο το πολύ upper_c πριν κάποια ενέργεια του C να πρέπει να συμβεί.

Μιλώντας αυστηρά, αυτό επιβάλλει ένα άνω όριο upperc στον χρόνο μεταξύ διαδοχικών ευκαιριών η εργασία C να εκτελέσει ένα βήμα. Μια δίκαιη εκτέλεση με χρόνους που σχετίζονται με αυτό τον τρόπο λέγεται χρονομετρημένη εκτέλεση. Παρατηρήστε ότι για ένα δεδομένο σύνολο ορίων upper_c, υπάρχουν πολλοί τρόποι να σχετιστούν οι χρόνοι με τα συμβάντα του α, δηλαδή πολλές χρονομετρημένες εκτελέσεις. Μετράμε τον χρόνο μέχρι κάποιο ορισμένο συμβάν π στο α με το ελάχιστο άνω όριο των χρονών που μπορούν να αντιστοιχιστούν σε όλες αυτές τις χρονομετρημένες εκτελέσεις. Παρομοίως μετράμε τον χρόνο μεταξύ δυο συμβατών στο α με το ελάχιστο άνω όριο των διαφόρων μεταξύ των χρόνων που μπορούν να ανατεθούν σε αυτά τα δυο συμβάντα.

'Παράδειγμα 9--Χρονική Ανάλυση'

Έστω α οποιαδήποτε δικαία εκτέλεση του συστήματος στο Παράδειγμα 4 στο οποίο όλες οι διαδικασίες να λαμβάνουν εισόδου init. Σχετίζουμε ένα άνω όριο l με κάθε εργασία κάθε διαδικασίας και ένα άνω όριο d με τις μοναδικές εργασίες κάθε καναλιού. Τότε ο χρόνος όπου η τελευταία διαδικασία λαμβάνει την πρώτη της είσοδο init στο α μέχρι όλες οι διαδικασίες να έχουν εκτελέσει την έξοδο decide είναι το πολύ l+d+l=d+2l. Ο λόγος είναι ότι χρειάζεται το πολύ χρόνος l για την τελευταία διαδικασία που λαμβάνει μια είσοδο init να εκτελέσει τα συμβάντα send για όλους του γείτονες της. Έπειτα χρειάζεται το πολύ χρόνο d για να παραδοθούν όλα αυτά τα μηνύματα , και έπειτα το πολύ χρόνος l για να εκτελέσει κάθε διεργασία την decide.

Περιγραφή Μοντέλου Ασύγχρονου Δικτύου

Τώρα θα αλλάξουμε σύστημα και απο σύστημα κοινής μνήμης θα μιλήσουμε για ασύγχρονα δίκτυα. Ένα ασύγχρονο δίκτυο αποτελείται απο μια συλλογή διαδικασιών που επικοινωνούν μέσω ενός υποσυστήματος επικοινωνίας. Στο πιο σύνηθες μοντέλο που απαντάτε αυτή η επικοινωνία είναι point-to-point, και χρησιμοποιεί ενέργειες send και receive. Υπάρχουν όμως και άλλες εκδόσεις του μοντέλου που επιτρέπουν ενέργειες μετάδοσης, με τις οποίες μια διαδικασία μπορεί να στείλει ένα μήνυμα σε ένα υποσύνολο των διαδικασιών . Επιπλέον υπάρχουν και συνδυασμοί του τύπου επικοινωνία και μετάδοσης και point-to-point επικοινωνία . Σε κάθε περίπτωση μπορεί να προκύψουν επισφαλής συμπεριφορές, που περιλαμβάνουν απώλειες και διπλότυπα.

1. Συστήματα Αποστολής/Λήψης(Send/Receive)

Ξεκινάμε με ένα κατευθυνόμενο γράφημα n κόμβων G=(V,E). Συμβολίζουμε ως out-nbrs_i τους εξερχόμενους γείτονες του κόμβου i και ως in-nbrs_i τους εισερχόμενους κόμβους του i στο κατευθυνόμενο γράφημα, ως distance(i,j)΄ το μήκος του συντομότερου κατευθυνόμενου μονοπατιού από το i στο j στο G και diam την μέγιστη απόσταση από οποιοδήποτε κόμβος σε κάποιων άλλο. Σχετίζουμε τους κόμβους του G με διαδικασίες και τους επιτρέπουμε να επικοινωνούν μέσω καναλιών που τα σχετίζουμε με κατευθυνόμενες ακμές. Επιτρέπουμε και στα βήματα των διαδικασιών και στην επικοινωνία να ενεργούν ασύγχρονα. Για να περιγράψουμε αυτό την ασύγχρονη λειτουργία, μοντελοποιούμε τις διαδικασίες και τα κανάλια ως Ι/Ο αυτόματα. Έστω οτι τοΜείναι ένα σταθερό αλφάβητο μηνυμάτων.

Διαδικασίες

Η διαδικασία που σχετίζεται με κάθε κόμβο i μοντελοποιείται ως ένα αυτόματο Ι/Ο, P_i. To P_i συνήθως έχει κάποιες ενέργειες εισόδου και εξόδου με τις οποίες επικοινωνεί με έναν εξωτερικό χρήστη. Αυτό μας επιτρέπει να εκφράζουμε προβλήματα που πρόκειται να επιλυθούν από ασύγχρονα δίκτυα μέσω των ιχνών στην διεπαφή του χρήστη. Επιπλέον το P_i έχει εξόδους της μορφής send(m)_i,j, όπου j είναι ένας εξερχόμενος χρήστης του i και m είναι ένα μήνυμα (που είναι στοιχείο του Μ), και εισόδους της μορφής receive(m)_j,i, όπου j είναι ένας εισερχόμενος γείτονας του i. Εκτός των περιορισμών της εξωτερικής διεπαφής , το P_i μπορεί να είναι ενα αυθαίρετο αυτόματο Ι/Ο.(Για συγκεκριμένα αποτελέσματα, μπορεί μερικές να θέλουμε να επιβάλουμε επιπλέον περιορισμούς στο P_i , όπως ο περιορισμός του πλήθους των εργασιών ή του πλήθους των καταστάσεων.

Θεωρούμε δύο είδη εσφαλμένων συμπεριφορών: την αποτυχία διακοπής και την Βυζαντινή αποτυχία. Την αποτυχία διακοπής του P_i την μοντελοποιούμε συμπεριλαμβάνοντας στην εξωτερική διεπαφή P_i μια ενέργεια εισόδου, stop_i η οποία έχει ως αποτέλεσμα την μόνιμη απενεργοποίηση όλων των εργασιών του P_i .(Δεν περιορίζουμε της αλλαγές καταστάσεων που προκαλούνται από ένα stop_i ούτε τις αλλαγές κατάστασης που προκαλούνται από υπακόλουθες ενέργειες εισόδου διότι τα αποτελέσματα τους δεν φαίνονται ποτέ έξω από το P_i). Η Βυζαντινή αποτυχία του P_i μοντελοποιείται επιτρέποντας στο P_i να αντικατασταθεί από ένα αυθαίρετο αυτόματο Ι/Ο που έχει την ίδια εξωτερική διεπαφή.

Κανάλια Αποστολής/Λήψης

Το κανάλι που σχετίζεται με κάθε κατευθυνόμενη ακμή (i,j) του G μοντελοποιείται με ένα αυτόματο Ι/Ο C_i,j. Η εξωτερική του διεπαφή αποτελείται από εισόδους της μορφής send(m)_i,j και εξόδους της μορφής receive(m)_i,j όπου m∈M. Εκτός από αυτή την συγκεκριμενοποίηση της εξωτερικής διεπαφής το κανάλι μπορεί να είναι ένα αυθαίρετο αυτόματο Ι/Ο. Ωστόσο τα ενδιαφέροντα κανάλια επικοινωνίας έχουν περιορισμούς στην εξωτερική τους συμπεριφορά, όπως για παράδειγμα ότι όποιο μήνυμα λαμβάνεται πρέπει όντως να έχει σταλεί νωρίτερα. Οι αναγκαίοι περιορισμοί στην εξωτερική συμπεριφορά ενός καναλιού μπορούν να εκφραστούν γενικά υπό την μορφή μιας ιδιότητας ίχνους P. Τα επιτρεπτά κανάλια είναι εκείνα τα αυτόματα Ι/Ο των οποίων η εξωτερική υπογραφή είναι η sig(P) και των οποίων τα δίκαια ίχνη βρίσκονται στο traces(P).

Υπάρχουν δυο τρόποι με τους οποίους μπορεί να μια ιδιότητα ίχνους P να γίνει συγκεκριμένη:

• H καταγραφή μιας συλλογής αξιωμάτων

Πλεονεκτήματα: Ένα πλεονέκτημα της καταγραφής αξιωμάτων είναι κάνει πιο εύκολο των ορισμό μιας ποικιλίας καναλιών, καθένα από τα οποία ικανοποιεί ένα διαφορετικό υποσύνολο των αξιωμάτων.

• Να δώσουμε ένα συγκεκριμένο αυτόματο Ι/Ο του οποίου η εξωτερική διεπαφή είναι η sig(P) και του οποίου τα δίκαια ίχνη είναι ακριβώς το traces(P).

Πλεονεκτήματα: Ένα πλεονέκτημα του να δίνουμε ένα ρητό αυτόματο Ι/Ο είναι ότι σε αυτή την περίπτωση ολόκληρο το σύστημα που αποτελείται από τις διαδικασίες και τα πιο γενικά επιτρεπτά κανάλια περιγράφεται ως μια σύνθεση Ι/Ο αυτομάτων, η όποια και αυτή είναι ένα Ι/Ο αυτόματο. Αυτό μας επιτρέπει να χρησιμοποιούμε τις μεθόδους απόδειξης που έχουν αναπτυχθεί για τα αυτόματα. Για παράδειγμα εδώ έχουμε την έννοια της κατάστασης για όλο το σύστημα(διαδικασίες και κανάλια) την οποία μπορούμε να χρησιμοποιήσουμε στους αμετάβλητους ισχυρισμούς και στις αποδείξεις προσομοίωσης.

Μερικές φορές μπορεί να χρειάζεται ένας εκνευριστικός προγραμματισμός για να ορίσουμε την επιθυμητή ιδιότητα ίχνους ως ένα Ι/Ο αυτόματο. Αυτό συμβαίνει κυρίως όταν η ιδιότητα ίχνους περιλαμβάνει περίπλοκους περιορισμούς ζωτικότητας. Αυτό οδηγεί σε μια σύνθετη στρατηγική όπου οι ιδιότητες ασφάλειας περιγράφονται υπό την μορφή ενός βασικού αυτόματου (το οποίο παρέχει τα κατάλληλα εργαλεία για την υποστήριξη των αμετάβλητων αποδείξεων και των αποδείξεων προσομοίωσης) ενώ οι ιδιότητες ζωτικότητας περιγράφονται χρησιμοποιώντας ειδικά αξιώματα ζωτικότητας. Έτσι η ιδιότητα ίχνους P ορίζει ότι τα ίχνη της είναι ακριβώς εκείνα τα ίχνη του βασικού αυτόματου που ικανοποιεί τα αξιώματα ζωτικότητας.

Αξιόπιστο κανάλι FIFO.

Το πιο συχνά χρησιμοποιούμενο κανάλι είναι το αξιόπιστο κανάλι FIFO. Οι επιτρεπόμενες συμπεριφορές σε αυτό το κανάλι είναι τα δίκαια ίχνη ενός Ι/Ο αυτομάτου με την κατάλληλη εξωτερική διεπαφή , της οποίας η κατάσταση είναι μια ουρά μηνυμάτων. Η ενέργεια send(m)_i,j προσθέτει το m στο τέλος της ουράς. Η ενέργεια receive(m)_i,j ενεργοποιείται αν το m είναι το πρώτο στην ουρά και έχει ως αποτέλεσμα να αφαιρεί το πρώτο μήνυμα από την ουρά. Ο καταμερισμός της εργασίας βάζει όλες τις τοπικά ελεγχόμενες ενέργειες σε μια μοναδική κλάση. Αυτό το αυτόματο δεν είναι απλώς μια περιγραφή της επιτρεπτής συμπεριφοράς για τα αξιόπιστα κανάλια FIFO, είναι το ίδιο ένα παράδειγμα ενός αξιόπιστου καναλιού FIFO. Το ονομάζουμε καθολικό αξιόπιστο κανάλι FIFO με την δοσμένη εξωτερική διεπαφή.

Τώρα θα δώσουμε μια εναλλακτική περιγραφή χρησιμοποιώντας αξιώματα της επιτρεπτής συμπεριφοράς για ένα αξιόπιστο κανάλι FIFO. Ορίζουμε μια ιδιότητα ίχνους P με sig(P) ίση με την δοσμένη υπογραφή και traces(P) ίσο με το σύνολο των ακολουθιών β των ενεργειών μέσα στην sig(P) που ικανοποιεί την ακόλουθη συνθήκη.

Υπάρχει μια συνάρτηση cause που αντιστοιχεί κάθε γεγονός receive στο β με ένα προγενέστερο συμβάν send στο β τέτοια ώστε

1. Για κάθε συμβάν receive π, το π και η cause(π) περιέχουν το ίδιο όρισμα μηνύματος (δηλ. μόνο σωστά μηνύματα παραδίδονται)

2. Η cause είναι συνάρτηση είναι συνάρτηση επί (δηλ. τα μηνύματα δεν χάνονται)

3. Η cause είναι συνάρτηση είναι συνάρτηση ένα προς ένα (δηλ. υπάρχουν διπλότυπα)

4. Η cause διατηρεί την σειρά, δηλαδή δεν υπάρχουν συμβάντα π₁ και π ₂ με το π₁ να προηγείται του π₂ και cause(π₂) να προηγείται του cause (π₁) στο β. (δηλ. δεν υπάρχει αλλαγή στην σειρά)

Η συνάρτηση cause είναι ένας μηχανισμός για τον εντοπισμό του συμβάντος send που προκαλεί το συμβάν receive κάθε φορά. Παρατηρείστε ότι γι’ αυτή την ιδιότητα ίχνους P η συνάρτηση cause για κάθε ακολουθία είναι μοναδική.

Αξιόπιστο κανάλι με αλλαγή σειράς.

Ένας άλλος τύπος καναλιού που υπάρχει εγγυάται την παράδοση όλων των μηνυμάτων , ακριβώς μια φορά το καθένα αλλά δεν διατηρεί απαραιτήτως την σειρά τους. Οι συμπεριφορές που επιτρέπονται για αυτό τον τύπο καναλιού δεν περιγράφονται εύκολα από Ι/Ο αυτόματα γι’ αυτό χρησιμοποιούμε αξιώματα. Η περιγραφεί είναι ίδια με την αξιωματική περιγραφή P για το αξιόπιστο FIFO κανάλι που περιγράφτηκα παραπάνω εκτός από την συνθήκη 4 που άραιται. Μια εναλλακτική περιγραφή μπορεί να δοθεί χρησιμοποιώντας την σύνθετη στρατηγική που περιγράφτηκε πιο πάνω- χρησιμοποιώντας ένα βασικό αυτόματο Ι/Ο Α για την περιγραφή των ιδιοτήτων ασφάλειας και επιπρόσθετα αξιώματα για την περιγραφή της ζωτικότητας. Ακολουθεί αυτό το βασικό αυτόματο Α:

Το Αυτόματο Α:

Υπογραφή:

Είσοδος:
  send(m)i,j, m∈ M

Έξοδος:
  receive(m)i,j,m∈ M


Καταστάσεις:
in-transit, ένα πολυσύνολο των στοιχείων του Μ, αρχικά κενό


Μεταβάσεις:

send(m)i,j
   Αποτέλεσμα:
      in-transit:=in-transit∪{m}

receive(m) i,j
   Προϋπόθεση:
      m∈ in-transit
   Αποτέλεσμα
      αφαίρεσε ένα αντίγραφο του m από το in-transit

Εργασίες:
Αυθαίρετες

Ο καταμερισμός της εργασίας δεν μας ενδιαφέρει γιατί δεν τον χρησιμοποιούμε. Χρησιμοποιώντας το αυτόματο A, ορίζουμε μια ιδιότητα ίχνους P. Η υπογραφή είναι ίδια με την sig(A) και το traces(P) είναι το σύνολο των ιχνών των (όχι απαραίτητα δίκαιων) εκτελέσεων α του Α που ικανοποιεί την ακόλουθη συνθήκη.

Αν σε οποιοδήποτε σημείο στο α και για οποιοδήποτε m∈M έχουμε ότι m∈in-transit, τότε σε κάποιο σημείο αργότερα στο α, θα συμβεί ένα συμβάν receive(m).

Κανάλια με αποτυχίες

Υπάρχουν και κανάλια στα οποία συμβαίνουν αποτυχίες. Οι αποτυχίες που θα συζητήσουμε είναι η απώλεια μηνυμάτων και τα διπλότυπα. Ένα κανάλι που επιτρέπει αυθαίρετη απώλεια αλλά κανένα διπλότυπο, ή αυθαίρετα διπλότυπα αλλά καθόλου απώλειες περιγράφεται με τον ίδιο τρόπο όπως τα αξιόπιστα κανάλια με αλλαγή σειράς χρησιμοποιώντας την συνάρτηση cause. Απλώς πρέπει να παραλείψουμε την συνθήκη 2 και/ή την συνθήκη 3 όπου είναι κατάλληλο. Ωστόσο θέλουμε ένα έχουμε περιορισμένο μέγεθος απώλειας μηνυμάτων και/ή διπλότυπων. Για παράδειγμα , όταν έχουμε απώλεια μηνυμάτων , δεν θέλουμε να θεωρήσουμε την περίπτωση όπου χάνονται όλα τα μηνύματα, γιατί σε αυ΄τη την περίπτωση τίποτα δεν είναι εγγυημένο ότι θα συμβεί. Μια τυπική συνθήκη που περιορίζει την απώλεια μηνυμάτων είναι αυτή που λέει ότι ένα μήνυμα που στέλνεται άπειρα πολλές φορές πρέπει να ληφθεί άπειρα πολλές φορές. Για να το πούμε τυπικά αυτό , χρησιμοποιούμε την ακόλουθη συνθήκη πάνω στην συνάρτηση cause.

Ισχυρός Περιορισμός Απώλειας(SSL):Αν υπάρχουν απείρως πολλά συμβάντα send(m) στο β (για κάθε συγκεκριμένο m), τότε υπάρχουν απείρως πολλά συμβάντα send(m) στο εύρος της συνάρτησης cause.

Αυτό μας λέει ότι απείρως πολλά διαφορετικά συμβάντα send επιτυγχάνουν την παράδοση των μηνυμάτων τους. Αυτή η συνθήκη για παράδειγμα δεν ικανοποιείται από μια ακολουθία στην οποία υπάρχουν απείρως πολλά συμβάντα receive που προκαλούνται όλα από το το ίδιο συμβάν send.

Μια άλλη συνθήκη που περιορίζει την απώλεια μηνυμάτων είναι αυτή που δεν αναφέρει το m αλλά λέει ότι απείρως πολλά send προκαλούν το receive απείρως πολλών μηνυμάτων.

Ασθενής περιορισμός απώλειας ( WLL): αν υπάρχουν απείρως πολλά συμβάντα send στο β, τότε το εύρος της συνάρτησης cause είναι άπειρο.

Όσον αφορά τα διπλότυπα, θέλουμε να περιορίσουμε των αριθμό των αντιγράφων κάθε μηνύματος να είναι πεπερασμένος ή φραγμένος από κάποια ιδιαίτερο αριθμό k. Για παράδειγμα,

Πεπερασμένα Διπλότυπα: η συνάρτηση cause αντιστοιχίζει μόνο πεπερασμένο αριθμό συμβάντων receive σε κάθε ιδιαίτερο συμβάν send.

Μέχρι τώρα έχουμε περιγράψει όλα τα κανάλια με απώλειες χρησιμοποιώντας αξιώματα. Θα χρησιμοποιήσουμε την σύνθετη στρατηγική για να περιγράψουμε δυο τέτοια κανάλια.

Παράδειγμα 1 -- Ένα κανάλι FIFO με απώλειες

Ορίζουμε ένα κανάλι που επιτρέπει περιορισμένη απώλεια, πεπερασμένα διπλότυπα και όχι αλλαγή στην σειρά. Ακολουθεί το αυτόματο.

Το Αυτόματο Α:


Υπογραφή:
Ως συνήθως.

Καταστάσεις:

queue, μια ουρά FIFO των στοιχείων του Μ, αρχικά κενή


Μεταβάσεις:

send(m) i,j
   Αποτέλεσμα:
       πρόσθεσε οποιοδήποτε πεπερασμένο αριθμό αντιγράφων του m στην queue


receive(m)i,j
   Προϋπόθεση:
       το m είναι πρώτο στην queue
   Αποτέλεσμα:
       αφαίρεσε το πρώτο στοιχείο της queue


Εργασίες:
Αυθαίρετες

Ο ορισμός του αυτόματου Α εγγυάται ότι το κανάλι δεν θα αλλάξει την σειρά των μηνυμάτων και ότι παραδίδει μόνο πεπερασμένο αριθμό αντιγράφων κάθε μηνύματος. Ωστόσο χρειάζεται να επιβάλλουμε άλλες δυο επιπλέον συνθήκες ζωτικότητας.

1. Αν σε οποιοδήποτε σημείο η queue δεν είναι άδεια, τότε σε κάποιο σημείο αργότερα γίνεται ένα συμβάν receive.

2. Αν υπάρχουν απείρως πολλά συμβάντα send, τότε απείρως πολλά από αυτά καταφέρνουν να τοποθετήσουν (τουλάχιστον ένα αντίγραφο) τα μηνύματά τους στην queue.

Το αυτόματο Α σε συνδυασμό με τις συνθήκες ζωτικότητας ορίζουν την ιδιότητα ίχνους , η οποία συνεπάγεται ότι αν υπάρχουν απείρως πολλά συμβάντα send τότε απείρως πολλά από αυτά έχουν ανταπόκριση από συμβάντα receive , δηλαδή συνεπάγεται την συνθήκη του ασθενή περιορισμού απώλειας(WLL).

'Παράδειγμα 2 -- Ένα κανάλι αναδιάταξης με απώλειες

Ορίζουμε ένα κανάλι που επιτρέπει περιορισμένη απώλεια, πεπερασμένα διπλότυπα και αλλαγή της σειράς. Ακολουθεί το αυτόματο.

Το Αυτόματο Α:

Υπογραφή:
Ως συνήθως


Καταστάσεις:
in-transit, ένα πολυσύνολο των στοιχείων του Μ, αρχικά κενό


Μεταβάσεις:

send(m)i,j
  Αποτέλεσμα:
     πρόσθεσε οποιοδήποτε πεπερασμένο πλήθος αντιγράφων του m στο in-transit


receive(m)i,j
  Προϋπόθεση:
     m∈ in-transit
  Αποτέλεσμα
     αφαίρεσε ένα αντίγραφο του m από το in-transit


Εργασίες:
Αυθαίρετες

Προσθέτουμε δυο συνθήκες ζωτικότητας.

1. Αν σε οποιοδήποτε σημείο , το in-transit δεν είναι κενό , τότε σε κάποιο σημείο αργότερα, θα γίνει ένα συμβάν receive.

2. Αν υπάρχουν απείρως πολλά συμβάντα send, τότε απείρως πολλά από αυτά επιτυγχάνουν να τοποθετήσουν (τουλάχιστον ένα αντίγραφο) τα μηνύματα τους στο in-transit.

Η προκύπτουσα ιδιότητα συνεπάγεται ότι αν υπάρχουν απείρως πολλά συμβάντα send τότε απείρως πολλά από αυτά έχουν ανταποκρινόμενα συμβάντα receive το οποίο συνεπάγεται την συνθήκη WLL. Σημειώστε ότι κάθε ίχνος που επιτρέπεται από το παράδειγμα 1 επιτρέπεται και εδώ. Ωστόσο υπάρχουν ίχνη τα οποία επιτρέπονται εδώ αλλά όχι και στο προηγούμενο παράδειγμα.

Ασύγχρονα συστήματα αποστολής λήψης(send/receive)

Ένα ασύγχρονο σύστημα δικτύου αποστολής λήψης για το κατευθυνόμενο γράφημα G προκύπτει από την σύνθεση των διαδικασιών και το Ι/Ο αυτομάτων καναλιού, χρησιμοποιώντας το συνηθισμένο Ι/Ο αυτόματο σύνθεσης. Ο ορισμός της σύνθεσης καθιστά δυνατή σωστή αλληλεπίδραση μεταξύ των στοιχείων, για παράδειγμα, όταν η διαδικασία P_i εκτελεί μια ενέργεια send(m)_i,j μια ταυτόχρονη ενέργεια εισόδου send(m)_i,j εκτελείται από το κανάλι C_i,j. Και στα δυο στοιχεία επιτελούνται κατάλληλες αλλαγές κατάστασης.

Μερικές φορές είναι βολικό να μοντελοποιούμε του χρήστες ενός συστήματος αποστολής λήψης σαν άλλο ένα αυτόματο Ι/Ο, U. Οι εξωτερικές ενέργειες του U είναι οι ενέργειες των διαδικασιών στης διεπαφές χρήστη τους. Το αυτόματο χρήστη U περιγράφεται συχνά ως η σύνθεση μιας συλλογής αυτομάτων χρήστη U_i, ένα για κάθε κόμβο i του βασικού γραφήματος. Σε αυτή την περίπτωση , οι εξωτερικές ενέργειες του U_i είναι ίδιες με τις ενέργειες του P_i στην διεπαφή χρήστη. (Αν θεωρήσουμε αποτυχίες διακοπής, η ενέργειες stop δεν περιλαμβάνονται μεταξύ των ενεργειών του χρήστη).

Ιδιότητες των συστημάτων αποστολής/λήψης με αξιόπιστα κανάλια FIFO

Θα δώσουμε ένα θεώρημα για αυτά τα συστήματα. Αυτό το θεώρημα αναγνωρίζει περιπτώσεις υπό τις οποίες τα συμβάντα ενός δίκαιου ίχνους μπορούν να αναδιαταχτούν για να αποδώσουν ένα άλλο δίκαιο ίχνος. (Σημειώστε ότι σύμφωνα με τον τυπικό ορισμό των αυτομάτων σύνθεσης I/O, τα ίχνη περιλαμβάνουν συμβάντα send και receive καθώς και συμβάντα στην διεπαφή χρήστη). Αυτό που απαιτείται είναι η αναδιάταξη να σέβεται ορισμένες βασικές εξαρτήσεις: την εξάρτηση ενός συμβάντος receive από ένα αντίστοιχο συμβάν send (με σεβασμό στην μοναδικά ορισμένη συνάρτηση cause) και την πιθανή εξάρτηση οποιουδήποτε συμβάντος από όλα τα προγενέστερα συμβάντα στην ίδια κομβική διαδικασία.

Ορίστε οποιοδήποτε ασύγχρονο σύστημα αποστολής λήψης Α με καθολικά αξιόπιστα κανάλια FIFO. Έστω β οποιοδήποτε ίχνος του Α. Ορίζουμε μια μη ανακλαστική μερική σειρά ->_β στα γεγονότα του β ως ακολούθως.

Αν π και φ είναι δυο συμβάντα στο β, με το π να προηγείται του φ τότε λέμε ότι π->_β φ, ή ότι το φ εξαρτάται από το π με την προϋπόθεση ότι ισχύει ένα από τα ακόλουθα:

1. Τα π και φ είναι συμβάντα της ίδιας διαδικασίας P_i

2. Το π είναι της μορφής send(m)_i,j και φ είναι το αντίστοιχο του συμβάν receive_i,j

3. Τα π και φ σχετίζονται με μια αλυσίδα σχέσεων τύπου 1 και 2.

Θεώρημα 1. Έστω Α ένα ασύγχρονο σύστημα αποστολής /λήψης με καθολικά αξιόπιστα κανάλια FIFO, και έστω ότι β είναι ένα δίκαιο ίχνος του Α. Έστω γ μια ακολουθία που προκύπτει από την αναδιάταξη των γεγονότων μέσα στο β αλλά με διατήρηση της σειράς -> _β. Τότε το γ είναι και αυτό ένα δίκαιο ίχνος του Α.

Απόδειξη. Το θεώρημα 4 της προηγούμενης ενότητας συνεπάγεται ότι β|P_i∈ fairtraces(P_i) για κάθε i. Αφου γ| P_i=β| P_i για κάθε i, έπεται ότι γ| P_i∈ fairtraces(P_i) για κάθε i. Επίσης το θεώρημα αυτό συνεπάγεται ότι β|C_i,j∈ fairtraces(C_i,j) για κάθε i και j. Αφού γ|C_i,j έχει το ίδιο σύνολο συμβάντων με το β|C_i,j και η αναδιάταξη διατηρεί την σειρά των συμβάντων στην P_i και την σειρά των στην P_j, και των συμβάντων receive με τα αντίστοιχα συμβάντων send, επομένως γ|C_i,j∈ fairtraces(C_i,j). Μετά το θεώρημα 6 από την προηγούμενη ενότητα συνεπάγεται ότι γ∈ fairtraces(Α).

Το θεώρημα 2 έχει ένα πόρισμα ότι οποίο λέει ότι μερικές αναδιατάξεις των δίκαιων εκτελέσεων είναι και αυτές δίκαιες εκτελέσεις.

Πόρισμα. Έστω Α ένα ασύγχρονο σύστημα αποστολής λήψης με καθολικά αξιόπιστα κανάλια FIFO, και έστω α μια δίκαιη εκτέλεση του Α. Έστω γ μια ακολουθία που προκύπτει από την αναδιάταξη των γεγονότων στο β=trace(α) διατηρώντας την σειρά -> _β. Τότε υπάρχει μια δίκαιη εκτέλεση α’ του Α τέτοια ώστε trace(α’)=γ και τέτοια ώστε α και α’ να μην ξεχωρίζονται από καμιά διαδικασία P_i.

Αποδεικτική ιδέα. Το θεώρημα 1 συνεπάγεται γ∈ fairtraces(Α). τα θεωρήματα 4 και 5 από την προηγούμενη ενότητα αποδεικνύουν την ύπαρξη του απαιτούμενου α’.

Η εκτέλεση του α’ του οποίου η ύπαρξη εγγυάται από το πόρισμα δεν μπορεί να διακριθεί από την αυθεντική εκτέλεση του α από τις διαδικασίες του συστήματος Α (ακόμη και αν συνδυάσουν τις πληροφορίες τους). Αυτό σημαίνει ότι οι διαδικασίες δεν γνωρίζουν την συνολική σειρά των γεγονότων σε μια εκτέλεση , δεν μπορούν να ορίσουν την σειρά των συμβάντων σε διαφορετικές διαδικασίες αν τα συμβάντα αυτά δεν σχετίζονται με τις εξαρτήσεις μηνύματος και διαδικασίας που περιγράφονται από την μερική σειρά -> _β.

Μετρικές πολυπλοκότητας

Την πολυπλοκότητα επικοινωνίας την μετρούμε με τον αριθμό των μηνυμάτων που στέλνονται και /ή τον αριθμό των μηνυμάτων που λαμβάνονται. Επίσης μπορούμε να λάβουμε υπόψη τον αριθμό των bit στα μηνύματα.

Για να μετρήσουμε την χρονική πολυπλοκότητα, χρησιμοποιούμε μια περίπτωση της γενικής μετρικής της χρονικής πολυπλοκότητας που ορίζεται για τα Ι/Ο αυτόματα. Δηλαδή σχετίζουμε ένα άνω όριο l με κάθε εργασία κάθε διαδικασίας. Αυτό επιβάλλει ένα άνω όριο l στον χρόνο μεταξύ δυο διαδοχικών ευκαιριών μιας εργασίας να εκτελέσει ένα βήμα. Επίσης χρειαζόμαστε υποθέσεις για τον χρόνο παράδοσης των μηνυμάτων. Για την ειδική περίπτωση καθολικών αξιόπιστων καναλιών FIFO, σχετίζουμε ένα άνω όριο 'd με την ενιαία εργασία που αποτελείται από τις ενέργειες receive κάθε καναλιού. Αυτό επιβάλλει ένα άνω όριο d στον χρόνο παράδοσης για το πιο παλιό μήνυμα στο κανάλι. Έτσι η συνήθης μας μετρική της χρονικής πολυπλοκότητας λαμβάνει υπόψη τον όγκο των μηνυμάτων στα κανάλια -- το k-οστό μήνυμα στην ουρά ενός καναλιού είναι εγγυημένο ότι παραδίδεται μέσα σε χρόνο kd.

Μερικές φορές κάνουμε μια λιγότερο ρεαλιστική αλλά πιο απλή υπόθεση για τον χρόνο παράδοσης μηνύματος: ένα άνω όριο d στον χρόνο παράδοσης για κάθε μήνυμα στο κανάλι ανεξαρτήτως του όγκου μηνυμάτων μέσα στο κανάλι. Αυτή η υπόθεση δεν εκφράζεται απλά με την συσχέτιση χρονικών ορίων με εργασίες (αλλά έχει λογική υπόσταση παρ’ όλα αυτά). Επίσης μπορούμε να επεκτείνουμε τις υποθέσεις για το χρονικό όριο καναλιού σε μη καθολικά κανάλια FIFO με προφανή τρόπο.</SOURCECODE>