Lock-Free stack in Ada SPARK

Lock-Free stack in Ada SPARK

[stevenselectronicmail]

It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.

https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD

There's also a lock-free condition variable like thing

https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le samedi 11 février 2017 04:07:43 UTC+1, stevensele...@gmail.com a écrit :
> It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
> 
> https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
> 
> There's also a lock-free condition variable like thing
> 
> https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD

Actually, I'm not convinced that Ada atomics provide the required properties for what you're trying to do here.

To me, Ada's "Atomic", as defined by section C.6 of the Ada 2012 RM, provides essentially the same synchronization guarantees as Java's "volatile":

1/Each read from an atomic variable is atomic.
2/Each write to an atomic variable is atomic.
3/Each thread sees the same atomic writes occuring, without reordering.

What it does not guarantee, however, is that nothing will happen between the time where a thread reads from a variable, and the time where a thread writes to a variable. Which means, for example, that "X := X + 1" is a race condition in Ada even if X is atomic.

It also means that the Linted.Compare_And_Swap primitive that your lock-free stack is using has a race condition inside of it, as far as I can tell. From https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.adb;h=a0a59e66568c8b5e11318691d97608dc33363315;hb=HEAD ...

  26       procedure Compare_And_Swap
  27         (Old_Ptr : Element_T;
  28          New_Ptr : Element_T;
  29          Success : in out Boolean)
  30       is
  31       begin
  32          if Old_Ptr = Ptr then
  33             Ptr := New_Ptr;
  34             Success := True;
  35          else
  36             Success := False;
  37          end if;
  38       end Compare_And_Swap;

...you actually cannot guarantee that Ptr will not be updated by another thread between the time where you check it at line 32 and the time where you write to it at line 33, which means that you have a data race on your hands.

You could expose this by running two tasks in parallel, have them call compare-and-swap on a shared memory location, and see if you can observe an inconsistent memory state (i.e. one where a task should have not written to memory but did so anyway).

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le samedi 11 février 2017 10:57:58 UTC+1, Hadrien Grasland a écrit :
> Le samedi 11 février 2017 04:07:43 UTC+1, stevensele...@gmail.com a écrit :
> > It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
> > 
> > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
> > 
> > There's also a lock-free condition variable like thing
> > 
> > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD
> 
> Actually, I'm not convinced that Ada atomics provide the required properties for what you're trying to do here.
> 
> To me, Ada's "Atomic", as defined by section C.6 of the Ada 2012 RM, provides essentially the same synchronization guarantees as Java's "volatile":
> 
> 1/Each read from an atomic variable is atomic.
> 2/Each write to an atomic variable is atomic.
> 3/Each thread sees the same atomic writes occuring, without reordering.
> 
> What it does not guarantee, however, is that nothing will happen between the time where a thread reads from a variable, and the time where a thread writes to a variable. Which means, for example, that "X := X + 1" is a race condition in Ada even if X is atomic.
> 
> It also means that the Linted.Compare_And_Swap primitive that your lock-free stack is using has a race condition inside of it, as far as I can tell. From https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.adb;h=a0a59e66568c8b5e11318691d97608dc33363315;hb=HEAD ...
> 
>   26       procedure Compare_And_Swap
>   27         (Old_Ptr : Element_T;
>   28          New_Ptr : Element_T;
>   29          Success : in out Boolean)
>   30       is
>   31       begin
>   32          if Old_Ptr = Ptr then
>   33             Ptr := New_Ptr;
>   34             Success := True;
>   35          else
>   36             Success := False;
>   37          end if;
>   38       end Compare_And_Swap;
> 
> ...you actually cannot guarantee that Ptr will not be updated by another thread between the time where you check it at line 32 and the time where you write to it at line 33, which means that you have a data race on your hands.
> 
> You could expose this by running two tasks in parallel, have them call compare-and-swap on a shared memory location, and see if you can observe an inconsistent memory state (i.e. one where a task should have not written to memory but did so anyway).

If Ada atomics end up not doing what you want, you have essentially three options:

