\contentsline {section}{\numberline {1}Introduction}{4}
\contentsline {paragraph}{Meaning of cost annotations}{4}
\contentsline {paragraph}{Soundness and precision of cost annotations}{5}
\contentsline {paragraph}{Compositionality}{5}
\contentsline {paragraph}{Labelling approach to cost annotations}{5}
\contentsline {paragraph}{A toy compiler}{6}
\contentsline {paragraph}{A C compiler}{7}
\contentsline {paragraph}{Organization}{7}
\contentsline {section}{\numberline {2}Labelling approach for the toy compiler}{7}
\contentsline {subsection}{\numberline {2.1}Labelled ${\sf Imp}$}{8}
\contentsline {subsection}{\numberline {2.2}Labelled ${\sf Vm}$}{8}
\contentsline {subsection}{\numberline {2.3}Labelled ${\sf Mips}$}{9}
\contentsline {subsection}{\numberline {2.4}Labellings and instrumentations}{9}
\contentsline {subsection}{\numberline {2.5}Sound and precise labellings}{10}
\contentsline {section}{\numberline {3}Labelling approach for the ${\sf C}$ compiler}{12}
\contentsline {subsection}{\numberline {3.1}Labelled languages}{12}
\contentsline {subsection}{\numberline {3.2}Labelling of the source language}{13}
\contentsline {paragraph}{Sequential instructions}{13}
\contentsline {paragraph}{Ternary expressions and conditionals}{13}
\contentsline {paragraph}{Loops}{13}
\contentsline {paragraph}{Program Labels and Gotos}{13}
\contentsline {paragraph}{Function calls}{13}
\contentsline {subsection}{\numberline {3.3}Verifications on the object code}{14}
\contentsline {subsection}{\numberline {3.4}Building the cost annotation}{15}
\contentsline {subsection}{\numberline {3.5}Testing}{15}
\contentsline {section}{\numberline {4}Conclusion and future work}{15}
\contentsline {section}{\numberline {A}A toy compiler}{17}
\contentsline {subsection}{\numberline {A.1}{\sf Imp}: language and semantics}{17}
\contentsline {subsection}{\numberline {A.2}{\sf Vm}: language and semantics}{17}
\contentsline {subsection}{\numberline {A.3}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{18}
\contentsline {subsection}{\numberline {A.4}${\sf Mips}$: language and semantics}{19}
\contentsline {subsection}{\numberline {A.5}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{20}
\contentsline {section}{\numberline {B}Proofs}{21}
\contentsline {subsection}{\numberline {B.1}Notation}{21}
\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {labelled-sim-imp-vm}}{21}
\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {sim-vm-mips-prop}}{21}
\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {lab-instr-erasure-imp}}{22}
\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {global-commutation-prop}}{22}
\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {instrument-to-label-prop}}{22}
\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {sound-label-prop}}{22}
\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {precise-label-prop}}{23}
\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {lab-sound}}{23}
\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {ann-correct}}{23}
\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {soundness-small-step}}{23}
\contentsline {section}{\numberline {C}A ${\sf C}$ compiler}{25}
\contentsline {subsection}{\numberline {C.1}${\sf Clight}$}{25}
\contentsline {subsection}{\numberline {C.2}${\sf Cminor}$}{25}
\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$}{25}
\contentsline {subsection}{\numberline {C.3}${\sf RTLAbs}$}{25}
\contentsline {paragraph}{Syntax.}{28}
\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{28}
\contentsline {subsection}{\numberline {C.4}${\sf RTL}$}{29}
\contentsline {paragraph}{Syntax.}{29}
\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{29}
\contentsline {subsection}{\numberline {C.5}${\sf ERTL}$}{29}
\contentsline {paragraph}{Syntax.}{30}
\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{30}
\contentsline {paragraph}{Optimizations.}{31}
\contentsline {subsection}{\numberline {C.6}${\sf LTL}$}{31}
\contentsline {paragraph}{Syntax.}{31}
\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{31}
\contentsline {paragraph}{Optimizations.}{31}
\contentsline {subsection}{\numberline {C.7}${\sf LIN}$}{32}
\contentsline {paragraph}{Syntax.}{32}
\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{32}
\contentsline {subsection}{\numberline {C.8}Assembly}{32}
\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{32}
\contentsline {subsection}{\numberline {C.9}Benchmarks}{34}
\contentsline {section}{\numberline {D}A direct approach}{35}
\contentsline {subsection}{\numberline {D.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{35}
\contentsline {subsection}{\numberline {D.2}${\sf Imp}$ cost annotation}{36}
\contentsline {subsection}{\numberline {D.3}Composition}{38}
\contentsline {subsection}{\numberline {D.4}${\sf Coq}$ development}{38}
\contentsline {subsection}{\numberline {D.5}Limitations of the direct approach}{38}
\contentsline {section}{\numberline {E}Related approaches}{39}
\contentsline {section}{\numberline {F}Assessment of the deliverable within the ${\sf CerCo}$ project, with hindsight}{39}
\select@language {english}