Changeset 59


Ignore:
Timestamp:
Sep 10, 2010, 3:51:04 PM (8 years ago)
Author:
sacerdot
Message:

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

Location:
Deliverables/D2.1
Files:
6 edited

Legend:

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

    r39 r59  
    202202\bibcite{Pottier}{12}
    203203\bibcite{W09}{13}
    204 \@writefile{toc}{\contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}}
    205 \newlabel{paper-proofs}{{A}{38}{Proofs\relax }{appendix.A}{}}
    206 \@writefile{toc}{\contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}}
    207 \@writefile{toc}{\contentsline {subsection}{\numberline {A.2}Proof of proposition \ref  {soundness-small-step}}{38}{subsection.A.2}}
    208 \newlabel{access-lemma}{{26}{38}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
    209 \@writefile{toc}{\contentsline {subsection}{\numberline {A.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{39}{subsection.A.3}}
    210 \newlabel{step1}{{7}{39}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.A.7}{}}
    211 \@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{39}{section*.19}}
    212 \@writefile{toc}{\contentsline {paragraph}{The inequation.}{39}{section*.20}}
    213 \@writefile{toc}{\contentsline {subsection}{\numberline {A.4}Proof of proposition \ref  {annot-composition}}{39}{subsection.A.4}}
    214 \@writefile{toc}{\contentsline {subsection}{\numberline {A.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{40}{subsection.A.5}}
    215 \@writefile{toc}{\contentsline {subsection}{\numberline {A.6}Proof of proposition \ref  {sim-vm-mips-prop}}{40}{subsection.A.6}}
    216 \@writefile{toc}{\contentsline {subsection}{\numberline {A.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{40}{subsection.A.7}}
    217 \@writefile{toc}{\contentsline {subsection}{\numberline {A.8}Proof of proposition \ref  {global-commutation-prop}}{40}{subsection.A.8}}
    218 \@writefile{toc}{\contentsline {subsection}{\numberline {A.9}Proof of proposition \ref  {instrument-to-label-prop}}{40}{subsection.A.9}}
    219 \@writefile{toc}{\contentsline {subsection}{\numberline {A.10}Proof of proposition \ref  {sound-label-prop}}{41}{subsection.A.10}}
    220 \@writefile{toc}{\contentsline {subsection}{\numberline {A.11}Proof of proposition \ref  {precise-label-prop}}{41}{subsection.A.11}}
    221 \@writefile{toc}{\contentsline {subsection}{\numberline {A.12}Proof of proposition \ref  {lab-sound}}{41}{subsection.A.12}}
    222 \newlabel{precise-lemma}{{29}{41}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
    223 \@writefile{toc}{\contentsline {subsection}{\numberline {A.13}Proof of proposition \ref  {ann-correct}}{41}{subsection.A.13}}
     204\@writefile{toc}{\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}}
     205\@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}}
     206\newlabel{paper-proofs}{{B}{40}{Proofs\relax }{appendix.B}{}}
     207\@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}}
     208\@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref  {soundness-small-step}}{40}{subsection.B.2}}
     209\newlabel{access-lemma}{{26}{40}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
     210\@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{41}{subsection.B.3}}
     211\newlabel{step1}{{7}{41}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.B.7}{}}
     212\@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{41}{section*.19}}
     213\@writefile{toc}{\contentsline {paragraph}{The inequation.}{41}{section*.20}}
     214\@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref  {annot-composition}}{41}{subsection.B.4}}
     215\@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{42}{subsection.B.5}}
     216\@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref  {sim-vm-mips-prop}}{42}{subsection.B.6}}
     217\@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{42}{subsection.B.7}}
     218\@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref  {global-commutation-prop}}{42}{subsection.B.8}}
     219\@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref  {instrument-to-label-prop}}{42}{subsection.B.9}}
     220\@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref  {sound-label-prop}}{43}{subsection.B.10}}
     221\@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref  {precise-label-prop}}{43}{subsection.B.11}}
     222\@writefile{toc}{\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref  {lab-sound}}{43}{subsection.B.12}}
     223\newlabel{precise-lemma}{{29}{43}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
     224\@writefile{toc}{\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref  {ann-correct}}{43}{subsection.B.13}}
  • Deliverables/D2.1/report.log

    r40 r59  
    1 This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.8.30)  6 SEP 2010 10:17
     1This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.8.31)  10 SEP 2010 16:02
    22entering extended mode
    33 restricted \write18 enabled.
     
    77LaTeX2e <2009/09/24>
    88Babel <v3.8l> and hyphenation patterns for english, usenglishmax, dumylang, noh
    9 yphenation, loaded.
     9yphenation, french, basque, italian, loaded.
    1010(/usr/share/texmf-texlive/tex/latex/base/article.cls
    1111Document Class: article 2007/10/19 v1.4h Standard LaTeX document class
     
    4545
    4646(/usr/share/texmf-texlive/tex/latex/pdftex-def/pdftex.def
    47 File: pdftex.def 2009/08/25 v0.04m Graphics/color for pdfTeX
     47File: pdftex.def 2010/03/12 v0.04p Graphics/color for pdfTeX
    4848\Gread@gobject=\count87
    4949))
     
    417417LaTeX Font Info:    Checking defaults for PD1/pdf/m/n on input line 538.
    418418LaTeX Font Info:    ... okay on input line 538.
    419  (/usr/share/texmf/tex/context/base/supp-pdf.mkii
     419 (/usr/share/texmf-texlive/tex/context/base/supp-pdf.mkii
    420420[Loading MPS to PDF converter (version 2006.09.02).]
    421421\scratchcounter=\count119
     
    447447
    448448\AtBeginShipoutBox=\box33
    449  <../style/cerco_logo.png, id=279, 804.00375pt x 213.79875pt>
     449 <../style/cerco_logo.png, id=283, 804.00375pt x 213.79875pt>
    450450File: ../style/cerco_logo.png Graphic file (type png)
    451451
     
    768768 []
    769769
    770 [37] [38] [39] [40]) [41] (./report.aux)
     770[37]
     771
     772Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
     773(hyperref)                removing `math shift' on input line 3053.
     774
     775
     776Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
     777(hyperref)                removing `math shift' on input line 3053.
     778
     779[38] [39] [40] [41] [42]) [43] (./report.aux)
    771780
    772781LaTeX Font Warning: Some font shapes were not available, defaults substituted.
     
    774783 )
    775784Here is how much of TeX's memory you used:
    776  8510 strings out of 495061
    777  110648 string characters out of 1182621
    778  247458 words of memory out of 3000000
    779  11286 multiletter control sequences out of 15000+50000
     785 8519 strings out of 495021
     786 110783 string characters out of 1180926
     787 247727 words of memory out of 3000000
     788 11300 multiletter control sequences out of 15000+50000
    780789 28130 words of font info for 114 fonts, out of 3000000 for 9000
    781790 28 hyphenation exceptions out of 8191
     
    789798b></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cmextra/cmex9.pfb></usr
    790799/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texm
    791 f-texlive/fonts/type1/public/amsfonts/cm/cmmi5.pfb></usr/share/texmf-texlive/fo
    792 nts/type1/public/amsfonts/cm/cmmi6.pfb></usr/share/texmf-texlive/fonts/type1/pu
    793 blic/amsfonts/cm/cmmi8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfont
    794 s/cm/cmmi9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr10.p
    795 fb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/sha
    796 re/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texmf-tex
    797 live/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/share/texmf-texlive/fonts/ty
    798 pe1/public/amsfonts/cm/cmr6.pfb></usr/share/texmf-texlive/fonts/type1/public/am
    799 sfonts/cm/cmr8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr
    800 9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr
    801 /share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texm
    802 f-texlive/fonts/type1/public/amsfonts/cm/cmss12.pfb></usr/share/texmf-texlive/f
    803 onts/type1/public/amsfonts/cm/cmss8.pfb></usr/share/texmf-texlive/fonts/type1/p
    804 ublic/amsfonts/cm/cmss9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfon
    805 ts/cm/cmsy10.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy5
    806 .pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy6.pfb></usr/s
    807 hare/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texmf-t
    808 exlive/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/texmf-texlive/fonts
    809 /type1/public/amsfonts/cm/cmti10.pfb></usr/share/texmf-texlive/fonts/type1/publ
    810 ic/amsfonts/cm/cmti7.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/
    811 cm/cmti8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmti9.pfb
    812 ></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/shar
    813 e/texmf-texlive/fonts/type1/public/amsfonts/cm/cmtt9.pfb></usr/share/texmf-texl
    814 ive/fonts/type1/public/amsfonts/latxfont/lasy10.pfb></usr/share/texmf-texlive/f
    815 onts/type1/public/amsfonts/latxfont/lasy9.pfb></usr/share/texmf-texlive/fonts/t
    816 ype1/public/xypic/xyatip10.pfb></usr/share/texmf-texlive/fonts/type1/public/xyp
    817 ic/xybtip10.pfb>
    818 Output written on report.pdf (41 pages, 851126 bytes).
     800f-texlive/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-texlive/f
     801onts/type1/public/amsfonts/cm/cmmi5.pfb></usr/share/texmf-texlive/fonts/type1/p
     802ublic/amsfonts/cm/cmmi6.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfon
     803ts/cm/cmmi8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmmi9.
     804pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/sh
     805are/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-te
     806xlive/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texmf-texlive/fonts/
     807type1/public/amsfonts/cm/cmr5.pfb></usr/share/texmf-texlive/fonts/type1/public/
     808amsfonts/cm/cmr6.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/c
     809mr8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr
     810/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texm
     811f-texlive/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texmf-texlive/f
     812onts/type1/public/amsfonts/cm/cmss12.pfb></usr/share/texmf-texlive/fonts/type1/
     813public/amsfonts/cm/cmss8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfo
     814nts/cm/cmss9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy1
     8150.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy5.pfb></usr/
     816share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy6.pfb></usr/share/texmf-
     817texlive/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texmf-texlive/font
     818s/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/texmf-texlive/fonts/type1/publ
     819ic/amsfonts/cm/cmti10.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts
     820/cm/cmti7.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmti8.pf
     821b></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmti9.pfb></usr/shar
     822e/texmf-texlive/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texmf-tex
     823live/fonts/type1/public/amsfonts/cm/cmtt9.pfb></usr/share/texmf-texlive/fonts/t
     824ype1/public/amsfonts/latxfont/lasy10.pfb></usr/share/texmf-texlive/fonts/type1/
     825public/amsfonts/latxfont/lasy9.pfb></usr/share/texmf-texlive/fonts/type1/public
     826/xypic/xyatip10.pfb></usr/share/texmf-texlive/fonts/type1/public/xypic/xybtip10
     827.pfb>
     828Output written on report.pdf (43 pages, 868174 bytes).
    819829PDF statistics:
    820  937 PDF objects out of 1000 (max. 8388607)
    821  206 named destinations out of 1000 (max. 500000)
    822  558 words of extra memory for PDF output out of 10000 (max. 10000000)
    823 
     830 960 PDF objects out of 1000 (max. 8388607)
     831 211 named destinations out of 1000 (max. 500000)
     832 566 words of extra memory for PDF output out of 10000 (max. 10000000)
     833
  • Deliverables/D2.1/report.out

    r39 r59  
    5454\BOOKMARK [2][]{subsection.6.6}{Testing}{section.6}
    5555\BOOKMARK [1][]{section.7}{Conclusion and future work}{}
    56 \BOOKMARK [1][]{appendix.A}{Proofs}{}
    57 \BOOKMARK [2][]{subsection.A.1}{Notation}{appendix.A}
    58 \BOOKMARK [2][]{subsection.A.2}{Proof of proposition 4}{appendix.A}
    59 \BOOKMARK [2][]{subsection.A.3}{Proof of proposition 8}{appendix.A}
    60 \BOOKMARK [2][]{subsection.A.4}{Proof of proposition 10}{appendix.A}
    61 \BOOKMARK [2][]{subsection.A.5}{Proof of proposition 11}{appendix.A}
    62 \BOOKMARK [2][]{subsection.A.6}{Proof of proposition 13}{appendix.A}
    63 \BOOKMARK [2][]{subsection.A.7}{Proof of proposition 14}{appendix.A}
    64 \BOOKMARK [2][]{subsection.A.8}{Proof of proposition 16}{appendix.A}
    65 \BOOKMARK [2][]{subsection.A.9}{Proof of proposition 17}{appendix.A}
    66 \BOOKMARK [2][]{subsection.A.10}{Proof of proposition 20}{appendix.A}
    67 \BOOKMARK [2][]{subsection.A.11}{Proof of proposition 22}{appendix.A}
    68 \BOOKMARK [2][]{subsection.A.12}{Proof of proposition 23}{appendix.A}
    69 \BOOKMARK [2][]{subsection.A.13}{Proof of proposition 25}{appendix.A}
     56\BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{}
     57\BOOKMARK [1][]{appendix.B}{Proofs}{}
     58\BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
     59\BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B}
     60\BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B}
     61\BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B}
     62\BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B}
     63\BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B}
     64\BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B}
     65\BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B}
     66\BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B}
     67\BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B}
     68\BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B}
     69\BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B}
     70\BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B}
  • Deliverables/D2.1/report.toc

    r39 r59  
    7171\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
    7272\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
    73 \contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}
    74 \contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}
    75 \contentsline {subsection}{\numberline {A.2}Proof of proposition \ref {soundness-small-step}}{38}{subsection.A.2}
    76 \contentsline {subsection}{\numberline {A.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{39}{subsection.A.3}
    77 \contentsline {paragraph}{The memory realisation.}{39}{section*.19}
    78 \contentsline {paragraph}{The inequation.}{39}{section*.20}
    79 \contentsline {subsection}{\numberline {A.4}Proof of proposition \ref {annot-composition}}{39}{subsection.A.4}
    80 \contentsline {subsection}{\numberline {A.5}Proof of proposition \ref {labelled-sim-imp-vm}}{40}{subsection.A.5}
    81 \contentsline {subsection}{\numberline {A.6}Proof of proposition \ref {sim-vm-mips-prop}}{40}{subsection.A.6}
    82 \contentsline {subsection}{\numberline {A.7}Proof of proposition \ref {lab-instr-erasure-imp}}{40}{subsection.A.7}
    83 \contentsline {subsection}{\numberline {A.8}Proof of proposition \ref {global-commutation-prop}}{40}{subsection.A.8}
    84 \contentsline {subsection}{\numberline {A.9}Proof of proposition \ref {instrument-to-label-prop}}{40}{subsection.A.9}
    85 \contentsline {subsection}{\numberline {A.10}Proof of proposition \ref {sound-label-prop}}{41}{subsection.A.10}
    86 \contentsline {subsection}{\numberline {A.11}Proof of proposition \ref {precise-label-prop}}{41}{subsection.A.11}
    87 \contentsline {subsection}{\numberline {A.12}Proof of proposition \ref {lab-sound}}{41}{subsection.A.12}
    88 \contentsline {subsection}{\numberline {A.13}Proof of proposition \ref {ann-correct}}{41}{subsection.A.13}
     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}
  • Deliverables/D2.1/text.tex

    r39 r59  
    30493049\appendix
    30503050
    3051 
     3051%\section{Choice of target architecture and intermediate languages}
     3052
     3053\section{Assessment of the deliverable within the $\cerco$ project}
     3054%RA This section is supposed to be a kind of `executive summary' for
     3055%the project reviewer. How about systematically adding a final appendix
     3056%to the scientific deliverables with a title such as the one proposed above?
     3057
     3058Following the extensive experiments described in the previous sections,
     3059we now feel confident about the possibility of scaling our approach to
     3060a realistic, mildly optimizing, complexity preserving\footnote{In the sense
     3061of the project proposal.}  compiler
     3062% RA:
     3063% Deliverable 2.1 makes no explicit reference to the notion of
     3064% `complexity preservation' though this can be simply derived.
     3065% If a program is soundly labelled and its execution generates a
     3066% sequence of labels lambda then the execution cost of the compiled code
     3067% is proportional to the lenght of the sequence lambda.
     3068for a target architecture of the kind described in the proposal. While we believe
     3069that our approach should scale to a retargetable compiler, in the timeframe
     3070of the European Project and according to the project work-plan we only commit
     3071to the investigation of a compiler having a single target processor.
     3072
     3073In particular, we will target the 8051 (also known as 8052 or MCS51) family
     3074of processors. The 8051 is an 8 bit CISC microprocessor introduced in the 1980
     3075by Intel, very popular and still manufactured by a host of companies,
     3076many European. It is widely used in embedded systems and, thanks to its
     3077predictable behaviour and execution cost, it will allow us to compute fully
     3078accurate measurement of the actual computational complexity of $O(1)$
     3079assembly program slices\footnote{In the sense of the project proposal.},
     3080to be manifested at the C level.
     3081% RA:
     3082% The terminology of `program slice' is used in the proposal but not in the
     3083% deliverable. Note that some confusion is possible with the notion of
     3084% `program slicing' which is a technique we plan to use in Frama-C
     3085
     3086With respect to the test-cases previously described, in particular the
     3087C compiler for MIPS, the main difficulty introduced by the 8051 is the
     3088non uniform concrete memory model: the processor has different types of
     3089memory (on-chip RAM, external RAM, on-chip and/or external ROM) that can
     3090be accessed using different access modes and pointer types.
     3091Moreover, memory mapped I/O is heavily used in the design of the chip,
     3092to the point that all registers (apart from the inaccessible program
     3093counter) are seen as memory locations and have their own memory address.
     3094To complete the picture, the different memories are
     3095split into regions that may overlap, and the same accessing mode can
     3096point to different regions (or even to memory mapped registers) according
     3097to the value of the pointer. Finally, the amount of memory available is
     3098quite limited, with a stack which is at most 80 bytes wide and different
     3099speeds and opcode sizes to access different memory areas. For this
     3100reasons, compilers that target 8051 processors usually abound in directives
     3101to drive the tool in assigning memory locations to values.
     3102
     3103Hence, because of the peculiar choice of target processor, in the next six
     3104months of the $\cerco$ project and partly as an extension of the original work-plan we will:
     3105% RA: Added partly
     3106
     3107\begin{itemize}
     3108
     3109 \item Extend the memory model used so far (and taken from CompCert) to
     3110       accurately describe the different memory types and regions of the 8051,
     3111       as well as to obey to the \texttt{volatile} directive used to map
     3112       memory mapped regions to program variables. This work will be done
     3113       as part of Tasks~T2.3 and T4.1 and the outcome will be described in
     3114       Deliverables~D2.2 and D4.1 where we will also provide a formalization in
     3115       Matita of the executable semantics of the extended memory model.
     3116       In case we decide to adopt the same memory model for all compilation
     3117       phases, as it is done in CompCert, the memory model extension will
     3118       also span over Task~T3.1, requiring close cooperation between
     3119       the front-end formalization (lead by Edinburgh) and the back-end
     3120       formalization (lead by Bologna).
     3121
     3122 \item Devise language extensions (possibly inspired by the variable modifiers
     3123       of the SDCC compiler) to let the user suggest or force the compiler to
     3124       put data into particular memory regions. Similarly, we could refine the
     3125       pointer types of ANSI C into classes of pointer types pointing to
     3126       particular regions, in order to reflect the difference in sizes of
     3127       pointers to different regions (8 bits to address internal RAM and
     3128       memory mapped registers; 8 bits to address bits in the bit memory
     3129       or in registers using an ad-hoc addressing mode;
     3130       16 bits for code memory and external memory; 24 bits for generic
     3131       pointers). All of these language extensions, if any, must be reflected
     3132       all over the compilation chain, with modifications to the intermediate
     3133       languages and/or memory model. This work will be done as part of
     3134       Tasks~T2.3, T3.1 and T4.1 and the outcome will be described in
     3135       Deliverables~D2.2, D3.1, D3.3, D4.1, D4.3 where we will provide
     3136       executable semantics in Matita of the source, target and intermediate
     3137       languages.
     3138
     3139       In order to remain compatible with the project schedule, we will first
     3140       focus on compiling standard Clight without floating points to the 8051,
     3141       adding the language extensions in a second moment, within Task~T2.3.
     3142
     3143%RA: If we want to follow the CompCert approach (one memory model for the
     3144% whole verification chain) then these two points should be done in cooperation
     3145% by Edinburgh (front-end formalisation) and  Bologna (back-end formalisation).
     3146
     3147
     3148 \item Modify and extend the experimental compiler from Clight
     3149(without floating point) to MIPS in order to target the 8051
     3150architecture (Task~T2.3, Deliverable~D2.2).
     3151%RA: In the 2 SVN (the one we used to prepare the proposal and the
     3152%one we are using now) I cannot find the latest version of the proposal
     3153%with the correct numbering of the deliverables. Would it be possible
     3154%to add it to the Contracts directory of the SVN?
     3155
     3156%RA: We (Paris) are supposed to deliver the prototype annotating compiler end of January
     3157% which means that the bulk of the work must be done before Christmas (also remember
     3158% that Nicolas will leave us end of February).
     3159% However, we started talking about the specification of the memory model
     3160% and the extension of the source Clight language only a few days ago.
     3161% This means that unless we get a solid specification in a couple of weeks,
     3162% the deliverable 2.2 will NOT necessarily cover all the `language extensions' which
     3163% are mentioned above but will focus on compiling Clight with floating point to 8051.
     3164
     3165
     3166\end{itemize}
     3167
     3168But for the modifications required by the selection of the target processor (8051),
     3169we plan to rely as much as possible on the architecture and the
     3170the intermediate languages described in this deliverable D2.1.
     3171
     3172
     3173\newpage
    30523174\section{Proofs}\label{paper-proofs}
    30533175
Note: See TracChangeset for help on using the changeset viewer.