Changeset 1725 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 23, 2012, 12:51:24 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1724 r1725 233 233 linearise graph visited required generated todo 234 234 else 235  Get the instruction at label ` `l'' in the graph235  Get the instruction at label `l' in the graph 236 236 let lookup := graph(l) in 237 237 let generated := generated $\cup\ \{$ lookup $\}$ in 238  Find the successor of the instruction at label ` `l'' in the graph238  Find the successor of the instruction at label `l' in the graph 239 239 let successor := succ(l, graph) in 240 240 let todo := successor::todo in … … 243 243 \end{lstlisting} 244 244 245 It is easy to see that this linearisation process eventually terminates. 246 In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising. 247 248 The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph. 249 We envisage needing to prove the following invariants on the linearisation function above: 250 251 \begin{enumerate} 252 \item 253 $\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels, 254 \item 255 $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$, 256 \item 257 $\mathtt{required} \subseteq \mathtt{visited}$, 258 \item 259 $\mathtt{visited} \cap \mathtt{todo} = \emptyset$. 260 \end{enumerate} 261 262 The invariants collectively imply the following properties, crucial to correctness, about the linearisation process: 263 264 \begin{enumerate} 265 \item 266 Every graph node is visited at most once, 267 \item 268 Every instruction that is generated is generated due to some graph node being visited, 269 \item 270 The successor instruction of every instruction that has been visited already will eventually be visited too. 271 \end{enumerate} 272 273 Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms. 274 In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions: 275 276 \begin{enumerate} 277 \item 278 For every jump to a label in a linearised program, the target label exists at some point in the program, 279 \item 280 Each label is unique, appearing only once in the program, 281 \item 282 The final instruction of a program must be a return. 283 \end{enumerate} 284 285 The final condition above is potentially a little opaque, so we explain further. 245 286 246 287 \section{The LIN to ASM and ASM to MCS51 machine code translations}
Note: See TracChangeset
for help on using the changeset viewer.