Should I change the race tests to look for race detected? Matching the entire string as they currently do seems quite redundant.

This is great, I was just thinking that we should finally tackle this issue. :)

In terms of interface, I would suggest to simply extend the existing read with an NaReadType parameter. I don't quite see why we'd want functions like assert_immutable_memory, that just makes the API surface one has to understand so much bigger. (I see for write we have this internal unique_access function; I think it'd be fine to remove this and just rename unique_access to write and expose that. In fact na_read and na_write or non_atomic_read/non_atomic_write would probably be better.)

In terms of wording, "shared reference invariant on thread" does not make a lot of sense to me. I would say something like "implicit non-atomic read due to retag". (Cc @saethlin in case you have better ideas)

Should I change the race tests to look for race detected? Matching the entire string as they currently do seems quite redundant.

The point of these tests is to ensure that we call out the right thread names and access types. So just saying "race detected" would risk regressions of those aspects.

I am surprised that there are so many test failures, even for tests that involve actual accesses. Take for instance the classic read_write_race.rs:

  -error: Undefined Behavior: Data race detected between (1) non-atomic read on thread `unnamed-ID` and (2) non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here
  +error: Undefined Behavior: Data race detected between (1) some potential non-atomic read access on thread `unnamed-ID` and (2) 4-byte non-atomic write on thread `unnamed-ID` at ALLOC. (2) just happened here

That is a completely different error. It now started mentioning the access size as well, and what is "some potential access"? There's a very clear non-atomic read access in the source. So something is definitely wrong with the diagnostics here.

implicit non-atomic read due to retag

I do find calling it a read quite confusing. I did initially go looking for a real read operation when I found a race, which is what promted the PR.

The point of these tests is to ensure that we call out the right thread names and access types. So just saying "race detected" would risk regressions of those aspects.

The usage in rustc is more to have the .stderr catch such regressions and the test source code just ensures the right kind and location.

It now started mentioning the access size as well

I fixed that now.

and what is "some potential access"

Maybe calling it "read or retag" is better? Tracking the information on reads would be nicer, but I don't know where to do that.

I do find calling it a read quite confusing. I did initially go looking for a real read operation when I found a race, which is what promted the PR.

This is the common terminology. These are reads, they are just implicit side-effects of retags rather than explicit in the source.

Calling it an "invariant" doesn't even make semantic sense. An invariant is a property that is maintained throughout execution. We're not talking about a property here but about an operation.

The usage in rustc is more to have the .stderr catch such regressions and the test source code just ensures the right kind and location.

I don't agree, in rustc we also use the annotations to ensure that the right things show up in the message. Otherwise we'd just use //~ERROR and never //~ERROR: message.

Maybe calling it "read or retag" is better? Tracking the information on reads would be nicer, but I don't know where to do that.

Why does "unknown" even happen? "read or retag" will be even more confusing for the common case where it is a regular read.

they are just implicit side-effects of retags rather than explicit in the source.

Maybe calling them speculative reads would be better?

Why does "unknown" even happen?

We only know the read type on the current thread, not on the other conflicting operation, so I wanted a hint to the user that it could be either.

Maybe calling them speculative reads would be better?

Hm... that sounds a bit like what CPUs are doing, which is unrelated. OTOH these reads are indeed related to the compiler's ability to insert read (or write) operations. So maybe the term makes sense. But then we should also use it for the aliasing errors (eventually, not in this PR).

@rust-lang/miri any opinions on terminology here?

We only know the read type on the current thread, not on the other conflicting operation, so I wanted a hint to the user that it could be either.

That sounds like it could cause a lot of confusion. Is there any way we can store that one bit of information (implicit/speculative read vs explicit read) somehow so that it is available later when computing the error? We already store an entire span, storing one more bit can't be so bad...

Hm... that sounds a bit like what CPUs are doing, which is unrelated. OTOH these reads are indeed related to the compiler's ability to insert read (or write) operations. So maybe the term makes sense

Speculative retag reads or retag reads could also be options that relates them back more to the borrow model.

Is there any way we can store that one bit of information (implicit/speculative read vs explicit read) somehow so that it is available later when computing the error?

Very likely, but I wasn't able to locate where it would go. The span logic seemed quite weird to me with it's handling of dummy spans too.

"retag read" also works for me, though using "retag" as an adjective seems a bit odd.

Very likely, but I wasn't able to locate where it would go. The span logic seemed quite weird to me with it's handling of dummy spans too.

VTimestamp probably needs a bool that indicates whether the read is "real" or not. That should likely be packed into time to avoid making it 4 bytes bigger.

I think our diagnostics should be informative for people who were completely unaware of this property of references until seeing the error. If we call them something like "a speculative retag read" we should provide a link or some other kind of reference to documentation that explains what that terminology refers to, or a separate help: message that says something like:

help: Retags permit optimizations that insert speculative (or hoisted) reads/writes. Therefore from the perspective of aliasing and data race invariants, a retag has the same implications as a read/write.

Tweaking the wording of that message:

help: Retags permit optimizations that insert speculative (or loop-hoisted) reads/writes. Therefore from the perspective of aliasing and data race models, a retag has the same implications as a read/write.

Or maybe "restrictions" instead of "models"? I don't like the use of "invariants" there, that's a specific technical term and this is too far outside its regular meaning.

"retag read" also works for me, though using "retag" as an adjective seems a bit odd.

Could we put an adjective in front of "retag" instead? "shared retag" and "unique retag"? That makes it more clear that there's no correspondence to reads in the source code.

Note that whether unique retags are reads or writes depends on the aliasing model (in SB they are writes, in TB reads).

Is the idea that you would the entirely relegate the explanation that "shared retag" means a form of read into the help? That would also work for me.

Further editing on the help text, since it is specifically for data races so I think we can remove the "aliasing model" part:

help: Retags permit optimizations that insert speculative (or loop-hoisted) reads/writes. Therefore from the perspective of data races, a retag has the same implications as a read/write.

Note that whether unique retags are reads or writes depends on the aliasing model (in SB they are writes, in TB reads).

I stuck with retag read and retag write then. It's useful from the data race perspective to know if they're reads or writes.

I like the wording you just pushed.

@rustbot author

Just one final tweak of the message. Then please squash all the commits.

Looks good, thanks for working through all these revisions with me. :)
Please squash, then we can land this.

@bors r+

📌 Commit 3cf20a2 has been approved by RalfJung

It is now in the queue for this repository.

⌛ Testing commit 3cf20a2 with merge 3670823...

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