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

[Tyson Dowd]

On 13-Apr-2000, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 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.

Sorry, that was a mistake.  It should be the semantics of which result
you will get, there is no order since there is only one result.

I think that when you have a program that is cc_multi, that unless you give
the strict sequential semantics option, you are saying any result is
equivalent.  So your programs intendend interpretation is any



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

Yes, this is the interpretation I have taken.

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

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.

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

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

I regarded this as something of a dark corner of the semantics anyway.

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

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

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

In general if you have a `canonicalize' operation available on a
non-canonical type, you can get around cc_multi OK.

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.

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

> 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.  If the starting states are different
you only get the informal guarantees given in the documentation of
the predicates you called.  It would be nice to give more than this but
we have no way of expressing any more at the moment.

-- 
       Tyson Dowd           # 
                            #  Surreal humour isn't everyone's cup of fur.
     trd at cs.mu.oz.au        # 
http://www.cs.mu.oz.au/~trd #
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------