packages feed

liquid-fixpoint-0.1.0.0: external/fixpoint/timeout.ml


module M = Mutex
module T = Thread

let get_time () = int_of_float (Unix.time ())

let mk_task =
  fun f x lk (ret, rd) -> let rv = f x in
    M.lock lk; ret := Some rv; rd := true; M.unlock lk

let not_done lk (ret, rd) = 
  M.lock lk; let trd = !rd in (M.unlock lk; not(trd))

let fail thread (ret, rd) =
  T.kill thread; ret := None; rd := true 

let do_timeout i f x =
  let task = mk_task f x in
  let (ret, rd) as rr = (ref None, ref false) in
  let stime = get_time () in
  let lk = M.create () in 
  let t  = T.create (task lk) rr in
  while not_done lk rr do
    if (get_time () - stime < i) then
      T.yield ()
    else
      fail t rr
  done; !ret