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

[Fergus Henderson]

On 12-Apr-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> On 06-Apr-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > The sentence "The behaviour of pure predicates
> > is never affected by the invocation of pure predicates" is not correct.
> > For pure procedures with determinism `cc_nondet' or `cc_multi',
> > the invocation of other pure predicates can affect which solution
> > you get. 
> 
> Hmmm...
> 
> I view the committed choice determinisms as a statement about the
> semantics of the order of results.

I'm not sure exactly what you mean by that sentence.

> In the strict sequential semantics the statement "The behaviour of pure
> predicates is never affected by the invocation of pure predicates"
> should be true (without qualification).
> 
> In other semantics, it is permissible for the results of these
> operations to be non-deterministic.  The fact that operationally
> some pure predicates might affect the operation of cc_* predicates is
> irrelevant -- declaratively these predicates are non-deterministic,
> anything at all can affect them.  So the declarative "behaviour" of pure
> predicates is unaffected by the invocation of pure predicates.
> 
> (this makes me think that perhaps benchmarking requires an I/O state
> after all, since in strict sequential semantics an I/O state is the only
> way you can account for different timing results brought about by the
> external environment).
> 
> Am I completely off target here?  Are we really disputing the word
> "behaviour"?  (I'd prefer to use something else).

The use of the word "behaviour" is part of it, but not the whole story.

Your statement 

> In the strict sequential semantics the statement "The behaviour of pure
> predicates is never affected by the invocation of pure predicates"
> should be true (without qualification).

is correct for procedures that the user defines in Mercury and
that do not call any procedures with determinism `cc_nondet' or
`cc_multi' that are defined in the standard library or using the
C interface.  But for procedures with determinism `cc_nondet' or
`cc_multi' that are defined using the C interface or that are
part of the standard library (and which therefore might be defined
using the C interface), or procedures which call such procedures,
the situation is not so clear.

The language reference manual does not explicitly address the
issue.  One reasonable interpretation of it, which you seem to
have taken, is that for library predicates or predicates defined
using the C interface, the same guarantee applies: the
declarative semantics for such procedures is specified by a bunch
of axioms, and the strict sequential operational semantics for
such procedures is a singleton set, determined by performing
SLDNF resolution on these axioms in (mode-reordered) top-down
left-to-right order.  However, the actual wording in the
reference manual says that "the program" is executed in this way,
rather than the axioms, and it is not clear what this means for
procedures which are defined using the C interface rather than
Mercury code.

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.

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'.

Another potential problem is that for many predicates the order of
solutions is dependent on the representation of the arguments,
not just on the value of the arguments.  So we might need to clarify
that the process of execution that the "Semantics" chapter uses
to define the operational semantics must keep track of the
representation of each variable, not just its value, and
that for a switch on a non-canonical type, the branch chosen
can depend on the representation.

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.

Examples of these are:

	- `benchmark_det' and `benchmark_nondet', from library/benchmarking.m.
		Impossible to implement deterministically.

	- `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.

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

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

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.


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.

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