atomic methods and invariants

[jcp19]

This PR improves Gobra's situation in dealing with atomicity, so that we no longer need informal arguments to justify that opening invariants around certain parts of the code is safe. In particular, it brings the following changes:

• introduces the atomic modifier for abstract methods and functions (non-abstract atomic members are disallowed, as we cannot prove atomicity - at least for now). Atomic methods should be those whose effects occur, logically, at a single linearization point. Interface methods may be marked as atomic too, in which case they may only be implemented by atomic methods.
• Introduces the notion of invariants as found in other CSLs like Iris. A value P of type pred() is an invariant, written as Invariant(p) if it has been shown to hold using the EstablishInvariant builtin ghost function. Once established, invariants must be preserved by all atomic operations, and thus, by all operations.
• Fixes a pre-existing issue where one could not previously write P(), where P is a built-in FPredicate like PredTrue. We were forced to write PredTrue!<!>() at all times before.
• Add support for critical regions for invariants:

critical P!<!>() (
S
)

This statement opens invariant P!<!>(), which is assumed at the start of the critical region, and must be shown at its end. Critical regions check that there is no re-entrance, i.e., no invariant is opened twice. Statements in S may contain, at most, a single call to an atomic method (from an interface or otherwise, more on this later) and arbitrary ghost code (which must be shown to terminate). Like the oultine statement, the critical statement does not introduce a block (i.e., it does not introduce its own namespace).

There are two critical decisions I took to simplify the logics here:

• To avoid re-entrance, we must guarantee that no method called from a critical region of an invariant P opens P again. One way of doing this would be to have some way of tracking the currently open invariants, and specify in the method specifications which invariants are required to not be open. This requires a more complex encoding. Instead, I opted for the following split of concerns, which I think is not very limiting: ghost methods cannot open invariants. The invariants must be opened in the actual code before calling ghost methods that depend on them. Thus, ghost methods may all be called safely from critical regions. This makes checking for reentrance very easy.
• Calls to atomic interface methods are supported in critical regions, even though they are not atomic (a call to an interface method causes a lookup on the vtable to dispatch the call, and the effects of this may be observable). Nonetheless, I believe it is safe to call these methods. when S contains a call i.M(), where i is of interface type, I believe that reasoning about this program is similar to reasoning about the following:

critical P!<!>() (
resolve i.M()             // (1)
call_resolved i.M()   // (2), atomic
)

Step (1) is "transparent", i.e., its effects cannot be observed, if the value stored in i cannot change between (1) and (2), which guarantees that the method that is called still matches the dynamic type of the value stored in i. I believe that is always the case:

1. the receiver i is either in an exclusive or shared memory location.
2. If it is exclusive, it may not be changed between (1) and (2) by another thread.
3. If it is shared it may only be modified by another thread. However, to resolve the call to i.M, there must be at least read permissions to i in the current thread. The permissions may either come from from the surrounding environment or from P!<!>().
   a. If they come the former, then no other thread may ever obtain full permission to i and modify it while the call is being performed.
   b. If they come from the latter, another thread could in principle try to open P!<!>() in parallel and modify i in an atomic step. However, there is no way to do so as far as I can tell. Regular assignments to i are not atomic (and thus, disallowed in critical regions) and the package atomic does not offer a way (as far as I can see) to atomically mutate a variable of interface type.

EDIT: disallowing opening invariants in ghost methods is too restrictive after all. An example where this is very limiting is in the implementation of Iris's ghost locations in gobra-libs, where the only way to implement a model for this requires an invariant. At first sight, a solution to this may be to require an annotation on methods that may open invariants and disallow calling those methods from methods without that annotation or inside critical regions. I have implemented this solution, and I have shown that it is not super restrictive by trying it in two different proofs:

• VerifiedSCION: Remove ghost Mutex, use invariants instead VerifiedSCION#412
• Model for Resource Algebras in gobra-libs: Add body to all functions that inhaled the invariant gobra-libs#35

[jcp19]

@ArquintL you may now take a look at this PR when you have a chance.

[ArquintL]

Some thoughts about the description (not having looked at the code yet). I think fixing the description would be good for documentation purposes and feel free to also add those clarifications to the codebase where you think it would make sense

• Invariant(p): how does one know which invariants exist, i.e., how is this modular? Does EstablishInvariant provide some (pure) predicate expressing that p is an invariant that then must be propagated through a codebase such that one can open p in a critical section?
• PredTrue(): Does this PR address only built-in FPreds, i.e., built-in MPreds and non-built-in FPreds still require !< and !>?

• Instead, I opted for the following split of concerns, which I think is not very limiting

