linuxaudio.org

On 07/13/2011 03:51 PM, Paul Davis wrote:

quoted text
> On Wed, Jul 13, 2011 at 9:46 AM, Olivier Guilyardi  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

Linux-audio-dev@lists.linuxaudio.org

http://lists.linuxaudio.org/listinfo/linux-audio-dev