Abstract: 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.
ECS-LFCS-96-340, January 1996.
This report is available in the following formats: