Changeset 3673


Ignore:
Timestamp:
Mar 21, 2017, 7:09:05 PM (7 months ago)
Author:
campbell
Message:

Tweak whole-compiler spec statement

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/specification.tex

    r3671 r3673  
    3737measure starts and ends at suitable points.  In particular, pure
    3838computation with no observable effects may be reordered and moved past
    39 cost labels, so we cannot measure time between arbitrary statements in
    40 the program.
     39cost labels, so we cannot expect to be able to measure time between
     40arbitrary statements in the program.
    4141
    42 There is also a constraint on the subtraces that we
    43 measure due to the requirements of the correctness proof for the
    44 object code timing analysis.  To be sure that the timings are assigned
    45 to the correct cost label, we need to know that each return from a
    46 function call must go to the correct return address.  It is difficult
    47 to observe this property locally in the object code because it relies
    48 on much earlier stages in the compiler.  To convey this information to
    49 the timing analysis extra structure is imposed on the subtraces, which
    50 is described in Section~\ref{sec:fegoals}. % TODO: update cross-ref
     42% TODO: Footnote might have a forward ref to further work (e.g.,
     43% sticking a label after every call)
     44Some cost labels in the program may cover statements before and after
     45a function call.  To be sure that the compiled machine code timings
     46are assigned to the correct cost label without approximation, we need
     47to know that each return from a function call resumes execution in the
     48caller\footnote{Our embedded compiler does not support non-local
     49  control flow functions such as \lstinline'longjmp' and
     50  \lstinline'exit'.}.
    5151
    52 These restrictions are reflected in the subtraces that we give timing
    53 guarantees on; they must start at a cost label and end at the return
    54 of the enclosing function of the cost label.  Finally, we need the
    55 execution to stay within the stack bounds, leading to the following
    56 definition.
     52These two restrictions are reflected in the subtraces that we give
     53timing guarantees on; they must start at a cost label and end at the
     54return of the enclosing function of the cost label.  Also, we need the
     55execution to stay within the machine's stack memory, leading to
     56the following definition.
    5757
    5858% Regarding the footnote, would there even be much point?
     
    6464\begin{enumerate}
    6565\item the subtrace, and the prefix of the full trace leading up to the
    66   subtrace, can be executed within the available stack space,
     66  subtrace, has predicted machine code stack usage less than or equal
     67  to the available stack space,
    6768\item the subtrace starts at a cost label, and
    6869\item the subtrace ends at the return of the enclosing function of the
     
    174175\end{itemize}]]
    175176
     177[[This was in the whole-compiler bit before, about properly bracketed code.
     178Might still be useful.]]
     179It is difficult to observe this property
     180locally in the object code because it relies on much earlier stages in
     181the compiler.  To convey this information to the timing analysis extra
     182structure is imposed on the subtraces, which is described in
     183Section~\ref{sec:fegoals}. % TODO: update cross-ref
     184
     185
    176186%%% Local Variables:
    177187%%% TeX-master: "cerco"
Note: See TracChangeset for help on using the changeset viewer.