[abc] Re: RV05 publication (fwd)

oops, forgot to copy all you guys... feel free to chip in or
correct me!

---------- Forwarded message ----------
Date: Fri, 15 Apr 2005 15:39:36 +0100 (BST)
From: Oege de Moor <oege@comlab.ox.ac.uk>
To: Eric Bodden <eric@bodden.de>
Subject: Re: RV05 publication

Hi Eric,

Thanks for your messages regarding our paper on tracematches, and
your own on LTL formulae.

The main difference, as you point out, seems to be the use of
the skip symbol in our implementation. This was indeed the
main thing we got wrong when we started this work - the
need for skip only became apparent only when we attempted to prove
the equivalence of the declarative and operational semantics.
I'd strongly encourage you, therefore, to prove a similar result
in your setting - without a formal proof, I for one won't
believe that they just disappear with the use of alternating
automata.

Our OOPSLA submission has a full explanation, and there's no
substitute for carefully going over the proof in that paper.
However, let me try to give an informal reason why skip is
needed.

Consider the sequence of method calls

    v.f(); v.g(); w.g(); w.h();

and the tracematch

   tracematch(X x, X y) {

     sym a before : call(* f(..)) && target(x);
     sym b before : call(* g(..)) && target(y);
     sym c before : call(* h(..)) && target(y);

     a b c

   {...}
   }

Now according to the declarative semantics, the above
sequence will trigger this tracematch, with the binding
  x=v and y=w
The binding
  x=v and y=v
does not work.

So consider what happens during the matching process
when we have only seen

    v.f(); v.g();

at this point we can have matched "ab" with binding x=v and y=v,
or "a" with binding (x=v). In the latter case however, we have
to record that y!=v. To see why, consider the sequence

    v.f(); v.g(); v.g(); v.h();

This should *not* match according to the declarative semantics:
we're not allowed to ignore either call of v.g(). If we had
said that v.f(); v.g(); matches "a" with binding "x=v" (and
no constraint on y), we will erroneously conclude that
v.f(); v.g(); v.g(); v.h() matches "abc" with "x=v and y=v".

The need for skip and negative bindings thus arises out of the
way we filter traces: when you've only seen the events (I'm
now being more precise, using events as in the paper, not
just method calls)
  enter v.f();
  exit v.f();
  enter v.g();
you want to record the matches

   a;skip;b with x=v and y=v
   a;skip;skip with x=v and y!=v

because you don't know what events will follow those in
the trace you've seen so far.

Hopefully this addresses the main point you raised. I'd be
interested to hear in detail how your framework addresses
this issue.

Let me now turn to the detailed comments.

> Chapter 2 - grammar: "strictfp" is never mentioned in the text, I think

right, thanks. It's just like advice that this is the only modifier
that makes sense

> chapter 2.1: replace "line 8)" by "line 8"

Ta!

>General comments on examples: Those *might* benefit from the use of
>Generics
>for Maps etc. to immediately make clear, what types are mapped to what
>other
>types. However I see that this coult be a space issue.

Right, we wanted to keep it just to Java 1.4 and AspectJ < 5.

>aspect SafeIteratos: I think the "new Object()" is passed in to
>invalidate
>the old object being held, if I understood correctly. This did not become
>quite clear to be in the text. Also I think "new Object()" is not
>actually
>possible in Java since the constructor is protected.

Thanks, correct!

>General comments on trace matches: You model events "which prevent a
>tracematch from matching" by symbols which do not occur in the pattern. I
>would maybe find one *distinct* "exit" symbol or somthing like this more
>intuitive. Using or (|) it could fulfill the same purpose.

I do not understand this comment; can you illustrate it with one of
the examples?

>aspect AJConnectionManagement: This could really need auto(un)boxing,
>because the code is really hard to read and this is *not* only due to a
>limitation of AspectJ but also due to Java 1.4 and missing autoboxing.

Yes, we thought so too (you're repeating several intense discussions
we had amongst ourselves!), but decided to keep the paper within 1.4.

>section 3.6: "perthread" does not occur in your grammar

Thanks for spotting that!

>section 4.3: small \sigma is not defined before it is used on the top of
>page 12

well spotted, thanks.

>also I would rather write "(\sigma (f))(e1)" instead of just "\sigma
>(f)(e1)" - that helps parsing the formula

Ah yes, that betrays the fact that several of us are secret
replace "replace the pointcut tm" by "replace the tracematch tm"

>section 4.4: you define "interleaving" rather informally. thus i would
>expect "\Sigma* skip* f g" to be a valid interleaving for your example as
>well. "\Sigma* f g skip*" is obviously not contained, since it's not in
>"\Sigma A".

correct, but note that
 \Sigma* skip* f g
<= {because skip in \Sigma}
 \Sigma* f g
<= {because epsilon in skip*}
 \Sigma* f skip* g

So the statement that Pat = \Sigma* f skip* g is correct.
I'm not sure a formal definition of interleaving would help?

>at the end of section 4.4 you write that the complete constraint is
>(x=v)^(x!=w). This is correct, however I had expected a more verbose form as
>(x=v)^(x!=w)^(x!=w)^(x=v) according to Figure 4. In theory this is
>equivalent, but your implementation rises the question which of the two we
>actually gain at runtime, because I did not read about any simplification
>that you apply within the constraint. If you use a set-based implementation,
>that's of course no issue.

We intentionally left the constraint implementation open at this point,
and didn't want to talk about the simplification rules. The actual
implementation uses a set-based representation.

>chapter 4.5: typo: "lagnuage"

Aargh! don't know how that passed the spell checker. Thanks.

