From a38481d9943482e42ba4cc5cc409969786f5a6d2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 31 Mar 2022 12:11:46 +0100 Subject: Add acknowledgments --- verified_resource_sharing.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index 9933ae8..4c403fc 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -300,7 +300,7 @@ int main() \end{figure} -Figure~\ref{fig:example_3AC} shows the 3AC representation of that C program, as obtained by the CompCert frontend. We see two CFGs, one per function. The control flow in this example is straightforward, but in general, 3AC programs can contain unrestricted gotos. The nodes of the CFGs are numbered in reverse, as are the parameters of the \lstinline{add} function, following CompCert convention. +Figure~\ref{fig:example_3AC} shows the 3AC representation of that C program, as obtained by the CompCert frontend. We see two CFGs, one per function. The \YHchanged{control-flow} in this example is straightforward, but in general, 3AC programs can contain unrestricted gotos. The nodes of the CFGs are numbered in reverse, as are the parameters of the \lstinline{add} function, following CompCert convention. Figure~\ref{fig:example_HTL} depicts the result of converting those CFGs into two state machines. The conversion of 3AC instructions into Verilog instructions has been described already by \citet{vericert}; what is new here is the handling of function calls, so the following concentrates on that aspect. Note that ``$*{\rightarrow}\langle\mathit{node}\rangle$'' stands for edges from all nodes to $\langle\mathit{node}\rangle$. The solid edges within the two state machines indicate the transfer of control between states, while the dashed edges between the state machines are more `fictional'. The ground truth is that both state machines run continuously, but it is convenient to think that only one machine does useful work at a time. So, the dashed edges indicate when the `active' machine changes. @@ -516,6 +516,10 @@ The bottom graph compares the execution time. We observe that \vericertfun{} gen Our immediate priority is to complete \vericertfun's correctness proof. In the medium term, we intend to improve our implementation of resource sharing by dropping the requirement to inline functions that access pointers; we anticipate that this will lead to further area savings \JWchanged{and also allow \vericertfun{} to be evaluated on benchmarks with more interesting call graphs}. We would also like \vericertfun{} to generate designs with one Verilog module per C function, as this is more idiomatic than cramming all the state machines into a single module; we did not do this yet because it requires extending the Verilog semantics to handle multiple modules. \JWchanged{It would also be interesting to implement \emph{selective} inlining of functions~\cite{huang+15}, either guided by heuristics or by programmer-supplied pragmas. It is worth noting that having proven inlining correct in general, the amount of inlining performed can be adjusted without affecting the correctness proof.} In the longer term, we would like to combine resource sharing with operation scheduling, i.e. resource-constrained scheduling~\cite{sdc}. +\section*{Acknowledgments} + +This work was financially supported by the EPSRC via the Research Institute for Verified Trustworthy +Software Systems (VeTSS) and the IRIS Programme Grant (EP/R006865/1). \bibliographystyle{ACM-Reference-Format} \bibliography{references} -- cgit