[m-dev.] diff: more trailing changes

[Peter Schachte]

On Sun, 24 Aug 1997, Fergus Henderson wrote:

> There is still a problem: when committing over a goal that
> has created multiple choice points, we only have one call
> `MR_reset_ticket(ticket, MR_commit); MR_discard(ticket)'.
> I don't see any easy way of making DJ's invariant -- namely the
> invariant that we call MR_discard() for every ticket that we
> create with MR_store_ticket() -- hold.  This means that
> the computed values of MR_ticket_counter will be incorrect,
> because it will not be properly restored after a commit.

In such cases I guess it will be necessary to save away the ticket counter
so it can be restored on commitment.

But note that there is no argument to MR_discard_ticket(), and that there
needn't be a call to MR_reset_ticket(old, MR_commit) corresponding to every
call to MR_store_ticket() or MR_discard_ticket().  As long as all paths
through the code call MR_discard_ticket() once for each call to
MR_store_ticket() and there is a call to MR_reset_ticket() with appropriate
reason for each sequence of contiguous choices that are unwound for the same
reason.  Eg, you can call MR_reset_ticket() once to cover committing to two
sequential choices each with its own call to MR_store_ticket(), as long as
you call MR_discard_ticket() twice. 

You might even want to have a MR_discard_tickets(n) macro that decrements
the ticket counter by the specified number.


-Peter Schachte      URL:  http://www.cs.mu.oz.au/~pets/
pets at cs.mu.OZ.AU     PGP:  finger pets at 128.250.37.150 for key
    Do insects spend hours demammaling their programs?