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

WIP: Proper handling of thread information in witness linter #51

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from

Conversation

SvenUmbricht
Copy link
Contributor

Last year there were several threading-related issues with the linter which raised questions about the witness specification (cf. #30, #33, #36).
This PR is to fix the handling of threading-related information in the linter.

@PhilippWendler PhilippWendler marked this pull request as draft October 21, 2021 10:11
@SvenUmbricht
Copy link
Contributor Author

Even after the changes made in this PR check_function_stack still had some implicit assumptions about the witness that
are not enforced by the specification and while trying to fix these I noticed some other issues / underspecifications that have to be resolved before this can be merged:

  • What if no thread id is specified on a given edge? A previous version of the specification stated

    If no threadId is given, any thread can be active

    but this line has been removed in 2323492. The current state of this PR is to treat edges
    without a thread id as if the id of the main thread was specified.

  • How to interpret edges having data elements with both enterFunction and returnFromFunction keys?
    When checking callstack validity the linter assumes function returns to happen first, because otherwise a transition with
    different values for enterFunction and returnFromFunction would always be invalid.

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.

1 participant