[patch] Bug in timings on x86
Hi, On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo. By the way, the /new ticket/ link at mrmc-tool.org/trac/wiki/Contact <http://www.mrmc-tool.org/trac/wiki/Contact> doesn't work, because it wants me to log in and I can't seem to make an account. Cheers, Bram Geron CS student at Eindhoven University of Technology --- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100 +++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100 @@ -103,7 +103,7 @@ } timer_started = FALSE; - return ((unsigned long) (stop_time - start_time) * 1000 + return ((clock_t) (stop_time - start_time) * 1000 + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC; } @@ -567,7 +567,7 @@ /* Clean the old results */ clearOldModelCheckingResults(); - /* Star the timer */ + /* Start the timer */ startTimer(); /* In case of simulation engine on we have to traverse the tree */
Hi Bram, Thanks for your report. I'll have the patch archived for the next release. Note that the ticket link only works for frequent committers. Viet Yen On 19.12.11, Bram Geron <bgeron@gmail.com> wrote:
Hi,
On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo.
By the way, the new ticket link at mrmc-tool.org/trac/wiki/Contact(http://www.mrmc-tool.org/trac/wiki/Contact) doesn't work, because it wants me to log in and I can't seem to make an account.
Cheers,
Bram Geron
CS student at Eindhoven University of Technology
--- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100
+++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100
@@ -103,7 +103,7 @@
}
timer_started = FALSE;
- return ((unsigned long) (stop_time - start_time) * 1000
+ return ((clock_t) (stop_time - start_time) * 1000
+ CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC;
}
@@ -567,7 +567,7 @@
/* Clean the old results */
clearOldModelCheckingResults();
- /* Star the timer */
+ /* Start the timer */
startTimer();
/* In case of simulation engine on we have to traverse the tree */
_______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
Hi Viet Yen, It appears I didn't test my patch properly, and clock_t is also uint32 on x86. We could use unsigned long long (uint64), but it's not in C90. Maybe it's best to go via doubles? A possible patch is below. Cheers, Bram diff -r a4a01de0c579 -r bca9d2052ed5 src/io/parser/parser_to_core.c --- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100 +++ b/src/io/parser/parser_to_core.c Thu Dec 29 21:40:27 2011 +0100 @@ -103,7 +103,7 @@ } timer_started = FALSE; - return ((unsigned long) (stop_time - start_time) * 1000 + return ((stop_time - start_time) * 1000.0 + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC; } @@ -567,7 +567,7 @@ /* Clean the old results */ clearOldModelCheckingResults(); - /* Star the timer */ + /* Start the timer */ startTimer(); /* In case of simulation engine on we have to traverse the tree */ On 12/20/2011 01:38 PM, Viet Yen Nguyen wrote:
Hi Bram,
Thanks for your report. I'll have the patch archived for the next release.
Note that the ticket link only works for frequent committers.
Viet Yen
On 19.12.11, Bram Geron <bgeron@gmail.com> wrote:
Hi,
On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo.
By the way, the new ticket link at mrmc-tool.org/trac/wiki/Contact(http://www.mrmc-tool.org/trac/wiki/Contact) doesn't work, because it wants me to log in and I can't seem to make an account.
Cheers,
Bram Geron
CS student at Eindhoven University of Technology
--- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100
+++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100
@@ -103,7 +103,7 @@
}
timer_started = FALSE;
- return ((unsigned long) (stop_time - start_time) * 1000
+ return ((clock_t) (stop_time - start_time) * 1000
+ CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC;
}
@@ -567,7 +567,7 @@
/* Clean the old results */
clearOldModelCheckingResults();
- /* Star the timer */
+ /* Start the timer */
startTimer();
/* In case of simulation engine on we have to traverse the tree */
_______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
Dear Bram, Thanks for your check. Your report is archived for the future maintainer. At the moment, I'm only a placeholder for collecting feedback. Viet Yen On Dec 29, 2011, at 21:49 , Bram Geron wrote:
Hi Viet Yen,
It appears I didn't test my patch properly, and clock_t is also uint32 on x86. We could use unsigned long long (uint64), but it's not in C90. Maybe it's best to go via doubles? A possible patch is below.
Cheers, Bram
diff -r a4a01de0c579 -r bca9d2052ed5 src/io/parser/parser_to_core.c --- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100 +++ b/src/io/parser/parser_to_core.c Thu Dec 29 21:40:27 2011 +0100 @@ -103,7 +103,7 @@ }
timer_started = FALSE; - return ((unsigned long) (stop_time - start_time) * 1000 + return ((stop_time - start_time) * 1000.0 + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC; }
@@ -567,7 +567,7 @@ /* Clean the old results */ clearOldModelCheckingResults();
- /* Star the timer */ + /* Start the timer */ startTimer();
/* In case of simulation engine on we have to traverse the tree */
On 12/20/2011 01:38 PM, Viet Yen Nguyen wrote:
Hi Bram,
Thanks for your report. I'll have the patch archived for the next release.
Note that the ticket link only works for frequent committers.
Viet Yen
On 19.12.11, Bram Geron <bgeron@gmail.com> wrote:
Hi,
On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo.
By the way, the new ticket link at mrmc-tool.org/trac/wiki/Contact(http://www.mrmc-tool.org/trac/wiki/Contact) doesn't work, because it wants me to log in and I can't seem to make an account.
Cheers,
Bram Geron
CS student at Eindhoven University of Technology
--- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100
+++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100
@@ -103,7 +103,7 @@
}
timer_started = FALSE;
- return ((unsigned long) (stop_time - start_time) * 1000
+ return ((clock_t) (stop_time - start_time) * 1000
+ CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC;
}
@@ -567,7 +567,7 @@
/* Clean the old results */
clearOldModelCheckingResults();
- /* Star the timer */
+ /* Start the timer */
startTimer();
/* In case of simulation engine on we have to traverse the tree */
_______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
Viet Yen
participants (3)
-
Bram Geron
-
Viet Yen Nguyen
-
Viet Yen Nguyen