Index: /Deliverables/D2.1/report.aux
===================================================================
 /Deliverables/D2.1/report.aux (revision 58)
+++ /Deliverables/D2.1/report.aux (revision 59)
@@ 202,22 +202,23 @@
\bibcite{Pottier}{12}
\bibcite{W09}{13}
\@writefile{toc}{\contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}}
\newlabel{paperproofs}{{A}{38}{Proofs\relax }{appendix.A}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.2}Proof of proposition \ref {soundnesssmallstep}}{38}{subsection.A.2}}
\newlabel{accesslemma}{{26}{38}{Proof of proposition \ref {soundnesssmallstep}\relax }{theorem.26}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.3}Proof of proposition \ref {labelledsimulationvmmips}}{39}{subsection.A.3}}
\newlabel{step1}{{7}{39}{Proof of proposition \ref {labelledsimulationvmmips}\relax }{equation.A.7}{}}
\@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{39}{section*.19}}
\@writefile{toc}{\contentsline {paragraph}{The inequation.}{39}{section*.20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.4}Proof of proposition \ref {annotcomposition}}{39}{subsection.A.4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.5}Proof of proposition \ref {labelledsimimpvm}}{40}{subsection.A.5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.6}Proof of proposition \ref {simvmmipsprop}}{40}{subsection.A.6}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.7}Proof of proposition \ref {labinstrerasureimp}}{40}{subsection.A.7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.8}Proof of proposition \ref {globalcommutationprop}}{40}{subsection.A.8}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.9}Proof of proposition \ref {instrumenttolabelprop}}{40}{subsection.A.9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.10}Proof of proposition \ref {soundlabelprop}}{41}{subsection.A.10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.11}Proof of proposition \ref {preciselabelprop}}{41}{subsection.A.11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.12}Proof of proposition \ref {labsound}}{41}{subsection.A.12}}
\newlabel{preciselemma}{{29}{41}{Proof of proposition \ref {labsound}\relax }{theorem.29}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {A.13}Proof of proposition \ref {anncorrect}}{41}{subsection.A.13}}
+\@writefile{toc}{\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}}
+\@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}}
+\newlabel{paperproofs}{{B}{40}{Proofs\relax }{appendix.B}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundnesssmallstep}}{40}{subsection.B.2}}
+\newlabel{accesslemma}{{26}{40}{Proof of proposition \ref {soundnesssmallstep}\relax }{theorem.26}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelledsimulationvmmips}}{41}{subsection.B.3}}
+\newlabel{step1}{{7}{41}{Proof of proposition \ref {labelledsimulationvmmips}\relax }{equation.B.7}{}}
+\@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{41}{section*.19}}
+\@writefile{toc}{\contentsline {paragraph}{The inequation.}{41}{section*.20}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annotcomposition}}{41}{subsection.B.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelledsimimpvm}}{42}{subsection.B.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {simvmmipsprop}}{42}{subsection.B.6}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {labinstrerasureimp}}{42}{subsection.B.7}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {globalcommutationprop}}{42}{subsection.B.8}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrumenttolabelprop}}{42}{subsection.B.9}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {soundlabelprop}}{43}{subsection.B.10}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {preciselabelprop}}{43}{subsection.B.11}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {labsound}}{43}{subsection.B.12}}
+\newlabel{preciselemma}{{29}{43}{Proof of proposition \ref {labsound}\relax }{theorem.29}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref {anncorrect}}{43}{subsection.B.13}}
Index: /Deliverables/D2.1/report.log
===================================================================
 /Deliverables/D2.1/report.log (revision 58)
