« The 'Scalability' Bugaboo | Main | What Can Be Implemented Anonymously? »

Concurrency Theory

Ironically, just a week after I posted a screed about the lack of purpose in process-calculus research, I found myself trying to write a semantic model for a distributed programming language.

My purpose was not to prove anything about computation, but just to explicate the language precisely.

I have some strange requirements. I want to show that my semantics are realistic for a certain kind of environment, having peculiar limitations (for example, threads exist in particular locations, which could fail, and not all primitives are available in all locations; some components of the system are single-threaded...), so I want to choose a system that is close to that environment. CCS, pi-calculus, and join calculus are not at all realistic for distributed computation of any sort, so I shied away from those.

Fortunately, not all process calculists are blind to the issues that arise in distributed computing. Andrew Gordon has a nice page on "Nominal Calculi for Security and Mobility," summarizing various attempts to resolve the unrealisms. He observes that "Synchronisation on global channels is the basic communication primitive of the pi calculus. Many authors note that this is an expensive primitive to implement in a distributed system."

Fournet, et al., motivate their "Calculus of Mobile Agents" [1] with this acknowledgement:

Suppose ... that we want to implement a concurrent calculus with CCS-like communication channels and with processes running on different physical sites. If we do not locate channels, we quickly face a global consensus problem for nearly every communication which uses the interconnection network.

Later, they introduce the distributed reflexive chemical machine (DRCHAM), an extension of CHAM, which offers located solutions—that is, bags of processes which are collected together and marked with a location—and limit the communication between locations. As a result, "The transport is deterministic, static, and point-to-point, and synchronization is only done locally on the receiving site during message treatment."

The mobile ambient calculus of Cardelli and Gordon [2] is similar to the DRCHAM model in that it provides named locations. I haven't read this work in detail yet so I can't compare the two.

The upshot is that there may be a calculus which is realistic enough to model the issues that our programming language is designed to solve, and hence it may be worthwhile modeling our language in that calculus. Using the classical process calculi would not have been fruitful, any more than modeling it on a regular old Turing machine.

[1] Cédric Fournet and Georges Gonthier and Jean-Jacques Lévy and Luc Maranget and Didier Rémy. A Calculus of Mobile Agents. Proceedings of the 7th International Conference on Concurrency Theory. Springer-Verlag, 1996.
[2] Luca Cardelli and Andrew D. Gordon. Mobile Ambients. Foundations of Software Science and Computation Structures: First International Conference. Springer-Verlag, 1998.

Post a comment