Feat: Ability to emit sync-compatible Rust code. #6040

MikaelMayer · 2025-01-10T19:32:05Z

Fixes #5969

What was changed?

I added a new Rust-specific option --rust-sync, set to false by default. When turned on, all the generated code uses std::sync::Arc instead of std::rc::Rc. Nothing else is normally needed for generated code.
The option --include-runtime=true now emits the runtime when translating to Rust.
I added a new feature for the dafny runtime which is feature = "sync", enabling or disabling some functions via #[cfg(feature = "sync")] and #[cfg(not(feature = "sync"))]. Regular tests don't use this feature.
I ran cargo fmt on the runtime.

How has this been tested?

A test comp/rust/arc/tokiouser.dfy uses this option and the runtime with the sync feature, compiled with --rust-sync

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…g/dafny into fix-5969-sync-for-rust

MikaelMayer · 2025-01-14T16:22:26Z

TODO: We need to downcast objects as well. Downcast requires send and sync but it's not implemented for objects for some reason.

<small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

…g/dafny into fix-5969-sync-for-rust

robin-aws

LGTM in general, made suggestions to improve the code but I'm not blocking on them, up to you how much to pull in. The comments about customer-facing documentation are the only blockers.

robin-aws · 2025-01-23T18:12:44Z

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy

@@ -594,6 +595,8 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
  }

  function CoerceImpl(
+    rc: R.Type -> R.Type,


Consider using a term distinct from "RC" throughout for the abstract concept that will be mapped to either Rc or Arc. It's easy to get the concepts confused here, and that might have been a factor in initially missing that IsRc was testing for the wrong thing.

I considered your proposition, but Arc and Rc are essentially the same concept "rc" that is used throughout the codebase. What prevented us from catch IsRc is that Rc was imported twice into two different names, which is no longer the case, so I think we are fine here.

Fair enough, and I wouldn't want to change the symbols in the runtime at this point since we've already updated smithy-dafny to use Rc too.

robin-aws · 2025-01-23T18:19:43Z

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

+pub use ::std::marker::Send;
+pub use ::std::marker::Sync;
+
+#[cfg(not(feature = "sync"))]


FYI this would probably be cleaner if you used https://crates.io/crates/cfg-if to group things into just two blocks:

cfg_if::cfg_if! { if #[feature = "sync"] { pub type DynAny = dyn Any + Send + Sync; pub struct UnsafeCell<T: ?Sized> { data: ::std::cell::UnsafeCell<T>, // UnsafeCell for interior mutability } ... } else { pub type DynAny = dyn Any; pub use ::std::cell::UnsafeCell; ... } }

I would like to avoid taking dependencies that are not strictly necessary. I'm ok with repeating the test in front of every specific declaration as well.

robin-aws · 2025-01-23T18:20:09Z

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

+    data: ::std::cell::UnsafeCell<T>, // UnsafeCell for interior mutability
+}
+#[cfg(feature = "sync")]
+unsafe impl<T: ?Sized> Sync for UnsafeCell<T> where T: Send {}


Why is unsafe necessary here? We should at least document it

Documented + removed use of UnsafeCell for sequences to prefer the mutex just in case, and added tests.

robin-aws · 2025-01-23T18:22:10Z

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

@@ -784,29 +822,59 @@ where
                left,
                right,
            } => {
+                #[cfg(feature = "sync")]


cfg-if even more appealing here IMO

I'm grouping statements together and do some renaming so that using cfg-if will look a bit less appealing :-)

robin-aws · 2025-01-23T18:24:49Z

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

        let t: Rc<T> = Rc::downcast::<T>(t).ok()?;
        mem::transmute(t)
    }

-    /// A reference counted smart pointer with unrestricted mutability.
-    pub struct ArcMut<T: ?Sized> {


Now I'm curious, why was this already in here?

Because I had envisioned since the beginning we might want to have the async version of Rc for objects; however, I had not used it. So removing it because now for sure we are implementing it differently.

robin-aws · 2025-01-23T18:32:26Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/arc/tokiouser-rust/src/main.rs

robin-aws · 2025-01-23T18:43:17Z

Source/DafnyCore/Backends/Rust/RustBackend.cs

  };
