@unpublished{PaulEMcKenney2007QRCUspin
,Author="Paul E. McKenney"
,Title="Using {Promela} and {Spin} to verify parallel algorithms"
,month="August"
,day="1"
,year="2007"
,note="Available:
\url{http://lwn.net/Articles/243851/}
[Viewed September 8, 2007]"
,annotation="
	LWN article describing Promela and spin, and also using Oleg
	Nesterov's QRCU as an example (with Paul McKenney's fastpath).
	Merged patch at: http://lkml.org/lkml/2007/2/25/18
"
}