Nondeterminism, Servers & Clients

In an episode of the “Type Theory Forall” podcast, Phil Wadler said:

❝Linear logic is good for the bits of concurrency where you don’t need concurrency.❞

— Phil Wadler, 2025

Thanks Phil, that’s very encouraging.

What Phil — the wonderful researcher and author of the process language Par is based on — is talking about here is nondeterminism and races. Indeed, linear logic and races are like water and oil. The research has been largely unsatisfying, yielding steps in certain directions, but never quite far enough to solve real-world problems in an elegant and obviously correct manner.

Par offers an innovative solution!

What is nondeterminism?

All features of Par that we’ve covered so far are deterministic. Yes, Par is an automatically concurrent language. Independent bits of your program proceed concurrently, without you needing to lift a finger to make it happen. But when it comes to each single piece, the next instruction clearly says who to talk to, and what to say. Decisions are being made, but they only depend on the inputs. If the inputs have the same values, the outcomes will be the same.

But sometimes, quite often in fact, decisions need to be made based on who speaks first. That’s the race, to speak first. A program gathering information from multiple slow sources can’t say “I’ll first listen to A, then to B.” If A takes 30 minutes to produce its first message, while B has already produced 50 of them, the program just won’t work well.

That’s nondeterminism. It’s not determined if I’ll speak to A or B first, it depends! In this case, it depends on timing.

We’re not talking about randomness, or “nondeterministic choice” here. While those fall under the general umbrella of nondeterminism, the randomness can be understood as a part of the program input. The nondeterminism we are interested in here is concerned with timing.

The problem-space of nondeterminism is quite large, but it mainly comes in two kinds:

  • Bidirectional communication — That’s when A and B have a channel between them, but either of them can speak first. If A speaks first, B must react, and vice versa. This is useful for preemptive cancellation, implementing chat servers or real-time dashboards without periodic pings, and so on.
  • Server and clients — I don’t mean web servers. What I mean is structuring your program as multiple independent agents — clients — that communicate with a central, stateful agent: the server. The server pays attention to one client at a time, but always the one who speaks first.

Par does not solve the first, yet. You can have cancellation, but it has to be cooperative, you can write a chat server, but there’s got to be periodic checks.

Par solves the second: server and clients, while:

  • Keeping all the guarantees: no deadlocks, no runtime crashes, no infinite loops.
  • Leveraging Par’s types as session types to allow arbitrary communication protocols between the server and the clients.
  • Being very simple to understand and reason about!

👉 Just to make sure it’s clear… we’re not talking about web servers here. We’re talking about a concurrent structure, where any number of client agents are communicating with a central server agent, all inside a single program.

The state of the research

When it comes to linear logic — the theory underlying Par — the problem of races is, to my best knowledge, unsolved in research. Here are some papers that shaped my understanding of the problem, and also why they fall short:

  • Client-server sessions in linear logic — This paper is spectacularly elegant. It invents coexponentials, which partially solve the client-server communication topology. Unfortunately, the clients are not resumable.
  • Concurrency and races in classical linear logic — This is a follow-up paper, which tries to solve the non-resumability of the clients by introducing single input, single output interfaces for clients to communicate with a central server. Unfortunately, it’s not as elegant, and still not expressive enough.
  • Safe session-based concurrency with shared linear state — This one is fairly simple, yet surprisingly potent. It introduces a deadlock-safe mutex type, that can be used to safely share a linear resource among independent processes. Unfortunately, it does not extend well to more involved communication protocols.
  • Towards races in linear logic — An extremely elegant approach presented with colorful formulas and icons. It fits very well into linear logic, but unfortunately is restricted to servers with a constant number of clients, which finds few use-cases.

Par’s solution here, its poll/submit control structure, can be used to implement everything from the first 3 papers above, and a lot more, with very few ingredients.

The last paper is able to express some invariants that poll/submit cannot (the constant number of clients), but it’s questionable how useful those could be in real-world programs.