Java Team4 Benchmark3

This benchmark aims at measuring the performance of tracking a large number of individual objects and their behaviour with respect to a central synchronising entity. A "device" has two switchable but exclusive operation modes. "Work pieces" depend on one of those modes and can be "processed" iff the device is in the corresponding mode.

Category: Software Engineering

Benchmark Data

Specification Information

It should be verified that no work piece depending on mode x is processed (by invoking the method Piece.process()) while the device that created it (invocation of Device.createPiece()) is in a mode different from x. The mode of a device is changed by invoking Device.toggleMode().

The resulting symbolic monitor is the following.

• State space Q = {1,2,3,4}
• Quantification: ∀d∀p
• Transitions
  • δ(1,¬create(d,p)) = 1, δ(1,create(d,p)) = 2
  • δ(2,¬toggleMode(d)) = 2, δ(2,toggleMode(d)) = 3
  • δ(3,¬toggleMode(d)∧¬process(p)) = 3, δ(3,toggleMode(d)) = 2, δ(3,process(p)) = 4
  • δ(4,true) = 4
• Accepting states (with output ⊤) F = {1,2,3}

The event create(d,p) holds iff the method Device.createPiece() is invoked on some Device object d instantiating a Piece object p. The predicate toggle(d) holds for some Device object d iff Device.toggleMode() is invoked on d and process(p) is true whenever Piece.process() is called on a Piece object p.

Instrumentation Information

Using AspectJ the events are identified as follows.

• The abstract event create(l,i) is identified by the pointcut/advice

 pointcut createPiece(Device d):  call(public Piece Device.createPiece() && target(d));
 after(Device d) returning(Piece p): createPiece(d) { ... }

• The abstract events toggleMode(d) and process(p) are identified by the pointcuts

   pointcut deviceModeToggle(Device d) :  call(public void Device.toggleMode() && target(d));
   pointcut processPiece(Piece p) :  call(public void Piece.process() && target(p));

Program Information

Location: Java_track/Mufin/Benchmark5

• The number of times the events should be observed in the program:
  • create: 100282
  • toggleMode: 9973
  • process: 3

• Verdict
  • property is violated

Example Traces

Valid:

• create(1,2) process(2) toggleMode(1)
• create(1,2) create(3,4) process(2) toggleMode(1) process(4) toggleMode(1) process(2)
• create(1,2) process(2) create(3,4) process(2) toggleMode(1) toggleMode(3) toggleMode(3) process(4)

Invalid:

• create(1,2) toggleMode(1) process(2)
• create(1,2) create(3,4) process(2) toggleMode(1) toggleMode(3) togglemode(1) process(4)
• create(1,2) process(2) create(3,4) toggleMode(1) toggleMode(1) toggleMode(1) process(4) process(2)

(The numbers 1,…,4 represent object identities.)