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

[kfriedberger]

This PR is based on #33 and improves the documentation about the usage of thread identifiers.
It also disables the current check for thread creation.

[MartinSpiessl]

This also adds additional checks on the spare thread IDs.
While this might be a reasonable thing to do in the future, for SV-COMP I think it is best to not introduce additional constraints after the tool submission deadline. Otherwise this might invalidate witnesses of tools that had no chance of reacting to this new constraint, and we would need to update the linter yet again in case people complain about that.

This PR also adds changes to the spec, which need to be coordinated with #30.
Easiest would be to just disable the check for now and later consolidate spec changes with #30.
Also feedback from @hernanponcedeleon and @tautschnig on these spec changes would be valuable, as they already discussed similar changes and their effects in https://gitlab.com/sosy-lab/sv-comp/archives-2021/-/issues/30

For now, I would recommend creating a PR that just disables the check for witness.CREATETHREAD with a comment similar to #29 and #31. Then we can merge the rest after a consensus is reached and after the SV-COMP results are final. (If we merge the new check after this PR, it is not guaranteed that there will not be another change requested for the linter before the results are final, and then we would need to revert the additional check again.)

[kfriedberger]

I created another PR #35 and will rebase this one when/if the other PR is merged. The branch was rebased.

[hernanponcedeleon]

I think the paragraph about createThread is clear and matches the intuition that we all have after the discussion.

I'm not sure I understand the following

The value should be a unique identifer for a thread as long as this thread is active. A thread identifier can be used several times to identify different threads in the program, as long as their execution traces do not interfere. The program trace of a thread can branch or merge along its execution, just the corresponding control flow.

Do we want to say that identifiers uniquely and completely identify active threads? Can we just say the following?

there is a one-to-on mapping between identifiers and active threads

[kfriedberger]

Do we want to say that identifiers uniquely and completely identify active threads? Can we just say the following?

there is a one-to-on mapping between identifiers and active threads

Yes, that would also match my intention.

[mdangl]

In #37, I update the specification for conformity with the upcoming journal paper.
I tried to incorporate the improvements suggested here, so that we can publish them with the paper.
Specifically, you can see my version of the wording in commit 52cd6d.
@kfriedberger: could you please review that part?
I used the notion of an automaton run (cf. the literature on automata for the definition) to more precisely describe what I think you meant when you wrote that the execution traces should not interfere.

[dbeyer]

@kfriedberger Could you please review the part that @mdangl asked about?