Library mcertikos.proc.ThreadGenAsmSource

Require Import Coqlib.
Require Import Integers.
Require Import Constant.
Require Import GlobIdent.
Require Import AST.

Require Import liblayers.compat.CompatLayers.
Require Import LAsm.

Section ASM_CODE.

  Definition enqueue_atomic_sig:= mksignature (Tint::Tint::nil) None cc_default.
  Definition enqueue_sig:= mksignature (Tint::Tint::nil) None cc_default.
  Definition release_lock_CHAN_sig:= mksignature (Tint::nil) None cc_default.
  Definition set_state_sig := mksignature (Tint::Tint::nil) None cc_default.
  Definition get_curid_sig := mksignature nil (Some Tint) cc_default.
  Definition get_CPU_ID_sig := mksignature nil (Some Tint) cc_default.
  Definition sleeper_inc_sig := mksignature nil None cc_default.
  Definition thread_poll_pending_sig := mksignature nil None cc_default.

  Definition AddrMake (ofs:int) :=
    Addrmode (Some ESP) None (inl ofs).

  Definition AddrMakeArg (ofs:int) :=
    Addrmode (Some EDX) None (inl ofs).

  Definition AddrMake2 (r: ireg) (mul: Z) (c: Z) :=
    Addrmode None (Some (r, Int.repr mul)) (inl (Int.repr c)).

  Definition AddrMake3 (r: ireg) (c: Z) :=
    Addrmode (Some r) None (inl (Int.repr c)).

  Section ThreadYield.


    Definition Im_thread_yield : list instruction :=
      asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8)) ::

                      asm_instruction (Pcall_s thread_poll_pending thread_poll_pending_sig) ::

                      asm_instruction (Pcall_s get_curid get_curid_sig) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 0)) EAX) ::
                      
                      asm_instruction (Pmov_ri EAX (Int.repr 0)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s set_state set_state_sig) ::

                      asm_instruction (Pmov_rm EAX (AddrMake (Int.repr 0))) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s get_CPU_ID get_CPU_ID_sig) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 0)) EAX) ::
                      asm_instruction (Pcall_s enqueue enqueue_sig) ::
                      
                      asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pjmp_s thread_sched null_signature) ::
                      nil.

    Definition threadyield_function: function := mkfunction null_signature Im_thread_yield.

  End ThreadYield.

  Section ThreadSleep.


    Definition Im_thread_sleep : list instruction :=
      asm_instruction (Pallocframe 20 (Int.repr 16) (Int.repr 12)) ::

                      asm_instruction (Pmov_rm EAX (AddrMakeArg (Int.repr 0))) ::

                      asm_instruction (Plea EAX (AddrMake3 EAX SLEEP_Q_START)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 0)) EAX) ::

                      asm_instruction (Pcall_s get_curid get_curid_sig) ::

                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s enqueue_atomic enqueue_atomic_sig) ::

                      asm_instruction (Pcall_s release_lock_CHAN release_lock_CHAN_sig) ::

                      asm_instruction (Pmov_rm EAX (AddrMake (Int.repr 4))) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 0)) EAX) ::
                      asm_instruction (Pmov_ri EAX (Int.repr 2)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s set_state set_state_sig) ::

                      asm_instruction (Pcall_s sleeper_inc sleeper_inc_sig) ::
                      
                      
                      asm_instruction (Pfreeframe 20 (Int.repr 16) (Int.repr 12)) ::
                      asm_instruction (Pjmp_s thread_sched null_signature) ::
                      nil.

    Definition thread_sleep_sig := mksignature (Tint::nil) None cc_default.

    Definition threadsleep_function: function := mkfunction thread_sleep_sig Im_thread_sleep.

  End ThreadSleep.

  Section ThreadKill.


    Definition Im_thread_kill : list instruction :=
      asm_instruction (Pallocframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pcall_s get_curid get_curid_sig) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 0)) EAX) ::
                      
                      asm_instruction (Pmov_ri EAX (Int.repr 3)) ::
                      asm_instruction (Pmov_mr (AddrMake (Int.repr 4)) EAX) ::
                      asm_instruction (Pcall_s set_state set_state_sig) ::
                      
                      asm_instruction (Pfreeframe 16 (Int.repr 12) (Int.repr 8)) ::
                      asm_instruction (Pjmp_s thread_sched null_signature) ::
                      nil.

    Definition threadkill_function: function := mkfunction null_signature Im_thread_kill.

  End ThreadKill.

End ASM_CODE.