William Marczak and Peter Alvaro and Neil Conway and Joseph M. Hellerstein and David Maier

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2011-154

December 18, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-154.pdf

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 Dedalus^S , 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.

---

BibTeX citation:

@techreport{Marczak:EECS-2011-154,
    Author= {Marczak, William and Alvaro, Peter and Conway, Neil and Hellerstein, Joseph M. and Maier, David},
    Title= {Confluence Analysis for Distributed Programs: A Model-Theoretic Approach},
    Year= {2011},
    Month= {Dec},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-154.html},
    Number= {UCB/EECS-2011-154},
    Abstract= {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 Dedalus^S , 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.},
}

EndNote citation:

%0 Report
%A Marczak, William 
%A Alvaro, Peter 
%A Conway, Neil 
%A Hellerstein, Joseph M. 
%A Maier, David 
%T Confluence Analysis for Distributed Programs: A Model-Theoretic Approach
%I EECS Department, University of California, Berkeley
%D 2011
%8 December 18
%@ UCB/EECS-2011-154
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-154.html
%F Marczak:EECS-2011-154