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

Στην επιστήμη υπολογιστών, οι Επικοινωνούσες Ακολουθιακές Διεργασίες (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, που ορίζουν τη σημασία των εκφράσεων της CSP που είναι συντακτικά σωστές. Η θεωρία της CSP περιλαμβάνει κανόνες σε δηλωτική σημασιολογία, αλγεβρική σημασιολογία και λειτουργική σημασιολογία.

Εργαλεία

Με την πάροδο του χρόνου, έχουν εμφανιστεί αρκετά εργαλεία για την ανάλυση και την κατανόηση συστημάτων που περιγράφονται σε CSP. Αρχικές υλοποιήσεις εργαλείων χρησιμοποίησαν μια ποικιλία από τρόπους σύνταξης CSP που να είναι ευανάγνωστοι από τους υπολογιστές, κάνοντας ασύμβατα τα αρχεία εισόδου των διάφορων εργαλείων. Τα περισσότερα εργαλεία CSP πια έχουν καταλήξει σε μια διάλεκτο της CSP που είναι κατάλληλη για εισαγωγή σε υπολογιστή, η οποία οφείλεται στον Bryan Scattergood, και κάποιες φορές αποκαλείται CSPM. Η διάλεκτος CSPM της 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 μοιάζει πολύ με αυτήν της CSPM. Οι βασικές διαφορές μεταξύ της σύνταξης του PAT και της κλασικής CSPM είναι η χρήση ελληνικών ερωτηματικών για τον τερματισμό εκφράσεων διεργασιών, η βολική σύνταξη για μεταβλητές και αναθέσεις, και η χρήση μιας λίγο διαφορετικής σύνταξης για την εσωτερική επιλογή και την παράλληλη σύνθεση.
Το CSPsim είναι ένας οκνηρός (lazy) προσομοιωτής. Αν και δεν είναι ελεγκτής μοντέλων της CSP, είναι χρήσιμο για την εξερεύνηση πολύ μεγάλων (ακόμα και άπειρων σε μέγεθος) συστημάτων.