On 1/5/12 4:16 AM, Manfred Nowak wrote:
Andrei Alexandrescu wrote:
specification can be refined
1) I do not see such refinements for D.
The shared qualifier is meant to guarantee sequential consistency. This
is not yet implemented.
2) If there is _no_ requirement for such refinements to be used
"manually": which theory enables the compiler to detect the
prerequisites for the refinements automatically?
If I understand this correctly, you're asking whether races can be
eliminated during compilation. Yes, it is possible, see a line of
research started by Boyapati:
http://eecs.umich.edu/~bchandra/publications/oopsla01.pdf.
D is also designed to eliminate low-level races (in safe programs)
during compilation because there is no undue aliasing. High-level races
are not eliminated.
3) If there _is_ a requirement for such refinements to be used
"manually", then there is no such theory and your starting "No" turns
into a "Yes, of course, even if the specification _is_ refined, because
humans might fail".
I don't understand what this are trying to convey.
Andrei
