source: Deliverables/D2.1/Revision/root.toc @ 1635

Last change on this file since 1635 was 792, checked in by amadio, 9 years ago

Deliverable D2.1 with addendum

File size: 5.2 KB
Line 
1\contentsline {section}{\numberline {1}Introduction}{4}
2\contentsline {paragraph}{Meaning of cost annotations}{4}
3\contentsline {paragraph}{Soundness and precision of cost annotations}{5}
4\contentsline {paragraph}{Compositionality}{5}
5\contentsline {paragraph}{Labelling approach to cost annotations}{5}
6\contentsline {paragraph}{A toy compiler}{6}
7\contentsline {paragraph}{A C compiler}{7}
8\contentsline {paragraph}{Organization}{7}
9\contentsline {section}{\numberline {2}Labelling approach for the toy compiler}{7}
10\contentsline {subsection}{\numberline {2.1}Labelled ${\sf Imp}$}{8}
11\contentsline {subsection}{\numberline {2.2}Labelled ${\sf Vm}$}{8}
12\contentsline {subsection}{\numberline {2.3}Labelled ${\sf Mips}$}{9}
13\contentsline {subsection}{\numberline {2.4}Labellings and instrumentations}{9}
14\contentsline {subsection}{\numberline {2.5}Sound and precise labellings}{10}
15\contentsline {section}{\numberline {3}Labelling approach for the ${\sf C}$ compiler}{12}
16\contentsline {subsection}{\numberline {3.1}Labelled languages}{12}
17\contentsline {subsection}{\numberline {3.2}Labelling of the source language}{13}
18\contentsline {paragraph}{Sequential instructions}{13}
19\contentsline {paragraph}{Ternary expressions and conditionals}{13}
20\contentsline {paragraph}{Loops}{13}
21\contentsline {paragraph}{Program Labels and Gotos}{13}
22\contentsline {paragraph}{Function calls}{13}
23\contentsline {subsection}{\numberline {3.3}Verifications on the object code}{14}
24\contentsline {subsection}{\numberline {3.4}Building the cost annotation}{15}
25\contentsline {subsection}{\numberline {3.5}Testing}{15}
26\contentsline {section}{\numberline {4}Conclusion and future work}{15}
27\contentsline {section}{\numberline {A}A toy compiler}{17}
28\contentsline {subsection}{\numberline {A.1}{\sf Imp}: language and semantics}{17}
29\contentsline {subsection}{\numberline {A.2}{\sf Vm}: language and semantics}{17}
30\contentsline {subsection}{\numberline {A.3}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{18}
31\contentsline {subsection}{\numberline {A.4}${\sf Mips}$: language and semantics}{19}
32\contentsline {subsection}{\numberline {A.5}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{20}
33\contentsline {section}{\numberline {B}Proofs}{21}
34\contentsline {subsection}{\numberline {B.1}Notation}{21}
35\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {labelled-sim-imp-vm}}{21}
36\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {sim-vm-mips-prop}}{21}
37\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {lab-instr-erasure-imp}}{22}
38\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {global-commutation-prop}}{22}
39\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {instrument-to-label-prop}}{22}
40\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {sound-label-prop}}{22}
41\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {precise-label-prop}}{23}
42\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {lab-sound}}{23}
43\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {ann-correct}}{23}
44\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {soundness-small-step}}{23}
45\contentsline {section}{\numberline {C}A ${\sf C}$ compiler}{25}
46\contentsline {subsection}{\numberline {C.1}${\sf Clight}$}{25}
47\contentsline {subsection}{\numberline {C.2}${\sf Cminor}$}{25}
48\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$}{25}
49\contentsline {subsection}{\numberline {C.3}${\sf RTLAbs}$}{25}
50\contentsline {paragraph}{Syntax.}{28}
51\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{28}
52\contentsline {subsection}{\numberline {C.4}${\sf RTL}$}{29}
53\contentsline {paragraph}{Syntax.}{29}
54\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{29}
55\contentsline {subsection}{\numberline {C.5}${\sf ERTL}$}{29}
56\contentsline {paragraph}{Syntax.}{30}
57\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{30}
58\contentsline {paragraph}{Optimizations.}{31}
59\contentsline {subsection}{\numberline {C.6}${\sf LTL}$}{31}
60\contentsline {paragraph}{Syntax.}{31}
61\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{31}
62\contentsline {paragraph}{Optimizations.}{31}
63\contentsline {subsection}{\numberline {C.7}${\sf LIN}$}{32}
64\contentsline {paragraph}{Syntax.}{32}
65\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{32}
66\contentsline {subsection}{\numberline {C.8}Assembly}{32}
67\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{32}
68\contentsline {subsection}{\numberline {C.9}Benchmarks}{34}
69\contentsline {section}{\numberline {D}A direct approach}{35}
70\contentsline {subsection}{\numberline {D.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{35}
71\contentsline {subsection}{\numberline {D.2}${\sf Imp}$ cost annotation}{36}
72\contentsline {subsection}{\numberline {D.3}Composition}{38}
73\contentsline {subsection}{\numberline {D.4}${\sf Coq}$ development}{38}
74\contentsline {subsection}{\numberline {D.5}Limitations of the direct approach}{38}
75\contentsline {section}{\numberline {E}Related approaches}{39}
76\contentsline {section}{\numberline {F}Assessment of the deliverable within the ${\sf CerCo}$ project, with hindsight}{39}
77\select@language {english}
Note: See TracBrowser for help on using the repository browser.