pthreads synchronization primitives: detect mutex/rwlock/... being moved to a different location

[RalfJung]

pthread's synchronization primitives must not be moved to a different location once they were initialized. However, Miri does currently not catch that kind of UB. We probably want a fundamentally different implementation of these primitives to detect such bugs -- instead of storing data in the memory that is occupied by pthread_mutex_t et al, we use the address of the pthread_mutex_t as the key into some table for managing the lock.

This would also avoid having to figure out which "offsets" inside pthread_mutex_t to use on which OS to do what... we'd entirely stop caring about the layout of pthread_mutex_t. So this is a better way to achieve FreeBSD support for the pthread primitives as well.

• mutex
• rwlock
• condvar

[RalfJung]

The macOS os_unfair_lock could also use this infrastructure to either abort execution when a lock is moved while locked, or implement behavior that matches the real OS.

[Mandragorian]

Would this be possible to do by storing the original address in memory with pthread_mutex_t and check if it has changed? Not sure how changing the miri layout of a type interferes with what the program actually sees. (I assume that since pointers have provenance information stored with them this might not be an issue though?)

This doesn't have the benefit of simplifying the code, but might be a less invasive change.

[RalfJung]

Some scheme like that could work, but it doesn't seem worth the effort to me. (Also not sure what your comment about provenance is meant to say.)

Probably the least invasive version of this is to store just the MutexId (etc) in the pthread_mutex_t, and then in the global mutex map store the address we are expecting this mutex to be at (and any other information, like the mutex kind). After all, we still need to store something inside the pthread_mutex_t to support the static initializers.

[Mandragorian]

regarding provenance comment: I wasn't sure if how miri represents type in the machine's memory might conflict with the expected layout for a type. Like if we added that extra field that stores the original address the type layout would have changed. And I remembered that provenance already does something similar, if I understand correctly, where it doesn't just store the address that a pointer holds, but also provenance information. I was basically trying to prove to myself that adding metadata to a type is fine.

If there already exists such a map, then yes, storing the metadata to it is probably the simplest way, yes.

I will need to read the code more to understand what needs to happen but from your commends and some initial reading I think I could give this a shot if there is interest.

Thanks for the answers!

[RalfJung]

There are several misconceptions here about how Miri works: there are no types in memory, only raw bytes. And we can never add more fields or anything like that, pthread_mutex_t has a certain size and that's the number of bytes we can use to store data in-place. We can do basically anything we want with these bytes, ignoring what they are used for "normally" on that platform, because users are supposed to treat pthread_mutex_t entirely opaquely. And yes provenance exists as "metadata" stored next to bytes, but that is a deeply invasive thing to add to the language with observable consequences, so we cannot put any other metadata there, it can only be used for provenance.

[Mandragorian]

I have some code for this but before I send anything stupid for review I have 2 questions:

• Regarding the mutex kind: From what I understand, static initializers set the kind of the mutex. So lock, trylock and unlock should always try to retrieve it from the bytes pointed by mutex_op. Doesn't this mean that we can't store the kind in some global map, and we need to keep storing it in the pthread_mutex_t?

• Do we want a new TerminationInfo variant? I see that there is a dedicated variant for data race detection, so we could have an IllegalMove variant?

[RalfJung]

Regarding the mutex kind: From what I understand, static initializers set the kind of the mutex. So lock, trylock and unlock should always try to retrieve it from the bytes pointed by mutex_op. Doesn't this mean that we can't store the kind in some global map, and we need to keep storing it in the pthread_mutex_t?

What I imagined was lazy initialization: there's a flag in the pthread_mutex_t value that indicates "has been initialized", and we ensure that it indicates "no" for all the static initializers. All lock operations begin by checking that flag, and then if it is not yet initialized, registering a mutex at that address, with the mutex kind as given by the static initializer, and setting the flag. Explicit initialization with pthread_mutex_init immediately sets this flag.

Do we want a new TerminationInfo variant? I see that there is a dedicated variant for data race detection, so we could have an IllegalMove variant?

That should not be needed, throw_ub_format should be sufficient. Data races do a bunch of special things for nicer errors, which is why they need their own variant.

[RalfJung]

For the initial PR, it's probably best to only convert one of the primitives, like mutex. :)

[Mandragorian]

This can't be closed yet. The above mentioned commit only implements the move detection for mutexes.

[RalfJung]

Ah, good point.

I moved the macos version of this into a separate issue: #3859.

[RalfJung]

I think condvar is the only one that's missing now, right?

[Mandragorian]

Yes. I started to prepare a PR a few days ago, but then life got a bit busy. I need to add a test and polish it a bit.