[m-dev.] for review - new stuff for the extras directory.

[Thomas Conway]

[Harald, I've cc'ed this to you, because I thought you might be interested,
and I can't remember if you get mercury-developers.]
On Tue, Feb 29, 2000 at 12:35:42AM EST, Ralph Becket wrote:
> > From: Ralph Becket [mailto:rbeck at microsoft.com]
> > > extras/concurrency/philo.m:
> > > 	An implementation of the classic dining philosophers program.
> > 
> > I've knocked out an alternative version where each fork is associated
> > with a separate lock and the philosophers use the alternating
> > left-right/right-left strategy to avoid deadlock.
> 
> Oops, just spotted a buglet.  That code should be fine, if somewhat
> inefficient, under pre-emptive scheduling, but may just sit there
> doing nothing under coroutining.  The solution is to change
> 
> :- pred loop_forever.
> :- mode loop_forever is erroneous.
> 
> loop_forever :- loop_forever.
> 
> into...
> 
> :- pred loop_forever(io__state, io__state).
> :- mode loop_forever(di, uo) is det.
> 
> loop_forever --> yield, loop_forever.

Hmmm, it looks like my reply turned into a more detailed explanation
of my semantics of coroutining than I set out for, but never mind...
I was just going to point out that your loop_forever (not having seen
how you use it yet), is unlikely to do anything useful.

In the coroutining view of the world, in

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

`IO0' and `IO' are basically a difference pair (in the Prolog sense),
with `IO0' representing a list of all the interactions with the external
world, and `IO' representing all those that happen after main/2.
Now, we can view the universe as operating like this:

?- toms_main(IO0, []), ralphs_main(IO1, []), ...,
	merge_ios([IO0, IO1, ...], IOs), do_world(IOs, Initial, Final).

where `Initial' and `Final' denote inital and final states of the world.

The trick to understanding yield is to look at how merge_ios is implemented.
The following code should be read as Prolog+coroutining (eg NU-Prolog, or
SICStus, or Eclipse). I've used one `when' declaration in the crutial
spot.

Try something like:

:- type io_transaction
	--->	read(T)
	;	write(T)
	...
	;	wait(sem)
	;	signal(sem)
	;	yield
	.

:- type io_transactions == list(io_transaction).

:- pred merge_ios(list(io_transactions), io_transactions).
:- mode merge_ios(some_sort_of_in, some_sort_of_out) is cc_multi.

merge_ios([IO0|IOs0], IOs) :-
	merge_ios(IO0, IOs0, IOs).

merge_ios([IOT|IOTs0], IOs0, IOs) :-
	merge_iot(IOT, IOTs0, IOs0, IOs).

:- merge_iot(X, _, _, _) when bound(X).

merge_iot(write(Thing), IOTs0, IOs0, IOs) :-
	IOs = [write(Thing)|IOs1],
		% We keep doing io_transactions for this stream until
		% it blocks or yields, so we keep putting it back on
		% the front of the "runqueue".
	IOs2 = [IOTs0|IOs0],
	merge_ios(IOs2, IOs1).

merge_iot(read(Thing), IOTs0, IOs0, IOs) :-
	IOs = [read(Thing)|IOs1],
		% ditto
	IOs2 = [IOTs0|IOs0],
	merge_ios(IOs2, IOs1).

merge_iot(wait(Sem), IOTs0, IOs0, IOs) :-
		% oops I should have threaded some internal state about
		% semaphores here. Let's call it Sems0, Sems...
		% The type is:
		% :- type semaphores == map(sem,
		%		pair(int, list(io_transactions))).
	lookup(Sems0, Sem, Val0 - Sus0),
	( Val0 > 0 ->
			% We effectively throw this transaction away,
			% since it functions only to constrain the
			% ordering of transactions, and is not a *real*
			% interaction with the external world.
		set(Sems0, Sem, (Val0 - 1) - Sus0, Sems),
		IOs2 = [IOTs0|IOs0],
		merge_ios(IOs2, IOs)
	;
			% Add this stream of io_transactions to the
			% suspended list for this semaphore:
		set(Sems0, Sem, Val0 - [IOTs0|Sus0], Sems0),
		merge_ios(IOs0, IOs)
	).

merge_iot(signal(Sem), IOTs0, IOs0, IOs) :-
	lookup(Sems0, Sem, Val0 - Sus0),
	( Val0 = 0 ->
		(
				% There aren't any suspended coroutines,
				% so simple set the semaphore to 1.
			Sus0 = [],
			set(Sems0, Sem, 1 - [], Sems),
			IOs2 = [IOTs0|IOs0],
			merge_ios(IOs2, IOs)
		;
				% Wake up one of the coroutines by taking
				% it off the suspended list, and putting it
				% at the front of the runqueue.
			Sus0 = [IOTs1|IOs3],
			set(Sems0, Sem, 0 - IOs3, Sems),
			IOs2 = [IOTs1, IOTs0|IOs0],
			merge_ios(IOs2, IOs)
		)
	;
			% Increment the value of the semaphore.
		% require(unify(Sus0, []), "invariant failed!"),
		set(Sems0, Sem, (Val0 + 1) - Sus0, Sems),
		IOs2 = [IOTs0|IOs0],
		merge_ios(IOs2, IOs)
	).

merge_iot(yield, IOTs0, IOs0, IOs) :-
		% simply put this coroutine at the end of the runqueue.
	append(IOs0, [IOTs0], IOs2),
	merge_ios(IOs2, IOs).

Now wrt the modes: as you know we always pass the io__state in the modes
di and uo, which correspond to ground, unique insts, but here am I using
difference lists - partially instantiated objects all over the place.
Fortunately, di and uo, because they are unique, are as conservative as
things can get, so in fact, if we had a mode system that could express the
partially instantiated modes for the difference list in my program,
nothing I could do with an io__state pair in (di, uo) modes would be
invalid. To me it's kind of obvious, so tell me if you don't get it and
I'll try to explain it better.

WRT to determinism: you'll notice that I declared merge_ios as being
cc_multi, not det, but all the code I've written is in fact det. That's
because, even if I executed this whole thing under SICStus or NU-Prolog,
it doesn't quite implement the operational behaviour I intend. I make
deterministic choices in several places, where in reality, I will get
(in some cases whether I want them or not) non-deterministic choices:
	- the code always chooses the first thing on the runqueue and may
	  block at the `when' declaration until it gets a message. In
	  practice, I'd want it to make a nondeterministic choice of which
	  coroutine for which to do the next IO operation, always guessing
	  luckily the one that happens to have an operation ready to go,
	  so I never actually block. This is something that I can't actually
	  implement in the logic (no calls to var/1 here!), so it gets left
	  to angelic nondeterminism.
	- which coroutine I choose to wake after a signal
	- actual IO operations block: in practice, if a read cannot
	  succeed right away, I'd like to queue it and get on with another
	  coroutine and come back to it when it has completed.
	- I might be running several Mercury engines, across multiple
	  processors, so OS scheduling etc will cause nondeterminism in
	  the order in which messages arrive on the various streams.

In case you were wondering, this is the reason that spawn/3 is cc_multi:
in the semantics, we could implement it in the following way:

spawn(Closure, IOs0, IOs) :-
	call(Closure, IOs1, []),
	merge_ios([IOs1, IOs], IOs0).

(Yes, the numbering of the variables is correct.)
Now, that works, but we have to engage in some fiddly business to get
semaphores working correctly, so instead, we can make spawn/3 itself
an io_transaction, adding the constructor to the type:
	;	spawn(pred(io_transactions, io_transactions))

which we then handle in the following way:

merge_iot(spawn(Coroutine), IOTs0, IOs0, IOs) :-
	call(Coroutine, IOTs1, []),
	merge_ios([IOTs0, IOTs1|IOs0], IOs).

and spawn is implemented:

spawn(Closure, [spawn(Closure)|IOs], IOs).

Now spawn itself is det, as indeed is main! All the IO transactions
are det - just consing onto a list. All the nondeterminism happens
outside at the toplevel in the call to merge_ios! However, we make
spawn cc_multi, and therefore main also, because it better reflects
the meaning of what we have written.
-- 
 Thomas Conway )O+     Every sword has two edges.
     Mercurian            <conway at cs.mu.oz.au>
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------