Truly Concurrent Constraint Programming

Vineet Gupta, Radha Jagadeesan, Vijay A. Saraswat

Abstract

Concurrent Constraint Programming (CCP) is a powerful computation model for concurrency obtained by internalizing the notion of computation via deduction over (first-order) systems of partial information (constraints). In [SRP91] a semantics for indeterminate CCP was given via sets of bounded trace operators; this was shown to be fully abstract with respect to observing all possible quiescent stores (= final states) of the computation. Bounded trace operators constitute a certain class of (finitary) "invertible" closure operators over a downward closed sublattice. They can be thought of as generated via the grammar:

t ::= c | c -> t | c /\ (c -> t)

where c ranges over constraints, /\ is conjunction and -> intuitionistc implication. We motivate why it is interesting to consider as observable a "causality" relation on the store: what is observed is not just the conjunction of constraints deposited in the store, but also the causal dependencies between these constraints - what constraints were required to be present in the computation before others could be generated. We show that the same construction used to give the "interleaving" semantics in [SRP91] can be used to give a true-concurrency semantics provided that denotations are taken to be sets of bounded closure operators, which can be generated via the grammar:

k ::= c | c -> k | k /\ k

Thus we obtain a denotational semantics for CCP fully-abstract with respect to observing this "causality" relation on constraints. This semantics differs from the earlier semantics in preserving more fine-grained structure of the computation; in particular the law

(c -> A) /\ (d -> B) = (c -> (A /\ (d -> B))) [] (d -> (B /\ (c -> A)))

is not verified ([] is indeterminate choice). Relationships between such a denotational approach to true concurrency and different powerdomain constructions are explored.

@InProceedings{truecc-concur96,
  author =       " Vineet Gupta and Radha Jagadeesan and Vijay Saraswat".
  title =        "Truly concurrent constraint programming",
  editor =       "Ugo Montanari and Vladimiro Sassone",
  booktitle =    "{CONCUR} '96: concurrency theory: 7th International
                 Conference, Pisa, Italy, August 26--29, 1996:
                 proceedings",
  volume =       "1119",
  publisher =    "Springer Verlag",
  series =       "Lecture Notes in Computer Science",

}

Postscript File (126K)
Pdf File (182K)