WitnessLinter does not consider different paths in a witness when checking thread information
Created by: 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.