AArch64 fastpath proofs #739
Conversation
Xaphiosis
force-pushed
the
aarch64_fastpath
branch
from
fc15436
to
de41cc6
Compare
|
rebased onto master, had a de-sync between seL4 versions |
|
Nice work. Personally I'd slightly prefer 3 commits, or if you want to minimise, maybe 2 (one for defs + equiv, and one for the C part), but I don't have strong feelings about it. |
| - can't use clarsimp because it'll introduce new free variables (\<exists>_. _ = Some _) that will | ||
| cause schematic unification problems |
There was a problem hiding this comment.
We could try to remove the simp rule that turns None into Ex Some. With that, clarsimp might be fine.
There was a problem hiding this comment.
There's still the issue of pairs, which would need to be folded back into fst and snd. Do we have tech to handle that?
There's also what Corey wrote on the wp schematic issue, where we might have a wrong rule in the wp_comb set.
There was a problem hiding this comment.
To clarify, if I'm right in what I thought was going on with the wp_comb rule then it would just help with the problem you ran into of a schematic assumption being produced and then unified with False. The actual proof would still require either your careful rule application or the careful adjustment of the simp set like you two are talking about.
There was a problem hiding this comment.
Pairs being split should be handled correctly by wpfix, so I think removing the None/Some rule has a chance in this case (it won't fix the general problem). It has a tag already, so we're fine to merge, I was just curious what people's thoughts were on this one. If I get to it in the cleanup run I might try out removing the rule and see what happens.
There was a problem hiding this comment.
Ok, that would be nice, but I think the wp_comb thing also should happen if we're doing cleanup at some point, because the combo of wp, simp, vcg is a disaster to work with otherwise. When you say "when I get to it in the cleanup run", does that mean you've assumed responsibility for the doing entire cleanup run?
There was a problem hiding this comment.
I was planning to volunteer to do a first pass, but I wouldn't say I have assumed responsibility for all of the cleanup :-) There will probably be a whole bunch of things that need some insight and where we might want to discuss more, it'd be nice to do these together in some way.
There was a problem hiding this comment.
Very cool. Modulo the small stuff above and commit squashing, I think this is ready to merge. It's still gigantic, but it looks to me like proof quality has improved a bit compared to the other fast path versions.
We should add a commit that removes the CREFINE_QUICK_AND_DIRTY from the Makefile.
I'd like your reply to my replies (maybe I catch you tonight) before resolving the rest. I also have some questions:
Good point, added that to the commits. I'm not sure whether anyone else is going to look at this, but I will wait with squashing until tonight when we can hopefully resolve/discuss the remaining issues. |
I think we should merge this one first, so the proof is properly finished and
It's ok to leave it for now. The proposed
👍
We're good to merge from my side after squashing. |
These rules completely discarded the assertion and directly linked the assertion with the precondition. The general form allows assuming the assertion in subsequent statements under the assumption on non-failure. Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
Add fastpathKernelAssertions to start of callKernel. Fastpath rewrite proofs don't get the state relation, so can't cross properties over from the abstract invariants. We also can't rely on asserts on the fast path side, since any failure in the rewrite must be correlated with failure in the original, and the locations and conditions of those failures can be quite distant. Signed-off-by: Rafal Kolanski <[email protected]>
Currently, this is only interesting on AARCH64 where we need no_fail preconditions for looking up an ASID map entry. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
aarch64_fastpath
branch
from
f1391d6
to
d5822dd
Compare
|
Squashed and pushed. Might be worth waiting for the test results on this one as it adds the quick_and_dirty removal from the Makefile. |
Update the existing fastpath function "design" specs with AArch64-specific functionality: * looking up the VMID / hardware asid is more complex, going via the ASID map, with additional checks necessary * redundant check for ReplyMaster no longer happens These specs will be shown to be equivalent to the slow path (callKernel) and fastpath C code. Signed-off-by: Rafal Kolanski <[email protected]>
Plus cleanup and commentary. Signed-off-by: Rafal Kolanski <[email protected]>
Shows fastpath spec refines down to C for Call and ReplyRecv. Includes much effort to document what is happening in the main proofs, updates for AArch64-specific and 64-bit-specific mechanisms and bitfields. Signed-off-by: Rafal Kolanski <[email protected]>
CRefine on AARCH64 is now sorry-free, and there are no other sorried developments at this time. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
aarch64_fastpath
branch
from
d5822dd
to
4efd093
Compare
|
Happy with the squash and commit messages. Will wait for the tests to pass before merging. |
Before I do more cleanup, I think this could use some feedback. Please ignore the horrid commit history (for now), but advice welcome on whether I should squash the actual fastpath commits into 3 parts (defs, rewrite, C refinement), or only one commit.
In any case the proofs work and look better than the ARM/ARM_HYP ones at least.