Library mcertikos.ticketlog.TicketLockIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import MCurID.
Require Import MCurIDCSource.
Require Import TicketLockIntroGenAsmSource.

Definition MTicketLockIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf incr_now f_incr_now ::
      lcf init_ticket f_init_ticket ::
      nil;
    lm_asmfun :=
      laf incr_ticket incr_ticket_function ::
      laf get_now get_now_function ::
      nil;
    lm_gvar :=
      lgv TICKET_LOCK_LOC ticket_lock_type ::
      nil
  |}.

Definition MTicketLockIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleOps0} `{MultiOracleOps} `{BigOracleOps} :=
  link_impl MTicketLockIntro_module mcurid.