Possible false-positive in MIRI race detector

language design Unsafe Code Guidelines
10

The difference in built MIR between the two is tiny, and seems due just to the additional scope entered for the extra &val. The relevant bits:

-// fail
+// pass
 let _1: u8;
+let mut _3: &u8;
 // …
 let _11: &u8;
 // …
 scope 1 {
     debug val => const 0_u8;
-    scope 2 {
         let _2: u8;
-        scope 3 {
+        scope 2 {
             debug val2 => _2;
-            scope 4 {
+            scope 3 {
                 // …
-                scope 5 {
+                scope 4 {
                     let _13: &u8;
-                    scope 6 {
+                    scope 5 {
                         debug r => _13;
                     }
                 }
             }
         }
-    }
 }

 bb0: {
     // …
     _1 = const 0_u8; // val
+    _3 = &_1;
-    _2 = _1; // val2
+    _2 = *_3; // val2
     // …
     _11 = &_2; // for println!
     // …
     _12 = spawn::<{closure}, ()>(const ZeroSized: {closure}) -> [return: bb4, unwind continue];
 }
 bb4: {
     _13 = &_1; // r
     // …
 }

(Where scopes actually cover isn't notated in the human consumption only MIR format.) This doesn't seem like it should have semantic impact; everything w.r.t. the place should be happening in the same causual order in both cases.

Without having dived into Miri, it likely is a false positive due to places not being allocated into memory until their reference is taken. It's an optimization for most cases (there's a lot of bookkeeping happening for allocations in Miri) but results in a false positive here. Assuming that's a correct assessment, the fix would be to assign a timestamp corresponding to the local place initialization when reifying into an allocation, instead of the timestamp of the reification itself.

3 Likes