Difference between revisions of "Java Team4 Benchmark3"

From CRV
Jump to: navigation, search
(Created page with "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 "devic...")
 
Line 4: Line 4:
 
"Work pieces" depend on one of those modes and can be "processed" iff the device
 
"Work pieces" depend on one of those modes and can be "processed" iff the device
 
is in the corresponding mode.
 
is in the corresponding mode.
 +
 +
Category: Software Engineering
  
 
== Benchmark Data ==
 
== Benchmark Data ==

Revision as of 10:54, 26 May 2016

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

Comments

Clarification Requests