Re: Lock-Free stack in Ada SPARK

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

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