[m-dev.] strict sequential semantics and committed choice

[Fergus Henderson]

On 13-Apr-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> On 13-Apr-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > Another reason for doubting that interpretation is that if that
> > interpretation were taken, then the current implementation would
> > not comply with the language reference manual.  It fails to
> > comply for several reasons.
> 
> I'm not really buying the "your interpretation is wrong because it means
> we have bugs" argument ;-)   

Well, looking at what the implementation does is a secondary or
tertiary consideration.  Before looking at that, you should first
check what the language specification says, and what the language
designers intended it to say.  But in cases where the language
reference manual is unclear, and where the language designers didn't
consider the issue, then what the implementation(s) do certainly
has some weight when it comes to determining the status quo.

Still, the more interesting discussion is to ask what is desirable,
rather than what is the status quo.

> I think it's a useful interpretation, and although it could be some
> work to fix it, it would provide a much clearer view of the entire
> strict sequential semantics issue.

I agree.  If it were just a matter of doing some work to fix it,
then I'd be happy.  But I'm worried that taking this approach
will cause serious difficulties for library procedures whose
behaviour is inherently nondeterministic; and if this approach
entirely eliminates the possibility of such procedures, then it
would significantly reduce the expressiveness of the language.

I think we may need to go back and reconsider what we were trying
to achieve with the strict sequential semantics.

> > The first is that although it provides a `--strict-sequential' option,
> > compiling with this option only affects the user's Mercury code, not the
> > library code that it gets linked with.  A simple fix for that problem would be
> > to always build the standard library with `--strict-sequential'.
> 
> No problems with that for the moment.
> 
> Obviously we need a better solution in general.  Sounds like a strict
> sequential grade option is required. 

I considered that.  But I think the efficiency loss from compiling the
library with --strict-sequential will be relatively minimal, and so
IMHO it is not worth the substantial costs of introducing another grade.

Most of the cases where --strict-sequential would make a significant
difference to performance are where code has been inlined or
specialized, and if you compile the library with --strict-sequential
but you compile the application without it, then so long as
intermodule optimization is enabled you will still get the benefit
of reordering optimizations for library code that is inlined or
specialized in the application.

> > A more serious problem is that there are some procedures in the standard
> > library, and more in the extras libraries, which provide useful
> > functionality, but which are inherently nondeterministic, and for
> > which it is difficult (anywhere from inconvient to impossible,
> > depending on the predicate) to implement them deterministically.
> 
> I think these problems are solvable.  Let's try them on a case by case
> basis...
>
> > Examples of these are:
> > 
> > 	- `benchmark_det' and `benchmark_nondet', from library/benchmarking.m.
> > 		Impossible to implement deterministically.
> 
> Time is an interesting issue.  I think you have to take time out of the
> semantics of the program somehow.  
> Since a program execution never starts with the same I/O state as any
> other program execution, committed choice non-determinism with respect
> to I/O is not an issue.  
> Since the only way you can get at time is using I/O states, time can be
> modelled by assuming getting the time is a deterministic operation
> with respect to that I/O state.
> 
> Assuming a deterministic universe, starting the same program with
> exactly the same input state will give the same I/O results, but since
> nobody can do that you don't have to worry about implementing any
> special code to handle it.
>
> The `cc_multi' declaration on predicates that take I/O states is really
> (or should really) just be an indication that nondeterministic
> operations may have been performed without the presence of I/O states.
> That is saying that even if you did have the same starting I/O you might
> still get different results.
> 
> While this is a meaningless disinction mathematically, it has some practical
> value because the programmer knows that even if the world is
> "basically" the same (that is, the set of things the program is
> documented to access is the same), they may still get different results.
> 
> Perhaps we could call these concepts relative determinism (where certain
> operations are deterministic relative to the programs thread of I/O
> states) and absolute determinism, where the operations are deterministic
> regardless of the I/O states.  cc_multi indicates absolute non-determinism
> is possible, and strict semantics removes absolute non-determinism.  
> I/O states indicate relative non-determinism is possible, and there
> is currently no way to remove it (although the proposed debugger redo
> I/O implementation based on capturing I/O might come pretty close).

That all sounds OK, but I'm not sure that it will really help us to
solve the problem that the strict sequential semantics was intended
to solve.   Hmm... I'll come back to this...

> > 	- `spawn', from extras/concurrency.
> > 		Can be implemented deterministically,
> > 		but only so long as there is no actual
> > 		concurrency going on, which basically
> > 		defeats the purpose.
> 
> I'm not really on top of concurrency at the moment.  Will the I/O
> modelling eliminate this problem?

