src/Pure/ML-Systems/multithreading.ML

more contributors;

(*  Title:      Pure/ML-Systems/multithreading.ML
    Author:     Makarius

Dummy implementation of multithreading setup.
*)

signature BASIC_MULTITHREADING =
sig
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
  val CRITICAL: (unit -> 'a) -> 'a
end;

signature MULTITHREADING =
sig
  include BASIC_MULTITHREADING
  val available: bool
  val max_threads_value: unit -> int
  val max_threads_update: int -> unit
  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
  val enabled: unit -> bool
  val no_interrupts: Thread.threadAttribute list
  val public_interrupts: Thread.threadAttribute list
  val private_interrupts: Thread.threadAttribute list
  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
  val interrupted: unit -> unit  (*exception Interrupt*)
  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
  val trace: int ref
  val tracing: int -> (unit -> string) -> unit
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
  val real_time: ('a -> unit) -> 'a -> Time.time
  val self_critical: unit -> bool
  val serial: unit -> int
end;

structure Multithreading: MULTITHREADING =
struct

(* options *)

val available = false;
fun max_threads_value () = 1: int;
fun max_threads_update _ = ();
fun max_threads_setmp _ f x = f x;
fun enabled () = false;


(* attributes *)

val no_interrupts = [];
val public_interrupts = [];
val private_interrupts = [];
fun sync_interrupts _ = [];

fun interrupted () = ();

fun with_attributes _ e = e [];

fun sync_wait _ _ _ _ = Exn.Res true;


(* tracing *)

val trace = ref (0: int);
fun tracing _ _ = ();
fun tracing_time _ _ _ = ();
fun real_time f x = (f x; Time.zeroTime);


(* critical section *)

fun self_critical () = false;
fun NAMED_CRITICAL _ e = e ();
fun CRITICAL e = e ();


(* serial numbers *)

local val count = ref (0: int)
in fun serial () = (count := ! count + 1; ! count) end;

end;

structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
open Basic_Multithreading;