source: Deliverables/D4.4/draft.tex @ 3118

Last change on this file since 3118 was 3118, checked in by piccolo, 7 years ago

1) finished return case in StatusSimulationHelper?

2) started to write Deliverable D4.4

File size: 6.3 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../style/cerco}
4
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage{amssymb} 
8\usepackage[english]{babel}
9\usepackage{graphicx}
10\usepackage[utf8x]{inputenc}
11\usepackage{listings}
12\usepackage{lscape}
13\usepackage{stmaryrd}
14\usepackage{threeparttable}
15\usepackage{url}
16\title{
17INFORMATION AND COMMUNICATION TECHNOLOGIES\\
18(ICT)\\
19PROGRAMME\\
20\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
21
22\lstdefinelanguage{matita-ocaml}
23  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
24   morekeywords={[2]whd,normalize,elim,cases,destruct},
25   morekeywords={[3]type,of},
26   mathescape=true,
27  }
28
29\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
30        keywordstyle=\color{red}\bfseries,
31        keywordstyle=[2]\color{blue},
32        keywordstyle=[3]\color{blue}\bfseries,
33        commentstyle=\color{green},
34        stringstyle=\color{blue},
35        showspaces=false,showstringspaces=false}
36
37\lstset{extendedchars=false}
38\lstset{inputencoding=utf8x}
39\DeclareUnicodeCharacter{8797}{:=}
40\DeclareUnicodeCharacter{10746}{++}
41\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
42\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
43
44\date{}
45\author{}
46
47\begin{document}
48
49\thispagestyle{empty}
50
51\vspace*{-1cm}
52\begin{center}
53\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
54\end{center}
55
56\begin{minipage}{\textwidth}
57\maketitle
58\end{minipage}
59
60\vspace*{0.5cm}
61\begin{center}
62\begin{LARGE}
63\textbf{
64Report n. D4.4\\
65??????????????
66}
67\end{LARGE} 
68\end{center}
69
70\vspace*{2cm}
71\begin{center}
72\begin{large}
73Version 1.1
74\end{large}
75\end{center}
76
77\vspace*{0.5cm}
78\begin{center}
79\begin{large}
80Main Authors:\\
81????????????
82\end{large}
83\end{center}
84
85\vspace*{\fill}
86
87\noindent
88Project Acronym: \cerco{}\\
89Project full title: Certified Complexity\\
90Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
91
92\clearpage
93\pagestyle{myheadings}
94\markright{\cerco{}, FP7-ICT-2009-C-243881}
95
96\newpage
97
98\vspace*{7cm}
99\paragraph{Abstract}
100BLA BLA BLA
101\newpage
102
103\tableofcontents
104
105\newpage
106
107\section{A modular approach to the correctness of each Compiler's Backend Pass}
108
109An instance of the record \verb=sem_graph_params= contains all common information about
110programs of a joint-language whose source code can be logically organized as a graph.
111Thus, every program of this kind will be an ihabitant of the type \verb=joint_program p=,
112where \verb=p= is an istance of \verb=sem_graph_params=. We want to stress that such a record
113is in a sub-type relation with the record \verb=params=, which was explained in  Deliverable 4.3.
114
115In order to establish the correctness of our cost-model in each compiler's backend pass, where
116both source and target programs are joint-graph-programs, i.e. the source program \verb=src=
117(resp. the target program \verb=out=) is such that there is a \verb=p_in=
118(resp. \verb=p_out=) of type \verb=sem_graph_params= such that
119\verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to
120prove a statement similar to this shape.
121\begin{verbatim}
122theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
123∀prog : joint_program p_in.∀stack_size.
124let trans_prog ≝ transform_program … prog in
125∀init_in.
126make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
127∃init_out.
128make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
129∃[1] R : status_rel (joint_abstract_status (mk_prog_params p_in prog stack_size))
130          (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)).
131  status_simulation_with_init
132    (joint_abstract_status (mk_prog_params p_in prog stack_size))
133    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
134    R init_in init_out.
135\end{verbatim}
136When proving this statement (for each concrete istance of language),
137we need to proceed by cases according the classification of
138each state in the source program (\verb=cl_jmp=, \verb=cl_other=, \verb=cl_call= and
139\verb=cl_return=) and then proving the suitable conditions explained in
140previous Section, according to the case we are currently considering (Condition 1 for
141\verb=cl_other= and \verb=cl_jump= case, Condition 2 for \verb=cl_call= or
142Condition 3 for \verb=cl_return= case). Roughtly speaking, proving these condition
143means producing traces of some kind in the target language that are in a suitable
144correspondence with an execution step in the source language.
145
146Since traces carry both extensional and intensional information, the main disadvantage
147with this approach is that the extensional part of the proof (for example
148the preservation the semantical relation between states of the program under evaluation)
149and the intensional part (for example, all proof obbligation dealing with
150the presence of a cost label in some point of the code) are mixed together in a not so clear way.
151
152Furthermore, some proof obbligations concerning the relation among program counters
153(for example, the call relation between states which is one of the field of
154\verb=status_rel= record) depend only on the way the translation from source to target program is done.
155In particular if the translation satisfies some suitable properties, then it is possible
156to define some ``standard relations'' that automatically satisfy these proof obbligations,
157in an independent way from the specific source and target languages.
158
159So our question is wether there is a way to use these observation in order to factorize all common
160aspects of all correctness proofs of each pass involving joint languages.
161The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove
162the correctness of a single pass involving two joint-languages, to provide some semnatical state relation that
163satisfies some conditions. These conditions never speak about traces and they are mostly
164extensional, with the intesional part being limited to some additional requirred properties of
165the translation. This layer will use the trace machineary in order to deliver the desired correctness
166proof of the pass.
167
168In order to reach this goal, we have to analyze first whether there is a common way to perform language
169translation for each pass. After having defined and specified the translation machienary, we will
170explain how it is possibile to use it in order to build such a layer.
171
172
173
174\end{document}
Note: See TracBrowser for help on using the repository browser.