Add sorted_ipc_queues invariant
#836
Conversation
michaelmcinerney
force-pushed
the
michaelm-sorted_ipc_queues
branch
2 times, most recently
from
3e285fe to
9e82e28
Compare
michaelmcinerney
added
the
MCS
| zprios' \<leftarrow> return $ filter (\<lambda>(_, p). p \<ge> prio) zprios | ||
| @ [(tptr, prio)] | ||
| @ filter (\<lambda>(_, p). p < prio) zprios; | ||
| return (map fst zprios') | ||
| od" |
There was a problem hiding this comment.
comprehension nitpick: if it's placing the tptr into a list such that it's sorted, does it still make sense to call it "append" without comment?
There was a problem hiding this comment.
Good point, it'd be more like an insert. I suspect the name hasn't changed in C either, but we could still do better in the specs.
| apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp) |
There was a problem hiding this comment.
if you had a lifting lemma for valid_sched_pred_strong, you could apply that here and then wp most of the conditions away; the hoare_lift_Pf way looks a bit uphill and happens 3 times in this file, so presumably also on RISCV64
| lemma set_pt_prios_of[wp]: | ||
| "set_pt ptr pt \<lbrace>\<lambda>s. P (prios_of s)\<rbrace>" | ||
| by (set_object_easy_cases def: set_pt_def) | ||
|
|
||
| lemma set_pd_prios_of[wp]: | ||
| "set_pd ptr pd \<lbrace>\<lambda>s. P (prios_of s)\<rbrace>" | ||
| by (set_object_easy_cases def: set_pd_def) |
There was a problem hiding this comment.
We should be proving P (tcbs_of s) here (and wherever we can), because that's the more general case that includes prios_of and all other tcb projections.
| for eps_of[wp]: "\<lambda>s. P (eps_of s)" | ||
| and ntfns_of[wp]: "\<lambda>s. P (ntfns_of s)" | ||
| and prios_of[wp]: "\<lambda>s. P (prios_of s)" |
There was a problem hiding this comment.
Since these 3 always occur together: I wonder if there is a combinator that we could build so that we only have to prove one lemma and then apply a rule or something else that is automatic to get all three together. Not for this PR, but in general for projections.
There was a problem hiding this comment.
(No action necessary for this, but if someone has an idea, do let me know)
| apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp) |
There was a problem hiding this comment.
oo, another candidate for that lifting rule
| apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp) |
| apply (rule hoare_lift_Pf2[where f=ntfn_queues_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf2[where f=prios_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf2[where f=eps_of, rotated], wpsimp) | ||
| apply (rule hoare_lift_Pf2[where f=ntfns_of, rotated], wpsimp) |
| @@ -26550,6 +27301,7 @@ lemma call_kernel_valid_sched: | |||
| \<and> cur_sc_offset_sufficient (consumed_time s) s\<rbrace> | |||
| call_kernel e | |||
| \<lbrace>\<lambda>_. valid_sched :: det_state \<Rightarrow> _\<rbrace>" | |||
| supply comp_apply[simp del] | |||
There was a problem hiding this comment.
I would like to take this opportunity to express concern at the size of DetSchedSchedule_AI on rt. My browser took longer than my tea does to brew in order to open this file's diff for review.
|
I like how you structured the proof of this invariant, and the way the asserts are lining up and not polluting Refine works out well. I didn't spot anything style-wise, and also appreciated where you pointed out a bunch of lemmas were moved. I think the outstanding non-minor issues from my side are:
|
michaelmcinerney
force-pushed
the
michaelm-sorted_ipc_queues
branch
from
9e82e28 to
5b6e657
Compare
|
I think I have addressed most of what we would like to change for this PR, with the exception of renaming |
Fine to do separately. Don't forget to make the issue for the misc/lifting/hoare_liftPf situation if you haven't already. Someone should double-check the squashed commits once they're squashed, but from my side this looks good. |
|
Here's my issue for the heap projections: #841 |
|
And nice job on resolving the |
Done in order to avoid unwanted interactions with comp_apply Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Done in order to avoid unwanted simplification of heaps which are defined via multiple uses of opt_map_Some Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This rule is no longer needed, now that opt_map_Some is not defined in terms of comp Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This adds the invariant sorted_ipc_queues, which states that the ipc queues are sorted by the priority of the TCB. More specifically, the queues are nonincreasing with respect to the priority of the TCB. This additionally uses the filter operation in the specification of tcb_ep_append and tcb_ep_dequeue. Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-sorted_ipc_queues
branch
from
747ada7 to
6e00090
Compare
|
I've force pushed to update this PR so that it now consists of the commits from #845 ("Some changes for |
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-sorted_ipc_queues
branch
from
6e00090 to
bff057f
Compare
Please see the commit messages for what is here. It might be best to review the files in the order in which they would appear in jedit. So for example, AInvs before Refine, and earlier files in AInvs before later files in AInvs.
As usual, there are many lemmas that we may want to move up, or to have in
master, and I would be happy to do that. I have moved many of the lemmas around, and I'll try to indicate them with comments. The diff is not very accurate, and some of what appears as green or red isn't anything I have actually touched.I'll try some things out to hopefully reduce the number of times I remove
comp_applyfrom the simp set.I have weakened
valid_ep'andvalid_ntfn'by removing some of the properties that can be crossed from the abstract state analogues. This was done because proving distinctness was a bit of a pain with the ordered insert. So I have added some asserts in the Haskell for distinctness of these queues.