Analysis of `pthread_cond`

[michael-schwarz]

Pthreads uses condition variables or synchronization (e.g. signal,broadcast,wait, ...). So far we do not really do anything meaningful for them, however there are some possible uses:

• Detecting more Dead Code

  • The most trivial case is that we can determine that a condition variable cv is never signaled, making everything past pthread_cond_wait(cv) dead.
  • The threads that can signal cv are all:
    • (transitively) started by the current thread after its pthread_cond_wait(cv).
    • (transitively) joined before this pthread_cond_wait(cv) is reached, thus meaning they can not be the signaler

• Improving Race Detection

  • Combined with our MHP information, one can exclude races for threads t1 and t2 where t2 has observed signal (Must-Received) cv and all the threads signalling cv are not started at this location in t1 yet. If one additionally collects May-Sent-Signal sets, one can also exclude cases where t1 is the one that will signal but has not reached that program point yet.

• Improving Privatization

  • Investigate to what extent privatization can benefit from this, I have not yet found a convincing use case there.

Things that are TODO here:

• [ ] Raising Deadcode during special for pthread_cond_wait does not work, probably related to the split and event business in mutexAnalysis.ml. Any ideas there @sim642?
• [ ] Cleanup MHP code when #518 lands
• [ ] Implement the Race Detection part of this PR
• [ ] Dream up improved Privatization schemes

[sim642]

• Raising Deadcode during special for pthread_cond_wait does not work, probably related to the split and event business in mutexAnalysis.ml. Any ideas there @sim642?

You would just conditionally have to not make the ctx.split calls. Then no splits are created and raise Deadcode makes it truly dead.

EDIT: Sorry, I see what you mean now. I was looking at the mutex analysis where the splits are made, but you mean making it dead from another analysis. I think you could achieve that by adding a new event like CondWait, changing mutex analysis to split with a list of three events: [CondWait; Unlock; Lock]. In your analysis you'd handle CondWait (and based on something raise Deadcode, which should work there). The other analyses would ignore CondWait and just see the Unlock-Lock (in case your analysis didn't make it dead) and the privatizations should still be sound thanks to that. Or alternatively I guess one could handle CondWait in base and apron directly (instead of Unlock and Lock) by calling both in order.

[michael-schwarz]

Improving Race Detection

Actually, I am starting to wonder if improving the Race Detection with this information is actually something that we want to do. The standard allows for spurious wakeups, so if a race is only excluded due to these conditions on condition variables, the race is still there in fact (!).

So maybe this information should be computed, but the race still reported with something such as (condition variable v does not prevent races due to spurious wakeup).

And for the reporting of code as dead, probably a warning should be generated that says only alive due to spurious wakeup or something... At least there should be an option to toggle how we handle spurious wakeups.

[michael-schwarz]

I would propose to leave the TODOs as is for now, as we have thus far not come up with a convincing use case yet.

We can already detect an interesting class of bugs with this analysis, namely code that is only alive due to spurious wakeup, which already is an interesting concurrency bug.

[michael-schwarz]

I switched the analysis to use the full power of MHP. This is both more powerful, and allows removing a lot of duplicated code.

I made the assumption that only few signals typically happen in programs for a given condition variable and that correspondingly the sets of MHP information at globals do not get too large. If this turns out to be problematic, one could go for HoareSet of MHP information.