+++ /Deliverables/D2.1/report.log (revision 59)
@@ 1,3 +1,3 @@
This is pdfTeX, Version 3.14159261.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.8.30) 6 SEP 2010 10:17
+This is pdfTeX, Version 3.14159261.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.8.31) 10 SEP 2010 16:02
entering extended mode
restricted \write18 enabled.
@@ 7,5 +7,5 @@
LaTeX2e <2009/09/24>
Babel and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, loaded.
+yphenation, french, basque, italian, loaded.
(/usr/share/texmftexlive/tex/latex/base/article.cls
Document Class: article 2007/10/19 v1.4h Standard LaTeX document class
@@ 45,5 +45,5 @@
(/usr/share/texmftexlive/tex/latex/pdftexdef/pdftex.def
File: pdftex.def 2009/08/25 v0.04m Graphics/color for pdfTeX
+File: pdftex.def 2010/03/12 v0.04p Graphics/color for pdfTeX
\Gread@gobject=\count87
))
@@ 417,5 +417,5 @@
LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 538.
LaTeX Font Info: ... okay on input line 538.
 (/usr/share/texmf/tex/context/base/supppdf.mkii
+ (/usr/share/texmftexlive/tex/context/base/supppdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count119
@@ 447,5 +447,5 @@
\AtBeginShipoutBox=\box33
 <../style/cerco_logo.png, id=279, 804.00375pt x 213.79875pt>
+ <../style/cerco_logo.png, id=283, 804.00375pt x 213.79875pt>
File: ../style/cerco_logo.png Graphic file (type png)
@@ 768,5 +768,14 @@
[]
[37] [38] [39] [40]) [41] (./report.aux)
+[37]
+
+Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
+(hyperref) removing `math shift' on input line 3053.
+
+
+Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
+(hyperref) removing `math shift' on input line 3053.
+
+[38] [39] [40] [41] [42]) [43] (./report.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
@@ 774,8 +783,8 @@
)
Here is how much of TeX's memory you used:
 8510 strings out of 495061
 110648 string characters out of 1182621
 247458 words of memory out of 3000000
 11286 multiletter control sequences out of 15000+50000
+ 8519 strings out of 495021
+ 110783 string characters out of 1180926
+ 247727 words of memory out of 3000000
+ 11300 multiletter control sequences out of 15000+50000
28130 words of font info for 114 fonts, out of 3000000 for 9000
28 hyphenation exceptions out of 8191
@@ 789,35 +798,36 @@
b>
Output written on report.pdf (41 pages, 851126 bytes).
+ftexlive/fonts/type1/public/amsfonts/cm/cmmi12.pfb>
+Output written on report.pdf (43 pages, 868174 bytes).
PDF statistics:
 937 PDF objects out of 1000 (max. 8388607)
 206 named destinations out of 1000 (max. 500000)
 558 words of extra memory for PDF output out of 10000 (max. 10000000)

+ 960 PDF objects out of 1000 (max. 8388607)
+ 211 named destinations out of 1000 (max. 500000)
+ 566 words of extra memory for PDF output out of 10000 (max. 10000000)
+
Index: /Deliverables/D2.1/report.out
===================================================================
 /Deliverables/D2.1/report.out (revision 58)
+++ /Deliverables/D2.1/report.out (revision 59)
@@ 54,16 +54,17 @@
\BOOKMARK [2][]{subsection.6.6}{Testing}{section.6}
\BOOKMARK [1][]{section.7}{Conclusion and future work}{}
\BOOKMARK [1][]{appendix.A}{Proofs}{}
\BOOKMARK [2][]{subsection.A.1}{Notation}{appendix.A}
\BOOKMARK [2][]{subsection.A.2}{Proof of proposition 4}{appendix.A}
\BOOKMARK [2][]{subsection.A.3}{Proof of proposition 8}{appendix.A}
\BOOKMARK [2][]{subsection.A.4}{Proof of proposition 10}{appendix.A}
\BOOKMARK [2][]{subsection.A.5}{Proof of proposition 11}{appendix.A}
\BOOKMARK [2][]{subsection.A.6}{Proof of proposition 13}{appendix.A}
\BOOKMARK [2][]{subsection.A.7}{Proof of proposition 14}{appendix.A}
\BOOKMARK [2][]{subsection.A.8}{Proof of proposition 16}{appendix.A}
\BOOKMARK [2][]{subsection.A.9}{Proof of proposition 17}{appendix.A}
\BOOKMARK [2][]{subsection.A.10}{Proof of proposition 20}{appendix.A}
\BOOKMARK [2][]{subsection.A.11}{Proof of proposition 22}{appendix.A}
\BOOKMARK [2][]{subsection.A.12}{Proof of proposition 23}{appendix.A}
\BOOKMARK [2][]{subsection.A.13}{Proof of proposition 25}{appendix.A}
+\BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{}
+\BOOKMARK [1][]{appendix.B}{Proofs}{}
+\BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
+\BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B}
+\BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B}
+\BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B}
+\BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B}
+\BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B}
+\BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B}
+\BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B}
+\BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B}
+\BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B}
+\BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B}
+\BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B}
+\BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B}
Index: /Deliverables/D2.1/report.toc
===================================================================
 /Deliverables/D2.1/report.toc (revision 58)