As you say, this depends on ghost methods not being able to open invariants and additionally atomic methods not having an implementation. Is there an appropriate remark in the type-checker that, should we ever relax the latter, this might introduce an unsoundness if we are not careful?

• I have implemented this solution, and I have shown that it is not super restrictive by trying it in two different proofs:

Is this solution part of this PR or will you create a separate PR to fix this limitation?

[ArquintL]

I've made a pass over the implementation without looking at the testcases yet

[ArquintL]

Is there a reason against using the same order as on L. 183?

[jcp19]

well, the two orders never matched anyway, but I don't mind changing that

[ArquintL]

That's what I noticed too. Double checking whether we assigned all of them just became increasingly difficult ^^

[ArquintL]

I hope the checks disallow gotos in here

[jcp19]

We do, the only actual statements we allow are calls to atomic functions whose parameters have been evaluated and assignments to local exclusive variables whose rhs are calls to atomic functions

[ArquintL]

Could you please document all these side-conditions at the place where we type-check critical?

[ArquintL]

Wouldn't it be cleaner do define an encoding for the critical stmt instead of making the desugarer even larger?

[jcp19]

What do you mean exactly? Introducing a critical statement in the intermediate representation?

[ArquintL]

Yes exactly

[jcp19]

@ArquintL thank you for taking the time to review the PR! I will revise the PR description to clarify your questions. For now, I will address the comments that I can address quickly, and I will come back to the bigger changes later.

[jcp19]

Answering your first comment:

Some thoughts about the description (not having looked at the code yet). I think fixing the description would be good for documentation purposes and feel free to also add those clarifications to the codebase where you think it would make sense

• Invariant(p): how does one know which invariants exist, i.e., how is this modular? Does EstablishInvariant provide some (pure) predicate expressing that p is an invariant that then must be propagated through a codebase such that one can open p in a critical section?

Yes, Invariant is a pure function that takes a pred(). EstablishInvariant consumes an instance of the predicate, and produces (duplicable) proof that the property is an invariant. When you open an invariant, you need to somehow to have learned this from a callee.

• PredTrue(): Does this PR address only built-in FPreds, i.e., built-in MPreds and non-built-in FPreds still require !< and !>?

The fix applies to all identifiers that resolve to the AstPattern BuiltInPredicate

• Instead, I opted for the following split of concerns, which I think is not very limiting

As you say, this depends on ghost methods not being able to open invariants and additionally atomic methods not having an implementation. Is there an appropriate remark in the type-checker that, should we ever relax the latter, this might introduce an unsoundness if we are not careful?

Hmm, I guess I can add sth to the type-checker of atomic methods, but I feel like these comments often go unnoticed or unmaintained when assumptions change. I think a much better way is to have tests that catch violations of expectations and design documents/PR descriptions for these features that we can later revisit.

• I have implemented this solution, and I have shown that it is not super restrictive by trying it in two different proofs:

Is this solution part of this PR or will you create a separate PR to fix this limitation?

Yes, it is already implemented in this PR.

[Felalolf]

Be aware that abstract atomic methods only appear atomic relative to some concurrency abstraction level. It's also the abstraction level that typically determines whether invariants may be opened or not. Whatever the design is, there should be a clear meaning of what the concurrency abstraction level is at a specific point in the program.

Identifying the concurrency abstraction level also makes it clear that the desired default concurrency abstraction level is different for actual and ghost methods. For actual methods, you want the top abstraction level, where no invariant is opened and thus called methods do not have to be abstract atomic. Conversely, for ghost methods, you arguably want the bottom abstraction level, so that ghost methods can be used in every context.

If it helps, I think originally, I had a design in mind where we introduce level definitions that (1) specify some static name, (2) define the invariants of that level, (3) may extend other levels.

For instance: level IO { SCION_IO_pred }; level IO2 extends IO { ... }.

For the level lattice, we introduce a "prev(L)" level that expresses the level just below level L (i.e. prev(L) < L and L' < prev(L), if L' extends L). Furthermore, there are some bottom and top elements. Analogously to your critical block, there would be an open level block that checks that the invariant of that level has been established and then opens these invariants. The open level block also requires that the current context level is at most the opened level and sets the context level to "prev" of the openened level. To check context levels statically, methods are annotated with their context level.

EDIT: If you only want to support the case where at most a single predicate is opened at a time, you could flatten my design such that the predicate name becomes the level.

[jcp19]

Well, I am making this PR a draft until I have some time to revise the docs. The current version is not conveying the ideas from the current design.

@Felalolf I would argue this PR implements a level system, although it does not make it explicit. Check my comments below:

