Double Checked Locking

[Andrei Alexandrescu]

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