Changeset 1413 for Deliverables/D4.2-4.3

Oct 19, 2011, 2:54:35 PM (8 years ago)

a lot more added, including updated parameters based on csc's recent submit

1 edited


  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1409 r1413  
    306306  framesT: Type[0];
     307  empty_framesT: framesT;
    307308  regsT: Type[0];
     309  empty_regsT: regsT;
     310  call_args_for_main: call_args p;
     311  call_dest_for_main: call_dest p;
    308312  succ_pc: succ p → address → res address;
    309313  greg_store_: generic_reg p → beval → regsT → res regsT;
    311315  acca_store_: acc_a_reg p → beval → regsT → res regsT;
    312316  acca_retrieve_: regsT → acc_a_reg p → res beval;
    313   accb_store_: acc_b_reg p → beval → regsT → res regsT;
    314   accb_retrieve_: regsT → acc_b_reg p → res beval;
     317  ...
    315318  dpl_store_: dpl_reg p → beval → regsT → res regsT;
    316319  dpl_retrieve_: regsT → dpl_reg p → res beval;
    317   dph_store_: dph_reg p → beval → regsT → res regsT;
    318   dph_retrieve_: regsT → dph_reg p → res beval;
     320  ...
    319321  pair_reg_move_: regsT → pair_reg p → res regsT;
    320322  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
    323325For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
    324326Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
    325 Here \texttt{framesT} is the type of stack frames.
     327Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame.
     329The two hypothesised values \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} deal with problems with the \texttt{main} function of the program, and how it is handled.
     330In particular, we need to know when the \texttt{main} function has finished executing.
     331But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++).
     332Therefore, to understand whether the exiting \texttt{main} function is really exiting, or just recursively calling itself, we need to remember the address at which \texttt{main} is located.
     333This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments.
    327335We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
    478486The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.
     488\subsection{Memory models}
     491Currently, the semantics of the front and backend intermediate languages are built around two distinct memory models.
     492The frontend languages reuse the CompCert memory model, whereas the backend languages employ a bespoke model tailored to their needs.
     493This split between the memory models is reflective of the fact that the front and backend language have different requirements from their memory models, to a certain extent.
     495In particular, the CompCert memory model places quite heavy restrictions on where in memory one can read from.
     496To read a value in this memory model, you must supply an address, complete with a number of `chunks' to read following that address.
     497The read is only successful if you attempt to read at a genuine `value boundary', and read the appropriate number of memory chunks for that value.
     498As a result, with the CompCert memory model you are unable to read the third byte of a 32-bit integer value directly from memory, for instance.
     499This has some consequences for the CompCert compiler, namely an inability to write a \texttt{memcpy} routine.
     501However, the CerCo memory model operates differently, as we need to move data `piecemeal' between stacks in the backend of the compiler.
     502As a result, the bespoke memory model allows one to read data at any memory location, not just on value boundaries.
     503This has the advantage that we can successfully write a \texttt{memcpy} routine with the CerCo compiler (remembering that \texttt{memcpy} is nothing more than `read a byte, copy a byte' repeated in a loop), an advantage over CompCert.
     505Right now, the two memory models are interfaced during the translation from RTLabs to RTL.
     506It is an open question whether we will unify the two memory models, using only the backend, bespoke memory model throughout the compiler, as the CompCert memory model seems to work fine for the frotend, where such byte-by-byte copying is not needed.
     507However, should we decide to port the frontend to the new memory model, it has been written in such an abstract way that doing so would be relatively straightforward.
    481510% SECTION.                                                                    %
    487516These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
    488517Closing these axioms should not be a problem.
    489 No further work remains, aside from `tidying up' the code.
     519Further, tailcalls to external functions are currently axiomatised.
     520This is due to there being a difficulty with how stackframes are handled with external function calls.
     521We leave this for further work, due to there being no pressing need to implement this feature at the present time.
     523There is also, as mentioned, an open problem as to whether the frontend languages should use the same memory model as the backend languages, as opposed to reusing the CompCert memory model.
     524Should this decision be taken, this will likely be straightforward but potentially time consuming.
Note: See TracChangeset for help on using the changeset viewer.