Lease & Concurrency

GAR MUST implement exclusive session lease.

Requirements

1. Only one executor may hold an active lease per session.

2. Lease MUST include a monotonic fencing token.

3. Checkpoint writes MUST use compare-and-swap on fencing token.

4. Stale fencing tokens MUST be rejected.

5. Lease loss MUST halt execution immediately.

6. Lease expiration MUST allow safe takeover.

This prevents:

• Double execution

• State corruption

• Distributed race conditions