Changeset 3222


Ignore:
Timestamp:
Apr 30, 2013, 11:45:00 AM (4 years ago)
Author:
tranquil
Message:

added pages to included papers. final version.

Files:
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.4/mauro.tex

    r3213 r3222  
    77An instance of the record \verb=sem_graph_params= contains all common information about
    88programs of a joint-language whose source code can be logically organized as a graph.
    9 Thus, every program of this kind will be an ihabitant of the type \verb=joint_program p=,
    10 where \verb=p= is an istance of \verb=sem_graph_params=. We want to stress that such a record
     9Thus, every program of this kind will be an inhabitant of the type \verb=joint_program p=,
     10where \verb=p= is an instance of \verb=sem_graph_params=. We want to stress that such a record
    1111is in a sub-type relation with the record \verb=params=, which was explained in  Deliverable 4.3.
    1212
    13 In order to establish the correctness of our cost-model in each compiler's backend pass, where
    14 both source and target programs are joint-graph-programs, i.e. the source program \verb=src=
    15 (resp. the target program \verb=out=) is such that there is a \verb=p_in=
    16 (resp. \verb=p_out=) of type \verb=sem_graph_params= such that
    17 \verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to
     13In order to establish the correctness of our cost-model in each compiler's back-end pass, where
     14both source and target programs are joint-graph-programs, i.e.\ the source program \verb=src=
     15(resp.\ the target program \verb=out=) is such that there is a \verb=p_in=
     16(resp.\ \verb=p_out=) of type \verb=sem_graph_params= such that
     17\verb=src : joint_program p_in= (resp.\ \verb=out : joint_program p_out=), we would like to
    1818prove a statement similar to this shape.
    1919\begin{lstlisting}
     
    4444Since traces carry both extensional and intensional information, the main disadvantage
    4545with this approach is that the extensional part of the proof (for example
    46 the preservation the semantical relation between states of the program under evaluation)
    47 and the intensional part (for example, all proof obbligation dealing with
     46the preservation the semantic relation between states of the program under evaluation)
     47and the intensional part (for example, all proof obligation dealing with
    4848the presence of a cost label in some point of the code) are mixed together in a not very clear way.
    4949
    50 Furthermore, some proof obbligations concerning the relation among program counters
     50Furthermore, some proof obligations concerning the relation among program counters
    5151(for example, the call relation between states which is one of the field of
    5252\verb=status_rel= record) depend only on the way the translation from source to target program is done.
    5353In particular if the translation satisfies some suitable properties, then it is possible
    54 to define some ``standard relations'' that automatically satisfy these proof obbligations,
     54to define some ``standard relations'' that automatically satisfy these proof obligations,
    5555in an independent way from the specific source and target languages.
    5656
    57 So our question is wether there is a way to use these observation in order to factorize all common
     57So our question is whether there is a way to use these observation in order to factorize all common
    5858aspects of all correctness proofs of each pass involving joint languages.
    5959The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove
    60 the correctness of a single pass involving two joint-languages, to provide some semnatical state relation that
     60the correctness of a single pass involving two joint-languages, to provide some semantic state relation that
    6161satisfies some conditions. These conditions never speak about traces and they are mostly
    62 extensional, with the intesional part being limited to some additional requirred properties of
    63 the translation. This layer will use the trace machineary in order to deliver the desired correctness
     62extensional, with the intensional part being limited to some additional required properties of
     63the translation. This layer will use the trace machinery in order to deliver the desired correctness
    6464proof of the pass.
    6565
    66 In order to reach this goal, we have to analyze first whether there is a common way to perform language
    67 translation for each pass. After having defined and specified the translation machienary, we will
    68 explain how it is possibile to use it in order to build such a layer. So this section is organized as follows:
    69 in the first part we explain the translation machienary while in the second part we explain such a layer.
     66In order to reach this goal, we have to analyse first whether there is a common way to perform language
     67translation for each pass. After having defined and specified the translation machinery, we will
     68explain how it is possible to use it in order to build such a layer. So this section is organized as follows:
     69in the first part we explain the translation machinery while in the second part we explain such a layer.
    7070
    7171\subsection{Graph translation}
     
    7373translation of a program in terms of the way we translate each internal function. Thus, if we let
    7474\verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and
    75 the target program, the aim is writing a Matita's function that takes as input an object of type
     75the target program, the aim is writing a \s{matita}'s function that takes as input an object of type
    7676\verb=joint_closed_internal_function src_g_pars= together with additional information
    7777(that we will explain better later) and gives as output an object of type
     
    8989    bind_new_instantiates ?? data' data regs ∧
    9090    b_graph_translate_props … data' def_in def_out f_lbls f_regs.
    91 ........
    9291\end{lstlisting}
    9392
     
    9796\subsubsection{Input requested by the translation process}
    9897Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate.
    99 But it also takes in input some useful infomrmation which will be used in order to dictate the translation process.
    100 These information are all contained in an instance of the following record.
     98But it also takes in input some useful information which will be used in order to dictate the translation process.
     99These informations are all contained in an instance of the following record,
     100where we skip some technical details.
    101101
    102102\begin{lstlisting}
     
    111111; f_step : label → joint_step src globals → bind_step_block dst globals
    112112; f_fin : label → joint_fin_step src → bind_fin_block dst globals
    113 ; good_f_step :
    114   ∀l,s.bind_new_P' ??
    115     (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in
    116        ∀l.
    117        let allowed_labels ≝ l :: step_labels … s in
    118        let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
    119        All (label → joint_seq ??)
    120          (λs'.step_labels_and_registers_in … allowed_labels allowed_registers
    121               (step_seq dst globals (s' l)))
    122          pref ∧
    123        step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
    124        All (joint_seq ??)
    125          (step_labels_and_registers_in … allowed_labels allowed_registers)
    126          post)
    127     (f_step l s)
    128 ; good_f_fin :
    129   ∀l,s.bind_new_P' ??
    130     (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in
    131        let allowed_labels ≝ l :: fin_step_labels … s in
    132        let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
    133        All (joint_seq ??)
    134          (λs.step_labels_and_registers_in … allowed_labels allowed_registers s)
    135          pref ∧
    136        fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
    137     (f_fin l s)
     113; good_f_step : …
     114; good_f_fin : …
    138115; f_step_on_cost :
    139116  ∀l,c.f_step l (COST_LABEL … c) =
     
    146123}
    147124\end{lstlisting}
    148 We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of
    149 a pseudo-register (resp. a code point) is {\em fresh} when it never appears in the code of the source function.
    150 \begin{center}
    151 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
    152 Field & Explanation \\
     125\autoref{tab:translate_data} summarizes what each field means and how it is used in the translation process. We will say that an identifier of
     126a pseudo-register (resp.\ a code label) is {\em fresh} when it never appears in the code of the source function.
     127\begin{table}
     128 \centering
     129\begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}}
     130Field & Explanation \\[5pt]
    153131\hline
    154 \texttt{init\_ret} & It tells how to fill the field \texttt{joint\_if\_result}, i.e. it tells what is the translation of the result for the translated function.\\
    155 \texttt{init\_params} & It tells how to fill the field \texttt{joint\_if\_params}, i.e. it tells what is the translation of the formal parameters of the translated function.\\
    156 \texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which is used in orderto deal with cost model of stack usage. \\
    157 \texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\
    158 \texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are used by statements in \texttt{added\_prologue}. \\
    159 \texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e. statements admitting a syntactical successor. Statements of this kind are all sequential statements, a cost emission statement, a call statement and a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the code-point of the instruction the execution flow will jump in case the guard of the conditional is evaluated to false. \\
    160 \texttt{f\_fin} & It is a function that tells how to translate all {\em final statements} i.e. statements do not admitting a syntactical successor. Statements of this kind are return statements, unconditioned jump statements and tailcalls.\\
    161 \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that all identifier (pseudo-registers or code points) used by the block of step statements being the translation of a step statement either come from the statement being translated or they are fresh and generated by the universe field of the translated function (\verb=joint_if_luniverse= in case of code point identifier or \verb=joint_if_runiverse= in case of pseudo-register identifier).  \\
    162 \texttt{good\_f\_fin} & It tells that the translation function of all final statements is well formed. Such a condition is similar to the one given for step statements.\\
    163 \texttt{f\_step\_on\_cost} and \texttt{cost\_in\_f\_step}& It gives a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e. it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source.
     132\texttt{init\_ret} & It tells where the result for the translated function is stored.\\[5pt]
     133\texttt{init\_params} & It tells what is the translation of the formal parameters.\\[5pt]
     134\texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which tells how much stack is required by the function at the given stage of compilation. \\[5pt]
     135\texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\[5pt]
     136\texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are generated when instantiating
     137this record. They are typically used to store data that must be saved across the call (e.g.\ the return address
     138popped from the internal stack).\\[5pt]
     139\texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e.\ statements admitting a syntactical successor. Statements of this kind are sequential statements, a cost emission statement, a call statement or a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the point where the flow will continue in case the guard is false. \\[5pt]
     140\texttt{f\_fin} & As above, but for {\em final statements} i.e.\ statements do not admitting a syntactical successor. Statements of this kind are return and unconditioned jump statements.\\[5pt]
     141\texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that
     142the block \verb=f_step I= for a step \verb=I= only uses code labels and register appearing in \verb=I=, \verb=new_regs= or generated by the appropriate identifier universe fields of the translated function. \\[5pt]
     143\texttt{good\_f\_fin} & As above, but for \verb=f_fin=.\\[5pt]
     144\texttt{f\_step\_on\_cost}, \texttt{cost\_in\_f\_step}& They give a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e.\ it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source.\\[5pt]
    164145\end{tabular*}
    165 \end{center}
     146\caption{The explanation of the various fields of the \verb=b_graph_translate_data= record.}
     147\label{tab:translate_data}
     148\end{table}
    166149
    167150\subsubsection{Output given the translation process}
     
    184167instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have
    185168fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudo-registers or
    186 (even worste) they may use some fresh code-point identifiers being generated by the translation (we will see later
     169(even worse) they may use some fresh code-point identifiers being generated by the translation (we will see later
    187170that this will be important when translating a call statement). We will use the above mentioned functions
    188171to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the
     
    213196; freshness_lbls :
    214197  (∀l.All …
    215     (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
    216            fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
     198    (λlbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧
     199           in_universe … lbl (joint_if_luniverse … def_out)) (f_lbls l))
    217200; freshness_regs :
    218201  (∀l.All …
    219     (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    220            fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
     202    (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧
     203           in_universe … reg (joint_if_runiverse … def_out)) (f_regs l))
    221204; freshness_data_regs :
    222   All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    223                fresh_for_univ … reg (joint_if_runiverse … def_out))
     205  All … (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧
     206               in_universe … reg (joint_if_runiverse … def_out))
    224207        (new_regs … data)
    225208; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
     
    242225; prologue_ok :
    243226  if not_emptyb … (added_prologue … data) then
    244     ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     227    ∃lbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧
    245228    joint_if_entry … def_out
    246229      -( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in),
     
    250233}.
    251234\end{lstlisting}
    252 
    253 We will now summarize the meaning of each field of the record using the same approach followed
    254 in the previous subsection.
    255 \begin{center}
    256 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
    257 Field & Explanation \\
     235\autoref{tab:translate_props} summarizes the meaning of each field of the record.
     236\begin{table}
     237\centering
     238\begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}}
     239Field & Explanation \\[5pt]
    258240\hline
    259 \texttt{res\_def\_out\_eq} & It tells that the result of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
    260 \texttt{pars\_def\_out\_eq} & It tells that the formal parameters of the translated function are the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
    261 \texttt{ss\_def\_out\_eq} & It tells that the \verb=joint_if_stacksize= field of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\
    262 \texttt{partition\_lbls} & All lists of code-point identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetition. \\
    263 \texttt{partition\_regs} & All lists of pseudo-register identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetion. \\
    264 \texttt{freshness\_lbls} & All lists of code-point identifiers generated by a code-point of the code of the source internal function are fresh.  \\
    265 \texttt{freshness\_regs} & All lists of pseudo-register identifiers generated by a code-point of the code of the source internal function are fresh.  \\
    266 \texttt{freshness\_data\_regs} & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\
    267 \texttt{data\_regs\_disjoint} &  All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input never appear in any list of pseudo-register identifiers generated by a code-point of the code of the source internal function. \\
     241\texttt{res\_def\_out\_eq}, \texttt{pars\_def\_out\_eq}, \texttt{ss\_def\_out\_eq}&
     242The return value location, the formal parameters and the syntactic stack size are
     243all as dictated by the corresponding \verb=b_graph_translate_data= fields.\\[5pt]
     244\texttt{partition\_lbls}, \texttt{partition\_regs}&
     245\verb=f_lbls= and \verb=f_regs= are partial partitions, i.e.\ all lists in their
     246image are repetition-free and disjoint for different input values. \\[5pt]
     247\texttt{freshness\_lbls}, \texttt{freshness\_regs}, \texttt{freshness\_data\_regs}&
     248All lists of code-point identifiers and register generated at a source code-point, and the registers in
     249\verb=new_regs= are fresh:
     250they were not in the former source universe and they are in the new one.\\[5pt]
     251 & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\[5pt]
     252\texttt{data\_regs\_disjoint} &  All pseudo-register in \texttt{new\_regs} never appear in \verb=f_regs=. \\[5pt]
    268253\texttt{multi\_fetch\_ok} & Given a statement $I$ and a code-point identifier $l$ of the source internal function such that $I$ is located in $l$, if the translation process translate $I$ into a statement block $\langle I_1,\ldots ,I_n\rangle$ then
    269254$f\_lbls(l) = [l_1,\ldots,l_{n-1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical
    270255successor, $I_2$ is located in $l_1$ with $l_2$ as syntactical successor, and so on with the last statement $I_n$ located in $l_{n-1}$
    271 and it may have a syntactical successor depending wether $I$ is a step-statement or not: in the former case we have that the
    272 syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\ 
    273 \texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the code-point identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a cost-emission statement followed by the instructions of  \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a NOOP instruction.
     256and it may have a syntactical successor depending whether $I$ is a step-statement or not: in the former case we have that the
     257syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\[5pt]
     258\texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the code-point identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a cost-emission statement followed by the instructions of  \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a \s{NOP} instruction.
    274259\end{tabular*}
    275 \end{center}
     260\caption{The explanation of the various fields of the \verb=b_graph_translate_props= record.}
     261\label{tab:translate_props}
     262\end{table}
    276263
    277264\subsection{A general correctness proof}
    278 In order to prove our general result, we need to define the usual semantical (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satify some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantical relation satisfying some conditions that allow us to prove our general result.
     265In order to prove our general result, we need to define the usual semantic (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satisfy some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantic relation satisfying some conditions that allow us to prove our general result.
    279266
    280267\subsubsection{A standard calling relation}
    281 Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will explot the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantical one). The idea of defining a standard calling relation is to compute the code-point identifier of this $I_k$, starting from the code-point identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$.
    282 
    283 In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a step-statement
     268Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will exploit the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantic one). The idea of defining a standard calling relation is to compute the code-point identifier of this $I_k$, starting from the code-point identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$.
     269
     270In order to explain how this machinery work. we need to enter more in the detail of the translation process. Given a step-statement
    284271$I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential
    285272statements called {\em preamble}, $p$ is a step-statement (we call it {\em pivot}) and $post$ is again a list of sequential statements
    286273called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation
    287274of $I$ is $\langle s_1,\ldots,s_n,p,s_1',\ldots,s_m'\rangle$. In case $I$ is a final statement, than its translation does not have
    288 postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
     275postamble, i.e.\ it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.
    289276
    290277Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation
     
    292279in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is non-empty.
    293280then $l'$ is $n-1$-th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble.
    294 The Matita's definition computing the code points according to the above mentioned specification is the following one.
     281The \s{matita}'s definition computing the code points according to the above mentioned specification is the following one.
    295282\begin{lstlisting}
    296283definition sigma_label : ∀p_in,p_out : sem_graph_params.
     
    304291! <id,fn> ← res_to_opt … (fetch_internal_function …
    305292                           (joint_globalenv p_in prog stack_size) bl);
    306 ! <res,s> ←
    307  find ?? (joint_if_code ?? fn)
    308   (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with
     293! <res,s> ← find ?? (joint_if_code ?? fn)
     294  (λlbl.λ_.
     295    match preamble_length … prog stack_size init init_regs f_regs bl lbl with
    309296             [ None ⇒ false
    310297             | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with
     
    316303\end{lstlisting}
    317304This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a
    318 function location and a code-point identifier $l$; it fetches the internal function of the source language in the correponding location.
     305function location and a code-point identifier $l$; it fetches the internal function of the source language in the corresponding location.
    319306Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that,
    320307either $l = l'$ in case the preamble of the translation of $I$ is empty or $l'$ is the $n -1$-th where $n \geq 0$ is the length
     
    325312
    326313We can prove that, starting from a code point identifier of the translated internal function,
    327 whenever there exists a code-point identifier in the source internal function satifying the above condition, then it is always unique.
     314whenever there exists a code-point identifier in the source internal function satisfying the above condition, then it is always unique.
    328315The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof
    329316of this statement.
    330 
    331 We can wrap this function inside the definition of the desired relation among program counter states in the following way
     317We can wrap this function inside the definition of the desired relation between program counter states in the following way
    332318The conditional at the beginning is put to deal with the pre-main case, which is translated without following the standard
    333 translation process we explain in previous section.
     319translation process we explained in previous section.
    334320\begin{lstlisting}
    335321definition sigma_pc_opt : 
     
    357343The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in
    358344at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program
    359 which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
    360 statement of the tranlation. The formalization of this statement in Matita is given in the following.
     345which is in relation with $pc$ (i.e.\ $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot
     346statement of the translation. The formalization of this statement in \s{matita} is given in the following.
    361347
    362348\begin{lstlisting}
     
    404390(λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call.
    405391 λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call.
    406 pc ? s1 =
    407  sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
     392pc ? s1 = sigma_stored_pc
     393  p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).
    408394\end{lstlisting}
    409395
     
    412398use the translation process we explain in the previous section.
    413399
    414 \subsubsection{The semantical relation}
    415 The semantical relation between states is the classical relation used in forward simulation proofs.
    416 It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state
     400\subsubsection{The semantic relation}
     401The semantic relation between states is the classical relation used in forward simulation proofs.
     402It correlates the data of the status (e.g. register, memory, \emph{etc}). We remind that the notion of state
    417403in joint language is summarized in the following record.
    418404\begin{lstlisting}
     
    428414when executing a return instruction.
    429415
    430 The type of the semantical relation between state is the following.
     416The type of the semantic relation between state is the following.
    431417
    432418\begin{lstlisting}
     
    435421\end{lstlisting}
    436422
    437 We would like to state some conditions the semantical relation between states have to satisfy in order
     423We would like to state some conditions the semantic relation between states have to satisfy in order
    438424to get our simulation result. We would like that this relation have some flavour of compositionality.
    439425In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e.
    440 the field that really contains data information of the state. So we need also a data relation, i.e.
     426the field that really contains data information of the state. So we need also a data relation, i.e.\
    441427a relation of this type.
    442428
     
    447433
    448434Notice that the data relation cab depend on a specific program counter of the source. This is done
    449 to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know
    450 where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or
     435to capture complex data relations like the ones in the \s{ERTL} to \s{LTL} pass, in which you need to know
     436where data in pseudo-registers of \s{ERTL} are stored by the translation (either in hardware register or
    451437in memory) and this information depends on the code point on the statement being translated.
    452438
     
    484470% \end{lstlisting}
    485471%
    486 Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical
     472Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic
    487473relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates
    488 that two states that are in semantical relation should have the same program counter. This is due
     474that two states that are in semantic relation should have the same program counter. This is due
    489475to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source
    490476internal function is translated with a block of instructions in the translated internal function
    491 whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}
    492 postulates that two states that are in semantical relation have the last popped calling address
     477whose initial statement is at the same code point $l$. The condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}
     478postulates that two states that are in semantic relation have the last popped calling address
    493479in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same
    494480program counter, the last pop fields in call relation and the data fields also in data relation, then
    495 they are in semantical relation.
     481they are in semantic relation.
    496482
    497483Another important condition is that the pivot statement of the translation of a call statement is
     
    513499% \end{lstlisting}
    514500
    515 The conditions we are going to present now are standard semantical commutation lemmas that are commonly
     501The conditions we are going to present now are standard semantic commutation lemmas that are commonly
    516502used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation.
    517503We will use $I,J\ldots$ to range over by statements. We will use $l_1,\ldots,l_n$ to range over by code point identifiers.
     
    519505over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by
    520506states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$
    521 the semantical relation, the call relation and the cost-label relation between states. These relations have
     507the semantic relation, the call relation and the cost-label relation between states. These relations have
    522508been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list
    523509of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is
     
    547533In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have
    548534to prove the following condition: for all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$,
    549 then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e. such that the following
     535then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e.\ such that the following
    550536diagram commutes.
    551537$$
     
    578564\begin{itemize}
    579565\item there are $s_2^{fin}$ and $s_2'$ such that $s_2 \stackrel{\pi_1(f\_step(COND \ r \ l))}{\longrightarrow} s_2^{fin}$,
    580 $s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2'$ and $s_1' \simeq_S s_2'$, i.e. the following diagram commutes
     566$s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2'$ and $s_1' \simeq_S s_2'$, i.e.\ the following diagram commutes
    581567$$
    582568\xymatrix{
     
    632618into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the
    633619following way. For all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then
    634 there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e. such that
     620there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e.\ such that
    635621the following diagram commutes.
    636622$$
     
    673659
    674660\paragraph{Commutation of call statement (\verb=call_commutation=).}
    675 For all $s_1,s_1',s_2$ such that $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and
    676 the statement fetched in the translated language at the program counter being in call relation
    677 with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$
     661For all $s_1,s_1',s_2$ such that we have $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and
     662the statement fetched in the target function at the program counter in call relation
     663with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL \ id' \ arg' \ dst'$
    678664for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that
    679665\begin{itemize}
     
    752738\paragraph{Commutation of return statement (\verb=return_commutation=).}
    753739For all $s_1,s_1',s_2$ such that $s_1 \stackrel{RETURN}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$, if $CALL \ id \ arg \ dst$
    754 is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier
     740is the call statement that caused the function call ened by the current return (i.e.\ it is the statement whose code point identifier
    755741is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are
    756742$s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$,
     
    818804
    819805\subsubsection{Conclusion}
    820 After having provided a semantic relation among states that satifies some conditions that correspond to
     806After having provided a semantic relation among states that satisfies some conditions that correspond to
    821807commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the
    822808general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=.
     
    843829    R init_in init_out.
    844830\end{lstlisting}
    845 The module formalizing the formal machienary we described in this document consists of about 3000 lines of
    846 Matita code. We stress the fact that this machienary proves general properties that do not depend on the
    847 specific backend graph compiler pass.
     831The module formalizing the formal machinery we described in this document consists of about 3000 lines of
     832\s{matita} code. We stress the fact that this machinery proves general properties that do not depend on the
     833specific back-end graph compiler pass.
  • Deliverables/D4.4/paolo.tex

    r3213 r3222  
    1111\usepackage{listings}
    1212\usepackage[all]{xy}
     13% \usepackage{supertabular}
    1314
    1415\newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}}
     
    6667\small Department of Computer Science and Engineering, University of Bologna\\
    6768\small \verb|\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it|}
    68 \title{Certifying the back end pass of the CerCo annotating compiler}
     69\title{Certifying the back-end pass of the CerCo annotating compiler}
    6970\date{}
    7071
     
    7273\maketitle
    7374\begin{abstract}
    74 We present the certifying effort of the back end of the CerCo annotating
    75 compiler to 8051 assembly. Apart from the usual effort needed in propagating
     75We present the certifying effort of the back-end of the CerCo annotating
     76compiler to 8051 assembly. Apart from the proofs needed for propagating
    7677the extensional part of execution traces, additional care must be taken in
    7778order to ensure a form of intensional correctness of the pass, necessary to
    78 prove the lifting of computational costs correct. We concentrate here on two
     79prove that the lifting of computational costs is correct. We concentrate here on two
    7980aspects of the proof: how stack is dealt with during the pass, and how generic graph
    8081language passes can be proven correct from an extensional and intensional point
     
    210211Care must be taken in dealing with the stack. The back-end pass produces a
    211212\emph{stack model}: the amount of stack needed by each function (\verb+stack_m+),
    212 together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals).
     213together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global variables).
    213214While programs in the front end do not fail for stack overflow, the stack
    214215information is lifted to source much in the same ways as time consumption information,
     
    364365\label{subfig:stacksame}
    365366\end{subfigure}
    366 \caption{Comparison between using tight stack sizes across langauges, i.e.\
     367\caption{Comparison between using tight stack sizes across languages, i.e.\
    367368reading how much stack is required from the function, and using the same
    368369stack sizes provided as a parameter to the semantics. We suppose the call stack
     
    382383
    383384\subsection{From an unbounded to a bounded stack}
    384 The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of
     385The way the \verb+ft_and_tlr+ is propagated is almost everywhere by means of
    385386the proof of existence of a special relation between states that is a simulation
    386387with respect to execution. There are more details involved than in a usual
     
    418419The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with
    419420a single, bounded stack space, where moreover memory has already been granted to
    420 globals too. From this semantics down to \s{LIN}, all data in memory excluding
     421global variables too. From this semantics down to \s{LIN}, all data in memory excluding
    421422pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}.
    422423However in order to show a
  • Deliverables/D4.4/report.tex

    r3213 r3222  
    1 \documentclass[11pt, epsf, a4wide]{article}
     1\documentclass[12pt]{article}
    22
    33\usepackage{../style/cerco}
     
    4747
    4848\begin{document}
    49 
     49\pagenumbering{roman}
    5050\thispagestyle{empty}
    5151
     
    9696
    9797\newpage
    98 
    99 \vspace*{7cm}
     98\addcontentsline{toc}{section}{Summary}
    10099\paragraph{Summary}
    101100The deliverable D4.4 is composed of the following parts:
     
    177176whole assembler.
    178177
    179 \includepdf[pages={-}]{itp2013.pdf}
    180 \includepdf[pages={-}]{paolo.pdf}
    181 \includepdf[pages={-}]{cpp-2012-asm.pdf}
    182 \includepdf[pages={-}]{cpp-2012-policy.pdf}
     178\includepdf[pages={-},addtotoc={1,section,1,Certification of the preservation of structure by a compiler's back-end pass,simulation}]{itp2013.pdf}
     179\includepdf[pages={-},addtotoc={1,section,1,Certifying the back-end pass of the CerCo annotating compiler,backend}]{paolo.pdf}
     180\includepdf[pages={-},addtotoc={1,section,1,On the correctness of an optimising assembler for the Intel MCS-51 microprocessor,asm}]{cpp-2012-asm.pdf}
     181\includepdf[pages={-},addtotoc={1,section,1,On the correctness of a branch displacement algorithm,policy}]{cpp-2012-policy.pdf}
    183182
    184183\end{document}
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2416 r3222  
    4242
    4343\begin{document}
     44\pagestyle{plain}
    4445
    4546\maketitle
  • Papers/itp-2013/ccexec.tex

    r3213 r3222  
    3131
    3232\begin{document}
     33\pagestyle{plain}
    3334
    3435\title{Certification of the Preservation of Structure by a Compiler's Back-end Pass\thanks{The project CerCo acknowledges the financial support of the Future and
Note: See TracChangeset for help on using the changeset viewer.