Macro vstd::invariant::open_atomic_invariant

macro_rules! open_atomic_invariant {
    [$($tail:tt)*] => { ... };
}

Macro used to temporarily “open” an AtomicInvariant object, obtaining the stored value within.

Usage

The form of the macro looks like,

open_atomic_invariant($inv => $id => {
    // Inner scope
});

This operation is very similar to open_local_invariant!, so we refer to its documentation for the basics. There is only one difference, besides the fact that $inv should be an &AtomicInvariant rather than a &LocalInvariant. The difference is that open_atomic_invariant! has an additional atomicity constraint:

• Atomicity constraint: The code body of an open_atomic_invariant! block cannot contain any exec-mode code with the exception of a single atomic operation.

(Of course, the code block can still contain an arbitrary amount of ghost code.)

The atomicity constraint is needed because an AtomicInvariant must be thread-safe; that is, it can be shared across threads. In order for the ghost state to be shared safely, it must be restored after each atomic operation.

The atomic operations may be found in the PAtomic library. The user can also mark their own functions as “atomic operations” using #[verifier::atomic)]; however, this is not useful for very much other than defining wrappers around the existing atomic operations from PAtomic. Note that reading and writing through a PCell or a PPtr are not atomic operations.

Note: Rather than using open_atomic_invariant! directly, we generally recommend using the atomic_ghost APIs.

It’s not legal to use open_atomic_invariant! in proof mode. In proof mode, you need to use open_atomic_invariant_in_proof! instead. This takes one extra parameter, an open-invariant credit, which you can get by calling create_open_invariant_credit() before you enter proof mode.

Example

TODO fill this in