Changeset 1773
 Timestamp:
 Feb 27, 2012, 3:53:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1772 r1773 317 317 318 318 \subsection{Graph translations} 319 RTLabs and most intermediate languages in the backend have a graph 320 representation: 321 the code of each function is represented by a graph of instructions. 322 The graph maps a set of labels (the names of the nodes) to the instruction 323 stored at that label (the nodes of the graph). 324 Instructions reference zero or more additional labels that are the immediate 325 successors of the instruction: zero for return from functions; more than one 326 for conditional jumps and calls; one in all other cases. The references 327 from one instruction to its immediates are the arcs of the graph. 328 329 Status of graph languages always have a program counter that holds a 330 representation of a reference to the current instruction. 331 332 A translation between two consecutive graph languages maps each instruction 333 stored at location $l$ in the first graph and with immediate successors 334 $\{l_1,\ldots,l_n\}$ to a subgraph of the output graph that has a single 335 entry point at location $l$ and exit arcs to $\{l_1,\ldots,l_n\}$. Moreover, 336 the labels of all non entry nodes in the subgraph are distinct from all the 337 labels in the source graph. 338 339 In order to simplify the translations and the relative proofs of forward 340 simulation, after the release of D4.2 and D4.3, we have provided: 341 \begin{itemize} 342 \item a new data type (called \texttt{blist}) that represents a 343 sequence of instructions to be added to the output graph. 344 The ``b'' in the name stands for binder, since a \texttt{blist} is 345 either empty, an extension of a \texttt{blist} with an instruction 346 at the front, or the generation of a fresh quantity followed by a 347 \texttt{blist}. The latter feature is used, for instance, to generate 348 fresh register names. The instructions in the list are unlabelled and 349 all of them but the last one are also sequential, like in a linear program. 350 \item a new iterator (called \texttt{b\_graph\_translate}) of type 351 \begin{displaymath} 352 \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist}) 353 \rightarrow \mathtt{graph} \rightarrow \mathtt{graph} 354 \end{displaymath} 355 The iterator transform the input graph in the output graph by replacing 356 each node with the graph that corresponds to the linear \texttt{blist} 357 obtained by applying the function in input to the node label. 358 \end{itemize} 359 360 Using the iterator above, the code can be written in such a way that 361 the programmer does not see any distinction between writing a transformation 362 on linear or graph languages. 363 364 In order to prove simulations for translations obtained using the iterator, 365 we will prove the following theorem: 366 367 \begin{align*} 368 \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\ 369 & \forall f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\ 370 & \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (next \ l \ G_i)\ G_{\sigma} 371 \end{align*} 372 373 Here \texttt{subgraph} is a computational predicate that given a \texttt{blist} 374 $[i_1, \ldots, i_n]$, an entry label $l$, an exit label $l'$ and a graph $G$ 375 expands to the fact that fetching from $G$ at address $l$ one retrieves a node 376 $i_1$ with a successor $l_1$ that, when fetched, yields a node $i_2$ with a 377 successor $l_2$ such that \ldots. The successor of $i_n$ is $l'$. 378 379 Proving a forward simulation diagram of the following kind using the theorem 380 above is now as simple as doing the same using standard small step operational 381 semantics over linear languages. 382 383 \begin{align*} 384 \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\ 385 & \forall s. \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\ 386 & \mathtt{let}\ l := pc\ s\ \mathtt{in} \\ 387 & s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma 388 \end{align*} 389 390 Because of the fact that graph translation preserves entry and exit labels of 391 translated statements, the state translation function $\sigma$ will simply 392 preserve the value of the program counter. The program code, which is 393 part of the state, is translated using the iterator. 394 395 The proof is then roughly the following. Let $l$ be the program counter of the 396 input state $s$. We proceed by cases on the current instruction of $s$. 397 Let $[i_1, \ldots, i_n]$ be the \texttt{blist} associated to $l$ and $s$ 398 by the translation function. The witness required for the existential 399 statement is simply $n$. By applying the theorem above we know that the 400 next $n$ instructions that will be fetched from $s\ \sigma$ will be 401 $[i_1, \ldots, i_n]$ and it is now sufficient to prove that they simulate 402 the original instruction. 319 403 320 404 \subsection{The RTLabs to RTL translation} … … 583 667 \end{diagram} 584 668 \end{displaymath} 585 586 \subsection{The RTL to ERTL translation}587 \label{subsect.rtl.ertl.translation}588 589 \begin{displaymath}590 \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})591 \rightarrow \mathtt{graph} \rightarrow \mathtt{graph}592 \end{displaymath}593 594 \begin{align*}595 \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\596 & \forall f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\597 & \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}598 \end{align*}599 600 \begin{align*}601 \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\602 & \forall s. \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\603 & \mathtt{let}\ l := pc\ s\ \mathtt{in} \\604 & s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma605 \end{align*}606 669 607 670 \begin{align*}
Note: See TracChangeset
for help on using the changeset viewer.