verification for deferred cache flush in untyped reset #811
Conversation
lsf37
force-pushed
the
ut-reset-caching
branch
from
b26b52f to
f5bc7ac
Compare
lsf37
force-pushed
the
ut-reset-caching
branch
from
f5bc7ac to
f212238
Compare
lsf37
changed the title
|
Right, I forgot to update RISCV64 and X64 for the new |
|
Now done. The two additional commits should probably be squashed into the first two. |
| apply (ctac (no_vcg) add: cleanCacheRange_RAM_ccorres) | ||
| apply csymbr | ||
| apply (rule ccorres_return_C; simp) | ||
| apply wp |
There was a problem hiding this comment.
out of curiosity: is there any reason why you prefer wp over wpsimp in this proof?
There was a problem hiding this comment.
If the simp is not necessary, I tend to prefer just wp because it's the less complex method and adding clarsimp into the mix at the end can mask problems later (although it can also solve simple unexpected new side goals, so it's not a completley clear cut argument -- I think I just like to use the simpler methods when they should suffice)
| apply monad_eq | ||
| by (force split: option.splits simp: fail_def return_def select_f_def empty_fail_def) | ||
|
|
||
| lemma doMachineOp_alignCheck: |
There was a problem hiding this comment.
I might discover this later in the review, but are all the doMachineOp lemmas in this file new, or moved?
There was a problem hiding this comment.
changed versions of moved lemmas (some where not phrased with monad_commute before, but the originals where in the same theoory). I guess we could move them further up, but we also do not seem to need them anywhere else, so I tried to keep noise low.
There was a problem hiding this comment.
I think this is not that bad, and the performance improvement on the seL4 side is definitely good.
Could I ask why x64 and RISCV are having such an easier time with this compared to the Arms?
For squashing, yes, I think the proofs update can be one commit (maybe add a note as to why it's mostly Arm-related).
Also small request: can this go in after the design spec arch-split overhaul?
RISCV64 and X64 have different cache flushing requirements -- on X64 the architecture doesn't require it, and the RISCV boards we are currently running don't have the level of caches that would need to be flushed, so there are only interface changes for those two, but content changes for ARM.
👍
No problem! |
lsf37
force-pushed
the
ut-reset-caching
branch
from
607dbc8 to
5f88d32
Compare
|
(rebased on current master) |
lsf37
force-pushed
the
ut-reset-caching
branch
from
5f88d32 to
f5639bd
Compare
mapM_x_commute requires "distinct" even if the operations in the mapM don't require any guards. Add a separate version without distinct when guard is \top. Signed-off-by: Gerwin Klein <[email protected]>
lsf37
force-pushed
the
ut-reset-caching
branch
2 times, most recently
from
526ae30 to
6febd3d
Compare
Defer the cache flush done in untyped_reset (inside clearMemory) to the actual retype call, and only flush for the object types where that is needed. This affects mostly the Arm architectures, but has some minor changes for adapting the arch interface init_arch_objects in RISCV64 and X64. See seL4/seL4#1289 for more detailed rationale. Signed-off-by: Gerwin Klein <[email protected]>
Most content is in the Arm architectures, RISCV64 and X64 only have interface changes, because X64 has different cache requirements and RISCV64 currently has no caches at level 2. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
lsf37
force-pushed
the
ut-reset-caching
branch
from
6febd3d to
f153579
Compare
Verification update for PR seL4/seL4#1289 where we defer the cache flush from untyped reset to the actual retype operation, which means that only flushes that are actually necessary will be performed.
This reduces the time for an untyped reset from 25 sec to 1.5 sec on the
tx2board with 8GB of memory. Smaller, but still significant benefits for boards with less memory.This was a lot more fiddly than I thought and touches some ugly old proofs. I've tried to streamline them at least a little bit and make them more consistent, but they have not become much prettier.
Test with: seL4/seL4#1289