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