Fix UB checking for Mutex misusage

[vakaras]

The relevant discussion on the PR:
#1362 (comment)

[RalfJung]

So what we have to do is quite clearly shown in this table: releasing a mutex owned by another thread, and acquiring a mutex we already own, is UB for a "DEFAULT" mutex. The former is also UB for a NORMAL mutex.

The hard thing will be to distinguish DEFAULT from NORMAL for the relock check, as they have the same value. We'll likely have to use a trick similar to what glibc did to achieve the same.

[vakaras]

The hard thing will be to distinguish DEFAULT from NORMAL for the relock check, as they have the same value. We'll likely have to use a trick similar to what glibc did to achieve the same.

Is the glibc trick sound? If I implemented that trick and someone created a mutex by passing in PTHREAD_MUTEX_DEFAULT, then that mutex would be assumed to be PTHREAD_MUTEX_NORMAL and, as a result, we would not report UB. Would not it be better to always report UB even though in some cases it would be a false positive?

[RalfJung]

Well, glibc basically says that the following two programs are not equivalent:

let mut mutex: libc::pthread_mutex_t = std::mem::zeroed();
libc::pthread_mutex_init(&mut mutex as *mut _, std::ptr::null());

and

let mut mutexattr: libc::pthread_mutexattr_t = std::mem::zeroed();
libc::pthread_mutexattr_init(&mut attr as *mut _);
libc::pthread_mutexattr_settype(&mut mutexattr as *mut _, libc::PTHREAD_MUTEX_DEFAULT);
let mut mutex: libc::pthread_mutex_t = std::mem::zeroed();
libc::pthread_mutex_init(&mut mutex as *mut _, &mutexattr as *const _);

The former creates a mutex where relocking is UB, the latter creates one where relocking is a deadlock.

If I implemented that trick and someone created a mutex by passing in PTHREAD_MUTEX_DEFAULT, then that mutex would be assumed to be PTHREAD_MUTEX_NORMAL and, as a result, we would not report UB.

That's the thing, if you call settype with PTHREAD_MUTEX_NORMAL you get a mutex where it is not UB.

Btw, I am not sure what glibc would do for this:

let mut mutexattr: libc::pthread_mutexattr_t = std::mem::zeroed();
libc::pthread_mutexattr_init(&mut attr as *mut _);
let mut mutex: libc::pthread_mutex_t = std::mem::zeroed();
libc::pthread_mutex_init(&mut mutex as *mut _, &mutexattr as *const _);

But to be on the safe side I'd say this is also a "relock is UB" mutex.

[vakaras]

Well, glibc basically says that the following two programs are not equivalent:

let mut mutex: libc::pthread_mutex_t = std::mem::zeroed();
libc::pthread_mutex_init(&mut mutex as *mut _, std::ptr::null());

and

let mut mutexattr: libc::pthread_mutexattr_t = std::mem::zeroed();
libc::pthread_mutexattr_init(&mut attr as *mut _);
libc::pthread_mutexattr_settype(&mut mutexattr as *mut _, libc::PTHREAD_MUTEX_DEFAULT);
let mut mutex: libc::pthread_mutex_t = std::mem::zeroed();
libc::pthread_mutex_init(&mut mutex as *mut _, &mutexattr as *const _);

The former creates a mutex where relocking is UB, the latter creates one where relocking is a deadlock.

I understand that this is how the glibc implementation behaves. However, this is just one of the possible behaviours allowed by the (POSIX) documentation and also not the most conservative one, or am I missing something? In other words, would not be better to rely only on the documentation and always assume the worst possible case that is allowed by the documentation in that situation?

By the way, in both cases when relocking happens, we would get an immediate error and the only difference would be whether the error is UB or a deadlock.

If I implemented that trick and someone created a mutex by passing in PTHREAD_MUTEX_DEFAULT, then that mutex would be assumed to be PTHREAD_MUTEX_NORMAL and, as a result, we would not report UB.

That's the thing, if you call settype with PTHREAD_MUTEX_NORMAL you get a mutex where it is not UB.

We know for sure that this is the case when PTHREAD_MUTEX_NORMAL != PTHREAD_MUTEX_DEFAULT. However, as far as I understand, when PTHREAD_MUTEX_NORMAL == PTHREAD_MUTEX_DEFAULT, the documentation does not really specify what should happen, right?

[RalfJung]

I understand that this is how the glibc implementation behaves. However, this is just one of the possible behaviours allowed by the (POSIX) documentation and also not the most conservative one, or am I missing something? In other words, would not be better to rely only on the documentation and always assume the worst possible case that is allowed by the documentation in that situation?