-  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { RustModuleNameOption };
+  public static readonly Option<bool> RustSyncOption = new("--rust-sync",
+    @"Ensures that both datatypes and Dafny collections use structures that implement the Sync and Send traits") {


Isn't this essentially all values, not just datatypes and collections?

robin-aws · 2025-01-23T18:46:21Z

Source/DafnyCore/Backends/Rust/RustBackend.cs

-    } else {
-      args.Add("--bin");
-      args.Add(Path.GetFileNameWithoutExtension(targetFilename));
+  private static void ImportRustRuntimeTo(string targetDirectory) {


Would it be possible to use SinglePassCodeGenerator.EmitRuntimeSource or .ReadRuntimeSystem instead, perhaps with some tweaks to those methods?

I think this function is the closest to ReadRuntimeSystem than EmitRuntimeSource since we don't emit the run-time inside the generated code. However, I think ReadRuntimeSystem is a terrible name since it essentially copies the runtime into a specific location.
I'll rename both Rust and Java version to ImportRuntimeTo

I started also looking into merging them but this function does not lies in the same architecture as the SinglePassCompiler. There is another compiler in between and linking them together would be more verbose than necessary. Moreover, I see that the code significantly differ so I'm not sure tweaking the existing ReadRuntimeSystem would actually help anything. I'll skip that part as, even if we end up to want it, would probably require a PR of its own.

robin-aws · 2025-01-23T18:48:05Z

Source/DafnyRuntime/DafnyRuntimeRust/Cargo.toml

@@ -7,3 +7,6 @@ edition = "2021"
 once_cell = "1.18.0"
 num = "0.4"
 itertools = "0.11.0"
+
+[features]
+sync = []


Worth a comment, since consumers have to turn on this feature and should be aware of what it's doing?

# Conflicts: # Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs

Feat: Ability to emit sync-compatible Rust code.

ba89c76

MikaelMayer added the run-integration-tests Forces running the CI for integration tests even if the deep tests fail label Jan 10, 2025

MikaelMayer and others added 2 commits January 10, 2025 17:07

Merge branch 'master' into fix-5969-sync-for-rust

03adc1b

Added missing Cargo.toml

fb43df6

MikaelMayer requested review from robin-aws and alex-chew January 11, 2025 00:50

MikaelMayer and others added 4 commits January 10, 2025 18:55

Merge branch 'master' into fix-5969-sync-for-rust

1c6bb02

Fixed cargo file

7f4c46e

Merge branch 'fix-5969-sync-for-rust' of https://github.com/dafny-lan…

ca0e2c1

…g/dafny into fix-5969-sync-for-rust

Added missing main

bbaf95d

MikaelMayer and others added 14 commits January 15, 2025 11:22

Unified the two downcast methods

d6eb4cb

Ensure Rc can coerce too

cd8b320

Fixed CI test

d0ad506

Merge branch 'master' into fix-5969-sync-for-rust

e661f2e

fix: remove deadlock from Sequence (#6056)

e837fb3

<small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Added necessary traits for trait generation (Sync + Send)

be5b210

Latest version

a03084d

Merge branch 'master' into fix-5969-sync-for-rust

b490b29

Other version with Sync and Send on top of Any

72bc49d

Merge branch 'fix-5969-sync-for-rust' of https://github.com/dafny-lan…

dfb533a

…g/dafny into fix-5969-sync-for-rust

Support for sync-ed functions

10c60f4

Support for functions in sync

7255d3d

Merge branch 'master' into fix-5969-sync-for-rust

d07403b

Fixed functions

f8225f9

MikaelMayer enabled auto-merge (squash) January 22, 2025 22:42

Merge branch 'master' into fix-5969-sync-for-rust

7429b75

robin-aws requested changes Jan 23, 2025

View reviewed changes

MikaelMayer added 2 commits January 23, 2025 16:00

Ensure sync behavior of sequences is tested + doc about unsafe

8e9129b

Review comments

b641ec8

Merge branch 'master' into fix-5969-sync-for-rust

345a59a

# Conflicts: # Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs

robin-aws previously approved these changes Jan 23, 2025

View reviewed changes

MikaelMayer added 2 commits January 24, 2025 10:03

Merge branch 'master' into fix-5969-sync-for-rust

fc64367

Updated the Rust runtime

e2e5f36

MikaelMayer dismissed robin-aws’s stale review via e2e5f36 January 24, 2025 16:12

robin-aws approved these changes Jan 24, 2025

View reviewed changes

MikaelMayer merged commit 18c538a into master Jan 24, 2025
22 checks passed

MikaelMayer deleted the fix-5969-sync-for-rust branch January 24, 2025 16:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Ability to emit sync-compatible Rust code. #6040

Feat: Ability to emit sync-compatible Rust code. #6040

MikaelMayer commented Jan 10, 2025 •

edited

Loading

MikaelMayer commented Jan 14, 2025

robin-aws left a comment

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

robin-aws Jan 23, 2025

robin-aws Jan 23, 2025

MikaelMayer Jan 23, 2025

MikaelMayer Jan 23, 2025

robin-aws Jan 23, 2025

Feat: Ability to emit sync-compatible Rust code. #6040

Feat: Ability to emit sync-compatible Rust code. #6040

Conversation

MikaelMayer commented Jan 10, 2025 • edited Loading

What was changed?

How has this been tested?

MikaelMayer commented Jan 14, 2025

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer commented Jan 10, 2025 •

edited

Loading