RE: [abc] J-LO benchmark results

Ok, now I see the difference. J-LO _is_ correct. It is just about the
semantics again... Let me explain.

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

In J-LO this pattern looks as follows: F(s1(x) /\XF s2(y)), i.e. finally
we see s1 and then from the next state on we see finally s2.
 
> now we could have the following trace:
>
> o1.foo(); // bind x = o1

After this step, the "successor formula" is F s2(y), since we now only
have the obligation left that we want to see a s2(y). We do not need the
value of x any more since we have no body which it could be used in and
also x does not occur any more in the successor formula.

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

After this, we evaluate to True, since we have seen s2(y) for one y.

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

As described above, the value of x is not relevant any more for
matching. Hence, it is not evaluated - it's value has no impact. I am
wondering - in the case of tracematches and in the case that x is never
use din the body can you then not also drop this binding? It is not used
for matching after all... (But maybe you still need it due to the way
your automaton implementation works - I am not sure. Please tell me.)

> Perhaps it is relevant that x does not occur in what you call
> the "successor formula"?

Exactly.

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

So did this become clearer now?

Eric
Received on Sat Mar 04 16:37:03 2006