RE: [abc] Joint work on specification formalisms?

Hi Eric,

I am keen to work on this, and as you know, the pragmatic approach to these
questions is the topic of the paper we're planning for OOPSLA. Personally I
believe it is is very important we resolve it from the pragmatic perspective
first. As it stands, our examples and benchmarks are quite weak. The example
specifications (be it in J-Lo, PQL, tracematches or whatever) are nice but
not totally convincing. Are they really worth a potential slowdown by a
factor of 30? True, they're short but at most it saves 2 pages of fairly
nice AspectJ. I think this is the issue we have to resolve first: are these
formalisms worth the candle, or is it better to use a simpler mechanism like
AspectJ? One particular area where we don't have a lot of good examples is
in properties of concurrent programs.

Before anything else, it is of paramount importance that we come up with
many more examples and benchmarks. As I've said privately to Klaus (and
indeed lots of other people who work in this area) it would be *superb* to
have more examples provided by him. Benchmarks from others are always better
than benchmarks written by us! I'll say it again: we must, must, must have
more good examples first, and measure their performance, before doing
anything else. That is the purpose of the OOPSLA paper: we want to have a
publication, of course, but it is also essential to further our own
understanding of how these specs can be used in practice.

If we're still happy about these formalisms once we have done put them to
the acid test of real applications, it would be great to have a better
formal understanding of their relative expressiveness. Formal results about
expressiveness will be pretty tough, however, as the presence of bound
variables changes the picture completely compared to the well-established
results: for instance, tracematches can express at least some non-regular
properties of traces. Of course the problem is fun, and indeed one of the
topics that we mentioned in the application for the "centre for
metacomputation" - a new grant that joins work in the theory, verification
and tools groups at Oxford.

You wrote an earlier message about static analysis. This is something we
(the Oxford gang) have been gunning for since the very earliest days of abc
- in my first conversation about aspects with Laurie we already talked about
specifying trace properties and optimising them with static analyses of the
kind found in TVLA etc. So several of us on the Oxford side would also like
to work on this. However, again it is putting the cart before the horse to
do that without a solid set of nice examples that can guide what we want to
do. There are umpteen (ok, perhaps only 10) papers that show how to check
properties like failsafe use of iterators. Great! we may be able to use
those! However, if you look at something like the hashcode example, there
it's much less clear we can devise a static analysis that does a good job.
So how common is that? There's little point working out a nifty analysis
only to find that it applies to three examples that we picked because we saw
them in the literature on static checking.

Finally, I think Klaus puts his finger on the spot pointing out the number
of collaborators. *Within our team* there are at least Ondrej, Nomair,
Laurie, you, Pavel, Julian, Damien and myself already interested and
actively working on this space. [Pavel & Julian: implementation, pattern
analysis, leak busting. Damien: formal properties of tracematches,
equivalence of various semantics]. As Laurie says, there's a lot to do, but
even within the team there is a danger of too much overlap when it comes to
writing theses; the soup may become rather thin if we have to divide it with
yet more collaborators.

For that reason I have been a little hesitant to draw in yet more people
from outside: we already have a lot of people working on it [perhaps even
too many, given that we don't find our own examples 100% convincing].
Consequently, I didn't take up Klaus's suggestion of joint work when he
emailed me about it in December, nor similar suggestions from Rob Walker and
the Darmstadt group. Of course we should talk to them, but I feel a little
uneasy expanding the group of collaborators yet further. Of course we should
talk to them - and keep asking for benchmarks!

Best wishes,

-Oege

  _____

From: Majordomo list server [mailto:majordomo@comlab.ox.ac.uk] On Behalf Of
Eric Bodden
Sent: 31 January 2006 01:19
To: abc@comlab.ox.ac.uk
Subject: [abc] Joint work on specification formalisms?

Hi all.

I just emailed with Klaus Havelund today, discussing some things about
expressiveness of tracematches, J-LO and so forth and it seems that Klaus
would be very much interested in some joint work about all those different
formalisms around, i.e. what formalisms exist at all, how they compare
w.r.t. expressiveness and applicability for certain tasks, i.e. what
properties exist and in what formalisms they can be specified best. So it's
going to be mostly a theory paper, I guess. For me, this is kind of going to
be part of my thesis anyway in the longterm, but I was wondering if somebody
else is interested in that. If so, please let me know.

Eric

  _____

From: Klaus Havelund [mailto:havelund@gmail.com]
Sent: Monday, January 30, 2006 7:58 PM
To: Eric Bodden
Subject: Re: AOSD

Eric,

Whatever collaboration/non-collaboration you are comfortable with is fine
with me.
I was wondering whether you are working on a logic with Oege? I mean: is the
tracematch
work going to evolve or are they happy about it as it is? And how would our
collaboration
relate to that work. The reason I ask is because I see collaborations from
anywhere between 2 people to
10 people.

Klaus

      
Received on Tue Jan 31 10:41:47 2006