Min-rfs induced by Pthread_create and Pthread_join

[ThomasHaas]

The encoding we use for thread creations involves creating write-read-pairs. While our encoding does not strictly enforce a spawned thread to actually run (i.e. read the write that activates it), it is reasonable to assume that it always does as this should only ever increase the possibility for violations if the CAT is not totally strange. We might also argue, that the fact that we allow a spawned thread to not run at all, is unintended to begin with. Either way, if we go with this assumption, the write-read-pairs created by Pthread_create and Pthread_join may induce must-edges for rf that statically induce some ordering between the creating and the created thread. Furthermore, once we have disabled sets working, this can potentially disable init-reads in the spawned thread if the creating thread performed proper initialization (as every UB-free C-program should) and the alias analysis was accurate enough.

[ThomasHaas]

As an alterantive to all this, we may also avoid using rf-edges to synchronize threads altogether and instead use po-edges directly. To make this work, we would need to add a cf-condition to the starting event of the spawned thread so that it only executes if its corresponding pthread_create gets called (cf(thread_start) <=> exec(pthread_create)). pthread_join can be handled similarly. Po-edges generally cause less synchronization than rf-edges under weak memory models. However, our translation surrounds the important events with additional fences which should force the expected orderings.

The advantages are obvious: We avoid encoding expensive read and write events and we then can also get rid of all the extra addresses associated with thread creation. However, we introduce the following problems:

• po relates events of different threads (not a problem in itself, but we need to make sure that this does not cause unexpected behavior)
• po is either not static or not transitive anymore. To see this, consider the following code

bool a = nondet_bool();
if (a) { pthread_create(&t1); }
x = 5;
if (!a) { pthread_create(&t1); }

Every execution will contain x=5 and also the init-event of t1. However, we have a po-edge IFF a==false, hence the po-edge is not static. If we do not force transitivity however, we still can make po static.

• The previous point begs the next question: Which events do we actually relate via po? The related events must be visible to the CAT for otherwise any po-edges will be invisible. For architectures that have fences, we may simply add a fence as the first event of the spawned thread and then connect the fences via po. However, for e.g. SC this won't work. Maybe we should have a fictional empty fence event that is visible but has no semantics under any WMM. It only serves as a point of connection for po. Alternatively, we could always choose to connect the most recent mem-event of the spawning thread with the first mem-event of the spawned thread. This, however, introduces non-static behaviour again as the notion of "most recent / first" is not static either (due to possible conditional executions affecting this).

Overall: If we take this approach, we should probably try to keep transitivity and abandon staticity as transitivity is generally assumed by all WMMs. To achieve transitivity (or more correctly: totality), we would need to add clock constraints to po just like we do for co, which makes the encoding more expensive again. But this approach is also used by CBMC and Deagle and they seem to be quite efficient in that regard. Either way, we are trading co/rf-edges and additional locations with a more complicated po-encoding. The po-encoding is probably still more efficient than whatever we did before and it furthermore allows a lot more optimizations.

[hernanponcedeleon]

@ThomasHaas is this one implemented already?

[ThomasHaas]

The must-rf edges for pthread_create are definitely there. I also implemented them for pthread_join at some point but IIRC I removed those because of some issues. I think we can consider this as completed.