Draft semantics of concurrency and foreign calls.
Note: This document assumes that every function takes exactly one argument. Just imagine that it's the last argument in a fully saturated call.
Foreign export asynchronous
Suppose that a Haskell function
exported function with argument
v, it has the effect of performing
the IO action
⟦f⟧ v, where the translation
⟦f⟧ is defined as
Not specified here is whether the scheduler is allowed to steal a few cycles to run previously forked threads.
N.B. This is just a semantics. We certainly have the option of implementing the entire action completely in the runtime system.
Foreign import asynchronous
g is imported asynchronously
(which might be the default). Let types
b stand for two
a and returns a
Promise that (if successful) eventually
delivers a value of type
b. When a Haskell thunk of the form
is forced (evaluated), the machine performs the following monadic
action, the result of which is (eventually) written into the thunk.
often I would like to use the CPU for a bounded time." It looks like
such that the function associated with that messages is "run Haskell
for N ticks." Is the right API to call
setTimeout with a delay of 0
Let's suppose the state of a Haskell machine has these components:
R("running") is either the currently running Haskell thread, or if no thread is currently running, it is • ("nothing")
Q("run queue") is a collection of runnable threads.
H("heap") is the Haskell heap, which may contain
MVars and threads that are blocked on them.
H are used linearly, so they can be stored in
global mutable state.
The machine will enjoy a set of labeled transitions such as are
described in Simon PJ's paper on the "Awkward Squad." Call these the
"standard transitions." (The awkward-squad machine state is a single
term, formed by the parallel composition of
R with all the threads
Q and all the MVars of
H. The awkward squad doesn't care about
order, but we do.) To specify the standard transitions, we could add
an additional clock that tells the machine when to switch the running
R out for a new thread from the queue. Or we could leave the
context switch nondeterministic, as it is in the awkward-squad paper.
Whatever seems useful.
Every state transition has the potential use to fuel. Fuel might
actually be implemented using an allocation clock, but for semantics
purposes, we can simply decrement fuel at each state transition, then
gate the standard transitions on the condition
F > 0.
At a high level, every invocation of Haskell looks the same:
⟨F, •, Q, H⟩, and
the Haskell machine makes repeated state transitions until it reaches
one of two stopping states:
⟨F',•, , H'⟩: no Haskell threads are left to run
⟨0, ̧R', Q', H'⟩: fuel is exhausted, in which case the machine moves the currently running thread onto the run queue, reaching state
⟨0, ̧•, R':Q', H'⟩
Once one of these states is reached, GHC's runtime system takes two actions:
setTimeoutwith a delay of 0 seconds.