I think I like it. Just to clarify: when you fork a new Haskell thread, it isn't associated with a native thread, right?
Right. I said so in \subsection{Initial State}.
(the semantics doesn't model forkIO, I think it probably should).
OK, I'll add it to the semantics.
If true, that gives us the important principle that
At any one time, there is at most one runnable Haskell thread associated with, or bound to, any given native thread.
Exactly. I'll make sure it's mentioned somewhere. (Also, a Haskell thread cannot be bound to a native thread that already has a different Haskell thread associated with it).
which is important for reducing the complexity of the implementation. In an implementation which actually runs the Haskell thread in its bound native thread (eg. GHC), we can be sure that when we want to switch to the bound native thread it isn't off doing something else. Is that the reason for wanting this property?
Yes, that's what I was thinking. I think I'll try to implement a prototype soon (unless someone protests quickly and loudly), because I have no courses at the university for one more week (3 weeks of Easter break), so I have some free time that I won't have afterwards. Cheers, Wolfgang