source: Deliverables/D2.1/Revision/report.toc @ 2732

Last change on this file since 2732 was 792, checked in by amadio, 10 years ago

Deliverable D2.1 with addendum

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