Quelle single_assignment.ML Sprache: SML

(*  Title:      Pure/Concurrent/single_assignment.ML
    Author:     Makarius

Single-assignment variables with locking/signalling.
*)

signature SINGLE_ASSIGNMENT =
sig
  type 'a var
  val var: string -> 'a var
  val peek: 'a var -> 'a option
  val await: 'a var -> 'a
  val assign: 'a var -> 'a -> unit
end;

structure Single_Assignment: SINGLE_ASSIGNMENT =
struct

datatype 'a state =
    Set of 'a
  | Unset of {lock: Thread.Mutex.mutex, cond: Thread.ConditionVar.conditionVar};

fun init_state () =
  Unset {lock = Thread.Mutex.mutex (), cond = Thread.ConditionVar.conditionVar ()};

abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
with

fun var name = Var {name = name, state = Unsynchronized.ref (init_state ())};

fun peek (Var {name, state}) =
  (case ! state of
    Set x => SOME x
  | Unset {lock, ...} =>
      Multithreading.synchronized name lock (fn () =>
        (case ! state of
          Set x => SOME x
        | Unset _ => NONE)));

fun await (Var {name, state}) =
  (case ! state of
    Set x => x
  | Unset {lock, cond} =>
      Multithreading.synchronized name lock (fn () =>
        let
          fun wait () =
            (case ! state of
              Unset _ =>
                (case Multithreading.sync_wait NONE cond lock of
                  Exn.Res _ => wait ()
                | Exn.Exn exn => Exn.reraise exn)
            | Set x => x);
        in wait () end));

fun assign_fail name = raise Fail ("Duplicate assignment to " ^ name);
fun assign (Var {name, state}) x =
  (case ! state of
    Set _ => assign_fail name
  | Unset {lock, cond} =>
      Multithreading.synchronized name lock (fn () =>
        (case ! state of
          Set _ => assign_fail name
        | Unset _ =>
            Thread_Attributes.uninterruptible_body (fn _ =>
             (state := Set x; RunCall.clearMutableBit state;
               Thread.ConditionVar.broadcast cond)))));

end;

end;

quality99%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.