Library mcertikos.mcslock.MCSLockIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import CDataTypes.
Require Import MCSMCurID.
Require Import MCSMCurIDCSource.
Require Import MCSLockIntroGenAsmSource.

Definition MMCSLockIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf mcs_init_node f_mcs_init_node ::
          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 ::
          nil;
    lm_asmfun :=
      laf mcs_log mcs_log_function ::
          laf mcs_SWAP_TAIL mcs_SWAP_TAIL_function ::
          laf mcs_CAS_TAIL mcs_CAS_TAIL_function ::
          nil;
    lm_gvar :=
      lgv MCS_LOCK_LOC mcslock_loc_type ::
          nil
  |}.

Definition MMCSLockIntro_impl `{CompCertiKOS} `{RealParams} `{MCSOracleProp} :=
  link_impl MMCSLockIntro_module mcurid.