Refactor det_ext to remove scheduler state #824
Conversation
|
These changes are correct enough for the AARCH64 abstract spec to still process, although of course we can't be certain that they are sufficient for our purposes until AInvs and the relevant VCPU and FPU proofs are updated. Reviews now would still be helpful to check style and to confirm that the state being moved is what we wanted. Some specific style choices made in this were to minimise the difference to the rt branch. |
|
Having read through it, looks good from my side. Thank you for fixing up of the style along the way! |
corlewis
force-pushed
the
det_ext_state
branch
2 times, most recently
from
39e4678
to
81efd6b
Compare
|
I've updated AInvs for one architecture now. It's a big commit and will be a pain to review, but feedback now would be very helpful, so that I can clean things up before copying it to other architectures. |
corlewis
force-pushed
the
det_ext_state
branch
4 times, most recently
from
a9fff5a
to
45bcca9
Compare
The scheduler is now fully part of the extensible abstract specification, because we are increasingly finding properties that are not able to be reasonably specified without it. This means that there is now no non-deterministic scheduler specification and that the only slots for non-determinism are now CDT and preemption operations. This came up due to some properties currently being proved not being true for all execution paths of the previous non-deterministic specification. Options that were considered were: 1 - move the minimal state (the current domain and tcb's domain) required for the properties currently being considered to the extensible abstract specification. 2 - move all of the scheduler state to the extensible abstract specification, the same as what has been done on the rt branch. 3 - move all state and remove the non-deterministic specification completely. 4 - add ghost state to sidestep the specific problem that we are currently encountering (it is unclear whether this would actually work). Option 2 was chosen because it is the least blocking (although may be more annoying than some of the others), will result in the smallest diff to the rt branch, and we don't think it will be significantly more work than option 1. If we want to reason about threads in the future (e.g. liveness), we will require that this information about the scheduler state is accessible. We are really not sure about whether moving specifically the scheduler action is the right decision, but we are moving it across because the correctness of the ready queues depends on it and any alternatives that we have thought of would be a lot of work that we do not want to do at this time. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
…ated This removes the threadSet loop at the end of the TCB case which previouly needed due to ekheap in createObject in Haskell/createNewCaps in design spec. This should simplify the proofs to some extent. Co-authored-by: Miki Tanaka <miki.tanaka@data61.csiro.au> Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
corlewis
force-pushed
the
det_ext_state
branch
from
45bcca9
to
5f1e411
Compare
| = state_hyp_refs_of s" | ||
| apply (rule all_ext) | ||
| apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits) | ||
| done |
There was a problem hiding this comment.
this is a bit repetitive, but it's probably fine, especially if you pulled it from rt
| @@ -508,7 +510,7 @@ lemma dmo_scheduler_act_sane[wp]: | |||
| lemma vgic_maintenance_irq_valid_sched[wp]: | |||
| "\<lbrace>valid_sched and invs and scheduler_act_sane and ct_not_queued\<rbrace> | |||
| vgic_maintenance | |||
| \<lbrace>\<lambda>rv. valid_sched\<rbrace>" | |||
| \<lbrace>\<lambda>rv. valid_sched :: det_state \<Rightarrow> _\<rbrace>" | |||
There was a problem hiding this comment.
hang on, we can do dummy types in a type signature? how did you discover this?
| @@ -232,6 +222,13 @@ locale is_extended = is_extended' + | |||
|
|
|||
| context is_extended begin | |||
|
|
|||
| lemma in_f_exst: | |||
| "(r, s') \<in> fst (f s) \<Longrightarrow> s\<lparr>exst := exst s'\<rparr> = s'" | |||
| apply (drule v) | |||
There was a problem hiding this comment.
oof, that name, v, also this proof is one-lineable
| "cur_tcb (cdt_update f s) = cur_tcb s" | ||
| by (simp add: cur_tcb_def) | ||
|
|
||
| lemma cur_tcb_more_update[iff]: |
There was a problem hiding this comment.
do you know why this one is [iff] when all the other ones are simp?
It also looks super repetitive, they all have nearly the same proof... it almost has a crunch-like flavour, but I'm not sure we have a mechanism that can do that. Maybe scrunching the proofs into one for cur_tcb and another for valid_ioc?
| apply (simp add: state_relation_def) | ||
| apply (clarsimp simp: state_relation_def) | ||
| apply (rule absSchedulerAction_correct, simp add: state_relation_def) | ||
| apply (simp add: state_relation_def) |
There was a problem hiding this comment.
use + to fold up subsequent repeats?
| wp: switch_to_thread_invs hoare_drop_imps) | ||
|
|
||
| (* still true without scheduler_action s \<noteq> resume_cur_thread, but the proof for schedule_invs | ||
| will be simpler with it *) |
There was a problem hiding this comment.
hang on, strengthening a precondition makes the proof simpler?!
| @@ -876,18 +876,17 @@ lemma threadSet_all_invs_triv': | |||
| unfolding all_invs'_def | |||
| apply (rule hoare_pre) | |||
| apply (rule wp_from_corres_unit) | |||
| apply (rule threadset_corresT [where f="tcb_arch_update (arch_tcb_context_set f)"]) | |||
| apply (rule threadset_corresT [where f="tcb_arch_update (arch_tcb_context_set f)"]; simp?) | |||
There was a problem hiding this comment.
given all resulting subgoals get simp anyway, and indent for subsequent apply hasn't changed, what does the simp? give you?
| @@ -3135,7 +3137,8 @@ lemma cnc_tcb_helper: | |||
| [heap_update (registers_of_tcb_Ptr p) | |||
| (array_updates (h_val (hrs_mem hrs) (registers_of_tcb_Ptr p)) | |||
| initContext_registers), | |||
| heap_update (machine_word_Ptr &(p\<rightarrow>[''tcbTimeSlice_C''])) 5]) | |||
| heap_update (machine_word_Ptr &(p\<rightarrow>[''tcbTimeSlice_C''])) 5, | |||
| heap_update (machine_word_Ptr &(p\<rightarrow>[''tcbDomain_C''])) (d' :: machine_word)]) | |||
There was a problem hiding this comment.
I'm a bit confused here... this looks like the C changed somehow, but we're only changing the det_ext definitions on the abstract level, right? So why is this change needed all the way down in CRefine?
| curdom \<leftarrow> curDomain; | ||
| mapM_x (\<lambda>tptr. threadSet (tcbDomain_update (\<lambda>_. curdom)) tptr) addrs; | ||
| addrs \<leftarrow> createObjects regionBase numObjects (injectKO ((makeObject ::tcb)\<lparr>tcbDomain := curdom\<rparr>)) 0; |
There was a problem hiding this comment.
interesting, but it seems more consistent now to go via createObjects
|
|
||
| lemma foldr_kh_eq: | ||
| "foldr (\<lambda>p kh. kh(p \<mapsto> ko')) ptrs kh t = Some ko \<Longrightarrow> | ||
| if t \<in> set ptrs then ko = ko' else kh t = Some ko" |
| applied to det_ext lemmas that contain e.g. preemption_point which needs the det_ext work_units, | ||
| i.e. those will need additional locales, because 'state_ext needs to be interpreted first | ||
| into ?'state_ext. | ||
| *) |
There was a problem hiding this comment.
good idea, keep track of this (create an issue?) and do it as a subsequent PR to this one
| lemma etcbs_of_update_state[simp]: | ||
| "get_tcb ref s = Some tcb \<Longrightarrow> | ||
| etcbs_of' (\<lambda>r. if r = ref then Some (TCB (tcb_state_update f tcb)) else kheap s r) = etcbs_of' (kheap s)" | ||
| by (auto simp: etcbs_of_update_unrelated dest!: get_tcb_SomeD) |
There was a problem hiding this comment.
this doesn't look like a good candidate for [simp], it both has a conditional and a very specific pattern to match on, that looks like an unfolded fun_upd; I remember on AARCH64 proofs we had issues like that with fun_upd somewhere, but don't remember where. I think we stuck with the fun_upd syntax though and prevented unfolding somewhere
| apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split) | ||
| done | ||
|
|
||
| lemma etcbs_of_update_bound_notification[simp]: | ||
| "get_tcb ref s = Some tcb \<Longrightarrow> | ||
| etcbs_of' (\<lambda>r. if r = ref then Some (TCB (tcb_bound_notification_update f tcb)) else kheap s r) = etcbs_of' (kheap s)" |
There was a problem hiding this comment.
this also looks like a strange fun_upd unfolded
| lemma thread_set_priority_ct_not_in_q[wp]: | ||
| "thread_set_priority p t \<lbrace>ct_not_in_q\<rbrace>" | ||
| unfolding thread_set_priority_def thread_set_def | ||
| by (wpsimp wp: set_object_wp) |
There was a problem hiding this comment.
this one and thread_set_priority_neq_st_tcb_at look crunchable
|
|
||
| lemma etcbs_of_update_tcb_time_slice[simp]: | ||
| "get_tcb ref s = Some tcb \<Longrightarrow> | ||
| etcbs_of' (\<lambda>r. if r = ref then Some (TCB (tcb_time_slice_update f tcb)) else kheap s r) = etcbs_of' (kheap s)" |
There was a problem hiding this comment.
another of the fun_upd unfolded mystery
| apply (rule ext, clarsimp simp: null_filter'_def map_to_ctes_delete) | ||
| apply (rule sym, rule ccontr, clarsimp) | ||
| apply (frule(2) pspace_relation_cte_wp_atI | ||
| [OF state_relation_pspace_relation]) |
There was a problem hiding this comment.
indent, or having [ on the prev line and indent, or try fit on same line
| lemma thread_set_domain_valid_ioports[wp]: | ||
| "thread_set_domain t d \<lbrace>valid_ioports\<rbrace>" | ||
| unfolding thread_set_domain_def | ||
| by (wpsimp wp: valid_ioports_lift thread_set_caps_of_state_trivial2 simp: tcb_cap_cases_def) |
There was a problem hiding this comment.
I should remember this one for later when it conflicts with the changes I'm doing getting rid of valid_ioports
| and caps_of_state[wp]: "\<lambda>s. P (caps_of_state s)" | ||
| and no_cdt[wp]: "\<lambda>s. P (cdt s)" | ||
| (simp: Let_def Let_def | ||
| wp: hoare_drop_imps hoare_vcg_if_lift2 mapM_wp) |
There was a problem hiding this comment.
I have a feeling that this huge crunch and the previous huge crunch have significant overlap
| apply (insert assms) | ||
| apply (case_tac "injectKO v"; simp) | ||
| by (simp add: pageBits_def pteBits_def objBits_simps | ||
| split: arch_kernel_object.split)+ |
There was a problem hiding this comment.
is this the right place for these? would Invariants_H be better?
| apply (rule_tac f=g in arg_cong) | ||
| apply clarsimp | ||
| apply wpsimp+ | ||
| apply simp+ |
There was a problem hiding this comment.
unexpected, you'd think wpsimp could clear a goal that is solved by simp?
There was a problem hiding this comment.
Very solid work, saw several improvements along the way, minor comments only from me. Some of the files have diffs so big they choke my browser for over a minute, not sure what can be done about that. Probably as we discussed dump the other arches in a separate PRs to the same branch?
The scheduler is now fully part of the extensible abstract specification, because we are increasingly finding properties that are not able to be reasonably specified without it. This means that there is now no non-deterministic scheduler specification and that the only slots for non-determinism are now CDT and preemption operations.
This came up due to some properties currently being proved not being true for all execution paths of the previous non-deterministic specification. Options that were considered were:
1 - move the minimal state (the current domain and tcb's domain) required for the properties currently being considered to the extensible abstract specification.
2 - move all of the scheduler state to the extensible abstract specification, the same as what has been done on the rt branch.
3 - move all state and remove the non-deterministic specification completely.
4 - add ghost state to sidestep the specific problem that we are currently encountering (it is unclear whether this would actually work).
Option 2 was chosen because it is the least blocking (although may be more annoying than some of the others), will result in the smallest diff to the rt branch, and we don't think it will be significantly more work than option 1. If we want to reason about threads in the future (e.g. liveness), we will require that this information about the scheduler state is accessible.
We are really not sure about whether moving specifically the scheduler action is the right decision, but we are moving it across because the correctness of the ready queues depends on it and any alternatives that we have thought of would be a lot of work that we do not want to do at this time.