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

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

1 edited


  • Deliverables/D2.1/text.tex

    r39 r59  
     3051%\section{Choice of target architecture and intermediate languages}
     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?
     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.
     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
     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.
     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
     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).
     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.
     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.
     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).
     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?
     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.
     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.
Note: See TracChangeset for help on using the changeset viewer.