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