Library mcertikos.mcslock.MCSLockOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import MMCSLockAbsIntro.
Require Import MMCSLockAbsIntroCSource.

Definition MMCSLockOp_module: link_module :=
  {|
    lm_cfun :=
      lcf pass_lock f_mcs_pass_lock ::
          lcf wait_lock f_mcs_wait_lock ::
          nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MMCSLockOp_impl `{CompCertiKOS} `{RealParams} `{MCSOracleProp} :=
  link_impl MMCSLockOp_module mmcslockabsintro.