src/Pure/ML-Systems/multithreading.ML
author wenzelm
Thu, 20 Dec 2007 21:12:02 +0100
changeset 25735 4d147263f71f
parent 25704 df9c8074ff09
child 25775 90525e67ede7
permissions -rw-r--r--
added get/put_data;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/multithreading.ML
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     4
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     5
Dummy implementation of multithreading interface.
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     6
*)
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     7
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
     8
signature BASIC_MULTITHREADING =
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
     9
sig
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    10
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    11
  val CRITICAL: (unit -> 'a) -> 'a
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    12
end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    13
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    14
signature MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    15
sig
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    16
  include BASIC_MULTITHREADING
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    17
  val trace: int ref
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    18
  val tracing: int -> (unit -> string) -> unit
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    19
  val available: bool
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    20
  val max_threads: int ref
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    21
  val self_critical: unit -> bool
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    22
  datatype 'a task =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    23
    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    24
  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    25
  val serial: unit -> int
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    26
  val get_data: 'a Universal.tag -> 'a option
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    27
  val put_data: 'a Universal.tag * 'a -> unit
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    28
end;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    29
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    30
structure Multithreading: MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    31
struct
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    32
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    33
(* options *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    34
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    35
val trace = ref (0: int);
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    36
fun tracing _ _ = ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    37
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    38
val available = false;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    39
val max_threads = ref (1: int);
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    40
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    41
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    42
(* critical section *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    43
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    44
fun self_critical () = false;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    45
fun NAMED_CRITICAL _ e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    46
fun CRITICAL e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    47
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    48
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    49
(* scheduling *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    50
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    51
datatype 'a task =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    52
  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    53
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    54
fun schedule _ _ _ = raise Fail "No multithreading support";
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    55
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    56
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    57
(* serial numbers *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    58
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    59
local val count = ref (0: int)
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    60
in fun serial () = (count := ! count + 1; ! count) end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    61
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    62
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    63
(* thread data *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    64
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    65
local
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    66
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    67
val data = ref ([]: Universal.universal ref list);
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    68
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    69
fun find_data tag =
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    70
  let
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    71
    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    72
      | find [] = NONE;
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    73
  in find (! data) end;
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    74
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    75
in
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    76
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    77
fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    78
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    79
fun put_data (tag, x) =
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    80
  (case find_data tag of
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    81
    SOME r => r := Universal.tagInject tag x
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    82
  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    83
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    84
end;
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    85
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    86
end;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    87
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    88
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    89
open BasicMultithreading;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    90