Changeset 3159

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

A bit more text in 3.4.

1 edited


  • Deliverables/D3.4/Report/report.tex

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