With the current version of the concurrency stuff, which all
takes io__states, you might get away with that.  But in the
future I would like a version of the concurrency stuff that
worked with stores rather than io__states.  In that case,
I/O modelling won't help you.

The point here is that there are a few operations, true concurrency
being one of them, which have inherently nondeterministic
behaviour.  For these operations, there is really no way
of making them deterministic.

Another example that is related to this is that I would like
to be able to treat conditions such as running out of memory
(e.g. stack space or heap space) or out of CPU time
(exceeding a time limit) as exceptions.  If we do this, then
the nondeterminism of the procedures that catch exceptions becomes
something that cannot easily be eliminated by --strict-sequential;
whether an exception is thrown depends not only on the order of
execution, but also on the amount of time and memory that
the program uses (which is clearly going to depend on the
target architecture and the optimization options) and
also on the amount of CPU time and memory which the OS
provides us with, which can depend on what other programs
are running.

Note that the exception catching procedures do not all
take io__states, and requiring that they do would significantly
reduce expressiveness.

> > 	- The reverse mode of `std_util__make_type'.
> > 		Inconvenient to implement deterministically
> > 		(results will change at different optimization levels).
> > 		We could easily expand out equivalence types,
> > 		like type_ctor_and_args does, but that would
> > 		defeat the purpose of this procedure, which
> > 		is to provide access to the unexpanded type.
> 
> type_ctor_descs are just a non-canonical type represented in C.
>
> I think it's fair to say that the C implementation has to follow the
> semantics of Mercury.
>
> If strict semantics is given, it has to return the same type_ctor_desc.
> This probably means using equivalences.
>
> So what's missing is a way to find out what the semantics is in
> C code you write.
> 
> Alternately it might be possible to allow user-written C code to 
> leave out a strict semantics interpretation and give a compile
> time error if compiled with this option.

The trouble is that both of these alternatives damage expressiveness.
Forcing that procedure to be deterministic would pretty much
defeat the purpose of having it.  And disallowing calls to it
if --strict-sequential were specified would mean that you couldn't
really use that procedure in portable Mercury code.

Another possible alternative would be for the compiler to simply issue
a warning, rather than an error.  In that case, the guarantee for
--strict-sequential would be weakened a little: rather than promising
deterministic behaviour, the compiler would give you deterministic
behaviour where it could and would promise to tell you about all the
places where it couldn't.

> > 	- The reverse mode of `object_value'.
> > 		This procedure is defined in ~fjh/src/mercury/robdd/object.m.
> > 		It essentially returns a term's address on the heap.
> > 		It is not yet part of the standard library or extras,
> > 		mainly because the current implementation of it assumes
> > 		conservative GC.  Nevertheless this, or something like it,
> > 		could be very useful.  ghc has "stable names", which
> > 		are similar.
> 
> In strict semantics     Val = object_value(Obj)  
> is really		Val = object_value(Obj0), Obj = canonical_object(Obj0)

That would be a mistake, because (a) object_value/1 is guaranteed to be O(1),
whereas there is no such guarantee for canonical_object/1,
and (b) objects for which you call canonical_object/1 are not
garbage collected, so indiscriminate use of canonical_object/1
would lead to memory leaks.

> Perhaps it would be better to force all non-canonical types to provide
> such an operation.  If you don't provide one then compilation aborts
> for strict semantics.

That would work, but it would significantly reduce expressiveness.

> > The other cc_ procedures in the extras and standard library are ones
> > whose behaviour depends on the representation of their arguments. 
> > Note that for procedures like var__is_ground and cfloat__dump the situation is
> > a bit more complicated again, because they are dynamically moded and so the
> > representation distinguishes between bound and unbound values, so we can't
> > just treat it as if it were a type with a user-defined equality.
> 
> This is more complex.  I'm going to see what your thoughts are on my
> comments above before tacking it.  It would also be nice if I could
> read some documentation on inst "any" as currently it isn't part of the
> Mercury language reference.
> 
> Currently I'm not sure whether dynamic modes are worth including in the
> strict sequential semantics at all.  I think it would rob them of their
> usefulness.

Well, the point of the strict sequential semantics is just to
give you deterministic behaviour.  Despite the "sequential" in
the name, it doesn't mean that there is no reordering -- the
compiler still does mode reordering as usual, using a deterministic
static analysis algorithm to schedule the code.  For dynamic modes,
you'd get the same thing: for the "strict sequential semantics",
code using dynamic modes and dynamically scheduling would be
dynamically reordered using a deterministic algorithm.

Perhaps we should rename it?

