Improve MHP precision using ancestor locksets

[dabund24]

First part of #1805. Second case will be handled in a separate PR.

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

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

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

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-Ancestor threads of $t$ (implemented in this PR)

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$

Possible solutions

1. Explicitly listing all descendants

• $\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\}$$

Conversion into $\mathcal{IL}$

$\mathcal{IL}\ t:= \mathcal{CL}\ t$

2. Only listing children explicitly

Alternative Creation Lockset

• $\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$ and all threads having $t_1$ as a must-ancestor can be protected by all mutexes in $L$ locked in $t_0$ and by nothing else".

Contributions

• create(t1): $$\mathcal{CL}\ t_1\sqsupseteq\{\mathcal T\mapsto\mathcal L\}$$

Alternative Tainted Creation Lockset

• $\mathcal{CL}\subseteq T\to T\to L\to 2^T$
• $T\to 2^L$ is MapBot
• $2^L$ is Must-Set
• Flow-Insensitive
• $(t_1\mapsto\{t_0\mapsto \{l\mapsto T_e\}\})\in\mathcal{TCL}$ means "(($t_1$ and all threads having $t_0$ as a must-descendant) except for exactly those in $T_e$) are definitely not protected by $l$ locked in $t_1$".

Contributions

• unlock(l): $\forall c\in\mathcal C$ $\mathcal{TCL}\ c\sqsupseteq \{\mathcal T\mapsto\{l\mapsto \mathcal J\}\}$
• unlock of unknown mutex: $\forall c\in\mathcal C$ $M:=\bigsqcup_{l\in \mathcal{CL}\ c\ \mathcal T}\{l\mapsto\mathcal J\}$ $\mathcal{TCL}\ c\sqsupseteq \{\mathcal T\mapsto M\}$

Conversion into $\mathcal{IL}$

$\mathcal{CL}_ \mathrm{transitive}\ t_d:=\mathcal{CL}\ t_d\sqcup\bigsqcup_{t_1\in\mathcal A\ t_d}\mathcal{CL}\ t_1$ $\mathcal{TCL}_ \mathrm{transitive}\ t_d:=\mathcal{TCL}\ t_d\sqcup\bigsqcup_{t_1\in\mathcal{A}\ t_d}\mathcal{TCL}\ t_1$ $\mathcal{IL}\ t_d:=\bigsqcup_ {t_0\mapsto L_ \mathcal{CL}\in\mathcal{CL}_ \mathrm{transitive}\ t_d}\{t_0\mapsto L_\mathcal{CL}\setminus\{l\mid l\mapsto J\in\mathcal{TCL}_\mathrm{transitive}\ t_d\ t_0,t_d\notin J\}\}$

Rules for MHP exclusion

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

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

