This paper presents a new technique for detection of probabilistic dangling references in multi-core programs. The technique has the form of a simply structured type system and provides a suitable framework for proof-carrying code applications like mobile code applications that have limited resources. The type derivation of each individual analysis serves as a proof for the correctness of the analysis. The type system is designed to analyze parallel programs with structured concurrent constructs: fork-join constructs, conditionally spawned cores, and parallel loops. For a given program S, a probabilistic threshold p_(ms), and a probabilistic reference analysis for S, if S is well-typed in our proposed type system then all computational paths with probabilities greater than or equal to p_(ms) will contain no dangling pointers at run time. The soundness of the presented type system is proved in this paper with respect to a probabilistic operational semantics to our model language.
展开▼
