Use atomic RMW for {mutex, rwlock, cond, srwlock}_get_or_create_id functions

[cbeuw]

This is required for #1963

{mutex, rwlock, cond, srwlock}_get_or_create_id() currently checks whether an ID field is 0 using an atomic read, allocate one and get a new ID if it is, then write it in a separate atomic write. This is fine without weak memory. For instance, in pthread_mutex_lock which may be called by two threads concurrently, only one thread can read 0, create and then write a new ID, the later-run thread will always see the newly created ID and never 0.

    fn pthread_mutex_lock(&mut self, mutex_op: &OpTy<'tcx, Tag>) -> InterpResult<'tcx, i32> {
        let this = self.eval_context_mut();

        let kind = mutex_get_kind(this, mutex_op)?.check_init()?;
        let id = mutex_get_or_create_id(this, mutex_op)?;
        let active_thread = this.get_active_thread();

However, with weak memory behaviour, both threads may read 0: the first thread has to see 0 because nothing else was written to it, and the second thread is not guaranteed to observe the latest value, causing a duplicate mutex to be created and both threads "successfully" acquiring the lock at the same time.

This is a pretty typical pattern requiring the use of atomic RMWs. RMW always reads the latest value in a location, so only one thread can create the new mutex and ID, all others scheduled later will see the new ID.

[cbeuw]

ecx.read_scalar_at_offset_atomic(mutex_op, 4, ecx.machine.layouts.u32, AtomicReadOp::Acquire)

Why these changes? These operations should not synchronize. That should be done by the lock itself.

@RalfJung I agree, changed them back to Relaxed

[RalfJung]

This is a pretty typical pattern requiring the use of atomic RMWs. RMW always reads the latest value in a location, so only one thread can create the new mutex and ID, all others scheduled later will see the new ID.

I agree, except that this here is Abstract Machine code that runs "on the meta level" so I am somewhat surprised it needs to play by the same rules. Using interpreter memory to store the state of these things seemed like a clever idea, but maybe it wasn't...

[RalfJung]

Thanks. :-)
@bors r+

[bors]

📌 Commit 9e38dc4 has been approved by RalfJung

[bors]

⌛ Testing commit 9e38dc4 with merge 3f111c1...

[bors]

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