Επικοινωνούσες Ακολουθιακές Διεργασίες

Στην επιστήμη υπολογιστών, οι Επικοινωνούσες Ακολουθιακές Διεργασίες (Communicating Sequential Processes ή CSP) είναι μια τυπική γλώσσα για την περιγραφή τρόπων αλληλεπίδρασης σε ταυτόχρονα συστήματα. Είναι μέλος της οικογένειας μαθηματικών θεωριών του ταυτοχρονισμού που είναι γνωστή σαν άλγεβρες διεργασιών (process algebras) ή λογισμοί διεργασιών. Η CSP είχε σημαντική επίδραση στη σχεδίαση της γλώσσας προγραμματισμού occam, και υπήρξε επιρροή στη σχεδίαση των γλωσσών Limbo και Go.

Η αρχική περιγραφή της CSP δόθηκε σε μια δημοσίευση του 1978 από τον Τόνυ Χόαρ, αλλά έχει εξελιχθεί σημαντικά από τότε. Η CSP έχει εφαρμοστεί στην πράξη στη βιομηχανία λογισμικού, σαν εργαλείο για την τυπική προδιαγραφή και επαλήθευση χαρακτηριστικών ταυτοχρονισμού διάφορων συστημάτων, όπως ο Transputer T9000, και ένα ασφαλές σύστημα ηλεκτρονικού εμπορίου. Η ίδια η θεωρία της CSP εξακολουθεί να είναι αντικείμενο έρευνας, ενώ γίνεται προσπάθεια να βελτιωθεί η καταλληλότητά της για πρακτικές εφαρμογές (π.χ. αυξάνοντας την κλίμακα των συστημάτων που μπορούν να αναλυθούν ρεαλιστικά).

Ιστορία

Η έκδοση της CSP που παρουσιάστηκε στην αρχική δημοσίευση του Χόαρ το 1978 ήταν στην πραγματικότητα μια ταυτόχρονη γλώσσα προγραμματισμού και όχι λογισμός διεργασιών (process calculus). Είχε σημαντικά διαφορετική σύνταξη σε σχέση με τις εκδόσεις της CSP που ακολούθησαν, δεν είχε μαθηματικά ορισμένη σημασιολογία, και δε μπορούσε να αναπαραστήσει μη-ντετερμινισμό χωρίς άνω όριο (unbounded nondeterminism). Τα προγράμματα στην αρχική CSP γράφονταν σαν παράλληλη σύνθεση ενός σταθερού αριθμού ακολουθιακών διεργασιών, οι οποίες επικοινωνούσαν μεταξύ τους με σύγχρονο πέρασμα μηνυμάτων (synchronous message-passing). Σε αντίθεση με τις μεταγενέστερες εκδόσεις της CSP, σε κάθε διεργασία δινόταν ένα όνομα και η πηγή ή ο προορισμός ενός μηνύματος οριζόταν δίνοντας το όνομα της επιθυμητής διεργασίας που το έστελνε ή το λάμβανε. Για παράδειγμα η διεργασία

COPY = *[c:character; west?c → east!c]

επαναληπτικά λαμβάνει ένα χαρακτήρα από τη διεργασία με όνομα west και τον στέλνει στη διεργασία με όνομα east. Η παράλληλη σύνθεση

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

δίνει τα ονόματα west στη διεργασία DISASSEMBLE, X στη διεργασία COPY και east στη διεργασία ASSEMBLE, εκτελώντας και τις τρεις διεργασίες ταυτόχρονα.

Μετά τη δημοσίευση της αρχικής έκδοσης της CSP, ο Χόαρ, ο Stephen Brookes και ο A. W. Roscoe ανέπτυξαν και βελτίωσαν τη θεωρία της CSP στη σύγχρονη μορφή της με αλγεβρικές διεργασίες. Επιρροή σε αυτήν την κατεύθυνση στην ανάπτυξη της CSP σε άλγεβρα διεργασιών υπήρξε η δουλειά του Robin Milner στο Λογισμό των Επικοινωνούντων Συστημάτων (Calculus of Communicating Systems, CCS), αλλά και αντίστροφα. Η θεωρητική έκδοση της CSP παρουσιάστηκε αρχικά σε ένα άρθρο το 1984 από τους Brookes, Χόαρ, και Roscoe, και αργότερα στο βιβλίο Communicating Sequential Processes του Χόαρ, το οποίο δημοσιεύτηκε το 1985. Το Σεπτέμβριο του 2006, αυτό το βιβλίο εξακολουθούσε να είναι το τρίτο όσον αφορά επιστημονικές αναφορές άλλων προς αυτό στην επιστήμη υπολογιστών σύμφωνα με τη σελίδα Citeseer (που δεν είναι όμως πλήρως αξιόπιστη, λόγω της φύσης του δείγματός της). Η θεωρία της CSP έχει υποστεί αρκετές μικροαλλαγές από τη δημοσίευση του βιβλίου του Χόαρ. Οι περισσότερες από αυτές προέκυψαν από την εμφάνιση αυτόματων εργαλείων για την ανάλυση διεργασιών της CSP και για επαλήθευση ιδιοτήτων τους. Το The Theory and Practice of Concurrency του Roscoe περιγράφει αυτήν τη νεότερη έκδοση της CSP.

