Τυπική ανάλυση και απόδοση αρχιτεκτονικών κατανεμημένων συναλλαγών:
Creators: name: Μεντής, Ανακρέοντας Π.
Publisher: name: Aristotle University of Thessaloniki
Year: 2012
Subjects: Τυπικές Μέθοδοι Ελέγχου Μοντέλων
Κατανεμημένες Συναλλαγές
Αρχιτεκτονική Λογισμικού
Επεξεργασία Συναλλαγών
Model Checking
Distributed Transactions
Software Architecture
Transaction Processing

description: Τα σύγχρονα πληροφοριακά συστήματα χαρακτηρίζονται από κατανεμημένη αρχιτεκτονική που συνήθως περιλαμβάνει πολλαπλούς εξυπηρετητές εφαρμογών. Ο σχεδιασμός των εφαρμογών βασίζεται στις θεμελιώδεις αρχές της αντικειμενοστρέφειας και η αρχιτεκτονική του συστήματος ταυτίζει το λογικό επιμερισμό της εφαρμογής σε διάφορα επίπεδα (π.χ εμφάνιση, λογική επεξεργασία, δεδομένα) με τη δομή του λογισμικό και του υλικού που το συναποτελούν. Οι συναλλαγές παρέχουν ένα κατάλληλο μηχανισμό για την οργάνωση κατανεμημένων εργασιών λόγω των ιδιοτήτων ACID (Ατομικότητα, Συνέπεια, Απομόνωση, Μονιμότητα) που παρέχουν. Ωστόσο, οι περιορισμοί που επιβάλλουν οι ACID ιδιότητες είναι πολύ δεσμευτικοί για κάποιες εφαρμογές. Σε περιβάλλον κινητού υπολογισμού ή σε εφαρμογές ιστού, λόγου χάρη, παρατηρούνται σχετικά μεγάλες καθυστερήσεις στην επικοινωνία ή συχνές απώλειες σύνδεσης που παρατείνουν το χρόνο εκτέλεσης των συναλλαγών και προσωρινά αποκλείουν άλλες ταυτόχρονες συναλλαγές από την πρόσβαση σε διαμοιρασμένους πόρους. Στα σύγχρονα μοντέλα συναλλαγών κάποιες από τις ACID ιδιότητες αντιμετωπίζονται λιγότερο αυστηρά ώστε να απαντηθούν οι προκλήσεις που παρουσιάζουν τα προαναφερθέντα περιβάλλοντα εκτέλεσης. Στη μνήμη συναλλαγών, λόγου χάρη, δεν παρέχονται οι εγγυήσεις συνέπειας και μονιμότητας. Τα νέα μοντέλα συναλλαγών, που συχνά αποκαλούνται προηγμένες συναλλαγές, ενδέχεται να μην ικανοποιούν κάποιες από τις επιδιωκόμενες ιδιότητες ορθότητας. Ο τυπικός ορισμός και τυπικός έλεγχος των ιδιοτήτων είναι θεμελιώδεις για την εγκυρότητα ενός μοντέλου συναλλαγών, αν και σήμερα η εγκυρότητα διασφαλίζεται κυρίως με προσεγγίσεις θεωρητικής απόδειξης παρά τις πρόσφατες εξελίξεις στο πεδίο του έλεγχου μοντέλων. Επιπλέον, μέχρι στιγμής δεν έχουμε δει τεχνικές αυτόματης σύνθεσης αποδεδειγμένα ορθής υλοποίησης από ελεγμένο μοντέλο συναλλαγών. Η απόδοση και η διαθεσιμότητα της επεξεργασίας συναλλαγών εξαρτώνται από την αρχιτεκτονική σχεδίαση που υιοθετείται για ένα μοντέλο συναλλαγών. Οι σχεδιαστικές αποφάσεις έχουν μετρήσιμες επιδράσεις στην απόδοση και τη διαθεσιμότητα του συστήματος επεξεργασίας συναλλαγών. Τα σημεία αντιστάθμισης που υπάρχουν μεταξύ των σχεδιαστικών παραγόντων της αρχιτεκτονικής επηρεάζουν την ποιότητα της επεξεργασίας συναλλαγών με σύνθετο τρόπο. Για την αντιμετώπιση των παραπάνω προβλημάτων προτείνουμε μια προσέγγιση καθοδηγούμενη από μοντέλα, για την αρχιτεκτονική συστημάτων συναλλαγών με δύο βασικές συνεισφορές. Πρώτα, παρέχουμε μία συστηματική διαδικασία για τον έλεγχο μοντέλου συναλλαγών και την αυτόματη σύνθεση εγγυημένα σωστής υλοποίησης . Τα μοντέλα ορίζονται με αυτόματα που αντιστοιχούν στις οντότητες που αλληλεπιδρούν και συγχρονίζονται μεταξύ τους ως προς ένα σύνολο μηνυμάτων. Ελέγχονται όλα τα πιθανά μονοπάτια εκτέλεσης των συγχρονισμένων αυτομάτων, για τυχόν παραβίαση ιδιοτήτων της συναλλαγής. Στη συνέχεια, επικεντρωνόμαστε σε μία προσέγγιση για τον εντοπισμό σημείων αντιστάθμισης στην αρχιτεκτονική και την εκτίμηση της επίδρασης των σχεδιαστικών αποφάσεων στην απόδοση και τη διαθεσιμότητα επεξεργασίας. Η προτεινόμενη μέθοδος εφαρμόζεται σε πειραματικά δεδομένα από προσομοίωση ή από πρωτότυπη υλοποίηση του συστήματος. Αν οι στόχοι απόδοσης και διαθεσιμότητας δεν ικανοποιούνται στα εξεταζόμενα σενάρια εκτέλεσης, η εφαρμογή της μεθόδου επαναλαμβάνεται μέχρι η αρχιτεκτονική να ικανοποιεί τους επιδιωκόμενους στόχους. Οι παραπάνω συνεισφορές εντάσσονται στο πλαίσιο μιας ολοκληρωμένης διαδικασίας ανάπτυξης συστημάτων επεξεργασίας συναλλαγών που πιστεύουμε ότι έχει την προοπτική να αντιμετωπίσει την εγγενή πολυπλοκότητα που χαρακτηρίζει την ανάπτυξη των συστημάτων αυτών.
description: Modern network centric information systems implement highly distributed architectures that usually include multiple application servers. Application design is mainly based on the fundamental object—oriented principles and the adopted architecture matches the logical decomposition of applications into several tiers such as presentation, logic and data to their software and hardware structuring. Transactions offer a convenient mechanism for structuring distributed workloads due to the ACID properties (Atomicity, Consistency, Isolation, Durability). For some applications however, the ACID properties are too restrictive. In mobile computing or in web applications for example, long intervals of non—responsiveness or frequent disconnections lead to long—running transactions that may block concurrently running transactions and render acquired resources unavailable to other processes. New transaction models often relax one of the ACID properties in order to cope with the challenges of the aforementioned execution environments. In transactional memory for example, consistency and durability guaranties are not provided. The new transaction models, often termed as advanced transactions, may not fulfill some intended properties. Formal specification and reasoning for transaction properties is essential for proving the validity of transaction models, but it has been limited to proof—theoretic approaches despite the recent progress in model checking. Moreover, we have not seen so far automated techniques that can derive a correct implementation from a valid transaction model. Performance and availability of transaction processing depends on the adopted architectural design for a given transaction model. Design decisions have measurable effects on availability and performance of transaction processing systems. Existing trade—offs among the design factors of an architecture affect the quality of the transaction processing service in a complex manner. In order to address the discussed problems, we introduce a model—driven architecture based approach with a two—fold contribution. First, we provide a systematic process for model checking a transaction model and automatically generate a correct implementation. Models are specified by state machines that represent interacting transactional entities synchronized on a set of events. Verification is performed by examining all possible execution paths of the synchronized state machines for property violations. Second, we elaborate on an approach for discovering architecture trade—offs and for evaluating the impact of design decisions on performance and availability. The proposed method is applicable on experimental data obtained by simulation or from a prototype implementation. If an architecture design fails to fulfill the performance and availability goals for the considered workloads, the method is iteratively applied towards modifying the initial architecture until the goals are achieved. The aforementioned contributions are part of a process for the development of transaction systems that we believe is capable to cope with the inherent complexity of distributed transaction processing.