>chapter 4.6, page 14: I find the formulas on the top-left very hard to
parse
>for my brain. maybe you *should* use bigger vees and wedges for your
>formulas...

It's a matter of familarity, but using big vees and wedges with subscripts
becomes quickly unreadable in 10-point font. I'm afraid I got swayed
to use this form by Dijkstra and his disciples...

>formula (2): don't you have to exclude the "skip" symbol from the alphabet
>in the second line, since it is already being treated in the first line? not
>sure here...

A doesn't include skip; \Sigma = A \cup \{ skip \}.
You're right, it's worthwhile reminding the reader of that at this point.

>chapter 4.7: for me it did not became clear, why we need two constraints
>labsj and labsjp for any state. What does the suffix "p" stand for?

This is explained in the third paragraph of 4.7. To summarise, we have

labs = lab(s,t)
labsp = lab(s,te)

so the labsp are just the "new version" of labs. In the text,
we write labs and labs' - the "p" thus is an ASCII-fication of "prime".

>Also actually I did not quite understand, why you need "skip" at all. I *do*
>understand why you need constraints, but why do you need the constraints on
>"skip"? E.g. if your constraint implies "x=v", why would you also need to
>imply "x!=w" ?

See above: the invention of skip is in fact one of the main technical
contributions of the paper, and the crux to achieving equivalence between
the declarative and operational semantics. There is no way round it if
you want that equivalence.

>Also on the aspect you generate: What confuses me is that I am seeing no
>explicit state variable (state \in {1,2,3}) here. I am sure, this is
>somehow
>hidden inside your constraints, but I don't see it.

The fact is that you can be in several states at once. The constraint
tells you under what assumptions you are in a particular state. The
intuition
behind this is spelled out in the second paragraph of p. 11.

>This is maybe due to the fact that Constraint.sols() is nowhere defined.

It returns the set of valuations (for the tracecut variables)
that are the solutions of a constraint. You're right this needs
a sentence or two of explanation, which we'll put in.

>I find your operational semantics really hard to follow, so it would be
nice
>to have more explanation on your example to see why the constraints have
to
>be updated the way you do.

The fact is that it is tricky; the ultimate explanation of why it must
be this way is the proof of Section 4.5. The intuition is explained in
a lot of detail in Section 4.1. We had a lot of discussions whether it
would be better to give the whole intuition first, or to intersperse
that explanation with the formal presentation. In the end we decided
that it was better to give a roadmap, and then leave it up to the reader
whether they want to understand all the formal details. Do you think
it would be better to merge 4.1 with the formal definitions that follow?
Ideally we would do both, but then we have a space problem!

>chapter 5.1: in your tracematch example does not adhere to your grammar.
you
>might want to move the "Object o" parameters from the pointcuts to the
>tracecut header.

You've found us out! We changed the syntax shortly before submitting the
paper :-)

>generally on 5.1: Nice and difficult topic. Are you certain, that there
can
>be no solution that guarantees safety w.r.t. memory. This did not become
>100% clear to me. Certainl, state has to be held as long as a trace has
not
>matched. But I actually thought, it ought to be possible to clean it up
>completely, once it *did* match.

Hm, not 100% certain... but would it make a big difference, as it is
more common to have non-matching traces, and thus that is where the
memory problems are?

>chapter 7: replace "Bockish" by "Bockisch"

Thanks!

>regarding my work "Bodden": You write that any LTL property has a natural
>equivalent in regular expressions. Well, it is true, that any LTL formula
>over finite words can be expressed by a regex. However, LTL allows
negation,
>while regular expressions don't.
>This means that you have to go from LTL to
>an automaton and then back from the automaton to a regex, which then
*does*
>give you a regex, which might not be so "natural" any more.

Hm, it would be easy to add negation to the syntax and
implementation, of course. So I don't see the problem here.

>This means
>especially that converting LTL into regex may also be quite cumbersome -
not
>only the other way around. Variable binding actually works quite the same
>way (and with the same semantics) as for regex. E.g. we have formulae as:
>(forall) Lock l: G( call(Lock.acquire()) && target(l) ->
>F(call(Lock.release()) && target(l)) )

In the end it is a question of pragmatics: are most applications
easier to express with regexs or with LTL? I don't know. Do you
have LTL formulae that would be difficult to express, even if we
allowed negation in regexps?

>The fact that we have to use a finite automaton to convert from LTL to
regex
>raises another issue, which is sharing:

We haven't thought about this yet, good point!

>Still another question: Do you know about a good package to handle finite
>automata in Java (things like regex<->DFA, power set constrution, etc.)?
I
>wrote some stuff myself for the prototype, but maybe you know something
>better...

Chris wrote his own, but it would make sense to use something
generic...

>So, that was about it for this time :-)

Super, many thanks. Sorry for the long time it took to reply!

>I know, you might still need time to tidy up your code, but it would be
>great if I could get a copy of your impl. as soon as possiblem just to
play
>around with it and see if the code generation I have in mind, would work.

Unfortunately Chris (the main implementor) has to sit his finals exams
soon, so I doubt that we will have something to give to you before summer.

Finally, I've briefly read your paper, hopefully I'll have more
time to study it in detail soon. I don't understand why you say
that handling variable bindings is more cumbersome in our setting than in
the use of alternating automata. Above you seem to be complaining
about the complexity of our semantics, not the way variable bindings
are described via constraints. It's a bit unfair to compare the complexity
of our formal account with the lightness of your own informal treatment...
but then, everyone always finds their own ideas easier to understand :-)

Thanks again,

-Oege
Received on Fri Apr 15 15:40:14 2005