Εφαρμογές

Μια πρώτη σημαντική εφαρμογή της CSP ήταν για την προδιαγραφή (specification) και την επαλήθευση (verification) στοιχείων του Transputer INMOS T9000, ενός πολύπλοκου υπερβαθμωτού επεξεργαστή με διοχέτευση, που είχε σχεδιαστεί για να υποστηρίζει πολυπεξεργασία μεγάλης κλίμακας. Η CSP χρησιμοποιήθηκε για την επαλήθευση της ορθότητας, τόσο της διοχέτευσης του επεξεργαστή, όσο και του Επεξεργαστή Εικονικού Καναλιού (Virtual Channel Processor) που χειριζόταν τις επικοινωνίες εκτός τσιπ για τον επεξεργαστή.

Η εφαρμογή της CSP στη βιομηχανία για τη σχεδίαση λογισμικού συνήθως εστιάζει σε ανθεκτικά συστήματα και σε συστήματα με σοβαρές απαιτήσεις ασφάλειας (safety-critical). Για παράδειγμα, το Ινστιτούτο Ασφαλών Συστημάτων της Βρέμης και η Daimler-Benz Aerospace μοντελοποίησαν σε CSP ένα σύστημα διαχείρισης σφαλμάτων και μια διεπαφή αεροναυπηγικής (avionics interface), που αποτελούνταν συνολικά από 23,000 γραμμές κώδικα, για χρήση στο Διεθνή Διαστημικό Σταθμό, και ανέλυσαν το μοντέλο για να βεβαιωθεί ότι δεν υπήρχαν αδιέξοδα (deadlocks) και ζωντανά αδιέξοδα (livelocks). Η διαδικασία μοντελοποίησης και ανάλυσης εμφάνισε κάποια λάθη που θα ήταν δύσκολο να εντοπιστούν μόνο από δοκιμές. Επίσης, η Praxis High Integrity Systems εφάρμοσε μοντελοποίηση και ανάλυση σε CSP κατά την ανάπτυξη λογισμικού (περίπου 100,000 γραμμές κώδικα) για μια Αρχή Πιστοποίησης για ασφαλείς έξυπνες κάρτες, για να βεβαιωθεί ότι η σχεδίαση ήταν ασφαλής και δεν περιείχε αδιέξοδα. Σύμφωνα με την Praxis, το σύστημα που προέκυψε είναι πολύ λιγότερα λάθη από παρόμοια συστήματα.

Επειδή η CSP προσφέρεται για μοντελοποίηση και ανάλυση συστημάτων με πολύπλοκες ανταλλαγές μηνυμάτων, έχει εφαρμοστεί στην επαλήθευση πρωτοκόλλων επικοινωνιών και ασφάλειας. Ένα γνωστό παράδειγμα τέτοιων εφαρμογών είναι η χρήση από τον Lowe της CSP και του ελεγκτή FDR (refinement-checker) για την εύρεση μιας άγνωστης μέχρι τότε επίθεσης στο πρωτόκολλο ταυτοποίησης δημόσιου κλειδιού Needham-Schroeder και η ανάπτυξη στη συνέχεια ενός διορθωμένου πρωτοκόλλου που δεν επηρεαζόταν από την επίθεση.

Περιγραφή

Όπως φαίνεται από το όνομά της, η CSP επιτρέπει την περιγραφή συστημάτων που αποτελούνται από διεργασίες που λειτουργούν ανεξάρτητα και αλληλεπιδρούν μεταξύ τους μόνο μέσω περάσματος μηνυμάτων (message passing). Η λέξη "Ακολουθιακές" ("Sequential") του τίτλου δεν είναι πια εντελώς σωστή, επειδή η σύγχρονη CSP επιτρέπει σε διεργασίες να ορίζονται είτε σαν ακολουθιακές διεργασίες, είτε σαν παράλληλη σύνθεση από πιο βασικές διεργασίες. Οι σχέσεις μεταξύ διάφορων διεργασιών και ο τρόπος που αυτές επικοινωνούν με το περιβάλλον τους, περιγράφονται από διάφορους τελεστές αλγεβρικών διεργασιών. Με βάση αυτήν την αλγεβρική προσέγγιση, πολύπλοκες περιγραφές διεργασιών μπορούν να κατασκευαστούν από λίγα βασικά στοιχεία.

Βασικά στοιχεία

