Thread Wrappers

[just-max]

Extends the concept of malloc wrappers to thread creation. Threads receive an ID based on the CFG node of the wrapper function's call, instead of the pthread_create call, which in the case of a wrapper is always the same node.

Closes #664.

[michael-schwarz]

We now have an issue with Duplicate test ID 66/01 here. The reason is that master got a group 66 in the meanwhile, so we should change the group number to the next free one.

[just-max]

Thanks for the reminder on this ;) I've addressed all the comments (thanks Simmo!)

There's one last problem I can't figure out: if the unique_thread_id_count is too small (e.g. set to 0 when there are two threads), Goblint should not be able to distinguish threads created at the same location. After implementing Simmo's suggestion to use fctx though, this isn't the case. See the test 71/05, which specifically checks that a race does occur if unique_thread_id_count is set to 0. This test passes before implementing the change, but fails after, and I can't figure out why Goblint considers the two threads in that test case to be distinct.

[sim642]

See the test 71/05, which specifically checks that a race does occur if unique_thread_id_count is set to 0. This test passes before implementing the change, but fails after, and I can't figure out why Goblint considers the two threads in that test case to be distinct.

When run with --enable allglobs to also see the non-racing accesses, it shows that the created threads are considered unique and thus joining "works". So Goblint actually only sees one unique thread being created (from the one location), not two. I didn't look into why that's the case though.

EDIT: It appears that the issue is in check whether the created set in threadid analysis already contains the same thread or not. If it does, then a non-unique and thus non-joinable thread should be spawned. But looks like the check is going wrong because the created threads set contains thread IDs without considering the wrapper.

[just-max]

In the wrapper function analysis' threadenter, the new thread receives a fresh view of the current wrapper node and counter. Then, when threadspawn goes to use fctx to add to the set of created threads, it adds the unwrapped node to the set of created threads.

analyzer/src/analyses/wrapperFunctionAnalysis.ml

Lines 85 to 87 in 68b2267

	let threadenter ctx lval f args =
	(* The new thread receives a fresh counter *)
	[D.bot ()]

analyzer/src/analyses/threadId.ml

Lines 100 to 103 in 68b2267

	let threadspawn ctx lval f args fctx =
	let (current, td) = ctx.local in
	let node, index = indexed_node_for_ctx fctx in
	(current, Thread.threadspawn td node index f)

I've changed threadenter in the wrapper function analysis to pass ctx.local instead of bot, but I'm not sure that's really the right approach.

[sim642]

I've changed threadenter in the wrapper function analysis to pass ctx.local instead of bot, but I'm not sure that's really the right approach.

That doesn't seem right indeed because the idea has been that each thread is handled on its own, independent of who created it.

Now looking at it, why is ThreadId.threadspawn using indexed_node_for_ctx at all? ThreadId.threadenter already computed the created thread's correct ID before the wrapper analysis' threadenter sets it to bot. Couldn't ThreadId.threadspawn just use the already computed thread ID from fctx.local?

[just-max]

The spawned thread's ID from fctx.local in ThreadId.threadspawn is a stateful thread ID (prefix-set if history is enabled), whereas the set of created threads contains just the thread creation nodes. So there's no way to directly add a node to the set given the abstract thread ID.

I've changed the ThreadId domain to also include the (wrapper) node that created the thread, so that it is available in fctx in addition to the abstract thread ID.

Alternative Idea

master...just-max:goblint-analyzer:thread_wrappers_stateful_id

Another option is: change Stateful so that it takes an abstract thread ID instead of a just a node. The prefix-set implementation uses the top element of the prefix stack for unique threads, and all the nodes in the suffix set for non-unique threads, to update the set of thread creation nodes. I'm not convinced this is a good idea though: for non-unique threads, this is quite an over-approximation.

[sim642]

I see, indeed they keep track of slightly different things. The current solution seems reasonable. It changes the domain and context for threadid analysis, so I wonder if this can have an effect on default performance. Although it shouldn't be too often that the same history thread ID set is created with a different node as the last one.

Anyway, conflicts with master still need to be resolved:

• The query number should be bumped.
• The test group number should be bumped.

[just-max]

Conflicts are resolved. Thanks again for the help getting this done!

[michael-schwarz]

Thank you @just-max, it's nice to have this feature in Goblint now!