sv-witnesses
sv-witnesses copied to clipboard
sosy-lab
WitnessLinter does not consider different paths in a witness when checking thread information
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.
I created another PR #35 and will rebase this one when/if the other PR is merged. The branch was rebased.
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
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.
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.
