[m-dev.] More trailing bugs. :-)

[Fergus Henderson]

On 28-Jan-2000, Warwick Harvey <wharvey at cs.monash.edu.au> wrote:
> Zoltan wrote:
> > There is no question of right and wrong here. The value of the ticket counter
> > at a given point in the program will be different with different trace levels,
> > but Mercury code is not supposed to depend on that; as long as the C code the
> > compiler emits obey the semantics of the trailing operations, it should be
> > all right.
> 
> OK, I'm going to stick my neck out again, and claim that the C code the 
> compiler emits does *not* obey the semantics of the trailing operations.  :-)

I think the problem that you have spotted is very real.
However, I would describe it slightly differently: the C code that the
compiler emits does obey the semantics of the trailing operations,
it's just that those semantics do not have the implications that we
thought they did.  And yes, this does cause serious problems.

> My understanding of how the trailing operations should work, is that during 
> forward execution, the ticket counter should never decrease.

This is not the case.

The documentation for MR_ticket_counter describes it as

** An integer variable that is incremented whenever we create a choice
** point (including semidet choice points, e.g. in an if-then-else)
** and decremented whenever we remove one.

Clearly failure is one way of removing choice points, but
they can also be pruned away, as is the case for the choice
points created by if-then-elses.

Likewise the documentation for MR_current_choicepoint says

	`MR_current_choicepoint_id()' returns a value indicating the
	identity of the most recent choice point; that is, the point to
	which execution would backtrack if the current computation failed.

and clearly after a choice point has been pruned away, then it can no
longer be the point to which execution would backtrack if the current
computation failed.

> This is not 
> what happens currently, since (when tracing) at the end of a det or semidet 
> procedure, the ticket allocated to allow retry is discarded, and the counter 
> decremented.  This means the counter in subsequent code can be smaller than 
> it was during the det or semidet code.

Right.

> OK, so why is this a problem?  [...]
> the point of the ticket counter is to allow redundant trailing to be 
> avoided.  According to the manual (and the feature is useless if this isn't 
> true), one can save the current value of the ticket counter (called the 
> current choicepoint ID at the user level), and if it's the same next time 
> you do an update, you don't need to trail.  So suppose an update occurs 
> inside a (semi)deterministic piece of code, and the value of the ticket 
> counter is saved.  Upon exit of that code (and perhaps several of its 
> ancestors), the ticket counter is decremented.  A nondet predicate is then 
> called, and a new (real) choice point is allocated, incrementing the ticket 
> counter.  Another update is performed, and (assuming appropriate relative 
> nesting levels) the ticket counter matches the saved value, no trailing is 
> performed, and upon backtracking to this new choice point, the variable has 
> the wrong value.

Yes, that is indeed a problem.
That section of the manual is incorrect.

I think it may be possible to salvage some usefulness for the feature,
though.

> Come to think of it, isn't this also an issue for commits in all (trailing) 
> grades?

Yes.

> If I understand correctly, if a nondet predicate is called in the 
> condition of an if-then-else and it succeeds, then ticket counter is reset 
> to its value before the call ---

Actually that only happens for semidet conditions, I think;
for nondet conditions, the condition of the if-the-else may itself
have allocated tickets, so we can't reset the ticket counter
when we reach the `then' part.

> but its value may have been stored during 
> the call to avoid redundant trailing, which means you have data structures 
> out there that think they were last updated in a future choice point.  Yick!

One way to avoid this would be to use a function trail entry,
and to have that function trail entry reset itself whenever it
gets a `MR_commit' callback.

That still doesn't solve the problem in debugging grades,
because the debugging code does not call MR_reset_ticket(..., MR_commit)
before calling MR_discard_ticket().  And indeed MR_commit has other
semantics that are not appropriate in this situation.  So we'd
need to invent another MR_untrail_reason.

Also it means that if you want to avoid redundant trailing,
then you need to use the function trail rather than the value
trail, which is a pity, because the function trail is a bit more
expensive.


But the other alternative -- changing the semantics of the trail operations
so that the ticket counter never gets decremented during forward execution,
which I think is what Warwick was suggesting -- would have significant problems.
In particular, any call to a det procedure which happens to execute an
if-then-else in it would result in the ticket counter being incremented.
This would essentially cripple the effectiveness of using the ticket counter
to avoid redundant trailing.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------