Hi Jesus,
On 21/05/2013 19:31, Jesus Aransay wrote:
this is my first mail to the list, so first I wanted to say hello and kindly ask you for forgiveness if I break any conventions that usually apply in the list.
Welcome to the list. It has a very low posting rate so we don't need to worry about conventions.
We were doing some program performance testing with Poly ML 5.5 and we detected the following behavior when trying to use the information
The last function returns a "run" time of "0.1" in a Linux machine, but "11.7" (approx) in our Windows machine, when the real time can be checked in both machines to be of the order of "0.1" (actually, the Windows machine in our case has much better hardware and is indeed faster in computations, this is the reason why we wanted to stick to it). Somehow, the timing information provided in the Windows machine is not correct. It scales to greater computations, where 200 seconds of real run time are shown in Windows as maybe 2000.
In our Linux machine we have used the polyml version shipped with Isabelle 2013, whereas in the Windows machine we are using the binary version for Windows obtained from sourceforge.
Are we doing anything wrong? Is this a known issue?
I would guess that you're using PolyML.timing for the timing. I discovered a bug in the way it worked on Windows and fixed it in SVN. Perhaps the easiest way to work-around it is to use the functions from the Timer structure (startCPUTimer and checkCPUTimes) and then wrap the function you want to time in calls to them. They should work correctly on both Windows and Linux. If there are any problems let me know.
David