For complicated constraint solvers such as CLP(R), there is
another issue that pops up: we don't want to have to specify
the constraint solving algorithm exactly, because it might
be different for different implementations, or for different
versions of the same implementation, or even for different
optimization levels.  So there may be some _portability_
problems there.  But this issue also arises for many other
things in the standard library that we don't want to fully
specify, for example `char__to_int'.  These kinds of issues
don't cause any _reproducability_ problems - if you compile and
execute the same program twice, using the same implementation
and the same options each time, then you'll get the same results.

There's an inherent trade-off between specifying things exactly,
in order to enhance program portability, and leaving things
incompletely specified, in order to give the implementer more
freedom.  Often specifying things exactly is best, but there
are many times when it is very important to leave things
incompletely specified.  I guess this just means that the
`--strict-sequential' option isn't going to solve all possible
portability problems automatically.

The best you can hope for when it comes to portability is
that for a single implementation, you should ideally be able
to ensure that compiling with different optimization levels
or to different target platforms will not change the
program's behaviour.

Perhaps I should introduce some terms for describing this stuff.
Let's define "weak reproducibility" to mean that if you compile
with a different optimization level or target platform you may
get different results, "strong reproducibility" to mean
that the results should be independent of the optimization level
and target platform, and "guaranteed portabilility" to mean
that you get exactly the same behaviour on all implementations.

Then, to restate what I said above, there are many cases where
requiring "guaranteed portability" would impose too many constraints
on implementations, so the best we can possibly hope for, in general,
is "strong reproducibility".

Dynamic modes and procedures like var__is_ground don't necessarily
cause any problems for strong reproducibility.  Procedures like
cfloat__dump could potentially cause some problems, e.g. if the dump
of the representation for unbound variables includes the variable's
address.  But if you carefully choose an appropriate interface and an
appropriate representation for dumping unbound variables, e.g. calling
them _v1, _v2, _v3, ... according to the order in which they appear in
the dumped term, then you can achieve that degree of portability.  Our
current implementation of cfloat__dump uses the variable creation
number, which can depend on the presence or absense of optimizations
such as duplicate call elimination, so it breaks strong
reproducibility.  But that is fixable.

However, there are some operations for which strong reproducibility is
unachievable: those that depend on the program's space consumption. 
One example is exception handling procedures (if space exhaustion
is treated as an exception).

The reverse mode of object_value/1 is another example, since it
exposes sharing, which will depend on the optimization level.
Also, because objects are comparable using compare/3, that procedure
also exposes the relative ordering in the address space.

Hmm, now that I think about it store__new_ref and store__new_arg_ref
also expose sharing... they ought to be cc_multi.  Currently
they're not, which is a bug.  But again for these procedures
strong reproducibility is not achievable.  (If the garbage
collector introduces sharing, and if furthermore it the times
at which it gets invoked are nondeterministic, then you would
lose even weak reproducibility.)

For some operations, even weak reproducibility may be unachievable.
These include those that depend on the program's time consumption.
Examples include benchmarking, timeouts and true concurrency.

> > Anyway, I'm not sure what to do -- whether to try and change
> > things so that `--strict-sequential' guarantees results
> > that are reproduceable (and if so, to what extent --
> > should the results always be the same regardless of
> > optimization level or target platform?), or whether
> > to just not guarantee so much.
> 
> I think I've answered this above -- when I have more time (and more
> feedback) I can work on a summary.
> 
> I think the guarantee we give is for things not involving I/O states
> you get reproducibility or a compile time or link time error.
> For things involving I/O states you get a guarantee that if you were to
> run the same program again with exactly the same starting external world
> you would get the same results.

I presume that above you just talking about weak reproducibility?


Let me summarize the situation as I see it:

    - Providing guaranteed portability is definitely not feasible,
      because it require require that we specify everything in full,
      which would overconstrain implementations.

    - There seem to be lots of features that are IMHO just far too useful
      to live without, for which we cannot guarantee strong reproducibility.
      So guaranteeing strong reproducibility looks like it is too much
      to ask.

    - There are also a few features that would be very nice,
      for which we cannot even guarantee weak reproducibility.
      Examples include benchmarking, timeouts and true concurrency.

      Threading io__states through these operations would allow us
      to meet the above guarantees.  However, it wouldn't make these
      operations any more reproducible.  At best it would perhaps
      make it a bit clearer to the user that the `--strict-sequential'
      option would not suffice to give these operations deterministic
      behaviour.

      For benchmarking, it would probably be fine to thread io__states
      through those operations.  But for timeouts and true concurrency,
      forcing the user to thread io__states through these operations
      would hurt expressiveness significantly.

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