Library mcertikos.proc.ThreadSchedGenLinkSource

Require Import LinkSourceTemplate.
Require Import PCVOp.
Require Import PCVOpCSource.
Require Import ThreadSchedGenAsmSource.

Definition PThreadSched_module: link_module :=
  {|
    lm_cfun :=
      lcf thread_spawn f_thread_spawn ::
      lcf thread_wakeup f_thread_wakeup ::
      lcf sched_init f_sched_init ::
      lcf thread_poll_pending f_thread_poll_pending ::
      nil;
    lm_asmfun :=
      laf thread_sched threadsched_function ::
      nil;
    lm_gvar :=
      nil
  |}.

Definition PThreadSched_impl `{CompCertiKOS} `{RealParams} `{MultiOracleProp} :=
  link_impl PThreadSched_module pcvop.