+++ /Deliverables/D2.1/report.toc (revision 59)
@@ 71,18 +71,19 @@
\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
\contentsline {section}{\numberline {A}Proofs}{38}{appendix.A}
\contentsline {subsection}{\numberline {A.1}Notation}{38}{subsection.A.1}
\contentsline {subsection}{\numberline {A.2}Proof of proposition \ref {soundnesssmallstep}}{38}{subsection.A.2}
\contentsline {subsection}{\numberline {A.3}Proof of proposition \ref {labelledsimulationvmmips}}{39}{subsection.A.3}
\contentsline {paragraph}{The memory realisation.}{39}{section*.19}
\contentsline {paragraph}{The inequation.}{39}{section*.20}
\contentsline {subsection}{\numberline {A.4}Proof of proposition \ref {annotcomposition}}{39}{subsection.A.4}
\contentsline {subsection}{\numberline {A.5}Proof of proposition \ref {labelledsimimpvm}}{40}{subsection.A.5}
\contentsline {subsection}{\numberline {A.6}Proof of proposition \ref {simvmmipsprop}}{40}{subsection.A.6}
\contentsline {subsection}{\numberline {A.7}Proof of proposition \ref {labinstrerasureimp}}{40}{subsection.A.7}
\contentsline {subsection}{\numberline {A.8}Proof of proposition \ref {globalcommutationprop}}{40}{subsection.A.8}
\contentsline {subsection}{\numberline {A.9}Proof of proposition \ref {instrumenttolabelprop}}{40}{subsection.A.9}
\contentsline {subsection}{\numberline {A.10}Proof of proposition \ref {soundlabelprop}}{41}{subsection.A.10}
\contentsline {subsection}{\numberline {A.11}Proof of proposition \ref {preciselabelprop}}{41}{subsection.A.11}
\contentsline {subsection}{\numberline {A.12}Proof of proposition \ref {labsound}}{41}{subsection.A.12}
\contentsline {subsection}{\numberline {A.13}Proof of proposition \ref {anncorrect}}{41}{subsection.A.13}
+\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}
+\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}
+\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}
+\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundnesssmallstep}}{40}{subsection.B.2}
+\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelledsimulationvmmips}}{41}{subsection.B.3}
+\contentsline {paragraph}{The memory realisation.}{41}{section*.19}
+\contentsline {paragraph}{The inequation.}{41}{section*.20}
+\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annotcomposition}}{41}{subsection.B.4}
+\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelledsimimpvm}}{42}{subsection.B.5}
+\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {simvmmipsprop}}{42}{subsection.B.6}
+\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {labinstrerasureimp}}{42}{subsection.B.7}
+\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {globalcommutationprop}}{42}{subsection.B.8}
+\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrumenttolabelprop}}{42}{subsection.B.9}
+\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {soundlabelprop}}{43}{subsection.B.10}
+\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {preciselabelprop}}{43}{subsection.B.11}
+\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {labsound}}{43}{subsection.B.12}
+\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref {anncorrect}}{43}{subsection.B.13}
Index: /Deliverables/D2.1/text.tex
===================================================================
 /Deliverables/D2.1/text.tex (revision 58)
+++ /Deliverables/D2.1/text.tex (revision 59)
@@ 3049,5 +3049,127 @@
\appendix

