Changeset 1725 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 23, 2012, 12:51:24 PM (8 years ago)

Author:

mulligan

Message:

commit to avoid conflicts

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -233 +233 @@
         linearise graph visited required generated todo
     else
-      -- Get the instruction at label ``l'' in the graph
+      -- Get the instruction at label `l' in the graph
       let lookup := graph(l) in
       let generated := generated $\cup\ \{$ lookup $\}$ in
-      -- Find the successor of the instruction at label ``l'' in the graph
+      -- Find the successor of the instruction at label `l' in the graph
       let successor := succ(l, graph) in
       let todo := successor::todo in
@@ -243 +243 @@
 \end{lstlisting}
 
+It is easy to see that this linearisation process eventually terminates.
+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.
+
+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.
+We envisage needing to prove the following invariants on the linearisation function above:
+
+\begin{enumerate}
+\item
+$\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,
+\item
+$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
+\item
+$\mathtt{required} \subseteq \mathtt{visited}$,
+\item
+$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
+\end{enumerate}
+
+The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
+
+\begin{enumerate}
+\item
+Every graph node is visited at most once,
+\item
+Every instruction that is generated is generated due to some graph node being visited,
+\item
+The successor instruction of every instruction that has been visited already will eventually be visited too.
+\end{enumerate}
+
+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.
+In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
+
+\begin{enumerate}
+\item
+For every jump to a label in a linearised program, the target label exists at some point in the program,
+\item
+Each label is unique, appearing only once in the program,
+\item
+The final instruction of a program must be a return.
+\end{enumerate}
+
+The final condition above is potentially a little opaque, so we explain further.
 
 \section{The LIN to ASM and ASM to MCS-51 machine code translations}