Lock with a lease

Several nodes share a lock with a lease. A node takes the lock, then writes to shared storage. If the node pauses (a long GC pause, a slow disk) between the two, the lease runs out and another node takes the lock and writes. The first node wakes up and writes too, and the storage now holds older data on top of newer data. The storage takes every write from a node that thinks it holds the lock:

src/lock.ts

export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

See how pnueli finds and fixes it.