Confluence Analysis for Distributed Programs: A Model-Theoretic Approach
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
Building on recent interest in distributed logic programming, we take a model-theoretic approach to analyzing confluence of asynchronous distributed programs. We begin with a model-theoretic semantics for Dedalus and develop the concept of ultimate models to capture the non-deterministic eventual outcomes of distributed programs. After demonstrating the undecidability of checking confluence for Dedalus programs, we look for restricted sub-languages that guarantee confluence while providing adequate expressivity. We observe that a simple semipositive restriction called Dedalus guarantees confluence while capturing PTIME, but demonstrate that the limited use of negation in Dedalus makes certain simple and practical programs very difficult to express. To remedy this, we introduce DedalusS , a restriction of Dedalus that allows a natural use of negation in the spirit of stratified negation, but retains the confluence of Dedalus and similarly captures PTIME.
- Computer Programming and Software