Rather than such an operational semantics, what I, as a programmer, would
prefer to see is an axiomatic semantics -- i.e. a list of guarantees of
the form
"if a program does S1, S2,..., and Sn, then R1, R2,..., and Rm will be true".
It is important that S1, S2,..., Sn be conditions that the programmer can
easily verify to be true -- preferably syntactically.
What *I* would like is for MPI implementors/vendors first determine whether
they can implement the Collective Semantics, below, efficiently on their
target platform. If so, then try the BBS Semantics, below. (If the former
is possible, but not the latter, it is probably because the latter allows
both PUTs and GETs to be performed at roughly the same time to the same
buffer. There are hardly any other differences.) If there are any problems,
more constraints (i.e. more "Si"s) can be added until the semantics are
implementable. If there are no problems, maybe constraints can be removed or
more axioms can be added, until counters and RMW and whatever have been
re-added.
I think that the "cache flush vs. cache invalidate" problem that Eric
mentioned might be solved by timing things properly -- e.g. in the Collective
Semantics, invalidating at the beginning of the collective operation and
flushing at the end, or something like that. Maybe.
Marc suggested that one possibility was to leave things as they are. I do
not think that the rules in the current chapter -- especially in regards to
*when a WINDOW_IN or WINDOW_OUT should be executed or
*when a FENCE can complete or
*whether a counter can update without a WINDOW_IN or WINDOW_OUT
-- can be expressed in terms of axioms like this, which means to me, as a
programmer, that I don't know what I must do to make my program work.
But maybe they can be expressed, and I am still missing something.
-Dave
==========================================================================
Note: These axioms are not *exactly* in the "If ... then ..." form I gave
above, but they are easily converted to that form.
==========================================================================
Collective Semantics (i.e. for the collective PUT and GET operations):
==========================================================================
Axiom 1 (PUT): If a collective PUT completes, and the target process did
not issue any stores to "recvbuf" between the initiation and completion
of the PUT in that process, then
(1) all elements of "recvbuf" which were not addressed by any of the
PUTs will have the same value as when the collective PUT was
initiated, AND
(2) any elements of "recvbuf" which were addressed by exactly one of
the PUTs will contain the value deposited there by that PUT.
(Other elements -- i.e. those addressed by multiple PUTs -- will have
undefined content.)
Axiom 2 (GET): (Similar to axiom 1, but for GETs -- obvious.)
==========================================================================
Barrier-Based Simplified (BBS) Semantics (i.e. for the PUTs and GETs that
require BARRIERs for sync):
==========================================================================
Axiom 1 (PUT):
If process A performs a PUT to location L in process B, then a
local fetch by process B from location L is guaranteed to return
the new value IF
(1) processes A and B perform a MPI_BARRIER on the communicator
after the PUT in process A and before the fetch in process B
AND
(2) no other local store occurs to location L between the
time process A performs the PUT and the time process B
performs the local fetch AND
(3) no other PUT to location L is initiated by any process between
the previous BARRIER (i.e. the BARRIER before the one mentioned
in 1, above), if any, and the time that process B performs the
local fetch
AND ONLY IF the PUT precedes the fetch.
Axiom 2 (GET):
If process A performs a local store to location L, then a GET by
process B from location L is guaranteed to return the new value IF
(1) processes A and B perform an MPI_BARRIER on the communicator
after the store in process A and before the GET in process B
AND
(2) no other local store or PUT to location L occurs between the
time process A performs the store and the next BARRIER (i.e. the
BARRIER after the one mentioned in 1, above), if any, AND
(3) process B does not attempt to access the value returned by the
GET until after the next BARRIER (i.e. the one mentioned in 2,
above)
AND ONLY IF the store precedes the GET.
===============================================================================
David C. DiNucci | MRJ, Inc., Rsrch Scntst |USMail: NASA Ames Rsrch Ctr
dinucci@nas.nasa.gov| NAS (Num. Aerospace Sim.)| M/S T27A-2
(415)604-4430 | Parallel Tools Group | Moffett Field, CA 94035