Feb 27, 2012, 4:08:40 PM (10 years ago)


1 edited


  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1773 r1774  
    10641064sketched in the previous section.
     1066\subsection{Contingency plan}
     1067On the basis of the proof strategy sketched in this document and the
     1068estimated effort, we can refine our contingency plan. In case we will end
     1069the certification of the basic compiler in advance we will have the choice
     1070of either proving loop optimizations and/or partial redundancy elimination
     1071correct (both tasks that seem difficult to achieve in a short time) or
     1072considering the MCS-51 specific extensions introduced during the first period
     1073and under-used in the formalized prototype. Yet another possibility would be
     1074to better study retargeting of the code and the commutation property between
     1075different compiler passes. The latter study is easily enabled by our
     1076approach where all back-end languages are instances of the same parameterized
     1079In the case of a consistent delay in the certification of some
     1080components, we will address first the passes that are more likely to have
     1081undetected bugs and we will follow a top-down approach, axiomatizing
     1082the properties of the data structured used in the compiler to focus more
     1083on the algorithms. The rational is that data structures are easier then
     1084algorithms to test using well known methodologies.
     1085The effort table clearly shows that commond definitions
     1086and data structures are 1/4th of the size of the code and require slightly
     1087less than 1/3rd of the total effort. At least half of this effort really goes
     1088into simple data structures (vectors, bounded and unbounded integers, tries
     1089and maps) whose certification is not very interesting and could be sacrificed.
    10671092The overall exercise, whose details have been only minimally reported here,
Note: See TracChangeset for help on using the changeset viewer.