+%\section{Choice of target architecture and intermediate languages}
+
+\section{Assessment of the deliverable within the $\cerco$ project}
+%RA This section is supposed to be a kind of `executive summary' for
+%the project reviewer. How about systematically adding a final appendix
+%to the scientific deliverables with a title such as the one proposed above?
+
+Following the extensive experiments described in the previous sections,
+we now feel confident about the possibility of scaling our approach to
+a realistic, mildly optimizing, complexity preserving\footnote{In the sense
+of the project proposal.} compiler
+% RA:
+% Deliverable 2.1 makes no explicit reference to the notion of
+% `complexity preservation' though this can be simply derived.
+% If a program is soundly labelled and its execution generates a
+% sequence of labels lambda then the execution cost of the compiled code
+% is proportional to the lenght of the sequence lambda.
+for a target architecture of the kind described in the proposal. While we believe
+that our approach should scale to a retargetable compiler, in the timeframe
+of the European Project and according to the project workplan we only commit
+to the investigation of a compiler having a single target processor.
+
+In particular, we will target the 8051 (also known as 8052 or MCS51) family
+of processors. The 8051 is an 8 bit CISC microprocessor introduced in the 1980
+by Intel, very popular and still manufactured by a host of companies,
+many European. It is widely used in embedded systems and, thanks to its
+predictable behaviour and execution cost, it will allow us to compute fully
+accurate measurement of the actual computational complexity of $O(1)$
+assembly program slices\footnote{In the sense of the project proposal.},
+to be manifested at the C level.
+% RA:
+% The terminology of `program slice' is used in the proposal but not in the
+% deliverable. Note that some confusion is possible with the notion of
+% `program slicing' which is a technique we plan to use in FramaC
+
+With respect to the testcases previously described, in particular the
+C compiler for MIPS, the main difficulty introduced by the 8051 is the
+non uniform concrete memory model: the processor has different types of
+memory (onchip RAM, external RAM, onchip and/or external ROM) that can
+be accessed using different access modes and pointer types.
+Moreover, memory mapped I/O is heavily used in the design of the chip,
+to the point that all registers (apart from the inaccessible program
+counter) are seen as memory locations and have their own memory address.
+To complete the picture, the different memories are
+split into regions that may overlap, and the same accessing mode can
+point to different regions (or even to memory mapped registers) according
+to the value of the pointer. Finally, the amount of memory available is
+quite limited, with a stack which is at most 80 bytes wide and different
+speeds and opcode sizes to access different memory areas. For this
+reasons, compilers that target 8051 processors usually abound in directives
+to drive the tool in assigning memory locations to values.
+
+Hence, because of the peculiar choice of target processor, in the next six
+months of the $\cerco$ project and partly as an extension of the original workplan we will:
+% RA: Added partly
+
+\begin{itemize}
+
+ \item Extend the memory model used so far (and taken from CompCert) to
+ accurately describe the different memory types and regions of the 8051,
+ as well as to obey to the \texttt{volatile} directive used to map
+ memory mapped regions to program variables. This work will be done
+ as part of Tasks~T2.3 and T4.1 and the outcome will be described in
+ Deliverables~D2.2 and D4.1 where we will also provide a formalization in
+ Matita of the executable semantics of the extended memory model.
+ In case we decide to adopt the same memory model for all compilation
+ phases, as it is done in CompCert, the memory model extension will
+ also span over Task~T3.1, requiring close cooperation between
+ the frontend formalization (lead by Edinburgh) and the backend
+ formalization (lead by Bologna).
+
+ \item Devise language extensions (possibly inspired by the variable modifiers
+ of the SDCC compiler) to let the user suggest or force the compiler to
+ put data into particular memory regions. Similarly, we could refine the
+ pointer types of ANSI C into classes of pointer types pointing to
+ particular regions, in order to reflect the difference in sizes of
+ pointers to different regions (8 bits to address internal RAM and
+ memory mapped registers; 8 bits to address bits in the bit memory
+ or in registers using an adhoc addressing mode;
+ 16 bits for code memory and external memory; 24 bits for generic
+ pointers). All of these language extensions, if any, must be reflected
+ all over the compilation chain, with modifications to the intermediate
+ languages and/or memory model. This work will be done as part of
+ Tasks~T2.3, T3.1 and T4.1 and the outcome will be described in
+ Deliverables~D2.2, D3.1, D3.3, D4.1, D4.3 where we will provide
+ executable semantics in Matita of the source, target and intermediate
+ languages.
+
+ In order to remain compatible with the project schedule, we will first
+ focus on compiling standard Clight without floating points to the 8051,
+ adding the language extensions in a second moment, within Task~T2.3.
+
+%RA: If we want to follow the CompCert approach (one memory model for the
+% whole verification chain) then these two points should be done in cooperation
+% by Edinburgh (frontend formalisation) and Bologna (backend formalisation).
+
+
+ \item Modify and extend the experimental compiler from Clight
+(without floating point) to MIPS in order to target the 8051
+architecture (Task~T2.3, Deliverable~D2.2).
+%RA: In the 2 SVN (the one we used to prepare the proposal and the
+%one we are using now) I cannot find the latest version of the proposal
+%with the correct numbering of the deliverables. Would it be possible
+%to add it to the Contracts directory of the SVN?
+
+%RA: We (Paris) are supposed to deliver the prototype annotating compiler end of January
+% which means that the bulk of the work must be done before Christmas (also remember
+% that Nicolas will leave us end of February).
+% However, we started talking about the specification of the memory model
+% and the extension of the source Clight language only a few days ago.
+% This means that unless we get a solid specification in a couple of weeks,
+% the deliverable 2.2 will NOT necessarily cover all the `language extensions' which
+% are mentioned above but will focus on compiling Clight with floating point to 8051.
+
+
+\end{itemize}
+
+But for the modifications required by the selection of the target processor (8051),
+we plan to rely as much as possible on the architecture and the
+the intermediate languages described in this deliverable D2.1.
+
+
+\newpage
\section{Proofs}\label{paperproofs}