Is undo/1 harmful?

[Jan Burse]

Dear All,

I am experimenting with the implementation of an undo/1,
it will have the name sys_unbind/1. Motivation are
forward and constraint stores, to have transient side
effects. So for example one would add an element to the
store via:

assume(X) :-
assertz(X),
sys_unbind(retract(X)).

I am now reading that the SICStus documentation has
deprecated the predicate undo/1. The documentation says:

"Dropped because it was not possible to ensure
the correct behavior in all circumstances. Users
that know what they are doing can still call the
unsupported predicate prolog:undo/1. The argument
should have a module prefix."

My understanding is that it can be implemented with special
cells on the trail, so that a strong version would be immune
against the cut. But I have also experience that it blows
up a little bit the code of an interpreter, especially when
exceptions should gracefully transpire.

My solution concerning exceptions is similar to the solution
of exception handling for setup_call_cleanup in Jekejeke
Prolog, i.e. exceptions are accumulated. So I would get
the following for multiple exceptions:

?- X=1, sys_unbind(throw(x)), Y=2, sys_unbind(throw(y));
X=3, Y=4.
X = 1,
Y = 2 ;
Unknown exception: y
Unknown exception: x
?- catch((X=1, sys_unbind(throw(x)), Y=2, sys_unbind(throw(y));
X=3, Y=4),Z,true).
X = 1,
Y = 2 ;
Z = cause(y, x)

cause/2 is the error term for accumulated exceptions. But the
SICStus comment confuses me a little bit. What are the circum-
stances when a strong undo/1 might behave wrongly? How can it
be that nevertheless the end-user is allow to use it? What
knowledge does the end-user need to master undo/1?

I am also observing that one needs to get used to the behaviour
of the undo/1. Most Prolog systems eliminate unnecessary choice
points and then try to defer the undoing of the trail as much as
possible. A single undo is cheaper that many small undos. Jekejeke
Prolog applies similar techniques. So I observed that the undo/1
can blur the borders of catch/3. Here are two examples:

?- catch((X=1, sys_unbind(throw(x))),Z,true).
X = 1
Unknown exception: x
?- catch((X=1, sys_unbind(throw(x)); X=2),Z,true).
X = 1 ;
Z = x

In the first example the catch optimizes away its choice point
since the inner goal has not left any choice point. As a result
the exception is throw when the top level query answer loop does
the unbind. The the second example everything works fine. The
first example would work differently when the catch/3 would not
only inspect the choice points, but also the trail.

Is the blurring of exceptions considered incorrect behaviour or
what the end-user needs to know?

Best Regards

[Jan Burse]

Dear All,

Jan Burse schrieb:
> - The constraint store could profit from
> a brother of setup_call_cleanup/3, that
> invokes a cleanup goal when bindings
> are undone.

I have created a study object. 8-queens via
forward chaining. The labeling makes use of
SICStus undo/1 to undo contraints stored
in the knowledge base.

Here is an example session. First load the
forward chainer (delta3.p), then forward rules for
fd_domain/1, #=/2 and #\=/2 (ineqr3.p). And finally
queens with forward rules for X + Y #\= Z
(queens3.p).

?- ['demo/forward/delta3.p'].
Yes
?- ['demo/forward/ineqr3.p'].
Yes
?- ['demo/forward/queens3.p'].
Yes

Here is an example of setting up the constraint
store. The list/0 predicate simply shows the
actual content of the knowledge base. (The
content will go away via SICStus undo/1 on redo
respectively undo, so queries can safely be
posted consecutively in the top level):

?- queens([x,y,z],[1,2,3]), list.
inr(x, [1, 2, 3]).
inr(y, [1, 2, 3]).
inr(z, [1, 2, 3]).
nqr(x, y).
nqr(x, z).
nqr(y, z).
naddr(x, 1, y).
naddr(y, 1, x).
naddr(x, 2, z).
naddr(z, 2, x).
naddr(y, 1, z).
naddr(z, 1, y).
Yes

Here is an example of setting up the constraint
store and then perform some labeling:

?- queens([x,y,z,t,u,v,w,q],[1,2,3,4,5,6,7,8]),
label_list([x,y,z,t,u,v,w,q]), list.
eqr(x, 1).
eqr(y, 5).
eqr(z, 8).
eqr(t, 6).
eqr(u, 3).
eqr(v, 7).
eqr(w, 2).
eqr(q, 4).
Yes ;
eqr(x, 1).
eqr(y, 6).
eqr(z, 8).
eqr(t, 3).
eqr(u, 7).
eqr(v, 4).
eqr(w, 2).
eqr(q, 5).
Yes

Here a little sanity check, how many solutions will the
labeling generate?

?- L^(findall(sol,(queens([x,y,z,t,u,v,w,q],[1,2,3,4,5,6,7,8]),
label_list([x,y,z,t,u,v,w,q])),L), length(L,N)).
N = 92

The above is still a study object. The forward chainer
has no indexing yet, constraints are not yet thread local.
And I did not yet compare the performance with other
constraint systems. Also sys_unbind/1, the undo/1
implementation in Jekejeke Prolog, is not yet released.

More info.
https://plus.google.com/u/0/b/103259555581227445618/103259555581227445618/posts/2q6nd6VbgZJ

Comments welcome.

Bye

[Per Mildner]

On Mar 28, 5:48 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> I am experimenting with the implementation of an undo/1,

> ...

> I am now reading that the SICStus documentation has
> deprecated the predicate undo/1. The documentation says:
>
>         "Dropped because it was not possible to ensure
>         the correct behavior in all circumstances. Users
>         that know what they are doing can still call the
>         unsupported predicate prolog:undo/1. The argument
>         should have a module prefix."
>

> ... What are the circum-

> stances when a strong undo/1 might behave wrongly?

I no longer remember all the details.

One problem is trailing of variables (and mutables) accessible from
the undo-goal. In effect, the undo-goal may be run with a term that
contains dangling pointers, or at least terms (or mutable values)
different from those used when undo/1 was called. I suspect that this
can be made worse by clever tricks played by the memory manager when
it tries to clean up the heap and the trail. These problems do not
occur with call_cleanup/2 since it can use a choice point that
prevents premature cleanup.

> How can it
> be that nevertheless the end-user is allow to use it? What
> knowledge does the end-user need to master undo/1?

It is available for backwards compatibility for users that know that
their code "happens" to work. It should not be used.

Regards,

Per Mildner

[Jan Burse]

Per Mildner schrieb:

> In effect, the undo-goal may be run with a term that
> contains dangling pointers, or at least terms (or mutable values)
> different from those used when undo/1 was called.

I see this in call cleanup. Not in the sense that there
are less bindings when cleanup is called compared to the
bindings when the cleanup was installed. But in the sense
that there are more bindings when the cleanup is called.

Here is an example:

?- setup_call_cleanup(true,(X=1;X=2),(write(X),nl)), !.
1
X = 1

But the ISO draft requires that during an exception event
the bindings are undone before calling the cleanup, so
that we have (works only since 0.9.3 in Jekejeke Prolog):

?- setup_call_cleanup(true,(X=1;X=2),(write(X),nl)), throw(x).
_A
Unknown exception: x

Now what has this to do with undo/1 (respectively sys_unbind/1
how it is now called in Jekejeke Prolog since 0.9.3). Well I
came to the conclusion that it is not possible to make this
distinction for undo/1.

The undo handler is called when the bindings are undo. This
is a loop similar to the cleanup loop that cleans the choice
points (very simplified, in the realization condition for
cleanup is not a mark as depicted below).

cleanup loop:

while (cp != mark) {
/* cleanup choice point */
cp = cp.next;
}


undo loop:

while (bind != mark) {
/* undo binding */
bind = bind.next;
}

Now for a handler posited by sys_unbind/1, the handler will
be called in the /* undo binding section */. This is how
sys_unbind/1 is implemented in Jekejeke Prolog. It sits in
a different datastructure from the choice points and it
reacts on different events. So its different from
setup_call_cleanup.