* Drop hardware portability and write assembly code that calls the atomic read-modify-write operations of you target CPU.
* Drop compiler portability and use compiler-provided atomic operations such as GNAT's System.Atomic_Counters.
* Write your atomic operations in a language with standard support for hardware atomic read-modify-write operations, such as C99 or C++11.

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le samedi 11 février 2017 11:07:30 UTC+1, Hadrien Grasland a écrit :
> Le samedi 11 février 2017 10:57:58 UTC+1, Hadrien Grasland a écrit :
> > Le samedi 11 février 2017 04:07:43 UTC+1, stevensele...@gmail.com a écrit :
> > > It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
> > > 
> > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
> > > 
> > > There's also a lock-free condition variable like thing
> > > 
> > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD
> > 
> > Actually, I'm not convinced that Ada atomics provide the required properties for what you're trying to do here.
> > 
> > To me, Ada's "Atomic", as defined by section C.6 of the Ada 2012 RM, provides essentially the same synchronization guarantees as Java's "volatile":
> > 
> > 1/Each read from an atomic variable is atomic.
> > 2/Each write to an atomic variable is atomic.
> > 3/Each thread sees the same atomic writes occuring, without reordering.
> > 
> > What it does not guarantee, however, is that nothing will happen between the time where a thread reads from a variable, and the time where a thread writes to a variable. Which means, for example, that "X := X + 1" is a race condition in Ada even if X is atomic.
> > 
> > It also means that the Linted.Compare_And_Swap primitive that your lock-free stack is using has a race condition inside of it, as far as I can tell. From https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.adb;h=a0a59e66568c8b5e11318691d97608dc33363315;hb=HEAD ...
> > 
> >   26       procedure Compare_And_Swap
> >   27         (Old_Ptr : Element_T;
> >   28          New_Ptr : Element_T;
> >   29          Success : in out Boolean)
> >   30       is
> >   31       begin
> >   32          if Old_Ptr = Ptr then
> >   33             Ptr := New_Ptr;
> >   34             Success := True;
> >   35          else
> >   36             Success := False;
> >   37          end if;
> >   38       end Compare_And_Swap;
> > 
> > ...you actually cannot guarantee that Ptr will not be updated by another thread between the time where you check it at line 32 and the time where you write to it at line 33, which means that you have a data race on your hands.
> > 
> > You could expose this by running two tasks in parallel, have them call compare-and-swap on a shared memory location, and see if you can observe an inconsistent memory state (i.e. one where a task should have not written to memory but did so anyway).
> 
> If Ada atomics end up not doing what you want, you have essentially three options:
> 
> * Drop hardware portability and write assembly code that calls the atomic read-modify-write operations of you target CPU.
> * Drop compiler portability and use compiler-provided atomic operations such as GNAT's System.Atomic_Counters.
> * Write your atomic operations in a language with standard support for hardware atomic read-modify-write operations, such as C99 or C++11.

-C99 +C11

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le samedi 11 février 2017 11:08:42 UTC+1, Hadrien Grasland a écrit :
> Le samedi 11 février 2017 11:07:30 UTC+1, Hadrien Grasland a écrit :
> > Le samedi 11 février 2017 10:57:58 UTC+1, Hadrien Grasland a écrit :
> > > Le samedi 11 février 2017 04:07:43 UTC+1, stevensele...@gmail.com a écrit :
> > > > It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
> > > > 
> > > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
> > > > 
> > > > There's also a lock-free condition variable like thing
> > > > 
> > > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD
> > > 
> > > Actually, I'm not convinced that Ada atomics provide the required properties for what you're trying to do here.
> > > 
> > > To me, Ada's "Atomic", as defined by section C.6 of the Ada 2012 RM, provides essentially the same synchronization guarantees as Java's "volatile":
> > > 
> > > 1/Each read from an atomic variable is atomic.
> > > 2/Each write to an atomic variable is atomic.
> > > 3/Each thread sees the same atomic writes occuring, without reordering.
> > > 
> > > What it does not guarantee, however, is that nothing will happen between the time where a thread reads from a variable, and the time where a thread writes to a variable. Which means, for example, that "X := X + 1" is a race condition in Ada even if X is atomic.
> > > 
> > > It also means that the Linted.Compare_And_Swap primitive that your lock-free stack is using has a race condition inside of it, as far as I can tell. From https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.adb;h=a0a59e66568c8b5e11318691d97608dc33363315;hb=HEAD ...
> > > 
> > >   26       procedure Compare_And_Swap
> > >   27         (Old_Ptr : Element_T;
> > >   28          New_Ptr : Element_T;
> > >   29          Success : in out Boolean)
> > >   30       is
> > >   31       begin
> > >   32          if Old_Ptr = Ptr then
> > >   33             Ptr := New_Ptr;
> > >   34             Success := True;
> > >   35          else
> > >   36             Success := False;
> > >   37          end if;
> > >   38       end Compare_And_Swap;
> > > 
> > > ...you actually cannot guarantee that Ptr will not be updated by another thread between the time where you check it at line 32 and the time where you write to it at line 33, which means that you have a data race on your hands.
> > > 
> > > You could expose this by running two tasks in parallel, have them call compare-and-swap on a shared memory location, and see if you can observe an inconsistent memory state (i.e. one where a task should have not written to memory but did so anyway).
> > 
> > If Ada atomics end up not doing what you want, you have essentially three options:
> > 
> > * Drop hardware portability and write assembly code that calls the atomic read-modify-write operations of you target CPU.
> > * Drop compiler portability and use compiler-provided atomic operations such as GNAT's System.Atomic_Counters.
> > * Write your atomic operations in a language with standard support for hardware atomic read-modify-write operations, such as C99 or C++11.
> 
> -C99 +C11

