author | wenzelm |
Sun, 09 Mar 2014 17:02:18 +0100 | |
changeset 56003 | eccac152ffb4 |
parent 52583 | 0a7240d88e09 |
child 57417 | 29fe9bac501b |
permissions | -rw-r--r-- |
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/mailbox.ML |
28140 | 2 |
Author: Makarius |
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
3 |
|
28579 | 4 |
Message exchange via mailbox, with non-blocking send (due to unbounded |
5 |
queueing) and potentially blocking receive. |
|
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
6 |
*) |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
7 |
|
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
8 |
signature MAILBOX = |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
9 |
sig |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
10 |
type 'a T |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
11 |
val create: unit -> 'a T |
28170 | 12 |
val send: 'a T -> 'a -> unit |
28579 | 13 |
val receive: 'a T -> 'a |
28139 | 14 |
val receive_timeout: Time.time -> 'a T -> 'a option |
52583 | 15 |
val await_empty: 'a T -> unit |
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
16 |
end; |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
17 |
|
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
18 |
structure Mailbox: MAILBOX = |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
19 |
struct |
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
20 |
|
28576
dc4aae271c41
simplified implementation using Synchronized.var;
wenzelm
parents:
28443
diff
changeset
|
21 |
datatype 'a T = Mailbox of 'a Queue.T Synchronized.var; |
28579 | 22 |
|
28576
dc4aae271c41
simplified implementation using Synchronized.var;
wenzelm
parents:
28443
diff
changeset
|
23 |
fun create () = Mailbox (Synchronized.var "mailbox" Queue.empty); |
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
24 |
|
28579 | 25 |
fun send (Mailbox mailbox) msg = |
26 |
Synchronized.change mailbox (Queue.enqueue msg); |
|
28139 | 27 |
|
28579 | 28 |
fun receive (Mailbox mailbox) = |
29 |
Synchronized.guarded_access mailbox (try Queue.dequeue); |
|
30 |
||
28576
dc4aae271c41
simplified implementation using Synchronized.var;
wenzelm
parents:
28443
diff
changeset
|
31 |
fun receive_timeout timeout (Mailbox mailbox) = |
28579 | 32 |
Synchronized.timed_access mailbox |
33 |
(fn _ => SOME (Time.+ (Time.now (), timeout))) (try Queue.dequeue); |
|
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
34 |
|
52583 | 35 |
fun await_empty (Mailbox mailbox) = |
36 |
Synchronized.guarded_access mailbox |
|
37 |
(fn queue => if Queue.is_empty queue then SOME ((), queue) else NONE); |
|
38 |
||
28135
4f6f0496e93c
Concurrent message exchange via mailbox -- with unbounded queueing.
wenzelm
parents:
diff
changeset
|
39 |
end; |