Changeset 1725


Ignore:
Timestamp:
Feb 23, 2012, 12:51:24 PM (7 years ago)
Author:
mulligan
Message:

commit to avoid conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1724 r1725  
    233233        linearise graph visited required generated todo
    234234    else
    235       -- Get the instruction at label ``l'' in the graph
     235      -- Get the instruction at label `l' in the graph
    236236      let lookup := graph(l) in
    237237      let generated := generated $\cup\ \{$ lookup $\}$ in
    238       -- Find the successor of the instruction at label ``l'' in the graph
     238      -- Find the successor of the instruction at label `l' in the graph
    239239      let successor := succ(l, graph) in
    240240      let todo := successor::todo in
     
    243243\end{lstlisting}
    244244
     245It is easy to see that this linearisation process eventually terminates.
     246In 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
     248The 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.
     249We 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
     262The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
     263
     264\begin{enumerate}
     265\item
     266Every graph node is visited at most once,
     267\item
     268Every instruction that is generated is generated due to some graph node being visited,
     269\item
     270The successor instruction of every instruction that has been visited already will eventually be visited too.
     271\end{enumerate}
     272
     273Note, 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.
     274In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:
     275
     276\begin{enumerate}
     277\item
     278For every jump to a label in a linearised program, the target label exists at some point in the program,
     279\item
     280Each label is unique, appearing only once in the program,
     281\item
     282The final instruction of a program must be a return.
     283\end{enumerate}
     284
     285The final condition above is potentially a little opaque, so we explain further.
    245286
    246287\section{The LIN to ASM and ASM to MCS-51 machine code translations}
Note: See TracChangeset for help on using the changeset viewer.