RVWMO support via Sail concurrency interface #458
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
billmcspadden-riscv
added
the
tgmm-agenda
arichardson
reviewed
Apr 30, 2024
Sail has for a while now had a flexible way of passing additional information to either operational or axiomatic concurrency models by instantiating outcomes (effects) with model-specific types. The set of possible outcomes is defined in the Sail library, and a subset of these can be instantiated by any model. As part of adapting the model to this newer concurrency interface, the riscv_analysis file is no-longer needed, so it has been removed.
arichardson
approved these changes
May 9, 2024
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.
Sail has for a while now had a flexible way of passing additional information to either operational or axiomatic concurrency models by instantiating outcomes (effects) with model-specific types. The set of possible outcomes is defined in the Sail library, and a subset of these can be instantiated by any model.
This PR refactors the base memory access functions to correctly instantiate these outcomes, which enables our concurrency tooling (most relevantly to this PR: https://github.com/rems-project/isla) to work correctly with the RISC-V model. Previously I had been maintaining this on my own fork, but it really should be upstreamed!
Outside of the memory read and write primitives being changed, there are several small changes required for the concurrency model. We need to announce when each instruction has ended, when branches occur, and tell the concurrency model what instruction is being executed after each ifetch. This for dependency analysis (deriving addr, data, and ctrl). The riscv_analysis.sail file that was previously being used for this is no longer required, so it is removed as part of this PR. There are also a few additional entry points to the model other than
mainused by the symbolic execution tooling to execute a single instruction, with and without any prior initialisation.This PR was tested on the tests in https://github.com/litmus-tests/litmus-tests-riscv, but I do need to re-run them so we should hold off on merging until that has been done.