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 | |
---|
84 | This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors. |
---|
85 | |
---|
86 | The work presented herein is a component of the EU-funded CerCo (`Certified Complexity') project. |
---|
87 | CerCo aims to produce a verified compiler from a large subset of C to the machine language of a microprocessor commonly used in embedded systems. |
---|
88 | In this respect, CerCo aims to go beyond the state of the art in verified compiler technology. |
---|
89 | |
---|
90 | Arguably, the CompCert C compiler currently represents the state of the art in the field of verified compilers. |
---|
91 | However, the verified backend of the CompCert C compiler stops at Power PC and ARM assembly \emph{languages}. |
---|
92 | Assembly of these languages into machine code is left untrusted. |
---|
93 | We aim to go further. |
---|
94 | |
---|
95 | The 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} |
---|