Prove schedContext_donate_ccorres
#807
Conversation
michaelmcinerney
added
the
MCS
proof/refine/RISCV64/IpcCancel_R.thy
Outdated
| crunch schedContextDonate | ||
| for replies_of': "\<lambda>s. P (replies_of' s)" (* this interfers with list_refs_of_replies' *) | ||
| and scReplies_of[wp]: "\<lambda>s. P' (scReplies_of s)" | ||
| (simp: crunch_simps wp: crunch_wps) | ||
| (simp: crunch_simps wp: crunch_wps | ||
| rule: schedContextDonate_def[simplified updateSchedContext_def]) |
There was a problem hiding this comment.
This use of rule feels a little bit strange, is it to avoid proving the equivalent lemmas for updateSchedContext?
There was a problem hiding this comment.
Some of the changes in Refine are a bit of a hack job, yes. A bit of background...
I wanted to use updateSchedContext rather than setSchedContext because firstly, updateSchedContext does seem to be a better abstraction to use (where we get the sched context object and then immediately set it with a variant of the object we get) and second, we already have ccorres rules for updateSchedContext which are exact analogues of the preexisting rules for threadSet, and I wanted to just use those.
But updateSchedContext was only defined fairly late on in the Refine run, and it has quite different rules when compared with the rules for setSchedContext. For example, some of the updateSchedContext rules will use the opt_pred/opt_map style functions for heap access, rather than obj_at' style, and this causes the proofs to go haywire unless we just try to get it back into the original formulation. So sometimes I do properly update the proofs for this change, and other times I just try to get back what we had before. Maybe once the opt_pred style is the only style we have, we could make these clunky proofs nicer
There was a problem hiding this comment.
This could use at least a short comment then ("prefer X because Y", or "avoid X due to Y") or something like that. This kind of hidden knowledge is what makes proofs difficult to figure out / fix / update later, e.g. in the case you cited if we ever want to go forth and change to the opt_pred style.
There was a problem hiding this comment.
Right, that all makes sense, I actually just added an updateReply for that exact reason of it being nicer to work with.
I can definitely understand making the minimal change to keep the proofs working. A comment could be helpful if you can find a suitable spot for it.
There was a problem hiding this comment.
On second thoughts, I decided to go with writing the rule
lemma updateSchedContext_scReplies_of:
"(⋀sc. scReply (f sc) = scReply sc) ⟹ updateSchedContext scPtr f ⦃λs. P' (scReplies_of s)⦄"
and then adding that to the crunch instead. Hopefully that's a nicer approach
There was a problem hiding this comment.
Yeah, that's a lot nicer, I'm happy with that. Do you definitely need to add it to the crunch though? I would have guessed that it picked it up automatically.
There was a problem hiding this comment.
You're right, it's not needed in the crunch. After all these years, I thought it had to be in the wp for crunch to pick it up. I'll remove it
There was a problem hiding this comment.
crunch picks rules up in a variety of different ways, including if the rule is already in the wp set and solves the generated goal, or if it has the same name as what crunch would produce. The former is how it works when a rule is passed in via wp, the latter is why you don't need to do anything in this case.
There was a problem hiding this comment.
That's great to know, thanks!
| > setSchedContext scPtr (sc { scTCB = Just tcbPtr }) | ||
| > when (from == cur || action == SwitchToThread from) | ||
| > rescheduleRequired | ||
| > updateSchedContext scPtr (\sc -> sc { scTCB = Just tcbPtr }) |
There was a problem hiding this comment.
It was kind of unexpected to see a haskell update in a commit that says "prove ..." with no further elaboration. It looks like this is a rephrase to make the proof easier, but it still left me scratching my head for a bit as to what's going on.
There was a problem hiding this comment.
Yes, this is just a rephrase to make the proof easier. This is what's happening the vast majority of the time when I update the Haskell, which was written seemingly without any thought as to the Simpl that will be produced. I can add a bit to the commit message saying that it is just to make the proof easier
There was a problem hiding this comment.
Yes please. I think it's important knowledge that this is only a rephrase and not a bug fix or update to match the C.
michaelmcinerney
force-pushed
the
michaelm-schedContext_donate_ccorres
branch
from
8c212f9
to
8dd5dfe
Compare
|
Forced pushed in order to update the commit message |
This correctly uses option_to_ctcb_ptr for the fields of a scheduling context which are TCB pointers. As a result, several theorems in ADT_C have been strengthened, since we now need to know more about the location of TCBs within the kernel heap. Signed-off-by: Michael McInerney <[email protected]>
This includes a small change to the Haskell which rephrases schedContextDonate, while preserving semantics, in order to make the proof of the ccorres rule easier. Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-schedContext_donate_ccorres
branch
from
8dd5dfe
to
f93c50f
Compare
No description provided.