Changeset 1725 for Deliverables/D1.2

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

commit to avoid conflicts

1 edited


  • 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
     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.
     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:
     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,
     255$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
     257$\mathtt{required} \subseteq \mathtt{visited}$,
     259$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
     262The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:
     266Every graph node is visited at most once,
     268Every instruction that is generated is generated due to some graph node being visited,
     270The successor instruction of every instruction that has been visited already will eventually be visited too.
     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:
     278For every jump to a label in a linearised program, the target label exists at some point in the program,
     280Each label is unique, appearing only once in the program,
     282The final instruction of a program must be a return.
     285The final condition above is potentially a little opaque, so we explain further.
    246287\section{The LIN to ASM and ASM to MCS-51 machine code translations}
Note: See TracChangeset for help on using the changeset viewer.