Update on Overleaf.

1 files changed, 4 insertions, 1 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index d08d373..5860a00 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -398,7 +398,10 @@ In more detail: Execution begins in state 9 of the \lstinline{main} machine, and
 
 The same sequence of events can also be understood using a timing diagram, as given in Figure~\ref{fig:timingdiagram}. In that diagram, the red lines indicate unspecified values. We see that each call of \lstinline{add} begins with a pulse on \lstinline{add.rst} (fifth waveform) and ends with a pulse on \lstinline{add.fin} (sixth waveform).
 
-One technical challenge we encountered in the implementation of \vericertfun{} has to do with the fact that the caller and callee state machines modify each other's variables. This is problematic because each function is translated into a state machine independently, and hence the variable names used in the other state machines are not necessarily fixed yet. We work around this problem by introducing an additional ... \JW{TODO: finish explaining externctrl.}
+One technical challenge we encountered in the implementation of \vericertfun{} has to do with the fact that the caller and callee state machines modify each other's variables. This is problematic because each function is translated into a state machine independently, and hence the register names used in the other state machines are not necessarily available. We work around this problem by introducing an additional component to our state machines: a mapping, called \lstinline{externctrl}, that maps local register names to pairs of module identifiers and register names in those modules. Once all the state machines have been generated, we erase \lstinline{externctrl}. We do this in two steps. First, we perform a renaming pass through
+the whole program, making all register names globally unique. This is necessary to avoid
+unintended conflicts between register names in different modules, as register names can only be assumed to be unique within their own module. We then do a second pass, renaming
+registers present in \lstinline{externctrl} to the name of the register they target. \JW{Maybe add an example of what the externctrl map would be for the worked example?}
 
 \JW{Explain the assumption made about no pointers in called functions.}