Wrong running time

[Halbaroth]

I am using Benchpress to track regressions in Alt-Ergo but sometimes I got regressions that I cannot reproduce manually. My guess is that the way Benchpress computes running times is not appropriate for this purpose and the current times can be wrong if the server is overloaded. Thus, I tried to run Benchpress with less jobs to prevent this behavior, but still I have non-replicable regressions.

I could solve my problem by adding the running time without IO operations (the CPU time?) in the database for each tests.

I would be glad to add the feature by myself ;)

[Halbaroth]

benchpress/src/core/Run_proc.ml

Lines 9 to 41 in 2d84e9d

	let run cmd : Run_proc_result.t =
	let start = Ptime_clock.now() in
	(* call process and block *)
	let p =
	try
	let oc, ic, errc = Unix.open_process_full cmd (Unix.environment()) in
	close_out ic;
	(* read out and err *)
	let err = ref "" in
	let t_err = Thread.create (fun e -> err := CCIO.read_all e) errc in
	let out = CCIO.read_all oc in
	Thread.join t_err;
	let status = Unix.close_process_full (oc, ic, errc) in
	object
	method stdout= out
	method stderr= !err
	method errcode=int_of_process_status status
	method status=status
	end
	with e ->
	object
	method stdout=""
	method stderr="process died: " ^ Printexc.to_string e
	method errcode=1
	method status=Unix.WEXITED 1
	end
	in
	let errcode = p#errcode in
	Log.debug
	(fun k->k "(@[run.done@ :errcode %d@ :cmd %a@]" errcode Misc.Pp.pp_str cmd);
	(* Compute time used by the command *)
	let rtime = Ptime.diff (Ptime_clock.now ()) start |> Ptime.Span.to_float_s in
	let utime = 0. in

Does Ptime_clock.now () return the elapsed time? As an experimentation, I will replace Ptime_clock.now () by Sys.time which returns the cpu time. It should fix my issue. If it do so, I will add an extra field in the DB to keep the total cpu time also.

[c-cube]

Sys.time will return the CPU time for the current process (i.e benchpress), not for the solver. Ptime_clock.now returns the posix wallclock, which indeed might vary if the server is overloaded.

I'm not sure what the clean solution is. Maybe @Gbury can chime in about using cgroups to ensure that subprocesses get dedicated CPU resources? I think François Bobot does this in his benchmark tool.

[Gbury]

This is all a bit complicated, but I'd say:

• to ensure a set amount of cpu ressources, the best best would probably be to set the cpu affinity (see, e.g. https://unix.stackexchange.com/questions/73/how-can-i-set-the-processor-affinity-of-a-process-on-linux ), but that would also require to set affinity for all the other processes running on the machine if one wants to ensure that the prover processes are alone on each core (or find another solution ?)
• One of the motivation for using something else that wall clock time to measure regression is that some colleagues told us that the OS might decide to batch IOs, which could result in arbitrary delays for some instances of provers on systems that are under load (or that do a lot of IO, e.g. when starting more than a dozen provers at the same time). One idea was to use cpu time to identity regressions, but maybe there would be other solutions (stagger the starting times of processes, preload/put in the cache the input problem files, etc...)

[Halbaroth]

I am trying another solution given by a colleague ;)