58 val groupkilling = ref true |
58 val groupkilling = ref true |
59 (* synchronizing *) |
59 (* synchronizing *) |
60 val lock = Mutex.mutex () (* to be aquired for changing state *) |
60 val lock = Mutex.mutex () (* to be aquired for changing state *) |
61 val state_change = ConditionVar.conditionVar () (* signal when state changes *) |
61 val state_change = ConditionVar.conditionVar () (* signal when state changes *) |
62 (* watches over running threads and interrupts them if required *) |
62 (* watches over running threads and interrupts them if required *) |
63 val managing_thread = ref (Thread.fork (fn () => (), [])) |
63 val managing_thread = ref (NONE: Thread.thread option); |
64 |
64 |
65 (* move a thread from active to cancelling |
65 (* move a thread from active to cancelling |
66 managing_thread trys to interrupt all threads in cancelling |
66 managing_thread trys to interrupt all threads in cancelling |
67 |
67 |
68 call from an environment where a lock has already been aquired *) |
68 call from an environment where a lock has already been aquired *) |
75 |
75 |
76 (* start a watching thread which runs forever *) |
76 (* start a watching thread which runs forever *) |
77 (* must *not* be called more than once!! => problem with locks *) |
77 (* must *not* be called more than once!! => problem with locks *) |
78 fun start () = |
78 fun start () = |
79 let |
79 let |
80 val new_thread = Thread.fork (fn () => |
80 val new_thread = SimpleThread.fork false (fn () => |
81 let |
81 let |
82 (* never give up lock except for waiting *) |
82 (* never give up lock except for waiting *) |
83 val _ = Mutex.lock lock |
83 val _ = Mutex.lock lock |
84 fun wait_for_next_event time = |
84 fun wait_for_next_event time = |
85 let |
85 let |
109 else |
109 else |
110 #1 (ThreadHeap.min (! timeout_heap)) |
110 #1 (ThreadHeap.min (! timeout_heap)) |
111 in |
111 in |
112 wait_for_next_event next_time |
112 wait_for_next_event next_time |
113 end |
113 end |
114 in wait_for_next_event Time.zeroTime end, |
114 in wait_for_next_event Time.zeroTime end) |
115 [Thread.InterruptState Thread.InterruptDefer]) |
115 in managing_thread := SOME new_thread end |
116 in managing_thread := new_thread end |
|
117 |
116 |
118 (* calling thread registers itself to be managed here with a relative timeout *) |
117 (* calling thread registers itself to be managed here with a relative timeout *) |
119 fun register birthtime deadtime (thread, name) = |
118 fun register birthtime deadtime (thread, name) = |
120 let |
119 let |
121 val _ = Mutex.lock lock |
120 val _ = Mutex.lock lock |
122 (* create the atp-managing-thread if this is the first call to register *) |
121 (* create the atp-managing-thread if this is the first call to register *) |
123 val _ = if Thread.isActive (! managing_thread) then () else start () |
122 val _ = |
|
123 if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false) |
|
124 then () else start () |
124 (* insertion *) |
125 (* insertion *) |
125 val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread)) |
126 val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread)) |
126 val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread)) |
127 val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread)) |
127 val _ = change active (cons (thread, birthtime, deadtime, name)) |
128 val _ = change active (cons (thread, birthtime, deadtime, name)) |
128 (*maximum number of atps must not exceed*) |
129 (*maximum number of atps must not exceed*) |