Correctness of Non-determinism Analyses in a Parallel-Functional Language

The presence of non-determinism in the parallel-functional language Eden creates some problems. Several non-determinism analyses have been developed to determine when an Eden expression is sure to be deterministic, and when it may be non-deterministic. The correctness of these analyses had not been proved yet. In this paper we define a “maximal” denotational semantics for Eden in the sense that the set of possible values produced by an expression is bigger than the actual one. This semantics is enough to prove the correctness of the analyses. We provide the abstraction and concretisation functions relating the cond abstract values so that the determinism property is adequately captured. Finally we prove the correctness of the analyses with respect to the previously defined semantics.

• Type: Conference
• Year: 2003
• Where: IFL
• Authors: Clara Segura, Ricardo Pena
• Keywords: Correctness, IFL 2003, Parallel-functional Language Eden, Several Non-determinism Analyses