Changeset 3351

Timestamp:

Jun 14, 2013, 11:54:19 AM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/itp-2013/ccexec2.tex (modified) (2 diffs)

Papers/itp-2013/ccexec2.tex

@@ -879 +879 @@
 
 Another reason why the standard argument breaks is due to the requirement that
-function calls should yield back control after the calling point. This must be
-enforced just after
-
-\textbf{XXXXXXXXXXXXXXXXXX}
-
-A compiler preserves the program semantics by suppressing or introducing
-$\tau$ actions.
-
-Intuitively, it is because
-
-To understand why, consider the case of a function call
-and the pass that fixes the parameter passing conventions. A function
-call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no
-input nor output parameters. The pass must add explicit code before and after
-the function call to move the pseudo-registers content from/to the hardware
-registers or the stack in order to implement the parameter passing strategy.
-Similarly, each function body must be augmented with a preamble and a postamble
-to complete/initiate the parameter passing strategy for the call/return phase.
-Therefore what used to be a call followed by the next instruction to execute
-after the function return, now becomes a sequence of instructions, followed by
-a call, followed by another sequence. The two states at the beginning of the
-first sequence and at the end of the second sequence are in relation with
-the status before/after the call in the source code, like in an usual forward
-simulation. How can we prove however the additional condition for function calls
-that asks that when the function returns the instruction immediately after the
-function call is called? To grant this invariant, there must be another relation
-between the address of the function call in the source and in the target code.
-This additional relation is to be used in particular to relate the two stacks.
-
-
-
+function calls should yield back control after the calling point. Some passes
+need to translate a function call to a function call followed by some
+instructions (for example to restore caller-saved registers in the pass that
+sets the parameter convenction). In the forward simulation proof, these
+instructions are taken care of when simulating the \texttt{RETURN} step:
+the state just after the return in the source code is matched by the state $s_2$
+after these steps in the object code. However, the aforementioned requirement
+does not involve $s_2$, but the state reached after the return in the object
+code, that preceeds $s_2$ in the execution fragment. Therefore the requirement
+cannot be enforced with the standard forward simulation argument.
+
+In this section we present now a modified forward simulation argument that
+can be used to prove at once that a compiler preserves the semantics of the
+program, its weak traces and that the compiler propagates measurability.
 
 % @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@@ -1381 +1364 @@
 % an equivalence relation.
 
+\textbf{----------------------------}
+
 We summarise here the results of the previous sections. Each intermediate
 unstructured language can be given a semantics based on structured traces,