\problemdata
{S00 ps4.5}
{state machine}
{cache}

\begin{problem}
%[[[New problem.  Needs solutions.  Needs formatting.  Needs
%proofreading, clarifying, etc.]]]
Cache management protocol $HybridCache$ is a hybrid of the two caching
protocols presented in Installment 2 of the notes on computational
processes.
$HybridCache$ maintains a memory and two caches, as before.
Only now, an update to memory causes the value to be cleaned out of
cache1 but not out of cache2.
The intent is that cache2 is allowed to be out-of-date, but cache1 is
not.

\begin{problemparts}

\problempart
Model $HybridCache$ carefully as a state machine.

\solution{


\begin{description}
\item[$Q$:] $\{ (memory, cache1, cache2) \mbox{ of the types described in Lecture 8 handouts}\}$. \\
\item[$Q_0$:] memory is arbitrary, caches map everything to $\ms{null}$. \\
\item[$\delta$:] 
$(\ms{memory}, \ms{cache1}, \ms{cache2}) \rightarrow 
 (\ms{memory}', \ms{cache1}', \ms{cache2}')$ where all steps are the same as in Lecture 8 except
the memory update step:
\begin{description}
\item[1. ] 
$\ms{memory}(a) :=$ arbitrary $\ms{value}$ (not null). \\
$\ms{cache1}(a) := \ms{null}$ 
\end{description}
\end{description}

}

\problempart
State carefully an invariant saying that cache1 is always up-to-date. 

\solution{

Can show, in all reachable states either
$\ms{cache1}(a) = \ms{memory}(a)$ or 
$\ms{cache1}(a) = \ms{null}$ \\
\\
In other words: 
If $\ms{cache1}(a) \neq \ms{null}$ then $\ms{cache1}(a) =
\ms{memory}(a)$. \\

Note: No such guarantees are provided for cache2.

}

\problempart
Prove your invariant carefully using the Invariant Theorem.

\solution{
\begin{description}
\item[Start condition:] 
Everything in cache1 is null so the invariant is trivially true.

\item[Transition condition:] 
We show all possible transitions:
\begin{description}
\item[1. Memory Update: ] 
After this step, 
the only changed value is in cache1 and is changed to null. In this case, the Invariant holds 
trivially (they only need to match if cache1 holds a value other than null).
\item[2. Cache1 Update: ] 
The only changed value is in cache1 and is changed to match the one in memory. Invariant holds.
\item[3. Cache2 Update: ] 
Only cache2 changes. Since the Invariant makes no claims about cache2, the Invariant still holds.
\item[4. Cache1 Drop Value: ] 
The only changed value is in cache1 and is changed to null. In this case, the Invariant holds 
trivially.
\item[5. Cache2 Drop Value: ]
Same as 3.
\end{description}
\end{description}
}

\problempart
Now modify $HybridCache$ to a new $WrongHybridCache$ algorithm,
which is just like $HybridCache$ but includes one additional type of
step,
which allows anything to be copied from
cache2 to (the same address in) cache 1.
Model this new algorithm as a state machine.

\solution{

Same as in a. except for one additional transition:
\begin{description}
\item[6. ] 
$\ms{cache1}(a) := \ms{cache2}(a)$ 
\end{description}
}

\problempart
Give an execution of $WrongHybridCache$ that demonstrates that the
invariant is violated. 

\solution{
\begin{description}
\item[memory\_write(1)] 
$~$\\
$\ms{memory}(a) := 1$ \\
$\ms{cache1}(a) := null$ 

\item[cache1\_update()]
$~$\\
$\ms{cache1}(a) := 1$ 

\item[cache2\_update()]
$~$\\
$\ms{cache2}(a) := 1$ 

\item[memory\_write(2)]
$~$\\
$\ms{memory}(a) := 2$ \\
$\ms{cache1}(a) := null$ 

\item[cache2\_to\_cache1()]
$~$\\
$\ms{cache1}(a) := 1$ 

\end{description}

Now cache1 holds a different value than memory in entry a. 
}

\problempart
Identify precisely where your proof of the invariant for $HybridCache$
would break down if you applied it to $WrongHybridCache$.

\solution{

It would break down in trying to prove the transition holds through transition 6. 
Here it is not the case that the value in cache1 is always changed to either match memory
or be null. Cache1 can take on any value from cache2, and we have no guarantees that the value in
cache2 is up to date.

}

\end{problemparts}
\end{problem}

