-
Notifications
You must be signed in to change notification settings - Fork 106
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Several sorries in IpcCancel_C
#789
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Cool. Happy to see more sorries melting away and somehow even Refine seems to have a lot of removed lines with this change.
Refine does seem to shrink most of the time I have to touch it. I often do add asserts and might need to strengthen an abstract guard as a result, but I am often able to remove lines by making proofs that were forwards backwards instead, or removing Hoare triples about properties that we no longer need, like |
08ea860
to
eecc6ee
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As Gerwin said, it's very nice to see more sorries disappear, along with Refine
being made a bit shorter. Thank you for also improving the style in a lot of places with your changes.
proof/refine/RISCV64/IpcCancel_R.thy
Outdated
@@ -3079,7 +3037,7 @@ lemma ct_not_in_ntfnQueue: | |||
|
|||
lemma sch_act_wf_weak[elim!]: | |||
"sch_act_wf sa s \<Longrightarrow> weak_sch_act_wf sa s" | |||
by (case_tac sa, (simp add: weak_sch_act_wf_def)+) | |||
by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While you're changing this line, I think this would be slightly better style
by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) | |
by (cases sa; fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def) |
supply Collect_const[simp del] | ||
if_split[split del] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Incredibly minor, but do we have a style preference between these?
supply Collect_const[simp del] | |
if_split[split del] | |
supply Collect_const[simp del] if_split[split del] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Reviewing further, we also sometimes see this alternative
supply Collect_const[simp del] | |
if_split[split del] | |
supply Collect_const[simp del] | |
supply if_split[split del] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My thoughts here were that we might like to emphasise that we're doing different sorts of things. Sometimes I add a bunch of things to the simp
set and then if if_split[split del]
is right alongside, it's hard to see. So I thought maybe we'd like one line per attribute, or whatever the correct terminology is. But I'm happy to go along with whatever
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, now that you point out the different attributes I think I like your approach
(invs' | ||
and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap | ||
\<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This indentation doesn't seem quite right yet, at first glance I was still confused before realising that the final ∨
is inside the cte_wp_at'
. This looks like a bit of a painful one to do properly without some awkward linebreaks, but at the very least I think the final line should be indented two more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I misread this bit. I can open it up and redo it
proof/refine/RISCV64/IpcCancel_R.thy
Outdated
by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) | ||
by (clarsimp simp: weak_sch_act_wf_def) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Haha, that's a lot nicer than what I suggested!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I significantly weakened weak_sch_act_wf
as part of this PR, so it really didn't need much. I should have looked more closely when I first came across this.
About the weakening: we've got valid_sched_action
in AInvs that has lots of information that we can cross if we need. I really just wanted there to be a TCB at the switch to target to make CRefine easier in a few spots. We often definitely do want a TCB somewhere so we can argue about NULL
properly, together with no_0_obj'
This proves ccorres rules for isSchedulable, rescheduleRequired, possibleSwitchTo, and setThreadState, including variants for when sch_act_simple holds. This also changes the Haskell definition of isSchedulable to more closely align with the C, to ease the proof of isSchedulable_ccorres. Signed-off-by: Michael McInerney <[email protected]>
e044074
to
63f0cde
Compare
Please see the commit message