Be aware that abstract atomic methods only appear atomic relative to some concurrency abstraction level. It's also the abstraction level that typically determines whether invariants may be opened or not. Whatever the design is, there should be a clear meaning of what the concurrency abstraction level is at a specific point in the program.

I would argue that this is the case already (once again, I recognize the docs need to be revised). At any rate, the current design fits very nicely the story of the levels. Implicitly, levels correspond to the sets of open invariants. For each non-ghost non-atomic member, its level is Top (which corresponds to an empty set -- more on this below). For each ghost member (they cannot be marked atomic), the default (more on this later) level is bottom (that would correspond to the set of all predicate instances). For every atomic member (which at the moment must be abstract), the level corresponds to bottom too. The syntactic constraints and proof obligations introduced in this PR follow from these conditions; in particular, by default, ghost methods may not open invariants and non-ghost non-abstract methods may not be called from critical regions -- a critical region is always associated with one invariant, and opening the invariant lowers the level. Notice that the current constraints for all invariants to be restored by the end of every non-ghost method.

Identifying the concurrency abstraction level also makes it clear that the desired default concurrency abstraction level is different for actual and ghost methods. For actual methods, you want the top abstraction level, where no invariant is opened

Yes. I hope my comment above makes it clear this is already the case.

and thus called methods do not have to be abstract atomic.

I am not sure I get what you mean by this. Do you mean that we could in principle allow calls to non-ghost non-atomic methods that do not open any invariants from critical regions?

Conversely, for ghost methods, you arguably want the bottom abstraction level, so that ghost methods can be used in every context.

I agree that is a good default, but it is very limiting in some cases. For example, if you have an invariant that grants you permission to a global ghost variable and want to open it in a ghost method, you wouldn't be able to do so with this choice of level. A good example for this is my model for Resource Algebras in gobra-libs (a link for this is in the PR description). That is why I introduced an annotation opensInvariants for ghost methods only that corresponds to marking the level of a ghost member to Top (this also prevents it from being called from critical regions). @ArquintL this comment may help clarify the role of the annotation opensInvariants.

If it helps, I think originally, I had a design in mind where we introduce level definitions that (1) specify some static name, (2) define the invariants of that level, (3) may extend other levels.

For instance: level IO { SCION_IO_pred }; level IO2 extends IO { ... }.

Hmm, I don't see a compelling reason (I am happy to be convinced of the contrary) for making levels a top-level member. Also, I guess this proposal covers 0-ary predicates. What would be your proposal if the predicates in a level declaration had to be parameterized by a value obtained from a methods "execution"?

For the level lattice, we introduce a "prev(L)" level that expresses the level just below level L (i.e. prev(L) < L and L' < prev(L), if L' extends L). Furthermore, there are some bottom and top elements. Analogously to your critical block, there would be an open level block that checks that the invariant of that level has been established and then opens these invariants. The open level block also requires that the current context level is at most the opened level and sets the context level to "prev" of the openened level. To check context levels statically, methods are annotated with their context level.

Given the interpretation of the levels as sets of open invariants, L1 < L2 iff L2 is a subset of L1 (i.e., L2 opens all the invariants of L1 and some more). The encoding keeps track of the set of open invariants (opening an invariant adds it to the set of open invariants if it is not there already, otherwise it gives a verification error; closing an invariant removes it from the set of open invariants). I think annotating methods with their context level could be useful, but I guess this could not be done purely syntactically (for example, if the invariants may be parameterized by values obtained during the method "execution"). I considered this possibility, but I find the current defaults, as well as the extra flexibility afforded by the opensInvariants annotation to be enough. I am happy to be convinced of the contrary if any users show me practical examples where this is too limiting and no obvious workaround exists.

EDIT: If you only want to support the case where at most a single predicate is opened at a time, you could flatten my design such that the predicate name becomes the level.

Hmm, I find this too limiting. The current design already supports opening multiple invariants at a time.

[Felalolf]

I would argue that this is the case already

I meant that the connection to concurrency abstraction levels should be defined explicitly in the documentation. The connection is a key part of the soundness argument of whatever design is picked.

I am not sure I get what you mean by this.

I just meant that we do not have to check which methods are called from non-atomic methods (regarding levels).

Hmm, I don't see a compelling reason (I am happy to be convinced of the contrary) for making levels a top-level member.

Since I was not sure whether you saw my original design, I just wanted to share it. I do not expect you to use any part of it.

Hmm, I find this too limiting. The current design already supports opening multiple invariants at a time.

I might be missing something, but since this PR does not intend to add the ability to prove abstract atomicity, I am not sure where we would need to open multiple invariants at the same time. Information hiding can be achieved through standard predicates that are unfolded and folded as usual. EDIT: I did come up with cases where we want to open multiple invariants at the same time.