Handle thread joins #137
Handle thread joins #137
Conversation
This is necessary to know what threads a thread variable corresponds to, e.g. when trying to join. # Conflicts: # src/analyses/base.ml # src/analyses/mTFlag.ml # src/analyses/stackTrace.ml # src/analyses/threadAnalysis.ml
# Conflicts: # src/analyses/base.ml
# Conflicts: # src/analyses/base.ml # src/analyses/threadAnalysis.ml
Only join threads that have joined all their subthreads.
# Conflicts: # src/analyses/base.ml # src/analyses/threadFlag.ml # src/analyses/threadId.ml
# Conflicts: # src/analyses/threadAnalysis.ml # src/analyses/threadFlag.ml # src/framework/constraints.ml
…ktrace-like analysis
|
As a further experiment, I tried to move most of these threading additions out of the base analysis as well using |
|
This behaves almost identically to #130 on SoftwareSystems, which isn't surprising because there threads aren't even used. On NoDataRace it solves some extra cases that involve excluding races after joins but only 5. Maybe this still needs some additional improvements, I haven't looked into NoDataRace benchmarks that we still don't solve. |
| (* TODO: is this type right? *) | ||
| set ctx.ask gs st ret_a (Cil.typeOf ret_var) (get ctx.ask gs st a None) |
There was a problem hiding this comment.
This needs to be considered after re-adding type to set.
| (* TODO: is this type right? *) | ||
| set ctx.ask ctx.global ctx.local (eval_lv ctx.ask ctx.global ctx.local lval) (Cil.typeOfLval lval) (`Address (AD.from_var tid)) |
There was a problem hiding this comment.
This needs to be considered after re-adding type to set.
This is based on #130.
Firstly, it makes base analysis track which
pthread_tvariable corresponds to which of our own thread ID (fakevarinfo). This is required, becausepthread_jointakes that as an argument to know which thread to join. The possible thread IDs a thread variable corresponds to are stored using address sets right now.This is, however, problematic, because
pthread_tis actually an integer type, so there's a disconnect between concrete value types and abstract value types. This itself shouldn't be a problem, because if a program treats apthread_tas integer (e.g. does arithmetic), then we lose track of which thread IDs it corresponds to. The bigger issue is related to #128, which for this experiment is right now commented out (which is why the test fails) to prevent all thread ID address sets from being cast to unknown ints, making any joining impossible.Secondly, based on the previous, the thread analysis, which currently keeps locally track of created threads as a set, now handles
pthread_joinby removing the joined thread from the set. This is only done if the joined thread is unique and it has joined (by this same logic) all of its created threads when returning (i.e., its created thread set is empty at return node).The thread analysis also answers to singlethreadedness queries: if it's the main thread and it's created thread set is empty, then it's back to being single threaded. That prevents accesses from being counted again, especially at the end of main thread after other threads have been joined.
This should also mutually improve the thread uniqueness analysis itself. For example, if a thread is created and joined in the same loop iteration, then it won't be considered to be repeatedly created there, because by the time it's created again, the previous instance has been removed from the set.
Thirdly, as a bonus,
pthread_joincan now also handle thread return values (either direct or viapthread_exit).