Σημειώσεις:Κατανεμημένοι Αλγόριθμοι:SimpleSynch

Από DistrSys

SimpleSynch

Πρόβλημα: Συγχρονισμός Δίκτυο: Γενικό Κλάση: Αποκεντρωτικός

Πολυπλοκότητα

Χρονική: r(c + d + O(l)) το πολύ, για την εξομοίωση r γύρων Επικοινωνίας: 2Ε σε κάθε γύρο

Στη σύνταξη του κειμένου συνεισέφερε ο Μητσάκος Χρήστος

SimpleSynch αλγόριθμος (άτυπος): Για κάθε γύρο r, μετά την παραλαβή μιας εισόδου της μορφής user-send(T, r)i, η διεργασία SimpleSynchi πρώτα στέλνει ένα μήνυμα σε κάθε γείτονα SimpleSynchi , που περιέχει τον αριθμό του γύρου r και όλα τα μηνύματα από το Ui στο Uj που εμφανίζονται στο Τ. Όταν η SimpleSynchi θα έχει λάβει ένα μήνυμα γύρος r από όλους τους γείτονες, βγάζει σαν έξοδο user-receive(T΄, r)i, όπου Τ΄ είναι το σύνολο των μηνυμάτων που παραλήφθηκαν, το καθένα με τον αποστολέα του.

Πιο τυπικά, ο SimpleSynch είναι το ακόλουθο αυτόματο.

SimpleSynch αυτόματο (τυπικά):

Ενέργειες:

Εισόδου: user-send(T, r)i, Τ ένα σύνολο από tagged messages, r Є N+
         receive(N, r)j,i N ένα σύνολο μηνυμάτων r Є N+, j Є nbrs

Εξόδου: user-receive(T, r)i, Τ ένα σύνολο από tagged messages, r Є N+
        send (N, r)i,j N ένα σύνολο μηνυμάτων r Є N+, j Є nbrs

Καταστάσεις: user-sent, user-rcvd, το καθένα ένα διάνυσμα από N+ μεταβλητές τύπου Boolean, αρχικά όλες στην τιμή false
             pkt-sent, pkt-rcvd, το καθένα ένας πίνακας από nbrs x N+ μεταβλητές τύπου Boolean, αρχικά όλες false
             outbox, ένας πίνακας από nbrs x N+ σύνολα μηνυμάτων, αρχικά όλα 0
             inbox, ένα διάνυσμα από N+ σύνολα από tagged messages, αρχικά όλα 0

Μεταβάσεις: user-send(T, r)i

   Αποτέλεσμα: User-sent(r) = true
               for all j Є nbrs do
                  outbox(j, r) = {m|(m, j) Є T}
               send (N, r)i,j

   Προϋπόθεση: user-sent(r) = true
               pkt-sent(j, r) = false
               N = outbox(j, r)

   Αποτέλεσμα: pkt-sent(j, r) = true
               receive(N, r)j,i

   Αποτέλεσμα: inbox(r) = inbox(r) U {(m, j) | m Є N}
               pkt-rcvd(j, r) = true
               user-receive(T, r)i

   Προϋπόθεση: user-sent(r) = true
               for all j Є nbrs
                  pkt-rcvd(j, r) = true
               T = inbox(r)
               user-rcvd(r) = false

   Αποτέλεσμα: user-rcvd(r) = true

Εκτέλεση: for every r:
             user-receive(T, r)i, Τ ένα σύνολο από tagged messages
          for every j Є nbrs and every r:
             send (N, r)i,j, N ένα σύνολο μηνυμάτων

Το SimpleSynch σύστημα προκύπτει συνθέτοντας τις SimpleSynchi διεργασίες, αξιόπιστα FIFO send/receive κανάλια Ci,j για όλες τις ακμές και τους χρήστες, όπως φαίνεται και στο παρακάτω σχήμα.

SimpleSynch

Λήμμα (SimpleSynch.1)

