Vp should never happen, since you'd never preserve a V page. And surely
it would be Pr -> Sr, since the hypervisor wouldn't push the page to
backing store when you change the client state.
Well, you implicitly see the hypervisor state. If you touch a [UV]z
page then you get a fault telling you that the page has been taken away
from you (I think). And it would definitely help with debugging (seems
likely there's lots of scope for race conditions if you prematurely tell
the hypervisor you don't need the page any more...).
Yes, there's no way I'd be able to get my head around this otherwise.
BTW, here's an updated one with the host-driven events as dashed lines,
and a couple of extra transitions I think should be in there (but
waiting for Martin's confirmation).
J