Ah, sorry. I just noticed that your Compare_And_Swap is implemented as part of a protected type.

Then the problem is actually simpler: your queue is not lock-free, because the protected type implementation very likely has a mutex inside of it.

Re: Lock-Free stack in Ada SPARK

[stevenselectronicmail]

On Saturday, February 11, 2017 at 2:14:20 AM UTC-8, Hadrien Grasland wrote:
> Le samedi 11 février 2017 11:08:42 UTC+1, Hadrien Grasland a écrit :
> > Le samedi 11 février 2017 11:07:30 UTC+1, Hadrien Grasland a écrit :
> > > Le samedi 11 février 2017 10:57:58 UTC+1, Hadrien Grasland a écrit :
> > > > Le samedi 11 février 2017 04:07:43 UTC+1, stevensele...@gmail.com a écrit :
> > > > > It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
> > > > > 
> > > > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
> > > > > 
> > > > > There's also a lock-free condition variable like thing
> > > > > 
> > > > > https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD
> > > > 
> > > > Actually, I'm not convinced that Ada atomics provide the required properties for what you're trying to do here.
> > > > 
> > > > To me, Ada's "Atomic", as defined by section C.6 of the Ada 2012 RM, provides essentially the same synchronization guarantees as Java's "volatile":
> > > > 
> > > > 1/Each read from an atomic variable is atomic.
> > > > 2/Each write to an atomic variable is atomic.
> > > > 3/Each thread sees the same atomic writes occuring, without reordering.
> > > > 
> > > > What it does not guarantee, however, is that nothing will happen between the time where a thread reads from a variable, and the time where a thread writes to a variable. Which means, for example, that "X := X + 1" is a race condition in Ada even if X is atomic.
> > > > 
> > > > It also means that the Linted.Compare_And_Swap primitive that your lock-free stack is using has a race condition inside of it, as far as I can tell. From https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.adb;h=a0a59e66568c8b5e11318691d97608dc33363315;hb=HEAD ...
> > > > 
> > > >   26       procedure Compare_And_Swap
> > > >   27         (Old_Ptr : Element_T;
> > > >   28          New_Ptr : Element_T;
> > > >   29          Success : in out Boolean)
> > > >   30       is
> > > >   31       begin
> > > >   32          if Old_Ptr = Ptr then
> > > >   33             Ptr := New_Ptr;
> > > >   34             Success := True;
> > > >   35          else
> > > >   36             Success := False;
> > > >   37          end if;
> > > >   38       end Compare_And_Swap;
> > > > 
> > > > ...you actually cannot guarantee that Ptr will not be updated by another thread between the time where you check it at line 32 and the time where you write to it at line 33, which means that you have a data race on your hands.
> > > > 
> > > > You could expose this by running two tasks in parallel, have them call compare-and-swap on a shared memory location, and see if you can observe an inconsistent memory state (i.e. one where a task should have not written to memory but did so anyway).
> > > 
> > > If Ada atomics end up not doing what you want, you have essentially three options:
> > > 
> > > * Drop hardware portability and write assembly code that calls the atomic read-modify-write operations of you target CPU.
> > > * Drop compiler portability and use compiler-provided atomic operations such as GNAT's System.Atomic_Counters.
> > > * Write your atomic operations in a language with standard support for hardware atomic read-modify-write operations, such as C99 or C++11.
> > 
> > -C99 +C11
> 
> Ah, sorry. I just noticed that your Compare_And_Swap is implemented as part of a protected type.
> 
> Then the problem is actually simpler: your queue is not lock-free, because the protected type implementation very likely has a mutex inside of it.

see https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-atomics.ads;h=2f668cb3e941a279cec9437c239348030b1c35c4;hb=HEAD#l20

