HB-relationship involving thread creations while mutexes are held

[dabund24]

second part of #1805. The first half was implemented in #1865.
closes #1805.

Summary

Simplest case: After creating $t_1$ in $t_0$ with mutex $l$ held, succeeding statements until maybe unlocking in $t_0$ must happen before everything after definitely locking $l$ in $t_1$.

generalizations:

• $t_1$ can be any descendant of $t_0$ as long as $t_0$ is a must-ancestor.
• It doesn't matter if locking happens in $t_1$ or a must-ancestor as long as that thread is also a must-ancestor of the thread created in $t_0$
• Succeeding statements of the thread creation in $t_0$ could also include statements in descendant threads as long as those are joined back into $t_0$ before an unlock could happen. This is what was computed in Improve MHP precision using ancestor locksets #1865.

Examples

In the following examples, A must happen before B.

Simple example

graph TB;
subgraph t1;
    E["lock(l);"]-->F;
    F["unlock(l);"]-->G;
    G((B))
end;
subgraph t0;
    A["lock(l);"]-->B;
    B["create(t1);"]-->C;
    C((A))-->D;
    D["unlock(l);"];
end;
B-.->E

Loading

B in a descendant of $t_1$

graph TB;
subgraph t2;
    H((B))
end;
subgraph t1;
    E["lock(l);"]-->F;
    F["create(t2);"]
end;
subgraph t0;
    A["lock(l);"]-->B;
    B["create(t1);"]-->C;
    C((A))-->D;
    D["unlock(l);"];
end;
B-.->E
F-.->H

Loading

A in a descendant of $t_0$

Here, it is important that no unlock happens in $t_0$ before $t_2$ is joined into $t_0$.

graph TB;
subgraph t1;
    E["lock(l);"]-->I;
    I["unlock(l);"]-->F;
    F((B));
end;
subgraph t2;
    H((A))
end;
subgraph t0;
    A["lock(l);"]-->B;
    B["create(t1);"]-->C;
    C["create(t2);"]-->D;
    D["join(t2);"]-->G;
    G["unlock(l);"]
end;
B-.->E
C-.->H
H-.->D

Loading

Analyses

Descendant Locksets $\mathcal{DL}$

$\mathcal{DL}\subseteq T\to 2^L$
$T\to 2^L$ is MapBot
$2^L$ is Must-Set
$\set{t_1\mapsto L}\in\mathcal{DL}$ means "the next operation must happen before operations in $t_0$ if a member of $L$ must have been locked before those after the child thread creation"

Transfer functions

• $[[\mathsf{create}(t_1)]]^\sharp_{\mathcal{DL}}\ S=S\sqcup\bigsqcup_{t_d\in\set{t_1}\cup\mathcal{DES}(t_1)}\set{t_d\mapsto \mathcal L}$
• $[[\mathsf{unlock}(l)]]^\sharp_\mathcal{DL}\ S=\set{t\mapsto S\ t\setminus \set l\mid t\in \left(\mathcal C\cup\bigcup_{t_c\in\mathcal C}\mathcal{DES}\ t_c\right)\setminus \mathcal J}$
• $[[\mathsf{unlock}(?)]]^\sharp_\mathcal{DL}\ S=\set{t\mapsto \emptyset\mid t\in \left(\mathcal C\cup\bigcup_{t_c\in\mathcal C}\mathcal{DES}\ t_c\right)\setminus \mathcal J}$

Mustlock History $\mathcal{LH}$

$\mathcal{LH}\subseteq L\to 2^T$
$T\to 2^T$ is MapTop
$2^T$ is Must-Set
$\set{l\mapsto T}\in\mathcal{DL}$ means "before the next operation, mutex $l$ must have been locked in all members of $T$"

Transfer functions

$[[\mathsf{lock}(l)]]^\sharp_{\mathcal{LH}}\ S=S\sqcup\set{l\mapsto S\ l \cup\set\mathcal T}$
$\mathsf{new}^\sharp_\mathcal{LH}\ S=S$

