-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
{:concurrent} attribute support in auditor #3463
Comments
It might be even better to be clear that the only supported form of this initially would be essentially an |
Yeah, at this time, this seems like a feature of the auditor. It's seems fine to me for the auditor to give the attribute the name |
Adds support to `dafny audit` for reporting instances of the `{:concurrent}` attribute, intended to mark code that should be safe for use in concurrent settings. Fixes #3463 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Dafny verification is currently based on sequential execution of code. It CAN be safe to concurrently execute the compiled code but only under certain assumptions. For example, the .NET AWS Encryption SDK exposes entry points that are threadsafe because they do not read or write any shared state. This RFC is intended to improve the robustness of this mechanism.
This feature request is the very first baby step towards making Dafny aware of concurrency. We would provide a warning in
dafny audit
for any Dafny program element with a body (constructors, methods, and functions?) annotated with{:concurrent}
. The attribute would be a way to document the fact that the code will be used in a concurrent setting, so that the auditor can point out this assumption. The suggested mitigation would be something like "target language concurrent testing and manual review", since Dafny can't yet offer any better.Later on we could provide more options to make Dafny happy without any warnings. The RFC above would make this warning go away if the attributed element had both
reads {}
and (often implicitly)modifies {}
. Even later on when Dafny has language features to support concurrent execution, there would be ways to synchronize so that arbitrary logic could be proven correct even under concurrent execution.Calling this a language definition change even though the initial change would only be in the auditor, since it would still be establishing semantics that interact with future language features.
The text was updated successfully, but these errors were encountered: