-- Copyright 2017 Steven Stewart-Gallus
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--     http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-- implied.  See the License for the specific language governing
-- permissions and limitations under the License.
private with Linted.ABAs;
private with Linted.Atomics;
private with Linted.Mod_Atomics;
private with Linted.Sched;

generic
   type Element_T is private;
package Linted.Strange_Locks with Spark_Mode is
   pragma Elaborate_Body;

   --  Inspired by seqlocks these are weird;

   type Strange_Lock is limited private;

   procedure Set (Lock : in out Strange_Lock; Element : Element_T);
   procedure Get (Lock : in out Strange_Lock; Element : out Element_T);

private
   pragma Spark_Mode (Off);

   type Word is mod 2 ** 16 with Default_Value => 0;
   package Word_ABAS is new ABAs (Word);
   package Atomic_Word_ABAS is new Atomics (Word_ABAS.ABA);
   package Seqno_Atomics is new Mod_Atomics (Word_ABAS.Tag_T);

   type Storage is array (1 .. Element_T'Size / 32) of Word;

   type Atomic_Storage is array (1 .. Element_T'Size / 32) of Atomic_Word_ABAS.Atomic;

   type Strange_Lock is record
      Seqno : Seqno_Atomics.Atomic;
      Storage : Atomic_Storage;
      Contention : Sched.Contention;
   end record;
end Linted.Strange_Locks;


-- Copyright 2017 Steven Stewart-Gallus
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--     http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-- implied.  See the License for the specific language governing
-- permissions and limitations under the License.
with Ada.Unchecked_Conversion;

package body Linted.Strange_Locks with Spark_Mode => Off is
   use type Word_ABAS.Tag_T;

   function Unsafe_To_Storage is new Ada.Unchecked_Conversion (Element_T, Storage);
   function Unsafe_From_Storage is new Ada.Unchecked_Conversion (Storage, Element_T);

   procedure Set (Lock : in out Strange_Lock; Element : Element_T) is
      Element_Storage : Storage;
      Old_Chunk : Word_ABAS.ABA;
      New_Chunk : Word;
      Seqno : Word_ABAS.Tag_T;
      Success : Boolean;
   begin
      Element_Storage := Unsafe_To_Storage (Element);

      Seqno_Atomics.Increment (Lock.Seqno, Seqno);

      for II in Storage'Range loop
     New_Chunk := Element_Storage (II);

     loop
        Atomic_Word_ABAS.Get (Lock.Storage (II), Old_Chunk);

        exit when Word_ABAS.Tag (Old_Chunk) > Seqno;

        Atomic_Word_ABAS.Compare_And_Swap (Lock.Storage (II),
                           Old_Chunk,
                           Word_ABAS.Initialize (New_Chunk, Seqno),
                           Success);
        exit when Success;
     end loop;
      end loop;
   end Set;

   procedure Get (Lock : in out Strange_Lock; Element : out Element_T) is
      Seqno : Word_ABAS.Tag_T;
      Element_Storage : Storage;
      Chunk : Word_ABAS.ABA;
   begin
      loop
     Seqno_Atomics.Get (Lock.Seqno, Seqno);

     Read_Loop : for II in Storage'Range loop
        loop
           Atomic_Word_ABAS.Get (Lock.Storage (II), Chunk);
           exit when Word_ABAS.Tag (Chunk) = Seqno;
           exit Read_Loop when Word_ABAS.Tag (Chunk) > Seqno;

           if Word_ABAS.Tag (Chunk) < Seqno then
          Sched.Backoff (Lock.Contention);
           end if;
        end loop;
        Sched.Success (Lock.Contention);

        Element_Storage (II) := Word_ABAS.Element (Chunk);
     end loop Read_Loop;
     exit when Word_ABAS.Tag (Chunk) <= Seqno;
      end loop;

      Element := Unsafe_From_Storage (Element_Storage);
   end Get;
end Linted.Strange_Locks;