I think it is the most conservative. Do you have an example for how we could be even more conservative?

By the way, in both cases when relocking happens, we would get an immediate error and the only difference would be whether the error is UB or a deadlock.

Fair. But UB still has a different quality to it. We should not say "UB" when really there's just a deadlock, and vice versa.

However, as far as I understand, when PTHREAD_MUTEX_NORMAL == PTHREAD_MUTEX_DEFAULT, the documentation does not really specify what should happen, right?

It specifies that if you use PTHREAD_MUTEX_NORMAL, no matter its value, relocking is a deadlock. This table is quite specific about that.

[vakaras]

I understand that this is how the glibc implementation behaves. However, this is just one of the possible behaviours allowed by the (POSIX) documentation and also not the most conservative one, or am I missing something? In other words, would not be better to rely only on the documentation and always assume the worst possible case that is allowed by the documentation in that situation?

I think it is the most conservative. Do you have an example for how we could be even more conservative?

If I look at the table and your second example (I repeat it below), I would say that the implementation of pthread_mutex_lock is allowed to cause UB. Hence, it would be more conservative to report UB in this case.

let mut mutexattr: pthread_mutexattr_t = std::mem::zeroed();
pthread_mutexattr_init(&mut attr as *mut _);
pthread_mutexattr_settype(&mut mutexattr as *mut _, PTHREAD_MUTEX_DEFAULT);
let mut mutex: pthread_mutex_t = std::mem::zeroed();
pthread_mutex_init(&mut mutex as *mut _, &mutexattr as *const _);

By the way, in both cases when relocking happens, we would get an immediate error and the only difference would be whether the error is UB or a deadlock.

Fair. But UB still has a different quality to it. We should not say "UB" when really there's just a deadlock, and vice versa.

Fair point.

However, as far as I understand, when PTHREAD_MUTEX_NORMAL == PTHREAD_MUTEX_DEFAULT, the documentation does not really specify what should happen, right?

It specifies that if you use PTHREAD_MUTEX_NORMAL, no matter its value, relocking is a deadlock. This table is quite specific about that.

But it does also say that if a programmer uses PTHREAD_MUTEX_DEFAULT, no matter its value, it may cause UB. Since we cannot distinguish whether the programmer passed in PTHREAD_MUTEX_DEFAULT or PTHREAD_MUTEX_NORMAL, shouldn't we pick a more conservative option and always report UB?

[RalfJung]

If I look at the table and your second example (I repeat it below), I would say that the implementation of pthread_mutex_lock is allowed to cause UB. Hence, it would be more conservative to report UB in this case.

Argh, I typo'd the example... I meant to set the mutex to NORMAL. (I fixed the code now.) That one certainly is not UB, I hope we agree. And if NORMAL == DEFAULT, it follows that it's also not UB with DEFAULT.

No the example is actually what I meant, I just forgot to say that for glibc it also happens to be the case that NORMAL == DEFAULT. The conclusion remains the same though.

Miri cannot affect whether NORMAL == DEFAULT, we have to live with whatever the constants are for the target we are emulating. Thus we have to say that the 2nd program is not UB. But we can still make the first UB. I think that is the most conservative we can be.

[vakaras]

And if NORMAL == DEFAULT, it follows that it's also not UB with DEFAULT.

This is the bit that is confusing me: if NORMAL == DEFAULT, then according to the documentation should not we treat them as equivalent in all cases? Specifically, shouldn't we create new mutexes (when the type is not specified) as NORMAL instead of DEFAULT?

If we cannot because that is incompatible with what glibc does, maybe it would be best to mention in the error message that this could be a false positive because of strange glibc semantics?

[bjorn3]

The problem here is that while the specification distinguishes between the two types, the actual implementation in glibc uses the same value for both. Miri could use NORMAL as default type, but that would prevent detection of some cases of UB.

[RalfJung]

This is the bit that is confusing me: if NORMAL == DEFAULT, then according to the documentation should not we treat them as equivalent in all cases?

You are basically saying that the two snippets I posted here must clearly be equivalent, since DEFAULT is, well, the default.

I think that is a reasonable interpretation of the spec. However, the glibc people clearly disagree. And since the spec does not explicitly say that NORMAL == DEFAULT implies anything, I think it is also a (somewhat less but still) reasonable interpretation to agree with them. More importantly, this is the more conservative interpretation. And as you said yourself earlier, we should be as conservative as possible.