Re: Undefined behaviour [was Re: The D Programming Language]
Francis Glassborow wrote:
In article <JA53M5.nxA@beaver.cs.washington.edu>, "Andrei Alexandrescu
(See Website For Email)" <SeeWebsiteForEmail@erdani.org> writes
I don't know. The proofs I can understand concern single-threaded
execution. Multithreaded execution follows different formalisms. The
example above turns out to be an easy particular case, because both 0
and 42 have the same type.
Indeed, it becomes real fun when:
given that x is a reference to a base type in Java (or is a pointer to a
base type in C++)
thread 1:
x = new derived1;
thread 2
x = new derived2;
That's still easy because x has the same static type. Proving that a
sound program using a type stays sound when using a subtype instead is easy.
Stuff that is atomic is not of much concern. The hard part is figuring
out ordering of complex operations.
Whilst I have reservations as to the validity of proofs even in single
threaded programs (try reading Proofs and Refutations by Lakatos --
http://www.complete-review.com/reviews/lakatosi/pandr.htm for a review
-- for some understanding as to how difficult it is to go from spec to
proof without a process of continual refinement) I am certain that we
have nothing that works for multi-threaded programs.
I'm not that sure. What happened to all that great work on Java's memory
model (the one that also serves as a reference for C++'s memory model
work)? All experts seem to find it a good piece of work. I'm no expert,
so I'm not a good assessor. But at least I'm not certain we have nothing.
Andrei
--
[ See http://www.gotw.ca/resources/clcm.htm for info about ]
[ comp.lang.c++.moderated. First time posters: Do this! ]