feat: {:assume_concurrent} attribute #4563
Conversation
…fny into attributes-on-reads-clauses
…ume-concurrent-attribute # Conflicts: # Source/DafnyCore/Auditor/Assumption.cs # Test/auditor/TestAuditor.dfy.expect
| @@ -1018,6 +1018,9 @@ public class Printer { | |||
|
|
|||
| int ind = indent + IndentAmount; | |||
| PrintSpec("requires", method.Req, ind); | |||
| if (options.Get(CommonOptionBag.ReadsClausesOnMethods)) { | |||
There was a problem hiding this comment.
This looks like a fix. I'm ok putting it in this PR as I don't expect this PR to cause issue, but normally I'd prefer to have a separate PR for fixes.
There was a problem hiding this comment.
Agreed on both points.
There was a problem hiding this comment.
Rustan ended up beating me to this one :) although I added an explicit ReadsOnMethods_Printing.dfy test to make sure that my check for the option wasn't necessary.
| @@ -74,6 +74,10 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFor | |||
| yield return new Assumption(this, tok, AssumptionDescription.ExternWithPrecondition); | |||
| } | |||
|
|
|||
| if (Attributes.Contains(Reads.Attributes, Attributes.AssumeConcurrentAttributeName)) { | |||
There was a problem hiding this comment.
Because functions always rely on all their reads to be immutable from verification point of view, I would actually remove the ability to put {:concurrent} in front of a function.
Methods, on the other hand, can encode non determinism by calling other methods, so for concurrency support, I'd remove functions as potential entry point altogether to avoid pitfalls.
There was a problem hiding this comment.
I'm totally willing to only support {:assume_concurrent} on methods, since as you say the risk of allowing non-empty reads and modifies on functions is greater, and I don't know of any use cases that want it on functions (e.g. smithy-dafny never generates any function entry points with reads clauses).
But I don't see any reason to not allow a {:concurrent} function with an empty reads clause, and smithy-dafny does generate function entry points for operations with the @readonly trait.
There was a problem hiding this comment.
At this stage, I'm fine with {:concurrent} on both methods and functions, provided we don't have {:assume-concurrent} on functions.
Test/dafny0/ConcurrentAttribute.dfy
Outdated
| } | ||
|
|
||
| // Auditor warning for {:assume_concurrent} | ||
| // TODO: Release notes! |
…ume-concurrent-attribute # Conflicts: # Source/DafnyCore/AST/Grammar/Printer.cs # Source/DafnyCore/Verifier/Translator.cs
Plus test to verify it isn’t necessary
…fny into assume-concurrent-attribute
robin-aws
added
run-deep-tests
This attribute complements the new verification support for
{:concurrent}, to encode the assumption that a declaration is safe to execute concurrently despite having non-emptyreadsormodifiesclauses.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.