Analysis of Thread Must Joins

[michael-schwarz]

This adds an analysis that tracks for all program points the set of must-joined (unique) thread ids.
This is hard to test now, so the two examples contain manual annotations.

This is another prerequisite for #379, but I thought it would make sense to discuss this in isolation first.

[sim642]

This is hard to test now, so the two examples contain manual annotations.

Couldn't you use this joined threads information to know when the main thread is back single threaded and have the test for something at that point, like races. Something similar to what the existing thread analysis tests.

[michael-schwarz]

Couldn't you use this joined threads information to know when the main thread is back single threaded and have the test for something at that point, like races. Something similar to what the existing thread analysis tests.

Yes, but this also requires extensively modifying both this analysis and the threadid analysis. This is because the set of created threads C currently talks only about directly created threads, so even if C \setminus J = \emptyset that does not mean we are single threaded.

In order to be able to draw that conclusion one would need to make a few modifications:

• threadid would need to record the may set of created threads at some global (e.g. [tid]) to be merged into the local state upon threadjoin, just like we do for J currently. Otherwise, I only know whether all threads I have directly created are joined back in, but do not know about the threads it may have in turn created transitively.

• Such a create set would also have to account for all threads a parent may have created before creating the current thread, and even those it (or even its ancestors) may create later. I am not sure how to efficiently accumulate such information, it would probably look a lot like what the thread analysis currently does.

For the paper, this is not necessary, as we will simply read \bot for threads that have not written to a global at all, so one does not need to know if all created threads are must joined (i.e. single threaded mode again), it suffices to have a set for which one knows that they are must joined. If they happen to be all threads that access a global, we just get \bot for the non-local writes.

I think this global C set that allows for concluding we are back in single-threaded mode, might not even be a straightforward abstraction of our local trace semantics.

It might be interesting to investigate how powerful such an analysis would be, but I think it is beyond the scope of what we want do to do for the current paper.