`atomic` methods and invariants by jcp19 · Pull Request #983 · viperproject/gobra

jcp19 · 2025-12-23T10:01:19Z

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:

the receiver i is either in an exclusive or shared memory location.
If it is exclusive, it may not be changed between (1) and (2) by another thread.
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 · 2026-01-25T22:00:13Z

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

ArquintL · 2026-02-02T14:58:39Z

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 · 2026-02-02T15:01:01Z

src/main/antlr4/GobraParser.g4

+specification returns[boolean trusted = false, boolean pure = false, boolean mayInit = false, boolean opensInv = false, boolean atomic = false, boolean opaque = false;]:
  // Non-greedily match PURE to avoid missing eos errors.
-  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | MAYINIT {$mayInit = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? backendAnnotation?
+  ((specStatement | OPAQUE {$opaque = true;} | PURE {$pure = true;} | OPENSINV {$opensInv = true;} |  MAYINIT {$mayInit = true;} | ATOMIC {$atomic = true;} | TRUSTED {$trusted = true;}) eos)*? (PURE {$pure = true;})? (ATOMIC {$atomic = true;})? backendAnnotation?


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

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

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

src/main/resources/builtin/builtin.gobra

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

...ain/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostTyping.scala

src/main/scala/viper/gobra/ast/frontend/Ast.scala

ArquintL · 2026-02-02T15:53:05Z

src/main/scala/viper/gobra/frontend/Desugar.scala

+              )(exprSrc)
+              _ <- write(inhaleInv)
+
+              // stmts


I hope the checks disallow gotos in here

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

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

src/main/scala/viper/gobra/frontend/Desugar.scala

ArquintL · 2026-02-02T15:55:15Z

src/main/scala/viper/gobra/frontend/Desugar.scala

+              )(exprSrc)
+              _ <- write(markClosed)
+
+            } yield exhaleInv


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

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

Yes exactly

src/main/scala/viper/gobra/frontend/Desugar.scala

src/main/scala/viper/gobra/reporting/VerifierError.scala

jcp19 · 2026-02-04T10:09:05Z

@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.

Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>

jcp19 · 2026-02-04T10:42:08Z

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.

The goal of this PR is to bring down the TCB of our resource algebra formalization to what I believe is the smallest possible TCB that we can have given the absence of existentially quantified permissions in Gobra. Our assumptions are all listed in file `docs.gobra`, and only have to do with the introduction and elimination of existential quantifiers. There are a couple of todos here: - [ ] (maybe) clean up the code and use the implementations for MonoSet and MonoMap instead of the bespoke cooliomapio and cooliosetio :) - [x] Make `GlobalMem()` an invariant established during initialization and replace the `inhale`/`exhale` pairs with code to open the invariant. Done in #35, but it depends on viperproject/gobra#983. - [ ] Prove the last outstanding assumption: the product of all currently allocated elements for a reference is valid (might do this in a separate PR) (#36) PS: I introduced a new packet rather than changing package `resalgebra`, as the API for RAs changed slightly. I might deprecate `resalgebra` soon though

jcp19 added 8 commits December 22, 2025 15:26

backup

b88b89b

add support for marking methods as atomic

0ec1a01

add check for termination for atomic methods

cdb92b1

fix tests

a2d5080

add more lexer rules

39198a3

fix typo

62e7a86

regenerate parser

979d876

Merge branch 'master' into atomicAndInvs

9db8f6f

jcp19 mentioned this pull request Jan 21, 2026

Add model for ghost locations viperproject/gobra-libs#31

Merged

3 tasks

jcp19 added 5 commits January 23, 2026 11:29

Merge branch 'master' into atomicAndInvs

30d9b0f

tests

8aa52cb

add support for parser

61a4218

add encoding and error messages

4d950a2

add type checks

9e4af81

jcp19 mentioned this pull request Jan 25, 2026

Add body to all functions that inhaled the invariant viperproject/gobra-libs#35

Open

jcp19 added 4 commits January 25, 2026 17:15

fix parsing tests

127928c

add missing restriction

ada03c9

fix check

97db219

fix typing of method receivers

db94648

jcp19 mentioned this pull request Jan 25, 2026

Remove ghost Mutex, use invariants instead viperproject/VerifiedSCION#412

Open

jcp19 added 4 commits January 25, 2026 20:33

make typing rules less strict

5b9253b

add more tests

8403fd5

add more tests

b7be63e

add more tests

7cac033

jcp19 requested a review from ArquintL January 25, 2026 21:59

jcp19 marked this pull request as ready for review January 25, 2026 21:59

jcp19 added 3 commits January 26, 2026 08:28

add one more test, fix the position of a test annotation

dec8198

add invariant to preserve openInvs

aed4e4a

fix issue with new invariant

627147e

ArquintL reviewed Feb 2, 2026

View reviewed changes

Apply suggestions from code review

de617aa

Co-authored-by: Linard Arquint <ArquintL@users.noreply.github.com>

Conversation

jcp19 commented Dec 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcp19 commented Jan 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ArquintL commented Feb 2, 2026

Uh oh!

ArquintL left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

jcp19 commented Feb 4, 2026

Uh oh!

jcp19 commented Feb 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jcp19 commented Dec 23, 2025 •

edited

Loading

jcp19 commented Jan 25, 2026 •

edited

Loading