search

cuplv / verivita

Dynamic verification using callbacks
2 stars 1 forks source link

printing program time to stderr broken in OSx (low priority) #183

Open ftc opened 7 years ago

ftc commented 7 years ago

Runlim.py from benchtools prints the runtime of a process at the beginning of stderr output instead of the end. Experiment.py expects it at the end. I think this is just a difference in how OSx handles processes somehow but didn't spend the time to debug. Here is a modified experiments.py which just bypasses the issue (we will do the timing on another system or fix it).

experiment.zip

ftc commented 7 years ago

Note that this difference with OSx may prevent benchtools from killing the process if it takes too long or too much memory.

ftc commented 7 years ago

Also scheduler.py can't correctly get the number of CPUs so I hardcoded the value for our new macbooks. This is probably another todo for automatically getting this number.

sheduler.zip