RE: [Caml-list] Evaluation Order

["Manuel Fahndrich" <maf@microsoft.com>]

I feel your pain, having run into this problem before. What we need is a
way for the compiler to alert the programmer in contexts where
evaluation order is unspecified, but where the programmer relies on some
order.

The only way I can imagine doing this is if the language contains a
notion of side effecting evaluation. If such a concept is present, then
in any context where evaluation order is undefined, all involved
expressions must be side effect free, which guarantees that the code
will evaluate in the same way no matter what order the actual
implementation chooses.

Of course, the side effect annotations can become burdensome. Also, one
pretty quickly wants to distinguish certain side effects from others.
Evaluation order independence can be guaranteed if the side effects of
two expressions don't interfere. 

In a language with regions (such as Tofte and Talpin) we can obtain some
of this directly:

If we have e1 + e2, and the effects of e1 are E1 and effects of e2 are
E2, then we merely have to check that the intersection of E1 and E2 is
empty. That sounds simple, but it is not, because of possible region
aliasing.

Yet another way to look at it is in terms of heap splitting. If in order
to evaluate e1 + e2, we can split the heap M into disjoint parts M1 + M2
and evaluate e1 under M1 and e2 under M2, then we know they can't
interfere. This is the notion studied in Reynold's syntactic control of
interference, and also in the logic of bunched implications, and in the
capability calculus.

(shameless plug)
In VAULT (http://research.microsoft.com/vault) we have a notion of
non-aliasing for regions, thus there are situations where we can decide
the above non-interference.

-Maf


-----Original Message-----
From: David McClain [mailto:dmcclain1@mindspring.com] 
Sent: Saturday, June 09, 2001 9:00 AM
To: caml-list@inria.fr
Subject: [Caml-list] Evaluation Order

I thought I would share an experience with all of you to solicit your
*constructive* comments.

I just rewrote my block convolution routine in pure OCaml native
compiled
along with the inner loop in C/C++. This is necessarily a side effecting
program since it must alter the outside world of data. I had a statement
in
OCaml that went something like this:

    let ans = fnx () + fny ()

where both fnx and fny are side effecting closures.

I consider myself a very experienced OCaml programmer, and I am so
accustomed to getting pristine results from OCaml, that I spent many
hours
going through my C/C++ code looking for the error. I was getting
anomalous
output values at the front of my convolution records, but everything
else
worked just fine. I was convinced something was awry with my C code ---
whenever a problem occurs that's almost always where it is -- never in
the
OCaml code.

I had forgotten about the evaluation ordering in OCaml being from right
to
left. I am aware of the reasons for this, having studied the Zinc paper
some
time ago. But the tendency to read implicit temporal ordering of
operations
as left to right is a very strong psychological factor here. The
problem,
once tracked down, was easily fixed by restating the routine as

    let ans = fnx() in
        ans + fny()

to force evaluation of fnx before fny.

I suppose if Hebrew or Arabic were my native tongue then the opposite
expectation would be true and I would have naturally written

    let ans = fny() + fnx()

and I would be no wiser about evaluation order here, since everything
would
have worked properly.

I don't have a good answer to this problem, but I did want to point out
the
one and only place where OCaml forced me to spend hours debugging a
problem
caused solely by a clash of psychology and OCaml semantics. All of my
other
debugging activities have, and will probably continue, to focus on C/C++
as
the likely culprit.

This problem will be permanently etched into my mind from now on, and I
will
be sure to remember to avoid order dependent syntax.

The same problem occurs regularly in C, and I have become quite
accustomed
and adept at avoiding these ordering problems. Good examples are to be
found
among C preprocessor macrology. I just now have to remember that the
same is
true of OCaml.

I had been lulled into a belief that OCaml was nearly perfect, while
C/C++
is definitely not. The problem is not one of OCaml, but rather a clash
between normal psychological expectations and the programming language
at
hand.

Since embedded realtime systems are chock full of temporally ordered
operations this must be one of the severe weak points in software
control
systems. There must be a better way to guide human thinking here. Just
as
OCaml has provided a system to look over our shoulders and force us to
write
the correct things, there must be a way of doing something similar for
temporally dependent clauses.

Any thoughts? (other than that I was boneheaded here!)

- DM


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ:
http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives:
http://caml.inria.fr
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr