20.5.5 Avoiding redundant trailing

If a mutable data structure is updated multiple times, and each update is recorded on the trail using the functions described above, then some of this trailing may be redundant. It is generally not necessary to record enough information to recover the original state of the data structure for every update on the trail; instead, it is enough to record the original state of each updated data structure just once for each choice point occurring after the data structure is allocated, rather than once for each update.

The functions described below provide a means to avoid redundant trailing.

• MR_ChoicepointId

Declaration:

typedef … MR_ChoicepointId;

The type MR_ChoicepointId is an abstract type used to hold the identity of a choice point. Values of this type can be compared using C’s ‘==’ operator or using ‘MR_choicepoint_newer()’.

• MR_current_choicepoint_id()

Prototype:

MR_ChoicepointId MR_current_choicepoint_id(void);

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. The value remains meaningful if the choicepoint is pruned away by a commit, but is not meaningful after backtracking past the point where the choicepoint was created (since choicepoint ids may be reused after backtracking).

• MR_null_choicepoint_id()

Prototype:

MR_ChoicepointId MR_null_choicepoint_id(void);

MR_null_choicepoint_id() returns a “null” value that is distinct from any value ever returned by MR_current_choicepoint_id. (Note that MR_null_choicepoint_id() is a macro that is guaranteed to be suitable for use as a static initializer, so that it can for example be used to provide the initial value of a C global variable.)

• MR_choicepoint_newer()

Prototype:

bool MR_choicepoint_newer(MR_ChoicepointId, MR_ChoicepointId);

MR_choicepoint_newer(x, y) true iff the choicepoint indicated by x is newer than (i.e. was created more recently than) the choicepoint indicated by y. The null ChoicepointId is considered older than any non-null ChoicepointId. If either of the choice points have been backtracked over, the behaviour is undefined.

The way these functions are generally used is as follows. When you create a mutable data structure, you should call MR_current_choicepoint_id() and save the value it returns as a ‘prev_choicepoint’ field in your data structure. When you are about to modify your mutable data structure, you can then call MR_current_choicepoint_id() again and compare the result from that call with the value saved in the ‘prev_choicepoint’ field in the data structure using MR_choicepoint_newer(). If the current choicepoint is newer, then you must trail the update, and update the ‘prev_choicepoint’ field with the new value; furthermore, you must also take care that on backtracking the previous value of the ‘prev_choicepoint’ field in your data structure is restored to its previous value, by trailing that update too. But if MR_current_choice_id() is not newer than the prev_choicepoint field, then you can safely perform the update to your data structure without trailing it.

If your mutable data structure is a C global variable, then you can use MR_null_choicepoint_id() for the initial value of the ‘prev_choicepoint’ field. If on the other hand your mutable data structure is created by a predicate or function that uses tabled evaluation (see Tabled evaluation), then you should use MR_null_choicepoint_id() for the initial value of the field. Doing so will ensure that the data will be reset to its initial value if execution backtracks to a point before the mutable data structure was created, which is important because this copy of the mutable data structure will be tabled and will therefore be produced again if later execution attempts to create another instance of it.

For an example of avoiding redundant trailing, see the sample module below.

Note that there is a cost to this — you have to include an extra field in your data structure for each part of the data structure which you might update, you need to perform a test for each update to decide whether or not to trail it, and if you do need to trail the update, then you have an extra field that you need to trail. Whether or not the benefits from avoiding redundant trailing outweigh these costs will depend on your application.

:- module trailing_example.
:- interface.

:- type int_ref.

    % Create a new int_ref with the specified value.
    %
:- pred new_int_ref(int_ref::uo, int::in) is det.

    % update_int_ref(Ref0, Ref, OldVal, NewVal).
    % Ref0 has value OldVal and Ref has value NewVal.
    %
:- pred update_int_ref(int_ref::mdi, int_ref::muo, int::out, int::in)
    is det.

:- implementation.

:- pragma foreign_decl("C", "

typedef struct {
    MR_ChoicepointId prev_choicepoint;
    MR_Integer data;
} C_IntRef;

").

:- pragma foreign_type("C", int_ref, "C_IntRef *").

:- pragma foreign_proc("C",
    new_int_ref(Ref::uo, Value::in),
    [will_not_call_mercury, promise_pure],
"
    C_Intref *x = malloc(sizeof(C_IntRef));
    x->prev_choicepoint = MR_current_choicepoint_id();
    x->data = Value;
    Ref = x;
").

:- pragma foreign_proc("C",
    update_int_ref(Ref0::mdi, Ref::muo, OldValue::out, NewValue::in),
    [will_not_call_mercury, promise_pure],
"
    C_IntRef *x = Ref0;
    OldValue = x->data;

    /* Check whether we need to trail this update. */
    if (MR_choicepoint_newer(MR_current_choicepoint_id(),
        x->prev_choicepoint))
    {
        /*
        ** Trail both x->data and x->prev_choicepoint,
        ** since we're about to update them both.
        */
        assert(sizeof(x->data) == sizeof(MR_Word));
        assert(sizeof(x->prev_choicepoint) == sizeof(MR_Word));
        MR_trail_current_value((MR_Word *)&x->data);
        MR_trail_current_value((MR_Word *)&x->prev_choicepoint);

        /*
        ** Update x->prev_choicepoint to indicate that
        ** x->data's previous value has been trailed
        ** at this choice point.
        */
        x->prev_choicepoint = MR_current_choicepoint_id();
    }
    x->data = NewValue;
    Ref = Ref0;
").