Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import PrimSemantics.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.

Require Import AbstractDataType.
Require Import MCSMCurID.

Require Import Conventions.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.

Section MCSLOCKINTRO_DEFINE.

  Context `{mcs_oracle_prop: MCSOracleProp}.

  Notation LDATAOps := (cdata RData).

  Inductive mcs_init_node_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    mcs_init_node_spec_low_intro s (WB: _ → Prop) b m m_la m0_bs m0_ne m1_bs m1_ne m2_bs m2_ne m3_bs m3_ne m4_bs m4_ne
                                 m5_bs m5_ne m6_bs m6_ne m7_bs m´ d d´ lock_index:
      ∀ (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (Hspec: mcs_init_node_log_spec (Int.unsigned lock_index) d = Some d´)
             (Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr NULL)) = Some m_la)
             (Hstore_busy0: Mem.store Mint32 m_la b (busy_pos (Int.unsigned lock_index) 0) Vzero = Some m0_bs)
             (Hstore_next0: Mem.store Mint32 m0_bs b (next_pos (Int.unsigned lock_index) 0) (Vint (Int.repr NULL)) = Some m0_ne)
             (Hstore_busy1: Mem.store Mint32 m0_ne b (busy_pos (Int.unsigned lock_index) 1) Vzero = Some m1_bs)
             (Hstore_next1: Mem.store Mint32 m1_bs b (next_pos (Int.unsigned lock_index) 1) (Vint (Int.repr NULL)) = Some m1_ne)
             (Hstore_busy2: Mem.store Mint32 m1_ne b (busy_pos (Int.unsigned lock_index) 2) Vzero = Some m2_bs)
             (Hstore_next2: Mem.store Mint32 m2_bs b (next_pos (Int.unsigned lock_index) 2) (Vint (Int.repr NULL)) = Some m2_ne)
             (Hstore_busy3: Mem.store Mint32 m2_ne b (busy_pos (Int.unsigned lock_index) 3) Vzero = Some m3_bs)
             (Hstore_next3: Mem.store Mint32 m3_bs b (next_pos (Int.unsigned lock_index) 3) (Vint (Int.repr NULL)) = Some m3_ne)
             (Hstore_busy4: Mem.store Mint32 m3_ne b (busy_pos (Int.unsigned lock_index) 4) Vzero = Some m4_bs)
             (Hstore_next4: Mem.store Mint32 m4_bs b (next_pos (Int.unsigned lock_index) 4) (Vint (Int.repr NULL)) = Some m4_ne)
             (Hstore_busy5: Mem.store Mint32 m4_ne b (busy_pos (Int.unsigned lock_index) 5) Vzero = Some m5_bs)
             (Hstore_next5: Mem.store Mint32 m5_bs b (next_pos (Int.unsigned lock_index) 5) (Vint (Int.repr NULL)) = Some m5_ne)
             (Hstore_busy6: Mem.store Mint32 m5_ne b (busy_pos (Int.unsigned lock_index) 6) Vzero = Some m6_bs)
             (Hstore_next6: Mem.store Mint32 m6_bs b (next_pos (Int.unsigned lock_index) 6) (Vint (Int.repr NULL)) = Some m6_ne)
             (Hstore_busy7: Mem.store Mint32 m6_ne b (busy_pos (Int.unsigned lock_index) 7) Vzero = Some m7_bs)
             (Hstore_next7: Mem.store Mint32 m7_bs b (next_pos (Int.unsigned lock_index) 7) (Vint (Int.repr NULL)) = Some m´)
             (Hkern: kernel_mode d),
        mcs_init_node_spec_low_step s WB (Vint lock_index :: nil) (m, d) Vundef (m´, d´).

  Inductive mcs_GET_NEXT_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    mcs_GET_NEXT_spec_low_intro s (WB: _ → Prop) b m d d´ lock_index cpuid next:
      ∀ (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (Hspec: mcs_GET_NEXT_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some d´)
             (Hlaod: Mem.load Mint32 m b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) = Some (Vint next))
             (Hkern: kernel_mode d),
             mcs_GET_NEXT_spec_low_step s WB (Vint lock_index :: Vint cpuid :: nil) (m, d) (Vint next) (m, d´).

  Inductive mcs_SET_NEXT_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    mcs_SET_NEXT_spec_low_intro s (WB: _ → Prop) b m m´ d d´ lock_index cpuid prev_id:
      ∀ (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (previd_range: 0 ≤ (Int.unsigned prev_id) < TOTAL_CPU)
             (Hspec: mcs_SET_NEXT_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) (Int.unsigned prev_id) d = Some d´)
             (Hstore: Mem.store Mint32 m b (next_pos (Int.unsigned lock_index) (Int.unsigned prev_id)) (Vint cpuid) = Some m´)
             (Hkern: kernel_mode d),
             mcs_SET_NEXT_spec_low_step s WB (Vint lock_index :: Vint cpuid :: Vint prev_id :: nil) (m, d) Vundef (m´, d´).

  Inductive mcs_GET_BUSY_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    mcs_GET_BUSY_spec_low_intro s (WB: _ → Prop) b m d d´ lock_index cpuid busy:
      ∀ (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (Hspec: mcs_GET_BUSY_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some d´)
             (Hlaod: Mem.load Mint32 m b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) = Some (Vint busy))
             (Hkern: kernel_mode d),
             mcs_GET_BUSY_spec_low_step s WB (Vint lock_index :: Vint cpuid :: nil) (m, d) (Vint busy) (m, d´).

  Inductive mcs_SET_BUSY_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    mcs_SET_BUSY_spec_low_intro s (WB: _ → Prop) b m m´ d d´ lock_index cpuid next:
      ∀ (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (next_range: 0 ≤ (Int.unsigned next) < TOTAL_CPU)
             (Hspec: mcs_SET_BUSY_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some d´)
             (Hload: Mem.load Mint32 m b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid)) = Some (Vint next))
             (Hstore: Mem.store Mint32 m b (busy_pos (Int.unsigned lock_index) (Int.unsigned next)) Vzero = Some m´)
             (Hkern: kernel_mode d),
             mcs_SET_BUSY_spec_low_step s WB (Vint lock_index :: Vint cpuid :: nil) (m, d) Vundef (m´, d´).

  Inductive mcs_log_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    mcs_log_low_intro s m m_la m0_bs m0_ne m1_bs m1_ne m2_bs m2_ne m3_bs m3_ne
                           m4_bs m4_ne m5_bs m5_ne m6_bs m6_ne m7_bs m´
                           b b0 d d´ rs sig lock_index cpuid la
                           bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7
                           ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7:
      ∀ (Hsymbol0: find_symbol s mcs_log = Some b0)
             (HPC: rs PC = Vptr b0 Int.zero)
             (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (Hspec: atomic_mcs_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d
                     = Some (d´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
                             (ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)))
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr la)) = Some m_la)
             (Hstore_busy0: Mem.store Mint32 m_la b (busy_pos (Int.unsigned lock_index) 0) (Vint (Int.repr bs0)) = Some m0_bs)
             (Hstore_next0: Mem.store Mint32 m0_bs b (next_pos (Int.unsigned lock_index) 0) (Vint (Int.repr ne0)) = Some m0_ne)
             (Hstore_busy1: Mem.store Mint32 m0_ne b (busy_pos (Int.unsigned lock_index) 1) (Vint (Int.repr bs1)) = Some m1_bs)
             (Hstore_next1: Mem.store Mint32 m1_bs b (next_pos (Int.unsigned lock_index) 1) (Vint (Int.repr ne1)) = Some m1_ne)
             (Hstore_busy2: Mem.store Mint32 m1_ne b (busy_pos (Int.unsigned lock_index) 2) (Vint (Int.repr bs2)) = Some m2_bs)
             (Hstore_next2: Mem.store Mint32 m2_bs b (next_pos (Int.unsigned lock_index) 2) (Vint (Int.repr ne2)) = Some m2_ne)
             (Hstore_busy3: Mem.store Mint32 m2_ne b (busy_pos (Int.unsigned lock_index) 3) (Vint (Int.repr bs3)) = Some m3_bs)
             (Hstore_next3: Mem.store Mint32 m3_bs b (next_pos (Int.unsigned lock_index) 3) (Vint (Int.repr ne3)) = Some m3_ne)
             (Hstore_busy4: Mem.store Mint32 m3_ne b (busy_pos (Int.unsigned lock_index) 4) (Vint (Int.repr bs4)) = Some m4_bs)
             (Hstore_next4: Mem.store Mint32 m4_bs b (next_pos (Int.unsigned lock_index) 4) (Vint (Int.repr ne4)) = Some m4_ne)
             (Hstore_busy5: Mem.store Mint32 m4_ne b (busy_pos (Int.unsigned lock_index) 5) (Vint (Int.repr bs5)) = Some m5_bs)
             (Hstore_next5: Mem.store Mint32 m5_bs b (next_pos (Int.unsigned lock_index) 5) (Vint (Int.repr ne5)) = Some m5_ne)
             (Hstore_busy6: Mem.store Mint32 m5_ne b (busy_pos (Int.unsigned lock_index) 6) (Vint (Int.repr bs6)) = Some m6_bs)
             (Hstore_next6: Mem.store Mint32 m6_bs b (next_pos (Int.unsigned lock_index) 6) (Vint (Int.repr ne6)) = Some m6_ne)
             (Hstore_busy7: Mem.store Mint32 m6_ne b (busy_pos (Int.unsigned lock_index) 7) (Vint (Int.repr bs7)) = Some m7_bs)
             (Hstore_next7: Mem.store Mint32 m7_bs b (next_pos (Int.unsigned lock_index) 7) (Vint (Int.repr ne7)) = Some m´)
             (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, d))
             (Hlow: low_level_invariant (Mem.nextblock m) d)
             (Hhigh: high_level_invariant d)
             (Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default)
             (Harg: extcall_arguments rs m sig (Vint lock_index ::Vint cpuid :: nil)),
             let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                        :: RA :: nil)
                                    (undef_regs (List.map preg_of destroyed_at_call) rs)) in
             mcs_log_low_step s rs (m, d) (rs´#PC <- (rs#RA)) (m´, d´).

  Inductive mcs_SWAP_TAIL_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    mcs_SWAP_TAIL_low_intro s m m0 m1 m´ b b0 d d´ rs sig bound lock_index cpuid prev_tail:
      ∀ (Hsymbol0: find_symbol s mcs_SWAP_TAIL = Some b0)
             (HPC: rs PC = Vptr b0 Int.zero)
             (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (Hspec: atomic_mcs_SWAP_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) d
                     = Some (d´, (Int.unsigned prev_tail)))
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint cpuid) = Some m0)
             (Hstore_next: Mem.store Mint32 m0 b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
                                     (Vint (Int.repr NULL)) = Some m1)
             (Hstore_busy: Mem.store Mint32 m1 b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
                                     (Vint Int.one) = Some m´)
             (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, d))
             (Hlow: low_level_invariant (Mem.nextblock m) d)
             (Hhigh: high_level_invariant d)
             (Hsig: sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
             (Harg: extcall_arguments rs m sig (Vint bound :: Vint lock_index ::Vint cpuid :: nil)),
             let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                        :: RA :: nil)
                                    (undef_regs (List.map preg_of destroyed_at_call) rs)) in
             mcs_SWAP_TAIL_low_step s rs (m, d) (rs´#PC <- (rs#RA) #EAX <- (Vint prev_tail)) (m´, d´).

  Inductive mcs_CAS_TAIL_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    mcs_CAS_TAIL_low_intro s m m´ b b0 d d´ rs sig lock_index cpuid new_tail succeed:
      ∀ (Hsymbol0: find_symbol s mcs_CAS_TAIL = Some b0)
             (HPC: rs PC = Vptr b0 Int.zero)
             (Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
             (Hspec: atomic_mcs_CAS_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d
                     = Some (d´, (new_tail, (Int.unsigned succeed))))
             (index_range: 0 ≤ (Int.unsigned lock_index) < lock_range)
             (curid_range: 0 ≤ (Int.unsigned cpuid) < TOTAL_CPU)
             (Hstore: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr new_tail)) = Some m´)
             (Hasm: asm_invariant (mem := mwd LDATAOps) s rs (m, d))
             (Hlow: low_level_invariant (Mem.nextblock m) d)
             (Hhigh: high_level_invariant d)
             (Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
             (Harg: extcall_arguments rs m sig (Vint lock_index ::Vint cpuid :: nil)),
             let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                        :: RA :: nil)
                                    (undef_regs (List.map preg_of destroyed_at_call) rs)) in
             mcs_CAS_TAIL_low_step s rs (m, d) (rs´#PC <- (rs#RA) #EAX <- (Vint succeed)) (m´, d´).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Definition mcs_init_node_spec_low: compatsem LDATAOps :=
      csem mcs_init_node_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition mcs_GET_NEXT_spec_low: compatsem LDATAOps :=
      csem mcs_GET_NEXT_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tint32.

    Definition mcs_SET_NEXT_spec_low: compatsem LDATAOps :=
      csem mcs_SET_NEXT_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Tvoid.

    Definition mcs_GET_BUSY_spec_low: compatsem LDATAOps :=
      csem mcs_GET_BUSY_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tint32.

    Definition mcs_SET_BUSY_spec_low: compatsem LDATAOps :=
      csem mcs_SET_BUSY_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition mcs_log_spec_low: compatsem LDATAOps :=
      asmsem_withsig mcs_log mcs_log_low_step
                     (mksignature (AST.Tint::AST.Tint::nil) None cc_default).

    Definition mcs_SWAP_TAIL_spec_low: compatsem LDATAOps :=
      asmsem_withsig mcs_SWAP_TAIL mcs_SWAP_TAIL_low_step
                     (mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default).

    Definition mcs_CAS_TAIL_spec_low: compatsem LDATAOps :=
      asmsem_withsig mcs_CAS_TAIL mcs_CAS_TAIL_low_step
                     (mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default).

  End WITHMEM.

End MCSLOCKINTRO_DEFINE.