Commit Points

A commit point is when state changes become permanent and irrevocable. Understanding commit points is essential for writing correct async code because they determine what survives a trap and what gets rolled back.

Tentative vs Permanent State

State changes in an actor method are tentative until a commit point occurs. If a trap happens before any commit point, all tentative changes are reverted:

commit-tentative.sr9

// State changes are tentative until a commit point
persistent actor {
  var balance : Int = 100;
  var pending : Int = 0;
  invariant balance >= 0;

  public func transfer(amount : Int) : async Bool
    modifies balance, pending
    entry_requires amount > 0 and amount <= balance;
    requires amount > 0;
    requires amount <= balance;
  {
    // These changes are tentative
    balance -= amount;
    pending += amount;

    // If we trap here, both changes are reverted
    trap balance < 0;

    // await is a COMMIT POINT - changes become permanent
    try { await confirmTransfer(); } catch (_) {};

    // After commit, balance change cannot be undone
    pending -= amount;
    true
  };

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

The key insight: before await confirmTransfer(), the changes to balance and pending can be undone if a trap occurs. After the await, the balance change is permanent.

Where Commit Points Occur

State changes become permanent at commit points:

1. await expression - Suspends execution and commits all prior changes
2. Suspending await* expression - Commits only when the async* computation may reach a real suspension
3. Implicit function exit - Returning a value at the end of a function
4. Explicit return - The return statement

commit-points-explicit.sr9

// The three types of commit points
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  // Commit point 1: await expression
  public func withAwait() : async Int modifies counter {
    counter += 1;        // Tentative
    try { await pause(); } catch (_) {};  // COMMIT - counter change is permanent
    counter += 1;        // Tentative again
    counter              // Commit point 2: function return
  };

  // Commit point 2: implicit function exit
  public func implicitReturn() : async Int modifies counter {
    counter += 10;
    counter  // Function exit commits all changes
  };

  // Commit point 3: explicit return
  public func explicitReturn(x : Int) : async Int
    modifies counter
    entry_requires x >= 0;
    requires x >= 0;
  {
    counter += x;
    if (x > 100) {
      return counter;  // COMMIT via explicit return
    };
    counter += 1;
    counter  // COMMIT via implicit return
  };

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

Each commit point locks in all state changes made since the previous commit point (or method entry).

Trap Behavior at Commit Points

The timing of a trap relative to commit points determines what state survives:

Trap Location	Effect
Before any commit point	All changes reverted
After commit point	Prior changes permanent, later changes reverted

commit-trap-after.sr9

// Trap AFTER commit point - prior changes are permanent
persistent actor {
  var committed : Int = 0;
  var uncommitted : Int = 0;
  invariant committed >= 0;

  public func partialCommit() : async ()
    modifies committed, uncommitted
    entry_requires uncommitted == 0;
    requires uncommitted == 0;
  {
    // Phase 1: before await
    committed := 100;

    // COMMIT POINT - committed := 100 is now permanent
    try { await checkpoint(); } catch (_) {};

    // Phase 2: after await
    uncommitted := 50;

    // If trap occurs here:
    // - committed stays at 100 (was committed at await)
    // - uncommitted reverts to 0 (never committed)
  };

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

If code after await checkpoint() traps:

• committed stays at 100 (committed at the await)
• uncommitted reverts to 0 (never reached a commit point)

Multiple Commit Points

Each ordinary await creates a separate commit point. An await* does so only if the computation it continues may actually suspend. Changes made between commit points form independent atomic units:

commit-multiple-awaits.sr9

// Multiple awaits create multiple commit points
persistent actor {
  var step1Done : Bool = false;
  var step2Done : Bool = false;
  var step3Done : Bool = false;

  public func multiStep() : async ()
    modifies step1Done, step2Done, step3Done
  {
    // Atomic block 1
    step1Done := true;

    try { await doStep1(); } catch (_) {};  // COMMIT 1: step1Done is permanent

    // Atomic block 2
    step2Done := true;

    try { await doStep2(); } catch (_) {};  // COMMIT 2: step2Done is permanent

    // Atomic block 3
    step3Done := true;
    // COMMIT 3: step3Done committed at function return
  };

  // If doStep2 call triggers a trap after returning:
  // - step1Done remains true (committed at await 1)
  // - step2Done remains true (committed at await 2)
  // - step3Done reverts to false (never committed)

  private func doStep1() : async () { };
  private func doStep2() : async () { };
}

If an error occurs after doStep2() returns but before the method completes:

• step1Done and step2Done remain true (committed at their respective awaits)
• step3Done reverts to false (never committed)

Commit Points vs Atomicity Boundaries

Commit points and atomicity boundaries occur at suspending boundaries, but they are distinct concepts:

Concept	What It Means
Atomicity boundary	Other actors can interleave here
Commit point	State changes become permanent here

For ordinary await, both happen at the await. For await*, both happen only when the continued computation may reach a real await; if the computation cannot suspend, it stays in the current atomic slice. Atomicity is about interleaving, while commit points are about permanence.

commit-vs-atomicity.sr9

// Commit points vs atomicity boundaries
persistent actor {
  var balance : Int = 1000;
  var log : Int = 0;
  invariant balance >= 0;

  public func withdraw(amount : Int) : async Bool
    modifies balance, log
    entry_requires amount > 0;
    requires amount > 0;
  {
    // --- Atomic block 1 ---
    // All these changes are atomic (no interleaving)
    // but still TENTATIVE (not yet committed)
    if (balance < amount) {
      return false;  // COMMIT via return
    };
    balance -= amount;
    log += 1;

    // --- COMMIT POINT (await) ---
    // balance and log changes become PERMANENT
    // AND this is an ATOMICITY BOUNDARY
    try { await notifyWithdrawal(amount); } catch (_) {};

    // --- Atomic block 2 ---
    // New atomic block, new tentative changes
    log += 1;
    true  // COMMIT via return
  };

  private func notifyWithdrawal(_ : Int) : async () { };
}

Verification Implications

The verifier models suspending commit points through the release-assume pattern. At each await, and at each await* whose callee may suspend:

Before the commit point:

• Prove the actor invariant holds
• All changes so far are assumed committed
• Release permissions on shared state

After the commit point:

• Assume the invariant holds (but exact values unknown)
• Regain permissions on shared state
• Prior field values cannot be referenced via old() (it captures method entry)

This means you cannot use old() to refer to pre-await state:

public func noPreAwaitOld() : async Int
  modifies x
{
  x := 100;
  try { await pause(); } catch (_) {};
  // old(x) is still the METHOD ENTRY value, not 100
  x
}

To capture pre-await values, use local variables:

public func withSnapshot() : async Int
  modifies x
{
  x := 100;
  let snapshot = x;  // Capture the committed value
  try { await pause(); } catch (_) {};
  // snapshot == 100, regardless of what happened during await
  snapshot
}

Why Commit Points Matter

Understanding commit points helps you:

1. Reason about partial failures - Know what state survives a trap
2. Design recovery logic - Place awaits strategically to commit important changes
3. Avoid inconsistencies - Ensure related changes commit together or not at all
4. Write correct postconditions - Know what the verifier assumes about committed state

Common Patterns

All-or-Nothing Pattern

Group related changes before an await to ensure they commit together:

public func atomicUpdate() : async ()
  modifies a, b, c
{
  // These all commit together at the await
  a := newA;
  b := newB;
  c := newC;
  try { await confirm(); } catch (_) {};
}

Staged Commit Pattern

Use multiple awaits to create checkpoints:

public func stagedProcess() : async ()
  modifies phase, data
{
  phase := #preparing;
  try { await prepareData(); } catch (_) {};  // Commit: phase is #preparing

  phase := #processing;
  data := processData();
  try { await checkpoint(); } catch (_) {};   // Commit: phase and data updated

  phase := #complete;
  // Final commit at return
}

Guard Before Commit Pattern

Validate before committing irreversible changes:

public func guardedCommit(amount : Int) : async Bool
  modifies balance
  entry_requires amount > 0;
  requires amount > 0;
{
  // Validate before any commit point
  if (balance < amount) {
    return false;  // No state changes committed
  };

  balance -= amount;
  try { await notifyWithdrawal(); } catch (_) {};  // Now the change is permanent
  true
}

Summary

• State changes are tentative until a commit point
• Commit points occur at await, suspending await*, return, and function exit
• Traps before a commit point revert all changes
• Traps after a commit point preserve prior committed changes
• old() captures method entry, not pre-await state
• Use local variables to snapshot pre-await values
• Group related changes before an await for atomic commits

See Also

• Atomicity Between Awaits - Interleaving and interference
• Await Expressions - Await syntax and semantics
• Trap Conditions - How traps work
• Invariants and Await - The release-assume pattern