Ταυτοχρονισμός: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
Μοντέλα |
μ Λογικές & Στην πράξη |
||
Γραμμή 31:
Κατά αυτόν τον τρόπο, το <tt>S</tt> μπορεί να χαρακτηριστεί μαθηματικά με βάση όλες τις πιθανές συμπεριφορές του.
=== Λογικές ===
Μπορούν να χρησιμοποιηθούν διάφοροι τύποι [[χρονική λογική|χρονικής λογικής]]<ref name="stirling">{{cite book|first=Colin|last=Roscoe|title=Modal and Temporal Properties of Processes|publisher=Springer|year=2001|isbn=0-387-98717-7}}</ref> για την ανάλυση ταυτόχρονων συστημάτων. Κάποιες από αυτές τις λογικές, όπως η [[γραμμική χρονική λογική]] και η [[λογική υπολογιστικού δένδρου]], επιτρέπουν βεβαιώσεις για ακολουθίες καταστάσεων, από τις οποίες μπορεί να περάσει ένα ταυτόχρονο σύστημα. Άλλες, όπως η λογική ενεργειών υπολογιστικού δένδρου (action computational tree logic), η [[λογική Hennessy-Milner]] και η [[Χρονική Λογική των Ενεργειών]] του [[Leslie Lamport]], κατασκευάζουν τις βεβαιώσεις τους από ακολουθίες ''ενεργειών'' (''actions''), που είναι οι αλλαγές κατάστασης. Η βασική εφαρμογή αυτών των λογικών είναι στη συγγραφή προδιαγραφών για ταυτόχρονα συστήματα.<ref name="cleaveland1996"/>
== Στην πράξη ==
Ο ταυτόχρονος προγραμματισμός περιλαμβάνει τις γλώσσες προγραμματισμού και τους αλγορίθμους που χρησιμοποιούνται στην υλοποίηση ταυτόχρονων συστημάτων. Ο ταυτόχρονος προγραμματισμός (concurrent programming) συχνά θεωρείται γενικότερος από τον παράλληλο προγραμματισμό (parallel programming) γιατί μπορεί να έχει αυθαίρετες και δυναμικές μορφές επικοινωνίας και αλληλεπίδρασης, ενώ τα παράλληλα συστήματα έχουν συνήθως προκαθορισμένο και καλά δομημένο τρόπο επικοινωνίας. Οι βασικοί σκοποί του ταυτόχρονου προγραμματισμού είναι η ''ορθότητα'' (''correctness''), η ''ταχύτητα'' (''performance'') και η ''ανθεκτικότητα'' (''robustness''). Ταυτόχρονα συστήματα όπως τα [[λειτουργικό σύστημα|λειτουργικά συστήματα]] και τα συστήματα διαχείρισης [[βάση δεδομένων|βάσεων δεδομένων]] γενικά σχεδιάζονται για να εκτελούνται χωρίς χρονικό όριο, με αυτόματη ανάκαμψη από σφάλματα, χωρίς να τερματίζουν απροσδόκητα (δείτε [[Έλεγχος ταυτοχρονισμού]]). Κάποια ταυτόχρονα συστήματα υλοποιούν μια μορφή διαφανούς (transparent) ταυτοχρονισμού, στον οποίο οι ταυτόχρονες υπολογιστικές οντότητες μπορούν να ανταγωνίζονται για έναν πόρο, αλλά οι λεπτομέρειες αυτού του ανταγωνισμού να μη φαίνονται στον προγραμματιστή.
Επειδή χρησιμοποιούν διαμοιραζόμενους πόρους, τα ταυτόχρονα συστήματα γενικά απαιτούν κάποια μορφή διαιτησίας (arbiter) στην υλοποίησή τους (συχνά το ίδιο το υλικό), για να ελέγχεται η πρόσβαση σε αυτούς τους πόρους. Η χρήση διαιτητών εισάγει την πιθανότητα απροσδιοριστίας, που έχει συνέπειες στην πράξη, ειδικά στην ορθότητα και στην ταχύτητα. Για παράδειγμα, η διαιτησία εισάγει μη-ντετερμινισμό χωρίς άνω όριο (unbounded nondeterminism), ο οποίος προκαλεί προβλήματα στον [[έλεγχος μοντέλων|έλεγχο μοντέλων]] γιατί προκύπτει έκρηξη του χώρυ των καταστάσεων, σε σημείο που τα μοντέλα μπορεί να έχουν ακόμα και άπειρο αριθμό καταστάσεων.
Κάποια μοντέλα ταυτόχρονου προγραμματισμού περιλαμβάνουν συν-διεργασίες (coprocesses) και ντετερμινιστικό ταυτοχρονισμό. Σε αυτά τα μοντέλα, τα νήματα του ελέγχου επιστρέφουν ρητά τις θυρίδες χρόνου που τους δίνονται, είτε στο σύστημα, είτε σε κάποια άλλη διεργασία.
== Δείτε επίσης ==
| |||