Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Opinionated deployment of enhanced Requalify capabilities on AInvs #791

Closed
wants to merge 9 commits into from

Conversation

Xaphiosis
Copy link
Member

@Xaphiosis Xaphiosis commented Jul 11, 2024

🦆🦆🦆 Temporarily only dealing with AARCH64; want feedback before applying to other arches.
(look at the top relevant "[wip]" commits only for now! this is supposed to be on top of the requalify changes #788 that are not yet merged, but since I'm making these PRs from my fork I can't stack them, lesson learned).

This yields a performance improvement (possibly due to context begin interpretation Arch . not being parallalisable by Isabelle):

AInvs after deploying tweaks:
glow: ( 0:13:50 real,  1:15:34 cpu, 13.13GB)
      ( 0:14:07 real,  1:16:58 cpu, 17.06GB)
pcr:  ( 0:08:30 real,  0:44:48 cpu, 16.97GB)

AInvs before requalify tricks:
glow: ( 0:17:17 real,  1:24:48 cpu, 16.01GB)
      ( 0:17:15 real,  1:25:41 cpu, 17.21GB)
pcr:  ( 0:14:13 real,  1:07:29 cpu, 10.46GB)

Here's what I changed:

  • global_naming AARCH64 -> arch_global_naming
  • try get rid of interpretation Arch . (slow) in lieu of (in Arch) (faster) or proper requalifying (nearly instant)
  • get rid of requalifications that were already requalified, or were global (thanks to new warnings) TODO: some of these will turn out to be broken because they're not actually global/exported on other arches
  • put arch_global_naming on same line as context Arch begin
  • annotate requalifications in Arch theories that can be moved to generic
  • put FIXMEs on unusual global_naming practices

Tracking TODOs for this stage:

  • change all FIXME arch_split to FIXME arch-split in entire repo to match github/project labels
  • add FIXME arch_split to PR linter to stop people reintroducing it
  • add arch_global_naming to the strange/missing Arch-only parts and fix fallout
  • use feedback from this PR to update docs/arch-split.md
  • deploy on other arches once approach is confirmed

@Xaphiosis Xaphiosis added enhancement proof performance making the proofs faster cleanup proof engineering nicer, shorter, more maintainable etc proofs labels Jul 11, 2024
@Xaphiosis Xaphiosis requested review from lsf37 and corlewis July 11, 2024 10:02
@Xaphiosis Xaphiosis marked this pull request as draft July 11, 2024 10:03
@Xaphiosis Xaphiosis marked this pull request as ready for review July 11, 2024 10:03
@lsf37 lsf37 added the arch-split splitting proofs into generic and architecture dependent label Jul 12, 2024
Comment on lines 639 to 642
context begin interpretation Arch .
lemma delete_objects_invs[wp]:
(* generic consequence of architecture-specific details *)
lemma (in Arch) delete_objects_invs[wp]:
"\<lbrace>(\<lambda>s. \<exists>slot. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one is less weird than I originally thought. It's in an Arch file and usually would be inside the big context Arch block that spans the entire file, but here it needed to be after the interpretation part that comes above. So it's mostly a "usual" Arch lemma that is getting exported and requalified.

Looks all good to me, and the new handling of the wp attribute is better.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The issue here is that the qualified name of delete_objects_invs becomes Arch.delete_objects_invs, instead of what we normally would do via global_prefix (AARCH64.delete_objects_invs). In this case that should be ok, because it's immediately requalified into the theory context (and also tagged [wp] for that context), but it's still a bit of a finicky policy to try canonise.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Got it. We don't seem to have many of these, and for exceptional cases I think this is Ok.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would the 'canonical' approach be to export enough facts so that this can be proved in a generic file outside of Arch?

Copy link
Member Author

@Xaphiosis Xaphiosis Jul 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, I think exporting enough facts would be the right idea. Alternatively, this entire lemma could be made an assumption.
I think someone took a shortcut here, but I'm not clear on why exactly.

Comment on lines +274 to 275
(* FIXME arch_split: is there any way to optimise this interpretation out? we can't nest contexts *)
interpretation Arch .
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a bit funky. Either retype_region_proofs is supposed to be generic or not. There is retype_region_proofs_arch just above, so you'd think retype_region_proofs is the generic one, in which case it shouldn't do interpretation Arch and the lemmas should instead be inside retype_region_proofs_arch.

Changing it probably breaks something down the line, but it looks like an abstraction violation to me. Definitely good to put a FIXME here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This one is beyond me, I think I'll leave it as a FIXME.

Comment on lines +19 to +24
context Arch begin arch_global_naming

crunch arch_post_cap_deletion
for (bcorres) bcorres[wp]: truncate_state

end
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Kinda neat that we can do this now in generic files, but also a little bit dangerous. Then again, it does remove duplication.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is a travesty, I agree. However, what we had before (context begin interpretation Arch .) was just as bad, and a lot slower :/

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is definitely nicer.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think it's worth doing with the BCorres files already being a bit of a mess of dependencies, but would our current preference be to assume this in a locale and move the proof to the arch file?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, absolutely. I think this is an example of "no one likes BCorres, so it doesn't get the nice new toys". It got the worst approach. Then the next approach was the "Pre" thing, which also wasn't great, and then someone discovered the locale assumptions approach which I think is the one we should go with in any new proofs, barring maybe esoteric moments in Invariants-like files.

Comment on lines -144 to +141
context begin interpretation Arch .
lemma free_index_update_test_function_stuff[simp]:
(* FIXME arch_split: exports properties of functions that are not necessarily in global context,
and then they get placed in the global simpset *)
lemma (in Arch) free_index_update_test_function_stuff[simp]:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the slightly stranger case. We probably should avoid this kind of Arch lemma inside generic files. Then again, it has the same kind of remove-duplication benefit as the crunch (bcorres) we had elsewhere, so maybe we don't need to be too strict.

Thumbs up to making the name available so it can be removed from [simp] again if needed.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is a result of the early approaches and "Pre" tech, I think we would try to avoid this in new files.

Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is pretty neat, and I really like the speed-up. I agree with the opinionated choices in here, and green light from my side to deploy it to the other architectures.

I don't think the missing global_naming parts were intentional. Most likely just forgotten and things happened to work anyway. I would add arch_global_naming.

@Xaphiosis
Copy link
Member Author

This is pretty neat, and I really like the speed-up. I agree with the opinionated choices in here, and green light from my side to deploy it to the other architectures.

I don't think the missing global_naming parts were intentional. Most likely just forgotten and things happened to work anyway. I would add arch_global_naming.

Yay. Glad to hear it. Added the missing global_naming parts to TODO list.

Comment on lines +14 to 19
arch_requalify_consts (A)
empty_context
init_A_st

arch_requalify_consts
ptable_lift
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, I hadn't considered that the new approach of not doing the interpretation means that when requalifying we need to be more specific about the naming. I guess this would fix itself if we were consistent, which the new arch_global_naming helps with. Either way, it's still a trade-off that seems worth making.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is a bit annoying. I thought about ways to work around it, but then it turns out that I like the aesthetic of knowing whether something came from ASpec/ExecSpec or the proofs. With a bunch of work we could make the command be able to take the (A/H) on a per-id level, e.g. arch_requalify_consts empty_context (A) ptable_lift init_A_st (A) or something, but I'm not sure about how beneficial that would be.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah right, I hadn't stopped to realise that the A/H is only on things from the specs. That's not as bad as I first thought then, I was thinking it was due to us not being consistent with naming.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Still a bit annoying but I agree, probably not worth making the command more complicated to handle it.

Comment on lines 21 to 22
(* There are multiple arch-dependent acap_rights_update_id, one for wellformed_acap,
one for valid_arch_cap. Prefer the latter. *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not as part of this PR, but this sounds like something we should fix.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll take a look, you're right, something is off here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fixed and added to PR

Copy link
Member

@corlewis corlewis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this, the improved consistency and performance is definitely very nice! I generally agree with all of the existing FIXMEs and comments.

Currently, my remaining questions are around when requalifications need to be in Arch files, and when we're ok with Arch proofs in generic files. For the latter, it sort of seems like a sign that we've gotten the abstraction wrong, and should be exporting whatever else is needed from Arch so that the proof could be properly generic.

Comment on lines -129 to +128
context begin interpretation Arch .
requalify_consts post_retype_invs_check
end
arch_requalify_consts post_retype_invs_check
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Requalification in an Arch file

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

Comment on lines -686 to +684
context begin interpretation Arch .
requalify_consts region_in_kernel_window
end
arch_requalify_consts region_in_kernel_window
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Requalification in an Arch file

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

Comment on lines -1903 to +1894
context begin interpretation Arch .
requalify_consts replaceable_or_arch_update
end
arch_requalify_consts replaceable_or_arch_update
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Requalification in an Arch file

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

@Xaphiosis
Copy link
Member Author

I think I addressed everything I could for the AARCH64 test run of rolling out these strategies. Next steps will be documentation update, then deployment to other arches, possibly involving other PRs that are cross-platform.

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms
("asms" is rarely expected outside of ML code)

Signed-off-by: Rafal Kolanski <[email protected]>
* add warnings when exporting a name that already exists in theory
  context, suppressable by `(aliasing)` option
* add `arch` variants of requalify commands that implicitly add the
  value of L4V_ARCH before whatever you give them, with optional
  suffixes for abstract (A) and Haskell (H) spec global naming.
* write hopefully-understandable documentation with commented examples

Signed-off-by: Rafal Kolanski <[email protected]>
Also document that requalify commands will issue warnings.

Signed-off-by: Rafal Kolanski <[email protected]>
Stops namespace pollution, allows us to use Arch locale as example.

Signed-off-by: Rafal Kolanski <[email protected]>
Temporarily only dealing with AARCH64; want feedback before applying to
other arches.

* global_naming AARCH64 -> arch_global_naming
* try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)` (faster)
  or proper requalifying (nearly instant)
* get rid of requalifications that were already requalified, or were
  global (thanks to new warnings)
  TODO: some of these will turn out to be broken because they're not
  actually global/exported on other arches
* put arch_global_naming on same line as `context Arch begin`
* annotate requalifications in Arch theories that can be moved to
  generic
* put FIXMEs on unusual global_naming practices

Signed-off-by: Rafal Kolanski <[email protected]>
* get rid of `global_naming Arch`, this is no longer needed since we can
  requalify directly from `arch_global_naming` with `arch_requalify`
  commands
* add missing `arch_global_naming` for `context Arch`, for consistency
Rename the wellformed_acap version to wf_acap_rights_update_id,
and the valid_arch_cap version to valid_acap_rights_update_id.

Signed-off-by: Rafal Kolanski <[email protected]>
* prevent duplication between arches by moving requalifications from
  Arch theories to generic ones
  * this strategy is not available for new constants that are introduced
    in the Arch locale that need to be referenced in generic definitions
    or locale instantiations
* prefer arch_global_naming
* prefer arch_requalify commands over interpretation
* indicate consts might need to be requalified in Arch theories
* explain (in Arch) + requalify pattern for generic consequences of
  arch-specific properties
@Xaphiosis
Copy link
Member Author

Closed, full deployment now at: #805

@Xaphiosis Xaphiosis deleted the arch_split_ainvs branch August 8, 2024 01:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
arch-split splitting proofs into generic and architecture dependent cleanup enhancement proof engineering nicer, shorter, more maintainable etc proofs proof performance making the proofs faster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants