author | wenzelm |
Wed, 20 Nov 2019 16:56:03 +0100 | |
changeset 71144 | d6b9dead8c8d |
parent 64370 | 865b39487b5d |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
56693 | 1 |
/* Title: Pure/Concurrent/mailbox.scala |
2 |
Author: Makarius |
|
3 |
||
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
4 |
Message exchange via mailbox, with multiple senders (non-blocking, |
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
5 |
unbounded buffering) and single receiver (bulk messages). |
56693 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
object Mailbox |
|
12 |
{ |
|
13 |
def apply[A]: Mailbox[A] = new Mailbox[A]() |
|
14 |
} |
|
15 |
||
16 |
||
17 |
class Mailbox[A] private() |
|
18 |
{ |
|
61590 | 19 |
private val mailbox = Synchronized[List[A]](Nil) |
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
20 |
override def toString: String = mailbox.value.reverse.mkString("Mailbox(", ",", ")") |
56693 | 21 |
|
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
22 |
def send(msg: A): Unit = mailbox.change(msg :: _) |
56693 | 23 |
|
71144 | 24 |
def receive(timeout: Option[Time] = None): List[A] = |
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
25 |
(mailbox.timed_access(_ => timeout.map(t => Time.now() + t), |
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
26 |
{ case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse |
56693 | 27 |
|
28 |
def await_empty: Unit = |
|
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
29 |
mailbox.guarded_access({ case Nil => Some(((), Nil)) case _ => None }) |
56693 | 30 |
} |