This PR adds fancy updates (i.e., global invariant accesses) between steps to the juicy semantics. This allows us to access global invariants at any time in a proof using viewshift_SEP, and removes the need for some previously Admitted lemmas in atomics/general_atomics. We can also use the Iris iInv tactic to interact with invariants in IPM.
Limitations:
Because of an extra step in the return operation in VST's semantics vs. CompCert's, we can't do fancy updates after a function call. This means that some fancy functions (e.g., allocating a lock invariant) might return their postconditions under a modality (that the caller can immediately remove using viewshift_SEP).
Unlike ghost-state updates, fancy updates have a major impact on the soundness proof. From a per-thread perspective, we may have hidden some of our memory permissions in an invariant, and then proved safety with the reduced permissions. To recover soundness, we need some new frame-style properties of external calls. These are:
Inline external calls can be run on memories with increased permissions, and ignore the increased permissions. This is a variant of CompCert's ec_mem_extends axiom, but with a much tighter relation than Mem.extends. It seems like we need this as an axiom at the top level, but maybe I'm missing something.
A full frame rule for juicy extspecs. We prove that all extspecs derived from VST funspecs satisfy this frame rule, so this shouldn't be a problem in practice.
Exit specs ignore increased permissions. Our exit specs so far are always True, so this is trivial in all current examples.
This PR adds fancy updates (i.e., global invariant accesses) between steps to the juicy semantics. This allows us to access global invariants at any time in a proof using
viewshift_SEP, and removes the need for some previouslyAdmittedlemmas inatomics/general_atomics. We can also use the IrisiInvtactic to interact with invariants in IPM.Limitations:
Because of an extra step in the return operation in VST's semantics vs. CompCert's, we can't do fancy updates after a function call. This means that some fancy functions (e.g., allocating a lock invariant) might return their postconditions under a modality (that the caller can immediately remove using
viewshift_SEP).Unlike ghost-state updates, fancy updates have a major impact on the soundness proof. From a per-thread perspective, we may have hidden some of our memory permissions in an invariant, and then proved safety with the reduced permissions. To recover soundness, we need some new frame-style properties of external calls. These are:
Inline external calls can be run on memories with increased permissions, and ignore the increased permissions. This is a variant of CompCert's
ec_mem_extendsaxiom, but with a much tighter relation thanMem.extends. It seems like we need this as an axiom at the top level, but maybe I'm missing something.A full frame rule for juicy extspecs. We prove that all extspecs derived from VST funspecs satisfy this frame rule, so this shouldn't be a problem in practice.
Exit specs ignore increased permissions. Our exit specs so far are always True, so this is trivial in all current examples.