Η εργασία αυτή αφορά την μελέτη ταυτόχρονων (concurrent) αλγορίθμων σε δομές ευρετηρίου (δευτερεύουσας μνήμης) καθώς και τα μοντέλα ορθότητάς τους. Οι δομές ευρετηρίου που θα μελετήσουμε είναι τα Β-δέντρα κατάλληλα τροποποιημένα έτσι ώστε να μεγιστοποιείται η απόδοσή τους σε περιβάλλον ταυτοχρονισμού . Συγκεκριμένα εκτός από τους δείκτες του Β-δέντρου έxουν προστεθεί και δείκτες που ενώνουν τον έναν κόμβο με τον άλλον στο ίδιο επίπεδο του δέντρου σχηματίζοντας έτσι αλυσίδες. Στην αρχή θα δούμε μερικά φαινόμενα που ανακύπτουν όταν διάφορες διεργασίες εκτελούνται παράλληλα. Τα φαινόμενα αυτά έχουν την βάση τους στην πρόσβαση των διεργασιών σε κοινά δεδομένα από τα οποία εξαρτάται η εκτέλεσή τους. Θα δούμε πως μπορούμε να συγχρονίσουμε τις διεργασίες έτσι ώστε να μην προκύπτουν ανεπιθύμητα φαινόμενα Κατόπιν θα δούμε μερικούς βασικούς ταυτόχρονους αλγορίθμους που αντιπροσωπεύουν την λύση σε μερικά βασικά προβλήματα στην θεωρία ταυτοχρονισμού (concurrency) ,όπως τα consumer-producer problem κ.ά. Στην συνέχεια θα μετακινηθούμε στο πεδίο των αλγορίθμων για δομές ευρετηρίου. Η δομή ευρετηρίου που θα εξετάσουμε είναι το Β-δέντρο. Το δέντρο αυτό αποτελεί την κατεξοχήν επιλογή για τους σχεδιαστές βάσεων δεδομένων για την οργάνωση μεγάλου όγκου πληροφορίας στην δευτερεύουσα μονάδα μνήμης του συστήματος. Η ανάγκη για ταυτοχρονισμό σε αυτήν την δομή είναι επιβεβλημένη για την υποστήριξη πολυχρηστικών βάσεων δεδομένων και άλλων χρήσιμων εφαρμογών. Η αποδοτικότητα των αλγορίθμων μετριέται σε μέγεθος μνήμης για το οποίο έχουν αποκλειστική πρόσβαση έτσι ώστε να συγχρονίζονται μεταξύ τους οι αλγόριθμοι. Θα δούμε διάφορους αλγορίθμους καθώς και έναν δικό μας. Τέλος θα εξετάσουμε την έννοια της ορθότητας σε ταυτόχρονους αλγορίθμους. Θα δούμε διάφορα μοντέλα ορθότητας καθώς και διάφορα κριτήρια. Σε αυτά θα προσθέσουμε και ένα δικό μας κριτήριο το οποίο εξασφαλίζει απλότητα στον σχεδιασμό των αλγορίθμων πολύ μεγαλύτερη απότι προηγούμενα κριτήρια. Η συνεισφορά αυτής της εργασίας έγκειται στα εξής : 1) Στην ανάπτυξη ενός καινούριου αλγορίθμου ο οποίος επιτυγχάνει μεγαλύτερη απόδοση από προηγούμενους λόγω του νέου τρόπου συγχρονισμού που προτείνει. Συγκεριμένα ο συγχρονισμός επιτυγχάνεται όχι μέσω καθολικού αμοιβαίου αποκλεισμού (όπως μέχρι τώρα) αλλά κατά περίπτωση αμοιβαίου αποκλεισμού. 2) Στην ανάπτυξη ενός κριτηρίου ορθότητας που επιτρέπει την απλότητα και την σαφήνεια στην ανάπτυξη ιδιαίτερα αποδοτικών ταυτόχρονων αλγορίθμων. Το κριτήριο λαμβάνει υπόψη του τις καταστάσεις που μπορεί να προκύψουν σε ένα ορισμένο τμήμα κοινής μνήμης και προσφέρει έναν τρόπο να αποκλείσουμε την μετάβαση του συστήματος σε αυτές τις καταστάσεις. / This thesis is about the study of concurrent algorithms on index structures (secondary memory) as well as their correctness models. The index structures that we are going to study are properly modified B-trees to maximize efficiency in a concurrent anvironmemt. More specifically, apart from the ordinary pointers of the B-tree, pointers between nodes in the same level have been added, thus forming chains. In the beggining we will observe some phenomena that occur during concurent execution of processes. These phenomena occur when processes access simultaneously common data form which their exectution is depended. We will see how we can synchronise the processes so that these unwnated phenomena may not occur. After that, we will see some basic concurrent algorithms that represent the solution to some basic problems in concurrency theory such as consumer-producer problems etc. Then we will move to the filed of algorithms for index structures.The structure that we will study is the B tree which is very commonly used by databse designers to store large amounts of data in the secondary memory unit of the system. The need for supporting concurency for this data structure is evident form the fact that these trees are used in multi-user databases and other useful applications. The efficiency of these concurrent algortihms is measured by the size of the memory that each algortihms may have exclusive access in it. We will review various algortihms and present one of our own. At the end we will study the notion of correctness in concurrent algorithms.We will review various correctness models and present our own criterion that assures simplicity in design of alorithms much more than achieved by previous modles of correctness. The contribution of this thesis lies in the following 1)To the development of a new algorithm , more efficeint than previous ones due to the new way of synchronisation suggested.More specifically, synchronisation is achieved not through global mutual exclusion (which is the standard practice) but through relative mutual exclusion. 2) To the development of a new correctness criterion that allows simplicity and clarity in the desing of highly efficient concurrent algorithms . This criterion takes in consideration the intermediate states that can occur in an are of shared memory and offers a new way of blocking transition to specific sets of states.

In this thesis I show is that it is possible to give modular correctness proofs of interesting higher-order imperative programs using higher-order separation logic. To do this, I develop a model higher-order imperative programming language, and develop a program logic for it. I demonstrate the power of my program logic by verifying a series of examples. This includes both realistic patterns of higher-order imperative programming such as the subject-observer pattern, as well as examples demonstrating the use of higher-order logic to reason modularly about highly aliased data structures such as the union-find disjoint set algorithm.

No description available.