[abc] Re: AOSD.06 Paper Notification (23)

Hi all.

I thought that w.r.t. the ECOOP submission, you might be interested in the
review we got from our AOSD proposal. A lot of what the reviewer's said was
unfortunaely simply wrong (or missunderstood) but maybe one can learn
something from this. Especially the last part about tracecuts sound's
interesting. Personally, I cannot believe what the reviewer is claiming
(tracecuts generating a usual DFA is a context free pattern is equivalent to
a regular one).

Eric

>
> - "Even if tracematches did support conjunction and nega- tion as for
> instance generalised regular expressions do, this would not yield
> similar expressiveness to LTL because the semantics are entirely
> different: While a* \intersection b* is only satisfied by the
> empty trace, ..."
>
> The authors do not define which generalized expressions they are
> referring to. One notion the present reviewer knows defines extended
> regular expressions as defined over predicates as basic terms (see
> [bbe01a], p. 5, below). The authors' statement is false w.r.t. this
> definition of extended generalized expressions.
>
> p. 11
>
> - "Consequently we ob- served memory usage linear to the number of
> bound objects and for a fixed number of bound objects constant over
> time. Any application tracking existing objects should show the
> same behaviour."
>
> Memory usage depending on the number of bound object is rather
> incomplete a discussion. What is much more interesting is how many
> objects have to be bound depending on the structure of temporal
> formulas. A formula such as F(\exists x -> F(\all y -> F(apply(x,
> y)))) will probably incur a huge memory overhead if x and y refer to
> arrays which are modified until the outer finally condition
> evaluates to try.
>
> References:
>
> @InProceedings{ als+03a,
> author = {R. A. {\AA}berg and J. L. Lawall and M.
> S{\"u}dholt and G. Muller and A.-F. Le
> Meur},
> title = {On the automatic evolution of an OS kernel using temporal
> logic and AOP},
> booktitle = {Proceedings of Automated Software Engineering (ASE'03)},
> year = 2003,
> organization = {IEEE},
> pages = {196--204},
> keywords = {aop, operating system, scheduling, Bossa, EAOP}
> }
>
> @Article{ bbe01a,
> author = "Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
> Fisman and Anna Gringauze and Yoav Rodeh",
> title = "The Temporal Logic Sugar",
> journal = "j-LECT-NOTES-COMP-SCI",
> volume = "2102",
> pages = "363--??",
> year = "2001",
> location =
> "http://www.research.ibm.com/people/e/eisner/papers/sugartoolpaper.ps"
> }
>
>

> 1. You argue that model checking is important; fine. You argue that
> constraint
> enforcement is important; fine. You imply that LTL is a great language for
> achieving these ends. It is here that I have the problem. Who is supposed
> to be
> using this language? Developers? Did you stop to wonder whether LTL will
> be an
> effective development language? The fact that you do not discriminate
> between
> the terms "specification" and "implementation" or between "formalism" and,
> say,
> "implementation" is rather worrisome. "We have presented a specification
> framework for formal reasoning about object-oriented programs": I could
> have
> sworn that this was an implementation language for enforcing temporal
> properties. If not, do model checkers need an implementation language?
>
> If tracechecks' typical users frequently cannot interpret what the
> tracechecks
> are saying correctly, they will either not use tracechecks or they will
> not use
> tracechecks correctly. In the latter case, the most insidious of bugs will
> occur: the wrong properties will be enforced, and the developer doing
> debugging
> will be hard-pressed to understand what the problem is. That the formalism
> is a
> favourite of theorists is irrelevant in this context. That "specifying
> this
> property is easily done by a straight forward translation into linear
> temporal
> logic" is a rather enormous claim.
>
> 2. Let's consider the formal expressiveness properties of this approach
> versus
> tracematches. LTL is known to be a proper subset of the regular languages.

Eric: This is completely wrong (and a prove for that the reviewer had no
clue about what was going on in the paper :-( ).

> Regular languages are expressible by tracematches. You claim that there
> are
> expressions available to tracechecks that cannot be expressed by
> tracematches.
> There is an apparent paradox here. Examining Section 6 closely, I see a
> variety
> of questionable statements that might be the source of this apparent
> paradox.
> Ultimately, any regular expression can be realized as tracematches, which
> means
> any LTL expression can be realized as tracematches. So it is hardly
> surprising
> that a "unified framework" is possible.
>
> I can't believe that you're making me a defender of tracematches, but here
> it
> goes. "This makes clear that negation and conjunction may hardly be needed
> [in
> situations where tracematches are being used]." Your arguments that
> tracematches are used for the positive while tracechecks are used for the
> negative are a stretch. After all, in your own examples, you negate the
> specified properties to cause exceptions to occur when the specified
> properties
> fail to hold (i.e., when the negatives do hold).
>
> Negation can only be defined with respect to a universe. Tracematches are
> explicit about this universe; tracechecks are not. A tracematch defines
> the
> alphabet of interest to it. This alphabet ought to be a subset of the
> universe
> of events within a program. Symbols from the program's universe not in the
> tracematch's alphabet are ignored. Thus, modifications to the universe not
> of
> interest within a tracematch will not require a change to the tracematch.
> So,
> this point is something of a "red herring": a negation operator could be
> provided as syntactic sugar, \forall x\in\Sigma, !x = union over (all
> a_i\in\Sigma where a_i!=x) a_i. Similarly, conjunction can be achieved
> through
> the use of one tracematch for each term in a conjunction; less elegant
> than
> direct support, but sufficient.
>
> "The property [LTL expression omitted] cannot be expressed at all using
> tracematches since AspectJ pointcuts cannot bind objects under negation."
> This
> comment seems rather bogus to me. Translate your LTL expression to the
> equivalent regular expression and then they can be implemented; after all,
> you
> claim that your model is a labelled transition system with states being
> joinpoints: you seem to be saying then that your own solution doesn't
> work.
> "However, given the fact that negation is only implicitly available, this
> would
> mean seval syntactic transformations, which we see as cumbersome in a
> general
> setting." This *might* be true if the transformations could not be
> performed
> mechanically, and if the more appropriate expression of the desired
> properties
> were via LTL. But this brings us full circle back to my first complaint.
>
> Other points:
>
> "These examples show that with respect to aspect-oriented programming,
> tracechecks are not just yet another AOP language extension. They can be
> seen
> as a formalism to extend the interface of an aspect or class ... with
> semantic
> properties." (a) I think that this is an unfair dismissal of a large class
> of
> work as "just AOP language extensions". (b) It seems to give the
> impression of
> something wholly new, rather than "just another history-based AOP
> approach".
>
> The approach of Walker and Viggers is not a formalism; it is based on a
> formalism. "Custom action blocks" are used only when CFLs do not suffice.
> Thus,
> not providing such a mechanism implies limiting the developer when they
> *need*
> to do something unusual. How can action blocks interfere with the matching
> process? Tracecuts are translated into aspects. Aspects apply to
> themselves and
> to each other. In the worst-case, you might not be able to automatically
> optimize away infeasible paths and the like, if that optimization depended
> on
> the CFL formalism. There is no "extra overhead" from the approach, as
> tracecuts
> reduce to regular expressions if a regular expression suffices. Stacks are
> only
> needed if actual recursion is present, and this is the only time they are
> paid
> for.

Isn't there a theorem that in general for a CFL it is not decidable wheter
there exists an equivalent regular CFG?

Eric
Received on Mon Dec 5 15:02:10 2005