Library mcertikos.ticketlog.TicketLockOpGenLinkSource

Require Import LinkSourceTemplate.
Require Import MTicketLockIntro.
Require Import MTicketLockIntroCSource.

Definition MTicketLockOp_module: link_module :=
  {|
    lm_cfun :=
      lcf ticket_lock_init f_ticket_lock_init ::
      lcf pass_lock f_pass_lock ::
      lcf wait_lock f_wait_lock ::
      nil;
    lm_asmfun :=
      nil;
    lm_gvar :=
      nil
  |}.

Definition MTicketLockOp_impl `{CompCertiKOS} `{RealParams} `{MultiOracleOps0} `{MultiOracleOps} `{BigOracleOps} :=
  link_impl MTicketLockOp_module mticketlockintro.