author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 71144 | d6b9dead8c8d |
child 78864 | 2024a2298d7a |
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 |
||
75393 | 11 |
object Mailbox { |
56693 | 12 |
def apply[A]: Mailbox[A] = new Mailbox[A]() |
13 |
} |
|
14 |
||
15 |
||
75393 | 16 |
class Mailbox[A] private() { |
61590 | 17 |
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
|
18 |
override def toString: String = mailbox.value.reverse.mkString("Mailbox(", ",", ")") |
56693 | 19 |
|
57417
29fe9bac501b
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents:
56693
diff
changeset
|
20 |
def send(msg: A): Unit = mailbox.change(msg :: _) |
56693 | 21 |
|
71144 | 22 |
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
|
23 |
(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
|
24 |
{ case Nil => None case msgs => Some((msgs, Nil)) }) getOrElse Nil).reverse |
56693 | 25 |
|
26 |
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
|
27 |
mailbox.guarded_access({ case Nil => Some(((), Nil)) case _ => None }) |
56693 | 28 |
} |