Miri: Use -Zmiri-tree-borrows instead of -Zmiri-disable-stacked-borrows

crossbeam-rs · Jun 17, 2023 · ce31c18 · ce31c18
1 parent a30f1d4
commit ce31c18
Showing 1 changed file with 8 additions and 12 deletions.
diff --git a/ci/miri.sh b/ci/miri.sh
@@ -19,26 +19,22 @@ MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag
     cargo miri test \
     -p crossbeam-channel 2>&1 | ts -i '%.s  '
 
-# -Zmiri-disable-stacked-borrows is needed for https://github.com/crossbeam-rs/crossbeam/issues/545
-MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-isolation -Zmiri-disable-stacked-borrows" \
+# Use Tree Borrows instead of Stacked Borrows because epoch is not compatible with Stacked Borrows: https://github.com/crossbeam-rs/crossbeam/issues/545#issuecomment-1192785003
+MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-isolation -Zmiri-tree-borrows" \
     cargo miri test \
-    -p crossbeam-epoch 2>&1 | ts -i '%.s  '
+    -p crossbeam-epoch \
+    -p crossbeam 2>&1 | ts -i '%.s  '
 
+# Use Tree Borrows instead of Stacked Borrows because epoch is not compatible with Stacked Borrows: https://github.com/crossbeam-rs/crossbeam/issues/545#issuecomment-1192785003
 # -Zmiri-ignore-leaks is needed for https://github.com/crossbeam-rs/crossbeam/issues/614
-# -Zmiri-disable-stacked-borrows is needed for https://github.com/crossbeam-rs/crossbeam/issues/545
-MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-isolation -Zmiri-disable-stacked-borrows -Zmiri-ignore-leaks" \
+MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-isolation -Zmiri-tree-borrows -Zmiri-ignore-leaks" \
     cargo miri test \
     -p crossbeam-skiplist 2>&1 | ts -i '%.s  '
 
-# -Zmiri-disable-stacked-borrows is needed for https://github.com/crossbeam-rs/crossbeam/issues/545
+# Use Tree Borrows instead of Stacked Borrows because epoch is not compatible with Stacked Borrows: https://github.com/crossbeam-rs/crossbeam/issues/545#issuecomment-1192785003
 # -Zmiri-compare-exchange-weak-failure-rate=0.0 is needed because some sequential tests (e.g.,
 # doctest of Stealer::steal) incorrectly assume that sequential weak CAS will never fail.
 # -Zmiri-preemption-rate=0 is needed because this code technically has UB and Miri catches that.
-MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-stacked-borrows -Zmiri-compare-exchange-weak-failure-rate=0.0 -Zmiri-preemption-rate=0" \
+MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-isolation -Zmiri-tree-borrows -Zmiri-compare-exchange-weak-failure-rate=0.0 -Zmiri-preemption-rate=0" \
     cargo miri test \
     -p crossbeam-deque 2>&1 | ts -i '%.s  '
-
-# -Zmiri-disable-stacked-borrows is needed for https://github.com/crossbeam-rs/crossbeam/issues/545
-MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-retag-fields -Zmiri-disable-stacked-borrows" \
-    cargo miri test \
-    -p crossbeam 2>&1 | ts -i '%.s  '