Changeset 3670 for Papers


Ignore:
Timestamp:
Mar 21, 2017, 3:57:28 PM (19 months ago)
Author:
campbell
Message:

Move a chunk of old specification text into place

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

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

    r3667 r3670  
    10421042\subsection{Main correctness statement}
    10431043
    1044 Informally, our main intensional result links the time difference in a source
    1045 code execution to the time difference in the object code, expressing the time
    1046 for the source by summing the values for the cost labels in the trace, and the
    1047 time for the target by a clock built in to the 8051 executable semantics.
    1048 
    1049 The availability of precise timing information for 8501
    1050 implementations and the design of the compiler allow it to give exact
    1051 time costs in terms of processor cycles, not just upper bounds.
    1052 However, these exact results are only available if the subtrace we
    1053 measure starts and ends at suitable points.  In particular, pure
    1054 computation with no observable effects may be reordered and moved past
    1055 cost labels, so we cannot measure time between arbitrary statements in
    1056 the program.
    1057 
    1058 There is also a constraint on the subtraces that we
    1059 measure due to the requirements of the correctness proof for the
    1060 object code timing analysis.  To be sure that the timings are assigned
    1061 to the correct cost label, we need to know that each return from a
    1062 function call must go to the correct return address.  It is difficult
    1063 to observe this property locally in the object code because it relies
    1064 on much earlier stages in the compiler.  To convey this information to
    1065 the timing analysis extra structure is imposed on the subtraces, which
    1066 is described in Section~\ref{sec:fegoals}.
    1067 
    1068 % Regarding the footnote, would there even be much point?
    1069 % TODO: this might be quite easy to add ('just' subtract the
    1070 % measurable subtrace from the second label to the end).  Could also
    1071 % measure other traces in this manner.
    1072 These restrictions are reflected in the subtraces that we give timing
    1073 guarantees on; they must start at a cost label and end at the return
    1074 of the enclosing function of the cost label\footnote{We expect that
    1075   this would generalise to more general subtraces by subtracting costs
    1076   for unwanted measurable suffixes of a measurable subtrace.}.  A
    1077 typical example of such a subtrace is the execution of an entire
    1078 function from the cost label at the start of the function until it
    1079 returns.  We call such any such subtrace \emph{measurable} if it (and
    1080 the prefix of the trace from the start to the subtrace) can also be
    1081 executed within the available stack space.
    1082 
    1083 Now we can give the main intensional statement for the compiler.
    1084 Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
    1085 program, there is a subtrace of the 8051 object code program where the
    1086 time differences match.  Moreover, \emph{observable} parts of the
    1087 trace also match --- these are the appearance of cost labels and
    1088 function calls and returns.
    1089 
    1090 
    1091 
    1092 More formally, the definition of this statement in \matita{} is
    1093 \begin{lstlisting}[language=Grafite]
    1094 definition simulates :=
    1095   $\lambda$p: compiler_output.
    1096   let initial_status := initialise_status $...$ (cm (c_labelled_object_code $...$ p)) in
    1097   $\forall$m1,m2.
    1098    measurable Clight_pcs (c_labelled_clight $...$ p) m1 m2
    1099        (stack_sizes (c_stack_cost $...$ p)) (c_max_stack $...$ p) $\rightarrow$
    1100   $\forall$c1,c2.
    1101    clock_after Clight_pcs (c_labelled_clight $...$ p) m1 (c_clight_cost_map $...$ p) = OK $...$ c1 $\rightarrow$
    1102    clock_after Clight_pcs (c_labelled_clight $...$ p) (m1+m2) (c_clight_cost_map $...$ p) = OK $...$ c2 $\rightarrow$
    1103   $\exists$n1,n2.
    1104    observables Clight_pcs (c_labelled_clight $...$ p) m1 m2 =
    1105      observables (OC_preclassified_system (c_labelled_object_code $...$ p))
    1106           (c_labelled_object_code $...$ p) n1 n2
    1107   $\wedge$
    1108    clock ?? (execute (n1+n2) ? initial_status) =
    1109      clock ?? (execute n1 ? initial_status) + (c2-c1).
    1110 \end{lstlisting}
    1111 where the \lstinline'measurable', \lstinline'clock_after' and
    1112 \lstinline'observables' definitions are generic definitions for multiple
    1113 languages; in this case the \lstinline'Clight_pcs' record applies them
    1114 to \textsf{Clight} programs.
    1115 
    1116 There is a second part to the statement, which says that the initial
    1117 processing of the input program to produce the cost labelled version
    1118 does not affect the semantics of the program:
    1119 % Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
    1120 \begin{lstlisting}[language=Grafite]
    1121   $\forall$input_program,output.
    1122   compile input_program = return output $\rightarrow$
    1123   not_wrong $...$ (exec_inf $...$ clight_fullexec input_program) $\rightarrow$
    1124   sim_with_labels
    1125    (exec_inf $...$ clight_fullexec input_program)
    1126    (exec_inf $...$ clight_fullexec (c_labelled_clight $...$ output))
    1127 \end{lstlisting}
    1128 That is, any successful compilation produces a labelled program that
    1129 has identical behaviour to the original, so long as there is no
    1130 `undefined behaviour'.
    1131 
    1132 Note that this statement provides full functional correctness, including
    1133 preservation of (non-)termination.  The intensional result above does
    1134 not do this directly --- it does not guarantee the same result or same
    1135 termination.  There are two mitigating factors, however: first, to
    1136 prove the intensional property you need local simulation results --- these
    1137 can be pieced together to form full behavioural equivalence, only time
    1138 constraints have prevented us from doing so.  Second, if we wish to
    1139 confirm a result, termination, or non-termination we could add an
    1140 observable witness, such as a function that is only called if the
    1141 correct result is given.  The intensional result guarantees that the
    1142 observable witness is preserved, so the program must behave correctly.
    1143 
    1144 These two results are combined in the the \lstinline'correct'
    1145 theorem in the file \lstinline'correctness.ma'.
     1044[[relocated to specification section]]
    11461045
    11471046\section{Correctness statement for the front-end}
  • Papers/jar-cerco-2017/specification.tex

    r3669 r3670  
    2525\end{itemize}
    2626]]
     27
     28Informally, our main intensional result links the time difference in a source
     29code execution to the time difference in the object code, expressing the time
     30for the source by summing the values for the cost labels in the trace, and the
     31time for the target by a clock built in to the 8051 executable semantics.
     32
     33The availability of precise timing information for 8501
     34implementations and the design of the compiler allow it to give exact
     35time costs in terms of processor cycles, not just upper bounds.
     36However, these exact results are only available if the subtrace we
     37measure starts and ends at suitable points.  In particular, pure
     38computation with no observable effects may be reordered and moved past
     39cost labels, so we cannot measure time between arbitrary statements in
     40the program.
     41
     42There is also a constraint on the subtraces that we
     43measure due to the requirements of the correctness proof for the
     44object code timing analysis.  To be sure that the timings are assigned
     45to the correct cost label, we need to know that each return from a
     46function call must go to the correct return address.  It is difficult
     47to observe this property locally in the object code because it relies
     48on much earlier stages in the compiler.  To convey this information to
     49the timing analysis extra structure is imposed on the subtraces, which
     50is described in Section~\ref{sec:fegoals}.
     51
     52% Regarding the footnote, would there even be much point?
     53% TODO: this might be quite easy to add ('just' subtract the
     54% measurable subtrace from the second label to the end).  Could also
     55% measure other traces in this manner.
     56These restrictions are reflected in the subtraces that we give timing
     57guarantees on; they must start at a cost label and end at the return
     58of the enclosing function of the cost label\footnote{We expect that
     59  this would generalise to more general subtraces by subtracting costs
     60  for unwanted measurable suffixes of a measurable subtrace.}.  A
     61typical example of such a subtrace is the execution of an entire
     62function from the cost label at the start of the function until it
     63returns.  We call such any such subtrace \emph{measurable} if it (and
     64the prefix of the trace from the start to the subtrace) can also be
     65executed within the available stack space.
     66
     67Now we can give the main intensional statement for the compiler.
     68Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
     69program, there is a subtrace of the 8051 object code program where the
     70time differences match.  Moreover, \emph{observable} parts of the
     71trace also match --- these are the appearance of cost labels and
     72function calls and returns.
     73
     74
     75
     76More formally, the definition of this statement in \matita{} is
     77\begin{lstlisting}[language=Grafite]
     78definition simulates :=
     79  $\lambda$p: compiler_output.
     80  let initial_status := initialise_status $...$ (cm (c_labelled_object_code $...$ p)) in
     81  $\forall$m1,m2.
     82   measurable Clight_pcs (c_labelled_clight $...$ p) m1 m2
     83       (stack_sizes (c_stack_cost $...$ p)) (c_max_stack $...$ p) $\rightarrow$
     84  $\forall$c1,c2.
     85   clock_after Clight_pcs (c_labelled_clight $...$ p) m1 (c_clight_cost_map $...$ p) = OK $...$ c1 $\rightarrow$
     86   clock_after Clight_pcs (c_labelled_clight $...$ p) (m1+m2) (c_clight_cost_map $...$ p) = OK $...$ c2 $\rightarrow$
     87  $\exists$n1,n2.
     88   observables Clight_pcs (c_labelled_clight $...$ p) m1 m2 =
     89     observables (OC_preclassified_system (c_labelled_object_code $...$ p))
     90          (c_labelled_object_code $...$ p) n1 n2
     91  $\wedge$
     92   clock ?? (execute (n1+n2) ? initial_status) =
     93     clock ?? (execute n1 ? initial_status) + (c2-c1).
     94\end{lstlisting}
     95where the \lstinline'measurable', \lstinline'clock_after' and
     96\lstinline'observables' definitions are generic definitions for multiple
     97languages; in this case the \lstinline'Clight_pcs' record applies them
     98to \textsf{Clight} programs.
     99
     100There is a second part to the statement, which says that the initial
     101processing of the input program to produce the cost labelled version
     102does not affect the semantics of the program:
     103% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
     104\begin{lstlisting}[language=Grafite]
     105  $\forall$input_program,output.
     106  compile input_program = return output $\rightarrow$
     107  not_wrong $...$ (exec_inf $...$ clight_fullexec input_program) $\rightarrow$
     108  sim_with_labels
     109   (exec_inf $...$ clight_fullexec input_program)
     110   (exec_inf $...$ clight_fullexec (c_labelled_clight $...$ output))
     111\end{lstlisting}
     112That is, any successful compilation produces a labelled program that
     113has identical behaviour to the original, so long as there is no
     114`undefined behaviour'.
     115
     116Note that this statement provides full functional correctness, including
     117preservation of (non-)termination.  The intensional result above does
     118not do this directly --- it does not guarantee the same result or same
     119termination.  There are two mitigating factors, however: first, to
     120prove the intensional property you need local simulation results --- these
     121can be pieced together to form full behavioural equivalence, only time
     122constraints have prevented us from doing so.  Second, if we wish to
     123confirm a result, termination, or non-termination we could add an
     124observable witness, such as a function that is only called if the
     125correct result is given.  The intensional result guarantees that the
     126observable witness is preserved, so the program must behave correctly.
     127
     128These two results are combined in the the \lstinline'correct'
     129theorem in the file \lstinline'correctness.ma'.
    27130
    28131\subsection{Specifications for phases of the compiler}
Note: See TracChangeset for help on using the changeset viewer.