RE: [abc] Joint work on specification formalisms?

I think that Oege has hit the nail on the head. I am also a firm
believer of the pragmatic approach and perhaps it is better to
concentrate more on good applications of the technology and setting
up good use cases and benchmarks at the moment.

Oege, do you think that we could set up a central bank, where we could
have other collaborators on that project (in fact, useful to have
as many collaborators as possible). In this way we could promote
collaboration, but not go down the tricky path of trying to write
joint papers with too many different authors?

Cheers, Laurie

+-----------------------------------------------------------------
| Laurie Hendren --- laurie.hendren@mcgill.ca
| Associate Dean (Academic), Faculty of Science,
| Dawson Hall, McGill University, 853 Sherbrooke St W,
| Montreal QC H3A 2T6 Canada, 514-398-7179, fax 514-398-1774
+----------------------------------------------------------------
| For contact and home page info as Professor, Computer Science:
| http://www.sable.mcgill.ca/~hendren --- hendren@cs.mcgill.ca
| Research: http://www.sable.mcgill.ca http://aspectbench.org
+----------------------------------------------------------------

On Tue, 31 Jan 2006, Oege de Moor wrote:

> 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 13:59:51 2006