synchronized access, similar to ML version;
authorwenzelm
Thu Apr 24 12:09:55 2014 +0200 (2014-04-24)
changeset 566928219a65b24e3
parent 56691 ad5d7461b370
child 56693 0423c957b081
synchronized access, similar to ML version;
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/synchronized.scala
     1.1 --- a/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 11:01:14 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/synchronized.ML	Thu Apr 24 12:09:55 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  structure Synchronized: SYNCHRONIZED =
     1.5  struct
     1.6  
     1.7 -(* state variables *)
     1.8 +(* state variable *)
     1.9  
    1.10  abstype 'a var = Var of
    1.11   {name: string,
     2.1 --- a/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 11:01:14 2014 +0200
     2.2 +++ b/src/Pure/Concurrent/synchronized.scala	Thu Apr 24 12:09:55 2014 +0200
     2.3 @@ -8,6 +8,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.annotation.tailrec
     2.8 +
     2.9 +
    2.10  object Synchronized
    2.11  {
    2.12    def apply[A](init: A): Synchronized[A] = new Synchronized(init)
    2.13 @@ -16,14 +19,59 @@
    2.14  
    2.15  final class Synchronized[A] private(init: A)
    2.16  {
    2.17 +  /* state variable */
    2.18 +
    2.19    private var state: A = init
    2.20 +
    2.21    def value: A = synchronized { state }
    2.22 +  override def toString: String = value.toString
    2.23 +
    2.24 +
    2.25 +  /* synchronized access */
    2.26 +
    2.27 +  def timed_access[B](time_limit: A => Option[Time], f: A => Option[(B, A)]): Option[B] =
    2.28 +    synchronized {
    2.29 +      def check(x: A): Option[B] =
    2.30 +        f(x) match {
    2.31 +          case None => None
    2.32 +          case Some((y, x1)) =>
    2.33 +            state = x1
    2.34 +            notifyAll()
    2.35 +            Some(y)
    2.36 +        }
    2.37 +      @tailrec def try_change(): Option[B] =
    2.38 +      {
    2.39 +        val x = state
    2.40 +        check(x) match {
    2.41 +          case None =>
    2.42 +            time_limit(x) match {
    2.43 +              case Some(t) =>
    2.44 +                val timeout = (t - Time.now()).ms
    2.45 +                if (timeout > 0L) {
    2.46 +                  wait(timeout)
    2.47 +                  check(state)
    2.48 +                }
    2.49 +                else None
    2.50 +              case None =>
    2.51 +                wait()
    2.52 +                try_change()
    2.53 +            }
    2.54 +          case some => some
    2.55 +        }
    2.56 +      }
    2.57 +      try_change()
    2.58 +    }
    2.59 +
    2.60 +  def guarded_access[B](f: A => Option[(B, A)]): B =
    2.61 +    timed_access(_ => None, f).get
    2.62 +
    2.63 +
    2.64 +  /* unconditional change */
    2.65 +
    2.66    def change(f: A => A) = synchronized { state = f(state) }
    2.67    def change_result[B](f: A => (B, A)): B = synchronized {
    2.68      val (result, new_state) = f(state)
    2.69      state = new_state
    2.70      result
    2.71    }
    2.72 -
    2.73 -  override def toString: String = state.toString
    2.74  }