Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland <hadrien.grasland@gmail.com>]

Le samedi 11 février 2017 20:36:31 UTC+1, Jeffrey R. Carter a écrit :
> 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.

A lock-free object is an object that can be concurrently manipulated by multiple threads, in such a fashion that any thread can fall asleep permanently at any point in time without preventing other threads from doing useful work.

A spinlock is not a lock-free object because if the thread holding the lock falls asleep, any other thread that needs to manipulate the spinlock is unable to make progress.

If you want an example of a lock-free object, consider Linux's Read-Copy-Update (RCU) mechanism, which is used to implement concurrent data structures that are read frequently but mutated rarely:

- The RCU data structure is accessed indirectly through a pointer.
- To access the data, a thread performs an atomic read on the pointer, then uses that pointer to read the data in a non-atomic fashion.
- To mutate the data, a thread does the following:
    * Access the data structure as above
    * Make a copy of it, and adjust the copy as needed
    * Try to replace the pointer to the old structure with the pointer to the new structure using an atomic compare-and-swap operation
    * If that fails, someone replaced the data structure under our feet: load the new data structure and try to perform our modifications again.

This algorithm is lock-free because threads that read data don't step on each other, and any thread which attempts to mutate the data can fall asleep at any point in time before the final compare-and-swap without preventing other threads from making progress.