Changeset 1007 for src/ASM

Jun 20, 2011, 5:57:32 PM (9 years ago)

added explanation of sdcc

1 edited


  • src/ASM/CPP2011/cpp-2011.tex

    r1005 r1007  
    186186Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory even after shrinking jumps according to the
    187 best policy. The first case is an example of compiler error because of
    188 ill-formedness of the input. It does not count for the compiler completeness.
    189 We plan to employ dependent types in CerCo to restrict the domain of the
    190 compiler to those programs that are semantically correct and should be compiled.
    191 In particular, in CerCo we are also interested in completeness of compilation
    192 whereas previous formalizations only focused on correctness.
     187best policy.
     188The first circumstance is an example of a serious compiler error, as an ill-formed assembly program was generated.
     189It does not count against the completeness of the assembler.
     190We plan to employ dependent types in CerCo in order to restrict the domain of the compiler to those programs that are `semantically correct' and should be compiled.
     191In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness.
    194193The rest of this paper is a detailed description of this proof.
    504503We leave extending this tracking of memory addresses throughout the whole of the MCS-51's address spaces as future work.
     505It is interesting to compare our work to an `industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}.
     506SDCC is the only open source C compiler available that targets the MCS-51 instruction set.
     507It appears that all pseudojumps in SDCC assembly are expanded to \texttt{LJMP} instructions, the worst possible jump expansion policy from an efficiency point of view.
     508Note that this policy is the only possible policy that can preserve the semantics of an assembly program during the assembly process.
     509However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory.
     510In this respect, there is a fundamental trade-off between the completeness of the assembler and the efficiency of the assembled program.
     511The definition and proof of an complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work.
    506513Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
    507514Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
    542549In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
    544 \subsection{Source code}
    545 \label{subsect.source.code}
    547554All files relating to our formalisation effort can be found online at~\url{}.
Note: See TracChangeset for help on using the changeset viewer.