[m-dev.] for review: stream I/O

[Peter Ross]

On Mon, Oct 02, 2000 at 07:08:20PM +1100, Fergus Henderson wrote:
> On 01-Oct-2000, Peter Ross <petdr at miscrit.be> wrote:
> 
> > +% File: stream.m.
> > +% Main author: petdr
> > +% Stability: exceptionally low.
> > +%
> > +% This file provides a typeclass for defining streams in Mercury.
> > +% It is completely pure and you are encouraged to use it to write
> > +% streams in Mercury.  If however you are a library implementor then you
> > +% may want to look at the impure interface described in stream.impure.m
> 
> I suggest s/want to/also want to/
> 
> > +	% Given a handle to a stream construct a unique stream object
> > +	% which can be used to do IO on the stream.
> > +	% This object initialises its state from the io__state.
> > +:- pred stream__init(S::in, stream(S)::uo, io__state::di, io__state::uo) is det.
> > +
> > +	% Tie the stream back into the io__state.  Omitting this call
> > +	% may allow the compiler to optimize away the stream I/O.
> > +:- pred stream__destroy(stream(S)::di, io__state::di, io__state::uo) is det.
> 
> There are some nasty semantic problems with these routines.
> At very least, the documentation is incomplete.
> More likely the interface declared here won't work (i.e. can't be
> implemented in a way that is logically sound and that matches
> their intended semantics).
> 
> The comment for `stream__destroy' explains its purpose, but
> doesn't describe its effect.  What are the declarative and
> operational semantics of `stream__destroy'?
> 
> In the case where there is no call to stream__destroy, the logically
> correct behaviour is for there to be no side effects, except those caused
> by stream__init, and currently stream__init is documented (and
> implemented) in a way that seems to mean that it has no side effects.
> So the comment "Omitting this call may allow the compiler to optimize
> away the stream I/O" is not really correct -- in fact omitting this
> call may result in the implementation *inserting* I/O side effects
> that are not in the program's declarative semantics.
> 
> One alternative would be to say that each call to stream__init
> must be matched by a corresponding call to stream__destroy
> and that if the call to stream__destroy is omitted, then the
> behaviour is undefined.  After all, we already document that
> you get undefined behaviour in the case where you try to write
> to a stream that has already been closed, so why not here too?
> 
> However, I wouldn't consider that acceptable.  There's a fundamental
> difference between the two cases.
> 
> For writes to closed files, an implementation can easily ensure that
> the behaviour is defined, e.g. throwing an exception, it's just that
> doing so comes at a performance or portability cost, so we don't want
> to require implementations to do so.  For the same reason, we don't
> require array bounds checks for array__unsafe_lookup.  For both writes
> to closed files and array__unsafe_lookup, the performance cost of
> doing the checks is only a constant, so implementations which need
> safety can easily do the checks.  But it may be an important constant,
> so implementations which need maximum performance are not required to
> do the checks.
> 
> In contrast, with this case, there is no easy way for a compiler to
> ensure soundness.  Disabling the optimizations in question would
> only ensure *unsoundness*.  In general, if a compiler using
> separate compilation sees
> 
> 	foo(S0, S) -->
> 		stream__init(S0, S1),
> 		{ write_string("hello\n", S1, S2) },
> 		bar(S2, S).
> 
> then without seeing the body of bar/4, it can't know whether
> bar/4 calls stream__terminate, and so it can't know whether
> `write_string/3' should have any side effects.
> 
> So, in summary, specifying that certain things result in undefined
> behaviour is IMHO OK only so long as it is feasible for an
> implementation to check whether those things occur and to provide a
> sound and well-defined behaviour in those cases, preferably with only
> constant-time overhead for the checking.  I don't think that is the
> case here with missing calls to stream__terminate.
> 
I understand the problem that you are pointing out here, and I would
appreciate a possible solution.

The only solution that I can think of is to have two stream type
classes, one which is side effect free and one which isn't.
Here is the interface for the side effect streams.

:- typeclass stream__input(S) where [
    pred stream__read_char(S, stream__result(char), io__state, io__state)
    mode stream__read_char(in, out, di, uo) is det
].

where S must be a handle which is used to select the correct read
character implementation.

Any other solutions?

> A related problem is with the ordering of I/O.
> The procedures here are all declared `det', but there's
> nothing which ensures that you don't try to open two
> different output streams to the same file or device
> and try to write to them at the same time.  If you do,
> then the order of the output will be unspecified,
> and so you won't necessarily get the same result each time.
> Likewise, there is a problem with reading from a file
> at the same time as writing to it.
> 
> There's two possible solutions that I can see.
> One is to ensure that files/devices get locked when you create
> input or output streams to them, and attempts to access a locked file 
> from more than one stream at the same time (apart from multiple input
> streams, which should be allowed) result in I/O errors.
> The other is to make some of the procedures concerned `cc_multi'
> rather than `det'.
> 
Currently there is nothing in io.m the prevents you from opening a file
twice for writing to it.  Shall I change all those to cc_multi as well?

Pete
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------