# HG changeset patch # User wenzelm # Date 1694002167 -7200 # Node ID 852ec09aef1376f7a269821e609790daa0069df2 # Parent 27380538d632c91120368af834e4fc3364b49ca9 more explicit type Isabelle_Thread.T; total operation Isabelle_Thread.self: upgrade raw ML threads implicitly; diff -r 27380538d632 -r 852ec09aef13 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Wed Sep 06 14:09:27 2023 +0200 @@ -26,21 +26,21 @@ structure Thread_Heap = Heap ( - type elem = Time.time * Thread.thread + type elem = Time.time * Isabelle_Thread.T fun ord ((a, _), (b, _)) = Time.compare (a, b) ) -fun lookup_thread xs = AList.lookup Thread.equal xs -fun delete_thread xs = AList.delete Thread.equal xs -fun update_thread xs = AList.update Thread.equal xs +fun lookup_thread xs = AList.lookup Isabelle_Thread.equal xs +fun delete_thread xs = AList.delete Isabelle_Thread.equal xs +fun update_thread xs = AList.update Isabelle_Thread.equal xs type state = - {manager: Thread.thread option, + {manager: Isabelle_Thread.T option, timeout_heap: Thread_Heap.T, active: - (Thread.thread + (Isabelle_Thread.T * (string * Time.time * Time.time * (string * string))) list, - canceling: (Thread.thread * (string * Time.time * (string * string))) list, + canceling: (Isabelle_Thread.T * (string * Time.time * (string * string))) list, messages: (bool * (string * (string * string))) list} fun make_state manager timeout_heap active canceling messages : state = @@ -85,7 +85,7 @@ fun check_thread_manager () = Synchronized.change global_state (fn state as {manager, timeout_heap, active, canceling, messages} => - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state + if (case manager of SOME thread => Isabelle_Thread.is_active thread | NONE => false) then state else let val manager = SOME (make_thread false (fn () => let fun time_limit timeout_heap = @@ -96,14 +96,14 @@ (*action: find threads whose timeout is reached, and interrupt canceling threads*) fun action {manager, timeout_heap, active, canceling, messages} = let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap + Thread_Heap.upto (Time.now (), Isabelle_Thread.self ()) timeout_heap in if null timeout_threads andalso null canceling then NONE else let val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling - val canceling' = filter (Thread.isActive o #1) canceling + val canceling' = filter (Isabelle_Thread.is_active o #1) canceling val state' = make_state manager timeout_heap' active canceling' messages in SOME (map #2 timeout_threads, state') end end @@ -138,7 +138,7 @@ (make_thread true (fn () => let - val self = Thread.self () + val self = Isabelle_Thread.self () val _ = register tool birth_time death_time desc self in unregister (f ()) self end); ()) diff -r 27380538d632 -r 852ec09aef13 src/Pure/Concurrent/event_timer.ML --- a/src/Pure/Concurrent/event_timer.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Wed Sep 06 14:09:27 2023 +0200 @@ -92,7 +92,7 @@ datatype status = Normal | Shutdown_Req | Shutdown_Ack; datatype state = - State of {requests: requests, status: status, manager: Thread.thread option}; + State of {requests: requests, status: status, manager: Isabelle_Thread.T option}; fun make_state (requests, status, manager) = State {requests = requests, status = status, manager = manager}; @@ -128,7 +128,7 @@ then manager_loop () else (); fun manager_check manager = - if is_some manager andalso Thread.isActive (the manager) then manager + if is_some manager andalso Isabelle_Thread.is_active (the manager) then manager else SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} manager_loop); diff -r 27380538d632 -r 852ec09aef13 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Sep 06 14:09:27 2023 +0200 @@ -150,7 +150,7 @@ val queue = Unsynchronized.ref Task_Queue.empty; val next = Unsynchronized.ref 0; -val scheduler = Unsynchronized.ref (NONE: Thread.thread option); +val scheduler = Unsynchronized.ref (NONE: Isabelle_Thread.T option); val canceled = Unsynchronized.ref ([]: group list); val do_shutdown = Unsynchronized.ref false; val max_workers = Unsynchronized.ref 0; @@ -161,7 +161,7 @@ val next_round = seconds 0.05; datatype worker_state = Working | Waiting | Sleeping; -val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); +val workers = Unsynchronized.ref ([]: (Isabelle_Thread.T * worker_state Unsynchronized.ref) list); fun count_workers state = (*requires SYNCHRONIZED*) fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0; @@ -245,18 +245,19 @@ in () end; fun worker_wait worker_state cond = (*requires SYNCHRONIZED*) - (case AList.lookup Thread.equal (! workers) (Thread.self ()) of + (case AList.lookup Isabelle_Thread.equal (! workers) (Isabelle_Thread.self ()) of SOME state => Unsynchronized.setmp state worker_state wait cond | NONE => wait cond); fun worker_next () = (*requires SYNCHRONIZED*) if length (! workers) > ! max_workers then - (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ())); + (Unsynchronized.change workers (AList.delete Isabelle_Thread.equal (Isabelle_Thread.self ())); signal work_available; NONE) else let val urgent_only = count_workers Working > ! max_active in - (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of + (case Unsynchronized.change_result queue + (Task_Queue.dequeue (Isabelle_Thread.self ()) urgent_only) of NONE => (worker_wait Sleeping work_available; worker_next ()) | some => (signal work_available; some)) end; @@ -297,10 +298,10 @@ then ML_statistics () else (); val _ = - if not tick orelse forall (Thread.isActive o #1) (! workers) then () + if not tick orelse forall (Isabelle_Thread.is_active o #1) (! workers) then () else let - val (alive, dead) = List.partition (Thread.isActive o #1) (! workers); + val (alive, dead) = List.partition (Isabelle_Thread.is_active o #1) (! workers); val _ = workers := alive; in Multithreading.tracing 0 (fn () => @@ -374,7 +375,7 @@ do (); last_round := Time.zeroTime); fun scheduler_active () = (*requires SYNCHRONIZED*) - (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); + (case ! scheduler of NONE => false | SOME thread => Isabelle_Thread.is_active thread); fun scheduler_check () = (*requires SYNCHRONIZED*) (do_shutdown := false; @@ -509,7 +510,8 @@ fun join_next atts deps = (*requires SYNCHRONIZED*) if null deps then NONE else - (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of + (case Unsynchronized.change_result queue + (Task_Queue.dequeue_deps (Isabelle_Thread.self ()) deps) of (NONE, []) => NONE | (NONE, deps') => (worker_waiting deps' (fn () => @@ -571,7 +573,7 @@ val (result, job) = future_job group orig_atts (fn () => f x); val task = SYNCHRONIZED "enroll" (fn () => - Unsynchronized.change_result queue (Task_Queue.enroll (Thread.self ()) name group)); + Unsynchronized.change_result queue (Task_Queue.enroll (Isabelle_Thread.self ()) name group)); val _ = worker_exec (task, [job]); in (case Single_Assignment.peek result of @@ -670,7 +672,7 @@ val passive_job = SYNCHRONIZED "fulfill_result" (fn () => Unsynchronized.change_result queue - (Task_Queue.dequeue_passive (Thread.self ()) task)); + (Task_Queue.dequeue_passive (Isabelle_Thread.self ()) task)); in (case passive_job of SOME true => worker_exec (task, [job]) diff -r 27380538d632 -r 852ec09aef13 src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.ML Wed Sep 06 14:09:27 2023 +0200 @@ -6,38 +6,63 @@ signature ISABELLE_THREAD = sig - val is_self: Thread.thread -> bool - val get_name: unit -> string + type T + val get_thread: T -> Thread.thread + val get_name: T -> string + val get_id: T -> int + val equal: T * T -> bool + val print: T -> string + val self: unit -> T + val is_self: T -> bool val stack_limit: unit -> int option type params = {name: string, stack_limit: int option, interrupts: bool} val attributes: params -> Thread.threadAttribute list - val fork: params -> (unit -> unit) -> Thread.thread - val join: Thread.thread -> unit - val interrupt_unsynchronized: Thread.thread -> unit + val fork: params -> (unit -> unit) -> T + val is_active: T -> bool + val join: T -> unit + val interrupt_unsynchronized: T -> unit end; structure Isabelle_Thread: ISABELLE_THREAD = struct +(* abstract type *) + +abstype T = T of {thread: Thread.thread, name: string, id: int} +with + val make = T; + fun dest (T args) = args; +end; + +val get_thread = #thread o dest; +val get_name = #name o dest; +val get_id = #id o dest; + +val equal = Thread.equal o apply2 get_thread; + +fun print t = + (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^ + "-" ^ string_of_int (get_id t); + + (* self *) -fun is_self thread = Thread.equal (Thread.self (), thread); - - -(* unique name *) +val make_id = Counter.make (); local - val name_var = Thread_Data.var () : string Thread_Data.var; - val count = Counter.make (); + val self_var = Thread_Data.var () : T Thread_Data.var; in -fun get_name () = - (case Thread_Data.get name_var of - SOME name => name - | NONE => raise Fail "Isabelle-specific thread required"); +fun set_self t = Thread_Data.put self_var (SOME t); -fun set_name base = - Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ()))); +fun self () = + (case Thread_Data.get self_var of + SOME t => t + | NONE => + let val t = make {thread = Thread.self (), name = "", id = make_id ()} + in set_self t; t end); + +fun is_self t = equal (t, self ()); end; @@ -58,19 +83,26 @@ (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts); fun fork (params: params) body = - Thread.fork (fn () => (set_name (#name params); body ()), attributes params); + let + val name = #name params; + val id = make_id (); + fun main () = (set_self (make {thread = Thread.self (), name = name, id = id}); body ()); + val thread = Thread.fork (main, attributes params); + in make {thread = thread, name = name, id = id} end; (* join *) -fun join thread = - while Thread.isActive thread +val is_active = Thread.isActive o get_thread; + +fun join t = + while is_active t do OS.Process.sleep (seconds 0.1); (* interrupt *) -fun interrupt_unsynchronized thread = - Thread.interrupt thread handle Thread _ => (); +fun interrupt_unsynchronized t = + Thread.interrupt (get_thread t) handle Thread _ => (); end; diff -r 27380538d632 -r 852ec09aef13 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Wed Sep 06 14:09:27 2023 +0200 @@ -35,16 +35,16 @@ val all_passive: queue -> bool val total_jobs: queue -> int val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int} - val cancel: queue -> group -> Thread.thread list - val cancel_all: queue -> group list * Thread.thread list + val cancel: queue -> group -> Isabelle_Thread.T list + val cancel_all: queue -> group list * Isabelle_Thread.T list val finish: task -> queue -> bool * queue - val enroll: Thread.thread -> string -> group -> queue -> task * queue + val enroll: Isabelle_Thread.T -> string -> group -> queue -> task * queue val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue val extend: task -> (bool -> bool) -> queue -> queue option - val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue - val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue - val dequeue_deps: Thread.thread -> task list -> queue -> + val dequeue_passive: Isabelle_Thread.T -> task -> queue -> bool option * queue + val dequeue: Isabelle_Thread.T -> bool -> queue -> (task * (bool -> bool) list) option * queue + val dequeue_deps: Isabelle_Thread.T -> task list -> queue -> (((task * (bool -> bool) list) option * task list) * queue) end; @@ -224,7 +224,7 @@ datatype job = Job of (bool -> bool) list | - Running of Thread.thread | + Running of Isabelle_Thread.T | Passive of unit -> bool; type jobs = job Task_Graph.T; @@ -299,7 +299,7 @@ val _ = cancel_group group Exn.Interrupt; val running = Tasks.fold (fn task => - (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I)) + (case get_job jobs task of Running thread => insert Isabelle_Thread.equal thread | _ => I)) (get_tasks groups (group_id group)) []; in running end; @@ -311,7 +311,7 @@ val _ = cancel_group group Exn.Interrupt; in (case job of - Running t => (insert eq_group group groups, insert Thread.equal t running) + Running t => (insert eq_group group groups, insert Isabelle_Thread.equal t running) | _ => (groups, running)) end; val running = Task_Graph.fold cancel_job jobs ([], []); diff -r 27380538d632 -r 852ec09aef13 src/Pure/Concurrent/timeout.ML --- a/src/Pure/Concurrent/timeout.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Concurrent/timeout.ML Wed Sep 06 14:09:27 2023 +0200 @@ -35,7 +35,7 @@ else Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => let - val self = Thread.self (); + val self = Isabelle_Thread.self (); val start = Time.now (); val request = diff -r 27380538d632 -r 852ec09aef13 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/System/message_channel.ML Wed Sep 06 14:09:27 2023 +0200 @@ -17,7 +17,7 @@ datatype message = Shutdown | Message of XML.body list; -datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Thread.thread}; +datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Isabelle_Thread.T}; fun shutdown (Message_Channel {mbox, thread}) = (Mailbox.send mbox Shutdown; diff -r 27380538d632 -r 852ec09aef13 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Mon Sep 04 21:03:13 2023 +0200 +++ b/src/Pure/Tools/debugger.ML Wed Sep 06 14:09:27 2023 +0200 @@ -22,7 +22,7 @@ if msg = "" then () else Output.protocol_message - (Markup.debugger_output (Isabelle_Thread.get_name ())) + (Markup.debugger_output (Isabelle_Thread.print (Isabelle_Thread.self ()))) [[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]]; val writeln_message = output_message Markup.writelnN; @@ -250,7 +250,7 @@ (SOME (fn (_, break) => if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ()) then - (case try Isabelle_Thread.get_name () of + (case try (Isabelle_Thread.print o Isabelle_Thread.self) () of SOME thread_name => debugger_loop thread_name | NONE => ()) else ()))));