Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feat: Dafny-to-Rust to emit Arc instead of Rc #5969

Open
Tracked by #5561
MikaelMayer opened this issue Dec 10, 2024 · 0 comments
Open
Tracked by #5561

Feat: Dafny-to-Rust to emit Arc instead of Rc #5969

MikaelMayer opened this issue Dec 10, 2024 · 0 comments

Comments

@MikaelMayer
Copy link
Member

It's currently not possible to use Dafny's datatypes and immutables collections with concurrent Rust code, because their generated structs are behind a reference-counted pointer Rc<> by default, and the reference count is not updated synchronously.
This makes it hard to use Dafny-generated code with external libraries like Tokio, which requires structs to implement the Send, and reference counting does not extend this trait. However, Arc<>, or asynchronous reference counting, implements the Send trait.

Sequences, Maps, Multisets and Sets all use Rc internally, so this means we would need to emit a modified version of the Runtime as well. Also, we should also ensure any lazy evaluation (like for sequence concatenation or codatatypes) also uses asynchronous reference counting or at least mutexes

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant