Update descriptions of graph elements, node elements, and edge elements from upcoming TOSEM paper #37

mdangl · 2020-12-08T20:44:28Z

No description provided.

…g journal paper to the README

… the upcoming journal paper to the README

README.md

MartinSpiessl · 2020-12-08T21:06:21Z

README.md

@@ -76,8 +76,8 @@ The following information should additionally be available in the witness:

 | key | Meaning | Allowed in Violation Witnesses | Allowed in Correctness Witnesses |
 | --- | --- | ---- | ---- |
-| 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 identifer 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 | ``createThread`` is used in the analysis of concurrent programs as part of the source-code guard of a transition and restricts the set of CFA edges matched by the source-code guard to operations where a new thread is created. The value of ``data`` elements with this key is an identifier for the new thread. Any string may be used as an identifier, provided that it is unique in the document in the sense that for any run through the automaton, there may not be two different threads that (1) are both active (i.e., created but not yet destroyed) and (2) share the same identifier. The ``attr.type`` attribute of this key is ``string``. | Yes | Yes |


this needs review by @kfriedberger and @hernanponcedeleon. There are currently pull requests for changing/fixing the underspecification for concurrency witnesses, cf. #30 #34. Please coordinate and tell me which version should be taken.
If this gets controversial I would recommend to take this section out and merge it separately, such that we can more easily merge the rest of this PR which is without conflict.

I don't think Specification fix: ensure that the initial thread can be referenced #30 is related --- regarding the content, I mean; of course both change sets need to be merged manually. By the way, I don't really see the point of Specification fix: ensure that the initial thread can be referenced #30 anyway, because we already allow an initial transition with enterFunction(main); the createThread for the main thread belongs on that transition, too, in my opinion. But that's off-topic here.

I think the improvements proposed in WitnessLinter does not consider different paths in a witness when checking thread information #34 are very valuable. Regarding the wording, I will discuss some modification with @kfriedberger at the soonest opportunity.

Was there any further discussion yet?
From my point the new description looks valid and sufficient.

MartinSpiessl · 2020-12-08T21:15:52Z

README.md

+| endline | *Valid values:* Valid line number of the program <br /> ``endline`` is the same as the ``startline`` key, except that it refers to the line number on which an operation of a CFA edge ends. | Yes | Yes |
+| startoffset | *Valid values:* Offset of a specific character in the program from the program start. <br /> ``startoffset`` is used as part of the source-code guard of a transition and restricts the set of CFA edges matched by the source-code guard to operations between specific character offsets in the source code, where the term character offset refers to the total number of characters from the beginning of a source-code file up to the beginning of some intended statement or expression. Any character offset between the beginning and end of a source-code file is a valid value for ``data`` elements with this key. While on the one hand, usage of ``data`` elements with this key allows the witness to convey very precise location information, on the other hand, this information is susceptible to even minor changes in the source code. If this is not desired, usage of ``data`` elements with this key should be omitted by the producer, or, if that is not an option, it can be removed during a post-processing step, provided that enough other source-code guards are present to make matching the witness against the source code feasible. A third option would be to recompute the offset values for the changed source code using a diff tool. The ``attr.type`` attribute of this key is ``int``. | Yes | Yes |
+| endoffset | *Valid values:* Offset of a specific character in the program from the program start. <br /> ``endoffset`` is the same as the ``startoffset`` key, except that it refers to the character offset at the end of an operation. | Yes | Yes |
+| enterLoopHead | *Valid values:* ``false`` (default) or ``true`` <br /> ``enterLoopHead`` is used as part of the source-code guard of a transition and restricts the set of CFA edges matched by the source-code guard to operations on CFA edges where the successor is a loop head. For our format specification, any CFA node that (1) is part of a loop in the CFA, (2) has an entering CFA edge where the predecessor node is not in the loop, and (3) has a leaving CFA edge where the successor node is not in the loop, qualifies as a loop head. Note, however, that depending on the programming language of the verification task, the loop head may be ambiguous. For example, in C it is possible to use ``goto`` statements to construct arbitrarily complex loops with many CFA nodes that match the definition above. The ``attr.type`` attribute of this key is ``boolean`` and its default value is ``false``. | Yes | Yes |


This definition would mean that there could be a loop without a loop head, since it can happen that there is no single node that both has entering edges from outside the loop and leaving edges to outside of the loop. This could e.g. be divided over several nodes in the CFA.

This definition is also sensitive to the exact form of the CFA, and is therefore fragile and can break between implementations.

Yes, there can be loops where no loop head can be defined. In these cases, the key cannot be used. I will update the text so reflect this.

Yes, if producer and consumer cannot agree on a control-flow model of the system, witness validation is going to be difficult. In practice, almost all loops have an obvious loop head, so this might be a non-issue (at least it was a non-issue in the past).

README.md

MartinSpiessl · 2020-12-08T21:29:27Z

README.md

