Atomicity Between Awaits

Code between suspending await points executes atomically, with no interleaving from other actors. This guarantee is fundamental to reasoning about concurrent state in Sector9.

What is Atomicity?

An atomic block is a sequence of statements that executes without interruption. Between any two suspending boundaries (or from method entry to the first suspending boundary, or from the last one to method exit), all code runs as a single indivisible unit.

atomicity-basic.sr9

// Basic atomicity: code between awaits runs without interruption
persistent actor {
  var counter : Int = 0;
  var flag : Bool = false;
  invariant counter >= 0;

  private func pause() : async () { };

  public func atomicBlock() : async ()
    modifies counter, flag
  {
    // This entire block runs atomically:
    counter := counter + 1;
    flag := true;
    assert counter > 0 and flag;  // Both changes visible together

    try { await pause(); } catch (_) {};  // <-- Atomicity boundary

    // New atomic block starts here:
    counter := counter + 1;
    flag := false;
    assert counter > 0 and not flag;
  };
}

Key properties of atomic blocks:

• No interleaving - Other actors cannot observe partial state changes
• All-or-revert before commit - If the block traps before the next commit point, its tentative state changes roll back
• Consistent snapshots - Assertions within a block see consistent state

Atomicity Boundaries

An ordinary await expression creates an atomicity boundary - the point where one atomic block ends and another begins. An await* creates the same kind of boundary only when the continued async* computation may reach a real await. At this boundary:

1. The current atomic block commits
2. Execution suspends
3. Other actors may execute (including your own public methods)
4. Execution resumes in a new atomic block

atomicity-no-interleaving.sr9

// Demonstrating no interleaving within atomic blocks
persistent actor {
  var x : Int = 0;
  var y : Int = 0;
  invariant x >= 0 and y >= 0;

  private func bump() : async ()
    modifies x
    ensures x == old(x) + 1;
  {
    x += 1
  };

  public func transfer(amount : Int) : async ()
    modifies x, y
    entry_requires amount >= 0 and x >= amount;
    requires amount >= 0;
    requires x >= amount;
  {
    // Atomic block 1: Both updates happen together
    x := x - amount;
    y := y + amount;
    // No other code can see x decremented but y not yet incremented
    assert x + y == old(x) + old(y);  // Conservation holds

    try { await bump(); } catch (_) {};

    // Atomic block 2
    assert x >= 0;  // From invariant, not from block 1
  };
}

Within the first atomic block, x and y change together. No external observer can see x decremented but y not yet incremented.

The Interference Model

At each suspending await boundary, the verifier models conservative interference. It assumes:

What The Verifier Assumes	Why
All public methods may execute	Any actor could call you
Multiple times	Same method could run repeatedly
In any order	No message ordering guarantees
By any caller	No caller restrictions

This means shared state is "havoced" (made unknown) at suspending await boundaries:

atomicity-boundary-interference_unsat.sr9

// At await boundaries, other actors can interfere
persistent actor {
  var balance : Int = 100;

  private func pause() : async () { };

  public func withdraw(amount : Int) : async ()
    modifies balance
    entry_requires amount > 0;
    requires amount > 0;
  {
    let before = balance;

    try { await pause(); } catch (_) {};  // Interference point

    // ERROR: Cannot assume balance unchanged after await
    assert balance == before;
  };

  public func deposit(amount : Int) : async ()
    modifies balance
    entry_requires amount > 0;
    requires amount > 0;
  {
    balance += amount;
  };
}

This fails verification because balance could have changed during the await. The deposit method is public and modifies balance, so the verifier assumes it might have been called.

Invariants Protect Across Boundaries

Actor invariants bridge atomicity boundaries. The verifier uses a release-assume pattern:

1. Before await: Prove the invariant holds
2. During await: State may change, but all methods preserve the invariant
3. After await: Assume the invariant holds

atomicity-invariant-protects.sr9

// Invariants protect properties across await boundaries
persistent actor {
  var balance : Int = 100;
  invariant balance >= 0;

  private func externalCall() : async () { };

  public func safeWithdraw(amount : Int) : async Bool
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    try { await externalCall(); } catch (_) {};  // Interference point

    // Invariant guarantees balance >= 0 after await
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };

  public func deposit(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    balance += amount;
  };
}

The invariant balance >= 0 is the only property guaranteed after the await. The exact value of balance is unknown, but we know it is non-negative.

Local State Remains Stable

Not all state is invalidated at await boundaries. Fresh local allocations that do not escape to actor fields remain stable:

atomicity-local-stable.sr9

// Fresh local state remains stable across await
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  private func bump() : async ()
    modifies counter
    ensures counter == old(counter) + 1;
  {
    counter += 1
  };

  public func withLocalState() : async Int
    modifies counter
  {
    // Fresh local allocation - not reachable by other actors
    let localData : [var Int] = [var 10, 20, 30];
    let snapshot = counter;  // Primitive value captured locally

    try { await bump(); } catch (_) {};

    // Local state is stable - no interference possible
    assert localData[0] == 10;
    assert localData[1] == 20;

    // snapshot holds pre-await value
    snapshot
  };
}