Global Descendant Locksets $\mathcal{DL}_g$

$T\to T\to 2^L$ is MapBot
$T\to 2^L$ is MapBot
$2^L$ is *Must-Set
$\mathcal{DL}_g\ t\subseteq T\to T\to L$
${t_0\mapsto{t_1\mapsto L}}\in \mathcal{DL}_g\ t$ means "throughout the entire existence of $t$, $t_0$ must have the descendant lockset ${t_1\mapsto L}$"

Contributions

• create(t1)
  $\forall t_d\in {t_1}\cup\mathcal{DES}\ t_1:$
  $M:=\set{t_l\mapsto L_\mathcal{CL}\cap L_\mathcal{DL}\mid t_l\mapsto L_\mathcal{DL}\in\mathcal{DL}, L_\mathcal{CL}\in\mathcal{CL}\ t_d\ t_l}$
  $\mathcal{DL}_g t_d\sqsupseteq \set{\mathcal T\mapsto M}$

Happens-Before rules

Statement s2 with $\mathcal{LH}_ 2, \mathcal T_2$ must happen after s1 with $\mathcal{DL}_ 1,\mathcal{DL}_ {g1}, \mathcal{LH}_ 1, \mathcal T_1$, if:
$\exists \mathcal T_2\mapsto L_a\in\mathcal{DL}_ 1, l_ {LH}\mapsto T_ {LH}\in \mathcal{LH}_ 1, t_ {LH}\in T_ {LH}:$
$l_{LH}\in L_a\land\mathcal T_1\in \mathcal A\ t_{LH}\land(t_{LH}\in\mathcal A\ \mathcal T_2\lor t_{LH}=\mathcal T_2)$

Additionally, we check if the condition above holds for any $t_1\mapsto DL_1\in\mathcal{DL}_g\ \mathcal T_1$ replacing $t_1$ with $\mathcal T_1$ and $DL_1$ with $\mathcal{DL}_1$

[Copilot]

Pull request overview

This PR implements the second part of happens-before (HB) relationship analysis for thread creations while mutexes are held. It introduces two new analyses (MustlockHistory and DescendantLockset) that work together to detect race conditions by establishing happens-before relationships between thread operations based on mutex locking patterns.

Changes:

• Added MustlockHistory analysis to track which threads have locked specific mutexes
• Added DescendantLockset analysis to compute descendant locksets and determine happens-before relationships
• Extended CreationLockset analysis with query support for integration with the new analyses
• Added 20 comprehensive test cases covering both race-free and racing scenarios

Reviewed changes

Copilot reviewed 21 out of 21 changed files in this pull request and generated 9 comments.

Show a summary per file

File	Description
src/analyses/mustlockHistory.ml	New analysis tracking mutex lock history per thread
src/analyses/descendantLockset.ml	New analysis computing descendant locksets and HB relationships
src/analyses/creationLockset.ml	Added CreationLockset query support
src/domains/queries.ml	Added CreationLockset and MustlockHistory query types with supporting domains
src/goblint_lib.ml	Exported the two new analysis modules
tests/regression/53-races-mhp/40-45-*.c	Race-free test cases validating correct HB detection
tests/regression/53-races-mhp/50-59-*.c	Racing test cases validating race detection

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[michael-schwarz]

Random thought: What do your analyses do for recursive mutexes? Are they sound in these cases?

[dabund24]

Thanks for bringing this up, those would never have crossed my mind. I think the analyses remain sound, but get less precise.

The only relevant thing changing here coming to my mind is the fact that after an unlock, we can't assume anymore that the mutex is now unlocked. As unlock statements have been places in our analyses, where we assume things to just break, but not start/keep working, this wouldn't be an issue.

[michael-schwarz]

I think the analyses remain sound, but get less precise.

👍 Could you add tests here and maybe also include some tests for your first analysis (potentially in a separate PR)?