So from the above we see that the handler will not have
any new bindings available, since it is part of the undo
loop, and thus the bindings are anyway gone when the handler
is called.

Fear I had was that the above is not performant enough.
Since the undo loop needs to check whether it will do a
normal variable undo or whether it needs to invoke the handler.
Also fear was that the handler will confuse the undo
loop itself.

But so far both pitfals did not materialize. There is actually
a performance drop, especially since the undo loop needs more
context parameters and better error handling. But the performance
drop is very small (~1% observed so far). And the undo loop
gets not broken, since the undo handler is called in a way
so that all new bindings are undone before returning.

But I guess other designs, for example using a separate list
for the undo handlers, could lead to the problem you describe.
When undo handlers are not called in the same order as normal
variable bindings are undone.

Unfortunately my design generates one more case where the
interpreter needs native stack. I have currently the same
problem with catch/3 and sys_cleanup/1. Its not a design
where we stay inside an interpreter loop. The interpreter
loop is recursively called inside the undo loop.

I have a simple idea how to avoid native stack for the catch/3.
But I am not yet close to any simple idea for sys_cleanup/1 or
sys_undo/1, except for building an elaborate state machine from
the sequential solution. Maybe this could be also a reason for
alternative designs and other pitfals.

Bye

[Jan Burse]

Jan Burse schrieb:

> Dear All,
>
> Jan Burse schrieb:
> > - The constraint store could profit from
> > a brother of setup_call_cleanup/3, that
> > invokes a cleanup goal when bindings
> > are undone.
>
> I have created a study object. 8-queens via
> forward chaining. The labeling makes use of
> SICStus undo/1 to undo contraints stored
> in the knowledge base.

Oho, more study objects:

MiniZinc Challenge 2011 Results
http://www.g12.csse.unimelb.edu.au/minizinc/challenge2011/results2011.html

Yummy

[Jan Burse]

Dear All,

Currently putting sys_unbind/1 to use for some
hypothetical reasoning. It seems that sys_unbind/1
needs to be combined with sys_atomic/1.

So retire/assume would be defined as follows:

assume(X) :-
sys_atomic((assertz(X),
sys_unbind(retract(X)))).

retire(X) :-
sys_atomic((retract(X),
sys_unbind(assertz(X)))).

sys_atomic/1 is the meta predicate that executes
a goal without allowing soft signals (i.e. error
terms thrown from the outside).

If a soft signal would be allowed it would be
possible that for example in assume/1 an assertz/1
is done but no undo handler is installed via
sys_unbind/1. So that hypothetical reasoning
step is incompletely execute and would leave the
knowledge base modified after undo.

Currently checking what the performance
penalty would be to have sys_atomic/1 around.
Of course assume/retire could also be implemented
natively, so that no sys_atomic/1 would be
needed.

Best Regards


Jan Burse schrieb:

[Jan Burse]

Dear All,

Jan Burse schrieb:

> Here a little sanity check, how many solutions will the
> labeling generate?
>
> ?- L^(findall(sol,(queens([x,y,z,t,u,v,w,q],[1,2,3,4,5,6,7,8]),
> label_list([x,y,z,t,u,v,w,q])),L), length(L,N)).
> N = 92

First benchmark results.
9-queens 2 times.

B-Prolog: 7ms
GNU Prolog: 7ms
SWI-Prolog: 782ms
Jekejeke Prolog: 2580ms

Could not yet pin-point the bottleneck.
For more info:
https://plus.google.com/u/0/b/103259555581227445618/103259555581227445618/posts/TcYxffHg57g

Bye

[Jan Burse]

Dear All,

Just noticed that SWI-Prolog CLP(FD) (*) has step, enum
and bisect branching. Any classical paper around that
shows the impact on some pratical problems and some
theoretical discussions.

Bye

(*)
http://www.swi-prolog.org/pldoc/doc_for?object=labeling/2

Jan Burse schrieb:

[Jan Burse]

Hi,

Oh, this one doesn't look too bad:

Principles of Constraint Programming
Krzysztof Apt,
Cambridge University Press (28. August 2003)

Bye


Jan Burse schrieb: