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
5 times, most recently
from
45bcca9 to
5f1e411
Compare
| "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?
There was a problem hiding this comment.
Not sure, presumably historical reasons of whoever wrote them preferring one attribute over the other. I guess simp would be the preference now if we wanted to make them consistent?
There was a problem hiding this comment.
I'm not sure what the difference is between [iff] and [simp] to be honest. If it's the same, simp will be more consistent, but ok to leave it.
There was a problem hiding this comment.
[iff] also makes [intro!] and [elim!] rules out of the equation, so e.g. clarify would act as well on that constant. Could be that this specific one has one such instance, or it was just done by another person than the rest.
| 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
There was a problem hiding this comment.
I'm not actually convinced that this factoring out would be worth it. We are in a DetSched* theory after all, and it would be perfectly fine for everything in here to be in det, even if some facts would also be true about state_ext.
There was a problem hiding this comment.
Right, but with this change the DetSched* theories don't actually depend on anything from the extended state, which is a bit unfortunate with the naming of them. I do agree anyway that this might not be worth it, although I would be more tempted by similar issues in locales in earlier files. They generally don't break the proofs but mean that lemmas need to be tagged with det_state a fair bit more than necessary.
There was a problem hiding this comment.
Right, that makes complete sense. Maybe filing an issue for that is the best idea then.
| 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
There was a problem hiding this comment.
Hmm, how against this sort of lemma are you? It was copied from rt and that specific pattern comes up in a few places in the proofs, so I don't really want to try and rework things to avoid it. I did have a quick look and the fun_upd seems to be expanded by fun_upd_apply, which would be a pain to have to delete from simp everywhere.
There was a problem hiding this comment.
If they're copied, I think for this PR we live with them.
I'm not sure about the fun_upd situation precisely, but one way I would handle it is writing the lemma with a := so that it makes sense, and using [simplified fun_upd_def] (or fun_upd_apply or whatever, to get it into simp normal form. Generally it looks really noisy, but I guess that's fun_upd for you.
There was a problem hiding this comment.
There's definitely a fair bit of supply fun_upd_apply[simp del] and simp_del: fun_upd_apply on AARCH64
There was a problem hiding this comment.
The lemma is not pretty, but it should be safe in the sense that the lhs of the equation is specific enough for Isabelle not to go chasing after the side condition all the time. So it shouldn't slow things down.
And agreed that this smells like fun_upd_apply repair which should ideally prevented before it happens. Ok to live with it for now, I'd say.
There was a problem hiding this comment.
It's of course not just fun_upd_apply repair, it is actual content: it's showing that a tcb_state_update is invisible in the etcbs_of projection. That part is actually needed. The phrasing as an expanded fun_upd_apply is not so great, but if it is the actual normal form in these proofs, then it's not unjustified, just a bit ugly.
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?
corlewis
force-pushed
the
det_ext_state
branch
from
b4e287f to
b9b3498
Compare
|
This has been rebased and includes all changes required for the AArch64 proofs. It is ready to be merged into a new branch to track this in-progress work until all of the proofs for all architectures have been updated. |
| done | ||
|
|
||
| lemmas mapM_x_defsym = mapM_x_def[symmetric] | ||
| crunch reset_untyped_cap | ||
| for etcb_at[wp]: "etcb_at P t" |
There was a problem hiding this comment.
but surely etcb_at could now be just tcb_at, or am I missing something?
There was a problem hiding this comment.
Huh, yeah, that's definitely true. That does feel like a something we should do, as long as it doesn't take too long now to update everywhere. But then we would want to make the same change on rt, and I'm not sure if that's a priority right now.
There was a problem hiding this comment.
True. Worth noting in an issue, though, it's something we should remove at some point. Happy for that to be some other time.
corlewis
force-pushed
the
det_ext_state
branch
from
0805c4f to
9e865b3
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 <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
…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 <[email protected]> Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
det_ext_state
branch
from
9e865b3 to
6cb7147
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.