[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 https://github.com/goblint/analyzer/pull/1865/commits/13443f99e6f64da28def8331a5a0e4779d52bc00

[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 https://github.com/goblint/analyzer/pull/1865/commits/f1efd326c95b6157a8b15edbfec0b062ba55797f, 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.

[michael-schwarz]

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

[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 :+1:

[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 (https://github.com/goblint/analyzer/pull/1065) which turned out to cause a slow-down by a factor of 4 (https://github.com/goblint/analyzer/issues/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 https://github.com/goblint/analyzer/pull/1865/commits/1db14cb7b21e2d3817ff57de032b75354e53e004 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.

[dabund24]

Both variants are now fully implemented and described in the pr summary. I'm really impressed with how well maps work as domains here. That saved a lot of work compared to using regular sets.

The naming of the analyses is not finalized yet. I'm excited to see what the benchmarks say, such that this can be fixed :D

[michael-schwarz]

Both variants are now fully implemented and described in the pr summary.

What is your opinion on which one is nicer? And did you run on larger programs to get a feeling for the performance penalty of either?

[dabund24]

What is your opinion on which one is nicer?

Subjectively, I still find the initial approach nicer. Now that the analysis doesn't require a corresponding tainted analysis anymore, it feels like a natural solution to the problem, since we are essentially constructing a graph with edge labels and nothing else. However, I know that that doesn't have to mean a lot in the scope of the project, so if the other approach ends up being objectively superior, we should go with that one.

And did you run on larger programs to get a feeling for the performance penalty of either?

I took all c files of a directory containing driver files with data races from sv-comp (sv-benchmarks/c/ldv-linux-3.14-races) as a sample and compared both versions with each other and another configuration with all dependencies, but none of the new analyses.

Config files

nothing.json

{
  "ana": {
    "sv-comp": {
      "enabled": true,
      "functions": true
    },
    "activated": [
      "base",
      "threadid",
      "mallocWrapper",
      "mutexEvents",
      "mutex",
      "access",
      "race",
      "escape",
      "threadJoins"
    ]
  }
}

creation-lockset.json

{
  "ana": {
    "sv-comp": {
      "enabled": true,
      "functions": true
    },
    "activated": [
      "base",
      "threadid",
      "mallocWrapper",
      "mutexEvents",
      "mutex",
      "access",
      "race",
      "escape",
      "threadJoins",
      "creationLockset",
      "threadDescendants"
    ]
  }
}

creation-lockset-alternative.json

{
  "ana": {
    "sv-comp": {
      "enabled": true,
      "functions": true
    },
    "activated": [
      "base",
      "threadid",
      "mallocWrapper",
      "mutexEvents",
      "mutex",
      "access",
      "race",
      "escape",
      "threadJoins",
      "creationLockset",
      "threadDescendants"
    ]
  }
}

Here are the results in case you want to have a glimpse at them:

linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.c

nothing

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.c --conf "conf/examples/nothing.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:04.145
[Info] vars: 9033, evals: 9145

[Info] |called|=0

Memory statistics: total=15725.72MB, max=57.06MB, minor=15721.28MB, major=129.29MB, promoted=124.84MB
    minor collections=7503  major collections=14 compactions=0

creation-lockset

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.c --conf "conf/examples/creation-lockset.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:05.618
[Info] vars: 9045, evals: 13244

[Info] |called|=0

Memory statistics: total=21021.92MB, max=65.62MB, minor=21016.15MB, major=173.47MB, promoted=167.69MB
    minor collections=10029  major collections=16 compactions=0

creation-lockset-alternative

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.c --conf "conf/examples/creation-lockset-alternative.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:05.920
[Info] vars: 9045, evals: 13670

[Info] |called|=0

Memory statistics: total=21589.98MB, max=65.62MB, minor=21584.06MB, major=188.17MB, promoted=182.25MB
    minor collections=10300  major collections=17 compactions=0

linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.c

nothing

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.c --conf "conf/examples/nothing.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:02.703
[Info] vars: 18554, evals: 16892

[Info] |called|=0

Memory statistics: total=7736.36MB, max=65.62MB, minor=7730.50MB, major=103.52MB, promoted=97.66MB
    minor collections=3691  major collections=11 compactions=0

creation-lockset

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.c --conf "conf/examples/creation-lockset.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:04.083
[Info] vars: 18576, evals: 26455

[Info] |called|=0

Memory statistics: total=12296.36MB, max=75.47MB, minor=12290.25MB, major=142.65MB, promoted=136.55MB
    minor collections=5867  major collections=14 compactions=0

creation-lockset-alternative

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.c --conf "conf/examples/creation-lockset-alternative.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:04.681
[Info] vars: 18576, evals: 27769

[Info] |called|=0

Memory statistics: total=13608.90MB, max=86.79MB, minor=13602.79MB, major=173.96MB, promoted=167.86MB
    minor collections=6493  major collections=15 compactions=0

linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.c

nothing

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.c --conf "conf/examples/nothing.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:01.656
[Info] vars: 7064, evals: 7320

[Info] |called|=0

Memory statistics: total=5640.98MB, max=37.52MB, minor=5637.40MB, major=57.57MB, promoted=53.99MB
    minor collections=2692  major collections=9 compactions=0

creation-lockset

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.c --conf "conf/examples/creation-lockset.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:02.346
[Info] vars: 7076, evals: 10758

[Info] |called|=0

Memory statistics: total=8202.27MB, max=43.15MB, minor=8198.01MB, major=75.44MB, promoted=71.17MB
    minor collections=3914  major collections=11 compactions=0

creation-lockset-alternative

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.c --conf "conf/examples/creation-lockset-alternative.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:02.482
[Info] vars: 7076, evals: 10758

[Info] |called|=0

Memory statistics: total=8481.22MB, max=43.15MB, minor=8476.96MB, major=83.92MB, promoted=79.65MB
    minor collections=4047  major collections=11 compactions=0

linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c

nothing

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c --conf "conf/examples/nothing.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:01.583
[Info] vars: 6909, evals: 6852

[Info] |called|=0

Memory statistics: total=5374.62MB, max=37.52MB, minor=5371.09MB, major=52.23MB, promoted=48.69MB
    minor collections=2565  major collections=11 compactions=0

creation-lockset

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c --conf "conf/examples/creation-lockset.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:02.692
[Info] vars: 6923, evals: 12967

[Info] |called|=0

Memory statistics: total=9188.66MB, max=43.15MB, minor=9183.97MB, major=76.70MB, promoted=72.01MB
    minor collections=4385  major collections=13 compactions=0

creation-lockset-alternative

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.c --conf "conf/examples/creation-lockset-alternative.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:02.894
[Info] vars: 6923, evals: 12967

[Info] |called|=0

Memory statistics: total=9621.00MB, max=49.62MB, minor=9616.30MB, major=90.76MB, promoted=86.06MB
    minor collections=4591  major collections=14 compactions=0

linux-3.14--drivers--usb--misc--adutux.ko.cil.c

nothing

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.c --conf "conf/examples/nothing.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:00.786
[Info] vars: 3174, evals: 3949

[Info] |called|=0

Memory statistics: total=2375.93MB, max=28.37MB, minor=2372.95MB, major=35.20MB, promoted=32.23MB
    minor collections=1135  major collections=8 compactions=0

creation-lockset

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.c --conf "conf/examples/creation-lockset.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:01.169
[Info] vars: 3182, evals: 6235

[Info] |called|=0

Memory statistics: total=3699.01MB, max=32.63MB, minor=3695.76MB, major=45.53MB, promoted=42.28MB
    minor collections=1766  major collections=9 compactions=0

creation-lockset-alternative

  ../../../analyzer/goblint ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.c --conf "conf/examples/creation-lockset-alternative.json" > /dev/null
[Info] SV-COMP specification: 

[Info] runtime: 00:00:01.248
[Info] vars: 3182, evals: 6235

[Info] |called|=0

Memory statistics: total=3837.11MB, max=32.63MB, minor=3833.86MB, major=49.32MB, promoted=46.08MB
    minor collections=1832  major collections=9 compactions=0

Interestingly, the initial solution used less memory and took less time to terminate in all cases. It could go the other way if we are analyzing problems with more mutexes and more threads and will probably improve once I have implemented your suggestions, but at least we are not seeing a significant slowdown already.

[dabund24]

we will stick with the initial version for now, since it is not dramatically slow and the alternative version is not faster in its latest implementation. The charts below compare the cputimes of the config for svcomp 2025 and identical configs with either the regular or alternative version of the analysis added.

x-axis: svcomp25; y-axis: svcomp25 + creation lockset x-axis: svcomp25 + alternative creation lockset; y-axis: svcomp25 + creation lockset

[sim642]

This PR has 115 commits which looks like a lot of intermediate changes that got reverted/removed by the end?

In that case it would make sense to squash merge this eventually to not introduce too much clutter to git history. However, it might also be too crude to squash all of this into a single commit, I'm not sure because I haven't looked at the intermediates. Alternatively, the git history could be cleaned up with an interactive rebase to avoid introducing things which get dropped by the end, although I don't know if it's worth the effort or not.

[sim642]

By the way, are there any programs in sv-benchmarks or our bench where such situation occurs at all?

[dabund24]

This PR has 115 commits which looks like a lot of intermediate changes that got reverted/removed by the end?

In that case it would make sense to squash merge this eventually to not introduce too much clutter to git history. However, it might also be too crude to squash all of this into a single commit, I'm not sure because I haven't looked at the intermediates. Alternatively, the git history could be cleaned up with an interactive rebase to avoid introducing things which get dropped by the end, although I don't know if it's worth the effort or not.

I can go for the interactive rebase. Would it be enough if I remove all commits concerning the alternative version, which is completely removed now or should I also take care of commits fixing some minor mistakes I made in previous commits like https://github.com/goblint/analyzer/pull/1865/commits/97a69679af6ee6742c1be960bdd147a601bfb5fa ?

[dabund24]

By the way, are there any programs in sv-benchmarks or our bench where such situation occurs at all?

Unfortunately, there are none. This analysis could be used for enhancing the precision of the deadlock analysis (if a thread locks a mutex it is also protected with, a deadlock must happen) and we may be lucky here, but we haven't investigated this further, yet.

[sim642]

I can go for the interactive rebase. Would it be enough if I remove all commits concerning the alternative version, which is completely removed now or should I also take care of commits fixing some minor mistakes I made in previous commits like 97a6967 ?

That I would move to be a fixup after the commit which introduced it, such that this change is completely cancelled from the history. Other minor reformatting or comment changes could be fixup-ed similarly. Other more semantic bug fixes could remain as separate commits though, as indication for future git blamers to document that this has intentionally been changed from something incorrect.

But it depends on how deep you want/can be bothered to go with the history cleanup. With 121 commits, it could also quickly get very tricky because dropping an early commit ends up making a lot of the remaining patches not apply cleanly. You could also do it in multiple passes: first drop all the alternative stuff and then interactive rebase again to clean the rest.

[dabund24]

There are a bunch of merge conflicts arising in commits unrelated to this PR already when keeping all commits (i.e. git rebase -i 2c9c39d and leaving everything in the editor window unchanged). Should I try to come up with sensible merge resolutions myself here or would it make more sense for us to deal with this in some different way?

[sim642]

Since this history contains some merges from master, the rebase also starts rebasing some merged things to linearize the history. Using --rebase-merges should help, one just needs to not touch those commits that are on master to not try to rewrite them.

It might also make sense to rebase --onto master to get rid of the old merges entirely, but I don't know if this would make things easier or harder in this case.

[dabund24]

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