Improve MHP precision using ancestor locksets

[dabund24]

First part of #1805.
Second case is handled in #1913.

To be handled

Non-transitive version

When creating $t_1$, $t_0$ must hold a lock $l$. If $l$ is not released before $t_1$ is definitely joined into $t_0$, $t_1$ is protected by $l$.

Examples

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

Loading

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

Loading

General version

Let $t_1$ be a must-ancestor of $t_0$. When creating $t_1$, $t_0$ must hold a lock $l$. If $l$ is not released before $t_d$ is definitely joined into $t_0$, $t_d$ is protected by $l$.

Example

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

Loading

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$

Conditions to satisfy

1. $t_0\in\mathcal A\ t_1\land (t_1=t_d\lor t_1\in\mathcal A\ t_d)$
2. maybe $\exists$ create(t1) in $t_0$ with $l\in\mathcal L$
3. $\forall$ create(t1) in $t_0:l\in\mathcal L$
4. $\forall$ unlock(l) in $t_0:t_d\notin\left(\mathcal C\cup\bigcup_{c\in\mathcal C}\mathcal{DES}\ c\right)\setminus\mathcal J$

Analysis

• $\mathcal{CL}\subseteq T\to T\to 2^L$
• $T\to 2^L$ is MapBot
• $2^L$ is Must-Set
• Flow-Insensitive
• $(t_1\mapsto\{t_0\mapsto L\})\in\mathcal{CL}$ means " $t_1$ is protected by all mutexes in $L$ locked in $t_0$ and by nothing else".

Contributions

• create(t1):
  $\forall t\in t_1\cup\mathcal{DES}\ t_1:$
  $$\mathcal{CL}\ t\sqsupseteq\{\mathcal T\mapsto\mathcal L\}$$

• unlock(l):
  $\forall t\in \left(\mathcal C\cup\bigcup_{c\in\mathcal C}\mathcal{DES}\ c \right)\setminus\mathcal J:$
  $\mathcal{CL}\ t\sqsupseteq \{\mathcal T\mapsto(\mathcal{CL}\ t\ \mathcal T)\setminus \{l\}\}$

• unlock of unknown mutex:
  $\forall t\in \left(\mathcal C\cup\bigcup_{c\in\mathcal C}\mathcal{DES}\ c \right)\setminus\mathcal J:$
  $$\mathcal{CL}\ t\sqsupseteq \{\mathcal T\mapsto\emptyset\}$$

Rules for MHP exclusion

Program points $s_1$ with $\mathcal T_1$, $\mathcal L_1$ and $\mathcal{CL}_1$ and $s_2$ with $\mathcal T_2$, $\mathcal L_2$ and $\mathcal{CL}_2$ cannot happen in parallel if at least one condition holds:

• $\exists (t_a\mapsto L_a)\in\mathcal{CL}_1:L_a\cap\mathcal L_2\neq\emptyset,t_a\neq \mathcal T_2$
• $\exists (t_a\mapsto L_a)\in\mathcal{CL}_2:L_a\cap\mathcal L_1\neq\emptyset,t_a\neq \mathcal T_1$
• $\exists(t_{a1}\mapsto L_{a1})\in\mathcal{CL}_ 1,(t_{a2}\mapsto L_{a2})\in\mathcal {CL}_ 2: L_{a1}\cap L_{a2}\neq\emptyset\land t_{a1}\neq t_{a2}$

[dabund24]

Some general questions:

• Is there a way to enforce configuration settings to be set to certain values in order for the analysis to work (i.e. similar to how analyses can be declared as dependencies)? This would be necessary for the settings revolving around thread ids as described in the pr summary. Checking settings using GobConfig.get_string at the start of transfer functions doesn't really seem ideal to me
• is there an ideal amount of tests I should write or can I write as many as I feel to be necessary?

[dabund24]

What does it mean for a thread id to be top or bottom? Not sure how to deal with this here and in some other places

[michael-schwarz]

It should usually not happen. If it does, I think the best is to assume that all bets are off.

[dabund24]

Would you suggest emitting a warning or something similar here or can I keep everything the way it is? (except for removing the comments of course)

[sim642]

