Difference between revisions of "Java Team4 Benchmark3"
Line 51: | Line 51: | ||
=== Program Information === | === Program Information === | ||
− | Location: Java_track/Mufin/ | + | Location: Java_track/Mufin/Benchmark3 |
* The number of times the events should be observed in the program: | * The number of times the events should be observed in the program: |
Revision as of 14:18, 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
Contents
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 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.)