1(* ========================================================================== *) 2(* FILE : tttTimeout.sml *) 3(* DESCRIPTION : Timing out PolyML functions. *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================== *) 7 8structure tttTimeout :> tttTimeout = 9struct 10 11exception TacTimeOut; 12 13datatype 'a result = Res of 'a | Exn of exn; 14 15fun capture f x = Res (f x) handle e => Exn e 16 17fun release (Res y) = y 18 | release (Exn x) = raise x 19 20open Thread; 21 22fun timeLimit time f x = 23 let 24 val result_ref = ref NONE 25 val worker = 26 let 27 fun worker_call () = result_ref := SOME (capture f x) 28 in 29 Thread.fork (fn () => worker_call (),[]) 30 end 31 val watchdog = 32 let 33 fun watchdog_call () = 34 ( 35 OS.Process.sleep time; 36 if Thread.isActive worker 37 then (Thread.interrupt worker; 38 if Thread.isActive worker 39 then Thread.kill worker 40 else () 41 ) 42 else () 43 ) 44 in 45 Thread.fork (fn () => watchdog_call (),[]) 46 end 47 fun self_wait () = 48 ( 49 if Thread.isActive worker 50 then self_wait () 51 else 52 case !result_ref of 53 NONE => Exn TacTimeOut 54 | SOME s => s 55 ) 56 val result = self_wait () 57 in 58 release result 59 end 60 61fun timeOut t f x = timeLimit (Time.fromReal t) f x 62 63end 64