ADT_C sorry-free
#685
ADT_C sorry-free
#685
Conversation
Signed-off-by: Michael McInerney <[email protected]>
This modifies active_sc_valid_refills to additionally state that an inactive scheduling context has zero budget Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
added
the
MCS
|
I think it looks mostly fine, I'm confused by "rt crefine: sorries related to cpspace_refill_relation_unique" ... that commit proves some things, changes a def or two, but doesn't introduce any new sorries... what am I missing? Won't manage any deeper than that this week, but can look at the contents more next week. |
That commit clears sorries related to |
There was a problem hiding this comment.
Excellent, this is a big chunk of additional work and brings a lot more confidence to the state relation and proof setup. Also aligns C and spec more closely, which is always good.
Only some minor style nitpicks in the comments that would be good to fix up before merging. For the commit message Raf mentioned, clear sorries .. is a good idea and would work.
Let me look at the history for a sec so I don't give bad advice... OK, Gerwin does say things like TLDR: Yes please, something like |
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-adt_c_sorry_free
branch
from
aa80af4
to
b843dad
Compare
| "\<And>P. \<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p | ||
| \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p) | ||
| \<and> I s\<rbrace> | ||
| f \<lbrace>\<lambda>_ s. \<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p | ||
| \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>" |
There was a problem hiding this comment.
Well spotted, we're deferring fixing that one up to a later PR.
This removes all the sorries in the file
ADT_C, thereby significantly increasing our confidence that the state relation is correct.This also removes the
budgetfield of scheduling contexts in the executable specification (and Haskell kernel). This brings the executable spec closer to the C code and shifts the condition that the budget is always the sum of all refills into the abstract refinement proofs where the corresponding invariants are more easily available.