Formally verified distributed locks for sandboxes

📝 摘要 #

本文作者在 Modal 实习期间设计并实现了 sandbox names——一种为沙箱提供互斥访问的分布式锁原语。文章从分布式系统的基本权衡（CAP/PACELC）出发，逐步推导出基于租约（lease）的分布式锁方案，并用 TLA+ 形式化验证其安全性（MutualExclusion）和活性（Liveness/EventualMutualExclusion）。随后探讨了一种可抢占锁（preemptible lock）的扩展设计，可将心跳开销从 O(sandboxes) 降至 O(workers)，但涉及 2-Phase Commit、Worker 信息存储、Kill-Switch 同步等复杂竞态条件处理。

核心概念： 分布式锁在沙箱场景下需要同时保证互斥安全和死锁恢复，TLA+ 形式化验证是发现隐含竞态条件和验证设计正确性的有效手段。

关键技术栈 / 关键要点：

1. 分布式租约（Distributed Lease） — 沙箱通过心跳续约持有锁，心跳失败则 kill-switch 在锁过期前终止沙箱，避免互斥违反
2. Fencing Token — Kleppmann 提出的经典方案：单调递增计数器防止过期锁持有者写入，但 Modal 因无法控制资源端而未采用
3. 放宽时钟假设 — 使用单调时钟 + 高优先级 supervisor + CPU pinning 放松"时钟不可靠"假设，使基于时间的方案在实践中可行
4. TLA+ 形式化验证 — 用 PlusCal 建模 5 个并发进程（创建/运行/心跳/清理/过期），参数化 UnreliableTiming 和 UnreliableNetworks，模型检查器发现需要 mutex violation recovery 和 lock timeout > scheduling latency
5. 可抢占锁扩展 — 利用 Worker 级别的失败检测器将心跳从 O(sandboxes) 降至 O(workers)，但引入创建-抢占竞态、调度-心跳竞态等复杂问题
6. 2-Phase Commit + Kill-Switch 同步 — 锁增加 acquiring 中间态防止创建期间被抢占；kill-switch 与命名沙箱创建必须同步，防止 kill-switch 触发后立即调度新沙箱导致互斥违反

关键结论 / 实践建议： 分布式系统没有万能方案，关键是用形式化方法将假设和交互显式化。可抢占锁虽在理论上更高效，但复杂性可能不值得——Modal 最终选择了简单可靠的租约方案。 Home

I’m wrapping up my internship at Modal, where I worked on our new, massively scalable sandbox architecture. The better part of it was spent building names, a distributed locking primitive for sandboxes. Acquiring a name is the same as acquiring a lock, except sandboxes keep their name until they terminate.

It turns out that distributed systems are hard to get right. Depending on assumptions, some results might even be provably impossible. I had to re-design names more than once: I’d overlook a race, requirements would change, or a decision would cause surprising interactions downstream. Being fed up, I learned TLA+, a modelling language built on top of temporal logic, to formally verify the system’s properties.

This post goes into the design and process behind sandbox names. It’s also my first blog post! My hope is that this will be an informative and fun read - if not, I take that personally, so please give me feedback.

What is a sandbox? #

Although I’ve been thinking about sandboxes for a while, you deserve some context. Let’s take a step back: what is a sandbox?

In short, it’s a secure environment where you can run untrusted programs. Sandboxes are abundant today for running agent-generated code to protect your machine from malicious behaviour (à la rm -rf /) - such as for RL rollouts. A single training run might spin up 100s of thousands of sandboxes in parallel, so we need to handle a lot of load.

Now, there’s no free lunch in distributed systems. To architect for reliability and scale, Modal trades consistency for availability. We’re able to continue scheduling new sandboxes even in the face of data store failures, at the cost of accepting eventual consistency. For those familiar, this implies that Modal sandboxes occupy the AP corner of CAP (actually, we’re PA/EL; eventual consistency also keeps scheduling latencies low, though this is better explained in the blog post from earlier).

AP works great for most use cases, but users may want stronger guarantees. When mutual exclusion is involved, for example, eventual consistency just doesn’t cut it.

Mutual exclusion #

Sometimes a sandbox needs exclusive access to a resource. An agent might book flights on your behalf, or an RL episode might interact with a stateful game server. Multiple sandboxes making non-idempotent requests would interfere with each other.

This is better explained with an example. Suppose I have a long-running coding agent working inside a sandbox. I need it to access stateful resources (like a database or repository). If multiple instances of this sandbox spun up, they could end up overwriting each other.

