Topic: Stacked borrows
Compiler, Lang — Unsafe Code Guidelines
Key People
Wednesday, 09:00-11:00
Meeting Style

Homework to do before meeting
  • Read Ralf’s blog posts
  • Discuss Stacked Borrows model and some of its implications
  • Explain basic idea
  • Consequences for libstd
  • Discuss 2PB + NLL interactions
  • Maybe record?


[review of examples from blog posts]
  • purpose: introduce more undefined behavior (but all safe code continues to not have UB)
  • code using &mut _ rejected; analogous code using casts of &mut  tounsafe pointers is accepted but the stacked borrows system today rejects it dynamically (developer observable via const-evaluation expressions), thus providing evidence of UB.
  • felix: what if you go straight to a raw pointer? [discussion followed, then deferred]
  • (other discussion clarifying that Shr is describing a raw *const/*mut pointer; not necessarily &T)
  • cramertj: what if you do let y = &x as *const _ as *mut _ and then have a write to *y, even if there are no other references to x?
  • ralfj: to first approximation, that is always undefined behavior
  • (but we discovered a playpen that seems to contradict that claim; but that is likely to be a bug in the implementation)
  • ralfj: We keep timestamps to enforce the property that frozen things have been frozen “long enough” (or “continuously”) — it is not legal to unfreeze something and then refreeze it later and expect it to work
  • ralfj: one gotcha: we don’t distinguish raw pointers. So if you have one raw pointer to a location that you created via casting one reference that is now invalid, and create a new valid raw pointer to that same location, then the first raw pointer [magically?] becomes valid again…

[discussion of implemetation linked above]

[discussion of libstd impact linked above]

ralfj: regarding this example there is no easy solution in terms of hypothetical compiler lints. The biggest red flag is the cast from a *const _ to *mut _ but you cannot see the input *const _ type from reading the surface source code. The fact that as does not allow one to make the input type explicit may be a footgun in many cases here.

additional discussion of

Two Phase Borrows

let mut v = vec![];
v.push(v.len()); // UB under model as described so far