logical atomicity

[tjhance]

Logical atomicity

Verus needs to support logical atomicity to be a serious concurrency-verification platform. It's possible to implement logical atomicity with traits or with "proof closures"; however, I think Verus should have logical atomicity as a built-in feature.

Background: Logical atomicity in Iris

Iris uses the following notation for logical atomicity:

  private_precondition -∗ <<{ ∀∀ x, atomic_precondition }>>
    code @ E
  <<{ ∃∃ y, atomic_postcondition | z, RET return_value; private_postcondition }>>

The atomic_precondition and atomic_postcondition can
manipulate resources owned by the atomic invariant, while the private_precondition and private_postcondition use thread-owned resources.

In Iris, "logical atomicity" can be accomplished by higher-order state: rather than opening an invariant "around" an operation, we can pass in a "ghost update" that is invoked at the "linearization point". This atomic update is therefore allowed to manipulate the resources in the atomic invariant.

private_precondition -∗
AU(x. atomic_precondition, y. atomic_postcondition) -∗
  wp (RET return_value, private_postcondition)

Where:

AU(x. atomic_precondition, y. atomic_postcondition) :=
    |={E, E'}=> ∃ x, atomic_precondition
        ∗ ∀ y , atomic_postcondition ={E', E}=∗ True

(This is not quite right but close enough for now.)

Now, this can be emulated in Verus using proof closures (or traits), sort of. One limitation with Verus is that proof functions can't change the mask, though even if we had that capability, it would still be incredibly tedious to do all that setup.

Therefore, it would be nice to have a concise logically-atomic spec notation in Verus, like in Iris. However, unlike Iris, Verus lacks the higher-order capabilities to define Hoare triple specifications within its own logic. I believe we should add logical atomicity as a built-in feature.

Verus notation for calling a LA function

A more ergonomic approach would be one that doesn't require the caller to setup proof closures, instead letting them seemlessly integrate the proof code into the body of the caller function.

For example, suppose latomic_fn is a logically atomic function. In order to capture the intuition that "a logically atomic function can be treated as if it were atomic", we would like to be able to write:

open_atomic_invariant!({

  latomic_fn(args...);

})

For this to be sound, though, we need to put all the conditions in the right places. That should amount to the following:

// PRIVATE PRECONDITION is required here
open_atomic_invariant!({

  /* user ghost code here */

  // ATOMIC PRECONDITION is required here
  latomic_fn(args...);
  // ATOMIC POSTCONDITION is assumed here
  
  /* user ghost code here */
  
})
// PRIVATE POSTCONDITION is assumed here

Verus notation for declaring a logically atomic function

In order for Verus to generate these VCs automatically, we need Verus to have a dedicated notation for logically atomic specs.

fn latomic_fn(args...)
    private_requires ...
    private_ensures ...
    atomic_requires ...
    atomic_ensures ...

In Iris, all private and atomic pre/postconditions are of course Iris propositions, thus allowing resources. Likewise in Verus, we need tracked inputs/outputs both for private and atomic conditions. This would be easiest to implement with better notation for tracked inputs and outputs like in this discussion.

We also need to include mask information.

Maybe something like this:

fn latomic_fn(args...)
    atomic[masks...] {
        with (tracked args ...)
        requires ...
        ensures ...
    }
    /* private precondition, postcondition */
    requires ...
    ensures ...

Examples

As an example, we can write AtomicU64 operations as logically atomic specs:

impl AtomicU64 {
    fn fetch_add(&self, v: u64)
        atomic {
            (tracked p: &mut PointsTo)
            requires
                old(p).id() == self.id(),
            ensures
                p.id() == old(p).id()
                p.value() == wrapping_add(old(p).value, v), 
        }   
        returns old(p).value();

(This operation is, of course, physically atomic, but in the long run I'd prefer to unify the notions, replacing our current #[atomic] attribute with logically atomic specs).

Example usage:

    fn example_code(&self, inv: &AtomicInvariant<PointsTo>) {
        open_atomic_invariant!(inv => points_to => {
            self.fetch_add(20)
              with (&mut points_to);
        }); 
        open_atomic_invariant!(inv => points_to => {
            self.fetch_add(30)
              with (&mut points_to);
        }); 
    } 

The with syntax is still fictional; here it's being used to transfer the tracked state that is part of the atomic precondition.

Now, what if we want to verify a function with a logically atomic spec? We need an operation that can "open" the atomic update, which would behave similarly to open_atomic_invariant!:

    fn fetch_add_plus_1(&self, v: u64)
        atomic_spec {
            (tracked p: &mut PointsTo)
            requires
                old(p).id() == self.id(),
            ensures
                p.id() == old(p).id(),
                p.value() == wrapping_add(
                    old(p).value,
                    wrapping_add(v, 1))
        }   
        returns old(p).value();
    {   
        let w = wrapping_add(v, 1);

        open_atomic_update!(AU => points_to => {

            self.fetch_add(w)
                with (&mut points_to);

        });
    }

Misc notes

I used the open_atomic_invariant! notation above, since that's what's currently in Verus, but I'd actually like to change the notation:

let tracked points_to = open_invariant!(&inv);
// ...
close_invariant!();

This would be a step towards supporting functions that change the mask, which would be useful. Also, I think it looks better.

Integrating logical atomicity with VerusSync

more on this later

Things to do

• Finalize notation
• Formalize VC gen

[zeldovich]

In our experience with logatom in Perennial, the angle-brackets sugar notation is convenient, but in many cases we need to then manipulate the logatom fupds (callbacks) explicitly, such as putting them in invariants, passing them to other threads or functions, associating them with data structures like a work queue, etc. What would be the tracked object that represents a logatom closure?

[tjhance]

I expect we'd have such a tracked object, yeah. I didn't discuss it explicitly, but it's mentioned up above in the open_atomic_update! line, a variable called AU, which is introduced into the function body as a result of the atomic_spec. Ideally its properties would be as close as possible to a Verus-equivalent of the Iris atomic_update definition. That includes the ability to "peek" into the atomic update without actually invoking it (though I don't know much about the use cases for this ability)