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$

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$

Note

This case is not covered by the analysis implemented in this Pull Request, but may be added some time later

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

Here, it is important that no unlock happens in $t_0$ before $t_2$ is joined into $t_0$, which was computed in #1865.

Dependency Analyses

• $\mathcal T$: Ego Thread Id at program point
• $\mathcal L$: Must-Lockset at program point
• $\mathcal C$: May-Creates of ego thread before program point
• $\mathcal J$: Transitive Must-Joins of ego thread before program point
• $\mathcal{DES}\ t$: Descendant threads of $t$ (implemented in this PR)
• $\mathcal A\ t$: Must-ancestors of $t$

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\oplus\set{t_d\mapsto \mathcal L\mid t_d\in\set{t_1}\cup\mathcal{DES}(t_1)}$
• $[[\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\oplus\set{l\mapsto S\ l \cup\set\mathcal T}$
$\mathsf{new}^\sharp_\mathcal{LH}\ S=S$

Happens-Before rules

Statement s2 with $\mathcal{LH}_ 2, \mathcal T_2$ must happen after s1 with $\mathcal{DL}_ 1, \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)$

[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)?

[dabund24]

@DrMichaelPetter and I decided to remove the flow-insensitive analysis detecting cases like the third example, since we did not see a simple way of both having only monotonic contributions and being certain that the analysis is sound

[michael-schwarz]

Just so I can understand: why is monotonicity important here? @dabund24 @DrMichaelPetter

(By default (without update rule) globals are accumulated, so their values grow monotonically anyway)

[dabund24]

What we did was pretty much copying a MapBot from the local analysis to the global analysis, where the (inner) domain is MapTop:

This felt problematic to me, since for example, if the local analysis also ever read from the global analysis (which it doesn't, but may at any time later on), the fixed-point iteration may never terminate. Maybe I am missing something here, though 🤔

[michael-schwarz]

I'm not deeply familiar with what exactly you're trying to do, but in general our fixpoint solvers can deal with non-monotonic right-hand sides without any issues.

====

Nothing wrong with copying values from a MapBot to a MapTop, though it usually doesn't do much for globals. If the binding is not present, it is assumed to be top, so contributing more to it will not really have much of an effect...

[dabund24]

Thanks for remarking this. In that case, I'm going to undo the changes

[michael-schwarz]

No, please discuss with @DrMichaelPetter what he suggests before doing so.