I use a small GNAT extension (which is not as good as actual low-level atomics but still pretty good) to have lock free behaviour and protected type semantics.

Re: Lock-Free stack in Ada SPARK

[Jeffrey R. Carter]

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

Re: Lock-Free stack in Ada SPARK

[stevenselectronicmail]

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

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

On 2017-02-11 20:36, 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.

Yes.

> To my mind, that's an implementation of a lock, and I don't understand
> why these are considered lock free.

You are right. An implementation based on protected objects is clearly a 
blocking.

Yet in its idea protected objects meant to be somewhere in-between. 
Logically, at the application level, a protected action is considered 
"instant" and thus logically it is "lock-free", provided the programmer 
does not abuse it running cycles on the context of a protected action.

But it is not instant at the machine level. If the protected object 
overhead were comparable to a few normal processor instructions and 
would never cause any task losing the CPU, then it might be considered 
"lock-free" both logically and physically. But it certainly not so on 
most architectures.

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

Re: Lock-Free stack in Ada SPARK

[stevenselectronicmail]

On Saturday, February 11, 2017 at 2:40:23 PM UTC-8, Dmitry A. Kazakov wrote:
> On 2017-02-11 20:36, 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.
> 
> Yes.
> 
> > To my mind, that's an implementation of a lock, and I don't understand
> > why these are considered lock free.
> 
> You are right. An implementation based on protected objects is clearly a 
> blocking.
> 
> Yet in its idea protected objects meant to be somewhere in-between. 
> Logically, at the application level, a protected action is considered 
> "instant" and thus logically it is "lock-free", provided the programmer 
> does not abuse it running cycles on the context of a protected action.
> 
> But it is not instant at the machine level. If the protected object 
> overhead were comparable to a few normal processor instructions and 
> would never cause any task losing the CPU, then it might be considered 
> "lock-free" both logically and physically. But it certainly not so on 
> most architectures.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de

Dmitry you seem confused. I don't use normal protected objects. I use the special Lock_Free pragma which allows to generate lock-free code for certain very restricted protected objects.

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

On 2017-02-12 00:02, stevenselectronicmail@gmail.com wrote:

> I don't use normal protected objects. I use the special Lock_Free
> pragma which allows to generate lock-free code for certain very
> restricted protected objects.

If that works... So far GNAT has difficulties already with pragma Atomic 
which fails on 64-bit objects for 32-bit targets. I would guess that 
Lock_Free will fails even quicker.

P.S. I am using GCC built-ins where Atomic fails.

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

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

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.

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

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

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le dimanche 12 février 2017 13:26:13 UTC+1, Hadrien Grasland a écrit :
> 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.

As an aside, notice that in the example above, if an infinite amount of other threads are concurrently manipulating the RCU structure, a thread can still end up being effectively blocked.

Algorithms which manage to avoid this caveat are called wait-free, with several sub-flavors depending on what guarantees they make about the execution time of a thread trying to manipulate the data structure under contention.

Although lock-free techniques are sometimes marketed as a magical antidote to poor parallel scalability, there are usually major tradeoffs involved when picking a lock-free algorithm over a lock-based one:

- Lock-free algorithms are more complex, and thus more likely to have bugs (just ponder how one should carry out garbage collection in the Linux RCU design)
- They are often less CPU- and memory-efficient in the absence of contention (RCU-like designs require memory copies which are not needed when using locked data structures)
- In the presence of heavy contention, lock-free algorithms tend to keep CPUs and caches spinning where a good mutex implementation would have made at least some threads go idle and reduce the overall system load.
- The performance characteristics of a lock-free algorithm are usually less portable from one hardware platform to another. They may even change from one version of an hardware platform to another (e.g. Sandy Bridge's compare-and-swap instruction is an order of magnitude slower than Nehalem's under contention)

To sum it up, lock-free algorithms are a complex and not very portable way to design shared data structures which can provide better performance and scalability characteristics than lock-based ones in situation where you have a bit of contention, but not too much. They are far from a magical bullet, and in many cases better results can be achieved by refraining from sharing data altogether. But sometimes, they're just the right answer to your problem.

Re: Lock-Free stack in Ada SPARK

[Hadrien Grasland]

Le dimanche 12 février 2017 13:49:54 UTC+1, Dmitry A. Kazakov a écrit :
> 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.

In this case, the integer itself is lock-free (if a thread stops writing to it, other threads will still be able to), but the algorithm of the waiting thread isn't lock-free.

This is why I tried to use terminology that puts the focus on objects (i.e. combinations of data structures and algorithms) rather than data alone.


