author  webertj 
Wed, 19 Sep 2007 18:48:54 +0200  
changeset 24651  452962f294a3 
parent 21266  288a504c24d6 
permissions  rwrr 
18760  1 
(* Title: Pure/MLSystems/polymlinterrupttimeout.ML 
2 
ID: $Id$ 

21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

3 
Author: Tjark Weber 
24651
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

4 
Copyright 20062007 
18760  5 

6 
Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML. 

7 
*) 

8 

21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

9 
(* Note: This code may cause an infrequent segmentation fault (due to a race 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

10 
condition between process creation/termination and garbage collection) 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

11 
before PolyML 5.0. *) 
18760  12 

24651
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

13 
(* Note: The timer process sometimes does not receive enough CPU time to put 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

14 
itself to sleep. It then cannot indicate a timeout when (or soon 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

15 
after) the specified time has elapsed. This issue is obviously caused 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

16 
by the process scheduling algorithm in current PolyML versions. We 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

17 
could use additional communication between the timer and the worker 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

18 
process to ensure that the timer receives /some/ CPU time, but there 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

19 
seems to be no way to guarantee that the timer process receives 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

20 
sufficient CPU time to complete its task. *) 
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

21 

21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

22 
(* Note: f must not manipulate the timer used by Posix.Process.sleep *) 
18814  23 

24 
fun interrupt_timeout time f x = 

21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

25 
let 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

26 
val ch = Process.channel () 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

27 
val interrupt_timer = Process.console (fn () => 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

28 
(Posix.Process.sleep time; Process.send (ch, NONE))) 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

29 
val interrupt_worker = Process.console (fn () => 
24651
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

30 
Process.send (ch, SOME (Exn.capture f x))) 
21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

31 
in 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

32 
case Process.receive ch of 
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

33 
NONE => (interrupt_worker (); raise Interrupt) 
24651
452962f294a3
comment added to explain a potential scheduling problem
webertj
parents:
21266
diff
changeset

34 
 SOME fx => (interrupt_timer (); Exn.release fx) 
21266
288a504c24d6
new CCSbased implementation that should work with PolyML 5.0
webertj
parents:
18814
diff
changeset

35 
end; 