Closed you-n-g closed 2 years ago
I go through the docs but didn't find any related docs. Now I plan to use some profiling tools to get the detailed timing.
Finally, I find a profiling tool named async-profiler
The test cost 6171 samples and 15.801 seconds
About 1380 samples are in org/jetbrains/kotlinx/lincheck/LinChecker.run
(val failure = scenario.run(this, verifier)
)
So I think the time of linearizability verification is about 1380/6171 * 15.801 = 3.5335 seconds
The timing solution is very cumbersome. I will appreciate you if you have any more convenient solution.
Thanks.
@you-n-g
Do you mean by linearizability verification
linearizability verification of execution results?
In this case you may be interested in Verifier.verifyResults
method.
By the way:
LinChecker.run
method. Other samples are collected from parallel threads.@alefedor
Thanks for your reply
I'm interested in the time information of the verification process. Can Verifier.verifyResults
provide this information?
Besides, I don't understand how to access the Verifier.verifyResults
. The check
function returns void.
Your way of estimating times apparently shows not what you want. There are several threads and the main one spends almost all the time in LinChecker.run method. Other samples are collected from parallel threads. Is it correct that my way of estimating time includes both trace collection and verification of multiple threads?
Thanks
P.S. Attached is the profiling file I got from async-profiler. profile.zip
@you-n-g
Can Verifier.verifyResults provide this information?
No, but this is the method you want to time.
@alefedor Thanks so much!
So is it correct that the time for verification in my case is about 276 / 6171 * 15.801 = 0.70670?
@you-n-g
There is still problem with parallel threads in your estimations.
More realistic will be Verifier.verify
samples / Lincheck.check
samples Time = 276 / 1400 15.8 = 3.11
Yet, I'm not sure whether async profiler works as expected in case of blocking methods such as Thread.join
.
Besides, I can not understand what you are trying to estimate.
If it is the percentage of time spent on verification
, it depends on number of iterations/invocations, size of test scenarios and the tested data structure.
Thanks so much for such detailed advice :)
My motivation is to measure the time cost of linearization verification given a specific example under different settings (iterations, actorsPerThread, threads)
Hi, Thanks to your help, I've successfully built and run the example
I have one more question now. How could I get the time cost of a Linearizability Test?
For example, each run of a Linearizability verification test consists of the following time.
I want to get the time cost of linearizability verification.
Thanks :)