Library mcertikos.mcslock.MCSLockAbsIntroGenLinkSource

Require Import CDataTypes.
Require Import LinkSourceTemplate.
Require Import MMCSLockIntro.
Require Import MMCSLockIntroCSource.

Definition MMCSLockAbsIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf ticket_lock_init f_mcs_lock_init ::
          lcf mcs_get_next f_mcs_get_next ::
          lcf mcs_set_next f_mcs_set_next ::
          lcf mcs_get_busy f_mcs_get_busy ::
          lcf mcs_set_busy f_mcs_set_busy ::
          lcf mcs_swap_tail f_mcs_swap_tail ::
          lcf mcs_cas_tail f_mcs_cas_tail ::
          lcf mcs_lock_get_index f_mcs_lock_get_index ::
          nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MMCSLockAbsIntro_impl `{CompCertiKOS} `{RealParams} `{MCSOracleProp} :=
  link_impl MMCSLockAbsIntro_module mmcslockintro.