Changeset 3671 for Papers


Ignore:
Timestamp:
Mar 21, 2017, 3:57:29 PM (2 years ago)
Author:
campbell
Message:

Rework some whole-compiler spec

File:
1 edited

Legend:

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

    r3670 r3671  
    4848on much earlier stages in the compiler.  To convey this information to
    4949the timing analysis extra structure is imposed on the subtraces, which
    50 is described in Section~\ref{sec:fegoals}.
     50is described in Section~\ref{sec:fegoals}. % TODO: update cross-ref
     51
     52These restrictions are reflected in the subtraces that we give timing
     53guarantees on; they must start at a cost label and end at the return
     54of the enclosing function of the cost label.  Finally, we need the
     55execution to stay within the stack bounds, leading to the following
     56definition.
    5157
    5258% Regarding the footnote, would there even be much point?
     
    5460% measurable subtrace from the second label to the end).  Could also
    5561% measure other traces in this manner.
    56 These restrictions are reflected in the subtraces that we give timing
    57 guarantees on; they must start at a cost label and end at the return
    58 of the enclosing function of the cost label\footnote{We expect that
     62\begin{definition}
     63A subtrace of an execution trace is \emph{measurable} if
     64\begin{enumerate}
     65\item the subtrace, and the prefix of the full trace leading up to the
     66  subtrace, can be executed within the available stack space,
     67\item the subtrace starts at a cost label, and
     68\item the subtrace ends at the return of the enclosing function of the
     69  cost label\footnote{We expect that
    5970  this would generalise to more general subtraces by subtracting costs
    60   for unwanted measurable suffixes of a measurable subtrace.}.  A
    61 typical example of such a subtrace is the execution of an entire
     71  for unwanted measurable suffixes of a measurable subtrace.}.
     72  % the formalisation splits this into first noting that the start is
     73  % a label and the end is a return, then a separate proof that it's
     74  % the *right* return
     75\end{enumerate}
     76\end{definition}
     77
     78A typical example of such a subtrace is the execution of an entire
    6279function from the cost label at the start of the function until it
    63 returns.  We call such any such subtrace \emph{measurable} if it (and
    64 the prefix of the trace from the start to the subtrace) can also be
    65 executed within the available stack space.
     80returns.
     81
     82[[Still need to revise the rest of this]]
    6683
    6784Now we can give the main intensional statement for the compiler.
     
    149166\item Will probably cover most of measurable subtraces above
    150167\item Figure needs updated, maybe concepts changed?
     168\item compiler ensures correct labelling, so only appears in particular places
    151169\item structured traces need a good explanation here
    152170\item change of perspective at RTLabs, maybe ASM too?
Note: See TracChangeset for help on using the changeset viewer.