13 Jul
2011
13 Jul
'11
4:36 p.m.
On Wed, Jul 13, 2011 at 10:28 AM, Gabriel Beddingfield
<gabrbedd(a)gmail.com> wrote:
funny, but just so that we're clear - I'm not suggesting that a paper
proof of correctness is enough, but I am suggesting that a paper proof
of incorrectness *is* enough.
i don't
see why this is needed. its trivial to demonstrate on a piece
of paper that in a system with weak memory ordering constraints,
absence of a memory barrier is incorrect for any code with coupled
data values (e.g. a read index and read data). it doesn't matter if
this doesn't happen very often. you don't need a simulator of any
given CPU+memory model - its just demonstrably incorrect.
"Beware of bugs in the above code -- I've only proved it correct not
actually run it." - Knuth