Skip to content

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

Add content

parent 4e3b942b
Show whitespace changes
Inline Side-by-side
Showing with 1577 additions and 548 deletions
.gitignore
View file @ a72ddd16
...@@ -44,3 +44,5 @@ Thumbs.db* ...@@ -44,3 +44,5 @@ Thumbs.db*
# The example PDF file # The example PDF file
/test.pdf /test.pdf
.vimrc
Makefile
View file @ a72ddd16
.PHONY: FORCE default clean distclean .PHONY: FORCE default clean distclean
FILE=test FILE=thesis
export SHELL=/bin/bash export SHELL=/bin/bash
export TEXINPUTS:=.:./Styles//:${TEXINPUTS} export TEXINPUTS:=.:./Styles//:${TEXINPUTS}
......
assets/recursive_client_2_simple.graphml 0 → 100644
View file @ a72ddd16
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:java="http://www.yworks.com/xml/yfiles-common/1.0/java" xmlns:sys="http://www.yworks.com/xml/yfiles-common/markup/primitives/2.0" xmlns:x="http://www.yworks.com/xml/yfiles-common/markup/2.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:y="http://www.yworks.com/xml/graphml" xmlns:yed="http://www.yworks.com/xml/yed/3" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd">
<!--Created by yEd 3.18.1-->
<key attr.name="Description" attr.type="string" for="graph" id="d0"/>
<key for="port" id="d1" yfiles.type="portgraphics"/>
<key for="port" id="d2" yfiles.type="portgeometry"/>
<key for="port" id="d3" yfiles.type="portuserdata"/>
<key attr.name="url" attr.type="string" for="node" id="d4"/>
<key attr.name="description" attr.type="string" for="node" id="d5"/>
<key for="node" id="d6" yfiles.type="nodegraphics"/>
<key for="graphml" id="d7" yfiles.type="resources"/>
<key attr.name="url" attr.type="string" for="edge" id="d8"/>
<key attr.name="description" attr.type="string" for="edge" id="d9"/>
<key for="edge" id="d10" yfiles.type="edgegraphics"/>
<graph edgedefault="directed" id="G">
<data key="d0"/>
<node id="n0">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="193.51999999999998" width="193.51999999999998" x="290.9499999999998" y="235.75"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="171.40234375" x="11.058828124999991" xml:space="preserve" y="87.40941406249999">v0: pid(1) ! atom x self x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<edge id="e0" source="n0" target="n0">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0">
<y:Point x="387.7099999999998" y="182.99"/>
</y:Path>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
</graph>
<data key="d7">
<y:Resources/>
</data>
</graphml>
assets/server_0_simple.graphml 0 → 100644
View file @ a72ddd16
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:java="http://www.yworks.com/xml/yfiles-common/1.0/java" xmlns:sys="http://www.yworks.com/xml/yfiles-common/markup/primitives/2.0" xmlns:x="http://www.yworks.com/xml/yfiles-common/markup/2.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:y="http://www.yworks.com/xml/graphml" xmlns:yed="http://www.yworks.com/xml/yed/3" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd">
<!--Created by yEd 3.18.1-->
<key attr.name="Description" attr.type="string" for="graph" id="d0"/>
<key for="port" id="d1" yfiles.type="portgraphics"/>
<key for="port" id="d2" yfiles.type="portgeometry"/>
<key for="port" id="d3" yfiles.type="portuserdata"/>
<key attr.name="url" attr.type="string" for="node" id="d4"/>
<key attr.name="description" attr.type="string" for="node" id="d5"/>
<key for="node" id="d6" yfiles.type="nodegraphics"/>
<key for="graphml" id="d7" yfiles.type="resources"/>
<key attr.name="url" attr.type="string" for="edge" id="d8"/>
<key attr.name="description" attr.type="string" for="edge" id="d9"/>
<key for="edge" id="d10" yfiles.type="edgegraphics"/>
<graph edgedefault="directed" id="G">
<data key="d0"/>
<node id="n0">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="164.08000000000004" width="164.08000000000004" x="89.73749999999995" y="165.9375"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="152.734375" x="5.672812500000006" xml:space="preserve" y="72.68941406250002">v0: ? atom x pid(1) x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<node id="n1">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="152.88000000000002" width="152.88000000000002" x="306.07499999999993" y="165.9375"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="138.068359375" x="7.405820312499998" xml:space="preserve" y="67.0894140625">v1: ? atom x pid x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<node id="n2">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="165.68" width="165.68" x="88.93749999999997" y="371.61749999999995"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="152.734375" x="6.472812500000003" xml:space="preserve" y="73.48941406250003">v2: ? atom x pid(1) x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<node id="n3">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="190.48000000000005" width="190.48000000000005" x="76.53749999999995" y="578.8974999999999"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="171.40234375" x="9.538828125000009" xml:space="preserve" y="85.88941406250001">v3: pid(1) ! atom x self x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<edge id="e0" source="n0" target="n2">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
<edge id="e1" source="n2" target="n3">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
<edge id="e2" source="n3" target="n0">
<data key="d9"/>
<data key="d10">
<y:ArcEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0">
<y:Point x="65.23748779296875" y="461.0574951171875"/>
</y:Path>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:Arc height="106.54000854492188" ratio="1.0" type="fixedRatio"/>
</y:ArcEdge>
</data>
</edge>
<edge id="e3" source="n3" target="n1">
<data key="d9"/>
<data key="d10">
<y:BezierEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0">
<y:Point x="-194.22516666666664" y="387.5991"/>
<y:Point x="6.841500000000082" y="-62.00090000000003"/>
</y:Path>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
</y:BezierEdge>
</data>
</edge>
<edge id="e4" source="n1" target="n1">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0">
<y:Point x="390.51499999999993" y="122.69749999999996"/>
</y:Path>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
<edge id="e5" source="n1" target="n0">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
</graph>
<data key="d7">
<y:Resources/>
</data>
</graphml>
assets/simple_client_1_simple.graphml 0 → 100644
View file @ a72ddd16
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:java="http://www.yworks.com/xml/yfiles-common/1.0/java" xmlns:sys="http://www.yworks.com/xml/yfiles-common/markup/primitives/2.0" xmlns:x="http://www.yworks.com/xml/yfiles-common/markup/2.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:y="http://www.yworks.com/xml/graphml" xmlns:yed="http://www.yworks.com/xml/yed/3" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd">
<!--Created by yEd 3.18.1-->
<key attr.name="Description" attr.type="string" for="graph" id="d0"/>
<key for="port" id="d1" yfiles.type="portgraphics"/>
<key for="port" id="d2" yfiles.type="portgeometry"/>
<key for="port" id="d3" yfiles.type="portuserdata"/>
<key attr.name="url" attr.type="string" for="node" id="d4"/>
<key attr.name="description" attr.type="string" for="node" id="d5"/>
<key for="node" id="d6" yfiles.type="nodegraphics"/>
<key for="graphml" id="d7" yfiles.type="resources"/>
<key attr.name="url" attr.type="string" for="edge" id="d8"/>
<key attr.name="description" attr.type="string" for="edge" id="d9"/>
<key for="edge" id="d10" yfiles.type="edgegraphics"/>
<graph edgedefault="directed" id="G">
<data key="d0"/>
<node id="n0">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="193.51999999999998" width="193.51999999999998" x="115.47499999999991" y="191.875"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="171.40234375" x="11.058828124999991" xml:space="preserve" y="87.40941406249999">v0: pid(1) ! atom x self x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<node id="n1">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="193.51999999999998" width="193.51999999999998" x="115.47499999999988" y="437.7950000000001"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="171.40234375" x="11.058828124999991" xml:space="preserve" y="87.40941406249999">v1: pid(1) ! atom x self x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<node id="n2">
<data key="d5"/>
<data key="d6">
<y:ShapeNode>
<y:Geometry height="193.51999999999998" width="193.51999999999998" x="115.47499999999991" y="683.7150000000001"/>
<y:Fill hasColor="false" transparent="false"/>
<y:BorderStyle color="#000000" raised="false" type="line" width="1.0"/>
<y:NodeLabel alignment="center" autoSizePolicy="content" fontFamily="Dialog" fontSize="12" fontStyle="plain" hasBackgroundColor="false" hasLineColor="false" height="18.701171875" horizontalTextPosition="center" iconTextGap="4" modelName="custom" textColor="#000000" underlinedText="true" verticalTextPosition="bottom" visible="true" width="152.734375" x="20.39281249999999" xml:space="preserve" y="87.40941406249999">v2: ? atom x pid(1) x integer<y:LabelModel><y:SmartNodeLabelModel distance="4.0"/></y:LabelModel><y:ModelParameter><y:SmartNodeLabelModelParameter labelRatioX="0.0" labelRatioY="0.0" nodeRatioX="0.0" nodeRatioY="0.0" offsetX="0.0" offsetY="0.0" upX="0.0" upY="-1.0"/></y:ModelParameter></y:NodeLabel>
<y:Shape type="ellipse"/>
</y:ShapeNode>
</data>
</node>
<edge id="e0" source="n0" target="n1">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
<edge id="e1" source="n1" target="n2">
<data key="d9"/>
<data key="d10">
<y:PolyLineEdge>
<y:Path sx="0.0" sy="0.0" tx="0.0" ty="0.0"/>
<y:LineStyle color="#000000" type="line" width="1.0"/>
<y:Arrows source="none" target="standard"/>
<y:BendStyle smoothed="false"/>
</y:PolyLineEdge>
</data>
</edge>
</graph>
<data key="d7">
<y:Resources/>
</data>
</graphml>
test.bib deleted 100644 → 0
View file @ 4e3b942b
@article{church-1932-spfl,
author="A. Church",
title="A Set of Postulates for the Foundations of Logic",
journal="Annals of Mathematics",
volume=33,
pages="346--366",
number=1,
year=1932
}
@article{church-1933-spfl,
author="A. Church",
title="A Set of Postulates for the Foundations of Logic",
journal="Annals of Mathematics",
volume=34,
pages="839--864",
number=2,
year=1933
}
@phdthesis{girard-1972-ifecaos,
author="J.-Y. Girard",
title="Interpr{\'e}tation Fonctionelle et {\'E}limination des "
# "Coupures Dans l'Arithm{\'e}tique d'Ordre Sup{\'e}rieur",
school="Universit{\'e} Paris 7",
year=1972
}
@article{girard-1989-pt,
author="J.-Y. Girard and Y. Lafont and P. Taylor",
title="Proofs and Types",
journal="Tracks in Theoretical Computer Science",
year=1989
}
@inproceedings{reynolds-1974-ttts,
author="John. C. Reynolds",
title="Towards a Theory of Type Systems",
booktitle="Lecture Notes in Computer Science",
year=1974,
editor="Ehring et al.",
volume=19,
pages="408--425",
publisher="Springer-Verlag"
}
@article{boehm-1985-astlpta,
author="C. B{\"o}hm and A. Bernarducci",
title="Automatic Synthesis of Typed $\lambda$-Programs on Term "
# "Algebras",
journal="Theoretical Computer Science",
volume=39,
number="2--3",
pages="135--154",
month=aug,
year=1985
}
@phdthesis{paulin-1989-epscc,
author="C. Paulin-Mohring",
title="Extraction de Programmes Dans le Calcul des Constructions",
month=jan,
school="Universit{\'e} Paris 7",
year=1989,
url="http://www.lri.fr/~paulin/these.ps.gz"
}
@inproceedings{pfenning-1990-pmfps,
author="F. Pfenning and C. Paulin-Mohring",
booktitle="Proceedings of Mathematical Foundations of "
# "Programming Semantics",
note="technical report CMU-CS-89-209",
publisher="Springer-Verlag",
address = "Berlin",
series="Lecture Notes in Computer Science",
volume=442,
title="Inductively defined types in the Calculus of Constructions",
year=1990
}
@incollection{paulin-1993-iddcrp,
author= "Christine Paulin-Mohring",
title = "Inductive Definitions in the System {Coq}: Rules and Properties",
booktitle = "Proceedings of the 1st Int.\ Conf.\ on Typed Lambda Calculi "
# "and Applications, {TLCA}'93, Utrecht, The Netherlands, "
# "16--18 March 1993",
volume = 664,
publisher = "Springer-Verlag",
address = "Berlin",
editor = "M. Bezem and J. F. Groote",
pages = "328--345",
year = 1993,
url = "citeseer.nj.nec.com/paulin-mohring92inductive.html"
}
@InProceedings{shao-2002-tscb,
author = "Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou",
title = "A Type System for Certified Binaries",
booktitle = "Proceedings of the 29th Annual Symposium on Principles of "
# "Programming Languages (POPL 2002)",
year = 2002,
pages = "217--232",
address = "Portland, OR, USA",
month = jan
}
@InProceedings{sellink-1994-vpaptt,
author = "M. P. A. Sellink",
title = "Verifying process algebra proofs in type theory",
booktitle = "Proceedings of the International Workshop on Semantics "
# " of Specipication Languages (SOSL 1993)",
year = 1994,
editor = "D. J. Andrews and J. F. Groote and C. A. Middelburg",
publisher = "Springer"
}
@inproceedings{necula-1997-pcc,
author="G. Necula",
title="Proof-Carrying Code",
booktitle="Proceedings of the 24th Annual Symposium on Principles of "
# "Programming Languages (POPL 1997)",
pages="106--119",
publisher="ACM Press",
address="New York",
year=1997,
month=jan
}
@inproceedings{necula-1996-skertc,
author="G. Necula and P. Lee",
title="Safe Kernel Extensions without Run-Time Checking",
booktitle="Proceedings of the 2nd USENIX Symposium on Operating "
# "System Design and Implementation",
year="1996",
publisher="USENIX Association",
pages="229--243"
}
@phdthesis{necula-1998-cp,
title = "Compiling with Proofs",
author = "G. Necula",
school = "Carnegie Mellon University",
year = 1998,
month=sep,
number = "CMU-CS-98-154"
}
@inproceedings{appel-2000-smtmipcc,
author="Andrew W. Appel and Amy P. Felty",
title="A Semantic Model of Types and Machine Instructions for "
# "Proof-Carrying Code",
booktitle="Proceedings of the 27th Annual Symposium on Principles of "
# "Programming Languages (POPL 2000)",
year=2000,
publisher = "ACM Press",
pages="243--253"
}
@InProceedings{appel-2001-fpcc,
author = "A. W. Appel",
title = "Foundational Proof-Carrying Code",
booktitle = "Proceedings of the 16th Annual IEEE Symposium on "
# "Logic in Computer Science",
pages = "247--258",
year = 2001,
month = jun
}
@inproceedings{harper-1995-cpita,
author="Robert Harper and Greg Morrisett",
title="Compiling Polymorphism Using Intensional Type Analysis",
booktitle="Proceedings of the 22nd Annual Symposium on Principles of "
# "Programming Languages (POPL 1995)",
publisher="ACM Press",
year="1995",
pages="130--141"
}
@inproceedings{morrisett-1998-sftal,
author="Greg Morrisett and David Walker and Karl Crary and Neal Glew",
title="From {S}ystem {F} to Typed Assembly Language",
booktitle="Proceedings of the 25th Annual Symposium on Principles of "
# "Programming Languages (POPL 1998)",
pages="85--97",
publisher="ACM Press",
year=1998,
month=jan
}
test.tex deleted 100644 → 0
View file @ 4e3b942b
\documentclass[diploma]{softlab-thesis}
%%%
%%% The document
%%%
\begin{document}
%%% Title page
\frontmatter
\title{Σχεδίαση και Υλοποίηση μιας Καταπληκτικής Γλώσσας Προγραμματισμού}
\author{Γεράσιμος Τ. Ιωάννου}
\date{Ιούλιος 2014}
\datedefense{17}{7}{2014}
\supervisor{Νικόλαος Σ. Παπασπύρου}
\supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}
\committeeone{Νικόλαος Σ. Παπασπύρου}
\committeeonepos{Αν. Καθηγητής Ε.Μ.Π.}
\committeetwo{Πέτρος X. Παπαδόπουλος}
\committeetwopos{Επίκ. Καθηγητής Ε.Μ.Π.}
\committeethree{Γεώργιος X. Νικολάου}
\committeethreepos{Καθηγητής Ε.Κ.Π.Α.}
\TRnumber{CSD-SW-TR-42-14} % number-year, ask nickie for the number
\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}
\maketitle
%%% Abstract, in Greek
\begin{abstractgr}%
Σκοπός της παρούσας εργασίας είναι αφενός η σχεδίαση μίας απλής
γλώσσας υψηλού επιπέδου με υποστήριξη για προγραμματισμό με
αποδείξεις, αφετέρου η υλοποίηση ενός μεταγλωττιστή για τη γλώσσα
αυτή που θα παράγει κώδικα για μία γλώσσα ενδιάμεσου επιπέδου
κατάλληλη για δημιουργία πιστοποιημένων εκτελέσιμων.
Στη σημερινή εποχή, η ανάγκη για αξιόπιστο και πιστοποιημένα ασφαλή
κώδικα γίνεται διαρκώς ευρύτερα αντιληπτή. Τόσο κατά το παρελθόν όσο
και πρόσφατα έχουν γίνει γνωστά προβλήματα ασφάλειας και
συμβατότητας προγραμμάτων που είχαν ως αποτέλεσμα προβλήματα στην
λειτουργία μεγάλων συστημάτων και συνεπώς οικονομικές επιπτώσεις
στους οργανισμούς που τα χρησιμοποιούσαν. Τα προβλήματα αυτά
οφείλονται σε μεγάλο βαθμό στην έλλειψη δυνατότητας προδιαγραφής και
απόδειξης της ορθότητας των προγραμμάτων που χαρακτηρίζει τις
σύγχρονες γλώσσες προγραμματισμού. Για το σκοπό αυτό, έχουν προταθεί
συστήματα πιστοποιημένων εκτελέσιμων, στα οποία έχουμε τη δυνατότητα
να προδιαγράφουμε την ορθότητα των προγραμμάτων, και να παρέχουμε
μία τυπική απόδειξη αυτής, η οποία μπορεί να ελεγχθεί μηχανιστικά
πριν το χρόνο εκτέλεσης.
Τα συστήματα που έχουν προταθεί είναι ενδιάμεσου επιπέδου οπότε η
διαδικασία προγραμματισμού σε αυτά είναι ιδιαίτερα πολύπλοκη. Οι
γλώσσες υψηλού επιπέδου που συνοδεύουν αυτά τα συστήματα, ενώ είναι
ιδιαίτερα εκφραστικές, παραμένουν δύσκολες στον προγραμματισμό. Μία
απλούστερη γλώσσα υψηλού επιπέδου, όπως αυτή που προτείνουμε σε αυτή
την εργασία, θα επέτρεπε ευρύτερη εξάπλωση του συγκεκριμένου
ιδιώματος προγραμματισμού.
Στη γλώσσα που προτείνουμε, ο προγραμματιστής προδιαγράφει τη μερική
ορθότητα του προγράμματος, δίνοντας προσυνθήκες και μετασυνθήκες για
τις παραμέτρους και τα αποτελέσματα των συναρτήσεων που ορίζει.
Επίσης δίνει ένα σύνολο θεωρημάτων βάσει του οποίου κατασκευάζονται
αποδείξεις της ορθής υλοποίησης και χρήσης των συναρτήσεων αυτών. Ως
μέρος της εργασίας, έχουμε υλοποιήσει σε γλώσσα OCaml ένα
μεταφραστή αυτής της γλώσσας στο σύστημα πιστοποιημένων
εκτελέσιμων NFLINT.
Επιτύχαμε να διατηρήσουμε τη γλώσσα κοντά στο ύφος των ευρέως
διαδεδομένων συναρτησιακών γλωσσών, καθώς και να διαχωρίσουμε τη
φάση προγραμματισμού από τη φάση απόδειξης της ορθότητας των
προγραμμάτων. Έτσι ένας μέσος προγραμματιστής μπορεί εύκολα να
προγραμματίζει στη γλώσσα που προτείνουμε με τον τρόπο που ήδη
γνωρίζει, και ένας γνώστης μαθηματικής λογικής να αποδεικνύει σε
επόμενη φάση την μερική ορθότητα των προγραμμάτων. Ως απόδειξη της
πρακτικότητας της προσέγγισης αυτής, παραθέτουμε ένα σύνολο
παραδειγμάτων στη γλώσσα με απόδειξη μερικής ορθότητας.
\begin{keywordsgr}
Γλώσσες προγραμματισμού, Προγραμματισμός με αποδείξεις, Ασφαλείς γλώσσες
προγραμματισμού, Πιστοποιημένος κώδικας.
\end{keywordsgr}
\end{abstractgr}
%%% Abstract, in English
\begin{abstracten}%
The purpose of this diploma dissertation is on one hand the design
of a simple high-level language that supports programming with
proofs, and on the other hand the implementation of a compiler for
this language. This compiler will produce code for an
intermediate-level language suitable for creating certified
binaries.
The need for reliable and certifiably secure code is even more
pressing today than it was in the past. In many cases, security and
software compatibility issues put in danger the operation of large
systems, with substantial financial consequences. The lack of a
formal way of specifying and proving the correctness of programs that
characterizes current programming languages is one of the main reasons
why these issues exist. In order to address this problem, a number of
frameworks with support for certified binaries have recently been
proposed. These frameworks offer the possibility of specifying and
providing a formal proof of the correctness of programs. Such a proof
can easily be checked for validity before running the program.
The frameworks that have been proposed are intermediate-level in
nature, thus the process of programming in these is rather cumbersome.
The high-level languages that accompany some of these frameworks,
while very expressive, are hard to use. A simpler high-level language,
like the one proposed in this dissertation, would enable further use
of this programming idiom.
In the language we propose, the programmer specifies the partial
correctness of a program by annotating function definitions with pre-
and post-conditions that must hold for their parameters and results.
The programmer also provides a set of theorems, based on which proofs
of the proper implementation and use of the functions are constructed.
An implementation in OCaml of a compiler from this language to the
NFLINT certified binaries framework was also completed as part of this
dissertation.
We managed to keep the language close to the feel of the current
widespread functional languages, and also to fully separate the
programming stage from the correctness-proving stage. Thus an average
programmer can program in a familiar way in our language, and later an
expert on formal logic can prove the semi-correctness of a program.
As evidence of the practicality of our design, we provide a number of
examples in our language with full semi-correctness proofs.
\begin{keywordsen}
Programming languages, Programming with proofs, Secure programming
languages, Certified code.
\end{keywordsen}
\end{abstracten}
%%% Acknowledgements
\begin{acknowledgementsgr}
Ευχαριστώ θερμά τον επιβλέποντα καθηγητή αυτής της διατριβής,
κ.~Γιάννη Παπαδάκη, για τη συνεχή καθοδήγηση και εμπιστοσύνη
του. Ευχαριστώ επίσης τα μέλη της συμβουλευτικής επιτροπής,
κ.κ.~Νίκο Παπαδόπουλο και Γιώργο Νικολάου για την πρόθυμη και
πάντα αποτελεσματική βοήθειά τους, τις πολύτιμες συμβουλές και
τις χρήσιμες συζητήσεις που είχαμε. Θέλω να ευχαριστήσω ακόμα
τον συμφοιτητή και φίλο Πέτρο Πετρόπουλο, ο οποίος με βοήθησε σε
διάφορα στάδια αυτής της εργασίας. Θα ήθελα τέλος να ευχαριστήσω
την οικογένειά μου και κυρίως τους γονείς μου, οι οποίοι με
υποστήριξαν και έκαναν δυνατή την απερίσπαστη ενασχόλησή μου τόσο
με την εκπόνηση της διπλωματικής μου, όσο και συνολικά με τις
σπουδές μου.
\end{acknowledgementsgr}
%%% Various tables
\tableofcontents
\listoftables
\listoffigures
%%% Main part of the book
\mainmatter
\chapter{Εισαγωγή}
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
\section{Η γλώσσα προγραμματισμού C}
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
\section{Σημασιολογία γλωσσών προγραμματισμού}
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα \nocite{*} μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα
μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα,
μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα,
μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα
μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα,
μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
\section{Θεωρία πεδίων}
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
Μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα μπλα μπλα μπλα,
μπλα μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα,
μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα,
μπλα, μπλα μπλα μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα
μπλα, μπλα μπλα, μπλα μπλα μπλα, μπλα, μπλα μπλα μπλα.
%%% Bibliography
\bibliographystyle{softlab-thesis}
\bibliography{test}
%%% Appendices
\backmatter
\appendix
\chapter{Ευρετήριο συμβολισμών}
$A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$.
\chapter{Ευρετήριο γλωσσών}
\textbf{Haskell} : η γλώσσα της ζωής μου.
\chapter{Ευρετήριο αριθμών}
42 : life, the universe and everything.
%%% End of document
\end{document}
thesis.bib 0 → 100644
View file @ a72ddd16
@article{church-1932-spfl,
author="A. Church",
title="A Set of Postulates for the Foundations of Logic",
journal="Annals of Mathematics",
volume=33,
pages="346--366",
number=1,
year=1932
}
@article{church-1933-spfl,
author="A. Church",
title="A Set of Postulates for the Foundations of Logic",
journal="Annals of Mathematics",
volume=34,
pages="839--864",
number=2,
year=1933
}
@phdthesis{girard-1972-ifecaos,
author="J.-Y. Girard",
title="Interpr{\'e}tation Fonctionelle et {\'E}limination des "
# "Coupures Dans l'Arithm{\'e}tique d'Ordre Sup{\'e}rieur",
school="Universit{\'e} Paris 7",
year=1972
}
@article{girard-1989-pt,
author="J.-Y. Girard and Y. Lafont and P. Taylor",
title="Proofs and Types",
journal="Tracks in Theoretical Computer Science",
year=1989
}
@inproceedings{reynolds-1974-ttts,
author="John. C. Reynolds",
title="Towards a Theory of Type Systems",
booktitle="Lecture Notes in Computer Science",
year=1974,
editor="Ehring et al.",
volume=19,
pages="408--425",
publisher="Springer-Verlag"
}
@article{boehm-1985-astlpta,
author="C. B{\"o}hm and A. Bernarducci",
title="Automatic Synthesis of Typed $\lambda$-Programs on Term "
# "Algebras",
journal="Theoretical Computer Science",
volume=39,
number="2--3",
pages="135--154",
month=aug,
year=1985
}
@phdthesis{paulin-1989-epscc,
author="C. Paulin-Mohring",
title="Extraction de Programmes Dans le Calcul des Constructions",
month=jan,
school="Universit{\'e} Paris 7",
year=1989,
url="http://www.lri.fr/~paulin/these.ps.gz"
}
@inproceedings{pfenning-1990-pmfps,
author="F. Pfenning and C. Paulin-Mohring",
booktitle="Proceedings of Mathematical Foundations of "
# "Programming Semantics",
note="technical report CMU-CS-89-209",
publisher="Springer-Verlag",
address = "Berlin",
series="Lecture Notes in Computer Science",
volume=442,
title="Inductively defined types in the Calculus of Constructions",
year=1990
}
@incollection{paulin-1993-iddcrp,
author= "Christine Paulin-Mohring",
title = "Inductive Definitions in the System {Coq}: Rules and Properties",
booktitle = "Proceedings of the 1st Int.\ Conf.\ on Typed Lambda Calculi "
# "and Applications, {TLCA}'93, Utrecht, The Netherlands, "
# "16--18 March 1993",
volume = 664,
publisher = "Springer-Verlag",
address = "Berlin",
editor = "M. Bezem and J. F. Groote",
pages = "328--345",
year = 1993,
url = "citeseer.nj.nec.com/paulin-mohring92inductive.html"
}
@InProceedings{shao-2002-tscb,
author = "Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou",
title = "A Type System for Certified Binaries",
booktitle = "Proceedings of the 29th Annual Symposium on Principles of "
# "Programming Languages (POPL 2002)",
year = 2002,
pages = "217--232",
address = "Portland, OR, USA",
month = jan
}
@InProceedings{sellink-1994-vpaptt,
author = "M. P. A. Sellink",
title = "Verifying process algebra proofs in type theory",
booktitle = "Proceedings of the International Workshop on Semantics "
# " of Specipication Languages (SOSL 1993)",
year = 1994,
editor = "D. J. Andrews and J. F. Groote and C. A. Middelburg",
publisher = "Springer"
}
@inproceedings{necula-1997-pcc,
author="G. Necula",
title="Proof-Carrying Code",
booktitle="Proceedings of the 24th Annual Symposium on Principles of "
# "Programming Languages (POPL 1997)",
pages="106--119",
publisher="ACM Press",
address="New York",
year=1997,
month=jan
}
@inproceedings{necula-1996-skertc,
author="G. Necula and P. Lee",
title="Safe Kernel Extensions without Run-Time Checking",
booktitle="Proceedings of the 2nd USENIX Symposium on Operating "
# "System Design and Implementation",
year="1996",
publisher="USENIX Association",
pages="229--243"
}
@phdthesis{necula-1998-cp,
title = "Compiling with Proofs",
author = "G. Necula",
school = "Carnegie Mellon University",
year = 1998,
month=sep,
number = "CMU-CS-98-154"
}
@inproceedings{appel-2000-smtmipcc,
author="Andrew W. Appel and Amy P. Felty",
title="A Semantic Model of Types and Machine Instructions for "
# "Proof-Carrying Code",
booktitle="Proceedings of the 27th Annual Symposium on Principles of "
# "Programming Languages (POPL 2000)",
year=2000,
publisher = "ACM Press",
pages="243--253"
}
@InProceedings{appel-2001-fpcc,
author = "A. W. Appel",
title = "Foundational Proof-Carrying Code",
booktitle = "Proceedings of the 16th Annual IEEE Symposium on "
# "Logic in Computer Science",
pages = "247--258",
year = 2001,
month = jun
}
@inproceedings{harper-1995-cpita,
author="Robert Harper and Greg Morrisett",
title="Compiling Polymorphism Using Intensional Type Analysis",
booktitle="Proceedings of the 22nd Annual Symposium on Principles of "
# "Programming Languages (POPL 1995)",
publisher="ACM Press",
year="1995",
pages="130--141"
}
@inproceedings{morrisett-1998-sftal,
author="Greg Morrisett and David Walker and Karl Crary and Neal Glew",
title="From {S}ystem {F} to Typed Assembly Language",
booktitle="Proceedings of the 25th Annual Symposium on Principles of "
# "Programming Languages (POPL 1998)",
pages="85--97",
publisher="ACM Press",
year=1998,
month=jan
}
thesis.pdf 0 → 100644
View file @ a72ddd16
File added
thesis.tex 0 → 100644
View file @ a72ddd16
\documentclass[diploma]{softlab-thesis}
\usepackage{listings}
\usepackage{trfrac}
\usepackage{amsmath, amssymb, latexsym}
\usepackage[svgnames]{xcolor}
\usepackage{color}
\usepackage{caption}
\DeclareCaptionLabelFormat{algocaption}{Algorithm} % defines a new caption label as Algorithm x.y
\lstnewenvironment{algorithm}[1][] %defines the algorithm listing environment
{
\captionsetup{labelformat=algocaption,labelsep=colon} %defines the caption setup for: it ises label format as the declared caption label above and makes label and caption text to be separated by a ':'
\lstset{ %this is the stype
mathescape=true,
frame=tB,
numbers=left,
numberstyle=\tiny,
basicstyle=\small,
keywordstyle=\color{black}\bfseries\em,
keywords={,input, output, return, datatype, function, in, if, else, foreach, while, begin, end, } %add the keywords you want, or load a language as Rubens explains in his comment above.
numbers=left,
xleftmargin=.04\textwidth,
#1 % this is to add specific settings to an usage of this environment (for instnce, the caption and referable label)
}
}
{}
\lstdefinestyle{erlangCodeStyle}{
basicstyle=\small,
captionpos=bottom,
tabsize=2,
showtabs=false,
numbers=left,
numbersep=5pt,
numberstyle=\tiny\color{gray},
showspaces=false,
showstringspaces=false
}
\newcommand{\mychoose}[2]{\bigl({{#1}\atop#2}\bigr)}
\graphicspath{ {./assets/} }
%%%
%%% The document
%%%
\begin{document}
%%% Title page
\frontmatter
\title{Σχεδίαση και Υλοποίηση ενός Στατικού Συστήματος Τύπων για Επικοινωνούσες Διεργασίες}
\author{Αχιλλέας Μπενετόπουλος}
\date{Ιούλιος 2018}
\datedefense{17}{7}{2018}
\supervisor{Νικόλαος Σ. Παπασπύρου}
\supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}
\committeeone{Νικόλαος Σ. Παπασπύρου}
\committeeonepos{Αν. Καθηγητής Ε.Μ.Π.}
\committeetwo{Γεώργιος Στάμου}
\committeetwopos{Αν. Καθηγητής Ε.Μ.Π.}
\committeethree{Αριστείδης Παγουρτζής}
\committeethreepos{Αν. Καθηγητής Ε.Μ.Π.}
\TRnumber{CSD-SW-TR-42-14} % number-year, ask nickie for the number
\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}
\maketitle
%%% Abstract, in Greek
%%% TODO
\begin{abstractgr}%
\setlength{\parskip}{1em}
Κινούμαστε όλο και περισσότερο προς κατανεμημένα προγραμματιστικά μοντέλα. Τα περισσότερα σύγχρονα συστήματα λογισμικού
είναι κατανεμημένα και ταυτόχρονα, που σημαίνει ότι αποτελούνται από διάφορα κομμάτια, το καθένα από τα οποία εκτελεί
ένα σύνολο από "εσωτερικές" σε αυτά λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
υποσύνολο των υπολοίπων για να τις εκτελέσουν, λόγο διαφόρων εξαρτήσεων. Αυτό σημαίνει ότι η επικοινωνία μεταξύ των
κομματιών αυτών ανάγεται σε ένα κρίσιμο κομμάτι του συστήματος, και η ορθότητα της επικοινωνίας αυτής αποτελεί μια
απαραίτητη προϋπόθεση για την ορθότητα του όλου συστήματος.
Παρουσιάζουμε ένα στατικό σύστημα τύπων συνεδρίας για Erlang, το οποίο ελπίζουμε ότι θα εξυπηρετήσει διττό σκοπό:
\setlength{\parskip}{0em}
\begin{itemize}
\item πρώτον, θα δείξει ότι ουσιώδης στατικός έλεγχος τύπων συνεδρίας είναι εφαρμόσιμος για μια δυναμική γλώσσα
προγραμματισμού, και
\item δεύτερον, θα αποτελέσει θεμέλιο για ένα εργαλείο αρκετά ισχυρό και χρήσιμο για να γίνει τελικά κομμάτι της
εργαλειοθήκης ενός προγραμματιστή κατά τη φάση ανάπτυξης ενός έργου
\end{itemize}
\begin{keywordsgr}
Γλώσσες προγραμματισμού, Τύποι Συνεδριών, Συστήματα Τύπων, Συστήματα Επιδράσεων, Ταυτοχρονισμός.
\end{keywordsgr}
\end{abstractgr}
%%% Abstract, in English
%%% TODO
\begin{abstracten}%
\setlength{\parskip}{1em}
We are increasingly moving towards distributed programming models. Most software systems are distributed and concurrent,
meaning that they are composed of various components, each of them performing a certain set of self-contained operations simultaneously
with all the others, but all of
them relying on a subset of the others to progress with their work, due to data dependencies and the like. This means that communication
between the components is nothing less than a critical part of the system, and its correctness therefore a prerequisite
to the correctness of the system as a whole.
We present a static session type checking tool for Erlang, which we hope will serve a twofold purpose:
\setlength{\parskip}{0em}
\begin{itemize}
\item firstly, show that meaningful static session type checking is viable for a dynamic programming language, and
\item secondly, become a foundation for a tool that would be useful and powerful enough to eventually become part of a
programmer's toolchain during a project's development lifecycle
\end{itemize}
\begin{keywordsen}
Programming languages, Session Types, Type systems, Effect Systems, Concurrency.
\end{keywordsen}
\end{abstracten}
%%% Acknowledgements
%%% TODO
\begin{acknowledgementsgr}
Not a placeholder
\end{acknowledgementsgr}
%%% Various tables
\tableofcontents
\listoftables
\listoffigures
%%% Main part of the book
\mainmatter
\chapter{Εισαγωγή}
Τα κατανεμημένα προγραμματιστικά μοντέλα αποκτούν όλο και μεγαλύτερη δημοτικότητα στο σύγχρονο κόσμο της βιομηχανίας
παραγωγής λογισμικού. Πολλά σύγχρονα συστήματα που πρέπει να ανταποκρίνονται σε υψηλούς φόρτους εργασίας με ισχυρές
απαιτήσεις ως προς την αξιοπιστία και τη διαθεσιμότητά τους
είναι κατανεμημένα και ταυτόχρονα, που σημαίνει ότι αποτελούνται από διάφορα κομμάτια, το καθένα από τα οποία εκτελεί
ένα σύνολο από "εσωτερικές" σε αυτό λειτουργίες συγχρόνως με τα υπόλοιπα, τη στιγμή όμως που όλα τους εξαρτώνται από ένα
υποσύνολο των υπολοίπων για να τους παρέχουν πληροφορίες προκειμένου να φέρουν τη δουλειά τους εις πέρας με επιτυχία.
Αυτό σημαίνει ότι η επικοινωνία μεταξύ των
κομματιών αυτών ανάγεται σε ένα κρίσιμο κομμάτι του συστήματος, και ότι η ορθότητα της επικοινωνίας αυτής αποτελεί μια
απαραίτητη προϋπόθεση για την ορθότητα του όλου συστήματος.
Προκειμένου να καθορίσουμε τα μοτίβα επικοινωνίας που θεωρούνται αποδεκτά στα πλαίσια των εφαρμογών μας, ορίζουμε
\textit{πρωτόκολλα} επικοινωνίας, δηλαδή προσπαθούμε να προσδιορίσουμε τους τύπους των μηνυμάτων που ανταλλάσονται, πότε
κατα τη διάρκεια της επικοινωνίας εμφανίζονται αυτά τα μηνύματα, και ανάμεσα σε ποια κομμάτια του συστήματος
αυτά ανταλλάσονται. Συνεπώς, μπορούμε να εκφράσουμε την ορθότητα της επικοινωνίας μεταξύ των επιμέρους συστημάτων ως τη
\textit{συμμόρφωση} σε αυτό το πρωτόκολλο από τους συμμετέχοντες στην επικοινωνία. Οι τύποι συνεδριών μας επιτρέπουν να
εκφράσουμε αυτά τα πρωτόκολλα επικοινωνίας, καθως και τις υλοποιήσεις τους από τα άκρα αυτών, με μια μορφή που
πηγάζει από τη θεωρία τύπων, και κατ'επέκταση να επαληθεύσουμε την ορθότητα της επικοινωνίας εφαρμόζοντας μεθόδους από
τον χώρο της θεωρίας τύπων.
Σε αυτήν την εργασία διερευνούμε την αποτελεσματικότητα ενός στατικού συστήματος τύπων δυαδικών συνεδριών για την Erlang,
μια γλώσσα προγραμματισμού για την οποία ο ταυτοχρονισμός αποτελεί κύριο χαρακτηριστικό. Επιχειρούμε να δουλέψουμε με
ένα υποσύνολο της γλώσσας το οποίο, αν και περιορισμένο, θεωρούμε ότι είναι ουσιώδες, αποκλείοντας μόνο εξωτικούς
εγγενείς τύπους δεδομένων της γλώσσας, καθώς και συναρτήσεις υψηλότερης τάξης.
\section{Στόχοι της παρούσας εργασίας}
Σκοπός της παρούσας εργασίας είναι η μελέτη των συστημάτων τύπων συνεδριών, και η διερεύνηση της αποτελεσματικότητας ενός
στατικού συστήματος τύπων δυαδικών συνεδριών για την Erlang, μια συναρτησιακή γλώσσα προγραμματισμού με δυναμικό σύστημα τύπων,
η οποία παρέχει ισχυρούς μηχανισμούς ταυτοχρονισμού.
Στη βιβλιογραφία υπάρχει ένας αριθμός από υλοποιήσεις μηχανισμών χρόνου εκτέλεσης για την παρακολούθηση της επικοινωνίας μεταξύ διεργασιών
σε γλώσσες με δυναμικό σύστημα τύπων όπως η Erlang [reference to Python's SPY, reference to Fowler's implementation]. Στη βάση τους, όλες χτίζουν
πάνω στη γλώσσα Scribble, η οποία είναι μια DSL για την περιγραφή πρωτοκόλλων
επικοινωνίας. Στη δική μας δουλειά, επιχειρούμε να κατασκευάσουμε ένα σύστημα στατικής ανάλυσης, το οποίο μπορεί να:
\begin{itemize}
\item Συμπεράνει τους τύπους συνεδριών των συναρτήσεων που αποτελούν ένα πρόγραμμα.
\item Εξακριβώσει τη συμμόρφωσή τους με το πρωτόκολλο που πρέπει να υλοποιούν.
\item Επαληθεύσει ότι δύο διεργασίες αποτελούν πράγματι τα δύο "άκρα" ενός δυαδικού πρωτοκόλλου επικοινωνίας.
\end{itemize}
\section{Σύνοψη της εργασίας}
\setlength{\parskip}{1em}
Στο κεφάλαιο 2 παρουσιάζουμε τη γλώσσα Erlang, και όλες τις πληροφορίες που είναι απαραίτητες για την κατανόηση του
τρόπου λειτουργίας του συστήματός μας. Εξηγούμε τι είναι η Erlang, και για ποιο λόγο ένα σύστημα τύπων συνεδρίας έχει
ιδιαίτερη αξία στα πλαίσια αυτής της γλώσσας. Καθώς ο συμπερασμός τύπων συνεδρίας βασίζεται ιδιαίτερα στο σύστημα τύπων της
γλώσσας, θα πραγματοποιήσουμε μια παρουσίαση αυτού, καθώς και του Dialyzer, του εργαλείου (μέρος του OTP) το οποίο
χρησιμοποιούμε για τον συμπερασμό των τύπων δεδομένων των προγραμμάτων που αναλύουμε.
Στο κεφάλαιο 3 πραγματοποιούμε μια παρουσίαση των συστημάτων τύπων και επιδράσεων (type and effect systems), τα οποία
αποτελούν μια επέκταση των κλασσικών συστημάτων τύπων με έναν τρόπο περιγραφής των παρενεργειών που ενδέχεται να έχει
ένα κομμάτι κώδικά.
Στο κεφάλαιο 4 παρουσιάζουμε τη θεωρία και την υπάρχουσα δουλειά πίσω από τα συστήματα τύπων συνεδρίας.
Στο κεφάλαιο 5 αναλύουμε το σύστημα που υλοποιήσαμε.
Στο κεφάλαιο 6 παρουσιάζουμε μερικά παραδείγματα χρήσης του συστήματός μας. Τα παραδείγματα αυτά αποτελούνται τόσο από
σχετικά απλουστευμένα προγράμματα, τα οποία είναι τυποποιημένα στη σχετική βιβλιογραφία, αλλά και παραδείγματα
προσαρμοσμένα στο να αναδείξουν τα προτερήματα της υλοποίησής μας.
Τέλος, στο κεφάλαιο 7 προσφέρουμε μερικά συμπεράσματα που προέκυψαν από την υλοποίηση του συστήματος αυτού, αλλά και τα
πειράματά μας. Επιπλέον, εκθέτουμε μερικές ιδέες για μελλοντική δουλειά πάνω στο συγκεκριμένο αντικείμενο.
\setlength{\parskip}{0em}
\chapter{Το σύστημα Erlang/OTP}
\section{Η γλώσσα προγραμματισμού Erlang}
Η Erlang είναι μια συναρτησιακή γλώσσα προγραμματισμού, η οποία σχεδιάσθηκε τη δεκαετία του 1980 στο Eργαστήριο Επιστήμης Υπολογιστών της Ericsson.
Αρχικά προοριζόταν για προγραμματισμό συστημάτων και εφαρμογών στον τομέα των τηλεπικοινωνιών, και κατα συνέπεια έπρεπε
να ανταποκρίνεται στις απαιτήσεις αυτής της βιομηχανίας για την ανάπτυξη κατανεμημένων συστημάτων υψηλού επιπέδου
παραλληλισμού, τα οποία επιδεικνύουν υψηλή ανοχή σε σφάλματα. Έκτοτε η χρήση της έχει διαδωθεί και σε βιομηχανίες
που μοιράζονται τις ίδιες λειτουργικές απαιτήσεις, όπως η τραπεζική, οι επικοινωνίες πραγματικού χρόνου (WhatsApp), κα.
To OTP είναι μια συλλογή εργαλείων, βιβλιοθηκών, middleware και αρχών σχεδιασμού για προγράμμτα Erlang. Είναι
αναπόσπαστο κομμάτι της διανομής ελεύθερου κώδικα της Erlang. Μερικά από τα περιεχόμενά του είναι:
\begin{itemize}
\item Ένα σύστημα χρόνου εκτέλεσης (εικονική μηχανή), ο BEAM
\item Ένας μεταγλωττιστής σε κώδικα μηχανής
\item Ένα εργαλείο στατικής ανάλυσης, ο Dialyzer, στο οποίο θα αναφερθούμε παρακάτω
\end{itemize}
\section{Ο μεταγλωττιστής της Erlang}
Μια εφαρμογή σε Erlang δομείται σε modules, τα οποία μεταγλωττίζονται ανεξάρτητα και φορτώνονται στο σύστημα χρόνου
εκτέλεσης. Ο μεταγλωττιστής της Erlang μεταγλωττίζει τον πηγαίο κώδικα σε κώδικα εικονικής μηχανής (bytecode), ο οποίος
εκτελείται από την εικονική μηχανή BEAM.
O μεταγλωττιστής δε μεταφράζει απευθείας τον πηγαίο κώδικα των προγραμμάτων σε κώδικα μηχανής, αλλά πρώτα σε μια ενδιάμεση
αναπαράσταση, που ονομάζεται Core Erlang. Αυτή είναι μια συμπαγής, υψηλού επιπέδου αναπαράσταση του προγράμματος, με
μια αρκετά απλουστευμένη γραμματική, και ξεκάθαρους σημασιολογικούς κανόνες.
Το κύριο κίνητρο πίσω από το σχεδιασμό της Core Erlang ήταν το να αναπτυχθεί μια αναπαράσταση προγραμμάτων Erlang που να
καθιστά εύκολη την ανάπτυξη εργαλείων που πρέπει να διατρέξουν και να επεξεργαστούν προγράμματα Erlang, όπως
αποσφαλματωτές, εργαλεία στατικής ανάλυσης κτλ. Κάτι τέτοιο δεν ήταν εφικτό απευθείας σε πηγαίο κώδικα Erlang, λόγω της
συντακτικής πολυπλοκότητάς της, και οι προσπάθειες απλούστευσης της γλώσσας οδηγήθηκαν σε αδιέξοδο.
Το OTP παρέχει τη δυνατότητα σε οποιοδήποτε πρόγραμμα Erlang να διαβάσει την Core Erlang αναπαράσταση ενός οποιουδήποτε
Erlang module. Σε αυτό το χαρακτηριστικό βασίζεται το σύστημά μας για την ανάλυση των προγραμμάτων που του δίνονται ως είσοδος.
Φορτώνει τα modules στο σύστημα χρόνου εκτέλεσης, και αποσπά το Core Erlang Αφηρημένο Δένδρο Σύνταξης αυτού σε μορφή
ενός συνόλου από εγγραφές (records, εγγενής τύπος δεδομένων της Erlang), όπως αυτά ορίζονται στο
$otp/lib/compiler/src/core\_parse.hrl$.
\section{Το "σύστημα τύπων" της Erlang}
Η Erlang είναι μια γλώσσα με δυναμικό συστήμα τύπων. Αυτό σημαίνει ότι ο μεταγλωττιστής της γλώσσας δεν πραγματοποιεί έλεγχο τύπων κατά τη μεταγλώττιση ενός
προγράμματος. Το σύστημα χρόνου εκτέλεσης είναι υπεύθυνο για να εγγυηθεί την ασφάλεια τύπων, με το να ελέγχει την πληροφορία τύπων που είναι συσχετισμένη με κάθε
κομμάτι δεδομένων ενός προγράμματος κατα τη διάρκεια της εκτέλεσης.
Ένα κομμάτι δεδομένων σε 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
\end{itemize}
Οποιοσδήποτε όρος της Erlang μπορεί να αποτελέσει το περιεχόμενο των μηνυμάτων που ανταλλάσσουν διεργασίες μεταξύ τους.
\section{Το εργαλείο Dialyzer}
Οι κόμβοι του Core Erlang Δένδρου Αφηρημένης Σύνταξης δε διαθέτουν πληροφορίες τύπων δεδομένων. Σε ορισμένες "απλές"
περιπτώσεις, όπως όταν έχουμε κυριολεκτικούς όρους στον κώδικα που αναλύουμε (για παράδειγμα $x = 42$), μπορούμε να
βρούμε τον τύπο των όρων χρησιμοποιώντας συναρτήσεις βιβλιοθήκης της γλώσσας. Προκειμένου να πραγματοποιήσουμε οποιαδήποτε
ουσιώδη ανάλυση
σχετικά με τους τύπους συνεδριών σε ένα πρόγραμμα, χρειάζεται να γνωρίζουμε τους τύπους των δεδομένων που περιέχονται στα μηνύματα που
ανταλλάσσονται μεταξύ διεργασιών. Συνεπώς, χρειαζόμαστε ένα εργαλείο το οποίο, δοθέντος ενός προγράμματος σε Erlang, να
πραγματοποιεί συμπερασμό τύπων δεδομένων.
Ο Dialyzer (DIscrepancy AnaLYZer) είναι ένα σύστημα που πραγματοποιεί μιας μορφής στατικό type checking σε προγράμματα Erlang.
Σε πρώτη φάση επεξεργάζεται ένα πρόγραμμα Erlang, προκειμένου να εξάγει τα λεγόμενα success typings. Τα success typings
είναι οι τύποι που πρέπει να έχουν οι συναρτήσεις (δηλαδή ο συνδυασμός των τύπων των ορισμάτων μιας συνάρτησης, και του
τύπου του αποτελέσματος που αυτή η συνάρτηση επιστρέφει) προκειμένου να εξασφαλιστεί ότι η συνάρτηση δε θα παρουσιάσει κάποιο
σφάλμα χρόνου εκτέλεσης που
οφείλεται σε κάποια ασυνέπεια στους τύπους. Για παράδειγμα, στο κομμάτι κώδικα του σχήματος $2.1$ το να καλέσουμε τη συνάρτηση $foo/1$
ως $foo("Hello")$ θα οδηγούσε σε σφάλμα χρόνου εκτέλεσης, καθώς ο τελεστής $+$ δε μπορεί να εφαρμοστεί σε ένα όρισμα
τύπου $List$ σε Erlang. Αυτό οδηγεί το Dialyzer στο να συμπεραίνει τύπους με έναν συντηρητικό τρόπο:
οι τύποι που κάνει assign σε συναρτήσεις, και οι οποίοι απορρέουν από τους τύπους που αποδίδει στα επιμέρους τμήματα δεδομένων στο
σώμα των συναρτήσεων, αποτελούν ένα υπερσύνολο των
πραγματικών τύπων των δεδομένων μιας συνάρτησης. Στο ίδιο κομμάτι κώδικα, ο τύπος που θα συμπέραινε ο Dialyzer για τη
συνάρτηση $foo/1$ είναι $Number \rightarrow Number$.
\lstset{style=erlangCodeStyle}
\begin{lstlisting}[language=Erlang, caption=Simple receive]
foo(X) ->
X + 42.
\end{lstlisting}
Προκειμένου ο Dialyzer να φτάσει στα success typings, πραγματοποιεί έναν συμπερασμό τύπων για όλα τα επιμέρους terms που
εμφανίζονται μέσα στα σώματα των συναρτήσεων. Η έκδοση του Dialyzer που δημοσιεύεται ως μέρος του OTP δεν αποθηκεύει αυτήν την
πληροφορία για όλη τη διάρκεια της ανάλυσης, αλλά μόνο για όσο χρειάζεται για την εκάστοτε συνάρτηση.
Για τους σκοπούς της δικής μας ανάλυσης, χρειάζεται να γνωρίζουμε τους τύπους δεδομένων των Erlang terms σε κάθε γραμμή
πηγαίου κώδικα ενός Erlang module. Προκειμένου να εξασφαλίσουμε αυτήν την πληροφορία, προβήκαμε στην τροποποίση του Dialyzer
με σκοπό την αποστολή της πληροφορίας τύπων δεδομένων στο σύστημά μας κατα τη διάρκεια της εκτέλεσης του dataflow analysis loop του.
\section{Ταυτοχρονισμός σε Erlang}
Ένα ισχυρό χαρακτηριστικό της Erlang είναι η υποστήριξη της για ταυτοχρονισμό. Παρέχει στον προγραμματιστή ένα σύνολο
από primitives για τη δημιουργία διεργασιών, και τη διαχείριση της επικοινωνίας μεταξύ αυτών. Αυτές δεν είναι διεργασίες
σε επίπεδο λειτουργικού συστήματος, ούτε όμως και νήματα, αλλά αποτελούν οντότητες τις οποίες διαχειρίζεται
η εικονική μηχανή εκτέλεσης της Erlang, ο BEAM.
Οι διεργασίες σε Erlang δε μοιράζονται αποθηκευτικό χώρο. Ο μοναδικός μηχανισμός που παρέχεται στον προγραμματιστή για
την υλοποίηση της επικοινωνίας και της ανταλλαγής πληροφοριών μεταξύ αυτών των διεργασιών
είναι η ασύγχρονη ανταλλαγή μηνυμάτων. Κάθε διεργασία διαθέτει ένα "κουτί εισερχομένων", μια ουρά από μηνύματα που έχει λάβει από άλλες διεργασίες. Για να καταναλώσει
ένα μήνυμα από αυτήν την ουρά, ο προγραμματιστής χρησιμοποιεί την έκφραση $receive$, με την οποία παίρνει ένα μήνυμα από
την κεφαλή της ουράς, και το συγκρίνει με μια σειρά από
μοτίβα (patterns) τα οποία αντιστοιχούνσ στα μηνύματα που περιμένει ότι το πρόγραμμά του θα λάβει στη συγκεκριμένη φάση
της εκτέλεσης. Όταν μια σύγκριση πετύχει, η διεργασία συνεχίζει την εκτέλεσή της.
\lstset{style=erlangCodeStyle}
\begin{lstlisting}[language=Erlang, caption=Simple receive]
foo() ->
receive
{num, Sender, N} -> io:format("Got a number ~p from ~p\n", [N, Sender]);
{atom, Sender, A} -> io:format("Got an atom ~p from ~p\n", [A, Sender]);
42 -> io:format("Got 42\n")
end.
\end{lstlisting}
Στο listing 2.2 φαίνεται ένα παράδειγμα μιας συνάρτησης που περιμένει να διαβάσει από το κουτί εισερχομένων της:
\begin{itemize}
\item Μια πλειάδα τιμών (tuple) που αποτελείται από ένα atom, ένα pid κι έναν αριθμό
\item Μια πλειάδα τιμών που αποτελείται από ένα atom, ένα pid κι ένα atom
\item Έναν απλό αριθμό
\end{itemize}
Αν μια διεργασία που επικοινωνεί με αυτήν της αποστείλει ένα μήνυμα της μορφής $\{num, 42\}$, τότε η $foo/1$ δε θα το "καταναλώσει"
ποτέ. Αντίστοιχα, αν καμία διεργασία δεν αποστείλει στη διεργασία που εκτελεί τον κώδικα του listing 2.2 κάποιο μήνυμα
που να αντιστοιχεί σε ένα από τα μοτίβα της εντολής $receive$, η εκτέλεση θα "κρεμάσει" επ' αόριστον.
Σε αυτήν την περίπτωση θα είχαμε ένα προβληματικό σενάριο, που
προκύπτει από τη μη-συμμόρφωση ενός εκ των δύο μερών της επικοινωνίας στο αναμενόμενο πρωτόκολλο.
%% Type and effect systems
\chapter{Συστήματα τύπων και επιδράσεων}
Πολλές γλώσσες προγραμματισμού υλοποιούν ένα στατικό σύστημα τύπων, προκειμένου να εγγυηθούν ότι τελεστές εφαρμόζονται μόνο σε
τελεσταίους της κατάλληλης μορφής, δηλαδή του κατάλληλου είδους. Για παράδειγμα, ένα κλασσικό σύστημα τύπων θα απέρριπτε
το πρόγραμμα 3.1 (γραμμένο σε μια υποθετική γλώσσα), καθώς η πράξη της αφαίρεσης ($-$), δεν έχει νόημα όταν εφαρμόζεται
σε μια συμβολοσειρά και έναν αριθμό (υποθέτουμε ότι η γλώσσα δεν παρέχει τη δυνατότητα υπερφόρτωσης τελεστών).
\begin{lstlisting}[caption=Ασύμβατοι Τελεσταίοι]
begin
print('Hello, world!' - 42)
end.
\end{lstlisting}
% FIXME uppercase greek letters
\section{Κλασσικά συστήματα τύπων με συμπερασμό}
Η προσέγγιση των συστημάτων τύπων είναι να συσχετίζουν τύπους με προγράμματα. Οι τύποι περιγράφουν το είδος των δεδομένων
τα οποία μεταχειρίζεται το πρόγραμμα. Ο συσχετισμός αυτός γίνεται μέσω ενός συνόλου κανόνων συμπερασμού, με βάση
τη σύνταξη του προγράμματος, κάνοντας χρήση ενός περιβάλλοντος τύπων, το οποίο αντιστοιχεί τις ελεύθερες μεταβλητές ενός
προγράμματος με τους τύπους τους. Η αντιστοίχηση αυτή εκφράζεται με μια σχέση του τύπου $ \Gamma |- e : τ $, όπου:
\begin{itemize}
\item $\Gamma$ είναι το περιβάλλον τύπων
\item $e$ είναι το πρόγραμμα υπό εξέταση
\item $τ$ είναι ο τύπος του προγράμματος $e$, δεδομένων των "περιορισμών" που τίθενται σχετικά με τις ελεύθερες
μεταβλητές που εμφανίζονται στο σώμα του $e$ από το περιβάλλον $\Gamma$
\end{itemize}
Οι προκλήσεις του σχεδιασμού ενός συστήματος τύπων είναι:
\begin{itemize}
\item Το σύστημα τύπων να είναι σημασιολογικά ορθό %% TODO elaborate
\item Το σύστημα τύπων να είναι αποφάνσιμο, το οποίο σημαίνει ότι πρέπει να είναι δυνατός ο σχεδιασμός ενός
αλγορίθμου ο οποίος να τερματίζει και να ελέγχει τις ιδιότητες του συστήματος
\end{itemize}
%% TODO simple type system (look at pl2 slides?)
%FIXME annotations <-> ετικετών
\section{Συστήματα τύπων με ετικέτες}
Μια προσέγγιση για την επέκταση της εκφραστικότητας ενός συστήματος τύπων είναι η προσθήκη ετικετών στους τύπους με
αποτέλεσμα την παραμετροποίησή τους, και στόχο το να καταστεί εφικτό ένα σύνολο στατικών αναλύσεων, όπως η ανάλυση ροής
ελέγχου σε έναν μεταγλωττιστή.
%% TODO simple annotated type system
\section{Συστήματα τύπων και επιδράσεων}
Ο στόχος της προσθήκης πληροφορίας επιδράσεων στα κλασσικά συστήματα τύπων είναι η επέκτασή τους ώστε να εκφράζουν
επιπλέον ιδιότητες που προκύπτουν από τους σημασιολογικούς κανόνες ενός προγράμματος.
Τα συστήματα τύπων και επιδράσεων αποτελούν ουσιαστικά μια παραλλαγή των annotated συστημάτων τύπων, με μια διαφορά: οι
ετικέτες σε αυτά εκφράζουν ιδιότητες που αφορούν τη δυναμική συμπεριφορά του προγράμματος, δηλαδή τη συμπεριφορά του
κατά το χρόνο εκτέλεσης του προγράμματος.
Σε ένα σύστημα τύπων και επιδράσεων, η αντιστοίχιση ενός προγράμματος με έναν τύπο και μια επίδραση γράφεται ως $ \Gamma |- e
: \tau; \phi $, που σημαίνει ότι στο περιβάλλον $\Gamma$, το πρόγραμμα $e$ εμφανίζει μια επίδραση $\phi$, και εν τέλει επιστρέφει μια
τιμή τύπου $\tau$.
%% TODO simple type and effect system
%% Session types
\chapter{Τύποι Συνεδρίας}
Στα δίκτυα, μια συνεδρία είναι μια λογική οντότητα ανταλλαγής πληροφοριών μεταξύ δύο ή περισσότερων πρακτόρων. Ο κύριος
σκοπός μιας συνεδρίας είναι το να εγκαθιδρύσει το θέμα της επικοινωνίας, αλλα και το περιεχόμενο και την κατεύθυνση των
μηνυμάτων που ανταλλάσουν οι πράκτορες της επικοινωνίας.
Στα [] έχουμε τους πρώτους φορμαλισμούς της επικοινωνίας παράλληλων διεργασιών σε όρους ενός κλασσικού συστήματος τύπων.
Στο [] έχουμε μια πρώτη απόπειρα φορμαλισμού της επικοινωνίας παράλληλων διεργασιών, με την εισαγωγή των θεμελιωδών
λειτουργιών επικοινωνίας:
\begin{itemize}
\item $k!x$, δηλαδή αποστολή μιας τιμής $x$ μέσω του καναλιού $k$.
\item $k?x$, δηλαδή λήψη μιας τιμής $x$ μέσω του καναλιού $k$.
\end{itemize}
To κανάλι επικοινωνίας $k$ δημιουργείται ρητά από τους δύο πράκτορες με βάση μια κοινώς αποδεκτή θύρα στην αρχή της
επικοινωνίας, με χρήση δύο άλλων θεμελιωδών λειτουργιών
\begin{itemize}
\item $request(a, k)$, που αποτελεί ένα αίτημα εγκαθίδρυσης ενός καναλιού επικοινωνίας $k$ μέσω της θύρας $a$.
\item $accept(a, k)$, που αποτελεί αποδοχή ενός αίτημα εγκαθίδρυσης ενός καναλιού επικοινωνίας $k$ μέσω της θύρας
$a$.
\end{itemize}
Έχουμε επίσης την εισαγωγή της έννοιας ενός typed καναλιού επικοινωνίας, δηλαδή την απόδοση ενός τύπου στο κανάλι
επικοινωνίας με βάση τους τύπους των δεδομένων που ανταλλάσσονται μέσω αυτού, και την κατεύθυνση με την οποία αυτά
"ρέουν" μέσω του καναλιού.
Αυτό πρακτικά σημαίνει ότι ένα κανάλι επικοινωνίας μπορεί να έχει τον τύπο
\[
a: \uparrow int \downarrow int
\]
που σημαίνει ότι μια διεργασία που χρησιμοποιεί τη θύρα $a$ για να επικοινωνεί θα:
\begin{itemize}
\item στείλει μια τιμή τύπου ακεραίου (int), το οποίο συμβολίζεται με $\uparrow$, και ακολούθως θα
\item λάβει μια τιμή τύπου ακεραίου, το οποίο συμβολίζεται με $\downarrow$
\end{itemize}
Επακόλουθο του typing ενός καναλιού επικοινωνίας, είναι ο ορισμός των σφαλμάτων επικοινωνίας, που διαχωρίζονται σε άμεσα
σφάλματα, δηλαδή σφάλματα όμοια με αυτά κλασσικών συστημάτων τύπων όπου έχουμε εφαρμογή τελεστών σε τελεσταίους λάθος
τύπων, και προβλήματα ασυμβατότητας των στοιχειωδών πράξεων επικοινωνίας που πραγματοποιούν ανα πάσα στιγμή οι δύο
πράκτορες. Αυτό το είδος προβλήματος εμφανίζεται όταν οι πράξεις αυτές δεν είναι συμπληρωματικές. Άξιοσημείωτο εδώ είναι
ότι οι Takeuchi et al. δεν ασχολούνται με τη συμπληρωματικότητα ως προς τον τύπο των δεδομένων που ανταλλάσσονται
(δηλαδή μια διεργασία να στέλνει έναν ακέραιο και η διεργασία με την οποία επικοινωνεί να περιμένει έναν ακέραιο), αλλά
μόνο ως προς το είδος της πράξης (μια διεργασία να στέλνει, ενώ η άλλη περιμένει να λάβει μια τιμή από το κανάλι).
%% TODO maybe talk about other aspects of session type research?
%% FIXME I mean, really
Ο πιο πρόσφατος φορμαλισμός των τύπων συνεδριών κάνει διαχωρισμό ανάμεσα σε μια καθολική και μια τοπική περιγραφή της
επικοινωνίας. Στο [] αναλύονται δύο άλγεβρες βασισμένες σε μια επέκταση της π-άλγεβρας και των τύπων συνεδριών:
\begin{itemize}
\item Η πρώτη είναι η άλγεβρα που αποτελεί το φορμαλισμό της καθολικής περιγραφής. Σε αυτήν μπορεί να περιγραφεί η
αλληλεπίδραση των πρακτόρων της επικοινωνίας σε ένα αφηρημένο επίπεδο, μόνο σαν μια αλληλουχία από ενέργειες
μεταξύ συμμετεχόντων
\item Η δεύτερη είναι ο φορμαλισμός της τοπικής περιγραφής. Σε αυτήν περιγράφεται η επικοινωνία από τη σκοπιά ενός
συμμετέχοντα στην επικοινωνία (ενός πράκτορα)
\end{itemize}
Οι δύο άλγεβρες συνδέονται μεταξύ τους με μια σχέση προβολής, η οποία με βάση την καθολική περιγραφή της επικοινωνίας
(τη χορεογραφία), παράγει την περιγραφή που αντιστοιχεί στα διάφορα endpoints αυτής.
% Implementation work
\chapter{Ένα στατικό σύστημα τύπων συνεδρίας σε Erlang}
Οι τύποι συνεδρίας είναι ένας από τους φορμαλισμούς που έχουν προταθεί για την δόμηση και την ανάλυση της αλληλεπίδρασης μεταξύ
διεργασιών.
\section{Το σύστημα τύπων}
Τα annotations που αποτελούν την επέκταση του υπάρχοντος συστήματος τύπων της Erlang με τις επιδράσεις έχουν ως εξής:
\[
\begin{array}{lrl}
sestype & ::= & monosestype \\
& \mid & sestype
\vspace{2mm}\\
monosestype & ::= & (datatype_{1}, \ldots, datatype_{n}) \to \\
& & datatype;\ \phi
\vspace{2mm}\\
\phi & ::= & \varnothing \\
& \mid & sesaction.\ \phi \\
& \mid & \mu \, \sigma \,.\ \phi \\
& \mid & (\mu \, \sigma \,.\ \phi) . \phi
\vspace{2mm}\\
sesaction & ::= & datatype;!^{P} datatype\\
& \mid & datatype_1;?\ datatype_2\\
& \mid & \& <datatype_1;\phi_{1}, \ldots, datatype_n;\phi_{n}>\\
& \mid & \oplus <datatype_1;\phi_{1}, \ldots, datatype_n;\phi_{n}>\\
& \mid & \sigma
\vspace{2mm}\\
datatype & ::= & pid[process] \\
& \mid & Type \\
& \mid & sestype
\vspace{2mm}\\
process & ::= & self \\
& \mid & P
\end{array}
\]
\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.
Ως $\phi$ ορίζουμε την επίδραση μιας έκφρασης $e$ σε Erlang.
Τα περιβάλλοντα τύπων μας είναι τα εξής:
\begin{itemize}
\item $DE$ το περιβάλλον των ζευγών $(x, t)$, όπου $x$ ένα Erlang Term, και $t$ ο τύπος του
\item $PE$ το περιβάλλον των ζευγών $(n, p)$, όπου $n$ το όνομα ενός process, όπως αυτό συναντάται στο πρόγραμμα,
και $p$ η διεύθυνση χρόνου εκτέλεσης της διεργασίας.
\item $SE$ το περιβάλλον των ζευγών $(f, st)$ όπου $f$ το όνομα μιας συνάρτησης, και $st$ ο τύπος συνεδρίας της.
\end{itemize}
Ορίζουμε ως $\Gamma = \{DE, PE, SE\}$ την τριάδα που μας δίνει τα type schemes.
Οι κανόνες συμπερασμού τύπων ακολουθούν:
\begin{gather*}
\trfrac [(\emph{send})]
{\Gamma\,\vdash e_1 : pid[process]; \phi_{1}\ \Gamma\,\vdash e_2 : datatype; \phi_{2}}
{\Gamma\,\vdash e_1\,!\,e_2 : datatype; \phi_{2}, \phi_{1}, !^{process} datatype}\\
\vspace{2mm}\\
\trfrac [(\emph{recv})]
{\Gamma\,\vdash e : datatype_{e}; nothing\ DE';PE';SE\,\vdash S : datatype; \phi_{S}}
{\Gamma\,\vdash receive e \to S end : datatype; ? datatype_{e}, \phi_{S}}\\
\vspace{2mm}\\
\trfrac [(\emph{offer})]
{\Gamma\,\vdash e_{i} : datatype_{e_i}; nothing\ DE';PE';SE\,\vdash S_i : datatype_i;
\phi_{S_i}}
{\begin{tralign}\Gamma\,\vdash receive\ {e_i \to S_i}^{i \in\{1..N\}}\ end : datatype_{j}^{j
\in \{1..N\}}
\text{\&} <? datatype_1\ .\
\phi_{1}, \ldots&,\\? datatype_N\ .\ \phi_{N}>\end{tralign}}\\
\vspace{2mm}\\
\trfrac [(\emph{choice\_case})]
{\begin{tralign} Pref
(\phi_i^{i \in \{1..N\}})\ =& \ !^P datatype\ \\ \Gamma\,\vdash S_i :
datatype_i; \phi_{i} \qquad \qquad \qquad \qquad \qquad \quad
\mid& nothing
\end{tralign}}
{\Gamma\,\vdash case\, e\, of {p_i \to S_i}^{i \in \{1..N\}}\, end :
datatype_j^{j \in \{1..N\}}; \oplus<\phi_1, \ldots, \phi_{N}>}\\
\vspace{2mm}\\
\trfrac [(\emph{sequencing})]
{\Gamma\,\vdash Expr : datatype_e; sesaction \ \Gamma\,\vdash ExprSequence :
datatype; \phi}
%%{\begin{trgather} \Gamma\,\vdash Expr : datatype_e; sesaction \\ \Gamma\,\vdash ExprSequence :
%% datatype; \phi
%%\end{trgather}}
{\Gamma\,\vdash Expr, ExprSequence \ \ :\ datatype; sesaction, \phi}
\end{gather*}
Ο κανόνας $send$ περιγράφει την επίδραση μιας αποστολής μηνύματος. Καθώς πρώτα αποτιμώνται οι τιμές των $e_{2}$ και
$e_{1}$, οι επιδράσεις τους θα παρατηρηθούν πρώτες. Ο τύπος του αριστερού τελεσταίου της έκφρασης αποστολής πρέπει πάντα
να είναι η διεύθυνση μιας διεργασίας. Ο τύπος του μηνύματος μπορεί να είναι οποιοσδήποτε έγκυρος τύπος δεδομένων ενός
Erlang term. Στο τέλος, παρατηρείται και η επίδραση της αποστολής του μηνύματος $e_{2}$.
Ο κανόνας $recv$ περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία "ακούει" μόνο για μηνύματα ενός
συγκεκριμένου τύπου $datatype_{e}$. Σε Erlang, το pattern του μηνύματος πρέπει να είναι ένα απλό term, με αποτέλεσμα
ποτέ να μην είναι effectful, εξού και η επίδρασή του ($nothing$). Κατά την αποτίμηση του σώματος του receive clause,
χρησιμοποιούμε το περιβάλλον $\Gamma' = \{DE', PE', SE\}$, όπου τα $DE'$ και $PE'$ προκύπτουν από τα $DE$ και $PE$
προσθέτοντας τυχών μεταβλητές που περιέχονται στο receive pattern.
Ο κανόνας $offer$ περιγράφει την επίδραση μιας λήψης μηνύματος, όταν μια διεργασία "ακούει" για μηνύματα διαφορετικών
μορφών. Και εδώ τα patterns είναι effectless.
Ο κανόνας $choice\_case$ περιγράφει την επίδραση μιας έκφρασης που προκαλεί διακλάδωση στην εκτέλεση, σε περίπτωση που τα
σώματα των
clauses είναι effectful, και οι επιδράσεις τους ξεκινούν όλες με ένα $send$ action.
Ο κανόνας $sequencing$ περιγράφει την επίδραση ενός συνόλου από εκφράσεις, οι οποίες αποτιμώνται με μια γραμμική σειρά.
Αυτός είναι ο κανόνας με βάση των οποίο συμπεραίνουμε τους τύπους και τις επιδράσεις συναρτήσεων.
Στο σύστημα τύπων και επιδράσεών μας, οι μόνες εκφράσεις που έχουν κάποια επίδραση είναι αυτή της αποστολής μηνύματος
(!), και αυτή της λήψης μηνύματος ($ receive ... end $). Όλες οι υπόλοιπες Erlang εκφράσεις είναι effectless.
\section{Υλοποίηση}
\subsection{Τμήματα}
Καθόλη τη διάρκεια αυτής της ενότητας, θα χρησιμοποιούμε το απλό πρόγραμμα που φαίνεται στο σχήμα 5.1 ως βάση για να
εξηγήσουμε τη λειτουργία του συστήματός μας.
\begin{lstlisting}[language=Erlang, caption=Απλό παράδειγμα, basicstyle=\small]
run() ->
ProcServer = spawn(fun() -> server() end),
Foo = spawn(fun() -> foo() end),
Biz = spawn(fun() -> biz() end),
spawn(fun() -> baz(Biz) end),
spawn(fun() -> bar(Foo) end),
spawn(fun() -> simple_client(ProcServer) end),
spawn(fun() -> recursive_client(ProcServer, rand:uniform(100)) end).
server() ->
receive
{num_1, Proc, X} ->
receive
{num_2, Proc, Y} ->
Proc ! {num_sum, self(), X + Y + 42},
server()
end;
{foo, Proc, X} -> server()
end.
simple_client(Server) ->
Server ! {num_1, self(), 17},
Server ! {num_2, self(), rand:uniform(100)},
receive
{num_sum, Server, X} -> X
end.
recursive_client(Server, 0) -> ok;
recursive_client(Server, N) ->
Server ! {foo, self(), N},
recursive_client(Server, N - 1).
foo() ->
receive
{foo, P, 42} ->
receive
{foo, P, 17} ->
P ! {foo, self(), 42 + 17},
foo()
end
end.
bar(Foo) ->
Foo ! {foo, self(), 42},
Foo ! {foo, self(), 17},
receive
{foo, Foo, X} ->
Foo ! {foo, self(), 42},
Foo ! {foo, self(), 17},
receive
{foo, Foo, X} -> X + 42
end
end.
baz(Biz) ->
Biz ! {foo, self(), 42},
Biz ! {bar, self(), 17},
baz(Biz).
biz() ->
receive
{foo, Pid, X} ->
receive
{bar, Pid, _Y} ->
receive
{foo, Pid, X} -> biz()
end
end
end.
\end{lstlisting}
Το συστημά μας αποτελείται από τα εξής επιμέρους κομμάτια:
\begin{itemize}
\item Το κομμάτι του συμπερασμού των τύπων συνεδριών του προγράμματος που δεχόμαστε ως είσοδο
\item To κομμάτι του ελέγχου των τύπων που συμπέρανε το σύστημά μας με τους τύπους που παρέχονται από τον χρήστη ως
ο "προδιαγεγραμμένος" τύπος συνεδρίας ενός τμήματος του προγράμματος
\item Το κομμάτι της σύγκρισης των τύπων δύο συναρτήσεων προκειμένου να διαπιστωθεί αν αποτελούν τα "άκρα" ενός
πρωτοκόλλου επικοινωνίας
\end{itemize}
Όλα τα προγράμματα που παρέχονται προς ανάλυση "περνάνε" από το πρώτο κομμάτι. Το δεύτερο και το τρίτο ενεργοποιούνται
με βάση την είσοδο του χρήστη.
\subsection{Συμπερασμός Τύπων Συνεδριών}
Όπως έχουμε αναφέρει και προηγουμένως, η Erlang είναι μια γλώσσα με δυναμικούς τύπους, πράγμα το οποίο σημαίνει ότι δεν
υπάρχουν πληροφορίες τύπων για τα δεδομένα ενός προγράμματος κατά το χρόνο μεταγλώττισης.
Στο κεφάλαιο 4 είδαμε ότι στους τύπους συνεδρίας, ένα θεμελιώδες κομμάτι της ανάλυσης είναι η γνώση των τύπων δεδομένων
που περιέχονται στα μηνύματα που ανταλλάσσονται μεταξύ των επικοινωνουσών διεργασιών.
Προκειμένουν να αποκτήσουμε αυτήν την πληροφορία για τους σκοπούς της δικής μας ανάλυσης, αξιοποιούμε τον Dialyzer. Με
αυτόν τον τρόπο, ο συμπερασμός τύπων συνεδρίας του συστήματός μας πραγματοποιείται σε δύο φάσεις:
\begin{itemize}
\item Στην πρώτη φάση, δίνουμε το προς ανάλυση πρόγραμμα ως είσοδο στον Dialyzer. Μετά το τέλος της εκτέλεσής του,
έχουμε συμπεράνει τους τύπους των δεδομένων του προγράμματος.
\item Στη δεύτερη φάση, επανεπεξεργαζόμαστε όλο το πρόγραμμα, και συμπεραίνουμε τους τύπους συνεδριών των
συναρτήσεων του με βάση τους κανόνες της προηγούμενης ενότητας, και αξιοποιώντας την πληροφορία που εξήγαγε ο
Dialyzer, την οποία χρησιμοποιήσαμε για να "γεμίσουμε" το περιβάλλον $\Gamma$ με τις αντιστοιχήσεις μεταβλητών με
τύπους.
\end{itemize}
Για μια ανάλυση του τρόπου με τον οποίο δουλεύει ο Dialyzer, ο αναγνώστης παραπέμπεται στα [].
Χρησιμοποιούμε μια έκδοση του Dialyzer βασισμένη σε αυτήν που περιέχεται στην έκδοση 19.0 του Erlang/OTP, ελαφρώς
τροποποιημένη για τους σκοπούς μας, ώστε να διατηρεί την πληροφορία που σχετίζεται με τους τύπους δεδομένων των
επιμέρους Erlang terms καθόλη τη διάρκεια της ανάλυσης, και ακολούθως να τη μεταδίδει στο σύστημά μας.
Μόλις ολοκληρωθεί η ανάλυση του προγράμματος από τον Dialyzer, τρέχουμε τη δική μας σημασιολογική ανάλυση πάνω στο Core
Erlang AST του κάθε module, αποδίδοντας σε κάθε κόμβο ένα effect, με βάση τους κανόνες συμπερασμού που περιγράφηκαν
παραπάνω.
Οι κλήσεις συναρτήσεων βιβλιοθήκης της Erlang, πέραν του $!$(send), είναι effectless.
Κατά την ανάλυση των συναρτήσεων ενός module, είναι πολύ πιθανό να συναντήσουμε κλήσεις σε άλλες, ορισμένες από τον
χρήστη, συναρτήσεις εντός του module (ή και μέσα σε άλλα modules του προγράμματος), για τις οποίες όμως δεν έχουμε ακόμη
διαθέσιμη την πλήρη πληροφορία σχετικά με τον τύπο συνεδρίας τους, είτε επειδή θα αναλυθούν σε μετέπειτα χρονική στιγμή,
είτε επειδή και εκείνες περιείχαν κλήση σε κάποια άλλη συνάρτηση.
Κατά τη φάση του συμπερασμού τύπων, στη θέση της επίδρασης της καλούμενης συνάρτησης βάζουμε μια τιμή placeholder, την
$\{unavailable, \{Module, Function, Arity\}\}$, όπου $Module$ το module στο οποίο ορίζεται η καλούμενη συνάρτηση,
$Function$ το όνομα της καλούμενης συνάρτησης, και $Arity$ η πολλαπλότητα αυτής.
Στο τέλος της ανάλυσης των modules του προγράμματος, πραγματοποιούμε ένα iteration πάνω σε όλες τις ορισμένες
συναρτήσεις, και κάνουμε resolve όλες τις επιδράσεις που δεν ήταν διαθέσιμες κατά τη διάρκεια αυτής. Εδώ, 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]
{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).>."
{simple_client,1} : "pid(1) !(atom x pid x integer). pid(1) !(atom x pid x integer). ?(atom x pid x any)."
{recursive_client,2} : "u (1). pid(1) !(atom x pid x integer).rec(1)."
{foo,0} : "u (5). ?(atom x {atom, pid, (atom x atom)} x integer). ?(atom x {atom, pid, (atom x atom)} x integer).
pid(1) !(atom x pid x integer).rec(5)."
{bar,1} : "pid(1) !(atom x pid x integer). pid(1) !(atom x pid x integer). ?(atom x pid x number).
pid(1) !(atom x pid x integer). pid(1) !(atom x pid x integer). ?(atom x any x number)."
{baz,1} : "u (2). pid(1) !(atom x pid x integer). pid(1) !(atom x pid x integer).rec(2)."
{biz,0} : "u (3). ?(atom x any x any). ?(atom x any x any). ?(atom x any x any).rec(3)."
\end{lstlisting}
\subsection{Έλεγχος σε σχέση με το specification}
Η Erlang παρέχει τη δυνατότητα στον προγραμματιστή να προσθέσει annotations στα modules των προγραμμάτων του, τα οποία
είναι διαθέσιμα κατα τη φάση της μεταγλώττισης.
Εισάγουμε ένα νέο τέτοιο annotation, $-sestype()$. Παρέχουμε στον προγραμματιστή ένα σύνολο από macros, με βάση τα
οποία μπορεί να περιγράψει τον αναμενόμενο τύπο συνεδρίας για μια συνάρτηση, όπως φαίνεται στο σχήμα 5.3. Τα annotations
αυτά αντιστοιχούν στις συναρτήσεις $server/0$, $simple\_client/1$ και $recursive\_client/2$ του σχήματος 5.1.
%%\begin{center}
%% \begin{tabular}{||c c c c||}
%% \hline
%% Col1 & Col2 & Col2 & Col3 \\ [0.5ex]
%% \hline\hline
%% 1 & 6 & 87837 & 787 \\
%% \hline
%% 2 & 7 & 78 & 5415 \\
%% \hline
%% 3 & 545 & 778 & 7507 \\
%% \hline
%% 4 & 545 & 18744 & 7560 \\
%% \hline
%% 5 & 88 & 788 & 6344 \\ [1ex]
%% \hline
%% \end{tabular}
%%\end{center}
%% TODO add data types to macros
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
-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])),
?sa_recv_tag(?dt_any_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
?sa_send_tag(1,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
?sa_rec_tag(1)]},
{?dt_any_tag, [?sa_recv_tag(?dt_any_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
?sa_rec_tag(1)]}])])}).
-sestype({{simple_client, 1},
[?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])),
?sa_recv_tag(?dt_integer_tag,
?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag]))]}).
-sestype({{recursive_client, 2},
?f_rec_tag(1, [?sa_send_tag(1, ?dt_tuple_tag([?dt_atom_tag, ?dt_pid_tag, ?dt_integer_tag])), ?sa_rec_tag(1)])}).
\end{lstlisting}
Για κάθε τέτοιο annotation που έχει χρησιμοποιήσει ο προγραμματιστής, το εργαλείο μας συγκρίνει τον τύπο συνεδρίας που
συμπέρανε, με αυτόν που περιγράφεται στο annotation.
Η σύγκριση μεταξύ αυτών των τύπων συνεδρίας και των συμπερασμένων γίνεται καταναλώνοντας ένα-ένα τα session actions και
από τους δύο τύπους, και ελέγχοντας:
\begin{itemize}
\item Ότι τα actions που περιγράφουν είναι ίδια
\item Ότι το datatype του user annotation για το συγκεκριμένο action είναι υποτύπος του inferred session type τύπου.
\end{itemize}
Το δεύτερο κριτήριο είναι αυτό που κάνει το σύστημά μας πλήρες: ποτέ δε θα απορρίψει ένα σωστό πρόγραμμα.
Αναγνωρίζοντας τους περιορισμούς που αντιμετωπίζουμε στο συμπερασμό των τύπων δεδομένων, το να απαιτούμε οι
συμπερασμενοι τύποι δεδομένων να είναι πάντοτε ακριβώς ίδιοι με αυτούς που προσδιορίζει ο χρήστης στα $-sestype()$
annotations θα οδηγούσε σε απόρριψη αρκετών σωστών προγραμμάτων, λόγω mismatch.
Για να ξεπεράσουμε αυτό το πρόβλημα, επιτρέπουμε στους τύπους που παρέχει ο χρήστης να είναι τουλάχιστον τόσο συγκεκριμένοι (με
την έννοια του subtyping) όσο οι τύποι που συμπεραίνει ο Dialyzer. Αν ο παρεχόμενος τύπος δεν είναι υποτύπος του συμπερασμένου,
σημειώνουμε ένα error στην υλοποίηση του πρωτοκολλου επικοινωνίας.
Για παράδειγμα, στο πρώτο clause της $simple\_send/3$, αν ο χρήστης είχε δώσει
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
-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.
% TODO
Το type lattice δίνεται στο σχήμα 5.Χ.
\subsection{Έλεγχος peers}
Πέραν του $-sestype()$, εισάγουμε και άλλο ένα annotation: $-peers()$. Χρησιμοποιώντας αυτό, ο προγραμματιστής μπορεί να
υποδείξει στο σύστημά μας πως πρέπει να ελέγξει ότι δύο συναρτήσεις αποτελούν τα δύο άκρα ενός πρωτοκόλλου επικοινωνίας.
Αυτό σημαίνει ότι πρέπει να ελεγχθεί αν οι τύποι τους είναι συμπληρωματικοί.
Δύο συναρτήσεις είναι communication peers αν, καταναλώνοντας τους τύπους τους ένα-ένα action, κάθε ζεύγος από αυτά είναι
συμπληρωματικό, και εάν κάποιος τύπος εξαντληθεί πρόωρα, ο τύπος της άλλης συνάρτησης μένει σε μια κατάσταση η οποία
μπορεί να θεωρηθεί τερματική.
% TODO describe the difficulties with this
\paragraph{Ο Αλγόριθμος}
% TODO describe the algorithm
Μοντελοποιούμε τους τύπους συνεδριών της κάθε συνάρτησης ως ένα (πιθανώς κυκλικό) κατευθυνόμενο γράφημα $G(V, E)$. Κάθε
κορυφή στο $V$ αναπαριστά ένα action. Μια ακμή $e$ από την κορυφή $u$ στην κορυφή $v$ σημαίνει ότι το action που
περιγράφεται από τη $v$ ακολουθεί αυτό που περιγράφεται από τη $u$ στον τύπο συνεδρίας της συνάρτησης.
% TODO example graph
\begin{algorithm}[caption={Session Type Matching}, label={match}]
input: graph $G_1$, graph $G_2$
output: list of successful routes
begin
S = { {root($G_1$), root($G_2$)}}
res = []
while S not empty:
Pair = S.pop()
if complementary(Pair):
if next(Pair[$G_1$]) is empty:
if next(Pair[$G_2$]) is empty:
res.push(current route)
else:
if valid(recursive_criteria(Pair[$G_2$])):
res.push(current route)
else:
if next(Pair[$G_2$]) is empty:
if valid(recursive_criteria(Pair[$G_1$])):
res.push(current route)
else:
if valid(recursive_criteria(Pair[$G_1$])) and
valid(recursive_criteria(Pair[$G_2$])):
res.push(current route)
else:
foreach v in recursive_criteria(Pair[$G_1$]):
foreach u in recursive_criteria(Pair[$G_2$]):
S.push({u, v})
return res
end
\end{algorithm}
Το σύνολο αναζήτησης $S$ είναι μια ουρά από ζευγάρια κορυφών, των οποίων τα actions προσπαθούμε να ελέγξουμε ως προς τη
συμπληρωματικότητα. Κρατάμε το μονοπάτι το οποίο μας οδήγησε στο κάθε ζευγάρι κορυφών, τόσο ως προς το από ποιες κορυφές
περάσαμε, όσο και ως προς τον τύπο συνεδρίας με τον οποίο "φτάσαμε" στα παρόντα actions.
Ο αλγόριθμός μας ξεκινά με το να προσθέτει τα ζευγάρια των κορυφών-ριζών του κάθε γραφήματος στο σύνολο αναζήτησης $S$,
όπως φαίνεται στη γραμμή $4$ του παραπάνω αλγορίθμου. Κάθε γράφημα μπορεί να έχει περισσότερους του ενός αρχικούς
κόμβους, σε περιπτώσεις όπου το πρώτο action είναι ένα $choice$ ή ένα $offer$.
Συνεχίζει με το να βγάζει από την ουρά το πρώτο ζευγάρι κορυφών, και να συγκρίνει τα actions που αναπαριστούν.
Αν τα actions τους δεν είναι συμπληρωματικά, τότε θεωρούμε ότι το παρόν μονοπάτι αποτελεί ένα μη επιτυχές match, και
προχωράμε στο επόμενο ζεύγος κορυφών.
Αν τα actions τους είναι συμπληρωματικά, ελέγχουμε το σύνολο των έξω-γειτόνων της κάθε κορυφής. Εάν και τα δύο είναι
άδεια, τότε καταναλώσαμε πλήρως και τους δύο τύπους, και μπορούμε να κρατήσουμε το μονοπάτι που ακολουθήσαμε στο σύνολο
των έγκυρων ακολουθιών.
Εάν οποιοδήποτε από τα δύο σύνολα δεν είναι άδειο, ελέγχουμε το είδος των έξω-γειτόνων με τον αλγόριθμο:
\begin{algorithm}[caption={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
begin
res = []
min_depth = inf
foreach out-neighbour $u$ of $v$:
if $u$ not (start of recursive sequence or
unvisited start of recursive sequence):
res.push($u$)
else:
min_depth = min(min_depth, depth($u$))
if res == [] && min_depth == 1:
return {true, []}
else:
return {false, res}
end
\end{algorithm}
Αυτός ο αλγόριθμος ελέγχει όλους τους έξω-γείτονες μιας κορυφής $v$, και μας λέει αν όλοι τους αποτελούν την πρώτη
κορυφή μιας αναδρομικής ακολουθίας, και αν ναι, το ελάχιστο "βάθος" της αναδρομής. Εδώ ορίζουμε ώς $βάθος$ το επίπεδο
εμφώλευσης της αναδρομικής ακολουθίας, καθώς σε ένα session type μπορούμε να έχουμε αναδρομικές υποακολουθίες.
Για παράδειγμα, στον τύπο συνεδρίας
\begin{align*}
\mu \sigma.pid(1)\ &!\ atom\ x\ integer.\\
pid(1)\ &!\ atom\ x\ self\ x\ integer.\\
&(\mu \phi.?\ atom\ x\ integer. \phi).\\
&\sigma
\end{align*}
η κορυφή που αντιστοιχεί στην πρώτη $send$ λειτουργία έχει βάθος 1, καθώς δεν είναι εμφωλευμένη. Η $receive$ λειτουργία
εντός της αναδρομικής υποακολουθίας έχει βάθος 2.
Οι συνθήκες ενός επιτυχούς ταιριάσματος είναι:
\begin{itemize}
\item Δεν υπάρχουν άλλοι έξω-γείτονες, δηλαδή εξαντλήσαμε τα δύο γραφήματα.
\item Όλοι οι έξω-γείτονες είναι αρχικές κορυφές αναδρομικών ακολουθιών βάθους 1.
\end{itemize}
Εάν υπάρχουν έξω-γείτονες οι οποίοι είτε δεν είναι αρχικές κορυφές αναδρομικών ακολουθιών, είτε είναι αρχικές
κορυφές αναδρομικών ακολουθιών με βάθος μεγαλύτερο του 1, ή αποτελούν έναν συνδυασμό από αρχικές και μη κορυφές αναδρομικών
ακολουθιών βάθους 1, τις οποίες δεν έχουμε επισκεφθεί, τότε προσθέτουμε όλα τα ζευγάρια έξω-γειτόνων στο τέλος του συνόλου
αναζήτησης, προκειμένου να τα ελεγξουμε στο μέλλον.
% TODO elaborate on why these are terminal conditions
Ακολουθούν μερικά peer annotations για το πρόγραμμα 5.1.
\begin{lstlisting}[language=Erlang, caption=-sestype() annotation, basicstyle=\tiny]
-peers([{{server, 0}, []}, {{simple_client, 1}, []}]).
-peers([{{server, 0}, []}, {{recursive_client, 2}, []}]).
-peers([{{foo, 0}, []}, {{bar, 1}, []}]).
-peers([{{biz, 0}, []}, {{baz, 1}, []}]).
\end{lstlisting}
Ας αναλύσουμε τα δύο πρώτα ζευγάρια annotations.
Τα κατευθυνόμενα γραφήματα των τύπων συνεδρίας των συναρτήσεων $server/0$, $simple\_client/1$ και
$recursive\_client/2$ φαίνονται στα σχήματα 5.Χ έως 5.Υ.
\begin{figure}[h]
\caption{server/0}
\centering
\includegraphics[scale=0.5]{server_0_simple.png}
\end{figure}
\begin{figure}[h]
\caption{simple\_client/1}
\centering
\includegraphics[scale=0.5]{simple_client_1_simple.png}
\end{figure}
\begin{figure}[h]
\caption{recursive\_client/2}
\centering
\includegraphics[scale=0.5]{recursive_client_2_simple.png}
\end{figure}
Στην ανάλυση που ακολουθεί, θα αναφερόμαστε στην κορυφή $v$ του γραφήματος που αντιστοιχεί στη συνάρτηση $f/a$ ως
$f/a[v]$.
Αρχικά προσπαθούμε να συσχετίσουμε τους τύπους συνεδρίας των $server/0$ και $simple\_client/1$. Σύμφωνα με τον αλγόριθμο
που περιγράφηκε πριν, το αρχικό σύνολο αναζήτησης έχει ως εξής:
\[
S = \{\{server/0[v_0], simple\_client/1[v_0]\}, \{server/0[v_1], simple\_client/1[v_0]\}\}
\]
Θεωρούμε το πρώτο εκ των δύο ζευγών. Ο έλεγχος της γραμμής 8 είναι επιτυχής, καθώς τα session actions που αναπαριστούν
οι δύο κορυφές είναι συμπληρωματικά. Κανένα από τα δύο σύνολα έξω-γειτόνων δεν είναι άδεια: το σύνολο $out$ για την
κορυφή $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]\}\}
\]
Εκτελώντας τον αλγόριθμο για για το δεύτερο ζεύγος κορυφών του αρχικού συνόλου αναζήτησης, και πάλι έχουμε επιτυχία του
ελέγχου της γραμμής 8 καθώς τα session actions είναι συμπληρωματικά. Και πάλι κανένα από τα σύνολα των έξω-γειτόνων των δύο κορυφών
δεν είναι άδειο, οπότε καταλήγουμε να προσθέτουμε το καρτεσιανό γινόμενο των συνόλων αυτών στο σύνολο αναζήτησης, το
οποίο σημαίνει ότι σε αυτήν τη φάση αυτό αποτελείται από τα εξής ζεύγη κορυφών:
\begin{equation}
\begin{split}
S = \{&\{server/0[v_2], simple\_client/1[v_1]\},\\
&\{server/0[v_1], simple\_client/1[v_1]\},\\
&\{server/0[v_0], simple\_client/1[v_1]\}\}
\end{split}
\end{equation}
Εκτελώντας το βρόχο των γραμμών 6-26 του αλγορίθμου μέχρι να εξαντλήσουμε το σύνολο αναζήτησης, βρίσκουμε ότι πράγματι
οι συναρτήσεις $server/0$ και $simple\_client/1$ αποτελούν communication peers, και τα συμπληρωματικά session sequences
μεταξύ τους είναι τα:
\begin{equation}
\begin{split}
&\{server/0[v_0], simple\_client/1[v_0]\}\} \rightarrow \\
\rightarrow\ &\{server/0[v_2], simple\_client/1[v_1]\}\} \rightarrow \\
\rightarrow\ &\{server/0[v_3], simple\_client/1[v_2]\}\}
\end{split}
\end{equation}
Κανένα sequence που ξεκινάει από το ζευγάρι $\{server/0[v_1], simple\_client/1[v_0]\}$ δεν οδηγεί σε μια επιτυχή
συνεδρία.
Προχωράμε στην επικοινωνία μεταξύ των $server/0$ και $recursive\_client/2$. Το αρχικό σύνολο αναζήτησης είναι το
\[
S = \{\{server/0[v_0], recursive\_client/2[v_0]\}, \{server/0[v_1], recursive\_client/2[v_0]\}\}
\]
Και τα δύο ζευγάρια αποτελούνται από συμπληρωματικά μεταξύ τους actions, οπότε αφού έχουν καταναλωθεί από το σύνολο
αναζήτησης, αυτό θα έχει διαμορφωθεί ως εξής:
\begin{equation}
\begin{split}
S = \{&\{server/0[v_2], recursive\_client/2[v_0]\},\\
&\{server/0[v_1], recursive\_client/2[v_0]\}, \\
&\{server/0[v_0], recursive\_client/2[v_0]\}\}
\end{split}
\end{equation}
% TODO maybe discuss why the pair (v0, v0) is added to the search set again, despite it being part of the initial
% search set?
Εξαντλώντας και πάλι το σύνολο αναζήτησης, βλέπουμε ότι το ζευγάρι session actions
\[
\{server/0[v_1], recursive\_client/2[v_0]\}\}
\]
καθιστά τις $server/0$ και $recursive\_client/2$ communication peers.
\paragraph{Πρωτόκολλα Πολλαπλών Συμμετεχόντων}
% TODO describe issues with multiparty session types here
Ο παραπάνω αλγόριθμος θεωρεί ότι υπάρχουν μόνο δύο συμμετέχοντες σε κάποια συνεδρία. Σε περίπτωση που θέλαμε να
επεκτείνουμε και να γενικεύσουμε τον αλγόριθμο αυτό ώστε να δουλεύει για πολλαπλούς συμμετέχοντες, θα ερχόμασταν
αντιμέτωποι πολύ γρήγορα με το πρόβλημα της συνδυαστικής έκρηξης (combinatoric explosion).
Εαν υποθέσουμε ότι προσπαθούμε να τσεκάρουμε την επικοινωνία μεταξύ $n$ διεργασιών, τότε σε κάθε βήμα θα έπρεπε να
θεωρούμε έως και $ \mychoose{n}{2} $ ζευγάρια. Κάτι τέτοιο, αν και αργό, ίσως να είναι εφικτό μόνο για μικρές τιμές του $n$,
και για σχετικά σύντομους και απλούς τύπους συνεδριών.
% Examples
\chapter{Παραδείγματα}
Παρουσίαση των toy παραδειγμάτων με τα οποία δουλεύουμε, και ίσως κάτι πιο involved?
\chapter{Συμπεράσματα και μελλοντική έρευνα}
Σε αυτήν την εργασία παρουσιάσαμε ένα στατικό σύστημα τύπων συνεδρίας για τη γλώσσα Erlang. Παρουσιάσαμε την αρχιτεκτονική
του, και τις αρχές πίσω από την ανάλυση που πραγματοποιεί.
% TODO maybe here we also need to talk about conclusions we have come to about the pros/cons of our technique, especially when compared
% to the various monitoring techniques we talk about [i.e static vs dynamic session type systems].
Κατά τη χρήση του εν λόγω συστήματος, διαπιστώσαμε ότι υπάρχει ένα σύνολο προσθηκών και αλλαγών που θα έπρεπε να γίνουν
σε αυτό, προκειμένου να μπορεί να χρησιμοποιηθεί αποτελεσματικά για την ανάλυση υπάρχουσων βάσεων κώδικα, αλλά και
ως ένα βοηθητικό εργαλείο αποσφαλμάτωσης κατά τη φάση της ανάπτυξης νέων εφαρμογών.
\begin{itemize}
\item Το παρόν σύστημα τύπων μας δεν είναι σε θέση να μοντελοποιήσει αμιγώς αναδρομικές συναρτήσεις.
\item Τα session type annotations που μπορεί να εισάγει κανείς στα modules θα έπρεπε να παρέχονται με έναν τρόπο πιο φιλικό
προς τον χρήστη, όπως μια συμβολοσειρά που μοιάζει περισσότερο με την περιγραφή των session types όπως τη
συναντάει κανείς στη βιβλιογραφία.
% TODO an example here would be nice.
\item Ο μηχανισμός επαλήθευσης των peer session types επιδέχεται σοβαρών βελτιστοποιήσεων, κυρίως σε περιπτώσεις
όπου αντιμετωπίζουμε αναδρομικούς τύπους.
% TODO elaborate a bit here.
\item Ο μηχανισμός επαλήθευσης των peer session types μπορεί να επεκταθεί ώστε να επαληθεύει τη συμμόρφωση σε
πρωτόκολλα επικοινωνίας σε περίπτωση multiparty sessions, δηλαδή σε περιπτώσεις όπου οι συμμετέχουσες διεργασίες
ξεπερνούν τις δύο σε αριθμό. Ο υφιστάμενος μηχανισμός στην παρούσα του μορφή δε μπορεί να υποστηρίξει αναζητήσεις
σε ένα τέτοιο search space. Η εισαγωγή τεχνικών που έχουν χρησιμοποιηθεί με επιτυχία στην περίπτωση του stateless
model checking [], καθώς επίσης και η εφαρμογή μεθόδων επέκτασης κατευθυνόμενων κυκλικών γραφημάτων μπορεί να
αποδειχθούν ιδιαίτερα αποτελεσματικές για την επίτευξη αυτού του στόχου.
\item Ο μηχανισμός συμπερασμού τύπων δεδομένων εξακολουθεί να είναι suboptimal, όμως δεν είναι ξεκάθαρο το πώς θα
μπορούσε να βελτιωθεί, δεδομένων των περιορισμών των γλωσσών προγραμματισμού με δυναμικά συστήματα τύπων.
\item Η επέκταση του συστήματος ώστε να είναι σε θέση να διαχειριστεί και τύπους δεδομένων ορισμένους από τον χρήστη.
\end{itemize}
%%% Bibliography
\bibliographystyle{softlab-thesis}
\bibliography{thesis}
%%% Appendices
\backmatter
\appendix
\chapter{Ευρετήριο συμβολισμών}
$A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$.
\chapter{Ευρετήριο γλωσσών}
\textbf{Haskell} : η γλώσσα της ζωής μου.
\chapter{Ευρετήριο αριθμών}
42 : life, the universe and everything.
%%% End of document
\end{document}
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