On 07/13/2011 03:51 PM, Paul Davis wrote: > On Wed, Jul 13, 2011 at 9:46 AM, Olivier Guilyardi <[email protected]> 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.
I see your point, although sometimes it's unclear what kind of barriers to use and where to place them. -- Olivier _______________________________________________ Linux-audio-dev mailing list [email protected] http://lists.linuxaudio.org/listinfo/linux-audio-dev
