3 ms·

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

by 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 rntz 12y ago

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.