William Marczak, Peter Alvaro, Neil Conway, 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}, Institution = {EECS Department, University of California, Berkeley}, 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