src/Pure/Concurrent/synchronized.scala
author wenzelm
Thu Apr 24 13:10:42 2014 +0200 (2014-04-24)
changeset 56694 c4e77643aad6
parent 56692 8219a65b24e3
child 64370 865b39487b5d
permissions -rw-r--r--
proper signaling after each state update (NB: ML version does this uniformly via timed_access);
wenzelm@56685
     1
/*  Title:      Pure/Concurrent/synchronized.scala
wenzelm@56685
     2
    Module:     PIDE
wenzelm@56685
     3
    Author:     Makarius
wenzelm@56685
     4
wenzelm@56685
     5
Synchronized variables.
wenzelm@56685
     6
*/
wenzelm@56685
     7
wenzelm@56685
     8
package isabelle
wenzelm@56685
     9
wenzelm@56685
    10
wenzelm@56692
    11
import scala.annotation.tailrec
wenzelm@56692
    12
wenzelm@56692
    13
wenzelm@56685
    14
object Synchronized
wenzelm@56685
    15
{
wenzelm@56685
    16
  def apply[A](init: A): Synchronized[A] = new Synchronized(init)
wenzelm@56685
    17
}
wenzelm@56685
    18
wenzelm@56685
    19
wenzelm@56685
    20
final class Synchronized[A] private(init: A)
wenzelm@56685
    21
{
wenzelm@56692
    22
  /* state variable */
wenzelm@56692
    23
wenzelm@56685
    24
  private var state: A = init
wenzelm@56692
    25
wenzelm@56687
    26
  def value: A = synchronized { state }
wenzelm@56692
    27
  override def toString: String = value.toString
wenzelm@56692
    28
wenzelm@56692
    29
wenzelm@56692
    30
  /* synchronized access */
wenzelm@56692
    31
wenzelm@56692
    32
  def timed_access[B](time_limit: A => Option[Time], f: A => Option[(B, A)]): Option[B] =
wenzelm@56692
    33
    synchronized {
wenzelm@56692
    34
      def check(x: A): Option[B] =
wenzelm@56692
    35
        f(x) match {
wenzelm@56692
    36
          case None => None
wenzelm@56692
    37
          case Some((y, x1)) =>
wenzelm@56692
    38
            state = x1
wenzelm@56692
    39
            notifyAll()
wenzelm@56692
    40
            Some(y)
wenzelm@56692
    41
        }
wenzelm@56692
    42
      @tailrec def try_change(): Option[B] =
wenzelm@56692
    43
      {
wenzelm@56692
    44
        val x = state
wenzelm@56692
    45
        check(x) match {
wenzelm@56692
    46
          case None =>
wenzelm@56692
    47
            time_limit(x) match {
wenzelm@56692
    48
              case Some(t) =>
wenzelm@56692
    49
                val timeout = (t - Time.now()).ms
wenzelm@56692
    50
                if (timeout > 0L) {
wenzelm@56692
    51
                  wait(timeout)
wenzelm@56692
    52
                  check(state)
wenzelm@56692
    53
                }
wenzelm@56692
    54
                else None
wenzelm@56692
    55
              case None =>
wenzelm@56692
    56
                wait()
wenzelm@56692
    57
                try_change()
wenzelm@56692
    58
            }
wenzelm@56692
    59
          case some => some
wenzelm@56692
    60
        }
wenzelm@56692
    61
      }
wenzelm@56692
    62
      try_change()
wenzelm@56692
    63
    }
wenzelm@56692
    64
wenzelm@56692
    65
  def guarded_access[B](f: A => Option[(B, A)]): B =
wenzelm@56692
    66
    timed_access(_ => None, f).get
wenzelm@56692
    67
wenzelm@56692
    68
wenzelm@56692
    69
  /* unconditional change */
wenzelm@56692
    70
wenzelm@56694
    71
  def change(f: A => A): Unit = synchronized { state = f(state); notifyAll() }
wenzelm@56694
    72
wenzelm@56687
    73
  def change_result[B](f: A => (B, A)): B = synchronized {
wenzelm@56685
    74
    val (result, new_state) = f(state)
wenzelm@56685
    75
    state = new_state
wenzelm@56694
    76
    notifyAll()
wenzelm@56685
    77
    result
wenzelm@56685
    78
  }
wenzelm@56685
    79
}