diff options
| author | John Wickerson <j.wickerson@imperial.ac.uk> | 2022-01-17 21:47:28 +0000 |
|---|---|---|
| committer | node <node@git-bridge-prod-0> | 2022-01-17 21:47:55 +0000 |
| commit | cf6235faa110ef26a0a3e7c846c0767134d5f502 (patch) | |
| tree | ee5df2c58de68b0685a3deaccad1c1fe3768cce0 | |
| parent | 0e191c994b3227903080a9bd5207e839be14c1f7 (diff) | |
| download | fccm22_rsvhls-cf6235faa110ef26a0a3e7c846c0767134d5f502.tar.gz fccm22_rsvhls-cf6235faa110ef26a0a3e7c846c0767134d5f502.zip | |
Update on Overleaf.
| -rw-r--r-- | verified_resource_sharing.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index cb29d75..c0650ce 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -110,7 +110,7 @@ The entire \vericertfun{} development is fully open-source~\cite{vericertfun-git \paragraph{The Coq proof assistant} \vericert{} is implemented using the Coq proof assistant~\cite{coq}. This means that it consists of a collection of functions that define the compilation process, together with the proof of a theorem stating that those definitions constitute a correct HLS tool. Coq mechanically checks this proof using a formal mathematical calculus, and then automatically translates the function definitions into OCaml code that can be compiled and executed. -Engineering a software system within a proof assistant like Coq is widely held to be the gold standard for correctness. Recent years have shown that it is feasible to design substantial pieces of software in this way, such as database management systems~\cite{malecha+10}, web servers~\cite{chlipala15}, and operating system kernels~\cite{gu+16}. Coq has also been successfully deployed in the hardware design process, both in academia~\cite{braibant+13, bourgeat+20} and in industry~\cite{silveroak}. It has even been applied specifically to the HLS process: Faissole et al.~\cite{faissole+19} used it to verify that HLS optimisations respect dependencies present in the source code. +Engineering a software system within a proof assistant like Coq is widely held to be the gold standard for correctness. Recent years have shown that it is feasible to design substantial pieces of software in this way, such as database management systems~\cite{malecha+10}, web servers~\cite{chlipala15}, and operating system kernels~\cite{gu+16}. Coq has also been successfully deployed in the hardware design process, both in academia~\cite{braibant+13, bourgeat+20} and in industry~\cite{silveroak}. It has even been applied specifically to HLS: Faissole et al.~\cite{faissole+19} used it to verify that HLS optimisations respect dependencies in the source code. \paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is the CompCert project~\cite{compcert}. CompCert is a lightly optimising C compiler, with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures~\cite{six+20}, that has been implemented and proven correct using Coq. CompCert accepts most of the C99 language, and generally produces code of comparable performance to that produced by GCC at optimisation level \texttt{-O1}. It transforms its input through a series of ten intermediate languages before generating the final output. This design ensures that each individual pass remains relatively simple and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of its passes. |