Reads clauses on methods #6

robin-aws · 2021-09-21T00:03:47Z

No description provided.

text/0000-reads-clauses-on-methods.md

keyboardDrummer · 2021-09-22T11:44:15Z

text/0000-reads-clauses-on-methods.md

+ if n <= 2 {
+ return 1;
+ }
+ var cached := cache.Get(n);


cache is implicit for this.cache, so it reads this, right? Then the call in SafeFibonacci would not compile.

Or are you saying the reads this is not necessary because cache is const? But I would think we don't know whether ExternalMutableMap is mutable or not, so even if the field is const, that doesn't mean reading it is thread-safe.

That's right, reads and modifies only care about mutable fields, so vars are in scope but not consts. I agree that's a bit surprising but already how reads works on functions.

Sure, we don't "know" if ExternalMutableMap is mutable since the verifier has no visibility into the external code. But there's no way around that, and modelling the assumptions we might make about external code using ghost state as in https://github.com/dafny-lang/dafny/wiki/Modeling-External-State-Correctly breaks down if that external state can change without Dafny being aware of it. The idea here is to verify that a method does not interact with any mutable state on the Dafny heap, but may still interact with "the outside world", and it's up to the external code to be thread-safe when necessary.

And if ExternalMutableMap was not implemented externally, how would you know that it's immutable?

Discussed this offline to understand the question better, and I can clarify how this all works with a few more details.

Note that clauses such as reads and modifies are not recursive. Take these classes as an example:

class A { constructor() {} var foo: int var b: B } class B { var bar: int }

If you had an object a: A, the clause reads {a} would only allow you to reference a.foo, but NOT a.b.foo. For the latter to be allowed, you would need reads {a, a.b}. This is why the Valid() / Repr idiom described in Chapters 8 and 9 of Using Dafny, an Automatic Program Verifier is useful for tracking what areas of the heap your code needs to read and write, without depending on the internals of your components.

That means Dafny doesn't allow the cache.Get call because it believes ExternalMutableMap is immutable, it's allowed because the cache.Get method has reads {}, which means the method does not read any state in the Dafny heap.

Btw, I presume that reads clauses are subject to themselves. That is, a reads clause has to be "closed", in the same way that they are for functions. Their well-formedness should then also be allowed to assume the method precondition, just as for functions. (The Dafny verifier has an encoding for this kind of thing. Look for the parameter called delayedReadsChecks or something like that.)

keyboardDrummer · 2021-09-22T11:46:53Z

text/0000-reads-clauses-on-methods.md

+
+This proposal does not aim to add concurrency primitives to Dafny, or even propose any particular choice of paradigm for asynchronous or concurrent execution. Instead, it supports verifying that a particular method is safe to use in a concurrent environment, by verifying that it does not operate on any mutable state unsafely.
+
+# Guide-level explanation


This section doesn't describe any use-cases that require something other than reads {}, so why not introduce a more restricted construct like threadsafe ? That gives less freedom to the programmer, so less chance of confusion, and you could relax the associated checks in the future, for example to allow reading passed in arguments as long as they are immutable or owned by the callee.

Other reads frames are necessary on internal methods (i.e. not exposed to external code) in the control flow though. For example, FibonacciMemoizer.Get has to declare reads this, because otherwise the default spec of reads * would violate the tighter reads {} frame of SafeFirstNFibonaccis.

