Changeset 2060

Ignore:
Timestamp:
Jun 13, 2012, 4:26:50 PM (7 years ago)
Message:

More work on paper.

File:
1 edited

Legend:

Unmodified
 r2058 Each of these three instructions expects arguments in different sizes and behaves in markedly different ways: \texttt{SJMP} may only perform a local jump'; \texttt{LJMP} may jump to any address in the MCS-51's memory space and \texttt{AJMP} may jump to any address in the current memory page. Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS-51's limited code memory, the smallest possible opcode that will suffice should be selected. This is a well known problem to assembler writers, often referred to as branch displacement'. This is a well known problem to assembler writers who target RISC architectures, often referred to as branch displacement'. Branch displacement is not a simple problem to solve and requires the implementation of an optimising assembler. This pseudo internal RAM corresponds to an internal RAM where the stack holds the real addresses after optimisation, and all the other values remain untouched. We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM. The current code is parametric on the implementation of the map itself. \begin{lstlisting} axiom internal_pseudo_address_map: Type[0]. \end{lstlisting} We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM: \begin{lstlisting} definition internal_pseudo_address_map := list ((BitVector 8) $\times$ (bool $\times$ Word)) $\times$ (option (bool $\times$ Word)). \end{lstlisting} The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set. Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes. All \texttt{MOV} instructions in the MCS-51 must use the accumulator \texttt{A} as an intermediary, moving a byte at a time. The second component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the boolean flag) complete with the corresponding, source address in full. The first component, on the other hand, performs a similar task for the rest of external RAM. Again, we use a boolean flag to describe whether a byte is the upper or lower component of a 16-bit address. The \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} function converts the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}. In particular, our assembly language featured labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register. Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is correct', in that the semantics of a subset of assembly programs are not changed is complex. Further, we have observed the shocking' fact that any optimising assembler cannot preserve the semantics of all assembly programs. The formalisation is a key component of the CerCo project, which aims to produce a verified concrete complexity preserving compiler for a large subset of the C programming language. The verified assembler, complete with the underlying formalisation of the semantics of MCS-51 machine code (described fully in~\cite{mulligan:executable:2011}), will form the bedrock layer upon which the rest of the CerCo project will build its verified compiler platform. However, further work is needed. In particular, as it stands, the code produced by the prototype CerCo C compiler does not fall into the semantics preserving' subset of assembly programs for our assembler. This is because the MCS-51 features a small stack space, and a larger stack is customarily manually emulated in external RAM. As a result, the majority of programs feature slices of memory addresses and program counters being moved in-and-out of external RAM via the registers, simulating the stack mechanism. At the moment, this movement is not tracked by \texttt{internal\_pseudo\_address\_map}, which only tracks the movement of memory addresses in low internal RAM. We leave extending this tracking of memory addresses throughout the whole of the MCS-51's address spaces as future work. It is interesting to compare our work to an industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}. However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory. In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program. The definition and proof of a complete, optimal (in the sense that object code size is minimised) and correct jump expansion policy is ongoing work. The definition and proof of a terminating, correct jump expansion policy is described in a companion publication to this one. Aside 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. Note that both CompCert and the seL4 formalisation assume the existence of trustworthy' assemblers. Our observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects. The observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects. If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that have a hope of having their semantics preserved by an optimising assembler. Our formalisation exploits dependent types in different ways and for multiple purposes. The first purpose is to reduce potential errors in the formalisation of the microprocessor. In particular, dependent types are used to constraint the size of bit-vectors and tries that represent memory quantities and memory areas respectively. They are also used as explained in~\cite{mulligan:executable:2011}. to simulate polymorphic variants in Matita. Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS-51 where every opcode must accept its own subset of the 11 addressing mode of the processor. The second purpose is to single out the sources of incompleteness. By abstracting our functions over the dependent type of correct policies, we were able to manifest the fact that the compiler never refuses to compile a program where a correct policy exists. This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some other one does so. Finally, dependent types, together with Matita's liberal system of coercions, allow to simulate almost entirely in user space the proof methodology Russell'' of Sozeau~\cite{sozeau:subset:2006}. However, not every proof has been done this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way. For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions. Our formalisation exploits dependent types in different ways and for multiple purposes. The first purpose is to reduce potential errors in the formalisation of the microprocessor. In particular, dependent types are used to constraint the size of bitvectors and tries that represent memory quantities and memory areas respectively. They are also used to simulate polymorphic variants in Matita, in order to provide precise typings to various functions expecting only a subset of all possible addressing modes than the MCS-51 offers. Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS-51 where every opcode must accept its own subset of the 11 addressing mode of the processor. The second purpose is to single out the sources of incompleteness. By abstracting our functions over the dependent type of correct policies, we were able to manifest the fact that the compiler never refuses to compile a program where a correct policy exists. This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some other one does so. Finally, dependent types, together with Matita's liberal system of coercions, allow to simulate almost entirely in user space the proof methodology Russell'' of Sozeau~\cite{sozeau:subset:2006}. However, not every proof has been done this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way. For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions. \subsection{Related work} We believe some other verified assemblers exist in the literature. However, what sets our work apart from that above is our attempt to optimise the machine code generated by our assembler. This complicates any formalisation effort, as the best possible selection of machine instructions must be made, especially important on a device such as the MCS-51 with a miniscule code memory. This complicates any formalisation effort, as an attempt at the best possible selection of machine instructions must be made, especially important on a device such as the MCS-51 with a miniscule code memory. Further, care must be taken to ensure that the time properties of an assembly program are not modified by the assembly process lest we affect the semantics of any program employing the MCS-51's I/O facilities. This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. This will be a \emph{leit motif} of CerCo. Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project related to CerCo. As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on. However, CerCo also extends CompCert in other ways. Namely, the CompCert verified compilation chain terminates at the assembly level, and takes for granted the existence of a trustworthy assembler. CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level. The work presented in this publication is one part of CerCo's extension over CompCert. \subsection{Resources} \label{subsect.resources} All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. The code of the compiler has been completed, and the proof of correctness described here is still in progress. In particular, we have assumed several properties of library functions'' related in particular to modular arithmetics and datastructures manipulation. Moreover, we only completed the interesting cases of some of the main theorems that proceed by cases on all the possible opcodes. We thus believe that the proof strategy is sound and that we will be able to close soon all axioms, up to possible minor bugs that should have local fixes that do not affect the global proof strategy. The development, including the definition of the executable semantics of the MCS-51, is spread across 17 files, totalling around 11,500 lines of Matita source. The bulk of the proof described herein is contained in a single file, \texttt{AssemblyProof.ma}, consisting at the moment of approximately 2500 lines of Matita source. Another 1000 lines of proofs are spread all over the development because of dependent types and the Russell proof style, that do not allow to separate the code from the proofs. The low ratio between the number of lines of code and the number of lines of proof is unusual. It is justified by the fact that the pseudo-assembly and the assembly language share most constructs and that large parts of the semantics is also shared. Thus many lines of code are required to describe the complex semantics of the processor, but, for the shared cases, the proof of preservation of the semantics is essentially trivial. All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. The code of the compiler has been completed, and the proof of correctness described here is still in progress. In particular, we have assumed several properties of library functions'' related in particular to modular arithmetic and datastructure manipulation. Moreover, we have axiomatised various ancillary functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, preferring instead to focus on the main meat of the theorems. We thus believe that the proof strategy is sound and that we will be able to close soon all axioms, up to possible minor bugs that should have local fixes that do not affect the global proof strategy. The development, including the definition of the executable semantics of the MCS-51, is spread across 29 files, totalling around 18,500 lines of Matita source. The bulk of the proof described herein is contained in a series of files, \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma} consisting at the moment of approximately 4200 lines of Matita source. Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs. The low ratio between the number of lines of code and the number of lines of proof is unusual. It is justified by the fact that the pseudo-assembly and the assembly language share most constructs and that large parts of the semantics are also shared. Thus many lines of code are required to describe the complex semantics of the processor, but, for the shared cases, the proof of preservation of the semantics is essentially trivial. \bibliography{cpp-2012-asm.bib}