The simple answer here is to just create one sandbox for the agent. However, if the sandbox ever abruptly terminates, I expect it to be re-created - the agent shouldn’t halt. This is more common than it sounds. A process could crash, the network could partition, or the AWS instance could be preempted. Naively recreating the sandbox whenever we hit an error could easily lead to double-creates.

Well, sounds like this agent needs a mutex.

Is distributed locking hard? #

Sandbox names act as a mutex, though sandboxes can only hold one name, and hold it until they terminate. Mutexes are also simple: atomic acquires, atomic releases. Any transactional database supports that. Why is this blog post so long?

Consider the situation where a sandbox acquires the mutex, then promptly crashes without releasing the lock.

Figure 1: A deadlock blocks all future acquires

This is a deadlock! Usually the kernel steps in, detects the process crash, and preempts the lock. But sandboxes are distributed actors, forced to communicate over unreliable networks. How do you tell whether the sandbox crashed or if there’s just a packet delay? You can’t, which makes resolving this deadlock hard.

That being said, distributed locks are more or less a solved problem. There’s a classic blog post by Martin Kleppmann that goes over the standard solution. Let’s work up to this solution, investigate its properties, then break the rules in the name of performance. More on that later.

Distributed leasing #

How we resolve deadlocks is by implementing a distributed lease. After initially acquiring the lock, sandboxes must continually refresh it, or else it expires. We call this intermittent ping sent by the sandbox a heartbeat.

Figure 2: The lease expires after Sandbox 1 fails to refresh

But networks are still unreliable. What if a sandbox continually fails to heartbeat? The lease might expire, allowing another sandbox to acquire it. To prevent a mutual exclusion (mutex) violation, the sandbox should self-terminate after failing to heartbeat for some time, before the lock is due to expire.

Figure 3: Sandbox 1 self-terminates before the lease expires

Is this enough? In his blog, Kleppmann argues no. We can’t rely on time-based methods (like self-termination) because of unreliable clocks and process pauses. It’s true that clock issues can be minimized, but unlucky garbage collection or scheduling starvation might cause a process to pause for an unbounded amount of time. In that case, we could see a mutex violation.

Figure 4: Mutex violations can still occur due to unlucky timing

Thus the final part of a distributed lease is a fencing token. The lock maintains a monotonic counter that increments after each acquire. When a sandbox acquires the lock, it receives the counter’s value and passes it to the resource as a token. The resource should check to make sure the token is greater or equal to the last seen value, otherwise it rejects the write.

Figure 5: The resource rejects token 1 because it has already seen token 2

Problems with fencing #

Fencing tokens enforce a total order on the writes to a resource and are required for true correctness. But fencing is not always practical: we often don’t have control over the resources used by sandboxes, and Modal doesn’t have a Resource primitive. This is interesting future work, but for now, are fencing tokens even necessary?

We saw earlier that time-based approaches don’t work because they can’t guarantee safety. For our system, let’s use a time-based approach!

I promise this isn’t as silly as it sounds. Recall the original assumptions: clocks cannot be trusted, processes can pause indefinitely. Can we relax these? A monotonic clock won’t jump back, and is unlikely to skew that much. Additionally, our supervisor process (which heartbeats on behalf of sandboxes) definitely does not have a GC. Give it high scheduling priority and CPU pin other processes to shield it, and it’s unlikely to pause for that long.

Network partitions can always happen, but we use our earlier strategy for dealing with them: if heartbeats keep failing, the supervisor initiates a kill-switch that terminates the sandbox before the lock expires.

Figure 6: The supervisor heartbeats on behalf of sandboxes, initiating the kill-switch if refreshes fail

Given these relaxed assumptions, the lock should work. But the actual system is a bit more complex than the above diagram. What if there’s a race we’re not thinking of?

Formal properties #

Designing correct concurrent systems is hard; the number of behaviours typically grows super-exponentially with size. For sandbox names, there were times where I finally finished the design only to catch a race in it afterwards. This is especially true for the preemptible lock I discuss later, though even the simple lease has complications. We’ll see why once we try formalizing it.

TLA+ is a logic-based specification language. It was created by Lamport (perhaps better known for Paxos) in the 90s, but emerges from an older research effort to develop practical frameworks for program verification. TLA is based on modal logic (unrelated to Modal), an extension of first-order logic that introduces two new operators: $\Box$ and $\Diamond$. Different modal logics have differing semantics for these; in TLA, they mean always and eventually, respectively. With the two, we can express both safety properties (the system is always safe) and liveness properties (the system eventually makes progress).

