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

Hi,

     I'm using tracematches to discover some concurrency problems in a
 simple Readers / Writers program.

 To do so, I have a tracematch to detect whether two writers have
 concurrently entered or not to a database. My tracematch is:

 tracematch(Writer w1, Writer w2)
 {
 /** A writer bound to w1 entered to the database**/
 sym enterWrite1 after:
 call(* Database.enterWrite()) && this(w1);

 /** A writer bound to w2 entered to the database**/
 sym enterWrite2 after:
 call(* Database.enterWrite()) && this(w2);

 /** The writer w1 exited the database**/
 sym exitWrite1 after:
 call (* Database.exitWrite()) && this(w1);

 /** The writer w2 exited the database**/
 sym exitWrite2 after:
 call (* Database.exitWrite()) && this(w2);

 /** Another, different writer, exited of the database**/
 sym exitWriteAnother after:
 call (* Database.exitWrite());

 /** Writers entered concurrently but between them can exit zero or more
 objects except w1 and w2 **/
 enterWrite1 exitWriteAnother* enterWrite2
 {
 System.out.println("Writers "+w1+" and "+w2+" have entered
 concurrently");
 }
 }

 I'm interested in the following execution sequence:

 w1.enterWrite();
 w2.enterWrite();
 w1.exitWrite();
 w3.enterWrite();

 My current code prints the following:

 Writers w1 and w2 have entered concurrently -->(Right)
 Writers w2 and w3 have entered concurrently -->(Right)
 Writers w1 and w3 have entered concurrently -->(Wrong because writer
 w1 exited before w3 entered)

 The last line was matched by:
 
 w1.enterWrite(); 
 w1.exiteWrite();
 w3.enterWrite();

 (Note: enterWrite() and exitWrite() method access Database.enterWrite()
 and Database.exitWrite() respectively).

 The previous match happened because the "exitWriteAnother"
 and "exitWrite1" symbols matched with the same event(w1.exitWrite();).

 My finally intention is to avoid that w1.exitWrite(); matches with
 exitWriteAnother because I want to express that "exitWriteAnother" is
 any object other except w1 and w2. The object bounded in
 exitWriteAnother symbol is not important because this symbol can
 happened several times(zero or more) and I do not want to bind these
 variables.

 To differentiate between the "exitWrite" and "exitWriteAnother" symbols,
 I tried modifying the "exitWriteAnother" symbol this way:

 sym exitWriteAnother after:
 call (* Database.exitWrite()) &&
  if(thisJoinPoint.getThis() != w1) &&
  if(thisJoinPoint.getThis() != w2);

 But when I compile this tracematch, I get the following errors:
 Local w1 is not bound by this symbol so it cannot be used within.
 Local w2 is not bound by this symbol so it cannot be used within.

 then, How can I express that "exitWriteAnother is any object other
 except w1 and w2"?.

 In other low level, I need an automaton state without free variables
 than accesses previously bounded variables. Thus, I can add the
 constraint "X != v", where v is a free variable previously bounded.

 Can you help me?

 Now, if I can have an automaton state without free variables than
 accesses previously bounded variables. What's happened with the
 following sequence of events?

 w1.exitWrite();
 w2.exitWrite();
 w3.exitWrite();

 In this sequence, which are symbols matched with w1.exitWrite(); event?

 1) exitWrite1
 2) exitWriteAnother

 Possible answers:
 1) yes.
 2) I do not know because it depends on:
  2.1) if the exitWrite1 symbol is matched before exitWriteAnother.
  2.2) if the exitWriteAnother symbol is matched before exitWrite1.

 To solve it, I think one can add the constraint "is v bounded?", where v
 is a free variable defined in tracematch header.

 Thank in advance.

 Paul Saint Leger Morales
Received on Wed Apr 23 2008 - 22:15:17 BST