Address reuse improvements and fixes

[RalfJung]

• when an address gets reused, establish a happens-before link in the data race model
• do not reuse stack addresses, and make the reuse rate configurable

Fixes #3450

[RalfJung]

@bors r+

[bors]

📌 Commit 2049ee7 has been approved by RalfJung

It is now in the queue for this repository.

[bors]

⌛ Testing commit 2049ee7 with merge 22895df...

[RalfJung]

Ah... this makes the weak memory emulation basically disappear. We do so much reuse even of stack variables that it is almost guaranteed that you pick up some address from another thread, and therefore synchronize with it...

[bors]

💥 Test timed out

[RalfJung]

I excluded stack allocations from reuse, and made the reuse rate configurable.

@bors r+

[bors]

📌 Commit f3b31c3 has been approved by RalfJung

It is now in the queue for this repository.

[bors]

⌛ Testing commit f3b31c3 with merge ab25a33...

[RalfJung]

This actually still has a quite significant impact on data race detection; I suspect this is due to heap allocations in the thread spawning logic. I'm not sure what the best way forward is here... other than reducing the reuse rate drastically. With a reuse rate of 25%, the simple data race I checked is still found around 70% of the time (but it's 100% without reuse). With the default reuse rate it's about 40% detection rate for data races.

I think the rate will be better with real programs; the issue is that in these tests the threads exist only for a very short time so there's a real chance it never gets preempted and so the first thread is done before the second thread starts, and therefore allocations can be reused. If I add a simple for _ in 0..100 {} to the first thread, the data race is detected ~100% of the time even with the default address reuse rate.

We could of course also just not do any reuse across threads, then we also will never add spurious synchronization. But for heap allocations that's not real either.

[bors]

💔 Test failed - checks-actions

[RalfJung]

OTOH, real programs will also do a bunch of stuff on the heap, which again increases the chance of address reuse inducting synchronization.

My current inclination is to add some extra randomness that makes address reuse across thread boundaries a lot less likely than address reuse within a single thread.

[RalfJung]

My current inclination is to add some extra randomness that makes address reuse across thread boundaries a lot less likely than address reuse within a single thread.

That's what I now implemented with the last commit.

@rust-lang/miri what do you think? With the cross-thread reuse rate of 10%, the simple data race tests still detect the race 80% of the time when preemption is disabled (and ~100% of the time when preemption is enabled). These tests do basically nothing in their threads, so there's a significant chance the 2nd thread starts after the 1st thread is already done and then address reuse inside thread::spawn can induce synchronization.

I'm thinking maybe I should increase the regular address reuse rate to around 70%; that makes the chance that a free; malloc pair reuses the just-freed address 50% (since we roll dice both on free and on malloc, and sqrt(0.5) is close to 0.7). I previously went back down to 50% to avoid too much accidental synchronization, but now that that is a separate knob it seems fine to go up to 70%. OTOH 50% also seems fine; when doing malloc; free in a loop this means we see about N/2 different addresses in N loop iterations.

[saethlin]

With the cross-thread reuse rate of 10%, the simple data race tests still detect the race 80% of the time when preemption is disabled (and ~100% of the time when preemption is enabled).

That seems fine to me. Anyone seriously looking to find data races should have preemption enabled.

[RalfJung]

Yeah... though it's hard to say what this will do for other cases. Not sure how many people run concurrency tests in a loop in Miri to give races more than one chance to appear.

But for now, let's go ahead with this, we can always re-adjust later if we realize that data race detection has become too non-deterministic.

@bors r+

[bors]

📌 Commit 2155a30 has been approved by RalfJung

It is now in the queue for this repository.

[bors]

⌛ Testing commit 2155a30 with merge 9b36914...

[bors]

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