Use the old script to measure time

diff --git a/cdschecker_modified_benchmarks/test.sh b/cdschecker_modified_benchmarks/test.sh
index 1fd5d1f50459b3930269e68e184c81522036f42a..feea3d75414bfe5e2468c2aa6b480426e8d58f1d 100755 (executable)
--- a/cdschecker_modified_benchmarks/test.sh
+++ b/cdschecker_modified_benchmarks/test.sh
@@ -6,25 +6,23 @@ CDSLIB="/home/vagrant/c11tester"
 export LD_LIBRARY_PATH=${CDSLIB}
 export C11TESTER='-x1'
 
+
 COUNT_DATA_RACE=0
 COUNT_TIME=0
 
 for i in `seq 1 1 $TOTAL_RUN` ; do
-  OUTPUT="$( { time $EXE; } 2>&1 )"
+  OUTPUT="$(/usr/bin/time -f "time: %U %S" $EXE 2>&1)"
   RACE="$(echo "$OUTPUT" | grep "race")"
   if [ -n "$RACE" ] ; then
     ((++COUNT_DATA_RACE))
   fi
 
-  USER_TIME="$(echo "$OUTPUT" | grep -o "user..m.\....")"
-  USER_TIME_S="$(echo $USER_TIME | cut -d 'm' -f2 | cut -d '.' -f1)"
-  USER_TIME_MS="$(echo $USER_TIME | cut -d 'm' -f2 | cut -d '.' -f2)"
-
-  SYS_TIME="$(echo "$OUTPUT" | grep -o "sys..m.\....")"
-  SYS_TIME_S="$(echo $SYS_TIME | cut -d 'm' -f2 | cut -d '.' -f1)"
-  SYS_TIME_MS="$(echo $SYS_TIME | cut -d 'm' -f2 | cut -d '.' -f2)"
-
-  TIME_EXE=$((10#$USER_TIME_S * 1000 + 10#$USER_TIME_MS + 10#$SYS_TIME_S * 1000 + 10#$SYS_TIME_MS))
+  TIME="$(echo "$OUTPUT" | grep -o "time: .\... .\...")"
+  TIME_USER_S="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f1)"
+  TIME_USER_CS="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f2)"
+  TIME_SYSTEM_S="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f1)"
+  TIME_SYSTEM_CS="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f2)"
+  TIME_EXE=$((10#$TIME_USER_S * 1000 + 10#$TIME_USER_CS * 10 + 10#$TIME_SYSTEM_S * 1000 + 10#$TIME_SYSTEM_CS * 10))
   COUNT_TIME=$((COUNT_TIME + TIME_EXE))
 done