Library mcertikos.proc.QueueIntroGenLinkSource

Require Import LinkSourceTemplate.
Require Import CDataTypes.
Require Import PSleeper.
Require Import PSleeperCSource.
Require Import QueueIntroGenAsmSource.

Definition PQueueIntro_module: link_module :=
  {|
    lm_cfun :=
      lcf get_state f_tcb_get_state ::
      lcf get_prev f_tcb_get_prev ::
      lcf get_next f_tcb_get_next ::
      lcf tcb_get_CPU_ID f_tcb_get_CPU_ID_state ::
      lcf set_state f_tcb_set_state ::
      lcf set_prev f_tcb_set_prev ::
      lcf set_next f_tcb_set_next ::
      lcf tcb_set_CPU_ID f_tcb_set_CPU_ID_state ::
      lcf tcb_init f_tcb_init ::
      lcf get_head f_tdq_get_head ::
      lcf get_tail f_tdq_get_tail ::
      lcf set_head f_tdq_set_head ::
      lcf set_tail f_tdq_set_tail ::
      lcf tdq_init f_tdq_init ::
      nil;
    lm_asmfun :=
      laf acquire_lock_TCB acquire_lock_TCB_function ::
      laf release_lock_TCB release_lock_TCB_function ::
      nil;
    lm_gvar :=
      lgv TCBPool_LOC tcbpool_loc_type ::
      nil
  |}.

Definition PQueueIntro_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PQueueIntro_module psleeper.