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

Specification fix: ensure that the initial thread can be referenced #30

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

tautschnig
Copy link
Contributor

@tautschnig tautschnig commented Dec 1, 2020

With the previous specification, the initially active thread (as created
by starting a program) could not be referenced in transitions without
violating the specification (only threads specified in createThread
could be referenced).

Marked as Draft as #29 should be merged first and we shouldn't change the spec while SV-COMP'21 is about to kick off, so let's not merge until after SV-COMP'21 has been fully executed.

With the previous specification, the initially active thread (as created
by starting a program) could not be referenced in transitions without
violating the specification (only threads specified in createThread
could be referenced).

Includes a revert of 1a83971, as the
check can now proceed as the ambiguity is resolved.
| threadId | Represents the currently active thread for the transition. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes |
| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes |
| threadId | Represents the currently active thread for the transition. The initially active thread has id ``0``. If no ``threadId`` is given, any thread can be active. The value should be a unique identififer for a thread. | Yes | Yes |
| createThread | The currently active thread (value of ``threadId``) creates a new thread (value of ``createThread``) . In general, using a ``threadId`` is only allowed after creating a matching thread, except for thread ``0``, which exits by virtue of starting the program. The new thread's function can be entered on a second transition following this transition, such that the transition with the ``enterFunction`` key has the ``threadId`` of the created thread. When the function of the thread is exited, the thread is assumed to be terminated and its ``threadId`` should no longer be used. | Yes | Yes |
Copy link
Member

Choose a reason for hiding this comment

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

I don't understand "which exits by virtue of starting the program".
Did you mean "exists"?

@dbeyer
Copy link
Member

dbeyer commented Sep 25, 2021

SV-COMP 2021 is over and I think we should merge this now? @tautschnig @mdangl @MartinSpiessl
Could you please review one more time?
(And also rebase, please.)

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.

3 participants