On Wed, Jul 13, 2011 at 9:46 AM, Olivier Guilyardi <l...@samalyse.com> wrote: > On 07/13/2011 11:09 AM, Tim Blechmann wrote: > >> in fact, testing is not the best approach for verifying lock-free data >> structures: an implementation may work for years, if a certain condition is >> never triggered. the only reasonable way to ensure the correctness is a >> formal >> proof. unfortunately, most publications assume a sequencially consistent >> memory >> model and sometimes even avoid dealing with the ABA problem. > > To me, testing on real devices is needed, it's a pragmatic approach. But I > agree > it doesn't solve the entire problem. > > That said, what about simulation? One could for example implement a minimal > emulator for the abstract CPU and memory model described in > linux/Documentation/memory-barriers.txt, and test lock-free algorithms on > this.
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. _______________________________________________ Linux-audio-dev mailing list Linux-audio-dev@lists.linuxaudio.org http://lists.linuxaudio.org/listinfo/linux-audio-dev
