Inconsistent variable sharing behavior of attribute_goals when called from frozen/2 vs. copy_term/3

[dgelessus]

I ran into this while looking into #818. attribute_goals//1 is called from both frozen/2 and copy_term/3, but with one small difference: frozen/2 passes the attvar in question directly to attribute_goals//1, whereas copy_term/3 passes in a copy of the attvar (as if created by copy_term/2).

This difference is relevant if attribute_goals//1 modifies the attvar's attributes in any way, either by putting/removing attributes or by binding variables inside existing attributes. If such an attribute_goals//1 implementation is called from copy_term/3, these changes have no lasting effect, because the received attvar and its attributes are freshly copied, and all attributes are deleted from the copied variable before copy_term/3 returns. On the other hand, if attribute_goals//1 is called from frozen/2, it receives the real variable, so any changes to the attributes remain in place and are not undone when frozen/2 returns.

Here's a contrived example. Every time this attribute_goals//1 is called, it adds an extra s(X) compound around the attribute value.

blah:attribute_goals(Var) -->
  {get_attr(Var, blah, Attr)},
  [put_attr(Var, blah, Attr)],
  {put_attr(Var, blah, s(Attr))}.

If you use this with copy_term/3, the modifications to the attribute are not visible externally (every goal shows a copy of the original attr(Attr) value):

?- put_attr(Var, blah, attr(Attr)), copy_term(Var, VarCopy, VarGoals).
VarGoals = [put_attr(VarCopy, blah, attr(_13494))],
put_attr(Var, blah, attr(Attr)).

?- put_attr(Var, blah, attr(Attr)), copy_term(Var, VarCopy, VarGoals), copy_term(Var, VarCopy2, VarGoals2).
VarGoals = [put_attr(VarCopy, blah, attr(_18552))],
VarGoals2 = [put_attr(VarCopy2, blah, attr(_18594))],
put_attr(Var, blah, attr(Attr)).

But with frozen/2, the modifications are permanent (every goal shows one more s in the attribute than the previous goal):

?- put_attr(Var, blah, attr(Attr)), frozen(Var, VarGoal).
VarGoal = put_attr(Var, blah, attr(Attr)),
put_attr(Var, blah, s(attr(Attr))).

?- put_attr(Var, blah, attr(Attr)), frozen(Var, VarGoal), frozen(Var, VarGoal2).
VarGoal = put_attr(Var, blah, attr(Attr)),
VarGoal2 = put_attr(Var, blah, s(attr(Attr))),
put_attr(Var, blah, s(s(attr(Attr)))).

The documentation for attribute_goals//1 isn't very clear about this, but it says "Its argument is that variable.", which implies that the received variable should always be the original variable and not a temporary copy. I don't have any strong opinions about which behavior is better, but IMO either there should be a consistent documented behavior, or the documentation should explicitly say that the exact behavior is undefined and that attribute_goals//1 shouldn't modify attributes.

FWIW, on SICStus (tested with version 4.5.1) the equivalent hook predicate attribute_goal/2 always receives the original variable and never a copy. But the SICStus documentation also doesn't explicitly say anything about this behavior or about modifying attributes inside attribute_goal/2.

[JanWielemaker]

Thanks for the observations. attribute_goals//1 was introduced for copy_term/3. More recently frozen/2 was changed from just dealing with freeze/2 to be generic, compatible with SICStus. Here we cannot copy as we would get copies of the variables. I'm not that deep into these issues, but I think this implies that attribute_goals//1 should be documented to (possibly) receive the original variable and (thus) is not allowed to modify attributes. I guess that implies when/2 is broken when combined with frozen/2 (at least for disjunctions).

I propose we wait with documenting these things until this is resolved.

[dgelessus]

Apparently there are multiple parts of SWI's builtins/standard library that expect attribute_goals//1 to receive a copy of the variable and that modifications are not permanent, which causes problems with frozen/2. I've already documented the problem with when in #818 (comment). Something similar happens with CLPFD as well - calling frozen on a CLPFD variable modifies its attributes in a way that causes errors when it's bound later:

[debug]  ?- Y #= X + 1, X = 3.
Y = 4,
X = 3.