• Is there a way to enforce configuration settings to be set to certain values in order for the analysis to work (i.e. similar to how analyses can be declared as dependencies)? This would be necessary for the settings revolving around thread ids as described in the pr summary. Checking settings using GobConfig.get_string at the start of transfer functions doesn't really seem ideal to me

Maingoblint.check_arguments has a bunch of ad-hoc checks like this.

[sim642]

• is there an ideal amount of tests I should write or can I write as many as I feel to be necessary?

As many as necessary to cover all the functionality and ideally the corner cases of the domains/analyses.
We also have code coverage available, but it's not required, although it might be useful for finding untested stuff.

[dabund24]

• Is there a way to enforce configuration settings to be set to certain values in order for the analysis to work (i.e. similar to how analyses can be declared as dependencies)? This would be necessary for the settings revolving around thread ids as described in the pr summary. Checking settings using GobConfig.get_string at the start of transfer functions doesn't really seem ideal to me

Maingoblint.check_arguments has a bunch of ad-hoc checks like this.

that's what I needed, nice :D
added in 13443f9

[dabund24]

• is there an ideal amount of tests I should write or can I write as many as I feel to be necessary?

As many as necessary to cover all the functionality and ideally the corner cases of the domains/analyses. We also have code coverage available, but it's not required, although it might be useful for finding untested stuff.

I'm going to add some more in the coming days 👍

[dabund24]

The ci builds failed due to an incorrect semi colon. I fixed this in f1efd32, so everything should be working now

[dabund24]

90/10 exposes a bug, which is caused by the fact that locksets have a more granular path sensitivity than the implemented creation lockset analyses. This will be fixed soon.

[michael-schwarz]

I asked copilot for a review, 50% joking. See what makes sense to you, but don't buy all the stuff it claims.

[Copilot]

Pull request overview

This PR implements ancestor lockset analysis to improve May-Happen-in-Parallel (MHP) precision in the Goblint analyzer. The approach tracks locks held by ancestor threads when creating descendant threads, enabling better race detection by identifying threads that are protected by ancestor locks.

Key changes:

• Adds transitiveDescendants analysis to track transitive descendant threads
• Implements creationLockset and taintedCreationLockset analyses for ancestor lock tracking
• Refactors lock domain handling with a new helper function
• Includes comprehensive test suite with 17 test cases covering various scenarios

Reviewed changes

