Skip to content

S
softlab-thesis
Commit f06a81eb authored by Achilles Benetopoulos's avatar Achilles Benetopoulos
Browse files
Options

WIP review comments

parent 91710a7b
Hide whitespace changes
Inline Side-by-side
Showing with 183 additions and 134 deletions
thesis.bib
View file @ f06a81eb
......@@ -211,3 +211,20 @@
url = {http://erlang.org/doc/reference_manual/typespec.html},
}
@inproceedings{damas-milner,
author = {Damas, Luis and Milner, Robin},
title = {Principal Type-schemes for Functional Programs},
booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '82},
year = {1982},
isbn = {0-89791-065-6},
location = {Albuquerque, New Mexico},
pages = {207--212},
numpages = {6},
url = {http://doi.acm.org/10.1145/582153.582176},
doi = {10.1145/582153.582176},
acmid = {582176},
publisher = {ACM},
address = {New York, NY, USA},
}
thesis.pdf
View file @ f06a81eb
No preview for this file type
thesis.tex
View file @ f06a81eb
......@@ -6,6 +6,7 @@
\usepackage{color}
\usepackage{caption}
\usepackage{array}
\usepackage{float}
\DeclareCaptionLabelFormat{algocaption}{Algorithm} % defines a new caption label as Algorithm x.y
\lstnewenvironment{algorithm}[1][] %defines the algorithm listing environment
......@@ -27,15 +28,17 @@
{}
\lstdefinestyle{erlangCodeStyle}{
basicstyle=\small,
captionpos=bottom,
basicstyle=\ttfamily,
captionpos=b,
tabsize=2,
showtabs=false,
numbers=left,
numbersep=5pt,
numberstyle=\tiny\color{gray},
showspaces=false,
showstringspaces=false
showstringspaces=false,
breaklines=true,
postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space}
}
\newcommand{\mychoose}[2]{\bigl({{#1}\atop#2}\bigr)}
......@@ -53,20 +56,20 @@
\title{Σχεδίαση και Υλοποίηση ενός Στατικού Συστήματος Τύπων για Επικοινωνούσες Διεργασίες}
\author{Αχιλλέας Μπενετόπουλος}
\date{Ιούλιος 2018}
\datedefense{17}{7}{2018}
\date{Οκτώβριος 2019}
\datedefense{21}{10}{2019}
\supervisor{Νικόλαος Σ. Παπασπύρου}
\supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}
\supervisor{Νικόλαος Παπασπύρου}
\supervisorpos{Καθηγητής Ε.Μ.Π.}
\committeeone{Νικόλαος Σ. Παπασπύρου}
\committeeonepos{Αν. Καθηγητής Ε.Μ.Π.}
\committeeone{Νικόλαος Παπασπύρου}
\committeeonepos{Καθηγητής Ε.Μ.Π.}
\committeetwo{Γεώργιος Στάμου}
\committeetwopos{Αν. Καθηγητής Ε.Μ.Π.}
\committeethree{Αριστείδης Παγουρτζής}
\committeethree{Κωνσταντίνος Σαγώνας}
\committeethreepos{Αν. Καθηγητής Ε.Μ.Π.}
\TRnumber{CSD-SW-TR-42-14} % number-year, ask nickie for the number
\TRnumber{CSD-SW-TR-8-19} % number-year, ask nickie for the number
\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}
\maketitle
......@@ -79,7 +82,7 @@
\setlength{\parskip}{1em}
Κινούμαστε όλο και περισσότερο προς κατανεμημένα προγραμματιστικά μοντέλα. Τα περισσότερα σύγχρονα συστήματα λογισμικού
είναι κατανεμημένα και ταυτόχρονα, που σημαίνει ότι αποτελούνται από διάφορα κομμάτια, το καθένα από τα οποία εκτελεί
ένα σύνολο από "εσωτερικές" σε αυτά λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
ένα σύνολο από ``εσωτερικές`` σε αυτά λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
υποσύνολο των υπολοίπων για να τις εκτελέσουν, λόγο διαφόρων εξαρτήσεων. Αυτό σημαίνει ότι η επικοινωνία μεταξύ των
κομματιών αυτών ανάγεται σε ένα κρίσιμο κομμάτι του συστήματος, και η ορθότητα της επικοινωνίας αυτής αποτελεί μια
απαραίτητη προϋπόθεση για την ορθότητα του όλου συστήματος.
......@@ -127,7 +130,18 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
%%% TODO
\begin{acknowledgementsgr}
Not a placeholder
Αρχικά θα ήθελα να ευχαριστήσω τους δύο συνεπιβλέποντες καθηγητές της παρούσας εργασίας, Νίκο Παπασπύρου και Κωστή
Σαγώνα, τόσο για τη βοήθεια και υποστήριξή τους κατά την εκπόνησή της, όσο και γιατί, με τα μαθήματα που δίδασκαν
αλλά και με το ενδιαφέρον που επιδείκνυαν, τροφοδότησαν και διαμόρφωσαν το δικό μου ενδιαφέρον στον τομέα.
Ακολούθως, θα ήθελα να ευχαριστήσω τον Σταύρο Αρώνη, για τη βοήθεια και τις συμβουλές του στο κομμάτι της
τροποποίησης του Dialyzer προκειμένου να εξυπηρετήσει τους σκοπούς της παρούσας εργασίας.
Επιπλέον, θα ήθελα να ευχαριστήσω τους συμφοιτητές και φίλους μου, καθώς η συναναστροφή μαζί τους μέσα στα χρόνια με
διαμόρφωσε και με έκανε τον άνθρωπο που είμαι σήμερα.
Τέλος, θα ήθελα να ευχαριστήσω την οικογένειά μου, για την αστείρευτη υποστήριξη και εμπιστοσύνη τους. Ξέρω ότι η
εκτίμησή μου δεν είναι πάντα εμφανής, αλλά είναι πάντα εκεί.
\end{acknowledgementsgr}
......@@ -147,7 +161,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
παραγωγής λογισμικού. Πολλά σύγχρονα συστήματα που πρέπει να ανταποκρίνονται σε υψηλούς φόρτους εργασίας με ισχυρές
απαιτήσεις ως προς την αξιοπιστία και τη διαθεσιμότητά τους
είναι κατανεμημένα και ταυτόχρονα, που σημαίνει ότι αποτελούνται από διάφορα κομμάτια, το καθένα από τα οποία εκτελεί
ένα σύνολο από "εσωτερικές" σε αυτό λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
ένα σύνολο από ``εσωτερικές`` σε αυτό λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
υποσύνολο των υπολοίπων για να τους παρέχουν πληροφορίες προκειμένου να φέρουν τη δουλειά τους εις πέρας με επιτυχία.
Αυτό σημαίνει ότι η επικοινωνία μεταξύ των
κομματιών αυτών ανάγεται σε ένα κρίσιμο κομμάτι του συστήματος, και ότι η ορθότητα της επικοινωνίας αυτής αποτελεί μια
......@@ -157,7 +171,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
\textit{πρωτόκολλα} επικοινωνίας, δηλαδή προσπαθούμε να προσδιορίσουμε τους τύπους των μηνυμάτων που ανταλλάσονται, πότε
κατα τη διάρκεια της επικοινωνίας εμφανίζονται αυτά τα μηνύματα, και ανάμεσα σε ποια κομμάτια του συστήματος
αυτά ανταλλάσονται. Συνεπώς, μπορούμε να εκφράσουμε την ορθότητα της επικοινωνίας μεταξύ των επιμέρους συστημάτων ως τη
\textit{συμμόρφωση} σε αυτό το πρωτόκολλο από τους συμμετέχοντες στην επικοινωνία. Οι τύποι συνεδριών μας επιτρέπουν να
\textit{συμμόρφωση} σε αυτά τα πρωτόκολλα από τους συμμετέχοντες στην επικοινωνία. Οι τύποι συνεδριών μας επιτρέπουν να
εκφράσουμε αυτά τα πρωτόκολλα επικοινωνίας, καθως και τις υλοποιήσεις τους από τα άκρα αυτών, με μια μορφή που
πηγάζει από τη θεωρία τύπων, και κατ'επέκταση να επαληθεύσουμε την ορθότητα της επικοινωνίας εφαρμόζοντας μεθόδους από
τον χώρο της θεωρίας τύπων.
......@@ -175,7 +189,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
Στη βιβλιογραφία υπάρχει ένας αριθμός από υλοποιήσεις μηχανισμών χρόνου εκτέλεσης για την παρακολούθηση της επικοινωνίας μεταξύ διεργασιών
σε γλώσσες με δυναμικό σύστημα τύπων όπως η Erlang \cite{spy, fowler-erlang}. Στη βάση τους, όλες χτίζουν
πάνω στη γλώσσα Scribble, η οποία είναι μια DSL για την περιγραφή πρωτοκόλλων
πάνω στη γλώσσα Scribble, η οποία είναι μια domain-specific language (DSL) για την περιγραφή πρωτοκόλλων
επικοινωνίας. Στη δική μας δουλειά, επιχειρούμε να κατασκευάσουμε ένα σύστημα στατικής ανάλυσης, το οποίο μπορεί να:
\begin{itemize}
\item Συμπεράνει τους τύπους συνεδριών των συναρτήσεων που αποτελούν ένα πρόγραμμα.
......@@ -188,7 +202,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
Στο κεφάλαιο 2 παρουσιάζουμε τη γλώσσα Erlang, και όλες τις πληροφορίες που είναι απαραίτητες για την κατανόηση του
τρόπου λειτουργίας του συστήματός μας. Εξηγούμε τι είναι η Erlang, και για ποιο λόγο ένα σύστημα τύπων συνεδρίας έχει
ιδιαίτερη αξία στα πλαίσια αυτής της γλώσσας. Καθώς ο συμπερασμός τύπων συνεδρίας βασίζεται ιδιαίτερα στο σύστημα τύπων της
γλώσσας, θα πραγματοποιήσουμε μια παρουσίαση αυτού, καθώς και του Dialyzer, του εργαλείου (μέρος του OTP) το οποίο
γλώσσας, θα πραγματοποιήσουμε μια παρουσίαση αυτού, καθώς και του Dialyzer, του εργαλείου (μέρος της υλοποίησης της γλώσσας) το οποίο
χρησιμοποιούμε για τον συμπερασμό των τύπων δεδομένων των προγραμμάτων που αναλύουμε.
Στο κεφάλαιο 3 πραγματοποιούμε μια παρουσίαση των συστημάτων τύπων και επιδράσεων (type and effect systems), τα οποία
......@@ -205,7 +219,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
πειράματά μας. Επιπλέον, εκθέτουμε μερικές ιδέες για μελλοντική δουλειά πάνω στο συγκεκριμένο αντικείμενο.
\setlength{\parskip}{0em}
\chapter{Το σύστημα Erlang/OTP}
\chapter{Η γλώσσα Erlang και το σύστημα OTP}
\section{Η γλώσσα προγραμματισμού Erlang}
Η Erlang είναι μια συναρτησιακή γλώσσα προγραμματισμού, η οποία σχεδιάσθηκε τη δεκαετία του 1980 στο Eργαστήριο Επιστήμης Υπολογιστών της Ericsson.
Αρχικά προοριζόταν για προγραμματισμό συστημάτων και εφαρμογών στον τομέα των τηλεπικοινωνιών, και κατα συνέπεια έπρεπε
......@@ -213,7 +227,7 @@ Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
παραλληλισμού, τα οποία επιδεικνύουν υψηλή ανοχή σε σφάλματα. Έκτοτε η χρήση της έχει διαδωθεί και σε βιομηχανίες
που μοιράζονται τις ίδιες λειτουργικές απαιτήσεις, όπως η τραπεζική, οι επικοινωνίες πραγματικού χρόνου (WhatsApp), κα.
To OTP είναι μια συλλογή εργαλείων, βιβλιοθηκών, middleware και αρχών σχεδιασμού για προγράμμτα Erlang. Είναι
To Open Telecom Platform (OTP) είναι μια συλλογή εργαλείων, βιβλιοθηκών, middleware και αρχών σχεδιασμού για προγράμμτα Erlang. Είναι
αναπόσπαστο κομμάτι της διανομής ελεύθερου κώδικα της Erlang. Μερικά από τα περιεχόμενά του είναι:
\begin{itemize}
\item Ένα σύστημα χρόνου εκτέλεσης (εικονική μηχανή), ο BEAM
......@@ -233,35 +247,34 @@ O μεταγλωττιστής δε μεταφράζει απευθείας το
Το κύριο κίνητρο πίσω από το σχεδιασμό της Core Erlang ήταν το να αναπτυχθεί μια αναπαράσταση προγραμμάτων Erlang που να
καθιστά εύκολη την ανάπτυξη εργαλείων που πρέπει να διατρέξουν και να επεξεργαστούν προγράμματα Erlang, όπως
αποσφαλματωτές, εργαλεία στατικής ανάλυσης κτλ. Κάτι τέτοιο δεν ήταν εφικτό απευθείας σε πηγαίο κώδικα Erlang, λόγω της
αποσφαλματωτές, εργαλεία στατικής ανάλυσης, κτλ. Κάτι τέτοιο δεν ήταν εφικτό απευθείας σε πηγαίο κώδικα Erlang, λόγω της
συντακτικής πολυπλοκότητάς της, και οι προσπάθειες απλούστευσης της γλώσσας οδηγήθηκαν σε αδιέξοδο.
Το OTP παρέχει τη δυνατότητα σε οποιοδήποτε πρόγραμμα Erlang να διαβάσει την Core Erlang αναπαράσταση ενός οποιουδήποτε
Erlang module. Σε αυτό το χαρακτηριστικό βασίζεται το σύστημά μας για την ανάλυση των προγραμμάτων που του δίνονται ως είσοδος.
Φορτώνει τα modules στο σύστημα χρόνου εκτέλεσης, και αποσπά το Core Erlang Αφηρημένο Δένδρο Σύνταξης αυτού σε μορφή
ενός συνόλου από εγγραφές (records, εγγενής τύπος δεδομένων της Erlang), όπως αυτά ορίζονται στο
$otp/lib/compiler/src/core\_parse.hrl$.
\texttt{otp/lib/compiler/src/core\_parse.hrl}.
\section{Το "σύστημα τύπων" της Erlang}
Η Erlang είναι μια γλώσσα με δυναμικό συστήμα τύπων. Αυτό σημαίνει ότι ο μεταγλωττιστής της γλώσσας δεν πραγματοποιεί έλεγχο τύπων κατά τη μεταγλώττιση ενός
\section{Οι τύποι δεδομένων της Erlang}
Η Erlang είναι μια γλώσσα ασφαλής ως προς τους τύπους (type safe), αλλά με δυναμικό συστήμα τύπων. Αυτό σημαίνει ότι ο μεταγλωττιστής της γλώσσας δεν πραγματοποιεί έλεγχο τύπων κατά τη μεταγλώττιση ενός
προγράμματος. Το σύστημα χρόνου εκτέλεσης είναι υπεύθυνο για να εγγυηθεί την ασφάλεια τύπων, με το να ελέγχει την πληροφορία τύπων που είναι συσχετισμένη με κάθε
κομμάτι δεδομένων ενός προγράμματος κατα τη διάρκεια της εκτέλεσης.
Ένα κομμάτι δεδομένων σε Erlang ονομάζεται όρος ($term$). Ο τύπος ενός όρου μπορεί να είναι είτε κάποιος από τους ενσωματωμένους τύπους της Erlang, είτε ένας τύπος που
έχει προσδιορίσει ο χρήστης. Οι ενσωματωμένοι τύποι της Erlang είναι:
\begin{itemize}
\item Pid
\item Port
\item Reference
\item Atom
\item Bitstring
\item Float
\item Fun
\item Integer
\item List
\item Map
\item Tuple
\item Union
\item Pid: τύπος διακριτικών διεργασιών
\item Port: τύπος διακριτικών μιας θύρας Erlang
\item Reference: τύπος όρων που είναι μοναδικοί στο σύστημα χρόνου εκτέλεσης
\item Atom: τύπος κυριολεκτικών όρων, σταθερών
\item Bitstring: τύπος μια περιοχή μνήμης, τα περιεχόμενα της οποίας δεν έχουν κάποιον συγκεκριμένο τύπο
\item Float: τύπος αριθμών κινητής υποδιαστολής
\item Fun: τύπος συναρτήσεων
\item Integer: τύπος ακεραίων αριθμών
\item List: τύπος μιας αθροιστικής δομής δεδομένων, με μεταβλητό πλήθος στοιχείων
\item Map: τύπος μιας αθροιστικής δομής δεδομένων, με μεταβλητό πλήθος αντιστοιχίσεων κλειδιού-τιμής
\item Tuple: τύπος μιας αθροιστικής δομής δεδομένων, με σταθερό πλήθος στοιχείων
\end{itemize}
Οποιοσδήποτε όρος της Erlang μπορεί να αποτελέσει το περιεχόμενο των μηνυμάτων που ανταλλάσσουν διεργασίες μεταξύ τους
......@@ -269,7 +282,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
\section{Το εργαλείο Dialyzer}
Οι κόμβοι του Core Erlang Δένδρου Αφηρημένης Σύνταξης δε διαθέτουν πληροφορίες τύπων δεδομένων. Σε ορισμένες "απλές"
Οι κόμβοι του Core Erlang Δένδρου Αφηρημένης Σύνταξης δε διαθέτουν πληροφορίες τύπων δεδομένων. Σε ορισμένες ``απλές``
περιπτώσεις, όπως όταν έχουμε κυριολεκτικούς όρους στον κώδικα που αναλύουμε (για παράδειγμα $x = 42$), μπορούμε να
βρούμε τον τύπο των όρων χρησιμοποιώντας συναρτήσεις βιβλιοθήκης της γλώσσας. Προκειμένου να πραγματοποιήσουμε οποιαδήποτε
ουσιώδη ανάλυση
......@@ -277,7 +290,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
ανταλλάσσονται μεταξύ διεργασιών. Συνεπώς, χρειαζόμαστε ένα εργαλείο το οποίο, δοθέντος ενός προγράμματος σε Erlang, να
πραγματοποιεί συμπερασμό τύπων δεδομένων.
Ο Dialyzer (DIscrepancy AnaLYZer) είναι ένα σύστημα που πραγματοποιεί μιας μορφής στατικό type checking σε προγράμματα Erlang.
Ο Dialyzer (DIscrepancy AnaLYZer) είναι ένα εργαλείο που πραγματοποιεί μιας μορφής στατικό type checking σε προγράμματα Erlang.
Σε πρώτη φάση επεξεργάζεται ένα πρόγραμμα Erlang, προκειμένου να εξάγει τα λεγόμενα success typings. Τα success typings
είναι οι τύποι που πρέπει να έχουν οι συναρτήσεις (δηλαδή ο συνδυασμός των τύπων των ορισμάτων μιας συνάρτησης, και του
τύπου του αποτελέσματος που αυτή η συνάρτηση επιστρέφει) προκειμένου να εξασφαλιστεί ότι η συνάρτηση δε θα παρουσιάσει κάποιο
......@@ -295,7 +308,7 @@ $otp/lib/compiler/src/core\_parse.hrl$.
συνάρτηση $foo/1$ είναι $Number \rightarrow Number$.
\lstset{style=erlangCodeStyle}
\begin{lstlisting}[language=Erlang, caption=Simple receive]
\begin{lstlisting}[language=Erlang, caption=Simple receive, captionpos=b]
foo(X) ->
X + 42.
\end{lstlisting}
......@@ -313,8 +326,8 @@ $otp/lib/compiler/src/core\_parse.hrl$.
σε επίπεδο λειτουργικού συστήματος, ούτε όμως και νήματα, αλλά αποτελούν οντότητες τις οποίες διαχειρίζεται
η εικονική μηχανή εκτέλεσης της Erlang, ο BEAM.
Οι διεργασίες σε Erlang δε μοιράζονται αποθηκευτικό χώρο. Ο μοναδικός μηχανισμός που παρέχεται στον προγραμματιστή για
την υλοποίηση της επικοινωνίας και της ανταλλαγής πληροφοριών μεταξύ αυτών των διεργασιών
Ο μηχανισμός που παρέχεται στον προγραμματιστή για
την υλοποίηση της επικοινωνίας και της ανταλλαγής πληροφοριών μεταξύ των διεργασιών του προγράμματός του
είναι η ασύγχρονη ανταλλαγή μηνυμάτων. Κάθε διεργασία διαθέτει ένα "κουτί εισερχομένων", μια ουρά από μηνύματα που έχει λάβει από άλλες διεργασίες. Για να καταναλώσει
ένα μήνυμα από αυτήν την ουρά, ο προγραμματιστής χρησιμοποιεί την έκφραση $receive$, με την οποία παίρνει ένα μήνυμα από
την κεφαλή της ουράς, και το συγκρίνει με μια σειρά από
......@@ -333,21 +346,23 @@ $otp/lib/compiler/src/core\_parse.hrl$.
Στο listing 2.2 φαίνεται ένα παράδειγμα μιας συνάρτησης που περιμένει να διαβάσει από το κουτί εισερχομένων της:
\begin{itemize}
\item Μια πλειάδα τιμών (tuple) που αποτελείται από ένα atom, ένα pid κι έναν αριθμό
\item Μια πλειάδα τιμών που αποτελείται από ένα atom, ένα pid κι ένα atom
\item Έναν απλό αριθμό
\item Μια τριάδα τιμών (tuple μεγέθους 3) που αποτελείται από το atom $num$, ένα pid κι έναν αριθμό.
\item Μια τριάδα τιμών που αποτελείται από το atom $atom$, ένα pid κι ένα ακόμη στοιχείο.
\item Τον ακέραιο $42$.
\end{itemize}
Αν μια διεργασία που επικοινωνεί με αυτήν της αποστείλει ένα μήνυμα της μορφής $\{num, 42\}$, τότε η $foo/1$ δε θα το "καταναλώσει"
ποτέ. Αντίστοιχα, αν καμία διεργασία δεν αποστείλει στη διεργασία που εκτελεί τον κώδικα του listing 2.2 κάποιο μήνυμα
που να αντιστοιχεί σε ένα από τα μοτίβα της εντολής $receive$, η εκτέλεση θα "κρεμάσει" επ' αόριστον.
Αν μια διεργασία που επικοινωνεί με αυτήν της αποστείλει ένα μήνυμα της μορφής $\{num, 42\}$, τότε η $foo/1$ δε θα το ``καταναλώσει``
ποτέ. Αυτό δεν αποτελεί πρόβλημα από μόνο του, αλλά η αποστολή πολλών μηνυμάτων σε μια διεργασία, τα οποία αυτή δεν καταναλώνει, μπορεί να αποτελέσει πρόβλημα δυνητικά,
καθώς ενδέχεται να οδηγήσει σε εξάντληση της μνήμης του συστήματος χρόνου εκτέλεσης της Erlang, και κατά συνέπεια στον τερματισμό της εκτέλεσης ενός κόμβου του συστήματος.
Αντίστοιχα, αν καμία διεργασία δεν αποστείλει στη διεργασία που εκτελεί τον κώδικα του listing 2.2 κάποιο μήνυμα
που να αντιστοιχεί σε ένα από τα μοτίβα της εντολής $receive$, η εκτέλεση θα ``κρεμάσει`` επ' αόριστον.
Σε αυτήν την περίπτωση θα είχαμε ένα προβληματικό σενάριο, που
προκύπτει από τη μη-συμμόρφωση τουλάχιστον ενός εκ των δύο μερών της επικοινωνίας στο αναμενόμενο πρωτόκολλο.
%% Type and effect systems
\chapter{Συστήματα τύπων και επιδράσεων}
Πολλές γλώσσες προγραμματισμού υλοποιούν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε
Πολλές γλώσσες προγραμματισμού ενσωματώνουν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε
τελεσταίους της κατάλληλης μορφής, δηλαδή του κατάλληλου είδους \cite{types-and-prog-langs, advanced-types-and-prog-langs}. Για παράδειγμα, ένα κλασσικό σύστημα τύπων θα απέρριπτε
το πρόγραμμα 3.1 (γραμμένο σε μια υποθετική γλώσσα), καθώς η πράξη της αφαίρεσης ($-$), δεν έχει νόημα όταν εφαρμόζεται
σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών, με την
......@@ -360,15 +375,15 @@ $otp/lib/compiler/src/core\_parse.hrl$.
\end{lstlisting}
\section{Κλασσικά συστήματα τύπων με συμπερασμό}
Τα πρώτα στατικά συστήματα τύπων βασίζονταν σε type annotations τα οποία παρείχε ο χρήστης. Αυτά ήταν ετικέτες που
Τα πρώτα στατικά συστήματα τύπων βασίζονταν σε επισημειώσεις τύπων (type annotations) τις οποίες παρείχε ο χρήστης. Αυτές ήταν ετικέτες που
συνόδευαν τις δηλώσεις μεταβλητών και συναρτήσεων, και περιέγραφαν τον τύπο που αυτές θα περιείχαν (στην περίπτωση
μεταβλητών), ή τους τύπους των ορισμάτων και της τελικής τιμής τους (στην περίπτωση συναρτήσεων), και υπηρετούσαν ως
οδηγίες προς τον μεταγλωττιστή. Κατά το χρόνο μεταγλώττισης, αυτός ήταν υπεύθυνος να συγκρίνει τον δηλωθέντα τύπο μιας
μεταβλητής ή συνάρτησης με τους προσδοκόμενους τύπους στο σημείο που αυτά τα constructs χρησιμοποιούνται σε ένα
μεταβλητής ή συνάρτησης με τους προσδοκόμενους τύπους στο σημείο που αυτές χρησιμοποιούνται σε ένα
πρόγραμμα, προκειμένου να διαπιστώσει αν υπάρχουν ασυμφωνίες τύπων.
Προκειμένου να εξαλειφθεί η ανάγκη για τη χειρονακτική δήλωση των τύπων τμημάτων δεδομένων σε ένα πρόγραμμα,
αναπτύχθηκαν συστήματα τύπων με αυτόματο συμπερασμό τύπων, όπως αυτό των Hindley-Milner (ή αλλιώς Dammas-Milner), με την
αναπτύχθηκαν συστήματα τύπων με αυτόματο συμπερασμό τύπων, όπως αυτό των Hindley-Milner (ή αλλιώς Dammas-Milner) \cite{damas-milner}, με την
γλώσσα ML να είναι η πρώτη για την οποία υλοποιήθηκε ένα τέτοιο σύστημα.
Η προσέγγιση των συστημάτων τύπων είναι να συσχετίζουν τύπους με προγράμματα. Οι τύποι περιγράφουν το είδος των δεδομένων
......@@ -386,9 +401,9 @@ $otp/lib/compiler/src/core\_parse.hrl$.
Οι προκλήσεις του σχεδιασμού ενός συστήματος συμπερασμού τύπων είναι:
\begin{itemize}
\item Το σύστημα τύπων να είναι σημασιολογικά ορθό %% TODO elaborate
\item Το σύστημα τύπων να είναι σημασιολογικά ορθό.
\item Το σύστημα τύπων να είναι αποφάνσιμο, το οποίο σημαίνει ότι πρέπει να είναι δυνατός ο σχεδιασμός ενός
αλγορίθμου ο οποίος να τερματίζει και να ελέγχει τις ιδιότητες του συστήματος
αλγορίθμου ο οποίος να τερματίζει και να ελέγχει τις ιδιότητες του συστήματος.
\end{itemize}
%FIXME annotations <-> ετικετών
......@@ -398,16 +413,17 @@ $otp/lib/compiler/src/core\_parse.hrl$.
όπως:
\begin{itemize}
% FIXME bind-time <-> χρονος δεσίματος
\item Ανάλυση χρόνου δεσίματος, κατα την οποία προσπαθούμε να πραγματοποιήσουμε μια διάκριση ανάμεσα σε αυτά τα δεδομένα των
\item Ανάλυση χρόνου δεσίματος (bind-time analysis), κατα την οποία προσπαθούμε να πραγματοποιήσουμε μια διάκριση ανάμεσα σε αυτά τα δεδομένα των
οποίων η τιμή είναι γνωστή κατα το χρόνο μεταγλώττισης (στατικά), και σε αυτά τα οποία αποκτούν τιμή κατα την
εκτέλεση του προγράμματος (δυναμικά). Αυτού του τύπου η ανάλυση αποτελεί τη βάση της μερικής αποτίμησης που
πραγματοποιούν μεταγλωττιστές
\item Ανάλυση χρήσεων, κατά την οποία θέλουμε να μάθουμε πόσες φορές χρησιμοποιείται η τιμή μιας έκφρασης στη
\item Ανάλυση χρήσεων (usage analysis), κατά την οποία θέλουμε να μάθουμε πόσες φορές χρησιμοποιείται η τιμή μιας έκφρασης στη
διάρκεια της εκτέλεσης ενός προγράμματος. Αν αποφανθούμε ότι δε γίνεται ποτέ χρήση μιας τιμής, ο μεταγλωττιστής
δε χρειάζεται να παράξει κώδικα για αυτήν. Επίσης, αν μια τιμή χρησιμοποιείται μόνο μια φορά, η μεταβλητή που
δε χρειάζεται να παράξει κώδικα για αυτήν.
\item Συλλογή σκουπιδιών (garbage collection): αν μια τιμή χρησιμοποιείται μόνο μια φορά, η μεταβλητή που
την περιέχει μπορεί να συλλεγεί από τον συλλέκτη σκουπιδιών του περιβάλλοντος εκτέλεσης αμέσως μετά τη χρήση
της.
\item Ανάλυση ροής ελέγχου, κατά την οποία προσπαθούμε, συνήθως σε γλώσσες με συναρτήσεις υψηλότερης τάξης, να
\item Ανάλυση ροής ελέγχου (control flow analysis), κατά την οποία προσπαθούμε, συνήθως σε γλώσσες με συναρτήσεις υψηλότερης τάξης, να
συμπεράνουμε ποιες συναρτήσεις είναι πιθανοί "αποδέκτες" μιας κλήσης σε ένα πρόγραμμα, δηλαδή ποιες συναρτήσεις
είναι πιθανό να αποκτήσουν τον ελέγχο ενός προγράμματος (το οποίο δεν είναι πάντα εμφανές σε γλώσσες τέτοιου
τύπου από τον πηγαίο κώδικά τους).
......@@ -465,7 +481,7 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
επικοινωνίας, με χρήση δύο άλλων θεμελιωδών λειτουργιών
\begin{itemize}
\item $request(a, k)$, που αποτελεί ένα αίτημα εγκαθίδρυσης ενός καναλιού επικοινωνίας $k$ μέσω της θύρας $a$.
\item $accept(a, k)$, που αποτελεί αποδοχή ενός αίτημα εγκαθίδρυσης ενός καναλιού επικοινωνίας $k$ μέσω της θύρας
\item $accept(a, k)$, που αποτελεί αποδοχή ενός αιτήματος εγκαθίδρυσης ενός καναλιού επικοινωνίας $k$ μέσω της θύρας
$a$.
\end{itemize}
......@@ -480,7 +496,7 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
που σημαίνει ότι μια διεργασία που χρησιμοποιεί τη θύρα $a$ για να επικοινωνεί θα:
\begin{itemize}
\item στείλει μια τιμή τύπου ακεραίου (int), το οποίο συμβολίζεται με $\uparrow$, και ακολούθως θα
\item στείλει μια τιμή τύπου ακεραίου ($int$), το οποίο συμβολίζεται με $\uparrow$, και ακολούθως θα
\item λάβει μια τιμή τύπου ακεραίου, το οποίο συμβολίζεται με $\downarrow$
\end{itemize}
......@@ -499,7 +515,7 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
Μέχρι πρόσφατα, η έρευνα επικεντρωνόταν σε τύπους συνεδριών δύο συμμετεχόντων. Αυτές ήταν σε θέση να περιγράφουν
επικοινωνία με πολλαπλούς συμμετέχοντες, όμως τα επιμέρους πρωτόκολλα έπρεπε να αφορούν δύο συγκεκριμένους συμμετέχοντες
και να είναι ανεξάρτητα μεταξύ τους. Συνέπεια αυτού είναι ότι τα συστήματα αυτά δε μπορούν να "περιορίσουν" ή να
και να είναι ανεξάρτητα μεταξύ τους. Συνέπεια αυτού είναι ότι τα συστήματα αυτά δε μπορούν να ``περιορίσουν`` ή να
διασφαλίσουν τη σειρά με την οποία ανταλλάσονται μηνύματα σε δύο διαφορετικά πρωτόκολλα.
......@@ -514,9 +530,9 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
\item Η πρώτη είναι η άλγεβρα που αποτελεί το φορμαλισμό της καθολικής περιγραφής της επικοινωνίας.
Σε αυτήν μπορεί να περιγραφεί η
αλληλεπίδραση των πρακτόρων της επικοινωνίας σε ένα αφηρημένο επίπεδο, μόνο σαν μια αλληλουχία από ενέργειες
μεταξύ συμμετεχόντων
μεταξύ συμμετεχόντων.
\item Η δεύτερη είναι ο φορμαλισμός της τοπικής περιγραφής. Σε αυτήν περιγράφεται η επικοινωνία από τη σκοπιά ενός
συμμετέχοντα στην επικοινωνία (ενός πράκτορα)
συμμετέχοντα στην επικοινωνία (ενός πράκτορα).
\end{itemize}
Οι δύο άλγεβρες συνδέονται μεταξύ τους με μια σχέση προβολής, η οποία με βάση την καθολική περιγραφή της επικοινωνίας
......@@ -564,8 +580,7 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
\[
\begin{array}{lrl}
sestype & ::= & monosestype \\
& \mid & sestype
sestype & ::= & monosestype
\vspace{2mm}\\
monosestype & ::= & (datatype_{1}, \ldots, datatype_{n}) \to \\
......@@ -596,16 +611,6 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
\]
\vspace{4mm}
\[
\begin{array}{lrl}
PE & ::= & \varnothing \\
& \mid & PE, P
\end{array}
\begin{array}{lrl}
SE & ::= & \varnothing \\
& \mid & SE, \sigma
\end{array}
\]
Ο τύπος $Type$ στον ορισμό του $datatype$ είναι ο τύπος ενός Erlang term, όπως αυτό περιγράφεται στο Erlang TypeSpec.
......@@ -615,8 +620,21 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
\begin{itemize}
\item $DE$ το περιβάλλον των ζευγών $(x, t)$, όπου $x$ ένα Erlang Term, και $t$ ο τύπος του
\item $PE$ το περιβάλλον των ζευγών $(n, p)$, όπου $n$ το όνομα ενός process, όπως αυτό συναντάται στο πρόγραμμα,
και $p$ η διεύθυνση χρόνου εκτέλεσης της διεργασίας.
και $p$ η διεύθυνση χρόνου εκτέλεσης της διεργασίας. Το περιβάλλον αυτό ορίζεται ως
\[
\begin{array}{lrl}
PE & ::= & \varnothing \\
& \mid & PE, P
\end{array}
\]
\item $SE$ το περιβάλλον των ζευγών $(f, st)$ όπου $f$ το όνομα μιας συνάρτησης, και $st$ ο τύπος συνεδρίας της.
Το περιβάλλον αυτό ορίζεται ως
\[
\begin{array}{lrl}
SE & ::= & \varnothing \\
& \mid & SE, \sigma
\end{array}
\]
\end{itemize}
Ορίζουμε ως $\Gamma = \{DE, PE, SE\}$ την τριάδα που μας δίνει τα type schemes.
......@@ -658,38 +676,38 @@ To κανάλι επικοινωνίας $k$ δημιουργείται ρητά
{\Gamma\,\vdash Expr, ExprSequence \ \ :\ datatype; sesaction, \phi}
\end{gather*}
Ο κανόνας $send$ περιγράφει την επίδραση μιας αποστολής μηνύματος. Καθώς πρώτα αποτιμώνται οι τιμές των $e_{2}$ και
Ο κανόνας \emph{send} περιγράφει την επίδραση μιας αποστολής μηνύματος. Καθώς πρώτα αποτιμώνται οι τιμές των $e_{2}$ και
$e_{1}$, οι επιδράσεις τους θα παρατηρηθούν πρώτες. Ο τύπος του αριστερού τελεσταίου της έκφρασης αποστολής πρέπει πάντα
να είναι η διεύθυνση μιας διεργασίας. Ο τύπος του μηνύματος μπορεί να είναι οποιοσδήποτε έγκυρος τύπος δεδομένων ενός
Erlang term. Στο τέλος, παρατηρείται και η επίδραση της αποστολής του μηνύματος $e_{2}$.
Ο κανόνας $recv$ περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία "ακούει" μόνο για μηνύματα ενός
συγκεκριμένου τύπου $datatype_{e}$. Σε Erlang, το pattern του μηνύματος πρέπει να είναι ένα απλό term, με αποτέλεσμα
Ο κανόνας \emph{recv} περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία "ακούει" μόνο για μηνύματα ενός
συγκεκριμένου τύπου $datatype_{e}$. Σε Erlang, το pattern του μηνύματος πρέπει να είναι σαν ένα απλό term (με τη διαφορά
ότι επιτρέπεται να περιέχει μεταβλητές που δεν έχουν συσχετισθεί ακόμη με κάποια τιμή), με αποτέλεσμα
ποτέ να μην είναι effectful, εξού και η επίδρασή του ($nothing$). Κατά την αποτίμηση του σώματος του receive clause,
χρησιμοποιούμε το περιβάλλον $\Gamma' = \{DE', PE', SE\}$, όπου τα $DE'$ και $PE'$ προκύπτουν από τα $DE$ και $PE$
προσθέτοντας τυχών μεταβλητές που περιέχονται στο receive pattern.
Ο κανόνας $offer$ περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία "ακούει" για μηνύματα διαφορετικών
Ο κανόνας \emph{offer} περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία ``ακούει`` για μηνύματα διαφορετικών
μορφών. Και εδώ τα patterns είναι effectless.
Ο κανόνας $choice\_case$ περιγράφει την επίδραση μιας έκφρασης που προκαλεί διακλάδωση στην εκτέλεση, σε περίπτωση που τα
Ο κανόνας \emph{choice\_case} περιγράφει την επίδραση μιας έκφρασης που προκαλεί διακλάδωση στην εκτέλεση, σε περίπτωση που τα
σώματα των
clauses είναι effectful, και οι επιδράσεις τους ξεκινούν όλες με ένα $send$ action.
Ο κανόνας $sequencing$ περιγράφει την επίδραση ενός συνόλου από εκφράσεις, οι οποίες αποτιμώνται με μια γραμμική σειρά.
Ο κανόνας \emph{sequencing} περιγράφει την επίδραση ενός συνόλου από εκφράσεις, οι οποίες αποτιμώνται με μια γραμμική σειρά.
Αυτός είναι ο κανόνας με βάση των οποίο συμπεραίνουμε τους τύπους και τις επιδράσεις συναρτήσεων.
Στο σύστημα τύπων και επιδράσεών μας, οι μόνες εκφράσεις που έχουν κάποια επίδραση είναι αυτή της αποστολής μηνύματος
(!), και αυτή της λήψης μηνύματος ($ receive ... end $). Όλες οι υπόλοιπες Erlang εκφράσεις είναι effectless.
Στο σύστημα τύπων και επιδράσεών μας, οι μόνες εκφράσεις που έχουν κάποια επίδραση είναι αυτές της αποστολής
(!) και της λήψης ($ receive ... end $) μηνύματος. Όλες οι υπόλοιπες Erlang εκφράσεις είναι effectless.
\section{Υλοποίηση}
\subsection{Τμήματα}
Καθόλη τη διάρκεια αυτής της ενότητας, θα χρησιμοποιούμε το απλό πρόγραμμα που φαίνεται στο σχήμα 5.1 ως βάση για να
εξηγήσουμε τη λειτουργία του συστήματός μας.
\begin{lstlisting}[language=Erlang, caption=Απλό παράδειγμα, basicstyle=\small]
\begin{lstlisting}[language=Erlang, caption=Απλό παράδειγμα, basicstyle=\ttfamily\small]
run() ->
ProcServer = spawn(fun() -> server() end),
Foo = spawn(fun() -> foo() end),
......@@ -761,16 +779,17 @@ biz() ->
end.
\end{lstlisting}
Το συστημά μας αποτελείται από τα εξής επιμέρους κομμάτια:
\subsection{Τμήματα}
Το συστημά μας αποτελείται από τα εξής επιμέρους τμήματα:
\begin{itemize}
\item Το κομμάτι του συμπερασμού των τύπων συνεδριών του προγράμματος που δεχόμαστε ως είσοδο
\item To κομμάτι του ελέγχου των τύπων που συμπέρανε το σύστημά μας με τους τύπους που παρέχονται από τον χρήστη ως
ο "προδιαγεγραμμένος" τύπος συνεδρίας ενός τμήματος του προγράμματος
\item Το κομμάτι της σύγκρισης των τύπων δύο συναρτήσεων προκειμένου να διαπιστωθεί αν αποτελούν τα "άκρα" ενός
πρωτοκόλλου επικοινωνίας
\item Το τμήμα του συμπερασμού των τύπων συνεδριών του προγράμματος που δεχόμαστε ως είσοδο.
\item To τμήμα του ελέγχου των τύπων που συμπέρανε το σύστημά μας με τους τύπους που παρέχονται από τον χρήστη ως
ο ``προδιαγεγραμμένος`` τύπος συνεδρίας ενός τμήματος του προγράμματος.
\item Το τμήμα της σύγκρισης των τύπων δύο συναρτήσεων προκειμένου να διαπιστωθεί αν αποτελούν τα ``άκρα`` ενός
πρωτοκόλλου επικοινωνίας.
\end{itemize}
Όλα τα προγράμματα που παρέχονται προς ανάλυση "περνάνε" από το πρώτο κομμάτι. Το δεύτερο και το τρίτο ενεργοποιούνται
Όλα τα προγράμματα που παρέχονται προς ανάλυση περνάνε από το πρώτο τμήμα. Το δεύτερο και το τρίτο ενεργοποιούνται
με βάση την είσοδο του χρήστη.
\subsection{Συμπερασμός Τύπων Συνεδριών}
......@@ -780,19 +799,19 @@ biz() ->
Στο κεφάλαιο 4 είδαμε ότι στους τύπους συνεδρίας, ένα θεμελιώδες κομμάτι της ανάλυσης είναι η γνώση των τύπων δεδομένων
που περιέχονται στα μηνύματα που ανταλλάσσονται μεταξύ των επικοινωνουσών διεργασιών.
Προκειμένουν να αποκτήσουμε αυτήν την πληροφορία για τους σκοπούς της δικής μας ανάλυσης, αξιοποιούμε τον Dialyzer. Με
Προκειμένου να αποκτήσουμε αυτήν την πληροφορία για τους σκοπούς της δικής μας ανάλυσης, αξιοποιούμε τον συμπερασμό τύπων
του Dialyzer. Με
αυτόν τον τρόπο, ο συμπερασμός τύπων συνεδρίας του συστήματός μας πραγματοποιείται σε δύο φάσεις:
\begin{itemize}
\item Στην πρώτη φάση, δίνουμε το προς ανάλυση πρόγραμμα ως είσοδο στον Dialyzer. Μετά το τέλος της εκτέλεσής του,
έχουμε συμπεράνει τους τύπους των δεδομένων του προγράμματος.
\item Στη δεύτερη φάση, επανεπεξεργαζόμαστε όλο το πρόγραμμα, και συμπεραίνουμε τους τύπους συνεδριών των
συναρτήσεων του με βάση τους κανόνες της προηγούμενης ενότητας, και αξιοποιώντας την πληροφορία που εξήγαγε ο
Dialyzer, την οποία χρησιμοποιήσαμε για να "γεμίσουμε" το περιβάλλον $\Gamma$ με τις αντιστοιχήσεις μεταβλητών με
Dialyzer, την οποία χρησιμοποιήσαμε για να ``γεμίσουμε`` το περιβάλλον $\Gamma$ με τις αντιστοιχήσεις μεταβλητών με
τύπους.
\end{itemize}
Για μια ανάλυση του τρόπου με τον οποίο δουλεύει ο Dialyzer, ο αναγνώστης παραπέμπεται στα \cite{dialyzer-reference-manual}
και \cite{practical-success-typings}.
Για μια ανάλυση του τρόπου με τον οποίο δουλεύει ο Dialyzer, ο αναγνώστης παραπέμπεται στο \cite{practical-success-typings}.
Χρησιμοποιούμε μια έκδοση του Dialyzer βασισμένη σε αυτήν που περιέχεται στην έκδοση 19.0 του Erlang/OTP, ελαφρώς
τροποποιημένη για τους σκοπούς μας, ώστε να διατηρεί την πληροφορία που σχετίζεται με τους τύπους δεδομένων των
......@@ -811,20 +830,21 @@ Erlang AST του κάθε module, αποδίδοντας σε κάθε κόμβ
Κατά τη φάση του συμπερασμού τύπων, στη θέση της επίδρασης της καλούμενης συνάρτησης βάζουμε μια τιμή placeholder, την
$\{unavailable, \{Module, Function, Arity\}\}$, όπου $Module$ το module στο οποίο ορίζεται η καλούμενη συνάρτηση,
$Function$ το όνομα της καλούμενης συνάρτησης, και $Arity$ η πολλαπλότητα αυτής.
$Function$ το όνομα της καλούμενης συνάρτησης, και $Arity$ η πολλαπλότητα της.
Στο τέλος της ανάλυσης των modules του προγράμματος, πραγματοποιούμε ένα iteration πάνω σε όλες τις ορισμένες
συναρτήσεις, και κάνουμε resolve όλες τις επιδράσεις που δεν ήταν διαθέσιμες κατά τη διάρκεια αυτής. Εδώ, resolution
συναρτήσεις, και επεκτείνουμε όλες τις επιδράσεις που δεν ήταν διαθέσιμες κατά τη διάρκεια αυτής. Εδώ, resolution
σημαίνει η αντικατάσταση των placeholders \[\{unavailable, \{Module, Function, Arity\}\}\] με το πλήρες session type της
καλούμενης συνάρτησης στο session type της καλούσας.
Αυτός είναι και ο λόγος που δε μπορούμε να διαχειριστούμε αμοιβαίως αναδρομικές συναρτήσεις. Η πλήρης ανάπτυξη του
Λόγω του τρόπου με τον οποίο διαχειριζόμαστε τις επιδράσεις συναρτήσεων που δεν έχουμε αναλύσει ακόμη, το σύστημα συμπερασμού τύπων μας δε μπορεί
να διαχειριστεί αμοιβαίως αναδρομικές συναρτήσεις. Η πλήρης ανάπτυξη του
session type της μιας στο session type της άλλης θα οδηγούσε σε ένα undecidable πρόβλημα.
% βασικά, θα οδηγούσε στο μη τερματισμό του αλγορίθμου (για προφανείς λόγους), αλλά και πέρα από αυτό, ακόμα και από το
% type system σε θεωρητικό επίπεδο είναι εμφανές ότι δε μπορούμε να μοντελοποιήσουμε αμοιβαίως αναδρομικές συναρτήσεις
Για το παράδειγμα του σχήματος 5.1, το σύστημά μας συμπεραίνει τους εξής τύπους συνεδριών:
\begin{lstlisting}[language=Erlang, caption=Inferred session types, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=Inferred session types, basicstyle=\ttfamily\scriptsize]
{server,0} : "u (4). Of<any; ?(atom x {atom, pid, (atom x atom)} x number). ?(atom x {atom, pid, (atom x atom)} x number).
pid(1) !(atom x pid x number).rec(4).,any; ?(atom x {atom, pid, (atom x atom)} x number).rec(4).>."
......@@ -878,7 +898,7 @@ session type της μιας στο session type της άλλης θα οδηγ
\end{tabular}
\end{center}
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\ttfamily\scriptsize]
-sestype({{server, 0},
?f_rec_tag(1, [?sa_offer_tag([{?dt_any_tag, [?sa_recv_tag(?dt_any_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
......@@ -908,7 +928,7 @@ session type της μιας στο session type της άλλης θα οδηγ
από τους δύο τύπους, και ελέγχοντας:
\begin{itemize}
\item Ότι τα actions που περιγράφουν είναι ίδια
\item Ότι το datatype του user annotation για το συγκεκριμένο action είναι υποτύπος του inferred session type τύπου.
\item Ότι το datatype του user annotation για το συγκεκριμένο action είναι υποτύπος του συμπερασμένου τύπου δεδομένων.
\end{itemize}
Το δεύτερο κριτήριο είναι αυτό που κάνει το σύστημά μας πλήρες: ποτέ δε θα απορρίψει ένα σωστό πρόγραμμα.
......@@ -923,13 +943,12 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
Για παράδειγμα, στο πρώτο clause της $simple\_send/3$, αν ο χρήστης είχε δώσει
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=Type mismatch, basicstyle=\ttfamily\scriptsize]
-sestype({{server, 0},
?f_rec_tag(1, [?sa_offer_tag([{?dt_any_tag, [?sa_recv_tag(?dt_any_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
...
\end{lstlisting}
ο έλεγχος θα είχε αποτύχει, καθώς το $any$ αποτελεί τον υπερτύπο όλων των τύπων δεδομένων της Erlang.
\subsection{Έλεγχος peers}
......@@ -945,11 +964,11 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
\paragraph{Ο Αλγόριθμος}
% TODO describe the algorithm
Μοντελοποιούμε τους τύπους συνεδριών της κάθε συνάρτησης ως ένα (πιθανώς κυκλικό) κατευθυνόμενο γράφημα $G(V, E)$. Κάθε
κορυφή στο $V$ αναπαριστά ένα action. Μια ακμή $e$ από την κορυφή $u$ στην κορυφή $v$ σημαίνει ότι το action που
κορυφή στο $V$ αναπαριστά ένα action. Μια ακμή $e=(u, v)$ σημαίνει ότι το action που
περιγράφεται από τη $v$ ακολουθεί αυτό που περιγράφεται από τη $u$ στον τύπο συνεδρίας της συνάρτησης.
% TODO example graph
\begin{algorithm}[caption={Session Type Matching}, label={match}]
\begin{algorithm}[caption={1. Session Type Matching}, label={match}]
input: graph $G_1$, graph $G_2$
output: list of successful routes
begin
......@@ -981,24 +1000,22 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
end
\end{algorithm}
Το σύνολο αναζήτησης $S$ είναι μια ουρά από ζευγάρια κορυφών, των οποίων τα actions προσπαθούμε να ελέγξουμε ως προς τη
Το σύνολο αναζήτησης $S$ είναι μια ουρά από ζευγάρια κορυφών, των οποίων τις πράξεις προσπαθούμε να ελέγξουμε ως προς τη
συμπληρωματικότητα. Κρατάμε το μονοπάτι το οποίο μας οδήγησε στο κάθε ζευγάρι κορυφών, τόσο ως προς το από ποιες κορυφές
περάσαμε, όσο και ως προς τον τύπο συνεδρίας με τον οποίο "φτάσαμε" στα παρόντα actions.
περάσαμε, όσο και ως προς τον τύπο συνεδρίας με τον οποίο φτάσαμε στις παρούσες πράξεις.
Ο αλγόριθμός μας ξεκινά με το να προσθέτει τα ζευγάρια των κορυφών-ριζών του κάθε γραφήματος στο σύνολο αναζήτησης $S$,
όπως φαίνεται στη γραμμή $4$ του παραπάνω αλγορίθμου. Κάθε γράφημα μπορεί να έχει περισσότερους του ενός αρχικούς
κόμβους, σε περιπτώσεις όπου το πρώτο action είναι ένα $choice$ ή ένα $offer$.
Συνεχίζει με το να βγάζει από την ουρά το πρώτο ζευγάρι κορυφών, και να συγκρίνει τα actions που αναπαριστούν.
Αν τα actions τους δεν είναι συμπληρωματικά, τότε θεωρούμε ότι το παρόν μονοπάτι αποτελεί ένα μη επιτυχές match, και
προχωράμε στο επόμενο ζεύγος κορυφών.
Αν τα actions τους είναι συμπληρωματικά, ελέγχουμε το σύνολο των έξω-γειτόνων της κάθε κορυφής. Εάν και τα δύο είναι
άδεια, τότε καταναλώσαμε πλήρως και τους δύο τύπους, και μπορούμε να κρατήσουμε το μονοπάτι που ακολουθήσαμε στο σύνολο
των έγκυρων ακολουθιών.
Εάν οποιοδήποτε από τα δύο σύνολα δεν είναι άδειο, ελέγχουμε το είδος των έξω-γειτόνων με τον αλγόριθμο:
\begin{algorithm}[caption={Out-neighbour criteria}, label={recursive_criteria}]
\begin{algorithm}[caption={2. Out-neighbour criteria}, label={recursive_criteria}]
input: graph $G$, vertex $v$
output: list of out-neighbours of $v$ which are not
starts of recursive sequences
......@@ -1020,7 +1037,7 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
\end{algorithm}
Αυτός ο αλγόριθμος ελέγχει όλους τους έξω-γείτονες μιας κορυφής $v$, και μας λέει αν όλοι τους αποτελούν την πρώτη
κορυφή μιας αναδρομικής ακολουθίας, και αν ναι, το ελάχιστο "βάθος" της αναδρομής. Εδώ ορίζουμε ώς $βάθος$ το επίπεδο
κορυφή μιας αναδρομικής ακολουθίας, και αν ναι, το ελάχιστο ``βάθος`` της αναδρομής. Εδώ ορίζουμε ώς $βάθος$ το επίπεδο
εμφώλευσης της αναδρομικής ακολουθίας, καθώς σε ένα session type μπορούμε να έχουμε αναδρομικές υποακολουθίες.
Για παράδειγμα, στον τύπο συνεδρίας
......@@ -1031,7 +1048,6 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
&(\mu \phi.?\ atom\ x\ integer. \phi).\\
&\sigma
\end{align*}
η κορυφή που αντιστοιχεί στην πρώτη $send$ λειτουργία έχει βάθος 1, καθώς δεν είναι εμφωλευμένη. Η $receive$ λειτουργία
εντός της αναδρομικής υποακολουθίας έχει βάθος 2.
......@@ -1048,7 +1064,7 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
% TODO elaborate on why these are terminal conditions
Ακολουθούν μερικά peer annotations για το πρόγραμμα 5.1.
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\ttfamily\scriptsize]
-peers([{{server, 0}, []}, {{simple_client, 1}, []}]).
-peers([{{server, 0}, []}, {{recursive_client, 2}, []}]).
......@@ -1058,9 +1074,24 @@ annotations θα οδηγούσε σε απόρριψη αρκετών σωστ
-peers([{{biz, 0}, []}, {{baz, 1}, []}]).
\end{lstlisting}
Ας αναλύσουμε τα δύο πρώτα ζευγάρια annotations.
Tο όρισμα του $-peers()$ annotation είναι μια λίστα, στοιχεία της οποίας είναι tuples μεγέθους 2, τα οποία αναπαριστούν
τις συναρτήσεις των οποίων τους τύπους συνεδρίας θέλουμε να συγκρίνουμε. Συγκεκριμένα:
\begin{itemize}
\item Το πρώτο στοιχείο του tuple είναι επίσης ένα tuple μεγέθους 2, που προσδιορίζει την συνάρτηση που μας
ενδιαφέρει, σε μορφή $\{function\_name, arity\}$.
\item Το δεύτερο στοιχείο είναι μια λίστα, που επιτρέπει στον προγραμματιστή να παραμετροποιήσει τη σύγκριση.
Ο προγραμματιστής μπορεί να δώσει συνδυασμό των επιλογών
\begin{itemize}
\item \emph{total}, με την οποία ο προγραμματιστής μας λέει ότι για να είναι επιτυχές το ταίριασμα, πρέπει ο
τύπος συνεδρίας της συνάρτησης να καταναλωθεί πλήρως.
\item \emph{user\_type}, με την οποία ο προγραμματιστής μας λέει να μη χρησιμοποιήσουμε τον τύπο συνεδρίας
που συμπεράναμε, αλλά τον τύπο που μας παρείχε ο ίδιος μέσω του \emph{-sestype()} annotation.
\end{itemize}
\end{itemize}
Ας αναλύσουμε τα δύο πρώτα ζευγάρια annotations του listing 5.7.
Τα κατευθυνόμενα γραφήματα των τύπων συνεδρίας των συναρτήσεων $server/0$, $simple\_client/1$ και
$recursive\_client/2$ φαίνονται στα σχήματα 5.Χ έως 5.Υ.
$recursive\_client/2$ φαίνονται στα σχήματα 5.1 έως 5.3.
\begin{figure}[h]
\caption{server/0}
......@@ -1087,14 +1118,14 @@ $f/a[v]$.
S = \{\{server/0[v_0], simple\_client/1[v_0]\}, \{server/0[v_1], simple\_client/1[v_0]\}\}
\]
Θεωρούμε το πρώτο εκ των δύο ζευγών. Ο έλεγχος της γραμμής 8 είναι επιτυχής, καθώς τα session actions που αναπαριστούν
Θεωρούμε το πρώτο εκ των δύο ζευγών. Ο έλεγχος της γραμμής 8 του αλγορίθμου 1 είναι επιτυχής, καθώς τα session actions που αναπαριστούν
οι δύο κορυφές είναι συμπληρωματικά. Κανένα από τα δύο σύνολα έξω-γειτόνων δεν είναι άδεια: το σύνολο $out$ για την
κορυφή $server/0[v_0]$ είναι $\{server/0[v_2]\}$, ενώ για την $simple_client/1[v_0]$ είναι το $\{simple_client/1[v_1]\}$.
κορυφή $server/0[v_0]$ είναι $\{server/0[v_2]\}$, ενώ για την $simple\_client/1[v_0]$ είναι το $\{simple\_client/1[v_1]\}$.
Καθώς όλες οι κορυφές που
ανήκουν σε αυτά τα σύνολα αποτυγχάνουν στον έλεγχο των γραμμών 20 και 21, προσθέτουμε το καρτεσιανό τους γινόμενο στο
τελος του συνόλου αναζήτησης, με αποτέλεσμα να έχουμε ως νέο σύνολο αναζήτησης το
\[
S = \{\{server/0[v_1], simple\_client/1[v_0]\}, \{server/0[v_2], simple_client/1[v_1]\}\}
S = \{\{server/0[v_1], simple\_client/1[v_0]\}, \{server/0[v_2], simple\_client/1[v_1]\}\}
\]
Εκτελώντας τον αλγόριθμο για για το δεύτερο ζεύγος κορυφών του αρχικού συνόλου αναζήτησης, και πάλι έχουμε επιτυχία του
......@@ -1109,7 +1140,7 @@ $f/a[v]$.
\end{split}
\end{equation}
Εκτελώντας το βρόχο των γραμμών 6-26 του αλγορίθμου μέχρι να εξαντλήσουμε το σύνολο αναζήτησης, βρίσκουμε ότι πράγματι
Εκτελώντας το βρόχο των γραμμών 6-26 του αλγορίθμου 1 μέχρι να εξαντλήσουμε το σύνολο αναζήτησης, βρίσκουμε ότι πράγματι
οι συναρτήσεις $server/0$ και $simple\_client/1$ αποτελούν communication peers, και τα συμπληρωματικά session sequences
μεταξύ τους είναι τα:
\begin{equation}
......@@ -1159,12 +1190,13 @@ $f/a[v]$.
Στην παρούσα ενότητα, παρουσιάζουμε ένα κλασσικό παράδειγμα στην ανάλυση συστημάτων τύπων συνεδριών. Το παράδειγμα αυτό
αποτελεί μια υλοποίηση του αναδρομικού arithmetic server που πρωτοπεριγράφηκε στο [], με μια διαφορά: έχουμε εξαλείψει
την έννοια του "καναλιού" μέσω του οποίου ένας client αποστέλει στον διακομιστή το αίτημά του, και το οποίο
την έννοια του ``καναλιού`` μέσω του οποίου ένας client αποστέλει στον διακομιστή το αίτημά του, και το οποίο
δημιουργείται κατά το αίτημα.
Το πρόγραμμα που υλοποιεί τον arithmetic server, καθώς και clients που αιτούνται πράξεις από αυτόν, έχει ως εξής:
Το πρόγραμμα που υλοποιεί τον arithmetic server, καθώς και clients που αιτούνται πράξεις από αυτόν, φαίνεται στο listing
5.8.
\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\ttfamily\scriptsize]
run() ->
Server = spawn(fun server/0),
process_flag(trap_exit, true),
......@@ -1244,10 +1276,10 @@ sqrt_client(Server, N) ->
end.
\end{lstlisting}
Και ακολουθούν τα annotations προς το σύστημά μας, που περιγράφουν το πρωτόκολλο που πρέπει να ακολουθείτα από την
υλοποίησή μας.
Στο listing 5.9 φαίνονται τα session type annotations που περιγράφουν το πρωτόκολλο που πρέπει να ακολουθείται από την
υλοποίηση.
\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=Arithmetic Server Implementation, basicstyle=\ttfamily\tiny]
-sestype({{server, 0},
?f_rec_tag(1, [?sa_offer_tag([{?dt_atom_tag, [?sa_recv_tag(?dt_atom_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag])),
......@@ -1296,10 +1328,10 @@ sqrt_client(Server, N) ->
Τα contracts αυτά μας λένε το εξής:
\begin{itemize}
\item Η συνάρτηση $server/0$ αρχικά περιμένει να λάβει μια τούπλα, η οποία αποτελείται από ένα atom (το οποίο, όπως
\item Η συνάρτηση $server/0$ αρχικά περιμένει να λάβει μια πλειάδα, η οποία αποτελείται από ένα atom (το οποίο, όπως
φαίνεται από τον κώδικα, περιγράφει την αριθμητική πράξη που ο client θέλει να εκτελεστεί εκ μέρους του από τον
server), και ένα $pid$, το οποίο αντιστοιχεί στο process του client. Το επόμενο βήμα, ασχέτως με τα περιεχόμενα
της τούπλας που θα λάβει, θα είναι να περιμένει και πάλι να λάβει μια τούπλα, η οποία αποτελείται από ένα $atom$,
της πλειάδας που θα λάβει, θα είναι να περιμένει και πάλι να λάβει μια πλειάδα, η οποία αποτελείται από ένα $atom$,
το $pid$ που έλαβε και στο προηγούμενο μήνυμα, και έναν αριθμό, στις δύο περιπτώσεις ακεραίου τύπου. Το επόμενο
βήμα εξαρτάται από το path που έχουμε διανύσει ως τώρα:
\begin{itemize}
......@@ -1307,20 +1339,20 @@ sqrt_client(Server, N) ->
απάντηση στο $pid$ του client, η οποία αποτελείται από μια τουπλα που περιέχει ένα $atom$, το $pid$ του
server, και το αποτέλεσμα της πράξης
\item Αν από την άλλη ο client αιτείται εκτέλεση πράξης εύρεσης τετραγωνικής ρίζας, τότε ο server και πάλι
θα αποστείλει μια τούπλα στον client, ίδιου τύπου με αυτήν της προηγούμενης περίπτωσης.
θα αποστείλει μια πλειάδα στον client, ίδιου τύπου με αυτήν της προηγούμενης περίπτωσης.
\item Σε περίπτωση που το αίτημα είναι για άθροιση αριθμών, τότε ο server θα περιμένει ένα ακόμη μήνυμα απο
τον client, με τον δεύτερο τελεσταίο της πράξης. Μόλις λάβει και αυτόν, θα επιστρέψει μια τούπλα
τον client, με τον δεύτερο τελεσταίο της πράξης. Μόλις λάβει και αυτόν, θα επιστρέψει μια πλειάδα
αντίστοιχη με τις προηγούμενες δύο.
\end{itemize}
Και στις τρεις περιπτώσεις, η εκτέλεση του server συνεχίζεται με την αναδρομική κλήση της $server/0$.
\item Η συνάρτηση $sum\_client/2$ υλοποιεί έναν client ο οποίος αιτείται μόνο πράξεις άθροισης από τον server.
Στέλνει τρία μηνύματα στη σειρά, εκ των οποίων το πρώτο περιέχει ένα $atom sum$ και το $pid$ του, και τα επόμενα
δύο περιέχουν ένα $atom$, το $pid$ του και από έναν ακέραιο, και περιμένει να λάβει πίσω μια τούπλα που
δύο περιέχουν ένα $atom$, το $pid$ του και από έναν ακέραιο, και περιμένει να λάβει πίσω μια πλειάδα που
περιέχει ένα $atom$, στην προκειμένη το $res$, το $pid$ του server, και το αποτέλεσμα της πράξης που
αιτήθηκε. Ακολούθως, καλείται αναδρομικά η $sum\_client/2$.
\item Η συνάρτηση $neg\_client/2$ υλοποιεί έναν client που αιτείται συνεχώς πράξεις αντιστροφής προσήμου από τον
server. Αποστέλει στην αρχή ένα μήνυμα που περιέχει το $atom neg$, ακολουθούμενο από το $pid$ του negation
client, και στη συνέχεια αποστέλει μια τούπλα που περιέχει ένα $atom$, το $pid$ του, και τον αριθμό που θα
client, και στη συνέχεια αποστέλει μια πλειάδα που περιέχει ένα $atom$, το $pid$ του, και τον αριθμό που θα
τελέσει χρέη τελεσταίου. Ακολούθως, περιμένει απάντηση με ένα $atom$ (το $res$), το $pid$ του server, και το
αποτέλεσμα της πράξης, πρωτού καλέσει αναδρομικά τον εαυτό της.
\item Η συνάρτηση $sqrt\_client/2$ συμπεριφέρεται με ακριβώς τον ίδιο τρόπο όπως η $neg\_client/2$, με τη διαφορά
......@@ -1357,7 +1389,7 @@ sqrt_client(Server, N) ->
Αναλύοντας την υλοποίηση αυτή με το σύστημά μας, παίρνουμε αρχικά τους συμπερασμένους τύπους διεργασιών των συναρτήσεων
που αποτελούν το πρόγραμμα:
\begin{lstlisting}[language=Erlang, caption=Inferred Session Types of Arithmetic Server, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=Inferred Session Types of Arithmetic Server, basicstyle=\ttfamily\small]
{server,0} : "u (4). Of<any; ?(atom x {atom, pid, (atom x atom)}).
?(atom x {atom, pid, (atom x atom)} x number).
?(atom x {atom, pid, (atom x atom)} x number).
......@@ -1391,7 +1423,7 @@ sqrt_client(Server, N) ->
Ακολούθως, προσπαθούμε να δούμε αν όντως μπορεί να διαδραματιστεί επιτυχής επικοινωνία ανάμεσα στα endpoints μας.
Αρχικά, έχουμε τον server με τον client άθροισης, $sum\_client/2$.
\begin{lstlisting}[language=Erlang, caption=server/0 and sum\_client/2, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=server/0 and sum\_client/2, basicstyle=\scriptsize]
{server,0} and {sum_client,2} are peers
The matching sequences are:
[{{recv,any,{tuple,[atom,{union,[atom,pid,{tuple,[atom,atom]}]}]}},
......@@ -1409,7 +1441,7 @@ The matching sequences are:
Τα πράγματα για τους $neg\_client/2$ και $sqrt\_client/2$ είναι ελαφρώς διαφορετικά:
\begin{lstlisting}[language=Erlang, caption=neg\_client/2 and sqrt\_client/2, basicstyle=\tiny]
\begin{lstlisting}[language=Erlang, caption=neg\_client/2 and sqrt\_client/2, basicstyle=\scriptsize]
{server,0} and {neg_client,2} are peers
The matching sequences are:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment