Refine AArch64 BBM modelling and add regression coverage#1864
Open
relokin wants to merge 10 commits into
Open
Conversation
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
writable2 e1 e2 was intended to return true if either e1 or e2 or both are writable PteVals. A PteVal is consider to give writeable access to the OA, if it is valid and the af the db are set. If hardware updates are enabled for the CPU that uses the PteVal, the af and the db can be set automatically on access. In this case the PteVal can be writable even when the af and db are not set. This patches fixes the function writable to consider whether hardware update for the right CPU or for no CPU is the event is due to an initialisation. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This allows other cat files to use ca. Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Summary
This branch refines the AArch64 Break-Before-Make (BBM) modelling in
herd, fixes related helper logic used by the model checker/interpreter, and adds a dedicated regression catalogue for BBM-oriented tests.Compared to
github/master, the branch includes 7 commits covering:writable2inmachModelCheckerdomaininmiaoucatalogue/aarch64-BBMregression suiteaarch64fences.catMain changes
caout ofaarch64.catintocos.catso it can be reused by the BBM-specific logic.aarch64.cat/aarch64bbm.cataround TTD/TLB-cacheability concepts rather than the olderPTE*naming, including:TLBCacheableTTD/TLBUncacheableTTDTTD-update-needsBBMwritable2inherd/machModelChecker.mlso writability is evaluated per event using the correct dirty-bit context.same_oa,oa_changes, andat_least_one_writable.tools/miaou.mlto handle thedomainprocedure.catdefinitions.tex.catalogue/aarch64-BBM/testssuite with expected outputs and acata-test-alltarget for running it.Testing
make test.herd.cata-ext.aarch64-BBM