[mercury-users] declarative kernels

[Thomas Conway]

On Sat, Mar 04, 2000 at 12:01:15PM EST, Michael Day wrote:
> 
> Hi,
> 
> given the recent discussion of coroutines and concurrency, does anyone
> have any references to declarative operating system kernels, or work being
> done in this area? What exactly does io__state represent, when it's being
> passed to multiple programs by another underlying program?

There are two interpretations of the io__state.

The first, proposed by Fergus, is that the io__state represents the state
of the external world, and that I/O operations modify the external state.
This has the drawback that if, for example someone else on the system
removes a file between when you finished writing it, and when you go to
read it again, then the act of closing the file has to implicitly remove
it as well, which is a bit strange, but it is a fairly simple model.

More recently I proposed an interpretation that owes a lot to concurrent
logic programming, where the io__state represents a list of interactions
with the external world. The io__state pair represents a difference list
(in the Prolog sense), with the second io__state representing the I/O
operations that come "after".

So, considering main:

main(IO0, IO) :-
	....

we interpret `IO0' as representing the list of I/O interactions performed
by my program, followed by all those which come after (represented by `IO').

You can then visualise the external world being the goal:

?- my_main(IO0, []), your_main(IO1, []), merge(IO0, IO1, IO), do_io(IO).

Where merge/3 performs some nondeterministic interleaving of the I/O
operations contained in the first two arguments.

This gives a more natural interpretation for what happens if someone else
removes a file, or whatever. It also provides a natural framework for
coroutining and concurrency. Using this interpretation of I/O, we can give
a defensible semantics to threads. I refer you to the mercury-developers
archives for more info. Search for `spawn'.

Thomas
-- 
 Thomas Conway )O+     Every sword has two edges.
     Mercurian            <conway at cs.mu.oz.au>
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------