# Changeset 59 for Deliverables/D2.1/text.tex

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

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

File:
1 edited

### Legend:

Unmodified
 r39 \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 work-plan 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 Frama-C With respect to the test-cases 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 (on-chip RAM, external RAM, on-chip 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 work-plan 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 front-end formalization (lead by Edinburgh) and the back-end 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 ad-hoc 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 (front-end formalisation) and  Bologna (back-end 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{paper-proofs}