(Assume we are working with a simple language, as in the JSR document
where pointer aliasing issues do not arise, i.e. the mapping between
names in source text and locations in runtime memory is one to one.)
Define a linking L to be a mapping of reads in a source program with
writes in the source program to the same location. An execution is said
to satisfy L if the value obtained from memory at read r is the same as
the value written to memory at L(r).
Linking Monotonicity Principle: Given a program P and a linking L, if P
has an execution satisfying L, then P || Q should have an execution
satisfying L (for any program Q).
The intuition behind this principle is that the implementation should be
able to link reads to writes compositionally, that is, without having to
examine the entire program. Intuitively, it should be possible to
postpone the first step of Q till after P has finished the portion of
its execution sequence which satisfies L. So Q should not be able to
prevent the system from implementing P as if it existed in isolation
from Q (at least any arbitrarily finite prefix of P, if you are
concerned about fairness issues).
*Semantics* should not depend on having the *entire* program available,
though of course an implementation might.
Please think about this and try and make up your mind on whether you buy
this without reading the rest of this message....
Best,
Vijay
====================================
And now the rest of the message :-)
An implication of this principle is that Test Case 18 should be
forbidden, not allowed. The analysis that R3!=0 "implies" R3=42 depends
on a closed world assumption, and is invalidated if you add another
thread that "may" write to X, though in fact it never will. That is, a
possible behavior of P is ruled out by running another program Q in
parallel with it.
Where is this principle coming from? Over the last ten years there has
been a lot of research on causality in concurent programming languages
(particularly synchronous programming languages). (There is a *lot* of
research in engineering on causality, and closer to computer science, in
AI and Qualitative Reasoning.) Gerard Berry introduced certain
constructs in Esterel in the early 90s that relied on what my colleagues
and I later called "negative information", i.e .the absence of
information. We wrote a series of papers on Timed Concurrent Constraint
Programming, and then Default Timed Concurrent Constraint Programming
which analyzed this phenomena in detail (see LICS 94, POPL 95, the
journal papers etc accessible from
http://www.stratify.com/emp/staff/resteam/vgupta/ )
A program depending on negative information allows computation to
progress on the *absence* of information. Usual control constructs rely
on the presence of information, e.g. read the information currently
present in memory location x, interprete it as an integer, add it to the
bits currently present in y, write it into z etc etc. An example of a
control construct that depends on negative information is the "if c else
A" of Default CCP. It says that in the absence of information c now *and
for the duration of the computation*, execute A. The construct,
naturally enough, leads to causal loops (e.g. what if A causes c to
happen) which end up implying that there are *no* behaviors for certain
programs. (e.g. if d else d). A large part of the sophistication of
the mathematical (operational and denotational) models we developed was
devoted to understanding this phenomena, and presenting a simple
account for it in terms of the meaning of a program as a set of pairs of
fixed points.
What does this mean here? The value (42) returned by a read (the read of
R3 in Line 1 of Case 18) for the case in question depends on knowledge
that a particular write (43) has not happened *and cannot happen in the
future*. This is the default assumption that is violated when another
program is run in parallel with it.
Default assumptions are complicated to deal with, though we showed that
in fact denotational models are possible. But I am not quite sure I
believe that they belong in a production language like Java just yet.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:58 EDT