Evgenii Akentev
·
2019-01-18
thesis.lagda
1\documentclass[a4paper,14pt]{report}
2\usepackage{extsizes}
3\usepackage[dvips]{graphicx}
4\usepackage{geometry}
5\geometry{left=25mm}
6\geometry{right=20mm}
7\geometry{top=20mm}
8\geometry{bottom=20mm}
9\graphicspath{{image/}}
10\usepackage[usenames]{color}
11\usepackage{colortbl}
12\usepackage{multirow}
13\usepackage{setspace}
14\usepackage{xargs}
15\usepackage{mathtools}
16\usepackage{qtree}
17\onehalfspacing
18
19\usepackage{ragged2e}
20\justifying
21
22\usepackage{etoolbox}
23\patchcmd{\chapter}{\thispagestyle{plain}}{\thispagestyle{fancy}}{}{}
24
25\usepackage{fancyhdr}
26\pagestyle{fancy}
27\fancyhf{}
28\fancyfoot[R]{\thepage}
29\renewcommand{\headrulewidth}{0pt}
30\renewcommand{\footrulewidth}{0pt}
31
32\usepackage{ucs}
33\usepackage{amssymb}
34\usepackage{amsthm}
35\usepackage[english]{babel}
36\usepackage[references]{agda}
37\usepackage{unicode-math}
38\usepackage[hidelinks,colorlinks=false]{hyperref}
39\usepackage[titletoc,title]{appendix}
40\usepackage[nottoc]{tocbibind}
41\usepackage{makeidx}
42\usepackage{setspace}
43\usepackage{authblk}
44\usepackage{titlepic}
45\usepackage{float}
46\usepackage{textgreek}
47\usepackage{tabularx}
48
49\floatstyle{ruled}
50\newfloat{program}{thp}{lop}
51\floatname{program}{Program}
52\newtheorem{theorem}{Theorem}[section]
53\newtheorem{corollary}{Corollary}[theorem]
54\newtheorem{lemma}[theorem]{Lemma}
55% set font
56\setmainfont{XITS}
57\setmathfont{XITS Math}
58\setsansfont[Scale=MatchLowercase]{DejaVuSansMono.ttf}
59
60\newcommand{\jkeyw}[1]{\texttt{\bfseries #1}}
61\newcommand{\jol}[1]{\texttt{#1}}
62
63\begin{document}
64\begin{titlepage}
65\begin{table}[]
66 \centering
67 \begin{tabular}{rcl}
68 Автономная некоммерческая &
69 \multirow{4}{*}{\includegraphics[width=40mm]{image/logo.eps}}
70 & Autonomous noncommercial \\
71 организация высшего & & organization of higher \\
72 образования & & education \\
73 «Университет Иннополис» &
74 & «Innopolis University» \\
75 \hline
76 \hline
77 \end{tabular}
78 \label{tab:my_label}
79\end{table}
80\vline
81\vspace{5mm}
82
83\begin{center}
84\textbf{
85ВЫПУСКНАЯ КВАЛИФИКАЦИОННАЯ РАБОТА \\
86ПО НАПРАВЛЕНИЮ ПОДГОТОВКИ \\
8709.03.01 --- «ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»}
88\vspace{5mm}
89
90\textbf{GRADUATE THESIS \\
91MAJOR: "COMPUTER SCIENCE"}
92\end{center}
93\vspace{20mm}
94
95
96 \begin{tabular}{ll
97|>{\columncolor[gray]{.8}}l|}
98\cline{3-3}
99\textbf{Тема:} &
100 \makebox[0.5mm] &
101 \makebox[135mm][l]{Верифицированный тайпчекер для языка программирования
102 } \\
103 && Jolie\\
104 && \\
105 && \\
106\cline{3-3}
107 \end{tabular}
108\vspace{5mm}
109
110 \begin{tabular}{ll
111|>{\columncolor[gray]{.8}}l|}
112\cline{3-3}
113\textbf{Topic:} &
114 &
115 \makebox[135mm][l]{Verified type checker for Jolie programming language} \\
116 &&\\
117 && \\
118 && \\
119\cline{3-3}
120 \end{tabular}
121\vspace{5mm}
122
123
124 \begin{tabular}{ll
125|>{\columncolor[gray]{.8}}l|l
126|>{\columncolor[gray]{.8}}l|}
127\cline{3-3} \cline{5-5}
128Работу выполнил / &
129 \makebox[0.5mm] &
130 \makebox[66mm][l]{Акентьев Евгений Андреевич /} &
131 & \\
132Thesis is executed by &
133 \makebox[0.5mm] &
134 \makebox[66mm][l]{Akentev Evgenii Andreevich} &
135 &
136 \makebox[40mm]{\textcolor[gray]{.6}{подпись / signature}} \\
137\cline{3-3} \cline{5-5} \\
138 \end{tabular}
139\vspace{5mm}
140
141 \begin{tabular}{ll
142|>{\columncolor[gray]{.8}}l|l
143|>{\columncolor[gray]{.8}}l|}
144\cline{3-3} \cline{5-5}
145Научный руководитель / &
146 &
147 \makebox[57mm][l]{Мануэль Маццара /} &
148 & \\
149Thesis supervisor &
150 &
151 \makebox[57mm][l]{Manuel Mazzara} &
152 &
153 \makebox[40mm]{\textcolor[gray]{.6}{подпись / signature}} \\
154\cline{3-3} \cline{5-5} \\
155 \end{tabular}
156\vspace{\fill}
157
158\begin{center}
159Иннополис, Innopolis, 2017
160\end{center}
161\end{titlepage}
162
163\begin{abstract}
164Jolie is a service-oriented programming language which comes with the formal specification of its type system ~\cite{nielsen2013type}. However, there is no tool to ensure that programs in Jolie are well-typed. I provide the results of building a part of Jolie syntax, type system and semantics formal model in Agda proof assistant, which are intended for building a verified type checker.
165\end{abstract}
166
167\chapter*{Acknowledgements}
168
169I would like to thank Manuel Mazzara, Alexander Tchitchigin and Larisa Safina for their help in writing this thesis.
170
171\tableofcontents
172\thispagestyle{empty}
173
174\newpage
175
176\if{False}
177\begin{code}
178-- Imports
179open import Syntax
180open import Typesystem
181open import Typingrules
182open import Semantics
183open import Theorems
184\end{code}
185\fi
186
187\chapter{Introduction}
188
189Microservices architecture is a modern paradigm in software development using a composition of autonomous entities for creating systems~\cite{DBLP:journals/corr/DragoniGLMMMS16}.
190It has been developed as the answer to the problems arisen in applications built in monolithic or Service-Oriented Architecture styles including difficulties with scalability, complexity and dependencies of the evolving application. Microservices implement only a limited and cohesive functionalities, run their own processes, and use lightweight communication mechanisms.
191
192In the fast-growing landscape of microservices, Jolie~\cite{montesi2010jolie} appears to be a good candidate to play the role of a paradigmatic programming language~\cite{MGZ14}.
193Since every program in Jolie is a microservice, everything can be reused or recomposed for obtaining new microservices easing the creation of simple services as well as complex architectural compositions. This may help to scale programs easily, thus supports distributed architecture with the simple managing of components, reducing maintenance and lower development costs.
194
195However, communication between microservices in Jolie is obtained by means of sending and receiving messages whose type correspondence is checked only at runtime. Having a formalized type system of programming language gives an opportunity to implement type checking mechanism and use it before the runtime. Also, such a formalized type system can serve a ground for experiments.
196
197The idea of this work is to augment Jolie with a static type-checking mechanism based on type system specification. In ~\cite{nielsen2013type}, Nielsen described the type system of Jolie. She covered the syntax of behavioural, network and service layers and their semantics. Nielsen's work extended the semantic rules at the service layer for receiving a message with a dynamic type check. The described type system is provided with typing rules for the core of programming language (excluding subtyping, recursive types and some other primitives).
198
199I decided to study the application of type theory as a foundation for the formalization of Jolie. Type theory is a branch of mathematical logic, which operates not only with terms but with their types too. Type theory is a formal language with an explicit set of rules for rewriting strings of symbols, which describe computations. Therefore, type theory may serve as:
200
201\begin{itemize}
202
203\item foundations of mathematics
204
205\item programming language, because of Curry-Howard correspondence~\cite{Sorensen} (type theory should be constructive)
206
207\item calculus for category theory~\cite{crole1993deriving}
208
209\end{itemize}
210
211Therefore, there are different types of type theories. Here are the popular ones:
212
213\begin{itemize}
214
215\item Per Martin-L{\"o}f's dependent type theory (intuitionistic type theory)~\cite{lof, nordstrom90} is a version with dependents types which supports constructive mathematics.
216
217\item Calculus of Constructions~\cite{coquand1988calculus} is a type theory developed by Thierry Coquand and Gerard Huet. It solved some problems of Martin-L{\"o}f's type theory and was used as a basis for Coq~\cite{coq} proof assistant.
218
219\item Homotopy type theory~\cite{hottwebsite} is an improvement of intensional~\cite{constable2011trimuph} dependent type theory, which started as a homotopy $\lambda$-calculus~\cite{voevodsky2006very}. The main idea is to interpret identity types as path space objects in homotopy theory.
220
221\end{itemize}
222
223There are many implementations of type theories. Here are some of them:
224
225\begin{itemize}
226\item
227
228NuPRL ("new pearl")~\cite{constable1986implementing} is a proof system based on \textit{Computational Type Theory}~\cite{constable2002naive}, extended Martin-L{\"o}f's intuitionistic type theory developed in the 1980s by Robert Lee Constable. It has tactics in the spirit of Edinburgh LCF~\cite{gordon1979edinburgh}.
229
230\item
231
232Coq~\cite{coq} is a formal proof system written in OCaml. It's based on Calculus of Inductive Constructions~\cite{pfenning1990inductively, altenkirch1993constructions} and was initiated by Thierry Coquand. There are two inner languages: Gallina and Ltac. Gallina is a purely functional programming language for programs, specifications and proofs. Ltac is a tactical language for building and searching proofs and can be used interactively.
233
234\item
235
236Agda~\cite{agda, bove} is a dependently typed functional programming language written in Haskell. It has many features of modern functional programming languages such as inductive families (data types which depend on values), Unicode characters, parametrised modules, mixfix operators. Also, Agda is a proof assistant, because it's based on Martin-L{\"o}f's intuitionistic type theory.
237
238
239\item
240
241Lean~\cite{de2015lean} is a new open source theorem prover written in C++ being developed at Microsoft Research and Carnegie Mellon University. Lean's kernel is based on dependent type theory with configuration options. It depends on impredicative sort \textbf{Prop}. With that sort, kernel provides a version of the Calculus of Inductive Constructions and a version Martin-L{\"o}f's type theory without \textbf{Prop}.
242\item
243
244RedPRL~\cite{redprl} is a currently in work proof assistant for Computational Cubical Type Theory~\cite{cohen2016cubical} being developed Jon Sterling inspired by NuPRL. It uses a multi-sorted version of abstract binding trees and a dependent version of LCF apparatus.
245
246\end{itemize}
247
248Proof assistants and proof systems are becoming more popular in various spheres of software engineering. Usually, there are applied in critical spheres such as medicine, avionics and transport, where the correctness of a program is very important.
249
250One of such spheres is programming languages. The compilers, virtual machines and interpreters should have no bugs, since they are used by a lot of people who are making their programs for different purposes. Here are the examples of such projects:
251
252\begin{itemize}
253
254\item
255
256CompCert~\cite{Leroy} is a formally verified optimizing ISO C 99 compiler. The main idea behind this project is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It supports generating machine code for ARM, PowerPC, and x86 architectures.
257
258\item
259CakeML~\cite{Kumar:2014:CVI:2578855.2535841} is the verified implementation of the subset of Standard ML~\cite{milner1997definition}. It has a proven-correct compiler and runtime system. CakeML supports different architectures such as x86-64, ARM, MIPS, and RISC-V.
260
261\item
262Vellvm (\textit{verified LLVM})~\cite{zhao2012formalizing} is a framework mechanized formal semantics of LLVM’s intermediate representation, type system, and properties of SSA form. Vellvm is built using the Coq theorem prover.
263
264\end{itemize}
265
266I decided to use Agda ~\cite{bove,agda} as a proof assistant because it's comfortable and rich functional programming language with allows to extract programs into Haskell. Therefore, it's possible to create a type checker as a command line utility in the future.
267
268The structure of this thesis is as follows:
269chapter 2 describes the syntax of behavioural, service and network layers of Jolie. In chapter 3 I present the type system with typing rules. Chapter 4 is about the semantics of behavioural layer, which is necessary for type checking process. Chapter 5 contains proof of the "Structural Congruence for Behaviours" lemma and particular cases of the theorem about type preserving of the behavioural layer.
270Finally, in the last chapter, I conclude and describe the possible directions of future work.
271
272This thesis is written in Literate Agda~\cite{literateagda}. The whole formalization is available at~\cite{jolierepo}.
273
274\include{Syntax}
275
276\include{Typesystem}
277
278\include{Semantics}
279
280\include{Theorems}
281
282\chapter{Conclusions and Future Work}\label{sec:concl}
283
284In this thesis, I presented the approach in creating a formal model of Jolie programming language which is currently dynamically type-checked. I developed the formalization for the subset of Jolie by means of Agda proof assistant. I expressed Jolie's syntax, type system, typing rules and semantics of behaviour layer in order to be able to build a static type checker to check the type correspondence of messages which are used for interaction of microservices in Jolie. I have provided the proof of structural congruence lemma and particular cases of type preservation property for behaviours. During this project, there were discovered several problems in the original work~\cite{nielsen2013type}.
285
286Standard quality attributes are not very suitable for the evaluation of this project. For example, the performance of the current implementation is not a good metric, because there are almost no computations. Mostly, the program is a bunch of declarations of data types, except the types where lists are used. One of such types is a type that expresses the presence of an element in the list. Another such example is a security attribute, which can't be applied to this work. The results of this project are also reusable. For example, the implemented data types for the syntax may be used in writing a verified parser for Jolie. Also, since this project is written in Agda, which has a backend for the Haskell, the code can be used from Haskell. The correctness attribute means that the current implementation should be correct with respect to the specification ~\cite{nielsen2013type}. Since some of the properties were omitted to simplify the implementation, it does not fully correspond to the specification, but it may be fixed and extended in the future work.
287
288The current implementation covers only a small subset of Jolie and has limitations. The provided implementation of expressions is synthetic and not complete. Also, the typing rule for expressions should check that the given expression is well typed with respect to its environment. There is a need in full support of variables as trees and therefore the support of subtyping in the type system. The current typing rule for parallel behaviour lacks the check of that the resulting environments are disjoint. Also, there is a need to replace the stub with a normal mechanism for working with states.
289Another important direction leads to the complete formalization of the service and network levels of Jolie. By accomplishing this, it would be possible to build the type checker to type-check Jolie program thoroughly, which may even lead to implementing of a verifiable compiler for Jolie similar to~\cite{Neis,Leroy}.
290
291\bibliographystyle{unsrt}
292\bibliography{thesis}
293
294\end{document}