rt crefine: prove several lemmas related to the endpoint and ntfn queues#992
Conversation
michaelmcinerney
requested review from
Xaphiosis,
corlewis and
lsf37
and removed request for
corlewis
michaelmcinerney
added
the
MCS
| apply (rule ccorres_symb_exec_l) | ||
| defer |
There was a problem hiding this comment.
can we reorder the proof to avoid the defer (another one a bit further down) or is the ordering necessary for instantiating something?
There was a problem hiding this comment.
This is a copy paste job from the other kernel objects that have analogous rules. I could fix this one up, but they're all exactly the same. Should I just do this one or do them all? The ccorres_lemma2/3/4 proofs are probably just as bad for all the kernel objects.
There was a problem hiding this comment.
Have a look if it is actually possible. It might be that the wp needs to instantiate the precondition first. If it is possible, we would ideally do all of them before we start porting to other architectures.
There was a problem hiding this comment.
For after I’ve figured out if it can be improved, should I do this for all the kernel objects in a separate cleanup PR? Or just for the new lemmas I’ve added here within this PR?
There was a problem hiding this comment.
As long as we end up with all of them being cleaned up, I don't mind which way.
There was a problem hiding this comment.
given that it's a ccorres_symb_exec_l with two rules taking out two slots, ccorres_symb_exec_l[OF ... get_ep_sp' getEndpoint_empty_fail, rotated ???] or something like that might do it? I agree that the double-defer is yuck
| apply (rule ccorres_symb_exec_l) | ||
| defer |
There was a problem hiding this comment.
same as the other one: would a reorder be possible to avoid the defer?
| apply assumption | ||
| apply (clarsimp simp: cendpoint_relation_def Let_def tcb_queue_relation'_def) | ||
| \<comment> \<open>non-empty case\<close> | ||
| apply (prop_tac "epptr = epptr AND NOT (mask 4)") |
| (tcb_at' thread and valid_objs' and no_0_obj' and pspace_canonical' | ||
| and pspace_aligned' and pspace_distinct' and ep_at' epptr and valid_bound_reply' replyOpt | ||
| and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) | ||
| and K (epptr = epptr && ~~ mask 4) |
There was a problem hiding this comment.
here is 4 again. Would be good to give this a symbolic name. Sounds like ep_bits alignment or similar. When we're porting this to other architectures, the number will change and it will be annoying to update.
| apply (rule ccorres_symb_exec_l'[OF _ _ stateAssert_sp]; (solves wpsimp)?)+ | ||
| apply (rule ccorres_symb_exec_l'[OF _ _ isRunnable_sp]; (solves wpsimp)?) | ||
| apply (rule ccorres_symb_exec_l'[OF _ _ assert_sp]; (solves wpsimp)?) | ||
| apply (rule ccorres_symb_exec_l'[OF _ _ stateAssert_sp]; (solves wpsimp)?)+ | ||
| apply (rule ccorres_symb_exec_l'[OF _ _ get_ntfn_sp']; (solves wpsimp)?) |
There was a problem hiding this comment.
I'm tempted to wrap this up into a method that tries various ccorres_symb_exec_l'[OF _ _ X]; solves wpsimp for a specific set of rules X. Would that make sense? It's not always going to work, but it could work often enough to be useful.
There was a problem hiding this comment.
That would make sense. It would be a ccorres analogue of the oft-mentioned sp method for Hoare triples.
I think I sometimes have to add an extra unfolding K_bind_apply or something to get it working.
I really like this approach, personally. I think when I first started to use it, you were sceptical because you didn’t want to mess with things before the first cinit but I’m always careful to use unfolding or simp only:.
There was a problem hiding this comment.
Yes, as long as we keep it to a controlled rule ccorres_symb_exec_l' and (solves ..)? it's safe to use. One more reason to wrap it up into a method -- makes it easier to keep the common case safe :-)
The method doesn't have to cover all cases, just most or even just many. I'm not sure if that works, but it's possible that we can even have a named_theorems set for the set of things to try.
There was a problem hiding this comment.
Should we merge this PR, and then I can write a little method and use it wherever we have this pattern? It would be used in many other places than in just this PR.
There was a problem hiding this comment.
Would definitely be nicer to review the tech and the improvement it represents separately from this PR.
There was some discussion on mattermost, I suggested "something like ccorres_symb_exec_l_pre
which is kinda long, but describes what it intends (preliminary execution of easy stuff on the left). We can probably abbreviate it to ccorres_exec_l_pre since we are extremely unlikely to have any other form of execution"
Also discussion yielded that ccorres_symb_exec_l'[OF _ _ X] can't take a set for X, but with suitable rotation something like X[THEN ccorres_symb_exec_l'] might work.
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Very nice! This could have been multiple 10k lines of new terrible proof, instead it solves a whole bunch of sorries and deletes about 2k lines of previous proof. Some of the IPC proofs are still very large, but there's no way around the additional MCS complexity there that I see.
| "ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') | ||
| (invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' ((=) Restart) | ||
| and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) | ||
| and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) |
There was a problem hiding this comment.
I'm curious, do you recall where this weakening came from? It looks like an improvement
There was a problem hiding this comment.
My guess is that I added sch_act_wf during the initial sorrying run and then realised much later that weak_sch_act_wf is all we need most of the time. The extra information in sch_act_wf can all be crossed. Crossing weak_sch_act_wf is annoying because we don't quite have enough in the abstract guards of the corres rules to make it seamless. So it's one of the few things I have to carry around everywhere. Luckily it's very basic so it can be crunched most of the time.
| apply (simp only: cross_valid_tcbs'_def) | ||
| apply (rule cthread_state_rel_imp_eq) | ||
| apply (drule_tac x=p in spec)+ | ||
| apply (drule_tac x=atcb' in spec)+ | ||
| apply (fastforce simp: map_comp_def) | ||
| apply (drule_tac x=p in spec)+ | ||
| apply (drule_tac x=atcb in spec)+ | ||
| apply (fastforce simp: map_comp_def) |
There was a problem hiding this comment.
It's hard to tell from just the proof text but is this working through the quantifiers in cross_valid_tcbs'? If it is, then maybe there could be a dest rule that wraps it up and makes it easier to use.
There was a problem hiding this comment.
The problem with all of these uniqueness lemmas is that they have things like map_to_tcbs for the two Haskell states, and it messes with unification a lot. I can't get a nice dest rule working here.
|
|
||
| lemmas updateNotification_ccorres_lemma3 = updateNotification_ccorres_lemma4[where R=UNIV] | ||
|
|
||
| lemmas updateNotification_ccorres_lemma2 = updateNotification_ccorres_lemma3[where P'=\<top>] |
There was a problem hiding this comment.
hehehehe, 3 comes before 2 (and 2 comes from 3?)
There was a problem hiding this comment.
Descending into hell.
| \<and> tcb_queue_head_end_valid q' s" | ||
| and Q="\<lambda>s ntfn. {s'. (s, s') \<in> rf_sr \<and> ko_at' ntfn ntfnPtr s | ||
| \<and> pspace_canonical' s \<and> tcb_queue_head_end_valid q' s}" | ||
| in updateNotification_ccorres_lemma3[where P=\<top>]) |
There was a problem hiding this comment.
I think this exact instantiation occurs three times, might be worth naming it. while the rest of the proof also looks like it has duplication, it doesn't seem so easy to resolve
|
|
||
| lemmas updateEndpoint_ccorres_lemma3 = updateEndpoint_ccorres_lemma4[where R=UNIV] | ||
|
|
||
| lemmas updateEndpoint_ccorres_lemma2 = updateEndpoint_ccorres_lemma3[where P'=\<top>] |
There was a problem hiding this comment.
do you not find this countdown strange to read?
There was a problem hiding this comment.
Yes these lemmas are very annoying, and we have them for TCBs, sched contexts, replies, endpoints, and notifications. So you kind of get used to them, but with all the various schematics, they're still frustrating.
There was a problem hiding this comment.
I think the question was more why is 3 coming before 2 :-)
There was a problem hiding this comment.
I have no idea what the person who wrote the original threadSet_corres_lemma4/3/2 was thinking. Maybe they thought that the higher numbers are more specialised and would be used less often. But then there's no 1 or lemma without a number, so I really don't know.
There was a problem hiding this comment.
It's Ok, let's leave these for a later cleanup. I think at that point, the numbers don't really mean anything any more apart from "one more variant".
| \<and> tcb_queue_head_end_valid q' s" | ||
| and Q="\<lambda>s endpoint. {s'. (s, s') \<in> rf_sr \<and> ko_at' endpoint epPtr s | ||
| \<and> pspace_canonical' s \<and> tcb_queue_head_end_valid q' s}" | ||
| in updateEndpoint_ccorres_lemma3[where P=\<top>]) |
There was a problem hiding this comment.
as before, same instantiation 3 times
There was a problem hiding this comment.
If we didn't already have a whole bunch of names with various numbers for the instantiations, I'd go ahead and make one. But maybe making another one would just be confusing things more.
There was a problem hiding this comment.
You could use notes to confine it to only the one lemma, using something other than numbers, i.e.
lemma foo:
notes moo = refl[of True] (* the local instantiation or common part of it *)
shows "True = True"
apply (rule moo)
done
There was a problem hiding this comment.
This particular instantiation is used in more than one proof, so I'm not sure what to do. Should I make a lemma2'? I think it would just be making things worse.
| simp: list_queue_relation_def queue_end_valid_def) | ||
| apply normalise_obj_at' | ||
| apply (fastforce dest: ko_at'_threadRead[where f=tcbPriority]) | ||
| apply (fastforce dest: ko_at'_threadRead[where f=tcbPriority]) |
There was a problem hiding this comment.
another proof which could use some comment markers
| \<and> weak_sch_act_wf (ksSchedulerAction s) s | ||
| \<and> ksCurDomain s \<le> maxDomain | ||
| \<and> pspace_aligned' s \<and> pspace_distinct' s | ||
| \<and> pspace_bounded' s \<and> pspace_canonical' s" |
There was a problem hiding this comment.
these post_imps are very repetitive; I think the first two are the same, and then the third one has a pspace_canonical' s added? This section of this proof doesn't have much commentary, but it feels like this should be compressible somehow. If not, at least some comments saying what's going would help (e.g. why is pspace_canonical appearing on iteration 3?).
There was a problem hiding this comment.
Actually, one of these can be removed very easily, and the two that remain aren't so similar. I can't see a nice way of improving it further.
| apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend) | ||
| apply (clarsimp simp: option_to_0_def) | ||
| apply (cases replyOpt; clarsimp) | ||
| apply (prop_tac "ptr_val (replyPtr_' s') = ptr_val (replyPtr_' s') && ~~ mask 4") |
| and val="case epState ep of | ||
| IdleEPState \<Rightarrow> scast EPState_Idle | ||
| | ReceiveEPState \<Rightarrow> scast EPState_Recv | ||
| | SendEPState \<Rightarrow> scast EPState_Send" |
There was a problem hiding this comment.
this looks like a from_H analogue to a to_H, might be worth considering a definition although I only recall seeing this direction once so far
| apply (vcg exspec=thread_state_ptr_get_blockingIPCBadge_modifies) | ||
| apply wpsimp | ||
| apply (wpsimp wp: gts_wp') | ||
| apply wpsimp |
There was a problem hiding this comment.
this proof needs markers to follow what's going on; it's clearly going through a bunch of chunks but I am unable to follow what they are
| apply (rule ccorres_pre_threadGet) | ||
| apply (rule ccorres_move_c_guard_tcb) | ||
| apply (clarsimp simp: when_def) | ||
| apply (rule ccorres_if_lhs) |
There was a problem hiding this comment.
I'm lost. the old proof had comments about waiting case etc. In this one, I don't know what the steps/branches are
There was a problem hiding this comment.
This does have idle/active/waiting markers in it. Except now in MCS, there are excruciatingly long blocks where we call all sorts of fun functions like maybeDonateSc and refillIUnblockCheck. This occurs in both idle and waiting branches, though there doesn't seem to be a nice way to consolidate the branches.
| lemma ep_SendEPState_split: | ||
| "(case epState ep of SendEPState \<Rightarrow> f | _ \<Rightarrow> g) = (if epState ep = SendEPState then f else g)" |
There was a problem hiding this comment.
I think there's a few rules being added like this. Is there nothing more abstract that can be done or a more generic split rule that can be used? It might not be quite what you want but is EPState.case_eq_if useful at all?
There was a problem hiding this comment.
I couldn't find EPState.case_eq_if, and while there is endpoint.case_eq_if, I'm not sure that will work.
It's a bit of a tradeoff with these special split rules. They're a bit of a nuisance to state and to have several variants of, but they do reduce duplication in the proofs considerably. I thought this was the better choice to make overall.
There was a problem hiding this comment.
Oh and because SendEPState is a constructor in the case expression (it says notation: pattern "case") I don't think it can be made more general, unfortunately.
There was a problem hiding this comment.
Yes, I don't think you can write a general rule about this (because of how case works). You could make a plugin for the datatype package to prove such rules automatically, but that's about as good as you can get I think.
corlewis
left a comment
corlewis
left a comment
There was a problem hiding this comment.
Like others have said, great job getting all of this to come together so nicely! It's very nice to see so much able to be removed here and thanks for all of the cleanup you've done along the way!
| apply (prop_tac "epptr = epptr AND NOT (mask 4)") | ||
| \<comment> \<open>this magic number 4 is coming from thread_state_ptr_set_tsType_spec\<close> |
There was a problem hiding this comment.
Is this really true? We're making an epptr here and we're doing a AND NOT (mask ..), which is an alignment constraint, not a size constraint. This does not look like it is coming out of thread_state.
(This is the one I was thinking about for epSizeBits)
There was a problem hiding this comment.
I thought these were coming out of the helper lemmas for setThreadState. I'll double check
There was a problem hiding this comment.
It might still come out of a thread_state if the ep_ptr was stored in the thread state. But in that case the alignment constraint would be from tsSize, but from whatever field stored the pointer (and in that case epSizeBits would be the right one to use, even that's not a name from C)
| K (epptr = epptr && ~~ mask 4)) | ||
| \<comment> \<open>this magic number 4 is coming from thread_state_ptr_set_tsType_spec\<close> |
There was a problem hiding this comment.
same here, I don't think this comes out of thread_state. It might be an ep_ptr that was stored in a thread state before, but the constraint would not be from tsType.
| apply (prop_tac "replyPtr = replyPtr && ~~ mask 4") | ||
| \<comment> \<open>this magic number 4 is coming from thread_state_ptr_set_tsType_spec\<close> |
There was a problem hiding this comment.
also unlikely to be from thread_state_ptr_set_tsType_spec (but maybe another thread state lemmas). In this case it'd be something about the size of replies (because it's against an alignment constraint).
| apply (prop_tac "ptr_val (replyPtr_' s') = ptr_val (replyPtr_' s') && ~~ mask 4") | ||
| \<comment> \<open>this magic number 4 is coming from thread_state_ptr_set_tsType_spec\<close> |
| and pspace_aligned' and pspace_distinct' and K (ntfnptr = ntfnptr && ~~ mask 4)) | ||
| \<comment> \<open>this magic number 4 is coming from thread_state_ptr_set_tsType_spec\<close> |
There was a problem hiding this comment.
for this one we should use ntfnSizeBits
Xaphiosis
left a comment
Xaphiosis
left a comment
There was a problem hiding this comment.
The queue overhaul worked out. Big thumbs up.
Prove - cancelAllIPC_ccorres - cancelAllSignals_ccorres - sendIPC_ccorres - receiveIPC_ccorres - receiveSignal_ccorres - setPriority_ccorres and remove several sorries that are no longer relevant. Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-ipc_queues_crefine
branch
from
481d016 to
46b3871
Compare
4 participants
This is the final PR for the work related to the new handling of the endpoint and notification queues, and includes proofs for many sorries (and removing several others that are no longer relevant), bringing the sorry count for MCS CRefine down to 4. The previous PRs are #978 (for ASpec + AInvs) and #986 (for Haskell + Refine).
I would recommend reviewing the files in the order in which they would appear in the Isabelle session.
Please see the C branch linked below for the associated changes for the C. The branch is the branch used for the seL4 PR for the IPC queues changes, seL4/seL4#1576, and then includes two already merged commits for
suspendandscheduleTCB, and finally has another commit for some small refactors. I will make a PR for the final commit once we're happy with this PR.Test with: seL4/seL4@michaelm/ipc_queues_mcs_testing
The following is from the commit message:
Prove
and remove several sorries that are no longer relevant.