Here's a quick sketch of a semantics for prophecies. Let's model a multi-threaded mini-Scheme where thread interleaving is represented by non-deterministically choosing a thread from a list of active threads and reducing it one step:
(e1, ..., E[e], e2, ...) → (e1, ..., E[e'], e2, ...)
We also need a store to represent creating and updating prophecy queues. So the rule for cleaning up a terminated thread looks like:
<(e1, ..., v, e2, ...), σ>
→ <(e1, ..., e2, ...), σ>
And beta-reduction occurs in a thread like so:
<(e1, ..., E[((lambda (x) e) v)], e2, ...), σ>
→ <(e1, ..., E[e[v/x]], e2, ...), σ>
Creating a new prophecy causes a new thread to be spawned and allocates a new, empty queue on the store. The prophecy's thread marks its context with the location of the queue so that subsequent calls to
yield will know where to store their values.
<(e1, ..., E[(prophecy e)], e2, ...), σ>
→ <(e1, ..., E[<prophecy: i>], e2, ..., e'), σ[i := <queue:>]>
where e' = (prophecy-context i e)
When yielding a value, we look up the current thread's prophecy context to find its associated queue, and add the value to the queue. (Because this is an atomic step, queue updates are thread-safe.)
<(e1, ..., E[(yield v)], e2, ...), σ>
→ <(e1, ..., E[null], e2, ...), σ[i := <queue: v1, ..., vn, v>]>
where E = (prophecy-context E0)
and σ[i] = <queue: v1, ..., vn>
Finally, reading a prophecy off the queue succeeds whenever the queue is non-empty.
<(e1, ..., E[(prophecy-next <prophecy: i>)], e2, ...), σ>
→ <(e1, ..., E[v1], e2, ...), σ[i := <queue: v2, ..., vn>]>
where E ≠ (prophecy-context i E0)
and σ[i] = <queue: v1, v2, ..., vn>
Conspicuously missing from this first draft: the
stop-iteration exception (because I didn't feel like adding exceptions to the model), and
prophecy->stream, which really can be considered a library function added on top, implementable in a language with
delay and
force by means of a recursive function that produces
null when it catches the
stop-iteration exception.
if i understand correctly, the prophecy mechanism is a way to produce an arbitrary number of values in a non-blocking way, and make those values available for another thread to collect in FIFO order.
ReplyDelete(and then you use the delay and force primitives via the stream abstraction to give the consuming thread a nice way to treat this stream of values as a datastructure.)
(the prophecy-next might have to block if the producing thread hasn't yet yielded more values, right?)
anyway, i think the prophecy semantics are quite similar to that of an infinitely-buffered, asynchronous "channel". for example, using mzscheme's "Buffered Asynchronous Channels" library, it seems that you could implement prophecies like this:
(define current-prophecy-channel (make-parameter #f))
(define (yield v)
(async-channel-put (current-prophecy-channel) v))
(define (prophecy-next p)
(async-channel-get p))
(define (prophecy thunk)
(let ([prophecy-channel (make-async-channel #f)])
(parameterize ([current-prophecy-channel prophecy-channel])
(thread thunk))
prophecy-channel))
(i've left "prophecy" as a function that takes a thunk for simplicity, but a quick macro would give the look you specify.)
with a unique "stop-iteration" value it would be straightforward to write prophecy->stream from prophecy-next.
That is hilarious -- you've just exactly reverse engineered my implementation! Download the PLaneT package and check out the source code. :D
ReplyDeleteha, yes i guess we're on the same page
ReplyDeletewith that one.
in fact, though, the fullness of your
implementation explains why a "prophecy"
is not just a watered-down channel (as
it seemed to me at first).
in particular, you ensure that the
stream of values is terminated when the
prophecy code returns:
(define (build-prophecy thunk)
(let ([ch (make-async-channel)])
(make-prophecy ch (thread (lambda ()
(parameterize ([current-channel ch])
(dynamic-wind void thunk (lambda ()
(yield *done*)))))))))
next, note that in the case of non-local
control flow (perhaps a backtracking
algorithm is yielding the values? work
with me ...) you might end up calling
(yield *done*) multiple times
via the dynamic-wind wrapper. it
appears that this won't effect the
behavior of prophecy-next in
the normal case -- multiple *done*
values won't confuse it. but it might
be cleaner to just do it once, like
this:
(define (build-prophecy thunk)
(let ([ch (make-async-channel)])
(make-prophecy ch (thread (lambda ()
(parameterize ([current-channel ch])
(thunk)
(yield *done*)))))))
of course, there's still the concern
about the case of the thunk not
returning directly, but rather
generating an exception.
in the current implementation, prophecy
code that produces an exception just
stops producing values, and
prophecy-next will give the
stop-iteration exception. but is this
really a "safe" semantics? for example,
if we take at face-value the
prophecy->stream of this
prophecy, we might get the wrong idea:
(prophecy
(set-exhaustion-alarm!)
(yield "the answer to life")
(yield "the universe")
(yield "and everything")
(yield "is ...")
(think)
(yield "forty")
(think) ;; alarm goes off here?
(yield "two"))
that is, we could get a truncated stream
of values without any way to know that
the prophet fell over mid-sentence.
of course, there is a similar problem
with asynchronous channels. but maybe
this is an opportunity for prophecies to
provide useful additional semantics.
what do you think of trying to propagate
exception information from the prophet
to the supplicant? you could wrap the
thunk in a handler that, upon catching
an exception, would pass the exception
message (say) along the channel in a way
that prophecy-next would
understand that it should not return a
normal value, nor raise the
stop-iteration exception, but rather
raise a dead-prophet exception
containing the prophet's dying words?
dang; in the attempt to wrangle my comment into blogger, i lost a part: please mentally insert the following just after the first code citation in my previous comment:
ReplyDelete---
this seems like a useful feature,
because with channels you'd have to
arrange for your own sentinel-passing
scheme to signal the end of data, and it
would be easy to screw up.
one funny thing about the implementation
is that, if you call
prophecy-next after the yielded
values have been exhausted, you'll get a
stop-iteration exception, and then if
you call it again you'll just
hang (on async-channel-get). you
haven't specified yet what semantics you
want here, but it might be more
intuitive to always return the exception
(in the same way that a port returns the
end-of-file object forever).