UC BERKELEY
EECS technical reports
TECHNICAL REPORTS


EECS-2012-171.pdf
Conditions of Use

Archive Home Page

Confluence Analysis for Distributed Programs: A Model-Theoretic Approach

Authors:
Marczak, William
Alvaro, Peter
Conway, Neil
Hellerstein, Joseph M.
Maier, David
Technical Report Identifier: EECS-2012-171
2012-06-29
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.