Add the Alioth chameneos-redux benchmark #2832
Closed
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
First test using the new comm system. About twice the throughput of the old system.
Fixed a bug in the atomic intrinsics where they wouldn't correctly return their old value. Pipes currently busy wait. The next step is to teach the scheduler how to deal with them.
… really fast. Fixing old-style vector, and xfail-prettying th contracts test because the pretty printer is unhappy.
… verify that busy waiting is no longer happening. Fixing the result of a bad merge.
Making all tests pass.
Updating syntax and test cases.
This integrates the pipe compiler into the proto syntax extension.
…use Paul's Early parser stuff.
…embering to add protocol parser.
…e pending snapshot.
|
Actually, I shouldn't just xfail pretty, but I should figure out how to fix that, too... |
|
D'oh, wrong version... |
This reverts commit c4af6e9. Branch was burning...many, many unresolved imports.
|
My further experimentation with pipes is on hold at the moment pending #2834. This version should be OK with just ports and channels, though. |
This adds a Rust implementation of the Alioth chameneos-redux benchmark: http://shootout.alioth.debian.org/u64q/performance.php?test=chameneosredux This version already seems faster than Clojure, Ruby, and OCaml. I'm running with N=6,000,000 in about 1m 50s. Further optimization would be good, though. I'm talking right now with @eholk about how pipes could be used (this is 1:many)...
|
Merged. Thanks! |
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this pull request
Jul 29, 2024
We believe the `--visualize` is much harder to use than concrete playback. In the rare cases where a trace might be relevant, users can still use CBMC trace. For most users, this will simplify installation since Kani will no longer depend on Python3. Note: As opposed to `--function` which was purely an internal feature, I believe we have mentioned `--visualize` to users before, so I think it's important to have a deprecation period. Related rust-lang#2832
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.
This adds a Rust implementation of the Alioth chameneos-redux benchmark:
http://shootout.alioth.debian.org/u64q/performance.php?test=chameneosredux
This version already seems faster than Clojure, Ruby, and OCaml. I'm running
with N=6,000,000 in about 1m 50s. Further optimization would be good, though.
I'm talking right now with @eholk about how pipes could be used (this is 1:many)...