diff options
Diffstat (limited to 'chapters/background.tex')
| -rw-r--r-- | chapters/background.tex | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/chapters/background.tex b/chapters/background.tex index 7208050..19a8c15 100644 --- a/chapters/background.tex +++ b/chapters/background.tex @@ -213,15 +213,15 @@ of the compiler, meaning this method of proving algorithms correct ensures a cor \subsection{CompCert} -CompCert~\cite{leroy09_formal_verif_compil_back_end} is a formally verified C compiler written in -Coq~\cite{bertot04_inter_theor_provin_progr_devel}. Coq is a theorem prover, meaning algorithms -written in Coq can be reasoned about in Coq itself by proving various properties about the -algorithms. To then run these algorithms that have been proven correct, they can be extracted -directly to OCaml code and then executed, as there is a straightforward correspondence between Coq -and OCaml code. During this translation, all the proofs are erased, as they are not needed during -the execution of the compiler, as they are only needed when the correctness of the compiler needs to -be checked. With this process, one can have a Compiler that satisfies various correctness -properties and can therefore be proven to preserve the behaviour of the code. +\index{CompCert}CompCert~\cite{leroy09_formal_verif_compil_back_end} is a formally verified C +compiler written in Coq~\cite{bertot04_inter_theor_provin_progr_devel}. Coq is a theorem prover, +meaning algorithms written in Coq can be reasoned about in Coq itself by proving various properties +about the algorithms. To then run these algorithms that have been proven correct, they can be +extracted directly to OCaml code and then executed, as there is a straightforward correspondence +between Coq and OCaml code. During this translation, all the proofs are erased, as they are not +needed during the execution of the compiler, as they are only needed when the correctness of the +compiler needs to be checked. With this process, one can have a Compiler that satisfies various +correctness properties and can therefore be proven to preserve the behaviour of the code. CompCert contains eleven intermediate languages, which are used to gradually translate C code into assembly that has the same behaviour. Proving the translation directly without going through the @@ -237,13 +237,13 @@ allocation and making sure that the stack variables are correctly aligned. \subsubsection{CompCertSSA} -CompCertSSA is an extension of CompCert with an additional \SSA\ intermediate language. This -language enforces \SSA\ properties and therefore allows for many convenient proofs about -optimisations performed on this intermediate language, as many assumptions about variables can be -made when these are encountered. The main interesting porperty that arises from using \SSA\ is the -\emph{equational lemma}, stating that given a variable, if it was assigned by an operation that does -not depend on memory, then loading the destination value of that variable is the same as recomputing -the value of that variable with the current context. +\index{CompCertSSA}CompCertSSA is an extension of CompCert with an additional \SSA\ intermediate +language. This language enforces \SSA\ properties and therefore allows for many convenient proofs +about optimisations performed on this intermediate language, as many assumptions about variables can +be made when these are encountered. The main interesting porperty that arises from using \SSA\ is +the \emph{equational lemma}, stating that given a variable, if it was assigned by an operation that +does not depend on memory, then loading the destination value of that variable is the same as +recomputing the value of that variable with the current context. Given a well formed SSA program $p$, a reachable state $\Sigma\ s\ f\ \sigma\ R\ M$, a memory independent operation which was defined at a node $d$ as $\mono{Iop}\ \mathit{op}\ \vec{a}\ x\ n$ |