Invoking the linearization point

To invoke the linearization point in the definition of a logically atomic function, we must “open” the atomic update object we were given by the atomic specification. To do so, we can use the try_open_atomic_update macro as follows:

let res_au = try_open_atomic_update!(au, mut? ax => {
    // assume atomic pre
    // ...
    // assert atomic post
    Tracked(ay)
})

When we open the atomic update, the macro consumes the atomic update. In the body of the macro call, we are then given the input ax: AX and learn the atomic precondition, and at the end of the macro call, we return the output ay: AY and prove the atomic postcondition.

The macro outputs a value of type Tracked<Result<(), AtomicUpdate<AX, AY, PredType>>>. If the atomic update is committed, as indicated by the UpdateTry trait, then the atomic update is consumed and we get Ok(()). Otherwise, if the atomic update is aborted, we get back the same atomic update we put in Err(au), allowing us to open it again later.

The resolves check

Verus requires the body of a logically atomic function to prove that the atomic update has been opened and committed by the time the function returns. We enforce this requirement using the prophecy variable au.resolves(). Initially, the value of au.resolves() is unknown; when the atomic update is resolved by the try_open_atomic_update! macro, the value of au.resolves() becomes true. The user must then prove that au.resolves() when the function returns.

Besides au.resolves(), there are two more prophecies we set when the atomic update is committed: au.input() and au.ouput(). These store the final value of ax and ay respectively. We use them internally to give the function postcondition access to the input and output resources of the atomic update.

For more complicate data structures where the resolution of the atomic update is non-trivial (such as those that exhibit “helping”), it may be necessary to assert the value of these prophecy variables manually after the AU has been committed.

Invariant masks

To open the atomic update, its outer mask must be valid in the current scope, that is, we must be able to open every invariant namespace in the set au.outer_mask() at the current program point. Inside the body of the try_open_atomic_update macro, we can only open the invariant namespaces in the set au.inner_mask(). The difference between the outer and inner mask is precisely the set of invariants which the client is allowed to open in the atomic function call.

Running examples

Here are the full definitions of our two example functions:

fn reset(var: &PAtomicU64)
    atomically (atomic_update) {
        (perm: PermissionU64) -> (commit: Commit<PermissionU64>),
        requires
            perm@.patomic == var.id(),
        ensures
            commit@@.patomic == perm@.patomic,
            commit@@.value == 0,
        outer_mask any,
        inner_mask none,
    },
{
    // open atomic update and commit
    try_open_atomic_update!(atomic_update, mut perm => {
        var.store(Tracked(&mut perm), 0);
        Tracked(Commit(perm))
    });

    // verify that the atomic update had been resolved
    assert(atomic_update.resolves());
}

Here, we open the atomic update, take the permission object for the atomic variable which we bind as mut perm, and use it to perform the store operation. Then, we commit the atomic update by returning Commit(perm) from the body of the try_open_atomic_update macro call. We can confirm that the atomic update has been resolved successfully using the assert at the end of the function body.

fn increment(var: &PAtomicU64) -> (out: u64)
    atomically (atomic_update) {
        (perm: PermissionU64)
            -> (res: Result<PermissionU64, (PermissionU64, OpenInvariantCredit)>),
        requires
            perm@.patomic == var.id(),
        ensures match res {
            Err((p, _)) => p@ == perm@,
            Ok(p) => p@.patomic == perm@.patomic
                  && p@.value == perm@.value.wrapping_add(1),
        },
        outer_mask any,
        inner_mask none,
    },
    ensures
        out == perm@.value,
{
    let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
    let tracked mut au = atomic_update;
    let mut curr;

    // open atomic update and abort for inital load
    let wrapped_au = try_open_atomic_update!(au, perm => {
        curr = var.load(Tracked(&perm));
        Tracked(Err((perm, credit)))
    });

    // recover `au` from the returned `Tracked(Err(au))`
    proof { au = wrapped_au.get().tracked_unwrap_err() };

    // compare exchange loop
    loop invariant au == atomic_update {
        let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
        let next = curr.wrapping_add(1);
        let res;

        // open atomic update again
        let maybe_au = try_open_atomic_update!(au, mut perm => {
            res = var.compare_exchange_weak(Tracked(&mut perm), curr, next);

            // dynamically commit or abort atomic update
            // depending on `compare_exchange_weak`
            Tracked(match res {
                Ok(_) => Ok(perm),
                Err(_) => Err((perm, credit)),
            })
        });

        match res {
            Ok(_) => return curr,
            Err(new) => {
                proof { au = maybe_au.get().tracked_unwrap_err() };
                curr = new;
            },
        }
    }
}

In this example, we use the abort case of the atomic update to gain temporary access of the permission object without modifying it. This allows us to perform the initial load, as well as all failed compare_exchange_weak operations, as they require access to the permission to be executed. For the initial load, we open the atomic update and abort it unconditionally. For the compare_exchange_weak on the other hand, we check if the operation was successful to determine whether the atomic update should be committed or aborted.

We note that, for Verus to accept this function definition, we need to set two verifier attributes on the function or in the module:

• #[verifier::exec_allows_no_decreases_clause] allows us to use unbounded loops in exec-mode without proving termination via a decreases clause, and
• #[verifier::loop_isolation(false)] gives us slightly better proof automation around the loop, allowing us to simplify the loop invariant quite a bit.