Η CSP έχει δύο κατηγορίες βασικών στοιχείων (primitives) στην άλγεβρα διεργασιών της:

Γεγονότα (Events)

Τα γεγονότα αναπαριστούν την επικοινωνία ή την αλληλεπίδραση. Θεωρούνται αδιαίρετα και στιγμιαία. Μπορούν να είναι ατομικά ονόματα (όπως το ${\mathit {on}}$ και το ${\mathit {off}}$), σύνθετα ονόματα (όπως το $valve.open$ και το $valve.close$) ή γεγονότα εισόδου/εξόδου (για παράδειγμα, το $mouse?xy$ ή το $screen!bitmap$).

Βασικές διεργασίες (Primitive processes)

Οι βασικές διεργασίες αναπαριστούν θεμελιώδεις συμπεριφορές: παραδείγματα είναι η ${\mathit {STOP}}$ (η διεργασία που δεν επικοινωνεί, γνωστή και σαν αδιέξοδο ή deadlock) και η ${\mathit {SKIP}}$ (που αναπαριστά τον τερματισμό με επιτυχία).

Αλγεβρικοί τελεστές

Η CSP έχει αρκετούς αλγεβρικούς τελεστές. Οι βασικότεροι είναι:

Πρόθεμα (Prefix)

Συνδυάζει ένα γεγονός και μια διεργασία για να παράγει μια νέα διεργασία. Για παράδειγμα, η

$a\rightarrow P$

είναι η διεργασία που επιθυμεί να επικοινωνήσει το ${\mathit {a}}$ στο περιβάλλον της, και μετά το ${\mathit {a}}$, συμπεριφέρεται όπως η διεργασία ${\mathit {P}}$.

Ντετερμινιστική Επιλογή (Deterministic Choice)

Ο τελεστής ντετερμινιστικής (ή εξωτερικής) επιλογής ορίζει τη μελλοντική εξέλιξη μιας διεργασίας σαν την επιλογή μεταξύ δύο διεργασιών-στοιχείων, και επιτρέπει στο περιβάλλον να επιλέξει επικοινωνόντας ένα αρχικό γεγονός για μια από τις διεργασίας. Για παράδειγμα, η

$\left(a\rightarrow P\right)\Box \left(b\rightarrow Q\right)$

είναι η διεργασία που επιθυμεί να επικοινωνήσει τα αρχικά γεγονότα ${\mathit {a}}$ και ${\mathit {b}}$, και στη συνέχεια συμπεριφέρεται είτε σαν την ${\mathit {P}}$ είτε σαν την ${\mathit {Q}}$, ανάλογα με το ποιο αρχικό γεγονός επέλεξε να επικοινωνήσει το περιβάλλον. Αν και το ${\mathit {a}}$ και το ${\mathit {b}}$ σταλούν ταυτόχρονα, η επιλογή γίνεται μη ντετερμινιστικά.

Μη ντετερμινιστική Επιλογή (Nondeterministic Choice)

Ο τελεστής μη ντετερμινιστικής (ή εσωτερικής) επιλογής ορίζει τη μελλοντική εξέλιξη μιας διεργασίας σαν την επιλογή μεταξύ δύο διεργασιών-στοιχείων αλλά δεν επιτρέπει στο περιβάλλον να ελέγξει ποια από αυτές θα επιλεγεί. Για παράδειγμα, η

$\left(a\rightarrow P\right)\sqcap \left(b\rightarrow Q\right)$

μπορεί να συμπεριφερθεί είτε σαν την $\left(a\rightarrow P\right)$ είτε σαν τη $\left(b\rightarrow Q\right)$. Μπορεί να αρνηθεί να δεχτεί το ${\mathit {a}}$ ή το ${\mathit {b}}$, και υποχρεώνεται σε επικοινωνία μόνο όταν το περιβάλλον προσφέρει και το ${\mathit {a}}$ και το ${\mathit {b}}$. Ο μη ντετερμινισμός μπορεί να εμφανιστεί σε μια (ονομαστικά) ντετερμινιστική επιλογή αν τα αρχικά γεγονότα και στις δύο πλευρές είναι ίδια. Επομένως, για παράδειγμα, η

$\left(a\rightarrow a\rightarrow STOP\right)\Box \left(a\rightarrow b\rightarrow STOP\right)$

είναι ισοδυύναμη με την

$a\rightarrow \left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)$

Διαστρωμάτωση (Interleaving)

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

$P\;\vert \vert \vert \;Q$

συμπεριφέρεται σαν ${\mathit {P}}$ και σαν ${\mathit {Q}}$ ταυτόχρονα. Τα γεγονότα και από τις δύο διεργασίες διαστρωματώνονται αυθαίρετα στο χρόνο.

Παράλληλη Διεπαφή (Interface Parallel)

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

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

