Ignore:
Timestamp:
May 22, 2012, 8:14:57 AM (8 years ago)
Author:
amadio
Message:

add 2.1 Survey

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.1/report.toc

    r59 r1982  
    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 TracChangeset for help on using the changeset viewer.