> 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.

I wouldn't say that this is always the case. For example, consider the following (admittedly inefficient) algorithm for finding prime numbers in a certain range [1, N]:

- Let there be a shared counter C, starting at value 1, a master thread, and a pool of N worker threads.
- Each worker thread runs on a loop doing the following:
   * Atomically increment C and check its value X.
   * Stop if X is greater than or equal to N.
   * Otherwise, check if X is prime.
   * If it is, add it to an internal list of primes and start over.
- Once all threads are finished, the master thread collects and merges the intermediate lists of primes of each thread to get the final global list of primes.

In this design, the master thread's algorithm is obviously not lock-free (it has to wait for the workers), but the worker thread's algorithms is. No spinning is involved when incrementing the atomic counter: the hardware takes care of all required synchronization for you using some cache trickery. And modern Intel hardware is remarkably scalable in the presence of concurrent atomic increments:

https://1.bp.blogspot.com/-wVF9DuFkrzk/Tm4nQC-ZNEI/AAAAAAAAABE/MQ6jfEoMc3s/s1600/atomics.png

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

On 2017-02-12 14:19, Hadrien Grasland wrote:
> Le dimanche 12 février 2017 13:49:54 UTC+1, Dmitry A. Kazakov a écrit :
>> 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.
>
> In this case, the integer itself is lock-free (if a thread stops
> writing to it, other threads will still be able to), but the algorithm
> of the waiting thread isn't lock-free.

Being lock-free must be a property of an object.

> This is why I tried to use terminology that puts the focus on
> objects  (i.e. combinations of data structures and algorithms) rather than data
> alone.

Integer is such an object with operations read and write. It can be 
lock-free, e.g. with pragma Atomic in effect or not when encapsulated in 
a protected object or handled by a monitor task. All this has nothing to 
do with any algorithm that may deploy this integer.

>> 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.
>
> I wouldn't say that this is always the case. For example, consider
> the  following (admittedly inefficient) algorithm for finding prime numbers
> in a certain range [1, N]:
>
> - Let there be a shared counter C, starting at value 1, a master thread, and a pool of N worker threads.
> - Each worker thread runs on a loop doing the following:
>    * Atomically increment C and check its value X.
>    * Stop if X is greater than or equal to N.
>    * Otherwise, check if X is prime.
>    * If it is, add it to an internal list of primes and start over.
> - Once all threads are finished, the master thread collects and
> merges  the intermediate lists of primes of each thread to get the final global
> list of primes.
>
> In this design, the master thread's algorithm is obviously not
> lock-free (it has to wait for the workers), but the worker thread's
> algorithms is.

They are not if atomic increment is not, e.g. handled by a monitor task. 
Nor are they lock-free at the point they must hand their lists over to 
the main task.

The point stands, if synchronization is needed, you either wait or 
retry. Being lock-free does not mean no synchronization, without 
synchronization there is no concurrent decomposition. Lock-free means a 
certain method of synchronization.

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

Re: Lock-Free stack in Ada SPARK

[Robert Eachus]

I see some dangerous thinking going on here.  Many years ago, at Hopneywell, I pointed out that the plan to grow from two to four CPUs in the DPS6 line was missing a key project schedule issue.  The current OS had lots of deadlock free locks, but they were not livelock free.  The cure was simple in one sense.  Every place that had one lock needed three.  Pairs of CPUs would contend for one of the new locks, and once they had it, could contend for the master lock.

We were able to automate most of the work, but there were a few dozen RMW instructions that were not part of the standard lock pattern, and converting them to the (new) standard pattern took longer than dealing with the majority. Just about every data table in the OS needed these locks.

Anyway, I used a tool to create a Markov chain model that allowed us to prove a lot of useful properties about the algorithm used. It also showed that for producer consumer cases, where there was one consumer, like a disk drive controller, we didn't need to do this. (Those waiting might get served out-of-order, but no livelocks or starvation.) We only needed the two-level locks for cases where all contenders were equal.*  The dining philosophers is the classic case--deadlocks occur when all philosophers pick up say the left fork first.  This turns into livelock if the philosophers put down the first fork if they can't pick up the second one.  A lot less likely, but in our OS locks livelock could have occurred several times a day.

Oh, and another neat trick, what if you need to grab multiple locks, and want to insure that you do not create a deadlock?  Never contend for a lock that has a lower address than a lock you hold.  By assigning addresses carefully you can insure that locking errors will normally be avoided, and will be detected when, for example, the OS tries to acquire a lock for your application while your program holds a (non-OS) lock.

