src/Pure/Concurrent/single_assignment.ML
author wenzelm
Sun, 05 Nov 2017 12:13:27 +0100
changeset 67009 b68592732783
parent 64276 622f4e4ac388
child 68589 9258f16d68b4
permissions -rw-r--r--
testing NewTestRegisterSave;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/single_assignment.ML
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     3
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     4
Single-assignment variables with locking/signalling.
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     5
*)
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     6
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     7
signature SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     8
sig
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
     9
  type 'a var
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    10
  val var: string -> 'a var
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    11
  val peek: 'a var -> 'a option
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    12
  val await: 'a var -> 'a
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    13
  val assign: 'a var -> 'a -> unit
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    14
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    15
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    16
structure Single_Assignment: SINGLE_ASSIGNMENT =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    17
struct
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    18
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    19
abstype 'a var = Var of
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    20
 {name: string,
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    21
  lock: Mutex.mutex,
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    22
  cond: ConditionVar.conditionVar,
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    23
  var: 'a SingleAssignment.saref}
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    24
with
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    25
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    26
fun var name = Var
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    27
 {name = name,
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    28
  lock = Mutex.mutex (),
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    29
  cond = ConditionVar.conditionVar (),
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    30
  var = SingleAssignment.saref ()};
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    31
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    32
fun peek (Var {var, ...}) = SingleAssignment.savalue var;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    33
37906
4195727a1f6c eliminated some unreferenced identifiers;
wenzelm
parents: 37216
diff changeset
    34
fun await (v as Var {name, lock, cond, ...}) =
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 47422
diff changeset
    35
  Multithreading.synchronized name lock (fn () =>
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    36
    let
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    37
      fun wait () =
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    38
        (case peek v of
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    39
          NONE =>
64276
622f4e4ac388 eliminated unused argument;
wenzelm
parents: 62923
diff changeset
    40
            (case Multithreading.sync_wait NONE cond lock of
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 37906
diff changeset
    41
              Exn.Res _ => wait ()
62505
9e2a65912111 clarified modules;
wenzelm
parents: 59054
diff changeset
    42
            | Exn.Exn exn => Exn.reraise exn)
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    43
        | SOME x => x);
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    44
    in wait () end);
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    45
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    46
fun assign (v as Var {name, lock, cond, var}) x =
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 47422
diff changeset
    47
  Multithreading.synchronized name lock (fn () =>
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    48
    (case peek v of
47422
5832630f049a tuned message;
wenzelm
parents: 43761
diff changeset
    49
      SOME _ => raise Fail ("Duplicate assignment to " ^ name)
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    50
    | NONE =>
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62891
diff changeset
    51
        Thread_Attributes.uninterruptible (fn _ => fn () =>
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    52
         (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    53
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    54
end;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    55
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    56
end;