stateright
cargo-asm
Our great sponsors
stateright | cargo-asm | |
---|---|---|
8 | 13 | |
1,516 | 1,104 | |
1.8% | - | |
7.0 | 0.0 | |
14 days ago | about 2 years ago | |
Rust | Rust | |
MIT License | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
stateright
- Distributed Async Executors?
-
Announcing `statig`: Hierarchical state machines for event-driven systems (using GAT’s)
stateright - which is meant for distributed state machines and includes a full on model checker
-
RiB Newsletter #27
Stateright.
-
Paxos vs Raft: Have We Reached Consensus on Distributed Consensus?
Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof.
I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright
The issue is that rust is a very large language and it's hard to get it right.
I have a python implementation of raft over here:
https://github.com/adsharma/raft/tree/master/raft/states
That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages.
The issue with TLA+ proofs such as:
https://github.com/fpaxos/raft.tla
is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.
So how do we check and transpile?
* https://www.philipzucker.com/Modelling_TLA_in_z3py/
-
Does "safety by default" scale?
Why make memory safety the exception? For example, https://github.com/stateright/stateright implements model checking for distributed systems at the library-level. If you could achieve the same effect with memory safety through the ecosystem, why wouldn't you?
-
Stateright: A model checker for implementing distributed systems
Regarding the last point — correct, Stateright aims to verify both.
It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…).
Examples:
SD Paxos: https://github.com/stateright/stateright/blob/master/example...
ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/example...
-
Rust and Julia
I believe they meant this: https://github.com/stateright/stateright
cargo-asm
-
Performance difference between obj.function(...) and function(obj, ...) ?
cargo asm might be useful here (if you can't use godbolt).
-
Is there a simple way to borrow the value of an Option without using a match statement?
They should be inlined in release mode. You'd have to verify by checking the assembly, though, which could be done directly in the Rust playground or with a tool like cargo-asm.
-
Hey Rustaceans! Got a question? Ask here (4/2023)!
You can use cargo asm - not sure if you can integrate it with VSCode, but even from a terminal it's a pretty convenient tool.
-
How does rust optimize this code to increase the performance so drastically?
There's probably a built-in one somewhere, but I suspect it'd be easier just to install https://github.com/gnzlbg/cargo-asm
-
Is there a library to display source with annotations?
I don't know if there's a way to do a side by side comparison but cargo-asm uses the source mapping information from rustc to annotate chunks of assembly with it's respective rust code, though it's an imperfect process.
-
Hey Rustaceans! Got a question? Ask here! (25/2022)!
After that you would need some tools to help figure out how to achieve improvements. That will depend on your system and personal preferences. As the other commenter suggested, perf is a good choice on linux. I personally like to look at the generated assembly, using either cargo asm, godbolt, or just rust playground.
-
New crate announcement cargo-show-asm
Doesn't this already exist? https://github.com/gnzlbg/cargo-asm
- on the fly disassembler for Rust symbols
-
Writing the fastest GBDT libary in Rust
From the flamegraph, we knew which function was taking the majority of the time, which we briefly described above. We started by looking at the assembly code it generated to see if there were any opportunities to make it faster. We did this with cargo-asm.
-
How can I profile this type of slowdown?
You're best bet at the moment is probably using cargo-asm to inspect the function assembly to see when it is performing the correct TCO.
What are some alternatives?
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
rust - Empowering everyone to build reliable and efficient software.
mina-vrf-rs
cargo-show-asm - cargo subcommand showing the assembly, LLVM-IR and MIR generated for Rust code
py2many - Transpiler of Python to many other languages
multitarget-issue
raft.tla - TLA+ specification for the Raft consensus algorithm
safe_arch - Exposes arch-specific intrinsics as safe function (via cfg).
lam - :rocket: a lightweight, universal actor-model vm for writing scalable and reliable applications that run natively and on WebAssembly
wide - A crate to help you go wide. By which I mean use SIMD stuff.
dylint - Run Rust lints from dynamic libraries
macroquad - Cross-platform game engine in Rust.