Copilot reviewed 23 out of 23 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/analyses/transitiveDescendants.ml	New flow-insensitive analysis mapping threads to may-sets of descendants
src/analyses/creationLockset.ml	Core implementation of ancestor lockset analysis with creation and tainted creation lockset specs
src/cdomains/lockDomain.ml	Adds of_addr helper function to convert addresses to must-locks
src/analyses/mutexGhosts.ml	Refactored to use new LockDomain.MustLock.of_addr helper
src/domains/queries.ml	Adds DescendantThreads and MayCreationLockset query types with supporting infrastructure
src/goblint_lib.ml	Registers new TransitiveDescendants and CreationLockset modules
src/maingoblint.ml	Adds configuration validation for creation lockset analysis requirements
tests/regression/90-races_ancestor_locksets/*.c	Comprehensive test suite with 17 test cases covering race-free and racing scenarios

---

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

[michael-schwarz]

@dabund24: I am inviting you to the organization so the CI runs automatically for your PRs.

[michael-schwarz]

I have not yet completely reviewed it (please re-request my review once you have fixed the bug you found).

I like the degree to which this re-uses things that are already there, and think it will make a nice addition to Goblint (even if we have to contribute the cases where it makes a difference to SV-COMP ourselves, but that's more a problem of how few benchmarks we have there).

While looking over it superficially, I started wondering about something:

You are explicitly constructing this set of descendants here. Is this actually needed?

• Can you get away with reconstructing it dynamically via the ancestor information encoded in the thread ids, e.g., in may_race?
• Or in the case of tainted locksets by storing something along the lines of (whatever is a descendant of t_1 except those that are given explicitly in J has potentially tainted lockset)?

May be that there is very good reasons that this is not possible (or not possible without massive precision loss), but one should maybe waste a few minutes thinking about it. The more modular the collected information is, the nicer the whole analysis becomes.

[dabund24]

Before discussing this, I'll start by first explaining the potential fix of the bug just in case this is part of the necessary considerations. The reason the bug happens is the fact that the lockset analysis does some path splitting, thus there exists a create(t2)-statement (the one after node 14) with mutex in the must-lockset.

So the implicit assumption of condition 1 $\implies$ condition 2 from the summary doesn't hold anymore for other creates from within the same thread. To fix this, the only working approach I can think of is just contributing to $\mathcal{TCL}$ everything from $\mathcal{CL}$, which would break due to a create-statement.

With that out of the way, I think that it is definitely possible to solve this without the descendants analysis and without any precision loss. As you have suggested, we can make both $\mathcal{CL}$ and $\mathcal{TCL}$ store only direct parents and additionally store a third component in G of $\mathcal{TCL}$ such that G is a subset of $2^{T\times L\times 2^T}$, where the third component is the must-set of every descendant explicitly excluded from the taint. If I didn't make any mistakes, the new $\mathcal{TCL}$ analysis would be implemented like this:

In the case of an unlock(l)-statement, we would contribute for all $t\in\mathcal C\setminus\mathcal J$:
$\mathcal{TCL}(t)\sqsupseteq\{(\mathcal T, l, \mathcal J)\}$.

Applying the bug fix from above facing a create(t1)-statement, we can contribute
$\mathcal{TCL}(t_1)\sqsupseteq \{(t,l,\emptyset)\mid (t,l)\in\mathcal{CL}(t_1), l\notin\mathcal L\}$

We would obtain $\mathcal{IL}(t)$ from the PR-summary like this (given $\mathcal A(t)$ is the set of the ancestors of $t$):
$\mathcal{CL}_ \mathrm{transitive}(t):=\mathcal{CL}(t)\cup\bigcup_{a\in\mathcal A(t)}\mathcal{CL}(a)$
$\mathcal{TCL}_ \mathrm{transitive}(t):=\{(t_\mathrm{parent},l)\mid(t_\mathrm{parent},l,S)\in\mathcal{TCL}(t)\}\cup\bigcup_{a\in\mathcal A(t)}\{(t_\mathrm{creating},l)\mid(t_\mathrm{creating},l, S)\in\mathcal{TCL}(a),t\notin S\}$
$\mathcal{IL}(t):=\mathcal{CL}_ \mathrm{transitive}(t)\setminus\mathcal{TCL}_ \mathrm{transitive}(t)$

Personally, I am not fully convinced (yet :D) that this is the superior way of implementing the analysis, as I have the following concerns:

• I find the approach harder to understand/to reason about. The "double negation" (excluding something from the exclusion set) involved in $\mathcal{TCL}$ feels more complex to me than anything from the initial solution
• The implementation requires more code; most notably for the implementation of a custom domain for $\mathcal{TCL}$ and the more complex access/may_race functions.
• I see the descendants analysis as an opportunity for future analysis to be more concise, as is a rather basic building block, which may be useful in a variety of places

Obviously, my experience with goblint/abstract interpretation in general is very limited, so if you think that the benefits of the new approach outweigh its drawbacks, I will happily implement it 👍

[michael-schwarz]

Before discussing this, I'll start by first explaining the potential fix of the bug just in case this is part of the necessary considerations. The reason the bug happens is the fact that the lockset analysis does some path splitting, thus there exists a create(t2)-statement (the one after node 14) with mutex in the must-lockset.

Stupid question: Is that not a problem of how CL is constructed that is in principle independent of path-sensitivity and can, e.g., also arise as a result of context-sensitivity?

void evil(int x) {
      if(x) lock(a);
      create(t1)
      if(x) unlock(a);
}

void main() {
    // Branching to ensure created thread has a unique tid, even if there is potentially two places it is created : -)
    if (top) {
        evil(0);
    } else {
        evil(1);
    }
}

Assuming evil is analyzed context-sensitively with x in context (which it usually is), we have the same problem here? Or not?

Would $T \to T \to 2^L$ with $2^L$ a must set not be the better choice?
(Alternatively, you may want to write it as $T \to 2^{(T \times 2^L)}$ with the invariant that there is only one tuple (t,L) for each t)

Then, $l \in CL \quad t_d \quad t_0$ means that $t_0$ is a must parent of $t_d$ and it always holds $l$ when creating $t_0$.

Afterthought: how do you deal with ambiguous creators? I guess giving up when the thread id is no longer unique?

---

The push for a more modular solution was that I implemented something that looks somewhat similar on the surface (#1065) which turned out to cause a slow-down by a factor of 4 (#1120), which we have still not fixed.

But maybe we can go with the descendant global invariant for now and then check later if it causes any slowdown we're unwilling to pay on real programs? We can still go for the more involved local solution later if this is the case?
(Probably something for @dabund24 and @DrMichaelPetter to decide).

[dabund24]

Before discussing this, I'll start by first explaining the potential fix of the bug just in case this is part of the necessary considerations. The reason the bug happens is the fact that the lockset analysis does some path splitting, thus there exists a create(t2)-statement (the one after node 14) with mutex in the must-lockset.

Stupid question: Is that not a problem of how CL is constructed that is in principle independent of path-sensitivity and can, e.g., also arise as a result of context-sensitivity?

void evil(int x) {
      if(x) lock(a);
      create(t1)
      if(x) unlock(a);
}

void main() {
    // Branching to ensure created thread has a unique tid, even if there is potentially two places it is created : -)
    if (top) {
        evil(0);
    } else {
        evil(1);
    }
}

Assuming evil is analyzed context-sensitively with x in context (which it usually is), we have the same problem here? Or not?

I haven't thought about that, but you are right, we do have the same problem here. In 1db14cb I added another test, which covers this. However, I think that the fix for the path-sensitivity problem should fix this, too, since in that case, we would again have another creation statement without the mutex locked and add it to the tainted set (or use your approach).

Afterthought: how do you deal with ambiguous creators? I guess giving up when the thread id is no longer unique?

I was assuming initially, that the three cases in the section "Notes on non-unique thread ids" from the PR-summary are the only relevant cases, where ambiguous creators could be a problem, but thinking about it, that is a really bold claim, which I just should not make without knowing a proof for it. Checking if the descendant threads have a unique thread id wouldn't even result in a loss of precision in most cases[1], since the threadJoin analysis also gives up on non-unique TIDs.

Would T → T → 2 L with 2 L a must set not be the better choice?
(Alternatively, you may want to write it as T → 2 ( T × 2 L ) with the invariant that there is only one tuple (t,L) for each t)

I'm amazed, that is so much nicer O_O

But maybe we can go with the descendant global invariant for now and then check later if it causes any slowdown we're unwilling to pay on real programs? We can still go for the more involved local solution later if this is the case?
(Probably something for @dabund24 and @DrMichaelPetter to decide).

I am going to implement the other case, too, since I am also somewhat intrigued now, how the two approaches will compare. Thanks a lot for your remarks!

---

[1] it would if we never unlock and never join, but I think that this wouldn't be too tragic

[dabund24]

Is there a way of accessing all (must-)ancestors of a thread? Getting all threads in general or all keys of a global analysis would also work, but I don't see any of that to be possible at first glance. If that's the cas, I can add a MustAncestors analysis, such that $\bigcup_{a\in\mathcal A}\ldots$ becomes possible to implement

[dabund24]

I have not yet completely reviewed it (please re-request my review once you have fixed the bug you found).

The simpler version is now done (at least that's what I believe) and in sync with the PR-summary. If you want to review it already, you can do so. Otherwise, feel free to ignore the review request until the alternative solution is also implemented.

[michael-schwarz]

If you want to review it already, you can do so.

I probably won't get around to it until some time next week, but I added it to my TODO (list / stack / multiset).

[michael-schwarz]

Is there a way of accessing all (must-)ancestors of a thread?

I think in general no. However, if you only need the must ancestors of definite thread ids (which I guess is true in your case?), you can reconstruct them as the new create edge is simply appended to the sequence of the parent.

Such a function must_ancestors: TID -> TID list option could then be added to the generic thread id interface, and just return None, i.e., "information not available" for the thread ids which don't allow this trick.

[sim642]

Looks fine by me as well, but @DrMichaelPetter should also have a look before we merge this.

[DrMichaelPetter]

LGTM

[dabund24]

Huge thanks to all of you for your reviews and helpful hints!