[bitc-dev] Use Case: Atomicity

[Jonathan S. Shapiro]

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.

Let me wave my hands for a moment, and assume that we can figure out how
to define a predicate

	(MODIFIES-SYSTEM-STATE-P some-ast)

Then the property of interest can be described as a control-flow model
checking property:

   Initial state: *good*
     transition-to: *bad* if (MODIFIES-SYSTEM-STATE-P cur-ast)
     transition-to: *post-commit* if (IS-COMMIT-AST cur-ast)
     else transition-to *good*

   State: *bad*
     terminal FAIL

   State: *post-commit*
     terminal OK
     transition-to: *bad* if (SLEEPS-P cur-ast)
     else transition-to *post-commit*

This is the kind of property that MOPS could be used to check if it
offered user-extensible predicates on ASTs. This would have been a
difficult extension for MOPS, but it isn't all that hard for us.

The idea here is that

  MODIFIES-SYSTEM-STATE-P
  IS-COMMIT-AST

are predicates on ASTs, and the test problem is being solved using
abstracted execution over the AST.


shap