απαιτεί η ${\mathit {P}}$ και η ${\mathit {Q}}$ πρέπει να μπορούν να εκτελέσουν το γεγονός ${\mathit {a}}$ πριν να συμβεί εκείνο το γεγονός. Επομένως, για παράδειγμα, η διαδικασία

$\left(a\rightarrow P\right)\left\vert \left[\left\{a\right\}\right]\right\vert \left(a\rightarrow Q\right)$

μπορεί να συμμετάσχει στο γεγονός ${\mathit {a}}$, και να γίνει η διεργασία

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

ενώ η

$\left(a\rightarrow P\right)\left\vert \left[\left\{a,b\right\}\right]\right\vert \left(b\rightarrow Q\right)$

απλά θα φτάσει σε αδιέξοδο.

Κρύψιμο (Hiding)

Ο τελεστής αυτός παρέχει αφαίρεση πάνω στις διεργασίες, κάνοντας κάποια γεγονότα μη παρατηρήσιμα. Ένα απλό παράδειγμα είναι η

$\left(a\rightarrow P\right)\setminus \left\{a\right\}$

η οποία, θεωρώντας ότι το γεγονός ${\mathit {a}}$ δεν εμφανίζεται στην ${\mathit {P}}$, απλά ανάγεται στην

${\mathit {P}}$

Παραδείγματα

Ένα από τα κλασικά παραδείγματα της CSP είναι μια αφηρημένη αναπαράσταση του μηχανήματος πώλησης σοκολάτας, και η αλληλεπίδρασή του με ένα άτομο που θέλει να αγοράσει μια σοκολάτα. Το μηχάνημα μπορεί να εκτελέσει δύο γεγονότα, “coin” και “choc”, που αναπαριστούν την εισαγωγή χρημάτων και την εμφάνιση μιας σοκολάτας αντίστοιχα. Μια μηανή που απαιτεί πληρωμή πριν δώσει μια σοκολάτα μπορεί να γραφεί σαν:

${\textit {VendingMachine}}={\textit {coin}}\rightarrow {\textit {choc}}\rightarrow {\textit {STOP}}$

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

${\textit {Person}}=({\textit {coin}}\rightarrow {\textit {STOP}})\Box ({\textit {card}}\rightarrow {\textit {STOP}})$

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

${\textit {VendingMachine}}\left\vert \left[\left\{{\textit {coin}},{\textit {card}}\right\}\right]\right\vert {\textit {Person}}\equiv {\textit {coin}}\rightarrow {\textit {choc}}\rightarrow {\textit {STOP}}$

ενώ αν ο συγχρονισμός είναι απαραίτητος μόνο στο “coin”, θα προέκυπτε

${\textit {VendingMachine}}\left\vert \left[\left\{{\textit {coin}}\right\}\right]\right\vert {\textit {Person}}\equiv \left({\textit {coin}}\rightarrow {\textit {choc}}\rightarrow {\textit {STOP}}\right)\Box \left({\textit {card}}\rightarrow {\textit {STOP}}\right)$

Αν γίνει αφαίρεση πάνω στην τελευταία σύνθετη διεργασία, κρύβωντας τα γεγονότα “coin” και “card” events, δηλ.

$\left(\left({\textit {coin}}\rightarrow {\textit {choc}}\rightarrow {\textit {STO}}P\right)\Box \left({\textit {card}}\rightarrow {\textit {STOP}}\right)\right)\setminus \left\{{\textit {coin}},card\right\}$

προκύπτει η μη ντετερμινιστική διεργασία

$\left({\textit {choc}}\rightarrow {\textit {STOP}}\right)\sqcap {\textit {STOP}}$

Αυτή είναι μια διεργασία που είτε δίνει ένα γεγονός “choc” και μετά σταματά, είτε απλά σταματά. Με άλλα λόγια, αν η αφαίρεση θεωρηθεί σαν μια εξωτερική άποψη του συστήματος (π.χ. από κάποιον που δε βλέπει την επιλογή που έκανε το άτομο που χρησιμοποιεί το μηχάνημα), εισάγεται μη ντετερμινισμός (nondeterminism).

Τυπικός ορισμός

Σύνταξη

Η σύνταξη της CSP ορίζει τους “έγκυρους” τρόπους με τους οποίους μπορούν να συνδυαστούν διεργασίες και γεγονότα. Έστω ότι το ${\mathit {e}}$ είναι γεγονός και ${\mathit {X}}$ ένα σύνολο από γεγονότα. Τότε η βασική σύνταξη της CSP μπορεί να οριστεί σαν:

