Sciweavers

29
Voted
IFL
2003
Springer

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

14 years 4 months ago
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.
Clara Segura, Ricardo Pena
Added 07 Jul 2010
Updated 07 Jul 2010
Type Conference
Year 2003
Where IFL
Authors Clara Segura, Ricardo Pena
Comments (0)