WitnessLinter ignores threads when checking callstack validity.

[kfriedberger]

The current witnesslinter only checks callstack validity for sequential programs and does not consider thread interleaving.
This could lead to marking valid witnesses as invalid. I have not tested the behaviour, this issue is only based on a quick code review.

The concurrent tasks of the current SV-COMP are simple enough and do (hopefully) not use more than one function call per thread. Thus, this problem is not urgent, but should be solved until next year.

As threadids are optional, the following sequence of transitions is valid:

- enter foo
- enter bar
- return from foo
- return from bar

With threadIds, the same sequence could be written as

- threadId=0, enter foo
- threadId=1, enter bar
- threadId=0, return from foo
- threadId=1, return from bar

[MartinSpiessl]

I think this is again underspecification of the concurrency witnesses. The current general witness spec quite clearly states:

The path is considered to stay in the specified function until another transition is annotated with this data node for another function or a transition annotated with returnFromFunction, telling the validator that the path continues in the previous function on the stack.

I think this could easily be fixed by declaring (and in the check tracking) the function callstack per thread.

[kfriedberger]

How strong is "consider to stay" in terms of "must" and "should"?
I fully agree that requiring the threadId at all function entering and return transitions is a good idea.

[MartinSpiessl]

Very good point!

From the wording I would interprete it as "must", i.e., there is no way the witness can match anything outside of that function unless we either enter another function or we encounter the matching returnFromFunction.

This interpretation would however be in conflict with how it is implemented in CPAchecker currently, cf. #20 (comment)

For Ultimate (read the next comment) it would probably be fine, they always put that returnFromFunction edge, but also do not actively use it in their validator.