The verifier uses escape analysis to distinguish:

State Category	Across Await
Actor fields	Invalidated (havoced)
Aliases to actor state	Invalidated
Fresh local allocations	Preserved
Primitive locals	Preserved

A "fresh" allocation is one created in the current method that never escapes to actor fields or is passed to external calls.

Reentrancy

Reentrancy occurs when code you call (directly or indirectly) calls back to your actor. At an await boundary, your actor's public methods are callable:

atomicity-reentrancy.sr9

// Reentrancy is modeled conservatively
persistent actor {
  var locked : Bool = false;
  var value : Int = 0;
  invariant value >= 0;

  private func externalCall() : async () { };

  public func criticalSection() : async ()
    modifies locked, value
    entry_requires not locked;
    requires not locked;  // Prevent reentrancy at contract level
  {
    locked := true;

    try { await externalCall(); } catch (_) {};  // Could trigger reentrancy

    // The requires clause prevents re-entry while locked
    // Invariant guarantees value >= 0 survives any interference
    value += 1;
    locked := false;
  };
}

The verifier models reentrancy conservatively: at any await, any public method could be invoked. Use a runtime entry_requires guard paired with a logical requires clause to prevent unwanted reentrancy at the contract level.

What Atomicity Does NOT Guarantee

No Ordering Between Awaits

Multiple awaits do not establish ordering with other actors:

public func sequential() : async () modifies x {
  try { await step1(); } catch (_) {};
  try { await step2(); } catch (_) {};  // Other calls may interleave between these
  try { await step3(); } catch (_) {};
}

Each await is an independent interference point. The verifier assumes arbitrary interleaving.

No Per-Await Snapshots

The old() expression refers to method entry, not pre-await state:

public func noPerAwaitOld() : async Int
  modifies x
  ensures result == old(x);  // old(x) is method entry value
{
  x += 1;
  try { await pause(); } catch (_) {};  // old(x) does NOT reset here
  old(x)  // Still the method entry value
}

To capture pre-await values, use local variables:

let preAwaitValue = x;
try { await pause(); } catch (_) {};
// Use preAwaitValue, not old(x)

No Frame Guarantees Without Invariants

In synchronous code, fields not in modifies are unchanged. In async code with await, this weakens:

Weak Frame

persistent actor {
  var a : Int = 0;
  var b : Int = 0;  // Not in modifies

  public func updateA() : async ()
    modifies a
    ensures b == old(b);  // May fail!
  {
    try { await pause(); } catch (_) {};
    a += 1;
  };
}

Strong with Invariant

persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  invariant b == 0;  // Pins b across await

  public func updateA() : async ()
    modifies a
    ensures b == old(b);  // Now succeeds
  {
    try { await pause(); } catch (_) {};
    a += 1;
  };
}

Add invariants for frame guarantees you need across await boundaries.

Verification at Await Points

The verifier performs checks at each await:

Before await:

• Prove actor invariant holds
• Prove callee preconditions
• Release permissions on shared state

After await:

• Assume actor invariant holds
• Assume callee postconditions
• Regain permissions on shared state
• Shared state values are unknown (except invariant properties)

This is the "exhale-inhale" pattern in the underlying Viper encoding.

Common Patterns

Snapshot Pattern

Capture values you need before await:

public func withSnapshot() : async Int modifies counter {
  let snapshot = counter;  // Capture before await
  try { await externalCall(); } catch (_) {};
  // snapshot still valid, counter unknown
  snapshot
}

Check-After-Await Pattern

Re-check conditions after await instead of assuming them:

public func safeOperation(amount : Int) : async Bool
  modifies balance
{
  try { await checkPermissions(); } catch (_) {};

  // Re-check condition after await
  if (balance >= amount) {
    balance -= amount;
    true
  } else {
    false
  }
}

Lock Pattern

Use a flag to prevent reentrancy:

persistent actor {
  var locked : Bool = false;

  public func critical() : async ()
    modifies locked
    entry_requires not locked;  // Blocks reentrant calls at the runtime boundary
    requires not locked;
  {
    locked := true;
    try { await riskyCall(); } catch (_) {};
    locked := false;
  };
}

Summary

• Code between suspending await boundaries runs atomically with no interleaving
• Each ordinary await is an atomicity boundary where interference can occur
• A non-suspending await* stays inside the current atomic block
• The verifier assumes all public methods may execute at each suspending boundary
• Invariants specify what properties survive interference
• Fresh local state is preserved; shared state is invalidated
• old() refers to method entry, not pre-await state
• Use snapshots to preserve values across await
• Use preconditions to prevent unwanted reentrancy

See Also

• Await Expressions - Await syntax and semantics
• Invariants and Await - The release-assume model
• Interference Model - What can change at await
• Local vs Shared State - Escape analysis details
• Frame Conditions Across Await - Framing in async code