Library mcertikos.ticketlog.QTicketLockGenLinkSource

Require Import LinkSourceTemplate.
Require Import MHTicketLockOp.
Require Import QTicketLockGenAsmSource.

Definition MQTicketLock_module: link_module :=
  {|
    lm_cfun :=
      nil;
    lm_asmfun :=
      (laf release_lock release_lock_function)::
      (laf acquire_lock acquire_lock_function)::
      nil;
    lm_gvar :=
      nil
  |}.

Definition MQTicketLock_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl MQTicketLock_module mhticketlockop.