Using Formal Methods on a Concurrency Bug

This is the second post about running formal models against real bugs in our tools. The first was a connection that kept failing [1]. This one is a race between two processes, and why passing a test many times was not enough to trust the fix.

Lux is our visual surface for agents, a window an agent draws into. Only one display process should own a given screen slot. When two agents started at the same moment, both could claim the same slot, and the extra windows leaked. We fixed it, and a new order of events brought it back. This happened sixteen times. Each fix closed one order and exposed another.

A test runs the two processes and checks the result, in whichever order the operating system picks that time. It runs a hundred times, passes a hundred times, and the one order that breaks can still be waiting. A green test here is confidence, not proof. After sixteen rounds we stopped sampling the orders and described them instead.

The states

We wrote the two processes and the socket they compete for in Z, a specification notation built on set theory and logic [2]. A Z specification names the states a system can be in and the rules those states must obey; the first post introduces it in more depth [1]. A display claims its slot by creating a Unix socket, a named endpoint in the file system, at a known path. The socket moves through four states.

SOCKSTATUS ::= sabsent | sbound | slistening | sstale

sabsent is no file. slistening is a live display accepting connections. sstale is a leftover file whose owner is gone. sbound is the one that caused the bug. The socket has been created and bound to the path, but the owner has not yet started accepting connections. For a brief moment the file exists and answers nothing, and another process that checks it reads it as dead.

Two rules must hold no matter what order the two processes run in.

# { a : AGENT | phase a = serving } ≤ 1
# { a : AGENT | phase a ∈ { bound, listening, serving } } ≤ 1

# is the number of. The first rule says at most one process is serving a slot. The second says at most one process is ever past the point of claiming it, so there is never a second winner, not even for a moment.

We kept these two rules out of the description of the state, on purpose. A rule written into the description is one the checker assumes and will not test. Left outside, a state that breaks it stays reachable, which is exactly what we want the checker to find.

PID files lie

The bug came from how a process decided whether an existing socket was alive. The old code read a process-id file next to the socket and asked the operating system whether that process still existed.

def is_running(self) -> bool:
    if not self.pid_path.exists():
        return False                 # no pid file, assume dead
    pid = int(self.pid_path.read_text())
    try:
        os.kill(pid, 0)              # signal 0 checks the pid exists; kills nothing
    except ProcessLookupError:
        return False                 # no process has that id
    except PermissionError:
        return True                  # a process has that id, owned by someone else
    return True                      # a process has that id

A process id only proves a process with that number exists. It does not prove the process is serving. One that has crashed without being reaped, or is still starting, or is hung, keeps its id and passes this check while answering nothing. A reused id is worse: it names a different process entirely. And a missing file can belong to a process that is still alive. The model forced a single source of truth. A socket’s owner is decided by connecting to the socket, not by reading a file beside it. In the words of our design note, PID files lie; sockets don’t.

Here is the new check. It connects to the socket and reads the reply. It never looks at a process id.

def _probe(self) -> SocketLiveness:
    if not self._socket_path.is_socket():
        return SocketLiveness.DEAD            # absent, or not a socket
    with socket.socket(socket.AF_UNIX, socket.SOCK_STREAM) as probe:
        try:
            probe.connect(str(self._socket_path))
        except (ConnectionRefusedError, FileNotFoundError):
            return SocketLiveness.DEAD         # no listener, or file gone
        except OSError:
            return SocketLiveness.ACCEPTING    # timeout or ambiguous, not dead
        reply = recv_message(probe, timeout=_HANDSHAKE_TIMEOUT)
        if isinstance(reply, ReadyMessage):
            return SocketLiveness.READY
    return SocketLiveness.ACCEPTING

The three results line up with the socket states in the model. DEAD is sabsent or sstale. ACCEPTING covers the sbound window, where a live owner exists but has not finished the handshake, so it is never read as dead. READY is slistening. The model and the code are two views of the same states.

The check

z-spec test runs ProB, the checker from the first post [3]. For a rule like “at most one process is serving,” we ask ProB the opposite question: is there any reachable state in which two processes are serving?

probcli display_lifecycle.tex -model_check \
  -goal "card({a | a : AGENT & phase(a) = serving}) > 1"
→ goal NOT found

goal NOT found means no reachable state has two servers. The rule holds across every order the processes can take.

To confirm the model was strict enough to catch the real bug, we removed the guard that stops one process from deleting another’s socket during the bind window, and ran the check again.

→ goal FOUND

ProB returned the order that breaks the rule. One process binds its socket. A second process checks it during the sbound window, reads it as dead, deletes it, and binds its own. Two winners. That order is the bug that cost us sixteen rounds. We put the guard back, and the goal is not found again.

The rule we changed

The fix in the code was a set of guards and a switch to socket-based liveness. The change in how we work was larger. For anything touching this kind of concurrency, the model check, not a passing test, is now the gate a change clears before it merges. We made it a standing rule: the second time a defect of the same kind returns, we stop patching and write the model.

What it cost, and what we do not yet know

The model took an afternoon, because the agent drafts the notation and we correct it. The limits are the same as the first post. This is one small tool from a small team. We check the model for one or two processes, not for arbitrary numbers of them. We run the check by hand and commit the result; it is not yet an automatic step in our build. The model did not replace our tests or our reviews. It caught the class of bug that sampling missed. We do not know how far this holds at larger scale. We are still finding out.

The specification is public: Lux’s display model is display_lifecycle.pdf.

References

1. Punt Labs. “Using Formal Methods on a Recurring Connection Bug.” 2026. punt-labs.com
2. ISO. “ISO/IEC 13568: Z Formal Specification Notation.” 2002. iso.org
3. Leuschel, M. and Butler, M. “ProB: The Animator and Model Checker.” 2003. prob.hhu.de