Αν α είναι μια δίκαιη εκτέλεση του SimpleSynch συστήματος, τότε υπάρχει μια δίκαιη εκτέλεση α΄ του LocSynch συστήματος που καμία Ui δεν μπορεί να την ξεχωρίσει από την α.

Απόδειξη:

Αυτή τη φορά, σε αντίθεση με την απόδειξη του Λήμματος 1, δεν υπάρχει αναδιάταξη των γεγονότων στους διαφορετικούς χρήστες και έτσι η αντιστοιχία μπορεί να αποδειχθεί χρησιμοποιώντας τεχνικές εξομοίωσης. Έστω S και L τα συστήματα SimpleSynch και LocSynch αντίστοιχα, το καθένα τροποποιημένο ελαφρά ώστε οι ενέργειές τους που κατηγοριοποιούνται ως εξωτερικές να είναι ακριβώς όλες οι ενέργειες των αυτομάτων χρήστη. (Δηλαδή, οι εσωτερικές ενέργειες των χρηστών επαναπροσδιορίζονται σαν έξοδοι και οι send και receive ενέργειες είναι «κρυφές» - επαναπροσδιορίζονται ως εσωτερικές) Αν s και u είναι καταστάσεις των S και L αντίστοιχα, τότε ορίζουμε το (s, u) Є f αν ισχύουν όλα τα παρακάτω:

1. Όλες οι καταστάσεις χρηστών είναι ίδιες στο s και στο u.
2. u.user-sent(i, r) = s.user-sent(r)i
3. u.user-rcvd(i, r) = s.user-rcvd(r)i
4. u.tray(i, r) = Uj≠i {(m, j) : m Є s.outbox(i, r)j}

Για να αποδείξουμε ότι η f είναι μια σχέση προσομοίωσης, χρειαζόμαστε τον ακόλουθο αμετάβλητο ισχυρισμό για το S.

Ισχυρισμός 2: Σε κάθε εφικτή κατάσταση του SimpleSynch συστήματος, αν pkt-rcvd(j, r)i = true, τότε

#user-sent(r)j = true
#{m : (m, j) Є inbox(r)i} = outbox(i, r)j

Η απόδειξη αυτού του αμετάβλητου ισχυρισμού χρησιμοποιεί άλλες ενδιάμεσες αμετάβλητες υποθέσεις, όπως την ορθότητα των μηνυμάτων κατά την μεταβίβαση. (Όπως και πριν, υποθέτουμε ότι τα κανάλια είναι γενικά αξιόπιστα FIFO για την δήλωση και την απόδειξη τέτοιων ισχυρισμών.) Δεδομένου του Ισχυρισμού 2, η απόδειξη ότι η f είναι μια σχέση προσομοίωσης είναι απλή. Η μόνη ενδιαφέρουσα περίπτωση είναι η user-receive, η οποία χρησιμοποιεί τον Ισχυρισμό 2 στην απόδειξή του.

Η ύπαρξη μιας σχέσης προσομοίωσης υπονοεί ότι κάθε ίχνος του S είναι ίχνος του L. (Θυμηθείτε ότι οι ενέργειες που περιλαμβάνονται σε αυτά τα ίχνη είναι ακριβώς οι ενέργειες των αυτομάτων χρήστη.) Όμως χρειαζόμαστε περισσότερα – συγκεκριμένα, χρειάζεται να γνωρίζουμε ότι οι συνθήκες δικαιοσύνης του S υπονοούν τις συνθήκες δικαιοσύνης του L. Θα δείξουμε ότι fairtraces(S) ≤ fairtraces(L), και στην συνέχεια θα εφαρμόσουμε γενικά θεωρήματα σύνθεσης για τα αυτόματα εισόδου/εξόδου για να συμπληρώσουμε τις καταστάσεις του χρήστη και να εξάγουμε την απαιτούμενη σχέση ανάμεσα στις εκτελέσεις.

