(*  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: int ref

  val max_threads_value: unit -> int

  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 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;

val max_threads = ref (1: int);

fun max_threads_value () = 1: int;

fun enabled () = false;

(* attributes *)

val no_interrupts = [];

val public_interrupts = [];

val private_interrupts = [];

fun sync_interrupts _ = [];

fun with_attributes _ e = e [];

fun sync_wait _ _ _ _ = Exn.Result 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;