Measuring execution times with JPF

[Alexander von Rhein]

Hi,

I would like to use JPF to measure execution times of a program (on all
execution paths).
I know that you should not use model checkers for this task, because
they do much more work than a normal VM.
However I think that most of this additional work is state
storing/loading/matching, right?
So if I measure only the time spent in transitions it should be more or
less accurate.
Do you think this could work?
Is there any other time-intensive JPF-specific part that I can exclude
from the timing?

-- Alexander

[Cyrille Artho]

Hi Alexander,
You may want to read "Model Checking Real Time Java Using Java PathFinder" to find some similar work on this.
Basically, you can compute the worst-case execution time if you have a good notion (estimate) of the time required to execute each instruction.
You cannot get a reliable estimate by measuring the execution time along each path. Java PathFinder is written in Java and does not have a Just-in-time (JIT) compiler. It is therefore one or two orders of magnitudes slower than the highly optimized JVM that you would probably use in deployment.
See "JNuke: Efficient Dynamic Analysis for Java" for a performance comparison (admittedly, that was a decade ago, but I think the overall outcome has not changed).

[Peter Mehlitz]

you have to model time, real time bears little resemblance to a production VM due to JIT and async GC, i.e. JPF is not only slower because of the state management overhead but also shows the more linear behavior of a classic interpreter without generational garbage collection.

It sounds as if you want execution bounds, and just counting the number of executed instructions along paths might already be a useful approximation. JPF already does instruction counting (ThreadInfo.getExecutedInstructions()), which is also the basis for simple TimeModels such as ConstInsnPathTime. If you want to be more sophisticated, you can use a instructionExecuted listener that differentiates between instructions.

-- Peter

> --
>
> --- You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Alexander von Rhein]

Thank you for your advice.
In my application, i am not concered with real time constraints in programs.
I only want to predict the time needed for execution (in a real VM) by
observing JPF.
Of course I could count the instructions, but as you said the
instructions might also differ in their complexity (and need more or
less time).

So, if I understand you right, I can assume that the time needed for
execution with JPF has a (linear) relation to the time needed by a
classic interpreter VM.
It would be ok for me to predict the time needed by a very simple VM, as
opposed to the time needed by an optimized VM (GC, JIT, ...).

-- Alex

On 05/07/2013 09:15 AM, Peter Mehlitz wrote:
> you have to model time, real time bears little resemblance to a production VM due to JIT and async GC, i.e. JPF is not only slower because of the state management overhead but also shows the more linear behavior of a classic interpreter without generational garbage collection.
>
> It sounds as if you want execution bounds, and just counting the number of executed instructions along paths might already be a useful approximation. JPF already does instruction counting (ThreadInfo.getExecutedInstructions()), which is also the basis for simple TimeModels such as ConstInsnPathTime. If you want to be more sophisticated, you can use a instructionExecuted listener that differentiates between instructions.
>
> -- Peter
>
> On May 5, 2013, at 11:02 PM, Alexander von Rhein <rh...@fim.uni-passau.de> wrote:
>
>> Hi,
>>
>> I would like to use JPF to measure execution times of a program (on all execution paths).
>> I know that you should not use model checkers for this task, because they do much more work than a normal VM.
>> However I think that most of this additional work is state storing/loading/matching, right?
>> So if I measure only the time spent in transitions it should be more or less accurate.
>> Do you think this could work?
>> Is there any other time-intensive JPF-specific part that I can exclude from the timing?
>>
>> -- Alexander
>>
>> --
>>

>> --- You received this message because you are subscribed to the Google Groups "Java� Pathfinder" group.

[Sang Phan]

Hello,

Execution time also depends on cache. Can jpf do cache analysis ?
I wonder how to get a reliable estimate of execution time without
considering cache behaviour.

Sang

[Corina Pasareanu]

i think this would be very approximate. there is extra work in jpf for e.g. backtracking, po reduction, perhaps other run-time checks. at the very least you would need to first run jpf versus that simple vm to get an estimate of their relation in execution time. ... my 2c

corina

--- You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfinder+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

--

--- You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfinder+unsubscribe@googlegroups.com.