Re: Lock-Free stack in Ada SPARK

[stevenselectronicmail@gmail.com]

On Saturday, February 11, 2017 at 11:36:31 AM UTC-8, Jeffrey R. Carter wrote:
> Perhaps someone will enlighten me.
> 
> All of the lock-free structures that I've looked at involved busy waiting on a 
> memory location via an atomic test-and-set/compare-and-swap operation.
> 
> To my mind, that's an implementation of a lock, and I don't understand why these 
> are considered lock free.
> 
> -- 
> Jeff Carter
> "Crucifixion's a doddle."
> Monty Python's Life of Brian
> 82

Jeffrey what you want are wait-free datastructures. In lock-free data structures at any single point in time the system as a whole can progress forward but some particular threads may end up waiting forever. In wait-free data structures every individual thread can progress forward in a finite amount of time. Note that there are also wait-free bounded and wait-free population oblivious algorithms which complete for any individual thread in a bounded amount of time (proportional to the amount of threads) and just bounded amount of time respectively. See also http://concurrencyfreaks.blogspot.ca/2013/05/lock-free-and-wait-free-definition-and.html