Για την απόδειξη χρησιμοποιούμε το γεγονός ότι μια σχέση εξομοίωσης δείχνει περισσότερα από μια σχέση ανάμεσα στα ίχνη – δείχνει μια στενή συσχέτιση ανάμεσα στις εκτελέσεις. Έστω β Є fairtraces(S) και α μια δίκαιη εκτέλεση του S με β = trace(α). Τότε από γνωστό θεώρημα της μοντελοποίηση ασύγχρονων συστημάτων γνωρίζουμε ότι υπάρχει μια εκτέλεση α΄ του L που αντιστοιχεί στο α, όσον αφορά το f. Ισχυριζόμαστε ότι η α΄ είναι μια δίκαιη εκτέλεση του L.

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

Δεύτερον, μπορεί να υπάρχουν r και i τέτοια ώστε το user-receivei έργο για τον r να είναι ενεργοποιημένο από κάποιο σημείο και μετά στην α΄, χωρίς όμως ωστόσο να συμβαίνει κάποιο βήμα αυτού του έργου. Αυτό σημαίνει ότι από εκείνο το σημείο και μετά στην α΄, user-sent(j, r) = true for all j Є nbrsi U {i} και user-rcvd(i, r) = false. Η αντιστοίχηση τότε μας λέει ότι για το αντίστοιχο σημείο στην α, user-sent(r)j = true for all j Є nbrsi U {i} και user-rcvd(r)i = false.

Χρησιμοποιούμε τον ακόλουθο ισχυρισμό:

Ισχυρισμός 3: Σε κάθε εφικτή κατάσταση του SimpleSynch συστήματος, το ακόλουθο ισχύει. Αν pkt-sent(i, r)j = true τότε είτε το κανάλι Cj,i περιέχει κάποιο μήνυμα, είτε pkt-rcvd(j, r)i = true.

Τότε για κάθε j Є nbrsi η δικαιοσύνη για το έργο send στον γύρο r μας λέει ότι τελικά, στην α, η pkt-sent(j, r)i γίνεται αληθής. Τότε ο Ισχυρισμός 3 και η δικαιοσύνη των καναλιών μας λένε ότι τελικά η pkt-rcvd(j, r)i γίνεται αληθής. Τότε η δικαιοσύνη για το user-receivei έργο στον γύρο r στο S μας λέει ότι τελικά συμβαίνει ένα βήμα αυτού του έργου στην α και έτσι, λόγω της συσχέτισης, και στην α΄. Άτοπο επίσης.

☐

Σημειώνουμε ότι η απόδειξη του Λήμματος 2 δείχνει και ότι fairtraces(S) ≤ fairtraces(L), πέραν την απόδειξης της αδυναμίας διαχωρισμού για τους μεμονωμένους χρήστες.

Θεώρημα (SimpleSynch.2)

Αν α είναι μια δίκαιη εκτέλεση του SimpleSynch συστήματος, τότε υπάρχει μια δίκαιη εκτέλεση του GlobSynch συστήματος τέτοια ώστε κανένα Ui να μην μπορεί να τις διαχωρίσει.

Απόδειξη:

Από τα Λήμματα 1 και 2.

☐

Ανάλυση Απόδοσης

Κάθε γύρος χρειάζεται 2|Ε| μηνύματα, ένα σε κάθε κατεύθυνση σε κάθε ακμή του γραφήματος. Υποθέτουμε ότι:

• c είναι ένα άνω όριο χρόνου για να συμβεί κάθε user-senti γεγονός, ενώ έχουν συμβεί όλα τα user-receivei γεγονότα για όλους τους προηγούμενους γύρους.
• l είναι ένα άνω φράγμα στον χρόνο εκτέλεσης κάθε ενέργειας ε σε κάποια διεργασία k.
• d είναι ένα άνω φράγμα στον χρόνο παράδοσης του παλαιότερου μηνύματος που βρίσκεται σε κάποιο κανάλι. επικοινωνίας τότε ο χρόνος που χρειάζεται για την εξομοίωση r γύρων είναι το πολύ r(c + d + O(l)).