Remove IO ports from non-X64 arches, move valid_ioports into valid_arch_state on X64 #829
Conversation
Xaphiosis
added
the
arch-split
Xaphiosis
force-pushed
the
hide-ioports
branch
from
37ce9f6 to
6787164
Compare
| apply (timeit \<open>auto elim!: delta_sym_refs pred_tcb_weaken_strongerE | ||
| simp: obj_at_def is_ep_def2 idle_not_queued refs_in_tcb_bound_refs | ||
| dest: idle_no_refs | ||
| split: if_split_asm\<close>)[2] (* slow: ~100s *) |
There was a problem hiding this comment.
Thanks for the comment, but do we want to keep the timeit command in?
There was a problem hiding this comment.
The last two times I've left the timeit in there for these very long commands, the reasoning being that when someone is doing changes in future, there's immediate feedback on whether the performance changed significantly (i.e. you get that info even if you already built all the proofs, don't have to re-trigger it and lose progress). You're right, the benefit is a bit marginal. What do you think, keep or remove?
There was a problem hiding this comment.
Hmm, I do like that benefit now that you've pointed it out. I reckon might as well keep it, it shouldn't be too confusing if we stumble across it in the future.
That does remind me though, I wish that the timing panel in Isabelle had some way of showing which entry corresponds to the command the cursor is currently on. If it had that then you could easily get the performance info without the timeit.
There was a problem hiding this comment.
timeit will work even when defer proofs is on (although it will only show output at the end of the proof block), but the timing panel will only show timing for the entire proof block/lemma, so I will leave it for now
There was a problem hiding this comment.
My vote is also for leaving the timeit in. Longer-term it would probably be nice to speed this proof up a bit, but that's out of scope for this PR.
Xaphiosis
force-pushed
the
hide-ioports
branch
from
70b6b1b to
0353607
Compare
Xaphiosis
force-pushed
the
hide-ioports
branch
from
5773431 to
8e562f9
Compare
|
I removed the X64 Refine+CRefine changes from this PR because I was able to get rid of |
|
I've not updated copyrights on any of the files. Looking at the sizes of the diffs, candidates for this are Ipc_AI and ArchIpc_AI (on all arches). Thoughts? |
I don't have strong feelings on this one. The change is significant enough to add it, but it's not like it's extremely important to do so. |
Having valid_ioports as a part of non-arch predicates caused its leakage into all other architectures, which do not have IO ports. By folding valid_ioports into valid_arch_state, the latter becomes a predicate affected by caps, causing changes in the generic interface in order to avoid any mentions of IO ports in non-arch-specific proofs. Signed-off-by: Rafal Kolanski <[email protected]>
…erface Previously valid_ioports was present on all arches. With it being migrated to valid_arch_state on X64, the interface changed to include valid_arch_state depending on caps. Update proofs to conform to the new interface, removing all mentions of IO ports from non-X64 arches. Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
Currently this means ARM and RISCV64. Already, these two architectures did not consider IO ports, so were not compatible with X64, and neither was an X64 integrity proof planned. This change leans on that by requalifying/assuming some extra lemmas which pretend that valid_arch_state not relying on caps is a generic concept. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
hide-ioports
branch
from
8e562f9 to
c158fbf
Compare
Commits are non-overlapping and can be reviewed on a commit-by-commit basis. It'll probably need more squashing than what I have now, advice welcome. 🦆🦆🦆
It was always a bit silly that valid_ioports existed on architectures with no IO ports. After discussing with Corey, the idea of moving it into valid_arch_state on X64 and retiring it on other arches came up. This worked, but resulted in changes to the arch-split interface in AInvs due to valid_arch_state now potentially depending on caps.
In Refine on X64, I did the same change so that during arch-split we won't need to see IO ports mentioned on arches that don't have them. It also required a fair bit of mangling to get through the extra valid_arch_state' dependency on caps. The hope is that maybe we can get rid of valid_ioports' altogether via assert magic. That will be the next experiment.Edit: experiment was successful, no X64 Refine+CRefine changes needed in this PR anymore
For Access+Infoflow, see commit message.