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

[Warwick Harvey]

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.  :-)

My understanding of how the trailing operations should work, is that during 
forward execution, the ticket counter should never decrease.  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.

OK, so why is this a problem?  It took me a while to figure this one out, 
since entries in the trail having non-sequential ticket numbers didn't seem 
to pose an immediate, direct problem, since those ticket numbers aren't used 
to decide how far the trail should be rolled back; that's what the trail 
pointer is for.

Anyway, 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.


Come to think of it, isn't this also an issue for commits in all (trailing) 
grades?  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 --- 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!

Warwick

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------