cleary@calgary.UUCP (John Cleary) (03/12/85)
I agree with Jacob Levy it is certainly time we sorted out the semantics of Concurrent prolog. First concerning the problem of ? annotations in the head of clauses, Jacob says he doesnt want the status of a variable to become read-only in a delayed fashion on a distributed system. I have running a distributed system which solves this particular problem (it was much easier than a lot of other problems). An example program may help: Goal: ...a(X), b(X), ... a(Z?):- true | some things which better have references to Z. b(1). In a sequential implementation (that is any where all bindings are seen immediately by everyone) either a or b is executed first. If a first then X is bound to Z? becoming read only, then b(X) suspends. If b first then X is bound to 1 and a suspends. If however the goal is ... a(X)@hither, b(X)@yon ... where hither and yon are distant processes with their own local copies of X. Then both may succeed locally and you have X bound to both 1 and Z? The approach I have taken is that this is fine but that when the bindings meet the unification suspends. I generate a ghost process unify(Z?,1) which will suspend until someone somewhere binds Z. This effect can be achieved locally by rewriting the goal as ... a(X1), b(X2), eq(X1,X2), ... eq(X,X). Then even in a sequential simulation of concurrency all possible things can happen depending on the order that a, b and eq are executed. This raises a serious problems (apart from the problem of what is CP?). I want to write distributed systems and I dont want the semantics of my programs to change when I run them distributed. Effects such as the above cannot occur in any of the CP interpreters I know of as all distribute their bindings immediately to everyone. Udi advises us to trust in our debuggers and interpreters and not in God. It seems that any trust in the debuggers is sadly misplaced. A good rule for a debugging system for concurrent programs is that if it can happen in any semanticly legal system then it can happen in your debugging system -- at least then it is possible to find your bugs. It seems that unification should NOT be seen as an atomic operation, but one whose individual steps occur concurrently. This is reinforced by the following problem: Goal: a(X?,X) a(1,1):- true. As pointed out by Vijay Saraswat this suspends if you unify left to right but doesnt if you unify right to left. (I wonder if a Hebrew implementation would differ here (-:)) The correct solution (it my opinion anyway) is to 'partially' suspend the attempt at unification at the point where unify(X?,1) is attempted but to continue with the second part unify(X,1) which will succeed waking the earlier unify which too succeeds so that ultimately there is no suspension. To do this I essentially split the unification into concurrent steps. The result gves an order independent unification. Code for my unify routine follows (it works or has given me no trouble for a year now, but is slower than Udi's original by a factor of about 2!). It also handles (one of) Vijays other concerns, unify(X?,X) this is special cased out and succeeds. Question: if unification is treated concurrently like this should the implicit sequencing between the unification in the head of a goal and execution of the guards be maintained, does it make any difference to the semantics? To put it another way are the following two clauses semanticly identical: a(1,foo):- some guard | some body. a(X,Y):- unify(X,1), unify(Y,foo), some guard | some body. I think as a point of principle that they aught to be. ---------------------------------------------------------- %this can replace the original unify in Ehud Shapiro's 1983 paper %a subset of concurrent prolog unify(X,Y):- u(X,Y,Head-[mark|Tail]), unify1(Head-Tail,changed). unify1([mark|_]-_,suspended):- !, fail. unify1([mark]-[],Flag):- !. unify1([mark|Head]-[mark|Tail],changed):- !, unify1(Head-Tail,suspended). unify1([u(X,Y)|Head]-Tail,Flag):- u(X,Y,Tail-NewTail), check_changed(u(X,Y),Tail-NewTail,Flag,NewFlag), unify1(Head-NewTail,NewFlag). check_changed(_,_,changed,changed). check_changed(XY,[Z|Tail]-Tail,suspended,suspended):- XY == Z, !. check_changed(XY,[Z|Tail]-Tail,suspended,changed). u(X,Y,H-H):- var(X), !, deref(Y,Y1), u0(X,Y1). u(X,Y,H-H):- var(Y), !, deref(X,X1), u0(Y,X1). u(X,Y,H-T):- deref(X,X1), deref(Y,Y1), u1(X1,Y1,H-T). u0(X,Y):- nonvar(Y), Y=Y1?, X==Y1, !. u0(X,X). u1(X?,Y?,H-H):- X==Y, !. /*Because of deref X&Y are both free variables*/ u1(X?,Y,[u(X?,Y)|T]-T):- !. u1(X,Y?,[u(X,Y?)|T]-T):- !. u1([X|Xs],[Y|Ys],H-T):- !, u(X,Y,H-T1), u(Xs,Ys,T1-T). u1([],[],H-H):- !. u1(X,Y,H-T):- X=..[F|Xs], Y=..[F|Ys], !, u1(Xs,Ys,H-T). deref(X,Y):- nonvar(X), X=X1?, nonvar(X1), !, deref(X1,Y). deref(X,X). ----------------------------------------------------------------------------