3 ms·

> Linear-session-typed process calculi are guaranteed deadlock-free and race-free While this may be true for certain restricted systems, this claim is mislead

by mafribe 12y ago

> Linear-session-typed process calculi are guaranteed deadlock-free and race-free While this may be true for certain restricted systems, this claim is misleading. Session types, as invented by K. Honda and refined by numerous others, guarantee deadlock and race freedom only within any given session. Session initiation (basically messages to replicated inputs) can deadlock and race in many (most?) session typing systems. The decision not to guarantee the absence of deadlock at session initiation points is what makes session types so simple. It is possible to restrict session types so that they are completely deadlock-free and race-free, but -- as far as we know -- that guarantee comes at the heavy price of making the typing system completely inexpressive, so you cannot type many natural forms of concurrent programming. Alternatively you can give up on simplicity and make the typing system very complicated (e.g. the system pioneered in "Strong Normalisation in the Pi-Calculus" by Honda et al, and its successors). The former is a real problem, as witnessed by the continuing inability of the session typing crowd to get a handle on message passing in Erlang. Finding a system that is expressive, simple and guarantees deadlock-freedom is a major open research problem (and I suspect infeasible).

rntz 12y ago
I mostly know about the linear logic side of session types; I'm not super familiar with the older line of research starting with Honda. I'll have to read up on it! I'm not sure what the equivalent in my world of "session initiation" is. If by "replicated inputs" you mean what in linear logic is expressed by the "!" connective (often called "replication"), it's definitely possible to have ! without deadlocks or any observable nondeterminism. See Caires & Pfenning, "Session Types as Intuitionistic Linear Propositions", for example. I already listed a few of the limitations of this approach (limited process topologies, and no `select()` analogue). I'm not sure whether these qualify as "completely inexpressive", but I do think the lack of any `select()` analogue is pretty limiting in practice. I'm not sure how hard it might be to remove that limitation, but it wouldn't surprise me if that were a major sticking point. Still, overall I think I'm more optimistic about the possibility of capturing most reasonable forms of concurrent programming in a deadlock & race-free manner.
- mafribe 12y ago
  Honda's pioneering papers on session types (and on everything else for that matter) are always worth reading. Yes, replicated input is !x(v1).P in pi-calculus, and Milner was directly inspired by linear logic's replication. > Still, overall I think I'm more optimistic about the possibility of capturing most reasonable forms of concurrent programming in a deadlock & race-free manner. I don't think you can, or indeed want to excise all forms of race condition from concurrent programs, for if you do that, there would be little concurrency left. You could only do deterministic concurrency, which is not what you want in many cases, e.g when you use concurrency to mask latency. For example how would you define a lock or mutex if all races are forbidden? You need race conditions, but you want them in homeopathic doses, you want them constrained and tightly controlled. I also doubt that concurrent programming patterns like dynamic deadlock detection and removal are amenable to a type-theoretic analysis in linear-logic based systems such as Caires & Pfenning's.

by mafribe 12y ago

rntz 12y ago

I mostly know about the linear logic side of session types; I'm not super familiar with the older line of research starting with Honda. I'll have to read up on it! I'm not sure what the equivalent in my world of "session initiation" is. If by "replicated inputs" you mean what in linear logic is expressed by the "!" connective (often called "replication"), it's definitely possible to have ! without deadlocks or any observable nondeterminism. See Caires & Pfenning, "Session Types as Intuitionistic Linear Propositions", for example. I already listed a few of the limitations of this approach (limited process topologies, and no `select()` analogue). I'm not sure whether these qualify as "completely inexpressive", but I do think the lack of any `select()` analogue is pretty limiting in practice. I'm not sure how hard it might be to remove that limitation, but it wouldn't surprise me if that were a major sticking point. Still, overall I think I'm more optimistic about the possibility of capturing most reasonable forms of concurrent programming in a deadlock & race-free manner.

mafribe 12y ago
Honda's pioneering papers on session types (and on everything else for that matter) are always worth reading. Yes, replicated input is !x(v1).P in pi-calculus, and Milner was directly inspired by linear logic's replication. > Still, overall I think I'm more optimistic about the possibility of capturing most reasonable forms of concurrent programming in a deadlock & race-free manner. I don't think you can, or indeed want to excise all forms of race condition from concurrent programs, for if you do that, there would be little concurrency left. You could only do deterministic concurrency, which is not what you want in many cases, e.g when you use concurrency to mask latency. For example how would you define a lock or mutex if all races are forbidden? You need race conditions, but you want them in homeopathic doses, you want them constrained and tightly controlled. I also doubt that concurrent programming patterns like dynamic deadlock detection and removal are amenable to a type-theoretic analysis in linear-logic based systems such as Caires & Pfenning's.