Re: [abc-users] Tracematch and "if(thisJoinPoint.getThis() != aParticularObject)"

From: Eric Bodden <eric.bodden_at_mail.mcgill.ca>
Date: Wed, 23 Apr 2008 17:53:28 -0400

Hi all.

Just to add to what Pavel said:

> I'm slightly confused about your choice of pattern. Why do you have the
> fragment "exitWriteAnother*"? Since that symbol binds none of the tracematch
> variables, and you intend it to match exit events that bind something other
> than w1 and w2, I believe the correct way of achieving this is simply having
> the pattern "enterWrite1 enterWrite2", which will allow zero or more objects
> distinct from w1 and w2 to exit in between the two events...

A agree with Pavel that your pattern is incorrect. In fact I once
wrote a very similar tracematch to detect lock order reversal. The
general workaround that one can take is to simply compare variables in
the tracematch body. This is not quite as efficient as a "distinct"
annotation would be but it should give you correct results. In your
example:

 tracematch(Writer w1, Writer w2)
 {
 sym enterWrite1 after:
 call(* Database.enterWrite()) && this(w1);

 sym enterWrite2 after:
 call(* Database.enterWrite()) && this(w2);

 sym exitWrite1 after:
 call (* Database.exitWrite()) && this(w1);

 sym exitWrite2 after:
 call (* Database.exitWrite()) && this(w2);

 enterWrite1 enterWrite2
   {
    if(w1!=w2) {
        System.out.println("Writers "+w1+" and "+w2+
        " have entered concurrently");
    }
   }
 }

Eric

-- 
Eric Bodden
Sable Research Group
McGill University, Montréal, Canada
Received on Wed Apr 23 2008 - 22:53:31 BST

This archive was generated by hypermail 2.2.0 : Wed Apr 23 2008 - 23:20:12 BST