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

[Jonathan S. Shapiro]

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.

So I have been trying to capture a description of what it means to be a
semantically significant change.

This evening, I think I came up with an answer, and I want to capture
it.

  A semantically significant change is one where the result of taking
  a checkpoint *before* the operation would differ from the result of
  taking a checkpoint *after* the operation.

Given this definition, it seems plausible that we might define a
semantically mutating operation as:

   (define (mutating-op op state)
      (let ((old-state (deep-copy state)))
        (do-op op state)
        (not (equal (checkpoint-image old-state)
                    (checkpoint-image state)))))

Since the YIELD operation is modeled as an exception, we can capture the
intended property as:

  (define (do-op-with-yield op state)
    (let* ((yielded false)
           (result (try (do-op op state)
                        (catch e (otherwise (set! yielded #t)
                                            state)))))
      (pair yielded state)))

  (defthm yield-implies-no-change
    (forall (op state)
    (implies (valid-state state)
             (let* ((state (deep-copy state))
                    ((yielded, new-state) (do-op-with-yield op state)))
               (or (not yielded)
                   (equal (checkpoint-image state)
                          (checkpoint-image new-state))))))

Provisionally, I *think* this captures the property we are after for
atomicity. I have absolutely no idea whatsoever if there is any hope of
discharging this property, and there is probably a simpler way to
capture it. Mostly, I wanted to capture the intuition before my tired
brain declared collapse for the evening.


shap