[bitc-dev] Use Case: Atomicity

[David Hopwood]

Jonathan S. Shapiro wrote:
> In the Coyotos kernel, we have a loosely-defined property concerning
> atomicity. Informally:
> 
>   Every path has a commit point.
>   Before the commit point, no "semantically observable" mutating
>     operations are permitted.
>   After the commit point, no blocking is permitted.
> 
> The definition of "semantically observable" is a bit fuzzy, but the
> intuition is this: you can encache and decache things, and you can
> re-optimize the in-cache representation of certain structures, but you
> cannot do anything that modifies the conceptual system state.

This need not be fuzzy:

Build a cacheless implementation of the system. Prove that it satisfies the
above property with strictly no mutation of the system state before a commit
point.

Then, prove that the actual system is a data refinement of the cacheless system.
As long as the changes from the cacheless system to the actual system don't
introduce operations that can block, there is no need to redo the atomicity
proof.

-- 
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>