src/Pure/Concurrent/single_assignment.ML
author wenzelm
Wed, 11 Apr 2012 13:37:46 +0200
changeset 47422 5832630f049a
parent 43761 e72ba84ae58f
child 59054 61b723761dff
permissions -rw-r--r--
tuned message;
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, ...}) =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35014
diff changeset
    35
  Simple_Thread.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 =>
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    40
            (case Multithreading.sync_wait NONE NONE cond lock of
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 37906
diff changeset
    41
              Exn.Res _ => wait ()
35014
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    42
            | Exn.Exn exn => reraise exn)
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 =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35014
diff changeset
    47
  Simple_Thread.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 =>
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    51
        uninterruptible (fn _ => fn () =>
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;
a725ff6ead26 explicit representation of single-assignment variables;
wenzelm
parents:
diff changeset
    57