[coyotos-dev] Pinning down "semantically observable mutation"

[Norman Hardy]

Here are some notes on the issue that Shap raises below. <http://cap- 
lore.com/CapTheory/KK/Kernel/FormSem.html>
I doubt they will suit the style of his plans, but they do address  
some real problems to a degree.
All formal systems are fuzzy (frayed?) at the edges. Even in  
mathematics.

On May 26, 2006, at 6:34 PM, Jonathan S. Shapiro wrote:

> As many of you will come to realize (and some to regret), one  
> thrust of
> Coyotos is to try to make our statements of system properties more
> rigorous so that we can verify them.
>
> I have been struggling with one property that (so far) we have only
> captured informally: the idea of a "semantically observable mutation".
> We need to define this to check the atomicity of system calls. The
> general idea is that you aren't supposed (conceptually) to change the
> system state before the commit point. The problem is that, in  
> practice,
> you *do* change the system state: all manner of cache state changes
> before the commit point. Capabilities get prepared, objects get  
> loaded,
> and so forth.
......