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} |
---|