필사 모드: When Two Services That Passed the Type Checker Halt Waiting for Each Other — Choreography as a Different Approach

• Two Services Halt Waiting for Each Other
• The Root of the Problem Is That the Code Is Split in Two
• Choreography — Writing the Whole System as One Program
• What Endpoint Projection Does
• Why Deadlock Disappears by Design
• What Wyzer Puts on Top
• Getting In-Place Update Without a Borrow Checker
• Writing Down the Current State of This Language as It Is
• Wrap-Up and Sources

Two Services Halt Waiting for Each Other

You built two services in a memory-safe language. Both compile cleanly. No null references, no data races, no use after free.

But once deployed, sometimes the two of them halt together. The server is waiting for the second message the client was supposed to send, and the client is waiting because it knows the server will respond first. The protocol is out of step.

The characteristic of this bug is that neither side's code is at fault. Read them separately and both are reasonable. The fault is between the two, and no compiler looks at what is between them.

The Root of the Problem Is That the Code Is Split in Two

Think about how far the boundary a type system protects extends and the reason becomes clear. A type checker sees the flow of values within one compilation unit. The moment something leaves that unit — the moment the bytes go onto a socket — it guarantees nothing. What order the other side expects those bytes in is information the checker cannot know.

So we fill that gap with human discipline. We draw sequence diagrams in documents, share schemas, and write integration tests. All three are useful and all three are convention rather than checking. You can change the code on one side without changing the diagram and compilation still passes.

There is a line of work that gives a different answer at this point. Do not check what is between them — do not split them in two in the first place.

Choreography — Writing the Whole System as One Program

Choreographic programming writes the whole interaction as a single global description instead of writing a distributed system process by process. The flow of the client sending this, the server computing that and sending it back, and the client receiving it reads in order inside one program.

The name came from Fabrizio Montesi's 2013 doctoral thesis, and since then a number of languages and libraries have implemented the idea. The core of the concept is a change of viewpoint. The code we write today is written from the viewpoint of one node. Choreography is written from a viewpoint that looks down from outside the system. Thinking of it as a sequence diagram made executable is broadly right.

What Endpoint Projection Does

You cannot execute the global description directly, because what actually runs is a process on each node. So one procedure gets added to the compilation stage: endpoint projection.

Projection mechanically extracts per-node code from a single choreography. The client binary keeps only the sends, receives, and computations the client has to do, and likewise for the server binary. The two artifacts do not know about each other, but because they came from the same original, their ordering cannot go out of step.

What matters here is that a job we have always done by hand has become the compiler's job. Until now, matching client code and server code was a person reading a diagram and transcribing it onto both sides. Two acts of transcription turn into one automatic transformation.

Why Deadlock Disappears by Design

Let me flag a part that is easy to misread. Deadlock disappears not because the compiler is clever but because you cannot write such a program.

In the global description, communication is expressed as a single construct. One line saying that someone sends something to someone else gives birth to a send and a receive at the same time. There is no way to write down in source a situation where there is a send with no receive, or where both sides start by receiving. So no such pairing can appear in the projection result either.

This property has been known as deadlock-freedom by design since the 2013 work of Carbone and Montesi. But the scope needs to be understood precisely. This guarantee is about deadlocks that come from protocol mismatch. A node dying, the network being cut, falling into an infinite loop, or a lock being taken on an external resource are separate problems.

What Wyzer Puts on Top

The recently published Wyzer is an attempt to bring this idea over into systems programming. The README introduces the language as a statically typed, compiled, resource-oriented language, and states that it combines choreography with the Perceus memory model.

What stands out in the syntax is that nodes attach to types.

role @Client;
role @Server;

fn fetch_data(query: str@Client) -> str@Client {
    // the client hands query over to the server
    let server_query: str@Server = query;

    // the server processes it
    let server_result: str@Server = db_lookup(server_query);

    // the server returns the result to the client
    let client_result: str@Client = server_result;

    return client_result;
}

Here a network transfer is not a separate function call but an assignment into another node type. And this language treats that assignment as a linear move. That is, the value handed over is destroyed in its original place. The error message the README carries is the result: use it again after moving it and you get a compile error saying you used a moved variable.

What this design aims at is clear. One common bug in distributed systems is continuing to use data you have already sent as if the local copy were still current, and making transfer a move turns that mistake into a type error.

Getting In-Place Update Without a Borrow Checker

The memory choice is worth looking at too. Wyzer states that it takes Perceus rather than having either a garbage collector or a borrow checker.

Perceus is a technique presented at PLDI 2021 in which the compiler precisely inserts reference count increment and decrement instructions so that no garbage remains in programs without cycles. Add reuse analysis on top and, when a value has only one reference, you can rewrite the existing memory in place instead of allocating anew. This way of having code written in a functional style compile to in-place update is called FBIP. It is implemented in the Koka language.

It is worth noting why this combination is natural. In a choreography, a value moving between nodes means ownership is being transferred, and counting ownership is already what reference counting does. The README's design principle of using the same rule for memory and for the network comes from here. That said, this is the design intent the language puts forward, and whether that rule actually works well in both areas is a question to judge after an implementation exists.

Writing Down the Current State of This Language as It Is

To avoid overstating maturity I write only what I confirmed. The repository is Apache-2.0 licensed and the primary language is OCaml. At the time I checked, not a single release had been posted. And the author has stated in a public post that it went through five months of research and a few weeks of development and that 0.1.0 is coming soon. In other words, the first version has not shipped yet.

So this is not the stage at which to plan on building something with this language. The reason I still think it is worth reading is that this project describes why it was made as a problem. The author states that it started from dissatisfaction with Rust, giving as the reason that type checking protects memory but does not protect against distributed deadlock or protocol mismatch between services. That diagnosis is correct regardless of the language's completeness. And the fact that an academic lineage accumulated over more than ten years exists as an answer to that diagnosis is the most practical thing you can take from looking at this project.

Wrap-Up and Sources

If we are matching up protocols between services with documents and tests, it is not because the tools do not exist but because the languages we use look at only one node. Choreography is an approach that changes that field of view, and when you change the field of view, some bugs stop being things to fix and become things that cannot be expressed.

• Choreographic Programming — Fabrizio Montesi's own definition. I confirmed from this document that the term came from a 2013 doctoral thesis, the role of endpoint projection, and that deadlock-freedom by design is known from the 2013 work of Carbone and Montesi.
• The Wyzer-Lang/wyzer repository — the syntax example, the design principles, the shape of the error message. The description of Wyzer and the code in this post are taken from that repository README.
• Confirmed from repository metadata: license Apache-2.0, language OCaml, no releases. The statement that 0.1.0 has not shipped yet is from an introductory post the author published.
• Perceus: Garbage Free Reference Counting with Reuse — Reinking, Xie, de Moura, Leijen, PLDI 2021. The source for FBIP and reuse analysis.
• I did not build or run the Wyzer compiler. The code in this post is the example carried in the README, not behavior I verified myself.