Hello, I’m trying to get a better understanding of the refinement proof strategy taken in sel4. In Section 2.1: Forward Simulation, the fw-sim statement contains the following clause:
∧ (∀event. Step C event O SR ⊆ SR O Step A event)
where SR is a state relation between the internal states of the abstract and executable specification processes. My question is, why is this necessary when the Fin function of each process maps their internal state to a common external state that can be compared for equality?
I found this surprising, since the process definitions specifically have a Fin function which means that they effectively share a state space to an outside observer. Can correctness be specified only in terms of the 'external state, or is looking at the internal states necessary for some other reason?
The main thing to consider for these definitions is that forward simulation is not the definition of correctness: refinement is the definition of correctness, and forward simulation is the proof technique we use to show refinement.
There are two main equivalent characterisations of refinement for sequential programs (it gets more complicated for concurrent ones): a) A refines B iff the behaviours of A are a subset of the behaviours of B (where behaviour is a relation), and b) A refines B iff all Hoare triples that hold on B also hold on A. The second one is the one that is really the point of it all, because it allows us to prove things about the implementation by proving them on the simpler specification instead.
These definitions use equality on the external/visible state.
Both definitions are hard to establish directly. Forward simulation is easier to show, and it implies refinement. You can formulate it on just the external states with equality, and it will most likely still imply refinement, but it is less useful as a proof technique, because the relation on internal states is what makes it inductive, and the property of being inductive lets us pull apart whole executions into single execution steps, proving them in isolation.
I see, so it’s more of an aid to the actual proof effort than strictly required for correctness. That makes sense.