* Why not make the contenders non-equal?  They were running the same (shared) OS code.  I guess we could have had two different OS images, but this was back when memory was expensive.

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

On 12/02/2017 23:25, Robert Eachus wrote:

> I see some dangerous thinking going on here.
[...]

Why? Actually when cores are cheap lock-free approach becomes preferable 
or the only way, e.g. in the case of a distributed system.

Regarding locks priorities, yes, it is IMO the easiest approach to 
prevent deadlocks, but it also introduces a danger of priority inversion.

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

Re: Lock-Free stack in Ada SPARK

[stevenselectronicmail]

On Sunday, February 12, 2017 at 2:25:53 PM UTC-8, Robert Eachus wrote:
> I see some dangerous thinking going on here.  Many years ago, at Hopneywell, I pointed out that the plan to grow from two to four CPUs in the DPS6 line was missing a key project schedule issue.  The current OS had lots of deadlock free locks, but they were not livelock free.  The cure was simple in one sense.  Every place that had one lock needed three.  Pairs of CPUs would contend for one of the new locks, and once they had it, could contend for the master lock.
> 
> We were able to automate most of the work, but there were a few dozen RMW instructions that were not part of the standard lock pattern, and converting them to the (new) standard pattern took longer than dealing with the majority. Just about every data table in the OS needed these locks.
> 
> Anyway, I used a tool to create a Markov chain model that allowed us to prove a lot of useful properties about the algorithm used. It also showed that for producer consumer cases, where there was one consumer, like a disk drive controller, we didn't need to do this. (Those waiting might get served out-of-order, but no livelocks or starvation.) We only needed the two-level locks for cases where all contenders were equal.*  The dining philosophers is the classic case--deadlocks occur when all philosophers pick up say the left fork first.  This turns into livelock if the philosophers put down the first fork if they can't pick up the second one.  A lot less likely, but in our OS locks livelock could have occurred several times a day.
> 
> Oh, and another neat trick, what if you need to grab multiple locks, and want to insure that you do not create a deadlock?  Never contend for a lock that has a lower address than a lock you hold.  By assigning addresses carefully you can insure that locking errors will normally be avoided, and will be detected when, for example, the OS tries to acquire a lock for your application while your program holds a (non-OS) lock.
> 
> * Why not make the contenders non-equal?  They were running the same (shared) OS code.  I guess we could have had two different OS images, but this was back when memory was expensive.

I think dealing with live-lock would require wait-free data structures which are significantly more difficult to implement. I am currently working on an approach that uses thread local nodes threaded together into a linked list. The initial registration of a node first time through is not wait-free but once registered the functions could iterate through the list and ensure wait-freedom for all tasks.

Re: Lock-Free stack in Ada SPARK

[Robert Eachus]

On Monday, February 13, 2017 at 3:04:01 PM UTC-5, stevensele...@gmail.com wrote:
 
> I think dealing with live-lock would require wait-free data structures which are significantly more difficult to implement. I am currently working on an approach that uses thread local nodes threaded together into a linked list. The initial registration of a node first time through is not wait-free but once registered the functions could iterate through the list and ensure wait-freedom for all tasks.

Exactly. If there are only at most two threads/tasks/processes/whatever contending for a lock, you can't have livelock. You also won't have starvation, or the subway train bunching problem.  (Where with equal priority threads, one thread eventually ends up heavily loaded and leading a sequence of lightly loaded threads.  Important to avoid if you are trying to do load balancing.)

Also if all the tasks are waiting for a single resource, hold no locks while waiting--any additional locks are acquired within the (Ada) rendezvous--that is an "easy" scheduling problem to solve.  Even if you need multiple priorities for waiting tasks. (Not necessarily Ada or system priorities, but something that can be handled nicely in Ada with an entry family.)

Are there existing, proven solutions for many busy waiters?  Yes, and if you need one, it is a good idea to choose one rather than try to devise a new one.  The hierarchical solution I mentioned is probably the easiest to implement using RMW memory cycles.

Re: Lock-Free stack in Ada SPARK

[Dmitry A. Kazakov]

On 21/02/2017 02:51, Robert Eachus wrote:

> Are there existing, proven solutions for many busy waiters?

There is no such problem, IMO. Lock-free methods are not composable 
(even less that blocking ones). So you would not come to the point where 
you could have one-grabbing-many synchronization problem. Lock-free is 
far too low-level and too complicated for that. You get stuck long 
before that...

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