[m-dev.] choicepoint id bug

[Julien Fischer]

Hi,

The following concerns the bug reported on mercury-users recently.  Could 
someone please check my reasoning here.

Julien.

-----------

The following program is a simplified version of the one Peter Biener posted
on mercury-users (it identical in most respects except that the predicate
foo/3 takes the place of io.print/3).

     main(!IO):-
         foo("a", !IO),
         write_current_choicepoint_id("b1", !IO),
         foo("a2", !IO),
         write_current_choicepoint_id("b2", !IO),
         foo("a3", !IO),
         write_current_choicepoint_id("b3", !IO).

     :- pred write_current_choicepoint_id(string::in, io::di, io::uo) is det.
     :- pragma foreign_proc("C", write_current_choicepoint_id(Key::in,
             IO0::di, IO::uo),
         [promise_pure, will_not_call_mercury],
     "
         printf(\"%s: %ld\\n\", Key, (long)MR_current_choicepoint_id());
         IO = IO0;
     ").

     :- pred foo(T::in, io::di, io::uo) is det.

     foo(Thing, !IO) :-
         ( if   dynamic_cast(Thing, String : string)
           then io.write_string(String ++ "\n", !IO)
           else io.write_string("Not a string\n", !IO)
         ).

When compiled in hlc.gc.trseg and run the program outputs:

         a
         b1: 1
         a2
         b2: 2
         a3
         b3: 3

This doesn't seems to agree with the behaviour described in
compiler/notes/trailing.html which says that one of the invariants for
MR_ticket_counter (i.e. the current choicepoint id), is that:

     any call to a model_det goal will leave it unchanged (MR_ticket_counter may
     change during the execution of the goal, but its value when the goal exits
     will be the same as the value it had when the goal was entered, because the
     goal must prune away any tickets that it allocates)

This is obviously not happening above!

The following is HLDS dump of foo/3 (stage 410, with any type-info related
stuff removed for clarity).

     cptest.foo(Thing, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
         impure private_builtin.store_ticket(TrailTicket),
         (if
             builtin.dynamic_cast(Thing, String)
          then
            impure private_builtin.reset_ticket_commit(TrailTicket),
            impure private_builtin.prune_ticket,
            V_12 = "\n",
            V_11 = string.(String ++ V_12),
            io.write_string(V_11, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO)
          else
            impure private_builtin.reset_ticket_undo(TrailTicket),
            impure private_builtin.discard_ticket,
            V_14 = "Not a string\n",
            io.write_string(V_14, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO)
        ).

The macro store_ticket/1 sets the value of MR_ticket_counter by
assigning it the next value of MR_ticket_high_water, i.e.

      MR_ticket_counter = ++MR_ticket_high_water;

The problem is that prune_ticket/0 and discard_ticket/0 "reset"
the value of MR_ticket_counter by decrementing it.  If, as here, you get
a sequence of goals containing semidet if-then-else conditions that succeed
then MR_ticket_high_water keeps growing and decrementing MR_ticket_counter
afer setting it to that value is not enough to reset it.

In short, the code for foo/3 ought to  be something like the following:

     cptest.foo(Thing, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO) :-
         impure private_builtin.store_ticket(TrailTicket),
         impure private_buitin.mark_ticket_stack(SavedTicketCounter),
         (if
             builtin.dynamic_cast(Thing, String)
          then
            impure private_builtin.reset_ticket_commit(TrailTicket),
            impure private_builtin.prune_tickets_to(SavedTicketCounter)
            V_12 = "\n",
            V_11 = string.(String ++ V_12),
            io.write_string(V_11, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO)
          else
            impure private_builtin.reset_ticket_undo(TrailTicket),
            impure private_builtin.discard_ticket_to(SavedTicketCounter) **
            V_14 = "Not a string\n",
            io.write_string(V_14, STATE_VARIABLE_IO_0, STATE_VARIABLE_IO)
        ).

** this doesn't actually exist in private_builtin.m (yet).



--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------