Add acknowledgments

1 files changed, 5 insertions, 1 deletions

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}