RE: [abc] J-LO benchmark results

>> ref. The same does not hold true for tracematches. Also, for
>> tracematches there is a potential problem of disjuncts
>> leaking. Why does that not happen in JLO, do you know?
>
> Hmm, to be honest I do not see why it exists in the TM implementation.
> In J-LO all the data is held within the formulae. So whenever we do a
> transition, we take the formula and build it's successor formula under
> the given input propositions. At this time, whenever we evaluate a
> proposition held in the formula which in the meantime lost a binding
> (the proposition has an internal counter to identify this), we evaluate
> this proposition to "False", which means that it is on the one hand
> semantically correct and on the other hand leads to elimination of the
> proposition due to the way the successor formula is built (because
> "False" AND "something" is "False" and "False" OR "something" is
> "something"). Does that make sense?

I think the set of disjuncts in the tm roughly correspond to the
way you manipulate formulae. However, I don't see that the
strategy you describe above is correct.

Consider the pattern

    sym s1 before : call(* foo(..)) && target(x);
    sym s2 before : call(* bar(..)) && target(y);

    s1 s2

now we could have the following trace:

    o1.foo(); // bind x = o1
    <gc o1> // nullify weak ref x
    o2.bar(); // bind y = o2

What you seem to describe is that the partial match with x=o1
gets thrown out when x is nullified; and that would mean the
pattern as a whole does not match - but it should have.
Perhaps it is relevant that x does not occur in what you call the
"successor formula"?

In any event, let me describe what happens in tracematches.
If the advice body does not mention x, we make it a weak reference.
However, we cannot discard a partial match simply because it
contained a nullified weakref: this is why it is essential to
distinguish between "collectable weakrefs" (which do allow
one to discard the partial match). As an example of that,
consider instead the pattern

    s1 s2 s1

Now when o1 is gc-ed, we know the partial match represented
by the binding (x=o1) cannot be completed, as that would require
another occurrence of o1. So in this case it *is* correct to
kill off the whole formula because one weak ref was nullified.

I'm probably misunderstanding what you said!

-Oege
Received on Sat Mar 04 16:24:27 2006