[linux-audio-dev] lock-free ring buffer code

[rm]

On Fri, Apr 04, 2003 at 07:48:20AM -0500, Paul Davis wrote:
> just for completeness sake, this isn't really true. the atomicness of
> int writes/reads isn't central. what is central is (as you noted) the
> single (group of synchronous) reader(s) and single (group of
> synchronous) writer(s), and the monotonic motion of the read+write
> pointers. 

necessary, but not sufficient :> 
(again i'm forgetting to state my assumptions).

> there is one aspect of the LFRB that bothers me. as has been explained
> many times, the monotonic motion of the read/write pointers is
> key. but when one the reader/writer moves the pointer to the end of
> the buffer and wraps it around, that operation does not cause
> monotonic motion (its semantically monotonic, but in fact the pointer
> value goes from high to low). i've never quite satisfied myself that
> this is threadsafe.

the cases where you can run into trouble are where you rely on
external state to remain unchanged between two non-atomic ops, right?

looking at my code, it does rely on external things being constant so
i guess you have to specify the invariants better.

so i assume, the size of the buffer never changes. additionally i
assume that if the write and read pointers are not equal when we test
it, whatever condition this implies holds until i'm done. 

the property i'm assuming (i think) is that if the reader (writer) was
not in the current (next position) when i checked last, it cannot be
there until i write my pointer back (i think this is a weaker property
than assuming monotonicity or at least different one)

so assume G is a connected, cyclic, directed graph w/ maximum outgoing
degree 1. given any vertex, there is a unique, immediate predecessor
which is adjacent to that vertex. so given any 3 vertices in the
graph, u,v,w, s.t. there is a path between (u,w) and (u,v), then the
either the path (u,w) include vertex v, or (u,v) include w.

this is true because given 3 vertices on G, there is only one outgoing
path from u to any other vertex (connected, cyclic, directed, out
degree 1), so either the path to v or the path to w must be a subpath
of the other. since one is a subpath of the other one path shares all
the vertices with the other path, and hence either w or v is included.

ok so now, we should show that our code is equivalent to the graph. so
hopefully it's clear that: in the code any cell has a unique
predecessor, all cells are reachable from any other cell, and there is
only one outgoing edge (a consequence of having a unique predecessor).
so there must exist positions a,b,c s.t. there is a series of
sucessors (a, ..., b, ..., c). (this step is fuzzy, how do you show
the functional equivalency? maybe 'there exists a one-to-one and onto
mapping between cells and vertices...', etc, or some finite field
modular stuff?).  (i always skipped the formal methods classes).

so for our invariant to hold (that an unoccupied cell remains that way
until we write our pointer), we must guarantee that given a reader at
a and writer at b, the writer never goes past the reader and vice
versa. this is sufficient to ensure that the current/immediate
successor vertex will remain unchanged.

finally, we show the sufficiency of checking reader == writer for
holding the above invariant. we fail in both cases without updating
the pointers so it must hold (one can not pass the other).

so our invariant holds and it's thread safe since since pointer/int
reads and writes are atomic, and we don't update the positions until
after we are done. (assuming that was the only assumption :>). the
other important thing i think is that we read the pointer we don't
have control over *exactly* once.

the initial conditions are a bit annoying since my code initializes to
(reader==writer), but that's easy enough to not do.

or that's my best dumb stab at it.

	rob

----
Robert Melby
Georgia Institute of Technology, Atlanta Georgia, 30332
uucp:     ...!{decvax,hplabs,ncar,purdue,rutgers}!gatech!prism!gt4255a
Internet: async at cc.gatech.edu