source: src/ASM/CPP2011/cpp-2011.tex @ 947

Last change on this file since 947 was 947, checked in by sacerdot, 9 years ago

...

File size: 5.7 KB
Line 
1\documentclass{llncs}
2
3\usepackage[english]{babel}
4\usepackage[colorlinks]{hyperref}
5
6\title{Proving the correctness of an assembler for the MCS-51 microprocessor}
7\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
8\institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna}
9
10\bibliographystyle{splncs03}
11
12\begin{document}
13
14\maketitle
15
16\begin{abstract}
17\end{abstract}
18
19% ---------------------------------------------------------------------------- %
20% SECTION                                                                      %
21% ---------------------------------------------------------------------------- %
22\section{Introduction}
23\label{sect.introduction}
24
25\begin{enumerate}
26 \item Assembler are considered simple pieces of code, but this is not the
27       case and they can be quite hard to formalize.
28 \item We are interested in an assembler for the legacy MCS family.
29 \item What does it do:
30  \begin{enumerate}
31   \item translates from human readabale to machine readable
32   \item expand labels
33   \item expand pseudo instructions by optimizing the expansion
34  \end{enumerate}
35 \item Problems due to the expansion/optimization:
36  \begin{itemize}
37   \item operations that fetch from the code memory do not make sense at
38         pseudo level
39   \item operations that combine the PC with constant shifts do not make sense
40         at pseudo level
41   \item more generally, memory addresses, wherever they are (memory, registers)
42         can only be copied and compared with other memory addresses
43         $\Rightarrow$ need to trace memory addresses UNDECIDABLE PROBLEM
44   \item consequence: full preservation of the semantics becomes IMPOSSIBLE
45  \end{itemize}
46 \item We are also interested in intensional properties
47  \begin{itemize}
48   \item the semantics is sensible to the timing (e.g. I/O, interrupts)
49   \item to show that the semantics is preserved, one needs to assign a
50         precise cost model to the pseudo instructions
51   \item the cost model is induced by the compilation itself
52         $\Rightarrow$ ``recursive'' statement
53  \end{itemize}
54 \item Finally, the optimizing expansion itself: certified compilers are
55   usually proved to be correct, but we want more: completeness and optimality
56   of the expansion.
57  \begin{itemize}
58   \item the optimization starts with a non solution
59    and incrementally refines it to a solution. At each step it uses functions
60    that are used to implement the expansion and that needs to be correct.
61    The solution can fail to exist. The proof becomes a mess
62   \item idea: split the policy from the implementation; prove the
63    implementation to be correct w.r.t. any correct policy; provide a correct
64    policy (when it exists) and show that it is also complete and optimal.
65    Show that the assembler fails iff a correct policy does not exist
66    (completeness).
67  \end{itemize}
68 \item Additional issues:
69  \begin{itemize}
70   \item use of dependent types to throw away wrong programs that would made
71    the statement for completeness complex. E.g. misuse of addressing modes,
72    jumps to non existent labels, etc.
73   \item try to go for small reflection; avoid inductive predicates that require
74    tactics (inversion, etc.) that do not work well with dependent types; small
75    reflection usually does
76   \item use coercions to simulate Russell; mix together the proof styles
77    a la Russell (for situations with heavy dependent types) and the standard
78    one
79  \end{itemize}
80\end{itemize}
81     
82\end{enumerate}
83
84This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors.
85
86The work presented herein is a component of the EU-funded CerCo (`Certified Complexity') project.
87CerCo aims to produce a verified compiler from a large subset of C to the machine language of a microprocessor commonly used in embedded systems.
88In this respect, CerCo aims to go beyond the state of the art in verified compiler technology.
89
90Arguably, the CompCert C compiler currently represents the state of the art in the field of verified compilers.
91However, the verified backend of the CompCert C compiler stops at Power PC and ARM assembly \emph{languages}.
92Assembly of these languages into machine code is left untrusted.
93We aim to go further.
94
95The MCS-51 is CerCo's target processor.
96
97% ---------------------------------------------------------------------------- %
98% SECTION                                                                      %
99% ---------------------------------------------------------------------------- %
100\subsection{CerCo}
101\label{subsect.cerco}
102
103% ---------------------------------------------------------------------------- %
104% SECTION                                                                      %
105% ---------------------------------------------------------------------------- %
106\subsection{Overview of the paper}
107\label{subsect.overview.of.the.paper}
108
109% ---------------------------------------------------------------------------- %
110% SECTION                                                                      %
111% ---------------------------------------------------------------------------- %
112\section{The proof}
113\label{sect.the.proof}
114
115% ---------------------------------------------------------------------------- %
116% SECTION                                                                      %
117% ---------------------------------------------------------------------------- %
118\subsection{Matita}
119\label{subsect.matita}
120
121% ---------------------------------------------------------------------------- %
122% SECTION                                                                      %
123% ---------------------------------------------------------------------------- %
124\section{Conclusions}
125\label{sect.conclusions}
126
127\bibliography{cpp-2011.bib}
128
129\end{document}
Note: See TracBrowser for help on using the repository browser.