Changeset 1413 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

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

Author:

mulligan

Message:

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

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (5 diffs)

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

@@ -305 +305 @@
 {
   framesT: Type[0];
+  empty_framesT: framesT;
   regsT: Type[0];
+  empty_regsT: regsT;
+  call_args_for_main: call_args p;
+  call_dest_for_main: call_dest p;
   succ_pc: succ p → address → res address;
   greg_store_: generic_reg p → beval → regsT → res regsT;
@@ -311 +315 @@
   acca_store_: acc_a_reg p → beval → regsT → res regsT;
   acca_retrieve_: regsT → acc_a_reg p → res beval;
-  accb_store_: acc_b_reg p → beval → regsT → res regsT;
-  accb_retrieve_: regsT → acc_b_reg p → res beval;
+  ...
   dpl_store_: dpl_reg p → beval → regsT → res regsT;
   dpl_retrieve_: regsT → dpl_reg p → res beval;
-  dph_store_: dph_reg p → beval → regsT → res regsT;
-  dph_retrieve_: regsT → dph_reg p → res beval;
+  ...
   pair_reg_move_: regsT → pair_reg p → res regsT;
   pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
@@ -323 +325 @@
 For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
 Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
-Here \texttt{framesT} is the type of stack frames.
+Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame.
+
+The 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.
+In particular, we need to know when the \texttt{main} function has finished executing.
+But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++).
+Therefore, 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.
+This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments.
 
 We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
@@ -478 +486 @@
 The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad.
 
+\subsection{Memory models}
+\label{subsect.memory.models}
+
+Currently, the semantics of the front and backend intermediate languages are built around two distinct memory models.
+The frontend languages reuse the CompCert memory model, whereas the backend languages employ a bespoke model tailored to their needs.
+This 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.
+
+In particular, the CompCert memory model places quite heavy restrictions on where in memory one can read from.
+To read a value in this memory model, you must supply an address, complete with a number of `chunks' to read following that address.
+The 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.
+As 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.
+This has some consequences for the CompCert compiler, namely an inability to write a \texttt{memcpy} routine.
+
+However, the CerCo memory model operates differently, as we need to move data `piecemeal' between stacks in the backend of the compiler.
+As a result, the bespoke memory model allows one to read data at any memory location, not just on value boundaries.
+This 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.
+
+Right now, the two memory models are interfaced during the translation from RTLabs to RTL.
+It 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.
+However, 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.
+
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 % SECTION.                                                                    %
@@ -487 +516 @@
 These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language.
 Closing these axioms should not be a problem.
-No further work remains, aside from `tidying up' the code.
+
+Further, tailcalls to external functions are currently axiomatised.
+This is due to there being a difficulty with how stackframes are handled with external function calls.
+We leave this for further work, due to there being no pressing need to implement this feature at the present time.
+
+There 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.
+Should this decision be taken, this will likely be straightforward but potentially time consuming.
 
 \newpage