Implementation of pthread_cond

[db7]

It seems that the current implementation of pthread_cond does not properly capture cases where one would forget to signal or broadcast the waiters.

The implementation of pthread_cond_signal points to pthread_cond_brodcast. The implementation of pthread_cond_broadcast is empty. The implementation of pthread_cond_wait is a pthread_mutex_unlock(); pthread_mutex_lock();. That is actually quite simple and nice. It can already capture some issues. But as said above, it actually always enventually wake up every waiter.

[ThomasHaas]

I remember that we were puzzled a lot about those pthread_cond_signal/broadcast/... functions.
IIRC, the conclusions was that (according to spec) spurious wakeups are always(!) possible and that is why signaling/broadcasting never have to do anything because in any execution where they would actually signal someone, you could have an alternative execution where the thread would just spuriously wake up instead.

Now I assume that you talk from a more practical point of view where you do not want to rely on spuriousness to argue about termination, right? Do you have a concrete example in mind where you expect Dartagnan to give a different result?

EDIT: Maybe I should also add that our support for pthread has many holes, especially when it comes to attributes (e.g. mutex_attr) and error codes.

[db7]

I remember that we were puzzled a lot about those pthread_cond_signal/broadcast/... functions. IIRC, the conclusions was that (according to spec) spurious wakeups are always(!) possible and that is why signaling/broadcasting never have to do anything because in any execution where they would actually signal someone, you could have an alternative execution where the thread would just spuriously wake up instead.

Well, yes and no. The spec says that spurious wake ups are possible, but I don't think that "always" should be understood with "eventually always" or something, ie, that if you just wait enough all waiters have to be waken up. So I think that the situation of having N waiters and sending a N-1 signals should trigger a deadlock error.

The real implementation of the signal might just always do broadcasts, yes, but for the verification we need to check the other case.

EDIT: Maybe I should also add that our support for pthread has many holes, especially when it comes to attributes (e.g. mutex_attr) and error codes.

No worries here. I think one can live with that.

[ThomasHaas]

I totally understand that for liveness issues you don't want to have a "fairness assumption" about spurious wakeups, i.e., just because one thread can spuriously wake up infinitely many times, it actually has to do so.

I'm not sure how to model this yet. For single signals, it would be fine to have each thread spin in a CAS-loop that waits for a signal and atomically consumes it.
But then I don't know how broadcasts would work or spurious wakeups. I think a fundamental issue is the conflict between liveness and safety here: for liveness verification you want no spurious wakeups at all but for safety verification you only want spurious one's.
Maybe we need a verification-goal specific rewrite? Well, I need to think about this more.