 Timestamp:
 Mar 21, 2017, 3:57:28 PM (19 months ago)
 Location:
 Papers/jarcerco2017
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/proof.tex
r3667 r3670 1042 1042 \subsection{Main correctness statement} 1043 1043 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) + (c2c1). 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 nonfunction 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 nontermination 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]] 1146 1045 1147 1046 \section{Correctness statement for the frontend} 
Papers/jarcerco2017/specification.tex
r3669 r3670 25 25 \end{itemize} 26 26 ]] 27 28 Informally, our main intensional result links the time difference in a source 29 code execution to the time difference in the object code, expressing the time 30 for the source by summing the values for the cost labels in the trace, and the 31 time for the target by a clock built in to the 8051 executable semantics. 32 33 The availability of precise timing information for 8501 34 implementations and the design of the compiler allow it to give exact 35 time costs in terms of processor cycles, not just upper bounds. 36 However, these exact results are only available if the subtrace we 37 measure starts and ends at suitable points. In particular, pure 38 computation 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. 41 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}. 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. 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 59 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 62 function 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. 66 67 Now we can give the main intensional statement for the compiler. 68 Given a \emph{measurable} subtrace for a labelled \textsf{Clight} 69 program, there is a subtrace of the 8051 object code program where the 70 time differences match. Moreover, \emph{observable} parts of the 71 trace also match  these are the appearance of cost labels and 72 function calls and returns. 73 74 75 76 More formally, the definition of this statement in \matita{} is 77 \begin{lstlisting}[language=Grafite] 78 definition 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) + (c2c1). 94 \end{lstlisting} 95 where the \lstinline'measurable', \lstinline'clock_after' and 96 \lstinline'observables' definitions are generic definitions for multiple 97 languages; in this case the \lstinline'Clight_pcs' record applies them 98 to \textsf{Clight} programs. 99 100 There is a second part to the statement, which says that the initial 101 processing of the input program to produce the cost labelled version 102 does not affect the semantics of the program: 103 % Yes, I'm paraphrasing the result a tiny bit to remove the observe nonfunction 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} 112 That is, any successful compilation produces a labelled program that 113 has identical behaviour to the original, so long as there is no 114 `undefined behaviour'. 115 116 Note that this statement provides full functional correctness, including 117 preservation of (non)termination. The intensional result above does 118 not do this directly  it does not guarantee the same result or same 119 termination. There are two mitigating factors, however: first, to 120 prove the intensional property you need local simulation results  these 121 can be pieced together to form full behavioural equivalence, only time 122 constraints have prevented us from doing so. Second, if we wish to 123 confirm a result, termination, or nontermination we could add an 124 observable witness, such as a function that is only called if the 125 correct result is given. The intensional result guarantees that the 126 observable witness is preserved, so the program must behave correctly. 127 128 These two results are combined in the the \lstinline'correct' 129 theorem in the file \lstinline'correctness.ma'. 27 130 28 131 \subsection{Specifications for phases of the compiler}
Note: See TracChangeset
for help on using the changeset viewer.