source: Deliverables/D2.1/Revision/report.aux @ 1635

Last change on this file since 1635 was 792, checked in by amadio, 9 years ago

Deliverable D2.1 with addendum

File size: 17.1 KB
Line 
1\relax
2\ifx\hyper@anchor\@undefined
3\global \let \oldcontentsline\contentsline
4\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
5\global \let \oldnewlabel\newlabel
6\gdef \newlabel#1#2{\newlabelxx{#1}#2}
7\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
8\AtEndDocument{\let \contentsline\oldcontentsline
9\let \newlabel\oldnewlabel}
10\else
11\global \let \hyper@last\relax
12\fi
13
14\bibstyle{abbrv}
15\select@language{english}
16\@writefile{toc}{\select@language{english}}
17\@writefile{lof}{\select@language{english}}
18\@writefile{lot}{\select@language{english}}
19\@writefile{toc}{\contentsline {paragraph}{Abstract}{2}{section*.1}}
20\citation{Leroy09}
21\citation{Cerco10}
22\citation{SCADE}
23\citation{Fornari10}
24\citation{AbsInt}
25\citation{AbsintScade}
26\citation{W09}
27\citation{Frama-C}
28\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{5}{section.1}}
29\newlabel{intro-sec}{{1}{5}{Introduction\relax }{section.1}{}}
30\@writefile{toc}{\contentsline {paragraph}{Meaning of cost annotations}{5}{section*.3}}
31\@writefile{toc}{\contentsline {paragraph}{Soundness and precision of cost annotations}{6}{section*.4}}
32\newlabel{comp-intro}{{1}{6}{Compositionality\relax }{section*.5}{}}
33\@writefile{toc}{\contentsline {paragraph}{Compositionality}{6}{section*.5}}
34\newlabel{label-intro}{{1}{6}{Labelling approach to cost annotations\relax }{section*.6}{}}
35\@writefile{toc}{\contentsline {paragraph}{Labelling approach to cost annotations}{6}{section*.6}}
36\newlabel{STEP1}{{1}{7}{Labelling approach to cost annotations\relax }{equation.1.1}{}}
37\newlabel{step2}{{2}{7}{Labelling approach to cost annotations\relax }{equation.1.2}{}}
38\newlabel{toy-intro}{{1}{7}{A toy compiler\relax }{section*.7}{}}
39\@writefile{toc}{\contentsline {paragraph}{A toy compiler}{7}{section*.7}}
40\citation{Leroy09}
41\citation{CIL02}
42\citation{Pottier}
43\citation{intel94}
44\citation{share}
45\newlabel{Ccompiler-intro}{{1}{8}{A C compiler\relax }{section*.8}{}}
46\@writefile{toc}{\contentsline {paragraph}{A C compiler}{8}{section*.8}}
47\@writefile{toc}{\contentsline {paragraph}{Organization}{8}{section*.9}}
48\@writefile{toc}{\contentsline {section}{\numberline {2}Labelling approach for the toy compiler}{8}{section.2}}
49\newlabel{label-toy-sec}{{2}{8}{Labelling approach for the toy compiler\relax }{section.2}{}}
50\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax definitions.}}{9}{figure.1}}
51\newlabel{fig:syntaxes}{{1}{9}{Syntax definitions}{figure.1}{}}
52\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Labelled ${\sf  Imp}$}{9}{subsection.2.1}}
53\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Labelled ${\sf  Vm}$}{9}{subsection.2.2}}
54\newlabel{labelled-sim-imp-vm}{{1}{10}{Labelled $\vm $\relax }{theorem.1}{}}
55\newlabel{rem:multi-set}{{2}{10}{Labelled $\vm $\relax }{theorem.2}{}}
56\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Labelled ${\sf  Mips}$}{10}{subsection.2.3}}
57\newlabel{sim-vm-mips-prop}{{3}{10}{Labelled $\mips $\relax }{theorem.3}{}}
58\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Labellings and instrumentations}{10}{subsection.2.4}}
59\newlabel{lab-instr-erasure-imp}{{4}{11}{Labellings and instrumentations\relax }{theorem.4}{}}
60\newlabel{labelling-def}{{5}{11}{Labellings and instrumentations\relax }{theorem.5}{}}
61\newlabel{global-commutation-prop}{{6}{11}{Labellings and instrumentations\relax }{theorem.6}{}}
62\newlabel{instrument-to-label-prop}{{7}{11}{Labellings and instrumentations\relax }{theorem.7}{}}
63\@writefile{toc}{\contentsline {subsection}{\numberline {2.5}Sound and precise labellings}{11}{subsection.2.5}}
64\newlabel{sound-label-sec}{{2.5}{11}{Sound and precise labellings\relax }{subsection.2.5}{}}
65\newlabel{sound-label-prop}{{10}{11}{Sound and precise labellings\relax }{theorem.10}{}}
66\newlabel{precise-label-prop}{{12}{11}{Sound and precise labellings\relax }{theorem.12}{}}
67\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Two labellings for the ${\sf  Imp}$ language}}{12}{table.1}}
68\newlabel{labelling}{{1}{12}{Two labellings for the $\imp $ language\relax }{table.1}{}}
69\newlabel{lab-sound}{{13}{12}{Sound and precise labellings\relax }{theorem.13}{}}
70\newlabel{ann-correct}{{15}{12}{Sound and precise labellings\relax }{theorem.15}{}}
71\@writefile{toc}{\contentsline {section}{\numberline {3}Labelling approach for the ${\sf  C}$ compiler}{13}{section.3}}
72\newlabel{C-label-sec}{{3}{13}{Labelling approach for the $\C $ compiler\relax }{section.3}{}}
73\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Labelled languages}{13}{subsection.3.1}}
74\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Labelling of the source language}{14}{subsection.3.2}}
75\@writefile{toc}{\contentsline {paragraph}{Sequential instructions}{14}{section*.10}}
76\@writefile{toc}{\contentsline {paragraph}{Ternary expressions and conditionals}{14}{section*.11}}
77\@writefile{toc}{\contentsline {paragraph}{Loops}{14}{section*.12}}
78\@writefile{toc}{\contentsline {paragraph}{Program Labels and Gotos}{14}{section*.13}}
79\newlabel{fun-call-sec}{{3.2}{14}{Function calls\relax }{section*.14}{}}
80\@writefile{toc}{\contentsline {paragraph}{Function calls}{14}{section*.14}}
81\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Verifications on the object code}{15}{subsection.3.3}}
82\citation{Cerco10}
83\bibcite{AbsInt}{1}
84\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Building the cost annotation}{16}{subsection.3.4}}
85\@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Testing}{16}{subsection.3.5}}
86\@writefile{toc}{\contentsline {section}{\numberline {4}Conclusion and future work}{16}{section.4}}
87\newlabel{conclusion-sec}{{4}{16}{Conclusion and future work\relax }{section.4}{}}
88\bibcite{Cerco10}{2}
89\bibcite{SCADE}{3}
90\bibcite{Frama-C}{4}
91\bibcite{AbsintScade}{5}
92\bibcite{Fornari10}{6}
93\bibcite{Larus05}{7}
94\bibcite{intel94}{8}
95\bibcite{Leroy09}{9}
96\bibcite{Leroy09-ln}{10}
97\bibcite{CIL02}{11}
98\bibcite{Pottier}{12}
99\bibcite{W09}{13}
100\bibcite{share}{14}
101\citation{Leroy09-ln}
102\@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Small-step operational semantics of ${\sf  Imp}$ commands}}{18}{table.2}}
103\newlabel{small-step-imp}{{2}{18}{Small-step operational semantics of $\imp $ commands\relax }{table.2}{}}
104\@writefile{toc}{\contentsline {section}{\numberline {A}A toy compiler}{18}{appendix.A}}
105\newlabel{toy-compiler-sec}{{A}{18}{A toy compiler\relax }{appendix.A}{}}
106\@writefile{toc}{\contentsline {subsection}{\numberline {A.1}{\sf  Imp}: language and semantics}{18}{subsection.A.1}}
107\newlabel{imp-sec}{{A.1}{18}{\imp : language and semantics\relax }{subsection.A.1}{}}
108\@writefile{toc}{\contentsline {subsection}{\numberline {A.2}{\sf  Vm}: language and semantics}{18}{subsection.A.2}}
109\newlabel{vm-sec}{{A.2}{18}{\vm : language and semantics\relax }{subsection.A.2}{}}
110\citation{Leroy09-ln}
111\@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Operational semantics ${\sf  Vm}$ programs}}{19}{table.3}}
112\newlabel{semantics-vm}{{3}{19}{Operational semantics $\vm $ programs\relax }{table.3}{}}
113\@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Conditions for well-formed code}}{19}{table.4}}
114\newlabel{well-formed-instr}{{4}{19}{Conditions for well-formed code\relax }{table.4}{}}
115\newlabel{unicity-height-prop}{{17}{19}{\vm : language and semantics\relax }{theorem.17}{}}
116\@writefile{toc}{\contentsline {subsection}{\numberline {A.3}Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}{19}{subsection.A.3}}
117\newlabel{compil-imp-vm-sec}{{A.3}{19}{Compilation from $\imp $ to $\vm $\relax }{subsection.A.3}{}}
118\citation{Larus05}
119\@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}}{20}{table.5}}
120\newlabel{compil-imp-vm}{{5}{20}{Compilation from $\imp $ to $\vm $\relax }{table.5}{}}
121\newlabel{soundness-big-step-prop}{{18}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.18}{}}
122\newlabel{soundness-small-step}{{19}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.19}{}}
123\newlabel{well-formed-prop}{{20}{20}{Compilation from $\imp $ to $\vm $\relax }{theorem.20}{}}
124\@writefile{toc}{\contentsline {subsection}{\numberline {A.4}${\sf  Mips}$: language and semantics}{20}{subsection.A.4}}
125\newlabel{mips-sec}{{A.4}{20}{$\mips $: language and semantics\relax }{subsection.A.4}{}}
126\@writefile{lot}{\contentsline {table}{\numberline {6}{\ignorespaces Operational semantics ${\sf  Mips}$ programs}}{21}{table.6}}
127\newlabel{semantics-mips}{{6}{21}{Operational semantics $\mips $ programs\relax }{table.6}{}}
128\@writefile{lot}{\contentsline {table}{\numberline {7}{\ignorespaces Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}}{21}{table.7}}
129\newlabel{compil-vm-mips}{{7}{21}{Compilation from $\vm $ to $\mips $\relax }{table.7}{}}
130\@writefile{toc}{\contentsline {subsection}{\numberline {A.5}Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}{21}{subsection.A.5}}
131\newlabel{compil-vm-mips-sec}{{A.5}{21}{Compilation from $\vm $ to $\mips $\relax }{subsection.A.5}{}}
132\newlabel{simulation-vm-mips}{{21}{22}{Compilation from $\vm $ to $\mips $\relax }{theorem.21}{}}
133\@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{23}{appendix.B}}
134\newlabel{paper-proofs}{{B}{23}{Proofs\relax }{appendix.B}{}}
135\@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{23}{subsection.B.1}}
136\@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref  {labelled-sim-imp-vm}}{23}{subsection.B.2}}
137\@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref  {sim-vm-mips-prop}}{23}{subsection.B.3}}
138\@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref  {lab-instr-erasure-imp}}{23}{subsection.B.4}}
139\@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref  {global-commutation-prop}}{24}{subsection.B.5}}
140\@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref  {instrument-to-label-prop}}{24}{subsection.B.6}}
141\@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref  {sound-label-prop}}{24}{subsection.B.7}}
142\@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref  {precise-label-prop}}{24}{subsection.B.8}}
143\@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref  {lab-sound}}{25}{subsection.B.9}}
144\newlabel{precise-lemma}{{24}{25}{Proof of proposition \ref {lab-sound}\relax }{theorem.24}{}}
145\@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref  {ann-correct}}{25}{subsection.B.10}}
146\@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref  {soundness-small-step}}{25}{subsection.B.11}}
147\newlabel{access-lemma}{{25}{25}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.25}{}}
148\citation{CIL02}
149\citation{Leroy09}
150\@writefile{toc}{\contentsline {section}{\numberline {C}A ${\sf  C}$ compiler}{27}{appendix.C}}
151\newlabel{C-compiler-sec}{{C}{27}{A $\C $ compiler\relax }{appendix.C}{}}
152\@writefile{toc}{\contentsline {subsection}{\numberline {C.1}${\sf  Clight}$}{27}{subsection.C.1}}
153\@writefile{toc}{\contentsline {subsection}{\numberline {C.2}${\sf  Cminor}$}{27}{subsection.C.2}}
154\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Clight}$ to ${\sf  Cminor}$}{27}{section*.16}}
155\@writefile{toc}{\contentsline {subsection}{\numberline {C.3}${\sf  RTLAbs}$}{27}{subsection.C.3}}
156\newlabel{syntax-clight}{{C.1}{28}{$\Clight $\relax }{subsection.C.1}{}}
157\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Syntax of the ${\sf  Clight}$ language}}{28}{figure.2}}
158\newlabel{syntax-cminor}{{C.2}{29}{$\Cminor $\relax }{subsection.C.2}{}}
159\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Syntax of the ${\sf  Cminor}$ language}}{29}{figure.3}}
160\@writefile{lot}{\contentsline {table}{\numberline {8}{\ignorespaces Syntax of the ${\sf  RTLAbs}$ language}}{30}{table.8}}
161\newlabel{RTLAbs:syntax}{{8}{30}{Syntax of the $\RTLAbs $ language\relax }{table.8}{}}
162\@writefile{toc}{\contentsline {paragraph}{Syntax.}{30}{section*.17}}
163\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Cminor}$ to ${\sf  RTLAbs}$.}{30}{section*.18}}
164\@writefile{lot}{\contentsline {table}{\numberline {9}{\ignorespaces Syntax of the ${\sf  RTL}$ language}}{31}{table.9}}
165\newlabel{RTL:syntax}{{9}{31}{Syntax of the $\RTL $ language\relax }{table.9}{}}
166\@writefile{toc}{\contentsline {subsection}{\numberline {C.4}${\sf  RTL}$}{31}{subsection.C.4}}
167\@writefile{toc}{\contentsline {paragraph}{Syntax.}{31}{section*.19}}
168\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTLAbs}$ to ${\sf  RTL}$.}{31}{section*.20}}
169\@writefile{toc}{\contentsline {subsection}{\numberline {C.5}${\sf  ERTL}$}{31}{subsection.C.5}}
170\@writefile{lot}{\contentsline {table}{\numberline {10}{\ignorespaces Syntax of the ${\sf  ERTL}$ language}}{32}{table.10}}
171\newlabel{ERTL:syntax}{{10}{32}{Syntax of the $\ERTL $ language\relax }{table.10}{}}
172\@writefile{toc}{\contentsline {paragraph}{Syntax.}{32}{section*.21}}
173\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTL}$ to ${\sf  ERTL}$.}{32}{section*.22}}
174\@writefile{lot}{\contentsline {table}{\numberline {11}{\ignorespaces Syntax of the ${\sf  LTL}$ language}}{33}{table.11}}
175\newlabel{LTL:syntax}{{11}{33}{Syntax of the $\LTL $ language\relax }{table.11}{}}
176\@writefile{toc}{\contentsline {paragraph}{Optimizations.}{33}{section*.23}}
177\@writefile{toc}{\contentsline {subsection}{\numberline {C.6}${\sf  LTL}$}{33}{subsection.C.6}}
178\@writefile{toc}{\contentsline {paragraph}{Syntax.}{33}{section*.24}}
179\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  ERTL}$ to ${\sf  LTL}$.}{33}{section*.25}}
180\@writefile{toc}{\contentsline {paragraph}{Optimizations.}{33}{section*.26}}
181\citation{intel94}
182\@writefile{lot}{\contentsline {table}{\numberline {12}{\ignorespaces Syntax of the ${\sf  LIN}$ language}}{34}{table.12}}
183\newlabel{LIN:syntax}{{12}{34}{Syntax of the $\LIN $ language\relax }{table.12}{}}
184\@writefile{toc}{\contentsline {subsection}{\numberline {C.7}${\sf  LIN}$}{34}{subsection.C.7}}
185\@writefile{toc}{\contentsline {paragraph}{Syntax.}{34}{section*.27}}
186\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LTL}$ to ${\sf  LIN}$.}{34}{section*.28}}
187\@writefile{toc}{\contentsline {subsection}{\numberline {C.8}Assembly}{34}{subsection.C.8}}
188\@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LIN}$ to ${\sf  Mips}$.}{34}{section*.29}}
189\@writefile{lot}{\contentsline {table}{\numberline {13}{\ignorespaces Syntax of the ${\sf  Mips}$ language}}{35}{table.13}}
190\newlabel{mips:syntax}{{13}{35}{Syntax of the $\mips $ language\relax }{table.13}{}}
191\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Benchmarks results (execution time is given in seconds).}}{35}{figure.4}}
192\newlabel{fig:benchmark-results}{{4}{35}{Benchmarks results (execution time is given in seconds)}{figure.4}{}}
193\@writefile{toc}{\contentsline {subsection}{\numberline {C.9}Benchmarks}{36}{subsection.C.9}}
194\newlabel{C-compiler-benchmarks}{{C.9}{36}{Benchmarks\relax }{subsection.C.9}{}}
195\@writefile{toc}{\contentsline {section}{\numberline {D}A direct approach}{37}{appendix.D}}
196\newlabel{direct-sec}{{D}{37}{A direct approach\relax }{appendix.D}{}}
197\@writefile{toc}{\contentsline {subsection}{\numberline {D.1}${\sf  Mips}$ and ${\sf  Vm}$ cost annotations}{37}{subsection.D.1}}
198\@writefile{lot}{\contentsline {table}{\numberline {14}{\ignorespaces Upper bounds on the cost of ${\sf  Vm}$ instructions}}{38}{table.14}}
199\newlabel{cost-approx-instr}{{14}{38}{Upper bounds on the cost of $\vm $ instructions\relax }{table.14}{}}
200\newlabel{annot-vm-mips}{{26}{38}{$\mips $ and $\vm $ cost annotations\relax }{theorem.26}{}}
201\newlabel{labelled-simulation-vm-mips}{{27}{38}{$\mips $ and $\vm $ cost annotations\relax }{theorem.27}{}}
202\@writefile{toc}{\contentsline {subsection}{\numberline {D.2}${\sf  Imp}$ cost annotation}{38}{subsection.D.2}}
203\newlabel{imp-cost-annotation}{{D.2}{38}{$\imp $ cost annotation\relax }{subsection.D.2}{}}
204\@writefile{lot}{\contentsline {table}{\numberline {15}{\ignorespaces Annotation for ${\sf  Imp}$ programs}}{39}{table.15}}
205\newlabel{annotation-imp}{{15}{39}{Annotation for $\imp $ programs\relax }{table.15}{}}
206\newlabel{annot-imp-vm}{{28}{39}{$\imp $ cost annotation\relax }{theorem.28}{}}
207\citation{Leroy09-ln}
208\@writefile{toc}{\contentsline {subsection}{\numberline {D.3}Composition}{40}{subsection.D.3}}
209\newlabel{annot-composition}{{29}{40}{Composition\relax }{theorem.29}{}}
210\@writefile{toc}{\contentsline {subsection}{\numberline {D.4}${\sf  Coq}$ development}{40}{subsection.D.4}}
211\newlabel{coq-development-sec}{{D.4}{40}{$\coq $ development\relax }{subsection.D.4}{}}
212\@writefile{toc}{\contentsline {subsection}{\numberline {D.5}Limitations of the direct approach}{40}{subsection.D.5}}
213\newlabel{limitations-direct-sec}{{D.5}{40}{Limitations of the direct approach\relax }{subsection.D.5}{}}
214\@writefile{toc}{\contentsline {section}{\numberline {E}Related approaches}{41}{appendix.E}}
215\newlabel{related-sec}{{E}{41}{Related approaches\relax }{appendix.E}{}}
216\@writefile{toc}{\contentsline {section}{\numberline {F}Assessment of the deliverable within the $CerCo$ project, with hindsight}{42}{appendix.F}}
217\newlabel{asmt-sec}{{F}{42}{Assessment of the deliverable within the $\cerco $ project, with hindsight\relax }{appendix.F}{}}
Note: See TracBrowser for help on using the repository browser.