{:concurrent} attribute support in auditor

[robin-aws]

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.

[robin-aws]

It might be even better to be clear that the only supported form of this initially would be essentially an {:axiom}. I'm not sure what syntax is best though - I'm not a huge fan of {:concurrent "axiom"}. If we were using this syntax suggested in #3149 I would suggest @Concurrent(axiom := true). {:concurrent true} is not good because it mixes up whether the concurrent-safe requirement is on or off at all with whether it is proven or assumed.

[RustanLeino]

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 {:concurrent}.