# source:Deliverables/D4.4/report.tex@3248

Last change on this file since 3248 was 3248, checked in by sacerdot, 7 years ago

Typos fixed.

File size: 5.9 KB
RevLine
[3222]1\documentclass[12pt]{article}
[3143]2
3\usepackage{../style/cerco}
4\usepackage{pdfpages}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
9\usepackage[english]{babel}
10\usepackage{graphicx}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14\usepackage{url}
15\usepackage{bbm}
16
17\title{
18INFORMATION AND COMMUNICATION TECHNOLOGIES\\
19(ICT)\\
20PROGRAMME\\
21\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
22
23\lstdefinelanguage{matita-ocaml}
24  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
25   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
26   morekeywords={[3]type,of},
27   mathescape=true,
28  }
29
30\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
31        keywordstyle=\color{red}\bfseries,
32        keywordstyle=[2]\color{blue},
33        keywordstyle=[3]\color{blue}\bfseries,
35        stringstyle=\color{blue},
36        showspaces=false,showstringspaces=false}
37
38\lstset{extendedchars=false}
39\lstset{inputencoding=utf8x}
40\DeclareUnicodeCharacter{8797}{:=}
41\DeclareUnicodeCharacter{10746}{++}
42\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
43\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
44
45\date{}
46\author{}
47
48\begin{document}
[3222]49\pagenumbering{roman}
[3143]50\thispagestyle{empty}
51
52\vspace*{-1cm}
53\begin{center}
54\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
55\end{center}
56
57\begin{minipage}{\textwidth}
58\maketitle
59\end{minipage}
60
61\vspace*{0.5cm}
62\begin{center}
63\begin{LARGE}
64\textbf{
65Report n. D4.4\\
66Back-end Correctness Proof}
67\end{LARGE}
68\end{center}
69
70\vspace*{2cm}
71\begin{center}
72\begin{large}
73Version 1.0
74\end{large}
75\end{center}
76
77\vspace*{0.5cm}
78\begin{center}
79\begin{large}
80Main Authors:\\
[3213]81Jaap Boender, Dominic P. Mulligan, Mauro Piccolo,\\ Claudio Sacerdoti Coen and
82Paolo Tranquilli
[3143]83\end{large}
84\end{center}
85
86\vspace*{\fill}
87
88\noindent
89Project Acronym: \cerco{}\\
90Project full title: Certified Complexity\\
91Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
92
93\clearpage
95\markright{\cerco{}, FP7-ICT-2009-C-243881}
96
97\newpage
[3213]99\paragraph{Summary}
100The deliverable D4.4 is composed of the following parts:
[3143]101
[3213]102\begin{enumerate}
[3143]103
[3213]104\item This summary.
[3143]105
[3213]106\item The paper \cite{simulation}.
[3143]107
[3213]108\item The paper \cite{backend}.
[3143]109
[3213]110\item The paper \cite{asm}.
[3143]111
[3213]112\item The paper \cite{policy}.
113
114\end{enumerate}
115
116This document and all the related \textsf{matita} developments can be downloaded at the
117page:
118\begin{center}
119{\tt http://cerco.cs.unibo.it/}
120\end{center}
121
122\bibliographystyle{unsrt}
123{\scriptsize\bibliography{report}}
124
[3143]125\newpage
126
[3213]127\paragraph{Aim}
128The aim of WP4 is is to build the trusted version of the compiler back-end,
129from the intermediate \textsf{RTLabs} language down to assembly. The development
[3248]130is made in \textsf{matita}, and it allows the trusted compiler to be extracted
[3213]131to \textsf{OCaml}.
132
133The main planned contributions of deliverable D4.4 are formally checked proof
134of the semantics correspondence between the intermediate code and the target
135code, and of the preservation/modification of the control flow for complexity
136analysis.
137
138\paragraph{Preservation of structure}
139In \cite{simulation} we present a genric approach to proving a forward
140simulation preserving the intensional structure of traces.
141
142When a language
143starts to be able to meddle with return addresses that live in memory, the call structure
144is no more guaranteed to be preserved after the high-level, structured
[3248]145languages. This has little meaning as far as pure extensional semantic
[3213]146preservation is required---after all, if the source language meddles with the
147call structure there is no problem as long as the target language will follow.
148However in our approach we have cost labels spanning multiple calls, so that
149the cost of what follows a call is paid'' in advance. This has no hope of
150being correct if there is no guarantee that upon return from a call we land
151after the call itself.
152
153In this part of the deliverable we will present our approach to this problem,
154which goes by including in semantic traces structural conditions, and giving
155generic proof obligations that enrich the classic step-by-step extensional
156preservation proof with the necessary hypotheses to ensure the preservation
157of the call and label structures. This approach can be applied on all passes
158starting from the \textsf{RTLabs} to \textsf{RTL} down to the assembly one.
159
160\paragraph{The back-end correctness proof}
161In \cite{backend}, we give an outline of the actual correctness proof for the
162passes from \textsf{RTLabs} down to assembly. We skip the details of the
163extensional parts of each pass and we concentrate on two main aspects:
164how we deal with stack and how we ensure the conditions explained in
165\cite{simulation} in the passes involving graph languages.
166
167\paragraph{The assembler correctness proof}
168In \cite{asm}, we present a proof of correctness of our assembler to object
169code, given a correct policy for branch expansion (see next paragraph).
170
171\paragraph{A branch expansion policy maker}
172In \cite{policy} we finally present our algorithm for branch expansion, that is
173how generic assembly jumps are expanded to the different type of jumps
174available in the 8051 architecture (short, absolute and long). The correctness
175of this algorithm is proved, and is what required by the correctness of the
176whole assembler.
177
[3222]178\includepdf[pages={-},addtotoc={1,section,1,Certification of the preservation of structure by a compiler's back-end pass,simulation}]{itp2013.pdf}
179\includepdf[pages={-},addtotoc={1,section,1,Certifying the back-end pass of the CerCo annotating compiler,backend}]{paolo.pdf}
180\includepdf[pages={-},addtotoc={1,section,1,On the correctness of an optimising assembler for the Intel MCS-51 microprocessor,asm}]{cpp-2012-asm.pdf}
181\includepdf[pages={-},addtotoc={1,section,1,On the correctness of a branch displacement algorithm,policy}]{cpp-2012-policy.pdf}
[3143]182
183\end{document}
Note: See TracBrowser for help on using the repository browser.