Today's trick : memory limits with Gc alarms

Learning
2

As the author of mSAT, I’d just like to say the trick of using gc alarms to implement a memory limit in mSAT was actually taken from the theorem prover zenon, where if I remember correctly it was written by @damiendoligez , which might explain the subtle use of alarms/finalisers ^^

Also, as a side note, for people who would like to implement a similar limit but for computation time, I’d advise against using alarms (as is done in the code of zenon iirc) as they have proven to be somewhat not reliable, and I’ve found using Unix timers to raise an Out_of_time exception much better:

let run_with_time_limit limit f =
  (* create a Unix timer timer *)
  let _ = Unix.setitimer Unix.ITIMER_REAL Unix.{it_value = limit; it_interval = 0.01 } in
  (* The Unix.timer works by sending a Sys.sigalrm, so in order to use it,
     we catch it and raise the Out_of_time exception. *)
  let () =
    Sys.set_signal Sys.sigalrm (
      Sys.Signal_handle (fun _ ->
          raise Out_of_time)
      ) in
  Fun.protect f ~finally:(fun () ->
    Unix.setitimer Unix.ITIMER_REAL Unix.{it_value = 0.; it_interval = 0. }
  )
7 Likes