Re: Lock-Free stack in Ada SPARK

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2017-02-12 13:26, Hadrien Grasland wrote:
> 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.

As a counterexample consider an atomic integer. Is it lock-free? Not 
according your definition, because there might be a thread waiting 
integer to become 123 while nobody writes that value there.

-------------------
It is correct to say that synchronization is achieved per busy waiting 
on lock-free shared objects. After all there is no other choice, a task 
that cannot continue must either be blocked or else retry.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de