Skip to content
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.

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

Open
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

kfriedberger
Copy link
Member

@kfriedberger kfriedberger commented Dec 8, 2020

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.

Copy link
Collaborator

@MartinSpiessl MartinSpiessl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Member Author

kfriedberger commented Dec 8, 2020

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

Ending lines with whitespaces is special in Markdown and causes a "newline" after rendering.
However, none of those trailing whitespaces is required for this file.
@hernanponcedeleon
Copy link

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
Copy link
Member Author

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
Copy link
Member

mdangl commented Dec 21, 2020

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
Copy link
Member

dbeyer commented Sep 25, 2021

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Development

Successfully merging this pull request may close these issues.

5 participants