(j3.2006) (SC22WG5.4962) A possible collective and atomic data consistency model
Tue Jul 16 08:25:33 EDT 2013
No need. It's interesting for me to take another look at this now. Some
of what he talks about is close to what we're doing (he mentions functional
programming and asynchronous execution), but he's using language mechanisms
that I don't employ partly because I don't fully understand them and partly
because some people who know the standard better than I do have deprecated
them. So I guess that makes what he's writing of less interest than it
On Mar 31, 2013, at 5:09 AM, N.M. Maclaren <nmm1 at cam.ac.uk> wrote:
> I shouldn't really have spent the time on this, but I have. This is an
> attempt to (a) explain Fortran's concepts to C++ people and (b) map the
> proven C++ design into Fortran, so that there is a chance of getting
> assistance from the C++ people who understand formal validation. I do
> not program in (or fully understand) HOL, and do NOT have time to learn
> before June!
> Please howl me down where I have got things wrong!
> As far as formalities go, I am NOT proposing this for inclusion in
> the TS, but I am absolutely certain that we need a clean and explicit
> data consistency model if we are to avoid introducing inconsistencies
> into the standard. And, worse, any such mistake is likely to be very,
> very hard to clean up later. At MOST, its last section might be an
> informative annex, with a comment that the intent is to make it
> rigorous and normative before the TS is incorporated into the main
> standard. Or it might just be a paper, designed to focus discussion.
> The main language extension I have assumed is that there are both
> inconsistent atomic definition and reference (as at present) and
> consistent forms. I have used new names for the latter, but there
> would be no problem in using the current names for them, and using
> new names for the inconsistent forms.
> Any feedback on that semaphore question would be very helpful,
> because I have assumed that events can be cleanly defined in terms
> of a DAG on the segments (i.e. as at present), but I have little
> idea of how that could be done except by simplifying them to simple
> Boolean semaphores.
> Nick Maclaren.
> J3 mailing list
> J3 at mailman.j3-fortran.org
More information about the J3