-| invariant | *Valid values:* A C expression that must evaluate to the C type ``int`` (used as boolean) and **may** consist of conjunctions or disjunctions, but not function calls. Local variables that have the same name as global variables or local variables of other functions can be qualified by using a data tag with the ``invariant.scope`` key. | No | Yes |
-| invariant.scope | *Valid values:* Function name <br /> The witness validator must map the variables in the given invariants to the variables in the C code. Due to scopes in C, there may be name conflicts. The witness validator will first look for a variable with a matching name in the scope of the provided function name before checking the global scope. This tag applies to the invariant as a whole. It is not possible to specify invariants about local variables of different functions. There is currently no support for different variables with the same name within different scopes of the same function. | No | Yes |
+| entry | *Valid values:* ``false`` (default) or ``true`` <br /> ``entry`` is used to mark a ``node`` as an entry node. An entry node represents the initial control state of the witness automaton. We require that exactly one initial control state is defined per document. The ``attr.type`` attribute of this key is ``boolean``. The default value is ``false``. | Yes | Yes |
+| sink | *Valid values:* ``false`` (default) or ``true`` <br /> ``sink`` is used to mark a ``node`` as a sink node. A sink node represents a sink control state in the automaton. Sink states are not allowed in correctness-witness automata. The ``attr.type`` attribute of this key is ``boolean``. The default value is ``false``. | Yes | No |


Here again we have the notion of "control state". Where is the definition of this kind of state, and how does it differ from other states?

Sink states are not allowed in correctness-witness automata

Isn't that redundant, as this is already clear from the last column in this table?

Here again we have the notion of "control state". Where is the definition of this kind of state, and how does it differ from other states?

The formal definition can be found in the upcoming paper. All states in witness automata are control states, because witness automata are protocol automata, and protocol automata consist of control states.

Isn't that redundant, as this is already clear from the last column in this table?

In some cases (like this one), I feel that it is helpful to include information from other columns (admittedly redundantly) in the detailed description.

README.md

…escription

… matching the given definition.

…ants

… thread's termination is signalled.

…n correctness witnesses; the restriction was not strong enough for the stated purpose

…ed) conditions

kfriedberger

Sometimes it is hard to see the difference in Github,
but overall I could not detect any blocking changes.

mdangl added 2 commits December 8, 2020 21:33

Copy overhauled descriptions of witness-element keys from the upcomin…

ef5f7bc

…g journal paper to the README

Copy overhauled descriptions of concurrency-witness-element keys from…

2323492

… the upcoming journal paper to the README

mdangl requested a review from MartinSpiessl December 8, 2020 20:44

MartinSpiessl suggested changes Dec 8, 2020

View reviewed changes

mdangl added 7 commits December 9, 2020 21:00

__VERIFIER_error -> reach_error in specification example in the key d…

58161d7

…escription

Clarify default values

799ef27

Clarify that the key can only be used for loops that have a loop head…

a930bb7

… matching the given definition.

Fix and improve wording for allowed values for assumptions and invari…

c4cb109

…ants

Switch back descriptions that had accidently been switched

bffa7dd

Remove trailing whitespace

16e9013

Specify how the initial function of the thread is specified and how a…

52cd6dd

… thread's termination is signalled.

mdangl mentioned this pull request Dec 21, 2020

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

Open

mdangl requested a review from kfriedberger December 21, 2020 10:53

mdangl added 2 commits December 22, 2020 11:05

Fix restriction to partitioning (i.e., non-restricting) assumptions i…

4216af3

…n correctness witnesses; the restriction was not strong enough for the stated purpose

Assumptions are allowed in correctness witnesses, under certain (stat…

90a5553

…ed) conditions

kfriedberger approved these changes Jun 23, 2021

View reviewed changes

mdangl requested a review from MartinSpiessl July 5, 2021 15:22

MartinSpiessl approved these changes Jul 6, 2021

View reviewed changes

MartinSpiessl merged commit 5fc4c23 into master Jul 6, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update descriptions of graph elements, node elements, and edge elements from upcoming TOSEM paper #37

Update descriptions of graph elements, node elements, and edge elements from upcoming TOSEM paper #37

mdangl commented Dec 8, 2020

MartinSpiessl Dec 8, 2020

mdangl Dec 9, 2020

kfriedberger Jun 23, 2021

MartinSpiessl Dec 8, 2020

mdangl Dec 9, 2020

MartinSpiessl Dec 8, 2020

mdangl Dec 9, 2020 •

edited

Loading

kfriedberger left a comment

Update descriptions of graph elements, node elements, and edge elements from upcoming TOSEM paper #37

Update descriptions of graph elements, node elements, and edge elements from upcoming TOSEM paper #37

Conversation

mdangl commented Dec 8, 2020

MartinSpiessl Dec 8, 2020

Choose a reason for hiding this comment

mdangl Dec 9, 2020

Choose a reason for hiding this comment

kfriedberger Jun 23, 2021

Choose a reason for hiding this comment

MartinSpiessl Dec 8, 2020

Choose a reason for hiding this comment

mdangl Dec 9, 2020

Choose a reason for hiding this comment

MartinSpiessl Dec 8, 2020

Choose a reason for hiding this comment

mdangl Dec 9, 2020 • edited Loading

Choose a reason for hiding this comment

kfriedberger left a comment

Choose a reason for hiding this comment

mdangl Dec 9, 2020 •

edited

Loading