Ο προσομοιωτής
αυτός περιγράφει το πρόβλημα των κρίσιμων περιοχών. Θεωρούνται δυο διεργασίες Pi και Pj.
Ο
προσομοιωτής χωρίζεται στα εξής βήματα τα οποία ο χρήστης προκαλεί σειριακά
επιλέγοντας το πλήκτρο .
·
Απόδειξη πρώτης ιδιότητας: Διατήρηση
αμοιβαίου αποκλεισμού
·
Κάθε Pi εισέρχεται στο κρίσιμο τμήμα μόνο όταν flag[j]==false ή turn==i
·
Επίσης αν και οι δυο διεργασίες μπορούν
να εκτελούν τα κρίσιμα μέρη τους ταυτόχρονα, τότε flag[i]==flag[j]==true
·
Αυτές οι δυο παρατηρήσεις υπονοούν ότι
οι Pi και Pj δε θα μπορούσαν να τρέξουν με επιτυχία τις εντολές
while στον ίδιο
περίπου χρόνο, καθώς η τιμή του “turn” μπορεί να είναι είτε μόνο i είτε μόνο j.
·
Συνεπώς, μια από τις διεργασίες, έστω η
Pj πρέπει
να έχει εκτελέσει με επιτυχία την εντολή while, ενώσω η Pi έπρεπε να εκτελέσει τουλάχιστον μια επιπλέον
εντολή (“turn==j”).
·
Όμως, καθώς τη συγκεκριμένη στιγμή, flag[j]==true και turn==j,
και αυτή η συνθήκη θα συνεχίσει να ισχύει όσο η Pj είναι στη κρίσιμη περιοχή της, διατηρείται ο
αμοιβαίος αποκλεισμός.
·
Απόδειξη δεύτερης και τρίτης ιδιότητας:
Πρόοδος (Progress Requirement)
Και αναμονή με όριο (Bounded-Waiting)
·
Μια διεργασία Pi μπορεί να εμποδιστεί να εισέλθει στην κρίσιμη
περιοχή μόνο όταν παραμένει στο βρόγχο του while με τη συνθήκη flag[j]==true και turn==j.
Αυτός είναι ο μοναδικός βρόγχος
·
Αν Pj δεν είναι έτοιμη να εισέλθει στην κρίσιμη περιοχή,
τότε flag[j]==false και η Pi μπορεί να εισέλθει στην κρίσιμη περιοχή της
·
Αν η Pj έχει flag[j]==true και επίσης εκτελεί την εντολή while τότε μπορεί να ισχύει είτε turn==i είτε turn==j.
·
Αν turn==i τότε η Pi μπορεί να εισέλθει στη κρίσιμη περιοχή της
·
Όμως, αν turn==j
και η Pj έχει
εισέλθει στη κρίσιμη περιοχή της, όταν η Pj εξέλθει θα θέσει flag[j]=false, επιτρέποντας στην Pi να εισέλθει εκείνη στη δική της.
·
Αν η Pj επιστρέφει στην αρχή του εξωτερικού της βρόγχου
και θέσει flag[j]=true,
πρέπει επίσης να θέσει turn=i, έτσι ώστε να
μπορεί να μπει ξανά στο βρόγχο του while ξανά.
·
Συνεπώς, καθώς η Pi δε μπορεί να αλλάξει τη τιμή της μεταβλητής turn ενώσω εκτελεί την εντολή while, η Pi θα εισέλθει στην κρίσιμη περιοχή της (Πρόοδος)
μετά την πρώτη εισαγωγή της Pj (αναμονή με όριο)