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: [EMAIL PROTECTED]