Changeset 1277 for Deliverables/D3.2/Report/report.tex

Timestamp:

Sep 26, 2011, 6:58:43 PM (9 years ago)

Author:

campbell

Message:

Runtime functions and conclusion for D3.2.

File:

• Deliverables/D3.2/Report/report.tex (modified) (2 diffs)

Deliverables/D3.2/Report/report.tex

@@ -255 +255 @@
 
 \subsection{Runtime functions}
-% TODO: this hasn't been implemented yet
+
+Some operations on integers do not have a simple translation to the target
+machine code.  In particular, we need to replace operations for 16 and 32-bit
+division and most bitwise shifts with calls to runtime functions.  These
+functions need to be added to the program at an early stage because of their
+impact on execution time:  any loops must be available to our labelling
+mechanism so that we can report on how long the resulting machine code will
+take to execute.
+
+We follow the prototype in replacing the affected expressions, which requires
+us to break up expressions into multiple statements because function calls are
+not permitted in \textsf{Clight} expressions.  We may investigate moving these
+substitutions to a later stage of the compiler if they prove difficult to
+reason about.  However, this would also require adjusting the semantics so
+that the costs still appear in the evaluation of \textsf{Clight} programs.
+
+The prototype adds the functions themselves by generating C code as text and
+reparsing the program.  This is unsuitable for formalization, so we generate
+\textsf{Clight} abstract syntax trees directly.
 
 \subsection{Conversion to Cminor}
@@ -418 +436 @@
 \section{Conclusion}
 
+We have formalized the front-end of the \cerco{} compiler in the \matita{}
+proof assistant, and shown that invariants can be added to the intermediate
+languages to help show properties of it.  This work provides a solid basis for
+the compiler correctness proofs in task 3.4.
+
 \bibliographystyle{plain}
 \bibliography{report}