Attributed variables: Interface convergence
triska opened this issue · 255 comments
There are two major deficits of the current attributed variable interface predicate attr_unify_hook/2
:
- It is called only after the unification has already taken place.
- In the case of simultaneous unifications like
[X,Y] = [a,b]
, it is called with all bindings already in place.
However, there are cases where we need to reason about variables before the unification takes place or, equivalently, any pre-existing triggering unifications are undone before the hook is called. See below for the justification.
I recommend convergence with the interface used by SICStus Prolog, also to increase portability across different Prolog systems, or the design of an interface that is at least as general.
Specifically, it would help tremendously if verify_attributes/3
were called upon unifications with the same semantics as in SICStus Prolog:
- first, the unifications are undone
verify_attributes(+Variable, +Value, -Goals)
is called- the unifications are redone
Goals
are executed
Real-world examples
I give two examples to explain why attr_unify_hook/2
is insufficient. The first example is shown in git commit 988ea20b7. It shows that the current interface is extremely error prone to use, because it can unexpectedly bind several variables at once and then trigger the hook with an arbitrary number of bindings suddenly in place. Realistically, nobody can exhaustively think of all cases that can simultaneously happen and cover them. The author of dif/2
also ran into this exact problem, as evidenced by a filed issue about dif/2
.
The second example arises in a CLP(B) implementation that uses Zero-suppressed Binary Decision Diagrams (ZDDs). A ZDD is interpreted like any decision diagram, but with the following twist: Variables that do not occur in a branch must be 0. Here is an example showing the ZDD for X=\=Y
, with the dotted lines indicating 0:
When working with ZDDs, we must keep track of all CLP(B) variables that appear in constraints, because we need to figure out "all variables that do not occur in the ZDD".
If unifications are performed step by step, i.e., just as with individual unifications, no problems arise, even with attr_unify_hook/2
. For example, suppose we have X = 1, Y = 1
. The first unification leads us into the right branch of the ZDD. We arrive at true
, which means that this is true if all variables that do not occur in the ZDD (i.e., Y
), are 0
. Therefore, we post Y=0
from within attr_unify_hook/2
. The second unification will therefore automatically fail.
But suppose the unifications are performed simultaneously, as in [X,Y] = [1,1]
. The first unification again leads us into the right branch of the ZDD, but now we cannot find out which variables do not occur in the ZDD, because Y
is no longer a variable at the time the hook is called!
More information about this issue: Minato task.
There may be ways to work around this, but they involve essentially duplicating the Prolog view of variables within the program, using IDs of variables to distinguish them. Also, this is not at all how we expect to reason about our datastructures.
For these reasons, it is very desirable that the unification hooks are called before the bindings are in place, and for each binding individually.
Secretly my mental picture of attribute variables had always been that they are not bound before calls to hooks. When I saw that so many people (yourself @triska included) seeming to be fine with them being bound at the time of the hooks I was really really impressed how you could still do CLP(??) . But, when I started ported to port a version of Description Logic, which amounts to porting CHR, (another todo list convergence LOL). I was stuck doing a mind numbing workaround of linearizing args: That means I was cloning attributed variables just to send them off to their impending "death by unification" in which attrib_unify_hook would send the original copy a gold star (a practice perhaps started in the Great War) .. But i needed to know where to send it and that meant every original variable needed to gensym a module for attrib_unify_hook) .
So let's discuss this issue, I have been working on a branch of SWI-Prolog capable of your needs this but will need help to make it lean towards convergence as well.
moved unrelated content/comments to logicmoo/swipl-devel#1
FYI, I don't have a strong opinion on the attvar interface. I'm happy with everything as long as the old interface remains supported or can be supported using an emulation layer that doesn't make it much slower. Please do look at existing interfaces, probably notably SICStus and ECLiPSe and design things to be as compatible as possible.
If you delay binding, be careful about cyclic terms and the occur check. See e.g., unifiable/3
in pl-prims.c
, which performs the normal unification and then unbinds by examining the trail.
Douglas, it is awesome that you are looking into this! Using the current interface (for clarity, please note the exact spelling: attr_unify_hook/2
) to implement actual constraint solvers is an uphill battle: I managed to do it for CLP(FD), but for CLP(B) it is definitely not general enough. In addition, it is extremely error prone to use, because all variables may already be aliased when the hook is called. So, it is not at all like I'm happily using the interface and everything is fine; in fact, it's more of the opposite: When implementing constraint solvers, I'm continuously struggling with the current SWI interface and always wish for a cleaner one. Thank you for helping to finally solve this issue, I am looking forward to working with you on this and will help in every way I can to port all constraint libraries to the new interface once it becomes available!
To (massively!) improve the situation, having verify_attributes/3
exactly as in SICStus Prolog would be my personal preference: It is very declarative, and most importantly is called with the bindings undone. Please check out the SICStus documentation. Note that the other predicates are all either already available in SWI, or can be easily mapped for compatibility, but verify_attributes/3
can not, because in SWI, the hook (attr_unify_hook/2
) is called with the binding already in place.
I therefore suggest you do the following: In your branch, provide verify_attributes/3
with the same semantics as in SICStus Prolog. In that branch, I will rewrite CLP(FD) and CLP(B) to use this new interface. (This will bring both of these systems closer to running in SICStus Prolog too, as a nice side-effect.) I will have some suggestions on how to support libraries that still use the attr_unify_hook/2
interface for the time being.
Most importantly, please first focus on getting the semantics right. This will allow us to run test cases and port actual solvers to the interface. Please let us postpone the discussion about performance: It is also important, but let us discuss it after having the SICStus-compatible semantics in place. If it is any reassurance, recall that SICStus is much faster than SWI-Prolog in many constraint benchmarks even though its interface for attributed variables is much more general than that of SWI, so this is a good indication that the SICStus interface can also be implemented efficiently.
Markus,
Nice, that get_attr/2
put_attr/2
are named differently than get_attrs/2
or put_attrs/2
. Yes, we can for now (or later) map them.
Looks like I can very easily make verify_attributes/3
work as documented though it will be called only on Module:verify_attributes/3
that has either put_attr/3
or put_attrs/2
in the identical manner and call order that we do with attr_unify_hook/2
Like Sicstus says: "Var might have no attributes present in Module; the unification extension mechanism is not sophisticated enough to filter out exactly the variables that are relevant for Module."
Interesting.. So for our mainstream inclusion into SWI we could leave attr_unify_hook/2
as-is and only called if verify_attributes/3
did not veto the unification?
I see that verify_attributes/3
is documented with the ability to create new choice points.. that won't be a problem (we will see if @JanWielemaker will need to answer a few questions.. But at least on one branch of this, I extended the pl-vmi.c )
I'll get a little bit ahead of myself: In fact, I am glad to create new choice points, this will make labeling/2
magically easier in the future.
Yes, for backward compatibility, we could simply either just call attr_unify_hook/2
after the unification (as is currently the case), or, more elegantly, simply remove special provisions for attr_unify_hook/2
entirely from the core, and automatically add a definition of verify_attributes/3
that yields [attr_unify_hook(Attr,Value)]
to modules that define attr_unify_hook/2
. This expresses attr_unify_hook/2
in terms of verify_attributes/3
, and requires only support for this predicate in the core.
Please expand on where verify_attributes/3
will be called: Note that the SICStus documentation says that verify_attributes/3
may even be called in modules where there are no attributes defined for that variable. It would be OK if that goes down to what you are saying, i.e., only where attributes are actually put on the variable, but it would still be interesting why the unification mechanism of SICStus does not do it as precisely. It may help you to improve the mechanism's performance in some cases if you know that it is OK to call verify_attributes/3
even in modules where the variable has no attribute attached.
Yes that can be a good with with core..
foo:attr_unify_hook(Attrib,Value):- ...CODE...
can be be replaced by
foo:verify_attributes(Var,Value,[]):-get_attr(Var,foo,Attrib), ...CODE...
Expanding on where verify_attributes/3 can be called is very easy to do in fact.
But first off our present situation:
At present in core as you know attr_unify_hook/2
must be present for all modules that wish to add attributes. Why? Optimization, because it is cheaper to assume a predicate exists and call it rather than doing something slow like current_predicate/N
. (I was thinking about this before I read your comments) Wondering if this should also be a requirement of verify_attributes/3
to be defined as well. Personally I don't like either being a requirement.. (so I made it iterated thru the Modules to call verify_attributes/3
I first have it check current_predicate/1
) And it did slow things down a little. Then I argued to myself, "Any module willing to put_attr/3 should be willing to step up and define hooks."
So right now this is how I have verify_attributes/3
implemented
%% '$wakeup'(+List)
%
% Called from the kernel *before* assignments have been made to
% attributed variables.
'$wakeup'(L):-
wno_hooks('$wakeup_attrs'(L)).
% 4096 disables the unification hooks presently running
% don't worry, hook code still be able to use wakeups on other variables.
% This wrapper is only for safe debugging
wno_hooks(G):- '$sinkmode'(W,W),T is W \/ 4096, '$sinkmode'(_,T), call_cleanup(G,'$sinkmode'(_,W)).
% version only calling it where modules have defined an attribute
'$wakeup_attrs'([]).
'$wakeup_attrs'(wakeup(Var, Attrs3, Value, Rest)) :-
call_all_attr_verify_hooks(Var, Attrs3, Value),
(nonvar(Var)->true;Var=Value),
call_all_attr_uhooks(Var, Attrs3, Value),
'$wakeup'(Rest).
% Allow someone who binds this Var to move us onto the next stage
% In fact, they do not even need to use the original value .. for example ...
% ==
% verify_attributes(Var, "between one and three", _Goals) :- member(Var,[1,2,3]).
% ==
% (this is for later labeling .. this does not conflict with Sicstus)
call_all_attr_verify_hooks(Var, _, _) :- nonvar(Var),!.
call_all_attr_verify_hooks(Var, [], Value).
call_all_attr_verify_hooks(Var, att(Module, AttVal, Rest), Value) :-
(current_predicate(Module:verify_attributes/3)->
(attvar_residuals(att(Module,AttVal,[]), Var, Goals, [])-> Module:verify_attributes(Var, Value, Goals)) ;true),
call_all_attr_verify_hooks(Var, Rest, Value).
call_all_attr_uhooks([], _).
call_all_attr_uhooks(att(Module, AttVal, Rest), Value) :-
uhook(Module, AttVal, Value),
call_all_attr_uhooks(Rest, Value).
The alternative that gives that flexibility
% Searches for modules defining verify_attributes/3.
% unused pseudocode :)
call_all_attr_verify_hooks(Var, Attr3, Value) :-
Template= Module:verify_attributes(Var,Value,Goals),
(( current_predicate(_,Template) ,
\+ predicate_property(Template,imported_from(_)),
attrs_to_residual_goals(Attr3,Goals),
(Template -> true ; (!,fail)) )
*-> true ; fail)).
Which I would be happy with if we didn't have to use current_predicate/2
current_predicate/2 and predicate_property/2 are out of the question. For one thing, ISO
current_predicate/2 is not supposed to work for static code (works in SWI). Second, these
are just too slow operations. A simple option is to define
system:verify_attributes(_Var, _Attr3, _Value) :- fail.
I think I'm more in favour of having an undefined predicate trap, as that is far easier to debug
instead of a failing unification because somebody adds an attribute without defining a hook.
Can you help clarifying what will happen if we do put_attr(V, test, a)
and call V = v
. This is my picture with holes:
- Unify
V=v
, this pushes the wakeup goals.- Does the actual binding happen?
- if yes, when and how is it undone? Immediately after unification? Just before
wakeup? - if no, how to we protect against the occur check? This would be problematic
if the answer above is Immediately after unification because there may be
multiple unifications before wakeup is called.
- if yes, when and how is it undone? Immediately after unification? Just before
- Does the actual binding happen?
- If wakeup is called
- We call
verify_attributes(Var, AttrList, Value)
in every module where we now call
attr_unify_hook/2. The difference is that the binding is not yet made and you
have access to all other attributes on this variable. - We can easily provide all attributes to all hooks without changing anything to the C
code. Why do we need access to the variable bound (also next question)?
- We call
- When is the binding actually done? Do the hooks to that? That would mean
X = Y, X == Y
is no longer necessarily true. That would worry me.
Agreed about current_predicate/2
and predicate_property/2
.
I am sure you thought of (and maybe this is what you meant) as well
:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).
And modules could do.
:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).
prolog:verify_attributes(Var,Value,Goals):- \+ mymodule:verify_attributes(Var,Value,Goals) -> (!,fail);true.
mymodule:verify_attributes(Var,Value,Goals):- ...MODULE_CODE...
Answers to the next questions (filling in outline).
But in preview I did test this...
?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X.
Call: (8) [$syspreds] leash(-all)
Unify: (8) [$syspreds] leash(-all)
Exit: (8) [$syspreds] leash(-all)
Call: (8) [system] _G307319{}=_G306598
Exit: (8) [system] _G307319{}=_G307319{}
Call: (8) [system] _G307319{}==_G307319{}
Exit: (8) [system] _G307319{}==_G307319{}
X = Y.
[trace] ?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X,X==Z.
Call: (8) [$syspreds] leash(-all)
Unify: (8) [$syspreds] leash(-all)
Exit: (8) [$syspreds] leash(-all)
Call: (8) [system] _G307384{}=_G306598
Exit: (8) [system] _G307384{}=_G307384{}
Call: (8) [system] _G307384{}==_G307384{}
Exit: (8) [system] _G307384{}==_G307384{}
Call: (8) [system] _G307384{}==_G306604
Fail: (8) [system] _G307384{}==_G306604
false.
Not sure what to think about the trace. In a hurry ...
For the modules, I meant system
. The trick is that whenever you have a module that has
no verify_attributes/3 definition, it will default (first to user
) to the system
module definition.
I definitely do not want to use the prolog
module.
Ahah, i get it.. great idea!
the small change of ...
system:verify_attributes(_Var, _Attr3, _Value).
(At least i think)
There are several misconceptions here, so I would like to first clear up a few important high-level aspects by using the SICStus documentation to walk through the example that Jan posted: Suppose we have put_attr(V, test, a)
, and then post V = v
.
- Engine: First, the binding is undone. The precise timing when this happens is still to be defined, let us discuss it separately. I think we can undo it any time we like, as long as it is before
verify_attributes/3
is called. In fact, if you can implement that, I think the binding need not even take place at all before (5), see below. - Engine:
test:verify_attributes(V, v, Gs)
is called. Note that the second argument is the value that the variable is about to be bound to, not a list of all attributes. - User:
test:verify_attributes/3
is the user-defined predicate. If it is not defined, failure is definitely not an option because that would silently break existing user code. It is also a misconception that the current "attr_unify_hook/2
must be present for all modules that wish to add attributes": This is not the case, as you can easily test, and the current state is desirable for the important reason that we often attach attributes to variables just for efficient lookup in certain datastructures, and these variables are never even unified with anything, so users should not have to defineattr_unify_hook/2
for them. In my view, iftest:verify_attributes/3
is undefined, it should be equivalent totest:verify_attributes(_, _, [])
. - User:
test:verify_attributes/3
must not bind the variable itself. Instead, it communicates via the third argument all goals that are to be invoked after the unification. For instance, the obvious emulation of the currenttest:attr_unify_hook/2
would be:test:verify_attributes(Var, Value, [test:attr_unify_hook(Attr,Value)]) :- get_attr(Var, test, Attr).
- Engine: The original variable binding is redone.
V = v
. - Engine: The goals computed by the third argument of
test:verify_attributes/3
are called.
Note specifically that, due to (5), if X = Y
succeeds, then X == Y
will also succeed.
I would also like to state the most important high-level goal: The current interface falls extremely short in the case of simultaneous unifications like [X,Y] = [a,b]
. This is because at the time attr_unify_hook/2
is called for X
, Y
is no longer a variable and its attributes cannot be directly accessed. Therefore, both unifications must be undone in such cases to truly benefit from verify_attributes/3
. As I understand it, the occurs check may as well take place after (5): Semantically, a unification that is STO is false, so the only downside I see is that an STO unification may fail instead of yielding an error when occurs_check
is set to error
.
if we do put_attr(V, test, a) and call V = v.
- Unify V=v, this pushes the wakeup goals.
- No actual binding happens. Instead, binding is scheduled to happen outside of C via $wakeup/1
- With the occurs_check code there might be some difficulties yet.
- Since there may be multiple unifications before wakeup is called. Each successive unification schedules more wakeup. The attributed variable continues to delay. And remains a variable so it can continue to claim it is free.
- If wakeup is called
- We disable the delay system temporarily for the V so unification treats it like a common variable.
- We call verify_attributes(Var, AttrList, Value) in every module where we now call attr_unify_hook/2. The difference is that the binding is not yet made and we have access to all other attributes on this variable.
- We can easily provide all attributes to all hooks without changing anything to the C code.
- Why do we need access to the variable bound? We really do not need to access it bound since most hooks can see the Value.
- Though I did design a usecase where it is partially bound and the hooks further bind it (like as a workspace) .. (Though a sane person would do that in attributes)
- attr_unify_hook/2 is agnostic to whether it was bound or not.
- Once I had left it unbound, and was able to implement a common prolog variable!
plvar(X):- mvar_set(X,+remainVar),put_attr(X,plvar,binding(X,_)).
plvar:attr_unify_hook(binding(Var,Prev),Value):- Value=Prev,put_attr(Var,plvar,binding(Var,Value)).
- When is the binding actually done it is by the hooks.
- The hooks if poorly written (or brilliantly written) could even make X = Y, X == Y fail. For example they could decide whenever X is bound to a variable to make X = 1 instead. (thus 1==Y fails) ..
- Some case that could be worrisome but other cases useful.
- I did leave in one barrier to hooks when unifying with a plain old prolog variable. Most likely the X=Y will have put X into Y (instead of the other way around) thus never calling wakeups on X. so X==Y.. will effectively be seen as X==X
- I gave us the ability to remove that barrier, that is the more experimental part
Marked with "eager" is where most C code that would call Trail(Y,makeRef(X)). will instead call unifyAttVar(X,Y) which will add a $wakeup/1
test:attr_unify_hook(nonvar,Value):-nonvar(Value).
test:attr_unify_hook(var,Value):- var(Value).
?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y.
false.
?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign),X=Y,X==Y.
X=Y. /*this is why *I* like eager it prevents ignoring the hooks */
?- put_attr(X, test, var), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y.
X=Y.
(BTW: I typed this before reading @triska's post above this one)
@triska Point 4, Perhaps I'll should throw an exception when I get the Var back and it's been bound?
- Engine: First, the binding is undone. The precise timing when this happens is still to be defined, let us discuss it separately. I think we can undo it any time we like, as long as it is before verify_attributes/3 is called. In fact, if you can implement that, I think the binding need not even take place at all before (5), see below.
✔️ completed
Engine: test:verify_attributes(V, v, Gs) is called. Note that the second argument is the value that the variable is about to be bound to, not a list of all attributes.
✔️ completed
User: test:verify_attributes/3 is the user-defined predicate. If it is not defined, failure is definitely not an option because that would silently break existing user code. It is also a misconception that the current "attr_unify_hook/2 must be present for all modules that wish to add attributes":
This is not the case, as you can easily test, and the current state is desirable for the important reason that we often attach attributes to variables just for efficient lookup in certain datastructures, and these variables are never even unified with anything, so users should not have to define attr_unify_hook/2 for them.
system:attr_unify_hook(_,_).
✔️ completed
In my view, if test:verify_attributes/3 is undefined, it should be equivalent to test:verify_attributes(_, _, []).
system:test:verify_attributes(_,_,[]).
✔️ completed
User: test:verify_attributes/3 must not bind the variable itself. Instead, it communicates via the third argument all goals that are to be invoked after the unification. For instance, the obvious emulation of the current test:attr_unify_hook/2 would be:
test:verify_attributes(Var, Value, [test:attr_unify_hook(Attr,Value)]) :-
get_attr(Var, test, Attr).
I think we are almost there .. Perhaps that can happen last and over the course of days and testing (I seem to picture swathes of legacy code).. Not that the above definition would break anything it just seems like we'll need to add it to every module at once .. Since we wont be calling attr_unify_hook/2. on it own
[5] Engine: The original variable binding is redone. V = v.
✔️ completed
Engine: The goals computed by the third argument of test:verify_attributes/3 are called.
✔️ completed
I would also like to state the most important high-level goal: The current interface falls extremely short in the case of simultaneous unifications like [X,Y] = [a,b]. This is because at the time attr_unify_hook/2 is called for X, Y, is no longer a variable and its attributes cannot be directly accessed. Therefore, both unifications must be undone in such cases to truly benefit from verify_attributes/3.
In the case of [X,Y] = [a,b].
Right now X isn't bound yet at the time that verify_attributes(Y,b,Out) will be called .. I like that .. but to make it useful I need to add that burden on the user to tell me when X needs bound ..
Here is an example case
[X,Y] = [a,b(X)].
verify_attributes(Y,b(X),Out) vs verify_attributes(Y,b(a),Out) .
Currently I implemented the C to allow both.
So perhaps test:verify_attributes(Var, Value, [=(Var,Value)])
If they want verify_attributes(Y,b(a),Out) .
to show up?
I need guidence here
As I understand it, the occurs check may as well take place after (5): Semantically, a unification that is STO is false, so the only downside I see is that an STO unification may fail instead of yielding an error when occurs_check is set to error.
unify_with_occurs_check as I understanding it usually takes place before .. it "sanity checks" for potential cyclic results and eventually deems that do_unify() will be mostly unharmed (It cant really protect the system from unifying "child term" which it deemed safe.. ( it wasn't crafty enough to search outside of the unify for a the parent compound structure that our "child term" just changed into a Cyclic term .. I like unify_with_occurs_check and believe its extremely important to have but I need help picturing an example scenario that isn't the fault of the hooks doing something by mistake
Hmmm. I'm a bit lost :( Time to look at the source and the docs. Where do I start?
I am getting ahead of myself :) and needing to set up some cases to confirm things are working as expected .. And when i Clicked on the link below I saw a I saw a couple silly things I meant to fix in attvar.pl and pl-attvars.c anyhow .. SWI-Prolog/swipl-devel@master...logicmoo:treading-lightly
Also I need to find a saner place to store the int value I am keeping around for getSinkMode/setSinkMode .. You (Jan) have probably thought of 100 ways to store extra data for transient variables. Since my system must be error prone (since maybe the global stack moves) and I was surprised it even worked ( it was just to get myself started ) SWI-Prolog/swipl-devel@master...logicmoo:treading-lightly#diff-71d04f2fb2968a749c485db7ea5627caR307
A thought, I realized we an keep the calls to attr_unify_hook/2 as-is since it is defined having a fallback in system
Please let us keep the discussion focused on ensuring compatibility with SICStus Prolog first, and by this I mean for now only the correct implementation of verify_attributes/3
. First, please all read the actual documentation of verify_attributes/3
, and then check out the following sample code that runs with SICStus Prolog (4.3.2):
:- module(test,
[]).
:- use_module(library(atts)).
:- attribute a/0.
verify_attributes(X, Value, []) :-
format("verifying: ~w = ~w\n", [X,Value]).
Please consider the example:
| ?- test:put_atts(X, +a), X = 3.
verifying: _6279 = 3
X = 3 ? ;
no
In SWI-Prolog, the code will look like this:
:- module(test,
[]).
verify_attributes(X, Value, []) :-
format("verifying: ~w = ~w\n", [X,Value]).
Douglas, when I try it with your branch, I get:
?- put_attr(X, test, a), X = a.
X = a ;
false.
Thus, it seems that verify_attributes/3
is not even called in this case.
verify_attributes/3
is really all that is needed to unlock the increased generality of the SICStus interface, everything else can be rather trivially worked around.
For reference, here is the example posted earlier, to test simultaneous unifications with SICStus Prolog:
:- module(test,
[]).
:- use_module(library(atts)).
:- attribute a/1.
verify_attributes(X, Value, []) :-
get_atts(X, a(Other)),
format("verifying: ~w(~w) = ~w\n", [X,Other,Value]).
Please study carefully the following query and result:
| ?- test:put_atts(X, +a(Y)), test:put_atts(Y, +a(X)), [X,Y] = [x,y(X)]. verifying: _3101(_3121) = x verifying: _3121(x) = y(x) X = x, Y = y(x) ? ; no
Note especially that Y is not instantiated in the first invocation, but X [sic!] is already instantiated in the second invocation of verify_attributes/3
. This is exactly as documented, and is also what we intuitively expect. In the SWI port, please also implement this semantics.
Generalizing, to see the behaviour for 3 variables in simultaneous unifications:
:- module(test,
[]).
:- use_module(library(atts)).
:- attribute a/1.
verify_attributes(X, Value, []) :-
get_atts(X, a(Vs)),
format("verifying: ~w = ~w; vars: ~w\n", [X,Value,Vs]).
Example query with SICStus:
?- A = a([X,Y,Z]), test:put_atts(X, +A), test:put_atts(Y, +A), test:put_atts(Z, +A), [X,Y,Z]=[0,1,2]. verifying: _359 = 0; vars: [_359,_371,_383] verifying: _371 = 1; vars: [0,_371,_383] verifying: _383 = 2; vars: [0,1,_383] A = a([0,1,2]), X = 0, Y = 1, Z = 2 ? ; no
@triska Thank you for those examples.. yep my branched regressed .. and looks like I didn't commit it in the last working state (so even if my earlier commits called verify_attributes/3
, there were other things that I needed to change).. so now hopefully w/in 12 hours of me posting this message I'll have an unregressed + have a the above multiple unification patterns.
In that case, I'll wait a little ... Should be able to find some time before X-mas for this.
test:verify_attributes(X, Value, []) :-
get_attr(X, test, Attr),
format("~Nverifying: ~w = ~w; (attr: ~w)\n", [X,Value,Attr]).
/*
?- put_attr(X, test, a), X = a.
verifying: _G389386 = a; (attr: a)
X = a.
?- put_attr(X,test, vars(Y)), put_attr(Y,test, vars(X)), [X,Y] = [x,y(X)].
verifying: _G389483 = x; (attr: vars(_G389490))
verifying: _G389490 = y(x); (attr: vars(x))
?- VARS = vars([X,Y,Z]), put_attr(X,test, VARS), put_attr(Y,test,VARS), put_attr(Z,test, VARS), [X,Y,Z]=[0,1,2].
verifying: _G389631 = 0; (attr: vars([_G389631,_G389638,_G389645]))
verifying: _G389638 = 1; (attr: vars([0,_G389638,_G389645]))
verifying: _G389645 = 2; (attr: vars([0,1,_G389645]))
VARS = vars([0, 1, 2]),
X = 0,
Y = 1,
Z = 2.
*/
Note that the SICStus documentation says that verify_attributes/3 may even be called in modules where there are no attributes defined for that variable. It would be OK if that goes down to what you are saying, i.e., only where attributes are actually put on the variable, but it would still be interesting why the unification mechanism of SICStus does not do it as precisely. It may help you to improve the mechanism's performance in some cases if you know that it is OK to call verify_attributes/3 even in modules where the variable has no attribute attached.
Looks like Yap (and Sicstus keep track of these "potentially interested" modules that do not place attributes onto variables (modules who have placed attributes at least on one variable once)
I would like do it in this order:
- Modules with attributes on the variable first
- Next the source module of the code that is using the attributes. (if not already tried)
- The current module at the top level (if not already tried)
- Modules in which YAP stored in
:- dynamic attributes:modules_with_attributes/1. (not already tried)
moved unrelated content/comments to logicmoo/swipl-devel#1
moved unrelated content/comments to logicmoo/swipl-devel#1
put_atts/2
get_atts/2
I wonder if it would be best to store..
?- test:put_atts(X,+a(Y)),test:put_atts(X,+b(Y)),test:put_atts(X,+c(Y)),test:put_atts(X,-b(Y)),get_attrs(X,Attrs).
Attrs = att(test,[a(Y),c(Y)],[]).
Very nice job Douglas! I have pushed versions of CLP(FD) and CLP(B) that use the new verify_attributes/3
to your branch, so that you can try them.
The new interface has allowed me to simplify the code in CLP(B), and will enable several performance improvements in CLP(FD), because the continuation goals now can be stated explicitly instead of via the detour involving the global queue. I will now work more on this, and also run more tests with the new interface, because there are still some errors I found (probably both in the branch and also in my changes).
The new interface will turn problems like this one into distant memories, and for this I am extremely grateful. Thank you for working on this, and I hope a cleaned up version of your changes will soon make it into the SWI core.
This is a great example how a concrete contribution will make SWI easier to use and more robust for everybody who is working with constraints, paving the way for more interesting and reliable applications!
@triska Thank you!
If it seems slower on orders of magnitudes.. don't despair, I can speed it up to what it was before pretty easily. (Just at the moment doing stuff that makes the code a little deeper in prolog frames than I need to in the long run.. (Finding the balance between minimalism in the Prolog<->C))
One thing I noticed is that if verify_attributes/3
itself vetoes the binding then the unification unexpectedly still succeeds. For example:
?- [library(clpfd)]. true. ?- X #\= 3, X = 3. X in inf..2\/4..sup.
It works as expected with the continuation goals: If they fail, then the unification also fails, which is exactly as one would expect.
Now if verify_attributes/3 itself vetoes the binding then the unification expectedly fails.
Hi Douglas,
I had a look using git diff HEAD..logicmoo/treading-lightly
. Seems some great work is done in that branch. Getting more powerful attributed variables is certainly something to strive for, in particular for exploring the sweet spot between classical Prolog and ASP that CLP provides us in my opinion.
I'm also worried about this patch. It is huge, it includes sources from various other projects with unclear license conditions, it includes a lot of stuff that does not follow the SWI-Prolog coding conventions including PlDoc documentation, it surely has some mistakes/misconceptions (see below) and (possibly incorrectly), some performance alarm-bells are ringing. Considering the level at which this integrates with the system, that must all be resolved.
Most of this is just work, which should be fine if you or someone else is willing to invest the time. I'm afraid I won't spend much time on this considering the pile of work I promised long time ago but still has not materialized. Roughly, this is what needs to be done:
- Get agreement to distribute this under the simplified BSD license (which will become the SWI-Prolog license somewhere in 2016).
- Get all code conforming to the SWI-Prolog coding conventions, including PlDoc usage.
- Make sure all existing code runs (e.g., coroutining, clp(qr), CHR) and worst case performance degradation is not much more than (say) 20%
- Integrate both conceptual and reference documentation in the manual.
I'm pretty worried looking at '$wakeup'/1
. It seems to be doing a lot of expensive stuff now. Some is debugging that I assume will disappear. $module'/2
and '$set_source_module'/2
are out of the question. We don't want code to behave differently depending on the default module of the toplevel or the current compilation context. Dealing with modes using
set_something,
call_cleanup(G, reset_something)
is highly dubious. If G is nondet, the reset will not happen after G succeeds but much later if G is exhausted or its choice point is committed. Passing some global context to a goal that is nondet is hard and expensive. Can this be avoided using an additional parameter? If actual access to the context is rare another option is to store it in an argument and walk the local stack to find it if you need it.
Hope this helps and we will see a nice, lean and fast new attvar API
Cheers --- Jan
So far, I have seen a few strange things in the branch, which may be due to the issues that Jan mentioned. For example, the current HEAD behaves differently after throwing an exception:
$ swipl -g "use_module(library(clpb))" ?- sat(A+B*C), B=C, B=A. A = B, B = C, C = 1 ; false. ?- throw(e) ; throw(e). ERROR: Unhandled exception: e ?- sat(A+B*C), B=C, B=A. A = B, B = 1, sat(C=:=C) ; false.
It also differs from upstream SWI in that an unexpected choice point is left in both cases.
At this point, issue #30 also comes into play: Users who would like to help with SWI development are encouraged to write good test cases for the constraint libraries, and share them in this tracker. This way, we have a chance to implement the interface more reliably.
Yeah $wakeup/1 I still has unneeded clutter (even though it looks like i scaled back since you've posted) and debugging.. it will thin out considerably.
Even the '$module'/2
and '$set_source_module'/2
was for debugging. trying to find a sweet spot as far as "to the caller of the unification " that will be wakeup/N param.
Whew, @triska
Looks like the extra choice point problem is now cleared up, can you confirm that is for you?
#swipl -g "use_module(library(clpb))"
?- sat(A+B*C), B=C, B=A.
A = B, B = C, C = 1.
?- sat(A+B*C), B=C, B=A.
A = B, B = C, C = 1.
May have been some of the extraneous debugging code I removed.
Sample query that unexpectedly fails with the current HEAD, but worked as expected previously:
?- sat(A+B), A = B. false.
At this stage, it is always hard to tell whether the mistake is in the branch or the library. I have created a small test program for CLP(B) that never stops if the library is working correctly:
:- use_module(library(clpb)). sat(_) --> []. sat(X*Y) --> [_], sat(X), sat(Y). sat(X+Y) --> [_], sat(X), sat(Y). sat(X#Y) --> [_], sat(X), sat(Y). vs_eqs(Vs, Eqs) :- phrase(vs_eqs(Vs), Eqs). vs_eqs([]) --> []. vs_eqs([V|Vs]) --> vs_eqs_(Vs, V), vs_eqs(Vs). vs_eqs_([], _) --> []. vs_eqs_([V|Vs], X) --> vs_eqs_(Vs, X), ( [X=V] ; [] ). run :- length(Ls, N), portray_clause(N), phrase(sat(Sat), Ls), term_variables(Sat, Vs0), permutation(Vs0, Vs), vs_eqs(Vs, Eqs), findall(Vs, (sat(Sat),maplist(call, Eqs),labeling(Vs)), Sols1), findall(Vs, (labeling(Vs),maplist(call,Eqs),sat(Sat)), Sols2), ( sort(Sols1, Sols), sort(Sols2, Sols) -> true ; throw(neq-Sat-Eqs-Vs0-Vs-Sols1-Sols2) ), false.
You start it by invoking run/0
. I hope this helps you to test your changes.
The test is based on the important declarative property that labeling/1
and posting constraints are commutative, that is: If the Prolog goal G
posts any constraints among the variables Vs
(including sat/1
constraints and unifications), then labeling(Vs),G
and G,labeling(Vs)
must yield the exact same set of solutions. The critical part here are the mixed in unifications: Most errors in constraint systems are due to unexpected aliasing between logical variables, and this is unfortunately also the area in which the current SWI interface falls short.
The witness above was found by this program, since the commutativity of conjunction is violated by the current HEAD:
?- sat(A+B), A = B, labeling([A,B]). false. ?- labeling([A,B]), sat(A+B), A = B. A = B, B = 1.
Next HEAD ....
root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel# swipl -g "use_module(library(clpb))"
?- labeling([A,B]), sat(A+B), A = B.
A = B, B = 1.
?- sat(A+B), A = B, labeling([A,B]).
A = B, B = 1.
We did just bump from swipl-7.3.13 to swipl-7.3.14
(The banner though will still show the version listed below)
% Version: ............. 7.3.13-121-gb96f7f7-DIRTY
% Address bits: ........ 64
% Architecture: ........ x86_64-linux
% Installed at: ........ /usr/local/lib/swipl-7.3.14
root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel# swipl -f clpb_santytest.pl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.13-121-gb96f7f7-DIRTY)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?- run.
0.
1.
2.
3.
4.
It's working hard. Failures in a abnormal code would happen on 2
or 3
?
This looks very nice! Failures can happen at any term depth, but if it passes 3 and 4 that's definitely already a good sign. I also have many other test cases which I am currently also using to test the solvers. So far, it looks very nice! Awesome work, thank you!
I will now work on enhancements that will use the new interface more thoroughly. Notably CLP(FD) should benefit from the continuation goals.
The extra choice point problem is gone, correct?
?- G1 = sat(A#(B#C+(D#E))), G2 = labeling([A,B,C,D,E]), findall(t, (G1,G2), Ls), length(Ls, L).
G1 = sat(A# (B#C+ (D#E))),
G2 = labeling([A, B, C, D, E]),
Ls = [t, t, t, t, t, t, t, t, t|...],
L = 16.
?- G1 = sat(A#(B#C+(D#E))), G2 = labeling([A,B,C,D,E]), findall(t, (G2,G1), Ls), length(Ls, L).
G1 = sat(A# (B#C+ (D#E))),
G2 = labeling([A, B, C, D, E]),
Ls = [t, t, t, t, t, t, t, t, t|...],
L = 16.
What is the best way for me to reproduce the state? Also are you on 32 bits or 64 bits?
I am testing this on a 64-bit system. The 12/16 discrepancy was with an older version, I cannot reproduce it with the current HEAD, so please consider it fixed. The choice-point problem is gone. Thank you!
As the next example, please consider the program shower.pl
:
:- use_module(library(clpfd)). shower(S, Done) :- D = [5, 3, 8, 2, 7, 3, 9, 3], R = [1, 1, 1, 1, 1, 1, 1, 1], length(D, N), length(S, N), S ins 0..100, Done in 0..100, maplist(ready(Done), S, D), tasks(S, D, R, 1, Tasks), cumulative(Tasks, [limit(3)]), labeling([], [Done|S]). tasks([], _, _, _, []). tasks([S|Ss], [D|Ds], [R|Rs], ID0, [task(S,D,_,R,ID0)|Ts]) :- ID1 #= ID0 + 1, tasks(Ss, Ds, Rs, ID1, Ts). ready(Done, Start, Duration) :- Done #>= Start+Duration.
With upstream SWI:
?- time(shower(S, Done)). % 2,099,829 inferences, 0.275 CPU in 0.275 seconds (100% CPU, 7632861 Lips) S = [0, 0, 0, 3, 5, 8, 5, 11], Done = 14 .
In contrast, with the branch HEAD:
$ swipl -f shower.pl -O Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.13-122-g86b039c-DIRTY) Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. Please visit http://www.swi-prolog.org for details. For help, use ?- help(Topic). or ?- apropos(Word). ?- time(shower(S, Done)). [Thread 1 (main) at Tue Dec 22 22:59:28 2015] pl-wam.c:1201: TrailAssignment__LD: Assertion failed: (__PL_ld->stacks.global.top)+1 <= (__PL_ld->stacks.global.max) && (__PL_ld->stacks.trail.top)+2 <= (__PL_ld->stacks.trail.max) C-stack trace labeled "assert_fail": [0] save_backtrace() at :? [0x7f51abca3c6a] [1] __assert_fail() at ??:? [0x7f51abc6544a] [2] TrailAssignment__LD() at :? [0x7f51abbf079a] [3] appendToWakeup() at pl-attvar.c:? [0x7f51abc6e840] [4] unifyAttVar() at :? [0x7f51abc71ce6] [5] do_unify() at pl-prims.c:? [0x7f51abc3529a] [6] unify_ptrs() at :? [0x7f51abc3687b] [7] PL_next_solution() at ??:? [0x7f51abc0533f] [8] query_loop() at :? [0x7f51abc3ac0e] [9] prologToplevel() at :? [0x7f51abc3b40b] [10] PL_toplevel() at ??:? [0x7f51abbf879d] [11] swipl(main+0x2d) [0x40083d] [12] __libc_start_main() at ??:? [0x7f51ab624b45] [13] swipl(+0x881) [0x400881]
The crash depends on both the "-O" switch and using time/1
.
When I omit the time/1
call around the query, then I get (with and without "-O"):
?- shower(S, Done). (long wait without result)
Hopefully will get this fixed over the next 48 hours .. I had been doing xmas travels.. If you note any other interesting failures don't hesitate to mention
@triska OK, it should be working..
@JanWielemaker Made this patch nice and light see
SWI-Prolog/swipl-devel@master...logicmoo:treading-lightly
The CLP(B) test case above is broken with the latest changes:
?- run.
0.
ERROR: Unhandled exception: neq-_G143-[]-[_G143]-[_G143]-[]-[[1]]
I recommend you always run the tests when making changes in this branch to be more certain about its correctness.
Odd even shower/2 is failing Oops I may have been testing upstream
OK, it is back to the running state again. Luckily, I wasn't testing the upstream. The initial version was working, but I had broken it since announcement since I hadn't tested the next few commits.
?- time(shower(S, Done)).
% 5,388,802 inferences, 0.818 CPU in 0.820 seconds (100% CPU, 6587099 Lips)
S = [0, 0, 0, 3, 5, 8, 5, 11],
Done = 14 .
?- run.
0.
1.
2.
3.
4.
Awesome job Douglas, thank you a lot! I have pushed changes to your branch that document the new interface also in the user documentation.
As to performance, the following shows the performance degradation (normalized for original performance = 1, no performance = 0) of inferences and CPU time for some benchmarks:
?- comparison.
sudoku1 0.860 0.857
sudoku7 0.697 0.795
queens80 0.946 0.998
alpha_ff 0.639 0.660
knight 0.909 0.959
shower1 0.383 0.509
alpha 0.814 0.826
queens25 0.901 0.994
starpic 0.437 0.454
golf9 0.990 0.979
mhex 0.908 0.938
shower2 0.406 0.465
false.
I find this completely acceptable, taking into account the increased generality and ease of use of the new verify_attributes/3
implementation. I may also be able to improve the remaining cases by more intelligent use of the new interface.
I am probably paraphrasing what you just said: When converting code that has had development time centered around exclusively using attr_unify_hook/2
and where attr_unify_hook/2
was adequate, it will be very likely that verify_attributes/3
will add the extra time since one might end up calling get_attrs/3
. However there are many more cases that attr_unify_hook/2
would have been inadequate. So there might e a delicate balance in which hook to use in which code.
For inclusion in SWI-Prolog, I recommend you clean up the code. For example, use a DCG to collect all continuation goals, like this:
do_verify_attributes(_, Var, _ , _) --> {\+ attvar(Var), ! }.
do_verify_attributes(AttsModules, Var, att(Module, _AttVal, Rest), Value) -->
{ Module:verify_attributes(Var, Value, Goals),
'$delete'(AttsModules,Module,RemainingMods) },
list(Goals),
do_verify_attributes(RemainingMods, Var, Rest, Value).
% Call verify_attributes/3 in rest of modules
call_verify_attributes([],_Var, _Att3s, _Value) --> [].
call_verify_attributes([Module|AttsModules], Var, [], Value):-
{ Module:verify_attributes(Var, Value, Goals) },
list(Goals),
call_verify_attributes(AttsModules, Var, [], Value).
list([]) --> [].
list([L|Ls]) --> [L], list(Ls).
This way, you avoid the mess of having to deal with defaulty data structures like (Goal1,Goal2)
. Instead, it will be a clean list like [Goal1,Goal2,...]
, and you can simply use maplist(call, Goals)
to call such a list of collected goals.
Also, please do not change the continuation goals that the individual verify_attributes/3
goals produce! I.e., do not prepend different modules etc.
Any code that has had significant development time dedicated to making attr_unify_hook/2
somehow work is very likely to contain mistakes, and should also be converted to use verify_attributes/3
instead. You cannot exhaustively think about or test all cases where simultaneous unifications may be in place, so I highly recommend verify_attributes/3
in all situations. I can understand that users prefer to get wrong results over correct ones when they see a performance improvement of an order or two of magnitude (as tragic as that may be in itself). But a factor ~2 performance impact is definitely not worth yielding wrong results, even for users who care least about correctness and more about performance (as is typically the case).
We can try it the way you suggest without the modules prefixes:
The return value of verify_attributes/3 should not need a module qualification (in either case).
I started out with lists and would have liked to DCG/append them. But to actually call those residual goals they must be called from the correct modules. So for instance YAP ends up prefixing each with the Module.. It puts the module into every list element. (I didn't like that) So I thought that only creating a call structure was lighter weight.
So where maplist come into play is ..
do_resids( ( M1: List1, M2:List2 ) ):- maplist(M1:call,List1),maplist(M2:call,List2)
But for now I'll go with your suggestion.. And we may not need to use YAP's workaround.
Offhand I am not able to get working..
'$wakeup'([]).
'$wakeup'(wakeup(UnifyAtMod, Var, Att3s, Value, Rest)) :-
attributes:modules_with_attributes(AttsMods),
'$delete'(AttsMods,UnifyAtMod,RestAttsMods),!,
do_verify_attributes([UnifyAtMod|RestAttsMods], Var, Att3s, Value, Goals,[]),
(attvar(Var)->'$attvar_assign'(Var,Value);true),
call_all_attr_uhooks(Att3s, Value),
'$wakeup'(Rest),
(Goals==[]->true;maplist_for_attvar(call,Goals)).
% boot/ is too early for maplist/2?
maplist_for_attvar(C,[G]):- !, call(C,G).
maplist_for_attvar(C,[G|Gs]):- call(C,G),maplist_for_attvar(C,Gs).
%% do_verify_attributes(+AttsModules, +Var, +Att3s, +Value, -Goals) is nondet.
%
% calls Module:verify_attributes/3
%
% 1) Modules that have defined an attribute in Att3s
% 2) The caller''s module (Head of AttsModules)
% 3) remaining modules who have defined attributes on some variable (Tail of AttsModules)
%
%
do_verify_attributes(_, Var, _ , _) --> {\+ attvar(Var) },!,[].
do_verify_attributes(AttsModules, Var, att(Module, _AttVal, Rest), Value) -->
{ Module:verify_attributes(Var, Value, Goals),
'$delete'(AttsModules,Module,RemainingMods) },
list(Goals),
do_verify_attributes(RemainingMods, Var, Rest, Value).
% Call verify_attributes/3 in rest of modules
call_verify_attributes([],_Var, _Att3s, _Value) --> [].
call_verify_attributes([Module|AttsModules], Var, [], Value):-
{ Module:verify_attributes(Var, Value, Goals) },
list(Goals),
call_verify_attributes(AttsModules, Var, [], Value).
It is giving me the regressions...
?- shower(S, Done).
false.
?- run.
0.
ERROR: Unhandled exception: neq-_G513836-[]-[_G513836]-[_G513836]-[]-[[1]]
If you want to try in boot/attvar.pl I won't complain.
I have also noticed that: The strange thing is that this happens also in cases where the above code is not even run. Notice for example:
?- sat(X+Y).
false.
One thing I noticed is that call_verify_attributes//4
must also be renamed to do_verify_attributes//4
, but other than that, the very simple translation to DCGs should work as expected.
Yes, for sure the code should be the same semantically in DCG form once call_verify_attributes//4
is renamed. I didn't notice our rename, since I had already prepared myself mentally to have it a separate predicate since it didn't need the Att3s params.
(With the exception of not calling code in the same modules) this I would assumed would have been the same:
'$wakeup'([]).
'$wakeup'(wakeup(UnifyAtMod, Var, Att3s, Value, Rest)) :-
attributes:modules_with_attributes(AttsMods),
'$delete'(AttsMods,UnifyAtMod,RestAttsMods),!,
do_verify_attributes([UnifyAtMod|RestAttsMods], Var, Att3s, Value, Goals,[]),
(attvar(Var)->'$attvar_assign'(Var,Value);true),
call_all_attr_uhooks(Att3s, Value),
'$wakeup'(Rest),
(Goals==[]->true;call_list(Goals)).
call_list([G]):- !,G.
call_list([G|Gs]):- G,call_list(Gs).
%% do_verify_attributes(+AttsModules, +Var, +Att3s, +Value, -Goals) is nondet.
%Yes, for sure the code should be the same semantically in DCG form.
% calls Module:verify_attributes/3
%
% 1) Modules that have defined an attribute in Att3s
% 2) The caller''s module (Head of AttsModules)
% 3) remaining modules who have defined attributes on some variable (Tail of AttsModules)
%
%
do_verify_attributes(_, Var, _ , _) --> {\+ attvar(Var),!}.
do_verify_attributes(AttsModules, Var, att(Module, _AttVal, Rest), Value) -->
{ Module:verify_attributes(Var, Value, Goals),
'$delete'(AttsModules,Module,RemainingMods) },
list(Goals),
do_verify_attributes(RemainingMods, Var, Rest, Value).
do_verify_attributes(Mods,Var,_,Value)--> do_verify_attributes_rest(Mods,Var,Value).
% Call verify_attributes/3 in rest of modules
do_verify_attributes_rest([],_Var, _Value) --> [].
do_verify_attributes_rest([Module|AttsModules], Var, Value) -->
{ Module:verify_attributes(Var, Value, Goals) },
list(Goals),
do_verify_attributes_rest(AttsModules, Var, Value).
But it somehow it isn't .. for example shower/2
will not terminate. (Did I do something incorrect above?)
And
?- run.
0.
1.
ERROR: Unhandled exception: neq- (_G262199+_G262200)-[_G262199=_G262200]-[_G262199,_G262200]-[_G262199,_G262200]-[[1,1],[1,1],[1,1],[1,1],[1,1],[1,1],[0,0],[0,0],[0,0],[1,1],[1,1],[1,1]]-[[1,1]]
It seems the construction in list//1
is adding an unexpected layer of unification even though it is term<->term which adds a new call (leaving behind an unexpected choice point).
I almost am tempted to leave it in the working state and deffer cleanup.
But did you note in current branch there is a problem with ?- sat(X+Y).
?
Oh I did see one mistake in my code above:
do_verify_attributes(Mods,Var,_,Value)--> do_verify_attributes_rest(Mods,Var,Value).
needed to be
do_verify_attributes(Mods,Var,[],Value)--> do_verify_attributes_rest(Mods,Var,Value).
Branch is now working as DCGified
Great work, I have also pushed a patch so that the code needs less !/0
. Please do one final review and remove all superfluous !/0
,I think at least one of them can be safely removed. I will in the meantime run some checks with SICStus to find out more about the module qualification.
OK, I have now compared this with SICStus: It is clear that the SICStus interface implicitly prepends the current module to the continuation goals. I have pushed a patch that does this, please have a look. If that is the way that is also implemented in YAP, I recommend we also do it that way for compatibility, so that the module qualification is the same in SWI, SICStus and YAP.
We'll need to defer to Jan's judgement if we may use maplist/2
in the upstream. Currently during the building of boot.prc predicates such as member/2
and append/3
cannot be used etc.. that is why we are using '$member'/2
, '$append'/3
. We are getting away with maplist/2
at the moment since system code does not usually use attributes.
That's OK, maplist/2
can be easily avoided here. The point is to have a version that clearly shows the intended semantics. We definitely need Jan's final review also for the core changes, so I try to keep everything compact, pure and easy to read.
committed version with removed cuts
Files on boot
cannot use any library predicate. So, no append/3,
maplist/3, etc. Some have $-replacements. It isn't that much code, so
that shouldn't be a real problem.
I pulled the last version. Didn't compile it yet. The diff is a lot
easier to access now. Thanks. Still, multiple relatively independent
things seem to be going on that confuse me. Notably I was seeking for a
high-level description of the sinkmode stuff, so I can access the
costs and benefits. Putting pointers in global tables based on atoms
created from variable addresses make me worry a lot. It is very
expensive, has consequences for GC that I'd like to keep to the minimum
and seems dangerous. A GC changes the addresses and thus two things that
may seem different addresses may in fact be the same.
I also found the code below. I fear that can't be right. A GC or shift
will invalidate anything that is not helt in a term_t
handle. Anything
that can (indirectly) call GC/shift must either use the (slow) term_t
route, make sure there is enough space before the job is started or work
in an opportunistic fashion and when running out of space signal this to
the caller, which ultimately performs an undo back to the last safe
point, resize the stacks and try again. I think that is what
unifyAttVar() must do
+ if ( !hasGlobalSpace(0) )
+ { int rc;
+
+ if ( (rc=ensureGlobalSpace(0, ALLOW_GC)) != TRUE )
+ return raiseStackOverflow(rc);
+ }
+
+ if(normalVarUnify)
+ {
+ DEBUG_ADDRLN("\t%% NORMAL VAR UNIFY ", value);
+ Trail(value,makeRefG(av));
+ ret = TRUE;
+ goto exit;
+ }
I'm also pretty worried about the verify_attributes/3 hook in general.
The implementation seems to have |attributes|*|modules| complexity?
Possibly some of this can be taken away using a more low-level approach
to finding the module list in which to call the hooks, given the
attribute list? Aren't we after a list holding the modules associated
with the attributes, followed by the remaining attribute modules?
I think that, if we go for this, we should implement the old API on top
of this one in user space rather than putting that into the kernel.
Occurs check is one of these other things that worry me. I think this
allows for unifications to attvars to create cycles, no? Ulrich was so
happy we solved the occurs check problem elegantly ...
Sorry to be picky. I see a lot of stuff that complicates the kernel in a
way I don't really like. Global pointers to stuff on the stacks is one
of them as that is a continuous source of trouble in GC I'd like to get
rid of rather than getting more of it. We need a good motivation for all
this. I wonder whether the problems we like to solve can't be solved in
an easier way.
Cheers --- Jan
Hi Jan,
please let me clarify one high-level issue of the new attributed variable interface: About the only thing that really matters and which will be new is to have access to the variable before it is unified with anything, the rest remains unchanged. The SICStus interface solves this elegantly, using verify_attributes/3
. As an additional bonus, verify_attributes/3
allows us to elegantly specify a continuation of goals, so that local stack overflows are avoided when repeatedly triggering propagators. Thus, for compatibility, I recommend to simply do it the SICStus way. On top of this, it will also allow us to run the original CLP(Q/R) implementation with SWI-Prolog, which should solve some issues that are needed for porting cTI.
Also, regarding the occurs check, I am 100% in agreement with Ulrich, and greatly admire the way in which you have implemented this in SWI-Prolog (using true
and error
in particular via a simple global flag). Please note that also with verify_attributes/3
, the original unification will eventually be executed, just after the hook is invoked. That is the place to do everything you already have in place regarding the occurs check. The current semantics is:
- unification is desired
- unification is executed, occurs check is triggered etc.
attr_unify_hook/2
is called
With verify_attributes/3
, we will have:
- unification is desired
verify_attributes/3
is invoked- unification is executed
Note that the only thing that can change with the new hook is that you get false
instead of error
, if occurs_check
is set to error
, the unification produces an occurs check, and verify_attributes/3
fails. But even here, there is a way to work around this: If occurs_check
is indeed set to error
, you can simply tentatively perform the unification, and throw the error even before executing verify_attributes/3
.
Regarding the implementation, verify_attributes/3
should not be much more costly than attr_unify_hook/2
: Simply call the hook in just the modules where it is defined. I have no idea what SICStus are doing to lose the information about which modules are involved, but we definitely have it in place and can guarantee to call the hook only in those modules where the attributes come from. (Still, we can tell users not to rely on this, and so their code will be portable to SICStus too.)
And yes, the current API should definitely be implemented on top of this one, using a simple term expansion rule as I outlined above: For any defined attr_unify_hook/2
, a definition of verify_attributes/3
should be automatically produced which simply calls the defined attr_unify_hook/2
in the continuation goals (see the definition above), and the kernel shouldn't have to know a thing about attr_unify_hook/2
.
Note in particular that it is not possible to "escape" from identities with verify_attributes/3
: If the unification succeeds, it is the unification that was asked for, not something else.
To help clarify discussion there are actually two different branches.
FIRST BRANCH...
The one Triska and I have been working on:
git clone -b threading-ligthly https://github.com/logicmoo/swipl-devel
Diff from upstream
SWI-Prolog/swipl-devel@master...logicmoo:treading-lightly#files_bucket
It happens in C with O_VERIFY_ATTRIBUTES (~50 lines of C changes)
Which I deem ready for a more critique.
The implementation seems to have |attributes|*|modules| complexity?
|attributes|+|modules|
Current problem (more of a TODO):
Where do the modules comes from?
Perhaps maintained in attributes:modules_with_attributes/1
.
by a library/atts.pl
simular to this:
:- module('$attributes', [op(1150, fx, attribute)]).
:- multifile attributes:modules_with_attributes/1.
% :- dynamic attributes:modules_with_attributes/1.
:- dynamic existing_attribute/4.
:- dynamic attributed_module/3.
% attributes:modules_with_attributes([]).
:- meta_predicate(attributes:attribute(:)).
attributes:attribute(M:V):- '$attributes':new_attribute(V,M).
%
% defining a new attribute is just a question of establishing a
% Functor, Mod -> INT mappings
%
:- meta_predicate(new_attribute(+,+)).
new_attribute(V,M) :- var(V), !,
throw(error(instantiation_error,attribute(M:V))).
new_attribute((At1,At2),M) :- !,
new_attribute(At1,M),
new_attribute(At2,M).
new_attribute(Na/Ar,Mod) :- !,
functor(S,Na,Ar),
(existing_attribute(S,Mod,_,_) -> true;
((store_new_module(Mod,Ar,Position),
assertz(existing_attribute(S,Mod,Ar,Position))))).
new_attribute(Mod:ANY,_) :- new_attribute(ANY,Mod).
store_new_module(Mod,Ar,ArgPosition) :-
(
retract(attributes:attributed_module(Mod,Position,_))
->
true
;
retract(attributes:modules_with_attributes(Mods)),
assert(attributes:modules_with_attributes([Mod|Mods])), Position = 1
),
ArgPosition is Position+1,
( Ar == 0 -> NOfAtts is Position+1 ; NOfAtts is Position+Ar),
functor(AccessTerm,Mod,NOfAtts),
assertz(attributes:attributed_module(Mod,NOfAtts,AccessTerm)).
:-meta_predicate(put_atts(:,+)).
:-meta_predicate(get_atts(:,-)).
system:put_atts(M:Var,PosNEgAttr):-
'$attributes':put_att(Var,M,PosNEgAttr).
system:get_atts(M:Var,PosNEgAttr):-
'$attributes':get_att(Var,M,PosNEgAttr).
put_att(Var,M,PosNEgAttr):-get_attr(Var,M,Current),
do_pos_neg(Current,PosNEgAttr,NewAttr),
put_attrs(Var,M,NewAttr).
get_att(Var,M,Current):-get_attrs(Var,M,CurrentL),member(Current,CurrentL).
do_pos_neg(Current,+Attr,NewAttr):- functor(Attr,F,A),functor(AttrTemp,F,A),
ord_delete(Current,AttrTemp,Mid),!,ord_add_element(Mid,Attr,NewAttr).
do_pos_neg(Current,-Attr,NewAttr):- ord_del_element(Current,Attr,NewAttr).
do_pos_neg(Current,[Attr|More],NewAttr):-!,do_pos_neg(Current,Attr,NewAttr),
do_pos_neg(Current,More,NewAttr).
do_pos_neg(Current,Attr,NewAttr):- functor(Attr,F,A),functor(AttrTemp,F,A),
ord_del_element(Current,AttrTemp,Mid),!,ord_add_element(Mid,Attr,NewAttr).
Or an alternate strategy
moved unrelated content to to logicmoo/swipl-devel#1
moved
Note that the only thing that can change with the new hook is that you get false instead of error, if occurs_check is set to error, the unification produces an occurs check, and verify_attributes/3 fails. But even here, there is a way to work around this: If occurs_check is indeed set to error, you can simply tentatively perform the unification, and throw the error even before executing verify_attributes/3.
I believed we already had this workaround behavior. Since occurs checking is completed before any do_unify() is called.
?- put_attr(Var,test,Var),Var=val(Var).
Var = val(Var).
?- put_attr(Var,test,a),Var=val(Var).
Var = val(Var).
?- set_prolog_flag(occurs_check,error).
true.
?- put_attr(Var,test,a),Var=val(Var).
ERROR: =/2: Cannot unify _G6376 with val(_G6376): would create an infinite tree
Nope. Occurs check is implemented by unify_with_occurs_check(), which performs the unification and then checks that every binding created does not contain the bound variable by examining the trailing performed by do_unify(). That is what makes the code only check for new cycles and what makes the code correct in the presence of cycles and sharing. My fear is that delaying the binding will break correctness. I think we should implement verify_attributes/3 by first calling normal unification and afterwards undoing the bindings to attributed variables, much like this is done for unifiable/3. If we have a quick check that we must perform this past processing step, this should not affect performance much. I guess we can test whether the global stack has grown. If so, we pushed wakeup terms and if not, it was a normal unification.
I get it now, verify_attributes/3
and attr_unify_hook/2
can get exposed to a potential cyclic terms and may not be ready for it. In which case cycle checking should be before and not after. Since the consequence was:
?- set_prolog_flag(occurs_check,error).
true.
?- asserta((test:verify_attributes(Var,Value,[]):-writeln((test:verify_attributes(Var,Value))))).
true.
?- asserta((test:attr_unify_hook(Attr,Value):-writeln((test:attr_unify_hook(Attr,Value))))).
true.
?- put_attr(A,test,a), foo(A)=foo(ax(A,A)).
test:verify_attributes(_G18612,ax(_G18612,_G18612))
@(test:attr_unify_hook(a,S_1),[S_1=ax(S_1,S_1)])
ERROR: =/2: Cannot unify _G18759 with ax(_G18759,_G18759): would create an infinite tree
?- put_attr(A,test,a), foo(A,X)=foo(X,ax(A,A)).
test:verify_attributes(_G1078,ax(_G1078,_G1078))
@(test:attr_unify_hook(a,S_1),[S_1=ax(S_1,S_1)])
ERROR: =/2: Cannot unify _G1246 with ax(_G1246,_G1246): would create an infinite tree
?- put_attr(A,test,a), foo(A,Y)=foo(X,ax(A,A)),X=Y.
ERROR: =/2: Cannot unify _G2392 with ax(_G2392,_G2392): would create an infinite tree
And here is the current BUG
?- set_prolog_flag(occurs_check,true).
true.
?- put_attr(A,test,a), foo(A,X)=foo(X,ax(A,A)).
test:verify_attributes(_G4340,ax(_G4340,_G4340))
@(test:attr_unify_hook(a,S_1),[S_1=ax(S_1,S_1)])
A = X, X = ax(X, X) .
I think we should implement verify_attributes/3 by first calling normal unification and afterwards undoing the bindings to attributed variables, much like this is done for unifiable/3.
Until a couple days ago unifiable/3
's C code had me confused, but now understand it. I see how it does and undoes bindings. I think I should be able to fix in the manner in which you refer.
Just to make this explicit (Douglas has solved this very nicely already in the current branch) and to give an important reason for verify_attributes/3
: One key point is that before verify_attributes/3
is called, all bindings (of the preceding unification) must be undone.
This is because it is otherwise impossible to reason about simultaneous unifications like [X,Y] = [a,b]
, where both variables may have attributes attached, and each unification handler may require access to the attributes of the other variable. This problem (i.e., no ready access to attributes in simultaneous unifications) is a very severe deficiency of the attr_unify_hook/2
interface, and will be solved with verify_attributes/3
.
Nope. assignAttVar() no longer performs the binding. Douglas already points out this breaks the occurs check. My gut feeling tell me it probably breaks more. I don't have all the details in my head though. Most likely, some of this gets fixed if you actually perform the unification and undo this selectively somewhere before the wakeup. unifiable/3 shows how this can be done. I'm not sure this is correct in this case if multiple unifications happen before the wakeup that mutually involve cycles and sharing. I fear the best way is to do this is just before the wakeup. I'm not sure this is feasible though. the wakeup structure can maintain a reference pointer to the attvar. Restoring it is probably easy, but you also need to cancel the corresponding trail record.
If it is just about attributed variables, I'd investigate an API that actually does the binding first. After all, the '$wakeup'/1 hook contains all info for the [X,Y] = [a,b]
unifications. It just does not allow to not perform the unification. The current API works binding-by-binding and attribute-by-attribute, but I see no compelling reason why it has to or why it can't pass more of the context to the hook, neither why it can't collect the continuation goals instead of executing them immediately.
Please not that relying on [X,Y] = [a,b]
to be handled by a single wakeup is dubious. Wakeup scheduling depends on the implementation and source code rewrites such as inlining or factoring out common subgoals. It isn't that clear when wakeups need to be scheduled. The current system is rather aggressive. Semantically, I guess you can collect them longer.
We also have Paul Tarau's fluents waiting. I'm not yet sure what to think of them. The idea of making a unification have side effects without actually doing the unification itself is a bit weird to me. I guess I must read Paul's papers first.
The good news is that the treading-lightly branch is small enough to understand.
?- asserta((
test:verify_attributes(X, Value, [format('~N~q, ~n',[goal_for(Name)])]) :-
sformat(Name,'~w',X), get_attr(X, test, Attr),
format('~Nverifying: ~w = ~w (attr: ~w),~n', [X,Value,Attr]))).
true.
?- asserta((test:attr_unify_hook(Attr,Value):-format('~N~q.~n',[test:attr_unify_hook(Attr,Value)]))).
true.
?- set_prolog_flag(occurs_check,true).
true.
?- VARS = vars([X,Y,Z]), put_attr(X,test, VARS), put_attr(Y,test,VARS), put_attr(Z,test, VARS), [X,Y,Z]=[0,1,[Z,Z]].
verifying: _G570 = 0 (attr: vars([_G570,_G577,_G584])),
verifying: _G577 = 1 (attr: vars([0,_G577,_G584])),
verifying: _G584 = [_G584,_G584] (attr: vars([0,1,_G584])),
false.
?- set_prolog_flag(occurs_check,error).
true.
?- VARS = vars([X,Y,Z]), put_attr(X,test, VARS), put_attr(Y,test,VARS), put_attr(Z,test, VARS), [X,Y,Z]=[0,1,[Z,Z]].
verifying: _G570 = 0 (attr: vars([_G570,_G577,_G584])),
verifying: _G577 = 1 (attr: vars([0,_G577,_G584])),
verifying: _G584 = [_G584,_G584] (attr: vars([0,1,_G584])),
ERROR: '$attvar_assign'/4: Cannot unify _G788 with [_G788,_G788]: would create an infinite tree
?- set_prolog_flag(occurs_check,false).
true.
?- VARS = vars([X,Y,Z]), put_attr(X,test, VARS), put_attr(Y,test,VARS), put_attr(Z,test, VARS), [X,Y,Z]=[0,1,[Z,Z]].
verifying: _G67 = 0 (attr: vars([_G67,_G74,_G81])),
verifying: _G74 = 1 (attr: vars([0,_G74,_G81])),
verifying: _G81 = [_G81,_G81] (attr: vars([0,1,_G81])),
@(test:attr_unify_hook(vars([0,1,S_1]),S_1),[S_1=[S_1,S_1]]).
goal_for("_G81"),
@(test:attr_unify_hook(vars([0,1,S_1]),1),[S_1=[S_1,S_1]]).
goal_for("_G74"),
@(test:attr_unify_hook(vars([0,1,S_1]),0),[S_1=[S_1,S_1]]).
goal_for("_G67"),
VARS = vars([0, 1, _S1]), % where
_S1 = [_S1, _S1],
X = 0,
Y = 1,
Z = [_S1, _S1].
Let us talk about the order in this case (I have no opinion and am open for critique here. I don't like the order in which I did the goals vs bindings vs attr_unify_hooks but before I correct it I'd rather have a suggestion)
Please arrange the below puzzle pieces
verifying: X
verifying: Y
verifying: Z
Occurs check Z
Occurs check Y
Occurs check X
Final assign X
Final assign Y
Final assign Z
Goals X
Goals Y
Goals Z
attr_unify_hook X
attr_unify_hook Y
attr_unify_hook Z
I know Jan I diverged slightly from doing what I said I'd do.. really badly want at least one hook (verify attributes) called before occurs check.. (this means one extra level of control) I'll commit the code that
produced the output showing the occurs check working. And this below unBugged the ealier bug...
?- set_prolog_flag(occurs_check,true).
true.
?- put_attr(A,test,a), foo(A,X)=foo(X,ax(A,A)).
verifying: _G1765 = ax(_G1765,_G1765) (attr: a),
false.
?- set_prolog_flag(occurs_check,error).
true.
?- put_attr(A,test,a), foo(A,X)=foo(X,ax(A,A)).
verifying: _G1759 = ax(_G1759,_G1759) (attr: a),
ERROR: '$attvar_assign'/4: Cannot unify _G1847 with ax(_G1847,_G1847): would create an infinite tree
?- set_prolog_flag(occurs_check,false).
true.
?- put_attr(A,test,a), foo(A,X)=foo(X,ax(A,A)).
verifying: _G2905 = ax(_G2905,_G2905) (attr: a),
@(test:attr_unify_hook(a,S_1),[S_1=ax(S_1,S_1)]).
goal_for("_G2905"),
A = X, X = ax(X, X).
?-
If there is another suspected occurs_check sanity bug though give me the ?- and I'll see if i fix
As for the order I think (as Markus), that attr_unify_hook/2 must be term-expanded as
attr_unify_hook(AttValue, Binding) :- Body.
becomes
verify_attributes(Var, Value, attr_unify_hook(AttValue, Value)) :-
get_attr(Var, <module>, AttValue).
More interesting, in which modules should we call verify_attributes? Is it somehow an option to limit this to the attributes? Possibly have a multifile hook that is called afterwards? That seems both easier to manage and implies less overhead.
Possibly have a multifile hook that is called afterwards?
We'd get a great perf gain if we only called verify_attributes/3
in modules that are useful (registered into a multifile singleton)
Though I meant we'd maintain that multifile singleton based on Sicstus style calls to attribute/1, put_atts/2, get_atts/2 .. And not forced to follow the conventions set up for attr_unify_hook/2
(But still follow the current attr_unify_hook/2 methodology for attr_unify_hook/2 .. keeps us in parity with YAP )
I'm more interested in an efficient and clean interface than in compatibility as long as we can fairly easily emulate the API of other systems. Typically, the hook implementations are small and isolated.
So, if we can improve, let us go for it.
That also brings be to verify_attributes(Var, Value, Goals). Why a list of goals? Seems that the implementation simply calls this. Why is it not defined as verify_attributes(?,?,0), which would give us module qualification, cross-referencing, and all the other meta-predicate aware stuff for free instead of forcing us to define additional rules.
Why a list of goals?
I assuming some other (code besides us) also calls verify_attributes/3
verify_attributes in one module1 might aggregate the verify_attributes/3 of module2 and module3 "I verify negative prime numbers. I work by go over and glean the 3 lists out of integer_numbers, negative_numbers and prime_numbers"
Also some Goals might be duplicated or better off sorted.
verify_attributes(Var,Value,List):- get_attr(Var,datatypes,DTs),collect_verify_attributes(DTs,Value,List).
Also I am assuming attribute_goals//1 in some cases will defer to simply calling verify_attributes/3 to get the list where it has filled in the "proposed" second argument .. and Visa-versa.
Hmm ... I realised that verify_attributes/3 is not a proper meta-predicate because it returns a continuation rather than calling a closure. Whether modules calling each others verify_attributes/3 hooks is a great idea is another matter ... Anyway, as it is a return, I still have some preference for using an arbitrary body-term as return rather than a list but compatibility might be a big enough reason to go for the list anyway.
The current API works binding-by-binding and attribute-by-attribute
Please note the following important deficit of the current API: With a unification like [X,Y] = [a,b]
at the time attr_unify_hook/2
is called for X
, the other variable Y
is already bound to b
. This means specifically that the current API does not work in a way that one would call "binding-by-binding", but rather considers "all bindings at once".
Please note that relying on [X,Y] = [a,b] to be handled by a single wakeup is dubious.
Definitely! Rephrasing what I wrote above, it is in fact the single greatest inconvenience that the current API does only perform a single wakeup in cases like this. The point is to have an API where one can rely on multiple wakeups in such cases, with the other variables still unbound. Many errors in constraint systems could have been avoided if that were indeed handled "binding by binding", i.e., exactly equivalent to X = a, Y = b
, which performs the unifications and hooks individually for each variable.
In which modules should we call
verify_attributes/3
? Is it somehow an option to limit this to the attributes?
Yes, it suffices to call verify_attributes/3
in modules where attributes are attached and the hook is defined, but users should not rely on this (for compatibility with SICStus, and because this may make some optimizations possible later), and instead be prepared for the hook being called even if the variable has no attributes from that module attached.
Note that the third argument is a list of goals, so attr_unify_hook/2
can be called with:
verify_attributes(Var, Value, [attr_unify_hook(AttValue, Value)]) :-
get_attr(Var, <module>, AttValue).
We also have Paul Tarau's fluents waiting. I'm not yet sure what to think of them. The idea of making
a unification have side effects without actually doing the unification itself is a bit weird to me.
Please let us keep this further generalisation separate, and let us focus for now on compatibility with SICStus.
I still have some preference for using an arbitrary body-term
This is tempting but not a good idea, first, as you note, for compatibility, and second because it will complicate all code that has to deal with such structures. The third argument should be a list of goals, just as it is a list of goals in copy_term/3
, and also in the new hook residual_goals//0
, where we had the exact same situation.
[actually wondering whether this is the good medium for this discussion].
I made some progress trying to figure out why we should perform unification and then undo, as we already do in unifiable/3. This resulted in some interesting findings. First the not so exciting code
below. This also shows why we must not call attr_unify_hook/2 from the core because we need to define it in every module using the new interface to avoid an undefined predicate.
:- module(demo, [ demo/1]).
demo(Var) :- put_attr(Var, demo, x).
verify_attributes(Var, _Value, [hello(Var)]).
hello(Var) :- writeln(Var).
attr_unify_hook(_,_).
After adding a format statement in $wakeup/1, we get:
demo(X), X = 1.
Wakeup: wakeup(system,_G1500,att(demo,x,[]),1,[])
1
X = 1
So far, so good. But ... we only get one wakeup here.
demo(X), a(X,Y) = a(1,2).
Wakeup: wakeup(system,_G1584,att(demo,x,[]),1,[])
1
X = 1,
Y = 2.
Or this. I think this should fail right away, no? Now we get dif(X,a), a(X,X) = a(1,2)
succeeds with X=1
. I fear that the verification hook gets really complicated if unification does not already catch this.
demo(X), a(X,X) = a(1,2).
Wakeup: wakeup(system,_G1572,att(demo,x,[]),1,wakeup(system,_G1572,att(demo,x,[]),2,[]))
1
X = 1.
Thinking about this, The problem with not doing the unification is not the occurs check as I feared, but multiple unifications that take place in case of sharing. This results in multiple (duplicate) calls to the verification hooks as well as unifications that succeed where they should not.
I'm also wondering what the module in which the unification takes place has to do with the attribute verification?
On 12/28/2015 04:44 PM, Markus Triska wrote:
The current API works binding-by-binding and attribute-by-attribute
Please note the following important deficit of the current API: With a
unification like |[X,Y] = [a,b]| at the time |attr_unify_hook/2| is
called for |X|, the other variable |Y| /is already bound to |b|/. This
means specifically that the current API does /not/ work in a way that
one would call "binding-by-binding", but rather considers "all bindings
at once".Please note that relying on [X,Y] = [a,b] to be handled by a single wakeup is dubious.
Definitely! Rephrasing what I wrote above, it is in fact the single
greatest inconvenience that the current API /does/ only perform a single
wakeup in cases like this. The point is to have an API where one can
rely on /multiple/ wakeups in such cases, with the other variables still
unbound. Many errors in constraint systems could have been avoided if
that were indeed handled "binding by binding", i.e., exactly equivalent
to |X = a, Y = b|, which performs the unifications and hooks
individually for each variable.
I don't really understand all this. |[X,Y] = [a,b]| calls
attr_unify_hook/2 for each attribute on X and Y. As I understand it,
(and from inspecting the code), verify_attributes/3 is called precisely
the same number of times from the same context. Only, it can access all
attributes (would be easy to add to the old API) and, if lucky that the
two unifications are combined in one '$wakeup' and if the hook can
somehow find X from Y or the other way around, the hooks for X can
inspect the hooks for Y or the other way around. Neither is guaranteed
though, and where in the old interface |X=a,Y=b| results in the same
calling sequence, it now depends on whether or not the unification is
split and how the wakeup is scheduled.
In which modules should we call |verify_attributes/3|? Is it somehow an option to limit this to the attributes?
Yes, it suffices to call |verify_attributes/3| in modules where
attributes are attached and the hook is defined, but users should not
rely on this (for compatibility with SICStus, and because this may make
some optimizations possible later), and instead be prepared for the hook
being called even if the variable has no attributes from that module
attached.
In that case, I'm in favour of dropping modules_with_attributes/1 and
the whole stuff related to it. It would bridge most of the preformance
gap and ensure ensure unifications doesn't become dependent on some
arbitrary module adding hooks.
Note that the third argument is a /list/ of goals, so
|attr_unify_hook/2| can be called with:|verify_attributes(Var, Value, [attr_unify_hook(AttValue, Value)]) :-
get_attr(Var, , AttValue). |We also have Paul Tarau's fluents waiting. I'm not yet sure what to think of them. The idea of making a unification have side effects without actually doing the unification itself is a bit weird to me.
Please let us keep this further generalisation separate, and let us
focus for now on compatibility with SICStus.
As I said. I only care to some extend: don't break compatibility for
no reason and make sure we can support the stuff we want to.
I still have some preference for using an arbitrary body-term
This is tempting but not a good idea, first, as you note, for
compatibility, and second because it will complicate all code that has
to deal with such structures. The third argument should be a list of
goals, just as it is a list of goals in |copy_term/3|, and also in the
new hook |residual_goals//0|, where we had the exact same situation.
That convinces me. One down ...
Cheers --- Jan
[X,Y] = [a,b]
callsattr_unify_hook/2
for each attribute on X and Y.
Yes, that's true, but before that, it binds all variables at once, and calls the hooks with all bindings already in place. In short, "everything at once" instead of "binding by binding".
verify_attributes/3
is called precisely the same number of times from the same context.
Yes, also true, but it is much more finely grained: In simultaneous unifications like [X,Y,...] = [a,b,...]
, first all bindings are undone, then the hook is called for X
, then the binding for X
is done, then the hook is called for Y
, then the binding for Y
is done etc. In short, "binding-by-binding".
With attr_unify_hook/2
, all variables are bound at once, and then the hook is called for each original variable, but with everything already bound. This is a nightmare in cases where you need to access structures like binary decision diagrams which are stored in attributes of all involved variables, because it means you can no longer access these attributes of the other involved variables (which have now become ground terms after such unifications).
You note correctly that much of this could be solved if attr_unify_hook/2
were simply called "binding-by-binding", that is, single-stepping through each involved variable and performing each unification and hook step by step. But this would only solve one part of the issue, because at the time attr_unify_hook/2
is called, the variable is already bound, and we may have to deal with structures where we really need access to the variable and not only its attributes. One example: Zero-suppressed Binary Decision Diagrams. In such diagrams, a variable that does not occur in some path is implicitly 0, so you need to be able to reason about the actual variable, before and after unifications. There certainly are ways around this in some cases (store IDs in attributes etc.), but it is at least a major inconvenience.
On 12/28/2015 06:00 PM, Markus Triska wrote:
|[X,Y] = [a,b]| calls |attr_unify_hook/2| for each attribute on X and Y.
Yes, that's true, but before that, it binds all variables at once, and
calls the hooks with all bindings already in place. In short,
"everything at once" instead of "binding by binding".|verify_attributes/3| is called precisely the same number of times from the same context.
Yes, also true, but it is much more finely grained: In simultaneous
unifications like |[X,Y,...] = [a,b,...]|, first all bindings are
undone, then the hook is called for |X|, then the binding for |X| is
done, then the hook is called for |Y|, then the binding for |Y| is done
etc. In short, "binding-by-binding".
For bindings collected into a single wakeup, yes. You have little control
over the granularity of the wakeups though. Translate [X,Y] = [a,b] into
X=a, Y=b and you have no access to the attributes of the other variable,
unless I miss something very badly.
With |attr_unify_hook/2|, all variables are bound at once, and then the
hook is called for each original variable, but with everything already
bound. This is a nightmare in cases where you need to access structures
like binary decision diagrams which are stored in attributes of all
involved variables, because it means you can no longer access these
attributes of the other involved variables (which have now become ground
terms after such unifications).
Why not? The old '$wakeup'/1 can tell the hook that some other variable
that used to have these attributes was involved in the same unification.
Yes, the identity of that variable is lost. I can imagine this is important
to know. If it concerns user code though, this would mean for the user to
split or combine unifications get a different behaviour. I think that is
one of the things you dislike. It can only make sense if the multiple
unifications result from terms created and unified by your code, so you
know the unifications will happen together. Is that what is going on?
I'm not sure you cannot generally cover this case using additional
information in the attributes though.
You note correctly that much of this could be solved if
|attr_unify_hook/2| were simply called "binding-by-binding", that is,
single-stepping through each involved variable and performing each
unification and hook step by step. But this would only solve one part of
the issue, because at the time |attr_unify_hook/2| is called, the
variable is already bound, and we may have to deal with structures where
we really need access to the variable and not only its attributes. One
example: Zero-suppressed Binary Decision Diagrams. In such diagrams, a
variable that does not occur in some path is implicitly 0, so you
need to be able to reason about the actual variable, before and after
unifications. There certainly are ways around this in some cases (store
IDs in attributes etc.), but it is at least a major inconvenience.
Could you make that clear using a concrete example? That might for once
and forever settle the case.
Surely, waking attr_unify_hook/2 for each binding made during a unification
is out of the question. That would imply calling Prolog during the
unification,
which is impossible both because the terms are unsafe for GC to happen and
unify() temporary changes the data such that it is illegal Prolog data. So,
doing the unify(), undo the attvar assignments and then calling the
wakeup is
the only feasible route. It is fairly tricky though (as Douglas is
discovering)
and thus it is interesting if we can avoid it.
undo the attvar assignments and then calling the wakeup is the only feasible route. It is fairly tricky though (as Douglas is discovering)
Indeed I am :) but
?- dif(X,a), a(X,X) = a(1,2)
proves I have no other choice!
I think Markus is content with
1 Engine: First, the binding is undone.
All three of us are on the same page now.
Regarding...
|[X,Y,...] = [a,b,...]|,
might end up being...
Bind X
Bind Y
Occurs check
Unbind X
Unbind Y
verifying: X
Rebind X
verifying: Y
Rebind Y
Goals X
attr_unify_hook X
Goals Y
attr_unify_hook Y
Which sounded satisfactory to Markus as well.
Though still feel free to adjust the ordering.
For example is this prefered over the above?
Bind X
Bind Y
Occurs check
Unbind X
Unbind Y
verifying: X
verifying: Y
Rebind X
Rebind Y
Goals X
attr_unify_hook X
Goals Y
attr_unify_hook Y
I have no opinion. Markus seems to like the first option. I do think we should remove attr_unify_hook/2 from the kernel. That dictates the order through emulation using verify_attributes.
Are we deciding to run our attr_unify_hook/2
(emulated) on exactly modules we plan to have ran verify_attributes/3 ?
Here is the current way what Sicstus does: maintain cached list of N modules that have defined an attribute (at least once somewhere).
For each wakeup Run those N modules towards M:verify_attributes/3
At least a few will fallback to the system:verify_attributes/3.
How many should emulate a call to attr_unify_hook/2 with code like?
M:verify_attributes(Var,Value,[M:attr_unify_hook(Attr,Value)]):-get_attr(Var,M,Value).
If a module did in fact implement emulation. This means it will not be permitted to a use good version of M:verify_attributes/3 that can fail. (Since the failed call would be ignored anyways)
must_int:verify_attributes(Var,Value,[must_int::attr_unify_hook(Attr,Value)]):- get_attr(Var,must_int,Value).
must_int:verify_attributes(_Var,Value,[]):-integer(Value).
I have a solution but first I need to confirm the problem I describe is actually a problem.
I wanted to give confirmation to the best of my knowledge the new treading-lightly branch as far as I can seems bug free despite not yet "undoing the attvars".. I had actually had to fix the inner-arg unification bug a(MyAttVar,1) =a(X,X) this fixed the dif/2 regression in a different branch before getting involved in this issue (and forgot that I had to!). I am not sure this will put all our minds at ease.
My "opinion" about the removal of attr_unify_hook/2
We'd have to completely make sure it's removed from user's code if we expect to remove it from kernel since we can't merely "emulate" from verify_attrtibutes/3
. What Douglas?! wasn't it consensus that could easily be done? Yes, they can simply replace their attr_unify_hook/2
with a version of verify_attributes/3
.. In fact Markus has been doing that in clpfd/clpb but he is switching over things completely and doesn't expect to be using both together.
Though I and Markus both have expressed misgivings about how attr_unify_hook/2
operates in 100% of our uses. And Jan concures attr_unify_hook/2
is totally unnecessary... We are all in agreement.
I want to say it is less of a bother to support both attr_unify_hook/2
and verify_attributes/3
and a performance boost to keep both. How is it a performance boost?
- In cases
put_attr/3
put_attrs/2
is used but notput_atts/2
(currently we do not implement this but I think we should) the nonverify_attributes/3
is not needing to be searched.. but only the att/3 props. (CIAO-Prolog documentation even brags about this as a perf boost!) - Search over hooks
attr_unify_hook/2
as limited as it, is very well designed. - Search over hooks
verify_attrtibutes/3
is vague and not well defined. Even though it seems to be very clearly documented, there are lots of holes and corner cases even in Sicstus.- what order are they called in?
- Oh, so it doesn't matter? So what it we decided to do it in reverse order that Sicstus does?
- Fine it should not matter.
- If module1 and module2 have
verify_attrtibutes/3
and module1 is not visible to your calling context should you only pay attention module2? - Certainly! or Certainly not! (Well can someone find that documented somewhere?)
- Ok fine skip module1 .. wait the variable contains a module1 attribute. So Douglas this for the time of the unification that module1 should be temporarily visible
- If
verifiy_attributes/3
succeeds in module2 leaving choice points (documentation says it may) and module3 fails (thus causing redo) should that redo visit any choice points in module2? Or just choices left before the unify? - Visit module2 choices is what Sicstus does. Wait, I thought order doesn't matter, so what if I called module3 before module2?
Not saying these are problems of verifiy_attributes/3
or even problems that need fixing .. I am saying that these are undocumented decisions made by implementations. These holes are purposeful and we try to make any assumptions. But we all know implementation sometimes compared their versions to other versions sometimes to make sure their filling of the holes doesn't stray too far from others holes filling.
These decisions made about verifiy_attributes/3
will all have performance gains and losses whereas attr_unify_hook/2
is not plagued by this. verifiy_attributes/3
emulating attr_unify_hook/2
is plagued. Also to "emulate" to must make sure we call verifiy_attributes/3
in the order dictated by the att/3s (Which I had already prematurely done so we could "emulate" later). Then I was going to sort the walk thru the "rest" of the modules determined by a put_atts/2
contract like Sicstus (currently missing from SWI) in order of module inheritance. (Sicstus, CIAO, YAP all do this since it is the only sane thing to do!, but all are afraid to document this.. Sicstus even purposely lies in its documentation claiming that it doesn't do this (mainly so it can be changed later))
In order to make of "emulation" possible attr_unify_hook/2
from verifiy_attributes/3
.
I leveraged a documentation hole and I damaged verifiy_attributes/3
performance and locked us in.
So what I am making a case for is me changing verifiy_attributes/3
to not try to emulate attr_unify_hook/2
but to be optimized on its merits thus to do what YAP and CIAO does.. leave them separated.. Let people choose either (And Markus can remove the uses of attr_unify_hook/2
from core libraries but we still support it It will not cause any real extra overhead) Jan can have his first initial thought.. Let's not break anything that already uses attr_unify_hook/2
. (I looked, there is quite a bit of attr_unify_hook/2
use in user code).
One additional test case: With the program:
:- use_module(library(clpfd)).
n_fib4(0, 1).
n_fib4(1, 1).
n_fib4(N, F) :-
N #> 1, N1 #= N - 1, N2 #= N - 2,
n_fib4(N1, F1), n_fib4(N2, F2),
false.
and the current branch HEAD, I get:
?- n_fib4(N, 8).
Assertion failed: (gTop+8 <= gMax && tTop+4 <= tMax), function registerWakeup, file pl-attvar.c, line 119.
This crash does not occur with upstream.
Ahah, Confirmed, thank you, fix coming w/in the next 2 hours hopefully.
Suppose users currently define Module:attr_unify_hook/2
. I think a simple term expansion can automatically add a definition of Module:verify_attributes/3
which simply calls the already defined Module:attr_unify_hook/2
in such cases.
Nobody should use both verify_attributes/3
and attr_unify_hook/2
at the same time. I think that is a very reasonable requirement: For compatibility with hProlog and backwards compatibility with existing user code, we can in this way support attr_unify_hook/2
(via term expansion), and new code should definitely use verify_attributes/3
because it is the more general and less error-prone interface. In my view, any efficiency advantages that attr_unify_hook/2
may have pale completely in face of its drawbacks.
I have added more explanation to my initial posting, underlining the advantages of the new interface with concrete examples.
On 12/29/2015 09:46 AM, Douglas R. Miles wrote:
I wanted to give confirmation to the best of my knowledge the new
treading-lightly branch as far as I can seems bug free despite not yet
"undoing the attvars".. I had actually had to fix the inner-arg
unification bug a(MyAttVar,1) =a(X,X) this fixed the dif/2 regression in
a different branch before getting involved in this issue (and forgot
that I had to!). I am not sure this will put all our minds at ease.
Not really. Yes, you missed multiple wakeups. That is now fixed, which
causes this eventually to fail. The price is significant though. Also
calls like a(X,X) = a(1,1) will cause two wakeups rather than one. We
can of course fix that in the wakeup, but that is way more expensive
than in the unification. Given my experience with unifiable/3 and (less
immediately related) subsumption checking make me sceptical that the
current thing is even correct if we start unifying cyclic terms and
terms with weird sharing subterms. The problem we have is very close to
that of unifiable/3 and easier because we do not need to do push data
onto the stack while undoing the bindings, so we cannot run out of stack
during that process.
On 12/29/2015 10:28 AM, Douglas R. Miles wrote:
My "opinion" about the removal of |attr_unify_hook/2|
We'd have to completely make sure it's removed from user's code if we
expect to remove it from kernel since we can't merely "emulate" from
|verify_attrtibutes/3|. What Douglas?! wasn't it consensus that could
easily be done? Yes, they can simply replace their |attr_unify_hook/2|
with a version of |verify_attributes/3| .. In fact Markus has been doing
that in clpfd/clpb but he is switching over things completely and
doesn't expect to be using both together.Though I and Markus both have expressed misgivings about how
|attr_unify_hook/2| operates in 100% of /our/ uses. And Jan concures
|attr_unify_hook/2| is totally unnecessary... We are all in agreement.I want to say it is less of a bother to support both |attr_unify_hook/2|
and |verify_attributes/3| and a performance boost to keep both. How is
it a performance boost?
- In cases |put_attr/3| |put_attrs/2| is used but not |put_atts/2|
(currently we do not implement this but I think we should) the non
|verify_attributes/3| is not needing to be searched.. but only the
att/3 props. (CIAO-Prolog documentation even brags about this as a
perf boost!)- Search over hooks |attr_unify_hook/2| as limited as it, is very well
designed.- Search over hooks |verify_attrtibutes/3| is vague and not well
defined. Even though it seems to be very clearly documented, there
are lots of holes and corner cases even in Sicstus.
o what order are they called in?
o Oh, so it doesn't matter? So what it we decided to do it in
reverse order that Sicstus does?
o Fine it should not matter.
o If module1 and module2 have |verify_attrtibutes/3| and module1
is not visible to your calling context should you only pay
attention module2?
o Certainly! or Certainly not! (Well can someone find that
documented somewhere?)
o If |verifiy_attributes/2| succeeds in module2 leaving choice
points (documentation says it may) and module3 fails (thus
causing redo) should that redo visit any choice points in
module2? Or just choices left before the unify?
Reading the above and Markus comment make me suggest the following:
- Make verify_attributes/3 walk over the property list just like
it used to be. As you say, this is well documented and easy.
This means drop modules_with_attributes/1. I'd be glad for that
also because these things are hard to maintain properly in the
dynamic multi-threaded environment that SWI-Prolog is. Also
drop the notion of the module in which the unification took place.
Unification is not module sensitive! - Given the above, the emulation is perfect and thus we can use
term-expansion to generate the verify_attributes/3 wrapper for
modules having attr_unify_hook/3.
That will keep the attvar interface nice and clean at practically the
same performance (if we implement the unbinding after unification). It
it turns out we come across cases that need the hooks to be called for
modules for which there are no attached attributes, we'll consider a
plan B. I'm inclined to resist that for some time as it does a lot of
damage.
I strongly oppose against two interfaces. I know Vitor doesn't mind such
things. That is his choice. If somehow possible, I'd like to keep the
system clean and simple and push compatibility to libraries.
I agree 100% with what Jan wrote above. This is exactly the way I expect verify_attributes/3
to be implemented, called, and used to emulate attr_unify_hook/2
. The main difference in comparison with attr_unify_hook/2
is only that it happens before the unification takes place (or, equivalently, with the unification undone), and that we can place a nice continuation in the third argument. Everything else is exactly the same, in particular the modules in which the hook is called.
We can of course fix that in the wakeup,
Yep, what I ended up doing.
do_verify_attributes(_, _, Var , Value) --> {\+ attvar(Var),!}.
to
do_verify_attributes(_, _, Var , Value) --> {\+ attvar(Var),!,Var=Value}.
(I know that seemed like a off the hip workaround. I wont defend) but I bring it up for this: Why did Douglas have a clause like
do_verify_attributes(_, _, Var , Value) --> {\+ attvar(Var),!}.
In the first place?!
This was to "skip verify_attributes/3
for when/2
freeze/2
callbacks.
Well wakeup/1 must be called with the attvar already bound :)
For the when/2
to work this means we'll need to port the when/2
freeze/2
infrastructure to no longer using attr_unify_hook/2
pre-call system.
I agree 100% with what Jan wrote above. This is exactly the way I expect verify_attributes/3 to be implemented, called, and used to emulate attr_unify_hook/2. The main difference in comparison with attr_unify_hook/2 is only that it happens before the unification takes place (or, equivalently, with the unification undone), and that we can place a nice continuation in the third argument. Everything else is exactly the same, in particular the modules in which the hook is called.
We also need to reimplement when/2
freeze/2
if we are typing to avoid that infrastructure
Which I am all for .. just need to define them based off verify_attributes/3
instead
Which actually is more sustainable and give us more power with when/2
verify_attributes(Var,Value,[ping_when(Var,Value,Attr)]):-get_attr(Var,'$when',Attr).
What my last two comments are about is this... We are much saner in my opinion having more than one style of $wakeup/1 goals we need 3 and at minimum 2. (My old old code used all 3 + Generalized Goal passed from kernel)
This means drop modules_with_attributes/1. I'd be glad for that also because these things are hard to maintain properly in the dynamic multi-threaded environment that SWI-Prolog is.
If it turns out we come across cases that need the hooks to be called for
modules for which there are no attached attributes
I think Markus is looking to be compatible with SICStus (Plan B) which means we must call ALL modules that have defined attributes even ones not on the variable itself.
https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus.html/lib_002datts.html#lib_002datts says..
"This predicate is called whenever a variable Var that might have attributes in Module is about to be bound to Value (it might have none). The unification resumes after the call to verify_attributes/3. Value is a non-variable term, or another attributed variable. Var might have no attributes present in Module; the unification extension mechanism is not sophisticated enough to filter out exactly the variables that are relevant for Module." (That is what I meant above as vague .. since even it leaves out information about threads and call order and non exported verify_attributes/3
etc)
My atts.pl in the comments way way avoid shows how Yap maintained modules_with_attributes/1
for SICStus compatibility layer
Also drop the notion of the module in which the unification took place. Unification is not module sensitive!
If one traces clpb's and clpfd's use of unification it is usually in a special odd module like clpfd
. I know 99% of what Jan saw seemed to originate from system
=/2. In most all my 80% of Douglas' cases the unification hooks were calling predicates only in my test module. Jan is still correct here.. I can drop the module from wakeup/N
since most (all) of the time the callbacks happen so close to the initial call the module hasn't switched yet. Why it was there in the first place? I was thinking "not sophisticated enough" clause in SICStus docs can be slightly improved on .. We have a Closure of available modules from any context for example how default_module/2
works that rather than calling every possible module. Also cases in pengines where modules can be renamed for isolation it be sanest to follow that same pattern.