Arch-split overhaul for design spec #809
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Xaphiosis
added
enhancement
cleanup
proof engineering
corlewis
approved these changes
Aug 12, 2024
There was a problem hiding this comment.
Very nice!
For your question about the commits, I actually don't see too much of a problem with how you've currently split it up. I would maybe combine the two 'use arch_global_naming' ones, although it's then not clear whether the arch_requalify part of the first one would belong there. Splitting up the generic and arch parts of deploying the architecture makes sense to me, since you need to do the generic ones first to easily see what can be removed from the arch files.
|
Promising initial benchmark! I'll add the other architectures once the tests complete. |
|
I'm almost a bit surprised with how good these numbers are! |
lsf37
reviewed
Aug 12, 2024
lsf37
approved these changes
Aug 12, 2024
|
In terms of commits, I wouldn't terribly mind the current state, but if you do want to squash more, I would squash the generic + arch part of the deployment, and maybe even put that together with the |
|
For completeness, |
These were requalified in the middle of the design spec and seemed out of place. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
* makes global_naming implicit (based on L4V_ARCH) * avoid unnecessary Arch context interpretation (slow) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
force-pushed
the
arch-split_design
branch
from
b79ce4f to
bd23eec
Compare
|
The latest changes look good to me, once squashed I think this is ready to be merged. |
Xaphiosis
force-pushed
the
arch-split_design
branch
from
bd23eec to
ca846db
Compare
* make global_naming implicit (based on L4V_ARCH) * avoid unnecessary Arch context interpretation (slow) * change inclusion point of MachineExports to Types_H and eliminate duplicated requalifications * migrate some Arch-theory requalifications to generic (more consistent interface) * document some name clash disambiguations * annotate vcpu type which can't be moved there, and leave vmrights which is needed for enum instantiations (can't be done in a locale) * unify interface for initIRQController and maxIRQ by providing abbreviations in _H global_naming * do not import generic constants sanitiseRegister and getSanitiseRegisterInfo; their definitions were never imported in lieu of using translated Arch versions that have the same type, causing aliasing warning during const requalification. * update comments where requalify clobbers arch version from abstract spec. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
force-pushed
the
arch-split_design
branch
from
ca846db to
e152c9e
Compare
|
Thank you again for benchmarking these @corlewis! |
|
Also happy with it, merging it now! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The adventure continues, this time deploying
arch_requalifyandarch_global_namingto the design spec skeleton files.Previously @corlewis benchmarked #805 as having 13-18% wall time improvement for ASpec, and 9-14% improvement for AInvs. This time I'm expecting only a bit of improvement in ExecSpec/BaseRefine/CBaseRefine, since only 52 cases of
context begin interpretation Arch .were eliminated from the design spec in total.🦆🦆🦆 I have split up the commits to be topical, which should make reviewing this easier, but it's a bit too much granularity to shove into l4v. Opinions welcome on how many commits we want this squashed to.