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