You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Auto merge of #3067 - Vanille-N:spurious-incremental, r=RalfJung
Continuation of #3054: enable spurious reads in TB
The last additions to the test suite of TB left some unresolved `#[should_panic]` that these new modifications solve.
## Problem
Recall that the issues were arising from the interleavings that follow.
### A. `Reserved -> Frozen` has visible effects after function exit
The transition `Reserved -> Frozen` irreversibly blocks write accesses to the tag, so in the interleaving below `y` initially `Reserved` becomes `Frozen` only in the target where a spurious read through `x` is inserted. This makes the later write through `y` UB only in the target and not in the source.
```
1: retag x (&, protect)
2: retag y (&mut, protect)
1: spurious read x
1: ret x
2: ret y
2: write y
```
### B. Protectors only announce their presence on retag
There is a read-on-reborrow for protected locations, but if the retag of `x` occurs before that of `y` and there is no explicit access through `x`, then `y` is unaware of the existence of `x`. This is problematic because a spurious read inserted through `x` between the retag of `y` and the return of the function protecting `x` is a noalias violation in the target without UB in the source.
```
1: retag x (&, protect)
2: retag y (&mut, protect)
1: spurious read x
1: ret x
2: write y
2: ret y
```
## Step 1: Finer behavior for `Reserved`
Since one problem is that `Reserved -> Frozen` has consequences beyond function exit, we decide to remove this transition entirely. To replace it we introduce a new subtype of `Reserved` with the extra boolean `aliased` set.
`Reserved { aliased: true }` forbids child accesses, but only temporarily: it has no effect on activation once the tag is no longer protected.
This makes the semantics of Tree Borrows slightly weaker in favor of being more similar to noalias.
This solves interleaving **A.**, but **B.** is still a problem and the exhaustive tests do not pass yet.
## Step 2: Read on function exit
Protected tags issue a "reminder" that they are protected until this instant inclusive, in the form of an implicit read (symmetrically to the implicit read on retag). This ensures that if the periods on which two tags `x` and `y` are protected overlap then no matter the interleaving of retags and returns, there is either a protector currently active or a read that has been emitted, both of which temporarily block activation.
This makes the exhaustive test designed previously pass, but it has an effect on the ability to return an activated pointer that I had not foreseen before implementing it.
## Step 2': Do not propagate to children
A naive implementation of **Step 2** makes the following code UB:
```rs
fn reborrow(x: &mut u8) -> &mut u8 {
let y = &mut *x;
*y = *y;
y // callee returns `y: Active`...
}
let x = &mut 0u8;
let y = reborrow(x); // ... and caller receives `y: Frozen`
*y = 1; // UB
```
This is unacceptable, and a simple fix is to make this implicit read visible only to foreign tags.
We still lack hindsight on the ramifications of this decision, and the fact that the problematic pattern was only discovered because it occured in one completely unrelated test (with a cryptic error message) is worrying. We should be vigilant as to how this interacts with the rest of the model.
## TODO
As of commit #281c30, the data race model has not been fully updated.
We have removed the reborrow of mutable references counting as a write access, but we still need the implicit read of function exit to count as a read.
Copy file name to clipboardExpand all lines: src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
+18-3
Original file line number
Diff line number
Diff line change
@@ -19,6 +19,7 @@ pub enum AccessCause {
19
19
Explicit(AccessKind),
20
20
Reborrow,
21
21
Dealloc,
22
+
FnExit,
22
23
}
23
24
24
25
impl fmt::DisplayforAccessCause{
@@ -27,6 +28,7 @@ impl fmt::Display for AccessCause {
27
28
Self::Explicit(kind) => write!(f,"{kind}"),
28
29
Self::Reborrow => write!(f,"reborrow"),
29
30
Self::Dealloc => write!(f,"deallocation"),
31
+
Self::FnExit => write!(f,"protector release"),
30
32
}
31
33
}
32
34
}
@@ -38,6 +40,7 @@ impl AccessCause {
38
40
Self::Explicit(kind) => format!("{rel} {kind}"),
39
41
Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
40
42
Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
43
+
Self::FnExit => format!("protector release (acting as a {rel} read access)"),
41
44
}
42
45
}
43
46
}
@@ -52,7 +55,9 @@ pub struct Event {
52
55
/// Relative position of the tag to the one used for the access.
53
56
pubis_foreign:bool,
54
57
/// User-visible range of the access.
55
-
pubaccess_range:AllocRange,
58
+
/// `None` means that this is an implicit access to the entire allocation
59
+
/// (used for the implicit read on protector release).
60
+
pubaccess_range:Option<AllocRange>,
56
61
/// The transition recorded by this event only occured on a subrange of
57
62
/// `access_range`: a single access on `access_range` triggers several events,
58
63
/// each with their own mutually disjoint `transition_range`. No-op transitions
@@ -123,7 +128,17 @@ impl HistoryData {
123
128
// NOTE: `transition_range` is explicitly absent from the error message, it has no significance
124
129
// to the user. The meaningful one is `access_range`.
125
130
let access = access_cause.print_as_access(is_foreign);
126
-
self.events.push((Some(span.data()),format!("{this} later transitioned to {endpoint} due to a {access} at offsets {access_range:?}", endpoint = transition.endpoint())));
131
+
let access_range_text = match access_range {
132
+
Some(r) => format!("at offsets {r:?}"),
133
+
None => format!("on every location previously accessed by this tag"),
134
+
};
135
+
self.events.push((
136
+
Some(span.data()),
137
+
format!(
138
+
"{this} later transitioned to {endpoint} due to a {access} {access_range_text}",
139
+
endpoint = transition.endpoint()
140
+
),
141
+
));
127
142
self.events
128
143
.push((None,format!("this transition corresponds to {}", transition.summary())));
0 commit comments