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

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2012-171
June 29, 2012

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2012/EECS-2012-171.pdf

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 introduce the ultimate model, which captures non-deterministic eventual outcomes of distributed programs. After showing the question of confluence undecidable for Dedalus, we identify restricted sub-languages that guarantee confluence while providing adequate expressivity. We observe that the semipositive restriction Dedalus+ guarantees confluence while capturing PTIME, but show that its restriction of negation makes certain simple and practical programs difficult to write. To remedy this, we introduce DedalusS, a restriction of Dedalus that allows a kind of stratified negation, but retains the confluence of Dedalus+ and similarly captures PTIME.

BibTeX citation:

@techreport{Marczak:EECS-2012-171,
    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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2012},
    Month = {Jun},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2012/EECS-2012-171.html},
    Number = {UCB/EECS-2012-171},
    Abstract = {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 introduce the ultimate model, which captures non-deterministic eventual outcomes of distributed programs. After showing the question of confluence undecidable for Dedalus, we identify restricted sub-languages that guarantee confluence while providing adequate expressivity. We observe that the semipositive restriction Dedalus+ guarantees confluence while capturing PTIME, but show that its restriction of negation makes certain simple and practical programs difficult to write. To remedy this, we introduce DedalusS, a restriction of Dedalus that allows a kind 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 2012
%8 June 29
%@ UCB/EECS-2012-171
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2012/EECS-2012-171.html
%F Marczak:EECS-2012-171