[m-dev.] Stream2000

[Fergus Henderson]

On 01-Nov-2000, Peter Ross <peter.ross at miscrit.be> wrote:
> On Wed, Nov 01, 2000 at 08:20:15AM +1100, Fergus Henderson wrote:
> > On 31-Oct-2000, Peter Ross <peter.ross at miscrit.be> wrote:
> > > The only issue I have with this version is that it makes heavy use of
> > > existential types.  It seems once you start using them you just have to
> > > keep using them.
> > 
> > Why not use abstract types rather than existential types?
>
> Abstract types are problematic when the stream has more then one extra
> property.

Hmm, I don't see why...

> For example putback and linenumbers would be encoded as the type
> putback(linenumber(S)) or linenumber(putback(S)) both of which are
> equally valid.

Ok, fine so far.

> Now you have a pred which requires putback stream
> 
> :- pred p(putback(S), io__state, io__state) <= stream__input(S).

Declaring `p' like that is not a good idea.  I meant "use abstract
types _and_ type classes rather than existential types and type
classes", not "use abstract types (alone) rather than existential
types and type classes".

So `p' should have type

	:- pred p(S, io__state, io__state) <= stream__putback(S).

> So I don't think that you can get away from using existential types.

Your example only shows that we can't get away from using type classes.

> > For cases where simultaneous access from multiple threads is desired,
> > we could define a `synchronized(S)' type (like the `putback(S)' type)
> > that adds a mutex to the stream type and that locks this mutax before
> > each operation and unlocks it afterwards.  The implementation would
> > probably need to use try_io to ensure that the stream gets unlocked if
> > an exception is thrown.  But this would probably be quite inefficient
> > compared to unsynchronized streams, so I don't think we want to make
> > it the default.
>
> Also you need to make sure that when constructing a synchronised stream,
> that the synchronisation is the last property that is added to the
> stream.

One way to help do that is to make the synchronized streams have
putback iff the underlying stream does, but not vice versa.

E.g.

	:- type synchronized_stream(S) --->
		synchronized_stream(lock::mutex, stream::S).
	:- type putback_stream(S) ---> ...

	:- typeclass synchronized(S) <= stream(S) where [
		pred acquire_lock(...),
		pred release_lock(...)
	].
	:- typeclass putback(S) <= input(S) where [
		pred putback_char(S::in, char::in,
				io__state::di, io__state::uo) is det
	].

	:- instance putback(synchronized_stream(S)) <= putback(S) where [
		putback_char(S, Char) -->
			acquire_lock(S^lock),
			putback_char(S^stream, Char)
			release_lock(S^lock)
	].

	% Deliberately NO instance declaration for
 	% :- instance synchronized(putback_stream(S))

The programmer can still screw up by using a
putback(synchronized(...)) stream from multiple threads,
but people writing code that will access streams from
multiple threads can document that by using a `synchronize_stream'
type class and the compiler will then check it.

> > > :- pragma promise_pure(putback_putback_char/4).
> > > putback_putback_char(pb(_Stream, MPutbackChars), Char) -->
> > > 	{ impure get_mutvar(MPutbackChars, PutbackChars) },
> > > 	{ impure set_mutvar(MPutbackChars, [Char | PutbackChars] ) }.
> > 
> > Both of these operations are non-atomic and so might result in inconsistent
> > behaviour if performed simultaneously from multiple threads.
>
> Using the concurrency mutvar would avoid this problem.

Using mutvar type from extras/concurrency would guarantee that
each get_mutvar or set_mutvar operation is atomic, but it
wouldn't guarantee that the putback_char operation itself is atomic,
and so you might get inconsistent results where e.g.
two threads both try to put back chars on the stream
at the same time, and both operations succeed,
but only one char has actually been pushed,
because the order of operations went

time	thread 1		thread 2
1	get_mutvar(A, B)
2				get_mutvar(A, B)
3	set_mutvar(A, [C1|B])
4				set_mutvar(A, [C2|B])

and the second set_mutvar thus overwrote the value
set in the first set_mutvar.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------