TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist #3742

Vanille-N · 2024-07-09T13:29:38Z

As discovered by @JoJoDeveloping, the result of having both Protector exceptions on lazy locations (protectors only protect initialized bytes) and interior mutability exceptions for protected tags (Reserved IM does not accept foreign writes when protected) leads to some very undesirable results, namely that we cannot do spurious writes even on protected activated locations.

We propose that Protected Reserved IM should no longer exist and instead when a type is retagged as part of a FnEntry it is assumed to lose interior mutability.

In fact, this was already being done implicitly because relevant transitions were guarded by an if protected, but the difference is that now it also applies to transitions that occur after the end of the protector.

src/borrow_tracker/tree_borrows/mod.rs

tests/fail/tree_borrows/reservedim_spurious_write.rs

RalfJung · 2024-07-09T14:35:33Z

tests/fail/tree_borrows/reservedim_spurious_write.rs

+
+fn example(spurious: bool) {
+    // For this example it is important that we have at least two bytes
+    // because lazyness is involved.


Why does that need two bytes? You can have 1 byte and an &() reference, and then laziness is still visible, no?

But () is not interior mutable. In general, using ZSTs here suggests the counterexample relies on "wonky" ZST semantics, even worse if we cook up an Interior mutable ZST type (UnsafeCell<()>), because what does that even mean? It would make the thing actually happening here much more obscure. And also, the counterexample is independent of whatever happens at ZST retags. It still occurs when the language has no notion of zero-sized objects at all.

What makes an UnsafeCell<()> accessed outside its range more wonky than an UnsafeCell<u8> outside its range?

The counterexample is independent of what happens in one of the two bytes that you have here, so having both bytes is somewhat confusing. It's not about zero-sized objects, it's about a reference that only has "lazy" accesses.

Because if you have an array of UnsafeCell<u8> and go to the next element you naturally do an actual memory access, but if you iterate an array of UnsafeCell<()> you're actually doing no memory accesses at all.

Oh I think I just understood the point. We wouldn't have two elements, we'd just have one single Cell<u8> that we retag as &mut *(r as *Cell<u8> as *Cell<()>) as *mut Cell<()> as *mut Cell<u8> I guess ?

@JoJoDeveloping not sure why array iteration would suddenly be relevant?

@Vanille-N yes.

I believe that @JoJoDeveloping interpreted your comment "you can have 1 byte and a &() reference" similarly to what I first did. Initially I thought you were arguing for using (Cell<()>, Cell<u8>) rather than [Cell<u8>; 2] but actually it would just be a single Cell<u8>.

Yes I disagree with it being a single byte allocation.

I don't understand your reasoning for that. There's a single byte that's actually relevant for this, and all this mucking about with shifting the pointer back and forth is a distraction. The key point is that the relevant byte is not inside the range that is initialized upon reborrow.

tests/fail/tree_borrows/reservedim_spurious_write.rs

- split test into two revisions - clarify comments

Vanille-N · 2024-07-10T06:25:22Z

Btw the exhaustive tests need to be updated, but it's a bit more work because now not all configurations are valid as initial permissions. There's nothing incorrect right now because we're just testing more configurations.
When we do update the tests we'll be able to simplify the state machine so that foreign_write no longer depends on protected.

RalfJung · 2024-07-10T06:41:23Z

When we do update the tests we'll be able to simplify the state machine so that foreign_write no longer depends on protected.

foreign_read still depends on it though I assume? But magically that actually does not cause problems?

Vanille-N · 2024-07-10T06:44:14Z

foreign_read still depends on it though I assume? But magically that actually does not cause problems?

foreign_read needs protected to know if Active becomes Frozen or Disabled.
foreign_write still implicitly depends on protected, but because !ty_is_freeze implies !protected the dependency kind of disappears in the implementation of the transition itself.

JoJoDeveloping · 2024-07-10T12:07:00Z

magically that actually does not cause problems

It does indeed not caue problems. The only other place it's relevant is on Active nodes, and there the protectors ending causes a write event (introduced in #3732). And nothing (protected) survives foreign writes.

tests/fail/tree_borrows/reservedim_spurious_write.rs

RalfJung · 2024-07-11T09:29:26Z

Test LGTM now, thanks!

Btw the exhaustive tests need to be updated, but it's a bit more work because now not all configurations are valid as initial permissions. There's nothing incorrect right now because we're just testing more configurations. When we do update the tests we'll be able to simplify the state machine so that foreign_write no longer depends on protected.

What is the plan with this? Should it happen in this PR or a future PR?

Co-authored-by: Ralf Jung <post@ralfj.de>

Vanille-N · 2024-07-12T08:57:34Z

Worth noting that now conflicted and ty_is_freeze are not orthogonal: maybe instead of (bool, bool) we should have a 3-variant enum (Activable | Conflicted | InteriorMut).
That and optimizing the exhaustive tests could be done simultaneously, probably in a different PR.

RalfJung · 2024-07-12T13:52:01Z

It seems fine to not do that in this PR, but then please leave a FIXME at the relevant place(s) in the code.

RalfJung · 2024-07-16T05:55:03Z

LGTM, thanks!
@bors r+

bors · 2024-07-16T05:55:06Z

📌 Commit c0c1028 has been approved by RalfJung

It is now in the queue for this repository.

bors · 2024-07-16T06:11:08Z

⌛ Testing commit c0c1028 with merge b11f82b...

bors · 2024-07-16T06:35:12Z

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing b11f82b to master...

Make unused states of Reserved unrepresentable In the [previous TB update](#3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable. This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable. As such it is desirable that this state would also be unrepresentable. This PR eliminates the unused configuration by changing ```rs enum PermissionPriv { Reserved { ty_is_freeze: bool, conflicted: bool }, ... } ``` into ```rs enum PermissionPriv { ReservedFrz { conflicted: bool }, ReservedIM, ... } ``` but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed. In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag. Currently waiting for - `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris, - `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.

Make unused states of Reserved unrepresentable In the [previous TB update](rust-lang/miri#3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable. This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable. As such it is desirable that this state would also be unrepresentable. This PR eliminates the unused configuration by changing ```rs enum PermissionPriv { Reserved { ty_is_freeze: bool, conflicted: bool }, ... } ``` into ```rs enum PermissionPriv { ReservedFrz { conflicted: bool }, ReservedIM, ... } ``` but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed. In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag. Currently waiting for - `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris, - `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.

Vanille-N added 2 commits July 9, 2024 14:24

This pattern using lazy protected Reserved IM prevents spurious writes

1eba725

Implement fix for reservedim_spurious_write: ignore IM on protected

23e8252

RalfJung reviewed Jul 9, 2024

View reviewed changes

JoJoDeveloping mentioned this pull request Jul 9, 2024

Tree Borrows: Two-phase borrows + interior mutability have surprising interactions rust-lang/unsafe-code-guidelines#501

Open

Apply suggestions

65e7669

- split test into two revisions - clarify comments

Second byte is not involved in the example; use a Cell<()> instead

4d384b4

RalfJung reviewed Jul 11, 2024

View reviewed changes

tests/fail/tree_borrows/reservedim_spurious_write.rs Outdated Show resolved Hide resolved

Clarify comment in tests/fail/tree_borrows/reservedim_spurious_write.rs

3d84161

Co-authored-by: Ralf Jung <post@ralfj.de>

Leave a trace of the current suboptimal status of foreign_write

c0c1028

bors merged commit b11f82b into rust-lang:master Jul 16, 2024
8 checks passed

Vanille-N mentioned this pull request Jul 18, 2024

Make unused states of Reserved unrepresentable #3754

Merged

JoJoDeveloping mentioned this pull request Aug 7, 2024

[Tree Borrows] Full Tree Borrows Support minirust/minirust#221

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist #3742

TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist #3742

Vanille-N commented Jul 9, 2024

RalfJung Jul 9, 2024

JoJoDeveloping Jul 9, 2024 •

edited

Loading

RalfJung Jul 9, 2024 •

edited

Loading

JoJoDeveloping Jul 9, 2024

Vanille-N Jul 10, 2024

RalfJung Jul 10, 2024

Vanille-N Jul 10, 2024

JoJoDeveloping Jul 10, 2024

RalfJung Jul 10, 2024

Vanille-N commented Jul 10, 2024

RalfJung commented Jul 10, 2024

Vanille-N commented Jul 10, 2024

JoJoDeveloping commented Jul 10, 2024 •

edited

Loading

RalfJung commented Jul 11, 2024

Vanille-N commented Jul 12, 2024

RalfJung commented Jul 12, 2024

RalfJung commented Jul 16, 2024

bors commented Jul 16, 2024

bors commented Jul 16, 2024

bors commented Jul 16, 2024

TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist #3742

TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist #3742

Conversation

Vanille-N commented Jul 9, 2024

RalfJung Jul 9, 2024

Choose a reason for hiding this comment

JoJoDeveloping Jul 9, 2024 • edited Loading

Choose a reason for hiding this comment

RalfJung Jul 9, 2024 • edited Loading

Choose a reason for hiding this comment

JoJoDeveloping Jul 9, 2024

Choose a reason for hiding this comment

Vanille-N Jul 10, 2024

Choose a reason for hiding this comment

RalfJung Jul 10, 2024

Choose a reason for hiding this comment

Vanille-N Jul 10, 2024

Choose a reason for hiding this comment

JoJoDeveloping Jul 10, 2024

Choose a reason for hiding this comment

RalfJung Jul 10, 2024

Choose a reason for hiding this comment

Vanille-N commented Jul 10, 2024

RalfJung commented Jul 10, 2024

Vanille-N commented Jul 10, 2024

JoJoDeveloping commented Jul 10, 2024 • edited Loading

RalfJung commented Jul 11, 2024

Vanille-N commented Jul 12, 2024

RalfJung commented Jul 12, 2024

RalfJung commented Jul 16, 2024

bors commented Jul 16, 2024

bors commented Jul 16, 2024

bors commented Jul 16, 2024

JoJoDeveloping Jul 9, 2024 •

edited

Loading

RalfJung Jul 9, 2024 •

edited

Loading

JoJoDeveloping commented Jul 10, 2024 •

edited

Loading