Using TLA+ involves writing a spec that defines three things: state, properties, and behaviour. I wrote parts of my spec with PlusCal, a language that compiles down to TLA+ but resembles regular code, to make things easier. You’ll see both in the snippets below. Once the spec is written, a model checker like TLC can be ran to automatically verify whether the properties hold.

Note that many details are omitted to get at the bigger picture. If this confuses you, ask Claude to fill in the blanks (or view it on my Github).

State #

The state of our distributed lease can be defined using PlusCal variables. For example, we need to know the lock’s owner (Lock), whether the lease has been refreshed before the expiry TTL (Refreshed), each sandbox’s state (Proc), whether each sandbox is in its critical section (Critical), and whether a heartbeat hit a network partition (HeartbeatNetworkFailure).

variables
    Lock = "NONE",
    Refreshed = FALSE,
    Proc = [s \in Sandboxes |-> "INIT"],
    Critical = [s \in Sandboxes |-> FALSE],
    HeartbeatNetworkFailure = [s \in Sandboxes |-> FALSE],
    ...

It is also useful to parameterize our assumptions. Is communication reliable? Can clocks be trusted? Running the model checker reveals which properties hold under which assumptions.

CONSTANT UnreliableTiming, UnreliableNetworks

Properties #

The defining safety property of a lock is mutual exclusion. If a sandbox is in its critical section, then it holds the lock. Or, expressed in TLA:

MutualExclusion ==
    \A s \in Sandboxes: Critical[s] => Lock = s

Are we missing something? You might notice that this should always hold. That is, we really should have: $$ \forall s\in S:\Box(\text{Critical}(s)\to \text{Lock}=s) $$ Instead, what we’re doing here is an optimization: tell the model checker that MutualExclusion is an invariant, and it will be checked more efficiently than generic temporal formulas.

The defining liveness property of a lock is deadlock-freedom. One formulation could be that all sandboxes eventually acquire the lock. However, this assumes all sandboxes eventually terminate (they can’t stay critical forever). While technically true, a sandbox’s lifetime can be long enough that our model should treat it as unbounded. So, here’s an alternative statement:

Liveness ==
    \A s \in Sandboxes: (~Critical[s] /\ Lock = s) ~> Critical[s] \/ Lock # s

Whenever a sandbox incorrectly holds the lock (is not in its critical section), it will eventually enter the critical section or release the lock. You might notice a lot of funky syntax above: ~ is negation, /\ is logical conjunction, # is “does not equal”, and ~> is leads to, syntactic sugar for “always if A then eventually B”. Altogether, we have: $$ \forall s\in S: \Box\big[(\lnot\text{Critical}(s)\land \text{Lock}=s)\to\Diamond (\text{Lock}\ne s)\big] $$

Last, recall that our approach is time-based. If we have UnreliableTiming, then we can’t guarantee mutual exclusion! In this case, we want the system to recover in a bounded amount of time. We can formalize this property as:

EventualMutualExclusion ==
    \A s \in Sandboxes: (Critical[s] /\ Lock # s) ~> ```

Whenever there’s a mutex violation, the offending sandbox eventually self-terminates (leaves the critical section permanently). Removing sugar, the statement becomes:
$$
\forall s\in S:\Box\big[(\text{Critical}(s)\land\text{Lock}\ne s)\to\Diamond\Box(\lnot\text{Critical}(s))\big]
$$

Remember how above I didn’t want to assume that all sandboxes terminate? If so, we’d get `EventualMutualExclusion` for free without any recovery mechanism. When modelling systems, one generally aims to make the least amount of assumptions possible.

### Behaviour

The final and most complex piece of the spec is its behaviour. PlusCal represents behaviour via *processes* that modify state: each process contains *labels* defining which actions happen atomically, and in what order. In other words, a label corresponds to an atomic step taken by the model, and labels across processes can be interleaved in any order.

What processes go into our lease? Top of mind is the sandbox itself, but there’s actually 2 parts to this: the creation flow (when a sandbox is first scheduled and acquires the lock) and the running sandbox process. We’ll model this as 2 separate processes.

Another thing is the worker heartbeat. We saw previously there’s a supervisor process that heartbeats on behalf of sandboxes. In Modal parlance, this per-machine supervisor is the *worker* process (the underlying machine is the worker). The heartbeat itself is conceptually 2 different things too: a lease refresh and a timeout-driven kill-switch, which we’ll also represent as 2 processes.

To close out, we have the lock expiry itself, which we also model as a process. That brings us to 5 processes:

fair process (sandboxcreation \in SandboxProcess("SandboxCreation")) { Create: either { (* Schedule a named sandbox atomically ) } or { ( Set name on an existing unnamed sandbox *) }; }

process (sandbox \in SandboxProcess("SandboxRunning")) { CriticalSection: (* The `await` keyword means this label is blocked from running until the condition evaluates to true ) await Critical[SandboxId(self)]; Release: ( Become non-critical and release lock atomically ) Terminate: ( Set state to terminated *) }

fair process (workerheartbeat \in SandboxProcess("WorkerHeartbeat")) { Heartbeat: while (TRUE) { await Critical[SandboxId(self)]; (* Attempt to refresh lease *) } }

fair process (workersweep = Process("WorkerSweep")) { Sweep: while (TRUE) { (* Kill sandboxes that fail to refresh lease *) } }

fair process (lockproc = Process("LockExpiry")) { Expire: while (TRUE) { (* Expire the lease if not refreshed *) } }

You might notice that all processes are labeled as `fair` except the `SandboxRunning` process. In PlusCal, this is called weak fairness: a weakly fair process must eventually get the chance to run, provided it isn’t deadlocked. In my spec, anything that happens in a bounded time interval must be weakly fair. Since sandbox termination isn’t guaranteed, the `SandboxRunning` process is not fair.

### Time dependencies

Running the model checker, we see that `MutualExclusion` is easily violated. We haven’t modelled any temporal dependencies yet! Heartbeats should occur before the kill-switch timeout, and the kill-switch should occur before lock expiry.

A common way of simulating time is to have a counter that represents discrete timesteps. That can get complex, so I instead modelled only the dependencies themselves: if event A happens before event B, we `await` on the occurrence of A in B. This looks like storing whether an event has occurred:

variables ... LastHeartbeat = [s \in Sandboxes |-> FALSE], LastSweep = [s \in Sandboxes |-> FALSE];

Then defining a temporal dependency:

(* The / represents logical disjunction *) HeartbeatBeforeSweep == / \A s \in Sandboxes: Critical[s] => LastHeartbeat[s] / UnreliableTiming

By taking the disjunction with `UnreliableTiming`, we can parameterize whether these timing relations actually hold.

One timing relation in particular is worth noting. In the creation flow, we acquire the name before scheduling the sandbox. Hence the lock TTL should be greater than the max scheduling time, or it could expire under our feet. That can actually bite us! The scheduler, being eventually consistent, may schedule onto full workers; in that case it retries with exponential backoff under a rather long deadline. TLA helps ensure we explicitly model this relation:

AcquiringCompleteBeforeLockExpiry == / \A s \in Sandboxes: ~Acquiring[s] / UnreliableTiming

### Unreliable networks

Recall we also have `UnreliableNetworks` as a parameter. If this knob is true, network calls should be allowed to fail, such as when heartbeating:

fair process (workerheartbeat \in SandboxProcess("WorkerHeartbeat")) { Heartbeat: ... LastHeartbeat[SandboxId(self)] := TRUE; either { HeartbeatNetworkFailure[SandboxId(self)] := FALSE; (* Attempt to refresh lease ) } or { await UnreliableNetworks; HeartbeatNetworkFailure[SandboxId(self)] := TRUE; ( Don't do anything *) }; ... }

### Mutex violations

If we have `UnreliableTiming`, then we can no longer guarantee `MutualExclusion`. We need some sort of recovery mechanism such that we still ensure `EventualMutualExclusion`.

To achieve this, a sandbox terminates if it realizes the lease is owned by another sandbox. This can happen every heartbeat:

fair process (workerheartbeat \in SandboxProcess("WorkerHeartbeat")) { Heartbeat: ... if (Lock = SandboxId(self)) { Refreshed := TRUE; } else { Critical[SandboxId(self)] := FALSE; Proc[SandboxId(self)] := "TERMINATED"; } ... }

Now running the model checker with `UnreliableTiming` shows `MutualExclusion` to be violated, but `EventualMutualExclusion` to hold.

## Scaling up

Great - we have a lease that is verifiably correct, given some assumptions. Although the design is simple, verifying still helped us discover that we need a mutex violation recovery mechanism, and that the lock timeout should exceed scheduling latency.

However, consider what happens as we scale the number of named sandboxes. Every sandbox makes a transactional write when refreshing, causing high steady-state load that could exceed what a single database node can handle. Typically, we’d shard the lock table and key by name. But that could be more cost than we actually need!

Let’s do a thought experiment: rather than expiring the lock, what if we made the lock preemptible if the owner has terminated? Then we might do away with heartbeats. In distributed systems, this is called a [failure detector](https://en.wikipedia.org/wiki/Failure_detector). Unfortunately for us, perfect ones don’t exist. Failure detectors must choose between completeness (all sandbox failures are reported) or accuracy (we never report false failure). For us, deadlocks are never acceptable, so any failure detector must be complete at the risk of inaccuracy - same as our lease.

Not all hope is lost: there’s one trick we can use by adopting a failure detector model. Instead of $O(\text{sandboxes})$ liveness updates, we can scale down to $O(\text{workers})$ liveness updates. If a worker is alive, we can simply ask it if the sandbox is running. Thus detecting sandbox failure reduces down to detecting worker failure!

![[8d7763ca94d6acc92d739220b4447a61_MD5.png]]

Figure 7: We only need one liveness update per worker rather than per sandbox

At this point, your race-condition alarms should be going off. What if the lock is preempted before we finished scheduling? What if we schedule onto a worker right before liveness expires? What if…?

## Preemptible locks

When first designing sandbox names, we actually started with the preemptible lock. This proved to be challenging: I kept running into races I hadn’t thought of, so it was hard to be convinced that it worked. TLA was meant to address this - which it did! The race addressed by the third pattern below, for example, was caught by our model checker.

But the process of formalizing the design was difficult and slow. And, certain design patterns - required for correctness - were controversial. For an initial implementation, this wasn’t worth it. A standard lease would suffice.

Still, I wanted the preemptible design to be an option should we ever need to scale. In this section, I cover three patterns for building out a functional preemptible lock. The TLA formalization is complex enough to no longer be informative, so I’ll omit it as an exercise for the reader (or again view it on my [Github](https://github.com/scott-22/tla-specs/blob/main/Preemptable.tla)).

### 2-Phase Commit

In our creation flow, we want lock acquisition and sandbox creation to behave atomically. Otherwise, we could acquire the lock, preempt it before scheduling the sandbox, then immediately cause a mutex violation.

The standard way to do this is [2-Phase Commit](https://en.wikipedia.org/wiki/Two-phase_commit_protocol). The lock has two “taken” states: an intermediate *acquiring* state, and a committed *acquired* state. In the acquiring state, the lock cannot be preempted. To prevent deadlocks (e.g, if a partition occurs right after acquisition and we fail to schedule the sandbox), an uncommitted lock will expire after some TTL.

![[a56ee31899e366dc232bfc7527d057b0_MD5.png]]

Figure 8: The lock represented as a state machine

A natural question to ask is what if the commit fails? To really make this work, the commit needs to happen via heartbeat. Once confirmed, the sandbox can stop heartbeating. Finally, if commits keep failing, then a kill-switch should activate before lock expiry.

### Storing worker information

Recall the preemption flow: if the failure detector reports that the worker is unresponsive, then the lock is preemptible. Otherwise, the worker is live and I ask it directly whether the lock owner is still running.

This requires knowing which worker a sandbox lives on, and storing that information in our lock table. We don’t know this information upfront - the control plane acquires the lock before scheduling the sandbox. Thus, worker information should be sent through the commit.

### Kill-switch synchronization

The kill-switch prevents mutex violations by terminating all sandboxes on a worker whose liveness is about to expire. What if we schedule a sandbox onto it right after?

To prevent yet another mutex violation, we should never create named sandboxes on a worker after its kill-switch initiates until it sends a successful heartbeat and refreshes its liveness.

![[5ca2dd0b361ea1c432e3a5137c6edd9d_MD5.png]]

Figure 9: Block named sandboxes after the kill-switch, until liveness is restored

This could be done in two ways: either the scheduler keeps track of this, or the worker does. It’s safer for the worker to do it - one can imagine a packet delay that holds a scheduling request just until the kill-switch triggers, for example.

However, there’s a worker analogue for the exact same situation! That is, the worker receives a request to create a new named sandbox, but the thread is preempted and resumes only after the kill-switch has already triggered. It follows that named sandbox creation and the kill-switch should be synchronized - have I mentioned this blog post is about locks?

## Conclusion

Distributed systems are about trade-offs. We choose between CP and AP, between liveness and safety, and between durability and latency.

Sometimes it’s ok to break rules if it makes the most sense for the system. However, sometimes we should just do the simplest thing. While the preemptible lock was a fun thought experiment, the added complexity may not be worth it. Today, sandbox names are built on a plain old lease.

Regardless of the choices we make, what we never want is unintended consequences. Assumptions and interactions should be explicit, and the best way to formalize that is mathematically.

Coming into this internship, I knew next to nothing about distributed systems. I’ve grown immensely over the past 4 months, and through trial by fire, had the chance to own systems end-to-end and bring them to life. Thanks for reading, and I hope you learned something!

Scott:)