Quelle isabelle_thread.ML Sprache: SML

(*  Title:      Pure/Concurrent/isabelle_thread.ML
    Author:     Makarius

Isabelle-specific thread management.
*)

signature ISABELLE_THREAD =
sig
  type T
  val get_thread: T -> Thread.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 threads_stack_limit: real Unsynchronized.ref
  val default_stack_limit: unit -> int option
  type params
  val params: string -> params
  val stack_limit: int -> params -> params
  val interrupts: params -> params
  val attributes: params -> Thread.Thread.threadAttribute list
  val fork: params -> (unit -> unit) -> T
  val is_active: T -> bool
  val join: T -> unit
  val interrupt: exn
  val interrupt_exn: 'a Exn.result
  val raise_interrupt: unit -> 'a
  val interrupt_thread: T -> unit
  structure Exn: EXN
  val expose_interrupt_result: unit -> unit Exn.result
  val expose_interrupt: unit -> unit  (*exception Exn.is_interrupt*)
  val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
  val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
  val try: (unit -> 'a) -> 'a option
  val can: (unit -> 'a) -> bool
end;

structure Isabelle_Thread: ISABELLE_THREAD =
struct

(* abstract type *)

abstype T = T of {thread: Thread.Thread.thread, name: string, id: int, break: bool Synchronized.var}
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;

fun equal (t1, t2) = Thread.Thread.equal (get_thread t1, get_thread t2);

fun print t =
  (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
    "-" ^ Int.toString (get_id t);

(* self *)

val make_id = Counter.make ();

local
  val self_var = Thread_Data.var () : T Thread_Data.var;
in

fun init_self name =
  let
    val break = Synchronized.var "Isabelle_Thread.break" false;
    val t = make {thread = Thread.Thread.self (), name = name, id = make_id (), break = break};
  in Thread_Data.put self_var (SOME t); t end;

fun self () =
  (case Thread_Data.get self_var of
    SOME t => t
  | NONE => init_self "");

fun is_self t = equal (t, self ());

end;

(* fork *)

val threads_stack_limit = Unsynchronized.ref 0.25;

fun default_stack_limit () =
  let val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0)
  in if limit <= 0 then NONE else SOME limit end;

abstype params = Params of {name: string, stack_limit: int option, interrupts: bool}
with

fun make_params (name, stack_limit, interrupts) =
  Params {name = name, stack_limit = stack_limit, interrupts = interrupts};

fun params name = make_params (name, default_stack_limit (), false);
fun stack_limit limit (Params {name, interrupts, ...}) = make_params (name, SOME limit, interrupts);
fun interrupts (Params {name, stack_limit, ...}) = make_params (name, stack_limit, true);

fun params_name (Params {name, ...}) = name;
fun params_stack_limit (Params {stack_limit, ...}) = stack_limit;
fun params_interrupts (Params {interrupts, ...}) = interrupts;

end;

fun attributes params =
  Thread.Thread.MaximumMLStack (params_stack_limit params) ::
  Thread_Attributes.convert_attributes
    (if params_interrupts params
     then Thread_Attributes.public_interrupts
     else Thread_Attributes.no_interrupts);

fun fork params body =
  let
    val self = Single_Assignment.var "self";
    fun main () =
      let
        val t = init_self (params_name params);
        val _ = Single_Assignment.assign self t;
      in body () end;
    val _ = Thread.Thread.fork (main, attributes params);
  in Single_Assignment.await self end;

(* join *)

val is_active = Thread.Thread.isActive o get_thread;

fun join t =
  while is_active t
  do OS.Process.sleep (seconds 0.1);

(* interrupts *)

val interrupt = Exn.Interrupt_Break;
val interrupt_exn = Exn.Exn interrupt;

fun raise_interrupt () = raise interrupt;

fun interrupt_thread t =
  Synchronized.change (#break (dest t))
    (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b);

fun reset_interrupt () =
  Synchronized.change_result (#break (dest (self ()))) (fn b => (b, false));

fun make_interrupt break = if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown;

fun check_interrupt exn =
  if Exn.is_interrupt_raw exn then make_interrupt (reset_interrupt ()) else exn;

fun check_interrupt_exn result =
  Exn.map_exn check_interrupt result;

structure Exn: EXN =
struct
  open Exn;
  fun capture f x = Res (f x) handle e => Exn (check_interrupt e);
  fun capture_body e = capture e ();
end;

fun expose_interrupt_result () =
  let
    val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
    fun main () =
      (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
       Thread.Thread.testInterrupt ());
    val test = Exn.capture0 main ();
    val _ = Thread_Attributes.set_attributes orig_atts;
    val break = reset_interrupt ();
  in if Exn.is_interrupt_exn test then Exn.Exn (make_interrupt break) else test end;

val expose_interrupt = Exn.release o expose_interrupt_result;

fun try_catch e f =
  Thread_Attributes.uninterruptible_body (fn run =>
    run e () handle exn =>
      if Exn.is_interrupt exn then Exn.reraise (check_interrupt exn) else f exn);

fun try_finally e f =
  Thread_Attributes.uninterruptible_body (fn run =>
    Exn.release (check_interrupt_exn (Exn.capture_body (run e)) before f ()));

fun try e = Basics.try e ();
fun can e = Basics.can e ();

end;

structure Exn = Isabelle_Thread.Exn;

quality99%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.