[debug]  ?- Y #= X + 1, frozen([X, Y], Frozen), X = 3.
ERROR: Uninstantiated argument expected, found processed (1-st argument)
ERROR: In:
ERROR:   [19] put_attr(processed,clpfd_aux,queued)
ERROR:   [18] clpfd:trigger_prop(propagator(pplus(3,1,_69498),processed)) at <builddir>/home/library/clp/clpfd.pl:3890
ERROR:   [17] clpfd:trigger_props_([propagator(...,processed)]) at <builddir>/home/library/clp/clpfd.pl:3888
ERROR:   [16] clpfd:trigger_props(fd_props([],[...],[])) at <builddir>/home/library/clp/clpfd.pl:3884
ERROR:   [15] clpfd:attr_unify_hook(clpfd_attr(no,no,no,from_to(inf,sup),fd_props([],...,[])),3) at <builddir>/home/library/clp/clpfd.pl:7266
ERROR:   [14] uhook(clpfd,clpfd_attr(no,no,no,from_to(inf,sup),fd_props([],...,[])),3) at <builddir>/home/boot/attvar.pl:86
ERROR:   [13] call_all_attr_uhooks(att(clpfd,clpfd_attr(no,no,no,...,...),[]),3) at <builddir>/home/boot/attvar.pl:63
ERROR:   [12] '$wakeup'(wakeup(att(clpfd,...,[]),3,[])) at <builddir>/home/boot/attvar.pl:58
ERROR:   [11] 3=3 <foreign>
ERROR:   [10] '<meta-call>'(user:user: ...) <foreign>
ERROR:    [9] toplevel_call(user:user: ...) at <builddir>/home/boot/toplevel.pl:1115
   Exception: (11) _67342{clpfd = ...}=3 ? 

And dif also has some strange behavior with frozen. Calling frozen on difed variables doesn't break the dif itself (or at least I can't find any case where it does), but it does break future frozen (or copy_term/3) calls on the same variables:

?- dif(X, Y), frozen([X, Y], Frozen), frozen([X, Y], Frozen2), copy_term([X, Y], _, AttrGoals).
Frozen = dif(X, Y),
Frozen2 = true,
AttrGoals = [].

(The correct result would be that Frozen2 and AttrGoals also contain a dif goal.)

Considering that (as you explained above) frozen/2 has to pass the original variable into attribute_goals and not a copy, the only real way to fix these problems is to rewrite the attribute_goals in question so that they don't modify the variable. But with that restriction, I'm not sure how the current behavior can be maintained where e. g. dif(X, Y), frozen([X, Y], Frozen) returns only one dif(X, Y) goal and not two. That would require some other way to keep temporary state that is shared across multiple attribute_goals calls, but scoped to a single frozen/copy_term call.

The alternative would be to switch to a different goal representation that can be rendered correctly without keeping state across attribute_goals calls, but such a goal representation would no longer match the original predicate calls and would be a lot less readable in general.

[JanWielemaker]

😢 I'm afraid you are right. As by its original design attribute_goals//1 was only designed to support copy_term/3 it was anticipated that rules could modify the attributes. If I understand correctly SICStus also uses attribute_goals//1 both for copy_term/3 and frozen/2 and does not allow the rules to modify the attributes, right?

If the above observation is correct the ideal way would be to follow this design. I'm afraid that will get nasty though and might require changing the internal constraints representation for some of the constraint libraries.

I pushed 52274a5 which I think is a sensible (at least short term) solution that restores (I think) correctness. At least it passes the tests, the clpfd example and the diff example (both added to the tests). Please have a look.

[dgelessus]

If I understand correctly SICStus also uses attribute_goals//1 both for copy_term/3 and frozen/2 and does not allow the rules to modify the attributes, right?

Right - on SICStus, attribute_goal always receives the original variable and not a copy, no matter if it's called from copy_term or frozen. You can modify the variable in attribute_goal and those modifications will affect the real variable, but I don't think there's any practical use for this, and the SICStus documentation doesn't mention it.

If the above observation is correct the ideal way would be to follow this design.

I agree that it would be better to always pass the original variable, once that's possible without breaking SWI's libraries. That way if an attribute_goals does modify the variable, the behavior is consistent between frozen and copy_term.

I'm afraid that will get nasty though and might require changing the internal constraints representation for some of the constraint libraries.