${\begin{matrix}Proc&::=&{\textit {STOP}}&\;\\&|&{\textit {SKIP}}&\;\\&|&e\rightarrow {\textit {Proc}}&({\textit {prefixing}})\\&|&{\textit {Proc}}\;\Box \;{\textit {Proc}}&({\textit {external}}\;{\textit {choice}})\\&|&{\textit {Proc}}\;\sqcap \;{\textit {Proc}}&({\textit {nondeterministic}}\;{\textit {choice}})\\&|&{\textit {Proc}}\;\vert \vert \vert \;{\textit {Proc}}&({\textit {interleaving}})\\&|&{\textit {Proc}}\;|[\{X\}]|\;{\textit {Proc}}&({\textit {interface}}\;{\textit {parallel}})\\&|&{\textit {Proc}}\setminus X&({\textit {hiding}})\\&|&{\textit {Proc}};{\textit {Proc}}&({\textit {sequential}}\;{\textit {composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{\textit {Proc}}\;\mathrm {else} \;Proc&({\textit {boolean}}\;{\textit {conditional}})\\&|&{\textit {Proc}}\;\triangleright \;{\textit {Proc}}&({\textit {timeout}})\\&|&{\textit {Proc}}\;\triangle \;{\textit {Proc}}&({\textit {interrupt}})\end{matrix}}$

Για λόγους συντομίας, η παραπάνω σύνταξη παραλείπει τη διεργασία $\mathbf {div}$, η οποία αναπαριστά την εκτέλεση που αποκλίνει (divergence), καθώς επίσης και διάφορους τελεστές όπως η αλφαβητικά παράλληλη (alphabetized parallel), η διοχετευση (piping), και η δεικτοδοτημένη (indexed) επιλογή.

Τυπική σημασιολογία

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

Δηλωτική σημασιολογία

Τα τρία σημαντικότερα δηλωτικά μοντέλα της CSP είναι το μοντέλο ιχνών (traces model), το μοντέλο σταθερών αποτυχιών (stable failures model), και το μοντέλο αποτυχίες/αποκλίσεις (failures/divergences model). Η δηλωτική σημασιολογία της CSP προκύπτει από σημασιολογικές αντιστοιχίες από εκφράσεις διεργασιών σε κάθε ένα από τα τρία αυτά μοντέλα.

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

• $traces\left(STOP\right)=\left\{\langle \rangle \right\}$ επειδή η $STOP$ δεν προκαλεί κάποια γεγονότα
• $traces\left(a\rightarrow b\rightarrow STOP\right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ επειδή η διεργασία $(a\rightarrow b\rightarrow STOP)$ μπορεί να παρατηρηθεί ότι δεν έχει προκαλέσει κάποιο γεγονός, το γεγονός $a$, ή τη διαδικασία γεγονότων $a$ που ακολουθείται από το $b$

Πιο τυπικά, η σημασία μιας διεργασίας $P$ στο μοντέλο ιχνών ορίζεται σαν $traces\left(P\right)\subseteq \Sigma ^{\ast }$ ώστε:

1. $\langle \rangle \in traces\left(P\right)$ (δηλ. η $traces\left(P\right)$ περιέχει την κοινή ακολουθία)
2. $s_{1}\smallfrown s_{2}\in traces\left(P\right)\implies s_{1}\in traces\left(P\right)$ (δηλ. η $traces\left(P\right)$ είναι κλειστή ως προς το πρόθεμα) όπου το $\Sigma ^{\ast }$ είναι το σύνολο όλως των πιθανών πεπερασμένων ακολουθιών γεγονότων.

Το μοντέλο σταθερών αποτυχιών επεκτείνει το μοντέλο ιχνών με σύνολα απόρριψης (refusal sets), που είναι σύνολοα από γεγονότα $X\subseteq \Sigma$, τα οποία μια διεργασία μπορεί να αρνηθεί να εκτελέσει. Μια αποτυχία (failure) είναι ένα ζεύγος $\left(s,X\right)$, που αποτελείται από ένα ίχνος $s$ και ένα σύνολο απόρριψης $X$ που δείχνει ποια γεγονότα μπορεί να απορρίψει μια διεργασία όταν έχει εκτελέσει το ίχνος $s$. Στο μοντέλο σταθερών αποτυχιών, η παρατηρούμενη συμπεριφορά μιας διεργασίας περιγράφεται από το ζεύγος $\left(traces\left(P\right),failures\left(P\right)\right)$. Για παράδειγμα,

• $failures\left(\left(a\rightarrow STOP\right)\Box \left(b\rightarrow STOP\right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$
• $failures\left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$

Το μοντέλο αποτυχίες/αποκλίσεις επεκτείνει το μοντέλο αποτυχιών ώστε να χειρίζεται εκτελέσεις που αποκλίνουν. Μια διεργασία σε αυτό το μοντέλο είναι ένα ζεύγος $\left(failures_{\perp }\left(P\right),divergences\left(P\right)\right)$ όπου το $divergences\left(P\right)$ ορίζεται σαν το σύνολο όλων των ιχνών που μπορούν να οδηγήσουν σε συμπεριφορά απόκλισης και $failures_{\perp }\left(P\right)=failures\left(P\right)\cup \left\{\left(s,X\right)\vert s\in divergences\left(P\right)\right\}$.

Εργαλεία

Με την πάροδο του χρόνου, έχουν εμφανιστεί αρκετά εργαλεία για την ανάλυση και την κατανόηση συστημάτων που περιγράφονται σε CSP. Αρχικές υλοποιήσεις εργαλείων χρησιμοποίησαν μια ποικιλία από τρόπους σύνταξης CSP που να είναι ευανάγνωστοι από τους υπολογιστές, κάνοντας ασύμβατα τα αρχεία εισόδου των διάφορων εργαλείων. Τα περισσότερα εργαλεία CSP πια έχουν καταλήξει σε μια διάλεκτο της CSP που είναι κατάλληλη για εισαγωγή σε υπολογιστή, η οποία οφείλεται στον Bryan Scattergood, και κάποιες φορές αποκαλείται CSP_M. Η διάλεκτος CSP_M της CSP έχει τυπικά ορισμένη λειτουργική σημασιολογία, η οποία περιλαμβάνει μια ενσωματωμένη γλώσσα συναρτησιακού προγραμματισμού.

Το γνωστότερο εργαλείο CSP είναι μάλλον το Failures/Divergence Refinement 2 (FDR2), το οποίο είναι εμπορικό προϊόν που αναπτύχθηκε από τη Formal Systems (Europe) Ltd. Το FDR2 συχνά περιγράφεται σαν ελεγκτής μοντέλων (model checker), αλλά τεχνικά είναι ελεγκτής εκλέπτυνσης (refinement checker), γιατί μετατρέπει δύο εκφράσεις διεργασιών CSP σε συστήματα μεταβάσεων με ετικέτες (Labelled Transition System ή LTSs), και στη συνέχεια βρίσκει αν η μια διεργασία είναι εκλέπτυνση της άλλης σε κάποιο καθορισμένο σημασιολογικό μοντέλο (ίχνη, αποτυχίες, αποτυχίες/αποκλίσεις). Το FDR2 εφαρμόζει διάφορους αλγόριθμους συμπίεσης του χώρου καταστάσεων στα LTSs των διεργασιών, ώστε να μειώσει το μέγεθος του χώρου καταστάσεων που πρέπει να εξερευνηθεί κατά τον έλεγχο εκλέπτυνσης.

Το Adelaide Refinement Checker (ARC) είναι ελεγκτής εκλέπτυνσης CSP που αναπτύχθηκε από το Formal Modelling and Verification Group του Πανεπιστημίου της Αδελαΐδας. Η διαφορά του ARC από το FDR2 είναι ότι αναπαριστά εσωτερικά τις διεργασίες CSP σαν Διατεταγμένα Διαγράμματα Δυαδικής Απόφασης (Ordered Binary Decision Diagram ή OBDDs), που αντιμετωπίζουν το πρόβλημα έκρηξης του χώρου καταστάσεων των ρητών αναπαραστάσεων κάθε LTS χωρίς να απαιτούν αλγόριθμους συμπίεσης του χώρου καταστάσεων όπως το FDR2.

Το εγχείρημα ProB, που βρίσκεται στο Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, δημιουργήθηκε αρχικά για την υποστήριξη της ανάλυσης προδιαγραφών που κατασκευάστηκαν με τη μέθοδο B (B method). Περιλαμβάνει όμως υποστήριξη για την ανάλυση διεργασιών σε CSP, μέσω ελέγχου εκλέπτυνσης και ελέγχου μοντέλων γραμμικής χρονικής λογικής (Linear Temporal Logic, LTL). Το ProB μπορεί επίσης να χρησιμοποιηθεί για την επαλήθευση ιδιοτήτων συνδυασμένων προδιαγραφών σε CSP και B.

Το Process Analysis Toolkit (PAT) είναι εργαλείο ανάλυσης CSP που αναπτύχθηκε στη Σχολή Πληροφορικής του Εθνικού Πανεπιστημίου της Σιγκαπούρης. Το PAT μπορεί να εκτελέσει έλεγχο εκλέπτυνσης, έλεγχο μοντέλων LTL, και προσομοίωση διεργασιών σε CSP και Χρονισμένη CSP (Timed CSP). Η γλώσσα διεργασιών του PAT επεκτείνει τη CSP με υποστήριξη για τροποποιήσιμες (mutable) κοινόχρηστες μεταβλητές, ασύγχρονο πέρασμα μηνυμάτων (asynchronous message passing), και κάποιες δομές δικαιοσύνης (fairness) και ποσοτικού χρόνου διεργασιών όπως η deadline και η waituntil. Η βασική σχεδιαστική αρχή της γλώσσας διεργασιών του PAT είναι ο συνδυασμός μιας γλώσσας προδιαγραφών υψηλού επιπέδου με διαδικαστικά προγράμματα (π.χ. ένα γεγονός στο PAT μπορεί να είναι ένα ακολουθιακό πρόγραμμα ή ακόμα και μια εξωτερική κλήση βιβλιοθήκης της C#) για μεγαλύτερη εκφραστικότητα. Οι τροποποιήσιμες κοινόχρηστες μεταβλητές και τα ασύγχρονα κανάλια (asynchronous channels) παρέχουν μια βολική σύνταξη για γνωστές μορφές μοντελοποίησης διεργασιών χρησιμοποιώντας κλασική CSP. Η σύνταξη του PAT μοιάζει πολύ με αυτήν της CSP_M. Οι βασικές διαφορές μεταξύ της σύνταξης του PAT και της κλασικής CSP_M είναι η χρήση ελληνικών ερωτηματικών για τον τερματισμό εκφράσεων διεργασιών, η βολική σύνταξη για μεταβλητές και αναθέσεις, και η χρήση μιας λίγο διαφορετικής σύνταξης για την εσωτερική επιλογή και την παράλληλη σύνθεση.

Το CSPsim είναι ένας οκνηρός (lazy) προσομοιωτής. Αν και δεν είναι ελεγκτής μοντέλων της CSP, είναι χρήσιμο για την εξερεύνηση πολύ μεγάλων (ακόμα και άπειρων σε μέγεθος) συστημάτων.

Σχετικοί φορμαλισμοί

Υπάρχουν πολλές άλλες γλώσσες προδιαγραφών και φορμαλισμοί που έχουν προκύψει (ή έχουν εμπνευστεί) από την κλασική CSP (χωρίς χαρακτηριστικά χρόνου), όπως τα εξής:

• Χρονισμένη CSP (Timed CSP) - περιλαμβάνει πληροφορία χρονισμού για την ανάλυση συστημάτων πραγματικού χρόνου (real-time systems)
• Receptive Process Theory - μια ειδική έκδοση της CSP που υποθέτει ασύγχρονη (που δεν μπλοκάρει, nonblocking) λειτουργία αποστολής
• CSPP
• HCSP
• Wright - μια γλώσσα περιγραφής αρχιτεκτονικής
• TCOZ - ενσωματώνει Timed CSP και Object Z
• Circus - ενσωματώνει CSP και Z (με βάση τα Unifying Theories of Programming)
• CspCASL - επέκταση της CASL που περιέχει τη CSP

Σύγκριση με το Μοντέλο Actor

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

• οι διεργασίες CSP είναι ανώνυμες ενώ οι actors έχουν ταυτότητες.

• η ανταλλαγή μηνυμάτων στη CSP απαιτεί σε βασικό επίπεδο ένα ραντεβού (rendezvous) μεταξύ των διεργασιών που στέλνουν και λαμβάνουν κάποιο μήνυμα, δηλαδή ο αποστολέας δε μπορεί να στείλει κάποιο μήνημα μέχρι ο παραλήπτης να είναι έτοιμος να το δεχτεί. Αντίθετα, η ανταλλαγή μηνυμάτων σε συστήματος με actors είναι βασικά ασύγχρονη, δηλαδή η αποστολή μηνυμάτων και η αποδοχή τους δε χρειάζεται να συμβαίνουν την ίδια στιγμή, και οι αποστολείς μπορούν να στέλνουν μηνύματα πριν οι παραλήπτες να είναι έτοιμοι να τα λάβουν. Αυτές οι προσεγγίσεις μπορούν να θεωρηθούν δύο όψεις του ίδιου θέματος, με την έννοια ότι τα συστήματα που βασίζονται στα ραντεβού μπορούν να χρησιμοποιηθούν για την κατασκευή επικοινωνιών με ενδιάμεση μνήμη (buffered communications) που συμπεριφέρονται σαν συστήματα ασύγχρονου περάσματος μηνυμάτων, ενώ τα ασύγχρονα συστήματα μπορούν να χρησιμποιηθούν για την κατασκευή επικοινωνιών σε στυλ ραντεβού χρησιμοποιώντας ένα πρωτόκολλο μηνύματος/επιβεβαίωσης για το συγχρονισμό αποστολέων και παραληπτών.

• η CSP χρησιμοποιεί ρητά κανάλια για την αποστολή μηνυμάτων, ενώ τα συστήματα με actors στέλνουν μηνύματα σε actors-προορισμούς με όνομα. Αυτές οι προσεγγίσεις μπορούν επίσης να θεωρηθούν διαφορετικές όψεις του ίδιου θέματος, με την έννοια ότι οι διεργασίες που δέχονται από ένα μοναδικό κανάλι πρακτικά έχουν όνομα που αντιστοιχεί σε αυτό το κανάλι, ενώ η σύνδεση με τα ονόματα μεταξύ actors μπορεί να αγνοηθεί με την κατασκευή actors που συμπεριφέρονται σαν κανάλια.

Δείτε επίσης

• Λογισμός των Επικοινωνούντων Συστημάτων

Γλώσσες

• occam - η πρώτη γλώσσα που υλοποίησε ένα μοντέλο της CSP.
• JCSP - μίξη ιδεών από τη CSP και την occam σε ένα API για υποστήριξη νημάτων στη Java.
• Limbo - μια γλώσσα που υλοποιεί ταυτοχρονισμό στο λειτουργικό σύστημα Inferno, με στυλ που μοιάζει με τη CSP.
• Plan 9 from Bell Labs, Plan 9 from User Space - περιλαμβάνουν τη βιβλιοθήκη libthread που επιτρέπει τη χρήση ενός μοντέλου ταυτοχρονισμού τύπου CSP από τη C.
• VerilogCSP - ένα σύνολο μακροεντολών που προστίθενται στη Verilog HDL για την υποστήριξη επικοινωνιών καναλιού CSP.
• Go - μια γλώσσα προγραμματισμού από τη Google που συμπεριλαμβάνει ιδέες από τη CSP.
• Ada - υλοποιεί χαρακτηριστικά της CSP (όπως τα rendezvous).

Περαιτέρω διάβασμα

• Hoare, C. A. R. (2004) [1985]. Communicating Sequential Processes (PDF). Prentice Hall International. ISBN 0131532715. 
  • Το βιβλίο έχει ανανεωθεί και η νέα έκδοση είναι διαθέσιμη σαν αρχείο PDF από τη σελίδα Using CSP.

• Roscoe, A. W.· Bill Roscoe (1997). The Theory and Practice of Concurrency. Prentice Hall. ISBN 0-13-674409-5. 
  • Κάποιοι σύνδεσμοι που είναι σχετικοί με το βιβλίο είναι διαθέσιμοι εδώ. Το πλήρες κείμενο είναι διαθέσιμο σε μορφή αρχείου PS ή PDF από τη λίστα ακαδημαϊκών δημοσιεύσεων του Bill Roscoe.

Εξωτερικοί σύνδεσμοι

Γενικά

• Μια έκδοση PDF του βιβλίου του Χόαρ - Υπάρχουν περιορισμοί Copyright, δείτε το κείμενο της σελίδας. (Αγγλικά)
• The CSP Archive (Αγγλικά)

Εργαλεία ανάλυσης

• Formal Systems Europe, Ltd. - ανάπτυξη εργαλείων CSP, κάποια από τα οποία είναι ελεύθερα για χρήση. (Αγγλικά)
• ARC - Adelaide Refinement Checker, ένα εργαλείο επαλήθευσης CSP. (Αγγλικά)
• ProB - animator και ελεγκτής μοντέλων για τη μέθοδο B, υποστηρίζει refinement checking και έλεγχο μοντέλων LTL της CSP. (Αγγλικά)
• PAT - ελεγκτής μοντέλων, εξομοιωτής και refinement checker για τη CSP και διάφορες επεκτάσεις της (όπως οι κοινές μεταβλητές, οι πίνακες και η διακιοσύνη/fairness). (Αγγλικά)

Υποστήριξη από υλοποιήσεις

• CTJ - υλοποίηση της CSP σε Java με δικτυακό/κατανεμημένο μοντέλο. (Αγγλικά)
• C++CSP - υλοποίηση των ιδεών των CSP/occam/JCSP στη C++, μοιάζει με τη JCSP. (Αγγλικά)
• Jibu (γνωστή παλαιότερα και σαν CSP.NET) - υλοποίηση μιας βιβλιοθήκης σε στυλ CSP για το Microsoft .NET. (Αγγλικά)
• csp - βιβλιοθήκη της Common Lisp για τη χρήση ενός μοντέλου ταυτοχρονισμού τύπου CSP από την SBCL και άλλες πολυνηματικές υλοποιήσεις της Common Lisp. (Αγγλικά)
• «CHP: Communicating Haskell Processes. Process-Oriented Concurrency for Haskell». Αρχειοθετήθηκε από το πρωτότυπο στις 7 Ιουνίου 2011. Ανακτήθηκε στις 2 Μαΐου 2011.  - η CHP είναι βιβλιοθήκη της Haskell με ένα μοντέλο ταυτοχρονισμού τύπου CSP. (Αγγλικά)
• PyCSP - υλοποίηση της CSP σε Python με δικτυακό/κατανεμημένο μοντέλο. (Αγγλικά)
• jCSP - μια βιβλιοθήκη κλάσεων σε 100% Java που παρέχει ένα βασικό σύνολο της CSP, μαζί με αρκετές επεκτάσεις. (Αγγλικά)