Changeset 3159

Timestamp:

Apr 17, 2013, 7:17:54 PM (6 years ago)

Author:

campbell

Message:

A bit more text in 3.4.

File:

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

Deliverables/D3.4/Report/report.tex

@@ -233 +233 @@
 initialisation, cost checks, had we dropped cminor loops in previous
 writing?, check mailing list in case I've forgotten something
+
+TODO: continued use of dep types to reduce partiality
 
 \subsection{Main goals}
@@ -579 +581 @@
 \section{Checking cost labelling properties}
 
-TODO: ideal for this development would be to prove at labelling stage,
-preserve throughout, fits with use of dep types to reduce partiality
-of phases; time pressures suggest different approach: t.v. style,
-runtime check only do proof in one place rather than three; can't push
-further due to structured traces, possible future investigation if ...
+Ideally, we would provide proofs that the cost labelling pass always
+produced programs that are soundly and precisely labelled and that
+each subsequent pass preserves these properties.  This would match our
+use of dependent types to eliminate impossible sources of errors
+during compilation, in particular retaining intermediate language type
+information.
+
+However, given the limited amount of time available we realised that
+implementing a compile-time check for a sound and precise labelling of
+the \textsf{RTLabs} intermediate code would reduce the proof burden
+considerably.  This is similar in spirit to the use of translation
+validation in certified compilation\todo{Cite some suitable work
+  here}, which makes a similar trade-off between the potential for
+compile-time failure and the volume of proof required.
+
+The check cannot be pushed into a later stage of the compiler because
+much of the information is embedded into the structured traces.
+However, if an alternative method was used to show that function
+returns in the compiled code are sufficiently well-behaved, then we
+could consider pushing the cost property checks into the timing
+analysis itself.  We leave this as a possible area for future work.
+
+\subsection{Implementation and correctness}
+
+For a cost labelling to be sound and precise we need a cost label at
+the start of each function, after each branch and at least once in
+every loop.  The first two parts are trivial to check by examining the
+code.  In \textsf{RTLabs} the last part is specified by saying
+that there is a bound on the number of successive instruction nodes in
+the CFG that you can follow before you encounter a cost label, and
+checking this is more difficult.
+
+The implementation works through the set of nodes in the graph,
+following successors until a cost label is found or a label-free cycle
+is discovered (in which case the property does not hold and we stop).
+This is made easier by the prior knowledge that any branch is followed
+by cost labels, so we do not need to search each branch.  When a label
+is found, we remove the chain from the set and continue until it is
+empty, at which point we know that there is a bound for every node in
+the graph.
+
+Directly reasoning about the function that implements this would be
+rather awkward, so an inductive specification of a single step of its
+behaviour was written and proved to match the implementation.  This
+was then used to prove the implementation sound and complete.
+
+While we have not attempted to proof that the cost labelled properties
+are established and preserved earlier in the compiler, we expect that
+the effort for the \textsf{Cminor} to \textsf{RTLabs} would be similar
+to the work outlined above, because it involves the change from
+requiring a cost label at particular positions to requiring cost
+labels to break loops in the CFG.  As there are another three passes
+to consider (including the labelling itself), we believe that using
+the check above is much simpler overall.
 
 \section{Existence of a structured trace}
 \label{sec:structuredtrace}
+
+\emph{Structured traces} enrich the execution trace of a program by
+nesting function calls in a mixed-step style\todo{Can I find a
+  justification for mixed-step} and embedding the cost properties of
+the program.  It was originally designed to support the proof of
+correctness for the timing analysis of the object code in the
+back-end, then generalised to provide a common structure to use from
+the end of the front-end to the object code.  See
+Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace}
+for an illustration of a structured trace.
+
+
 
 TODO: design, basic structure from termination proof, how cost