For reference, here's how some of SICStus' goal representations look. Since SICStus attribute_goal never allowed passing state, the goal representations are usually less detailed/pretty compared to SWI. For example, for CLPFD variables SICStus only displays each variable's domain and no other constraints, and for when it displays its internal attributes/goals directly without trying to format them nicely.

| ?- X in 1..10, Y in 1..10, Y #= X + 1.
X in 1..9,
Y in 2..10 ? ;
no
| ?- when((ground(X) ; ground(Y)), Whened = true).
prolog:trig_ground(X,[],[X],_A,_B),
prolog:trig_ground(Y,[],[Y],_A,_C),
prolog:trig_or([_B,_C],_A,_A),
prolog:when(_A,(ground(X);ground(Y)),user:(Whened=true)) ? ;
no

SWI could do something similar, but it would be a shame to lose the higher-quality output, and it might break SWI-specific code that depends on e. g. looking for CLPFD constraints in the goals. Would it make any sense to add a variant of attribute_goals with extra parameters for passing temporary state without modifying the actual variable?

I pushed 52274a5 which I think is a sensible (at least short term) solution that restores (I think) correctness. At least it passes the tests, the clpfd example and the diff example (both added to the tests). Please have a look.

Yes, this seems to fix all the problems with frozen modifying attributes, thank you! Sadly with the new frozen code our test suite is now showing lots of errors about extra residual variables (many of our tests run with call_residue_vars and check that there are no unexpected residual variables). I haven't figured out yet what exactly is going on here - perhaps the problem isn't on the SWI side, but somewhere in our code or in my local WIP version of the SICStus emulation modules. I'll let you know once I've debugged this futher.

[JanWielemaker]

Just for the record, copy_term/3 also passes the original variables. It uses findall/3 to get a copy of the derived term and goal and as findall/3 backtracks the changes by attribute_goal//1 are reverted.

I think when with disjunctions still leaves residual variables, no? I think we can close this one. Please reopen should that be needed.

[dgelessus]

Alright, I've figured out where the unexpected residual variables are coming from, and it is indeed caused by the changes in 52274a5. It happens when backtracking past a frozen call. Here's the expected behavior, before the change:

?- call_residue_vars((X in 1..2, frozen(X, FX) ; true), Vars).
FX = clpfd:(X in 1..2),
Vars = [X],
X in 1..2 ;
Vars = [].

?- call_residue_vars((X in 1..2, (frozen(X, FX) ; true)), Vars).
FX = clpfd:(X in 1..2),
Vars = [X],
X in 1..2 ;
Vars = [X],
X in 1..2.

And here's the incorrect behavior after the change, where backtracking past frozen leaves a copy of X as an extra residual variable:

?- call_residue_vars((X in 1..2, frozen(X, FX) ; true), Vars).
FX = clpfd:(X in 1..2),
Vars = [X],
X in 1..2 ;
Vars = [_9660],
_9660 in 1..2.

?- call_residue_vars((X in 1..2, (frozen(X, FX) ; true)), Vars).
FX = clpfd:(X in 1..2),
Vars = [X],
X in 1..2 ;
Vars = [_19150, X],
X in 1..2,
_19150 in 1..2.

I'm guessing this comes from the nb_setarg in the new frozen implementation, which will persist even if the entire frozen call is backtracked.

[JanWielemaker]

I see. Pushed c536f79 to handle this, using findall/3 rather than nb_setarg/3. The duplicated term indeed contains residual variables. Under normal execution this is not a problems as GC will take care of the term rather than backtracking. call_residue_vars/2 blocks GC for resitual vars though, so it is left. findall/3 also copies the term, but off the stacks and back onto the stacks rather than using the frozen bar mechanism that supports non-backtrackable data on the stacks. Now backtracking can simply discard the copy. Tricky stuff 😢

Please give it a try. Should be functionally equivalent. At least the tests still pass. If you do more testing, please create a PR with them (they are in src/Tests/core/test_coroutining.pl)

[dgelessus]

This seems to have fixed the problem with the residual variables, thank you! Our unit tests are much happier now too 🙂

Yes, I've been meaning to write down my one-off test calls as proper plunit tests, but haven't gotten around to it yet... Once I do, I'll send a PR with the relevant ones.