src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sun Sep 07 22:20:11 2008 +0200 (2008-09-07)
changeset 28160 e0177b67ecd9
parent 28149 26bd1245a46b
child 28169 356fc8734741
permissions -rw-r--r--
added sync_interrupts, regular_interrupts;
wenzelm@24690
     1
(*  Title:      Pure/ML-Systems/multithreading.ML
wenzelm@24690
     2
    ID:         $Id$
wenzelm@24690
     3
    Author:     Makarius
wenzelm@24690
     4
wenzelm@28149
     5
Dummy implementation of multithreading setup.
wenzelm@24690
     6
*)
wenzelm@24690
     7
wenzelm@25704
     8
signature BASIC_MULTITHREADING =
wenzelm@25704
     9
sig
wenzelm@25704
    10
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
wenzelm@25704
    11
  val CRITICAL: (unit -> 'a) -> 'a
wenzelm@25704
    12
end;
wenzelm@25704
    13
wenzelm@24690
    14
signature MULTITHREADING =
wenzelm@24690
    15
sig
wenzelm@25704
    16
  include BASIC_MULTITHREADING
wenzelm@24690
    17
  val trace: int ref
wenzelm@24690
    18
  val tracing: int -> (unit -> string) -> unit
wenzelm@24690
    19
  val available: bool
wenzelm@24690
    20
  val max_threads: int ref
wenzelm@25775
    21
  val max_threads_value: unit -> int
wenzelm@28149
    22
  val no_interrupts: Thread.threadAttribute list
wenzelm@28160
    23
  val sync_interrupts: Thread.threadAttribute list
wenzelm@28160
    24
  val regular_interrupts: Thread.threadAttribute list
wenzelm@28160
    25
  val with_attributes: Thread.threadAttribute list ->
wenzelm@28160
    26
    (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
wenzelm@24690
    27
  val self_critical: unit -> bool
wenzelm@25704
    28
  val serial: unit -> int
wenzelm@24690
    29
end;
wenzelm@24690
    30
wenzelm@24690
    31
structure Multithreading: MULTITHREADING =
wenzelm@24690
    32
struct
wenzelm@24690
    33
wenzelm@25735
    34
(* options *)
wenzelm@25735
    35
wenzelm@24690
    36
val trace = ref (0: int);
wenzelm@24690
    37
fun tracing _ _ = ();
wenzelm@24690
    38
wenzelm@24690
    39
val available = false;
wenzelm@24690
    40
val max_threads = ref (1: int);
wenzelm@25775
    41
fun max_threads_value () = Int.max (! max_threads, 1);
wenzelm@24690
    42
wenzelm@28149
    43
val no_interrupts = [];
wenzelm@28160
    44
val sync_interrupts = [];
wenzelm@28160
    45
val regular_interrupts = [];
wenzelm@28160
    46
wenzelm@28160
    47
fun with_attributes _ f x = f [] x;
wenzelm@28149
    48
wenzelm@25735
    49
wenzelm@25735
    50
(* critical section *)
wenzelm@25735
    51
wenzelm@24690
    52
fun self_critical () = false;
wenzelm@24690
    53
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    54
fun CRITICAL e = e ();
wenzelm@24690
    55
wenzelm@25735
    56
wenzelm@25735
    57
(* serial numbers *)
wenzelm@25735
    58
wenzelm@25704
    59
local val count = ref (0: int)
wenzelm@25704
    60
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    61
wenzelm@28123
    62
end;
wenzelm@28123
    63
wenzelm@28123
    64
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@28123
    65
open BasicMultithreading;