Open
Conversation
The "ExecutionGraph" GenMC folder has been renamed to "Execution", and there is a GenMC class named ExecutionState. This commit adjust the include paths in some cpp files, and renames an enum in lib.rs (ExecutionState->ExecutionStatus).
The new parameter allows to step the event index by an arbitrary amount. The functions now return void. This is a preparatory commit that lays the ground before adjusting all API calls to match the new GenMC API. The code does not compile.
Another preparatory commit before API adjustment.
This commit adds a new result type for malloc (preparatory).
In the newer GenMC version, two RMWs might read from the same write during an exploration. In such a case, the exploration has to be dropped so that an alternative one can be explored. Miri did not provide a way to completely stop an execution without throwing an error. This commit adds a new TerminationInfo case in diagnostics that is used by GenMC to signal that an execution should be aborted. On the API side, a new result field is introduced.
…ocking Add support for non-blocking TCP sockets and operations
- Fixes API calls to existing GenMC functions, which now
return the number by which event_count should be increased
- Properly handles "Invalid" results (where applicable)
- Introduces handle_non_atomic_{store,load} in Miri and
ensures they call their GenMC counterparts.
- Adds NA handlers in Miri's GenmcCtx, and renames the previous
handle_{load,store} to handle_atomic_{load,store}.
- Removes handle_load_reset_if_none, the only purpose of which
was to decrease the event counter.
- Removes dec_pos(), which is now also unnecessary.
BUG_ON() no longer exists in GenMC.
GenMC no longer relies on interpreter callbacks. It collects all information it needs for both exploration and error-reporting dynamically.
Necessary for GenMC to build. Makes exploration much faster since NAs are not explicitly tracked.
The difference is caused by the different order in which GenMC explores executions, and the new error-detection mechanism.
GenMC: Fixes and improved non-atomic handling
GenMC is now able to handle larger and mixed-size non-atomic accesses.
GenMC: Don't split up non-atomic accesses to smaller chunks
Bumps [rand](https://github.com/rust-random/rand) from 0.9.2 to 0.9.3. - [Release notes](https://github.com/rust-random/rand/releases) - [Changelog](https://github.com/rust-random/rand/blob/0.9.3/CHANGELOG.md) - [Commits](rust-random/rand@rand_core-0.9.2...0.9.3) --- updated-dependencies: - dependency-name: rand dependency-version: 0.9.3 dependency-type: direct:production ... Signed-off-by: dependabot[bot] <support@github.com>
…d-0.9.3 build(deps): bump rand from 0.9.2 to 0.9.3
genmc tests: add -Zmiri-genmc by default
Add shims for `fcntl` and `ioctl` to change socket blocking mode.
…n-blocking Allow changing socket blocking state
fix 'cargo miri nextest <verb> --help' output
…lt.stderr remove vec_unique.default.stderr
This updates the rust-version file to 6f109d8.
Pull recent changes from https://github.com/rust-lang/rust via Josh. Upstream ref: rust-lang/rust@6f109d8 Filtered ref: rust-lang/miri@b3bc25a Upstream diff: rust-lang/rust@4c42051...6f109d8 This merge was created using https://github.com/rust-lang/josh-sync.
Automatic Rustup
This updates the rust-version file to e22c616.
Pull recent changes from https://github.com/rust-lang/rust via Josh. Upstream ref: rust-lang/rust@e22c616 Filtered ref: rust-lang/miri@1aa2d78 Upstream diff: rust-lang/rust@6f109d8...e22c616 This merge was created using https://github.com/rust-lang/josh-sync.
Automatic Rustup
Collaborator
|
The Miri subtree was changed cc @rust-lang/miri |
rustbot
added
the
S-waiting-on-review
Member
Author
|
@bors r+ |
Contributor
rust-bors
bot
added
S-waiting-on-bors
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
5 participants
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.
Subtree update of
mirito rust-lang/miri@16dd940.Created using https://github.com/rust-lang/josh-sync.
r? @ghost