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/Benchmark3

The benchmark can be compiled via the compile.sh script, compiled with instrumentation via the compile-instrumented.sh script and run via the run.sh script.

• 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.)

Clarification Requests

The format changed from last year so the benchmark isn't quite organised in the way required for this year. However, as it is quite a bit of work to reformat it for little obvious gain, don't worry. If anybody needs clarifications due to the different format please post them here -- Giles 2016-07-06

Please indicate how to (compile? and ) run the benchmark for the competition (if there is a choice of arguments give which ones should be used in the competition) -- Giles 2016-07-06