Library mcertikos.proc.CVIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import PAbQueueAtomic.
Require Import PAbQueueAtomicCSource.
Require Import CVIntroGenAsmSource.

Definition PCVIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf get_sync_chan_to f_get_sync_chan_to ::
      lcf get_sync_chan_paddr f_get_sync_chan_paddr ::
      lcf get_sync_chan_count f_get_sync_chan_count ::
      lcf get_sync_chan_busy f_get_sync_chan_busy ::
      lcf set_sync_chan_to f_set_sync_chan_to ::
      lcf set_sync_chan_paddr f_set_sync_chan_paddr ::
      lcf set_sync_chan_count f_set_sync_chan_count ::
      lcf set_sync_chan_busy f_set_sync_chan_busy ::
      lcf init_sync_chan f_init_sync_chan ::
      lcf get_kernel_pa f_get_kernel_pa ::
      nil;
    lm_asmfun :=
      laf acquire_lock_CHAN acquire_lock_SC_function ::
      laf release_lock_CHAN release_lock_SC_function ::
      nil;
    lm_gvar :=
      (lgv SYNCCHPOOL_LOC syncchpool_loc_type) ::
      nil
  |}.

Definition PCVIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PCVIntro_module pabqueue_atomic.