Add auditor support for the :concurrent attribute
#3660
Conversation
There was a problem hiding this comment.
We should add this to the reference manual too at a minimum (and hopefully guide users to that entry for details). Perhaps we could even point to dafny-lang/rfcs#6 as the necessary change to support proving this in many cases?
|
|
||
| ### Member `ConcurrentMethod` | ||
|
|
||
| * Declaration has `{:concurrent}` attribute. MUST manually review and test in a concurrent setting. |
There was a problem hiding this comment.
Does the auditor have a way of guiding the user to further documentation about a particular class of assumption and mitigation? I feel like this one deserves a bit of text about how Dafny can't (yet) analyze this for you etc.
There was a problem hiding this comment.
It might make sense to add some text including a link to documentation, for all of the assumption types. I'll look into that.
There was a problem hiding this comment.
I updated the reference manual to describe all of the forms of assumption that the auditor reports, including a link to rfcs#6 in the bullet for {:concurrent}. The generated report currently doesn't include a link to that section of the manual, however.
There was a problem hiding this comment.
I think that's good enough for now at least, so a user can search the manual for that attribute and get a hit.
| @@ -0,0 +1 @@ | |||
| The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. | |||
There was a problem hiding this comment.
| The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. | |
| The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended to be safe for use in a concurrent setting. |
"but can't be proven" implies there is could that could be proven safe, but Dafny can't do that yet.
|
|
||
| ### Member `ConcurrentMethod` | ||
|
|
||
| * Declaration has `{:concurrent}` attribute. MUST manually review and test in a concurrent setting. |
There was a problem hiding this comment.
I think that's good enough for now at least, so a user can search the manual for that attribute and get a hit.
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Adds support to
dafny auditfor reporting instances of the{:concurrent}attribute, intended to mark code that should be, but can't be proven to be, safe for use in concurrent settings.Fixes #3463
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.