WitnessLinter does not consider different paths in a witness when checking thread information

[kfriedberger]

The WitnessLinter currently assumes that there is a "globally" unique thread identifier for each thread,
and such an identifier can only be created once in the witness (via createThread=NEW_ID).
This is based on the sentence "The value should be a unique identifer for a thread." in the corresponding specification.

However, it is much more convenient and also more intuitive, if the same thread identifier can be created on several transitions, for example, if (and only if?) those transitions appear along different paths in the witness.
We found several witnesses that were not accepted by the linter due to that problem.
For example, we refer to this CPAchecker issue.

In my opinion, allowing multiple creations of a thread with ID=2 on different branches without intersecting suffixes does not violate the previously given specification, because each thread is actually unique, and an identical thread coming from the same program location calling pthread_create does not violate the uniqueness.

[kfriedberger]

Just for clarification:
Even with intersection suffixes, a unique thread can have several creation points.

Overall, a witness can contain the information that some (unique!) thread is created at transition A or B or C and afterwards executes some other transitions. This case needs support in the linter.

[MartinSpiessl]

The spec can and should certainly be made more precise to clearly convey the desired constraints.

if (and only if?) those transitions appear along different paths in the witness.

The witness encodes a possibly infinite number of program paths. It is better to refer to traces of the witness automaton. We should try to keep such constraints purely syntactic, i.e., describe them on the witness automaton alone and not consider semantics of the program.

Your description is still informal and needs to be formalized further. As far as I understand you you want the following to hold:

For every trace of the witness automaton, each thread id is at most created once

This is decidable in worst case O(k*n) where k is the number of thread creation nodes and n is the number of transitions in the automaton.

In my opinion, allowing multiple creations of a thread with ID=2 on different branches without intersecting suffixes does not violate the previously given specification, because each thread is actually unique, and an identical thread coming from the same program location calling pthread_create does not violate the uniqueness.

When we need to resort to opinion, the format is underspecified. We can however ask the author of the format extension (which would be you iirc 😉 ) how they envisioned it, and then fix the underspecification.

I propose the following steps:

1. disable that check in witnesslint for SV-COMP 2021. Please file a PR similiar to Disable ThreadId check as the spec needs to be clarified first #29 and Use default when checking for invariants on cycle heads #31.
2. The README.md needs to be updated such that the spec becomes clearer.
3. The check should be rewritten and reenabled to conform to the updated spec. The check could also be dropped completely, but since the property is decidable dropping it seems unnecessary.