I would actually argue that reusing an existing concept in a very similar additional context is a lower cognitive burden on programmers than a new concept like threadsafe (and again I'm trying not to introduce the concept of a "thread" unless we're 100% sure that's the right concurrency model for Dafny).

I would actually argue that reusing an existing concept in a very similar additional context is a lower cognitive burden on programmers than a new concept

I guess that's a difficult thing to determine, but I was thinking that if there is a specific pattern (reads {}) used for a specific use-case (calling externally exposed methods concurrently), it does help to name that use-case and remove the need for the pattern.

Other reads frames are necessary on internal methods (i.e. not exposed to external code) in the control flow though. For example, FibonacciMemoizer.Get has to declare reads this, because otherwise the default spec of reads * would violate the tighter reads {} frame of SafeFirstNFibonaccis.

I see. I'm a little confused by the file text/guide-level-explanation-example-1.dfy which has similar but different content that's what's inline in text/0000-reads-clauses-on-methods.md. The former has reads this but the latter one doesn't.

Given that FibonacciMemoizer.Get doesn't take any reference type parameters, isn't reads this the upper bound of what it can read so reads this can be implicit?

I guess that's a difficult thing to determine, but I was thinking that if there is a specific pattern (reads {}) used for a specific use-case (calling externally exposed methods concurrently), it does help to name that use-case and remove the need for the pattern.

That's true. I could imagine something like {:threadsafeExtern}, or some way of parameterizing {:extern}. It wouldn't eliminate the need for reads clauses in general in order to verify this property, though. You'd have to either have that annotation imply reads {} or require that such methods also declare reads {} explicitly, and I'd likely prefer the latter.

Given {:extern} is currently very weakly specified and already has several other sharp edges (https://github.com/dafny-lang/dafny/labels/foreign-function-interface), it's my preference to leave this out of scope for now, just as we also want to leave any concurrency semantics for Dafny out of scope if we can.

I see. I'm a little confused by the file text/guide-level-explanation-example-1.dfy which has similar but different content that's what's inline in text/0000-reads-clauses-on-methods.md. The former has reads this but the latter one doesn't.

Ah that's my fault for letting the two versions get out of sync. I was hoping to find a way to include the source files into the markdown. I've deleted them and put the missing reads this clause into the example.

Some classes will only have const fields, so some class methods can declare reads {} rather than reads this. I'm still thinking making the default reads * everywhere would be better for simplicity.

That's true. I could imagine something like {:threadsafeExtern}, or some way of parameterizing {:extern}. It wouldn't eliminate the need for reads clauses in general in order to verify this property, though. You'd have to either have that annotation imply reads {}

Yes, that was what I was thinking of

or require that such methods also declare reads {} explicitly, and I'd likely prefer the latter.

I think I agree that reads clauses on methods are the more lightweight feature to add since it doesn't introduce any new concept.

If we're okay with a keyword like threadsafe, then the language could say the following:

A method that is not declared to be threadsafe is not allowed to have a reads clause. Such a method is allowed to read anything (just like today).

A method declared with threadsafe method is allowed to have a reads clause. We now even have the freedom to say that the default reads clause for a threadsafe method is the empty set. This would make it consistent with both reads and modifies clauses today. Furthermore, this would completely address my concern about beginning users getting the wrong idea that they must declare the reads set for method -- if they ever see, or try to declare, a method with a reads clause, then that method is declared as threadsafe method, which the user can identify.

text/0000-reads-clauses-on-methods.md

RustanLeino

This looks really good. My concerns about beginners developing the incorrect idea that methods must have reads clauses is captured in the RFC. We could consider a command-line option that opts in to using reads clauses, and without which beginners would get an error for trying a reads clause on a method.

I have but one comment of substance, which concerns ghost state. For example, it seems to me that lemmas should be callable from anywhere, even though they may actually read state. Probably, the same goes for ghost methods. But what about reading mutable ghost fields? Do such reads have to be declared as well? (If the answer is not clear, a first implementation could be conservative and treat ghost state in the same way as non-ghost state.)

RustanLeino · 2021-09-29T22:43:05Z

text/0000-reads-clauses-on-methods.md

+{
+ var memoizer := new FibonacciMemoizer();
+ rs := [];
+ for i := 1 to n + 1 {


If you want the first n Fibonacci numbers, you want

Suggested change

for i := 1 to n + 1 {

for i := 0 to n {

As written, you'll get the first n + 1 Fibonacci numbers, except the first one.

RustanLeino · 2021-09-29T22:48:56Z

text/0000-reads-clauses-on-methods.md

+//
+class {:extern} ExternalMutableMap<K, V> {
+ constructor {:extern} () reads {}
+ method {:extern} Put(k: K, v: V) reads {}


You'd expect a nonempty modifies clause for Put. Add modifies this.

This also means that FibonacciMemoizer.Get on L139 needs a modifies clause. (Without the usual Repr/Valid() abstraction, this can be done with modifies cache. With this change, it would then be fair to clients to add the postcondition ensures fresh(cache) to the FibonacciMemoizer constructor.)

Believe it or not, no! The entire point here is to NOT model the external state in Dafny frames at all. To Dafny, an ExternalMutableMap is a completely opaque object, and its methods have non-deterministic behavior. This means this has no mutable state and adding modifies this will just add confusion and probably more verification difficulties.

RustanLeino · 2021-09-29T23:01:19Z

text/0000-reads-clauses-on-methods.md

+
+The biggest potential drawback is that inexperienced Dafny programmers might have the incorrect impression that defining a tight `reads` clause for methods is necessary, and hence expend unnecessary effort for no benefit. The verifier would never prompt users to add `reads` clauses unless they already appear elsewhere in a codebase, so the issue is more that they could see them used in documentation or examples and not realize they are largely optional.
+
+Reusable Dafny code such as the modules in https://github.com/dafny-lang/libraries will need to specify `reads` clauses in order to support consumers that need to specify them. This does not appear to be a significant burden: at the time of writing this the `libraries` repo only contained one `method`. All other uses of the `method` keyword were in defining `function method`s instead, which already default to `reads {}` and hence can be used as is in the control flow of methods with `reads` clauses. Also note that adding a `reads` clause to a method that does not already have one will never break existing callers of that method. Again, the issue is more that users could imitate standard library `method` definitions and include superfluous `reads` clauses. The answer is likely to document explicitly why the standard library uses this feature and to emphasize that it should not be copied blindly. There is already a similar issue with the standard library's use of `{:trigger}` attributes, which are not encouraged in most Dafny codebases.


The sentence about function method does not seem relevant. (Functions already have reads clauses, and details of where the letters method appear (perhaps in comments?) have no bearing on the RFC.) I suggest dropping the sentence.

RustanLeino · 2021-09-29T23:04:21Z

text/0000-reads-clauses-on-methods.md

+# Unresolved questions
+[unresolved-questions]: #unresolved-questions
+
+- Parsing is simplest if `reads` clauses are allowed on all `method`-like definitions, including the various flavours of lemmas. Allowing `reads` clauses on lemmas seems harmless, but are there downsides?


The parser already disallows modifies clauses on lemma declarations. The parser could do something similar for reads.

RustanLeino · 2021-09-29T23:07:24Z

text/0000-reads-clauses-on-methods.md

+When sharing state externally really is necessary, it must be implemented externally in native code, where native facilities for synchronizing access to mutable state can be used. Therefore the solution is to push the caching logic into the target language instead:
+
+```dafny
+datatype Option<T> = Some(value: T) | None


I suggest moving this type definition down below the ExternalMutableMap. I found myself reading it and the sentence above it several times, trying to figure out their connection, until I realized the sentence above has nothing to do with datatypes and that this datatype is introduced only to support the example.

RustanLeino

I suggest that the RFC spell out explicitly that the by method part of a function by method also needs to check reads clauses. In particular, the by method must live up to the same reads clause as the function has. This is required for soundness. More precisely, in order to rely on the proposed method reads clauses when determine a program to be "thread safe", it would not be okay if the by method part read the heap in places where the caller is not aware (which is allowed today).

seebees · 2023-02-09T00:57:18Z

I need to read the full RFC, but my question is:
Since a methods reads clause bounds the things it can read
does this mean that I can be much more permissive in state that I return?

When proving things with complex frames I find I have to protect
agains crazy developers who just might randomly add an object into my frame.
(I use Modifies: set<object> because Repr is to opaque)
I do this with fresh(Modifies - old(Modifies)).
But if I understand what is happening here
if I define reads Modifies then I would not need to have the above correct?

If this is true, this would be amazing in terms of simplifying the mental model to verify mutation.

keyboardDrummer · 2023-08-17T08:16:02Z

text/0000-reads-clauses-on-methods.md

+
+If this class is compiled to C#, for example, and its instances are shared between multiple threads, its verified properties are no longer true. If two threads both invoke `Increment` on a single counter, the effect could easily be to only increment `x` once, since reading and writing `x` does not occur atomically. Even the post-condition on `Get` is no longer valid, because the value of `x` could change in-between reading its value and returning from the compiled body.
+
+This proposal does not aim to add concurrency primitives to Dafny, or even propose any particular choice of paradigm for asynchronous or concurrent execution. Instead, it supports verifying that a particular method is safe to use in a concurrent environment, by verifying that it does not operate on any shared mutable state.


by verifying that it does not operate on any shared mutable state.

Can't you also achieve that by controlling which arguments are passed to the method? If the (static) method doesn't have any pointers to traverse from, then it can't read from or write to any mutable state, can it?

That could work too! But there are a few downsides to that approach:

The analysis to traverse all paths from a value to find any potential mutable state doesn't exist as any part of Dafny's implementation already, and would have to deal with some tricky cases where it would have to be overly conservative (e.g. if you have a generic method that takes a T value, you'd probably have to be safe and reject it just in case it ends up making mutable state reachable). The framing approach is quite a bit cheaper to implement since modifies already exists and reads can heavily reuse its verification machinery.

That analysis would not be compatible with modular verification, since you'd need to look inside dependent modules in case there is any mutable state lurking there. Whereas reads and modifies frames will be/are part of the specification of module contents.

Rejecting any input connected to mutable state is more restrictive than necessary, since there's no danger if you don't actually read or write that state.

Ok, thanks !

Implements dafny-lang/rfcs#6. This functionality is guarded by a new `--reads-clauses-on-methods` option, even though it's almost completely backwards compatible: the only wrinkle is function-by-methods, where valid code today might be rejected when the reads clause of the function definition is applied to the by-method body. Note that "methods" here is interpreted as it is in the Dafny reference manual and similar documentation: it includes constructors and ghost methods, but NOT lemmas. The `{:concurrent}` attribute, which previously only existed to generate an auditor warning that Dafny could not verify this property, now creates assertions that the `reads` and `modifies` clauses on the function or method are empty. The core implementation strategy is relatively straightforward: enabling reads checks (via the `WFOptions` value) in the well-formedness check for statements as well as expressions. The existing `$_Frame` variable is now split into `$_ReadsFrame` and `$_ModifiesFrame`, since we now need both at once in method contexts. To help make reads checks optional based on the new option, and to optimize by not enabling them when in a `reads *` context (the default for methods), the `ExpressionTranslator.readsFrame` field may be null. I performed some mild refactoring to make this cleaner but open to suggestion on further improvements. Documentation changes preview at https://robin-aws.github.io/dafny/. <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>

robin-aws added 6 commits September 18, 2021 11:14

Partial progress

a4791e0

More progress

dca81f2

Filled out remaining sections, need to tweak code examples

47df41d

More example code

b3274cc

Improved examples

5de90e6

Addressed the last todo

668cf87

robin-aws marked this pull request as ready for review September 21, 2021 17:09

keyboardDrummer reviewed Sep 22, 2021

View reviewed changes

robin-aws mentioned this pull request Sep 22, 2021

Lazy sequence concatenation in Java runtime is not thread-safe dafny-lang/dafny#1454

Closed

nchong-at-aws reviewed Sep 23, 2021

View reviewed changes

text/0000-reads-clauses-on-methods.md Outdated Show resolved Hide resolved

robin-aws added 3 commits September 24, 2021 10:44

Improve example

a34635d

Wording tweak

15e4731

Remove out-of-sync Dafny source files

1762c7f

RustanLeino approved these changes Sep 29, 2021

View reviewed changes

robin-aws mentioned this pull request Oct 22, 2021

feat: AwsKmsMrkAwareSymmetricKeyring aws/aws-encryption-sdk-dafny#383

Merged

robin-aws self-assigned this Nov 6, 2021

robin-aws added the enhancement New feature or request label Nov 8, 2021

RustanLeino reviewed Jul 8, 2022

View reviewed changes

robin-aws mentioned this pull request Feb 6, 2023

{:concurrent} attribute support in auditor dafny-lang/dafny#3463

Closed

keyboardDrummer reviewed Aug 17, 2023

View reviewed changes

PR feedback

a69a452

robin-aws mentioned this pull request Aug 25, 2023

feat: Read clauses on methods dafny-lang/dafny#4440

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reads clauses on methods #6

Reads clauses on methods #6

robin-aws commented Sep 21, 2021

keyboardDrummer Sep 22, 2021

robin-aws Sep 22, 2021

keyboardDrummer Sep 27, 2021

robin-aws Sep 29, 2021

RustanLeino Sep 29, 2021

keyboardDrummer Sep 22, 2021 •

edited

Loading

robin-aws Sep 22, 2021

keyboardDrummer Sep 27, 2021

robin-aws Sep 27, 2021

keyboardDrummer Sep 28, 2021 •

edited

Loading

RustanLeino Sep 29, 2021

RustanLeino left a comment

RustanLeino Sep 29, 2021

RustanLeino Sep 29, 2021

robin-aws Nov 5, 2021

RustanLeino Sep 29, 2021

RustanLeino Sep 29, 2021

RustanLeino Sep 29, 2021

RustanLeino left a comment

seebees commented Feb 9, 2023

keyboardDrummer Aug 17, 2023 •

edited

Loading

robin-aws Aug 17, 2023

keyboardDrummer Aug 18, 2023


		This proposal does not aim to add concurrency primitives to Dafny, or even propose any particular choice of paradigm for asynchronous or concurrent execution. Instead, it supports verifying that a particular method is safe to use in a concurrent environment, by verifying that it does not operate on any mutable state unsafely.

		# Guide-level explanation


		The biggest potential drawback is that inexperienced Dafny programmers might have the incorrect impression that defining a tight `reads` clause for methods is necessary, and hence expend unnecessary effort for no benefit. The verifier would never prompt users to add `reads` clauses unless they already appear elsewhere in a codebase, so the issue is more that they could see them used in documentation or examples and not realize they are largely optional.

		Reusable Dafny code such as the modules in https://github.com/dafny-lang/libraries will need to specify `reads` clauses in order to support consumers that need to specify them. This does not appear to be a significant burden: at the time of writing this the `libraries` repo only contained one `method`. All other uses of the `method` keyword were in defining `function method`s instead, which already default to `reads {}` and hence can be used as is in the control flow of methods with `reads` clauses. Also note that adding a `reads` clause to a method that does not already have one will never break existing callers of that method. Again, the issue is more that users could imitate standard library `method` definitions and include superfluous `reads` clauses. The answer is likely to document explicitly why the standard library uses this feature and to emphasize that it should not be copied blindly. There is already a similar issue with the standard library's use of `{:trigger}` attributes, which are not encouraged in most Dafny codebases.


		If this class is compiled to C#, for example, and its instances are shared between multiple threads, its verified properties are no longer true. If two threads both invoke `Increment` on a single counter, the effect could easily be to only increment `x` once, since reading and writing `x` does not occur atomically. Even the post-condition on `Get` is no longer valid, because the value of `x` could change in-between reading its value and returning from the compiled body.

		This proposal does not aim to add concurrency primitives to Dafny, or even propose any particular choice of paradigm for asynchronous or concurrent execution. Instead, it supports verifying that a particular method is safe to use in a concurrent environment, by verifying that it does not operate on any shared mutable state.

Reads clauses on methods #6

Are you sure you want to change the base?

Reads clauses on methods #6

Conversation

robin-aws commented Sep 21, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 22, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 28, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RustanLeino left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RustanLeino left a comment

Choose a reason for hiding this comment

seebees commented Feb 9, 2023

keyboardDrummer Aug 17, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Sep 22, 2021 •

edited

Loading

keyboardDrummer Sep 28, 2021 •

edited

Loading

keyboardDrummer Aug 17, 2023 •

edited

Loading