Skip to main content

Computations (async* / await*)

async* creates a computation and await* continues through it. The important difference from ordinary async/await is that await* does not automatically split the current atomic slice. It passes control into the computation, and only a real suspension inside that computation creates an interleaving boundary.

When to Use async*​

Use async* when you want to factor async control flow into helpers without forcing an extra await boundary at every helper call.

Common cases:

  • Local helper computations that should behave like an inlined call when they do not suspend.
  • Update flows that call a sequence of helpers, where only the helper that reaches an ordinary await should split the atomic slice.
  • Composite queries, where calls to other query/composite-query functions use await*.

async* is not a consensus bypass. Whether execution goes through consensus is determined by the enclosing shared method and the calls it performs. In an update method, async* helper code still belongs to the update execution. If an async* computation reaches an ordinary await, that await is the commit and interference point.

Verification Semantics​

In verification, await* behaves like a commit point only if the callee may actually suspend. A callee may suspend if its body contains an ordinary await, or if it await*s another computation that may suspend.

If the callee cannot suspend, await* is treated like a local call:

  • actor-state facts are not havoced;
  • no interleaving is introduced;
  • the caller does not need a try/catch solely for that await*.

If the callee may suspend, await* is treated like a real await boundary:

  • actor invariants must hold before the boundary;
  • shared actor state may be invalidated by interference;
  • the success and failure paths must be explicit.

Additional restrictions:

  • Any await* that may suspend must be wrapped in try/catch with a catch-all (same as await).
  • Result-producing suspending uses should be wrapped as try { await* f() } catch (_) { fallback }, so both success and failure paths are explicit.
persistent actor {
  var flag : Int = 0;
  var counter : Int = 0;

  private func localStep() : async* Int
    modifies counter
  {
    counter += 1;
    counter
  };

  public func runLocal() : async Int
    reads flag
    modifies counter
  {
    let before = flag;
    let value = await* localStep(); // no suspension, no interference
    assert flag == before;
    value
  };
}
persistent actor {
  var flag : Int = 0;
  var counter : Int = 0;

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

  private func suspendingStep() : async* Int
    modifies counter
  {
    try { await pause() } catch (_) {};
    counter += 1;
    counter
  };

  public func runSuspending() : async Int
    reads flag
    modifies counter
  {
    let before = flag;
    let value = try { await* suspendingStep() } catch (_) { counter };
    // flag may have changed while suspendingStep awaited.
    value
  };
}