Skip to content

Stacked Borrows retags should also be accesses for the data race model #2648

Closed
@RalfJung

Description

@RalfJung

Currently, many Stacked Borrows retags are effectively read/write accesses for the aliasing model:

// A "safe" reborrow for a pointer that actually expects some aliasing guarantees.
// Here, creating a reference actually counts as an access.
// This ensures F2b for `Unique`, by removing offending `SharedReadOnly`.
self.access(access, derived_from, global, dcx, exposed_tags)?;

However, the data race model never hears about them, which as @JakobDegen points out leads us to accept some code that we probably should not accept.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-aliasingArea: This affects the aliasing model (Stacked/Tree Borrows)A-data-raceArea: data race detectorC-bugCategory: This is a bug.I-misses-UBImpact: makes Miri miss UB, i.e., a false negative (with default settings)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions