Detecting Local Channels in Distributed Poly/ML
Paul A. Steckler · 1996
Distributed Poly/ML is a variation on Standard ML that includes primitives for creating threads and for inter-thread communication. Threads may be spawned on remote machines. Values are sent from one thread to another over dynamically-created channels. A channel is considered local iff all its uses take place on the processor on which it was created. We present a constraint-based static analysis that detects local channels. Using a tree replacement technique, we show that constraint solutions may be maintained as invariants at each transition step in a concurrent operational semantics. Relying on such invariants, we prove the soundness of the analysis with respect to the operational semantics. 1