source: Deliverables/D2.1/report.toc @ 1462

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

Added a new appendix for assessment within the CerCo? project.

File size: 7.7 KB
Line 
1\select@language {english}
2\contentsline {paragraph}{Abstract}{2}{section*.1}
3\contentsline {section}{\numberline {1}Introduction}{5}{section.1}
4\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}
5\contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}
6\contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}
7\contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}
8\contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}
9\contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}
10\contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}
11\contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}
12\contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}
13\contentsline {subsection}{\numberline {2.1}{\sf Imp}: language and semantics}{9}{subsection.2.1}
14\contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}
15\contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}
16\contentsline {subsection}{\numberline {2.4}{\sf Vm}: language and semantics}{11}{subsection.2.4}
17\contentsline {subsection}{\numberline {2.5}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{12}{subsection.2.5}
18\contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}
19\contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}
20\contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}
21\contentsline {subsection}{\numberline {2.9}${\sf Mips}$: language and semantics}{13}{subsection.2.9}
22\contentsline {subsection}{\numberline {2.10}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{14}{subsection.2.10}
23\contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}
24\contentsline {subsection}{\numberline {3.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{15}{subsection.3.1}
25\contentsline {subsection}{\numberline {3.2}${\sf Imp}$ cost annotation}{16}{subsection.3.2}
26\contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}
27\contentsline {subsection}{\numberline {3.4}${\sf Coq}$ development}{18}{subsection.3.4}
28\contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}
29\contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}
30\contentsline {subsection}{\numberline {4.1}Labelled ${\sf Imp}$}{18}{subsection.4.1}
31\contentsline {subsection}{\numberline {4.2}Labelled ${\sf Vm}$}{19}{subsection.4.2}
32\contentsline {subsection}{\numberline {4.3}Labelled ${\sf Mips}$}{20}{subsection.4.3}
33\contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}
34\contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}
35\contentsline {section}{\numberline {5}A ${\sf C}$ compiler}{23}{section.5}
36\contentsline {subsection}{\numberline {5.1}${\sf Clight}$}{23}{subsection.5.1}
37\contentsline {subsection}{\numberline {5.2}${\sf Cminor}$}{23}{subsection.5.2}
38\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$.}{23}{section*.3}
39\contentsline {subsection}{\numberline {5.3}${\sf RTLAbs}$}{23}{subsection.5.3}
40\contentsline {paragraph}{Syntax.}{26}{section*.4}
41\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{26}{section*.5}
42\contentsline {subsection}{\numberline {5.4}${\sf RTL}$}{27}{subsection.5.4}
43\contentsline {paragraph}{Syntax.}{27}{section*.6}
44\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{27}{section*.7}
45\contentsline {subsection}{\numberline {5.5}${\sf ERTL}$}{27}{subsection.5.5}
46\contentsline {paragraph}{Syntax.}{28}{section*.8}
47\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{28}{section*.9}
48\contentsline {paragraph}{Optimizations.}{28}{section*.10}
49\contentsline {subsection}{\numberline {5.6}${\sf LTL}$}{29}{subsection.5.6}
50\contentsline {paragraph}{Syntax.}{29}{section*.11}
51\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{29}{section*.12}
52\contentsline {paragraph}{Optimizations.}{29}{section*.13}
53\contentsline {subsection}{\numberline {5.7}${\sf LIN}$}{30}{subsection.5.7}
54\contentsline {paragraph}{Syntax.}{30}{section*.14}
55\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{30}{section*.15}
56\contentsline {subsection}{\numberline {5.8}${\sf Mips}$}{30}{subsection.5.8}
57\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{30}{section*.16}
58\contentsline {section}{\numberline {6}Labelling approach for the ${\sf C}$ compiler}{31}{section.6}
59\contentsline {subsection}{\numberline {6.1}Labelled ${\sf Clight}$ and labelled ${\sf Cminor}$}{31}{subsection.6.1}
60\contentsline {subsection}{\numberline {6.2}Labels in ${\sf RTLAbs}$ and the back-end languages}{32}{subsection.6.2}
61\contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}
62\contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}
63\contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}
64\contentsline {paragraph}{Related cases.}{33}{section*.17}
65\contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}
66\contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}
67\contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}
68\contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}
69\contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}
70\contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}
71\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
72\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
73\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}
74\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}
75\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}
76\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundness-small-step}}{40}{subsection.B.2}
77\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{41}{subsection.B.3}
78\contentsline {paragraph}{The memory realisation.}{41}{section*.19}
79\contentsline {paragraph}{The inequation.}{41}{section*.20}
80\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annot-composition}}{41}{subsection.B.4}
81\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelled-sim-imp-vm}}{42}{subsection.B.5}
82\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {sim-vm-mips-prop}}{42}{subsection.B.6}
83\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {lab-instr-erasure-imp}}{42}{subsection.B.7}
84\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {global-commutation-prop}}{42}{subsection.B.8}
85\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrument-to-label-prop}}{42}{subsection.B.9}
86\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {sound-label-prop}}{43}{subsection.B.10}
87\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {precise-label-prop}}{43}{subsection.B.11}
88\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {lab-sound}}{43}{subsection.B.12}
89\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref {ann-correct}}{43}{subsection.B.13}
Note: See TracBrowser for help on using the repository browser.