Arch-split overhaul for design spec #809
Conversation
Xaphiosis
added
enhancement
cleanup
proof engineering
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! |
|
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 <[email protected]>
* makes global_naming implicit (based on L4V_ARCH) * avoid unnecessary Arch context interpretation (slow) Signed-off-by: Rafal Kolanski <[email protected]>
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 <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
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! |
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.