Library mcertikos.proc.PCVOpCSource

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.

      #define READY 0
      #define num_chan 263317
      
      extern unsigned int kctxt_new(void *, unsigned int, unsigned int);
      extern void set_state(unsigned int, unsigned int);
      extern void enqueue(unsigned int, unsigned int);
      extern unsigned int get_CPU_ID(void);
      extern void tcb_set_CPU_ID(unsigned int, unsigned int);
      
      unsigned int thread_spawn(void * entry, unsigned int id, unsigned int quota)
      {
          unsigned int i, cpuid;
          i = kctxt_new(entry, id, quota);
          set_state(i, READY);
          cpuid = get_CPU_ID();
          enqueue(cpuid, i);
          tcb_set_CPU_ID(i, cpuid);
          return i;
      }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let tentry: ident := 1.
Let _i: ident := 2.
Let _id: ident := 3.
Let _quota: ident := 4.
Let _entry: ident := 5.
Let _cpuid: ident := 6.

Local Open Scope Z_scope.

Definition thread_spawn_body : statement :=
  (Ssequence
     (Scall (Some _i)
            (Evar kctxt_new (Tfunction
                               (Tcons (tptr tvoid)
                                      (Tcons tuint (Tcons tuint Tnil))) tuint
                               cc_default))
            ((Etempvar _entry (tptr tvoid)) :: (Etempvar _id tuint) ::
                                            (Etempvar _quota tuint) :: nil))
     (Ssequence
        (Scall None
               (Evar set_state (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                          cc_default))
               ((Etempvar _i tuint) :: (Econst_int (Int.repr 0) tint) :: nil))
        (Ssequence
           (Scall (Some _cpuid)
                  (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
           (Ssequence
              (Scall None
                     (Evar enqueue (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                              cc_default))
                     ((Etempvar _cpuid tuint) :: (Etempvar _i tuint) :: nil))
              (Ssequence
                 (Scall None
                        (Evar tcb_set_CPU_ID (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                                        tvoid cc_default))
                        ((Etempvar _i tuint) :: (Etempvar _cpuid tuint) :: nil))
                 (Sreturn (Some (Etempvar _i tuint))))))))
.

Definition f_thread_spawn :=
  {|
    fn_return := tint;
    fn_callconv := cc_default;
    fn_vars := nil;
    fn_params := ((_entry, tptr tvoid) :: (_id, tint) :: (_quota, tint) :: nil);
    fn_temps := ((_i, tint) :: (_cpuid, tint) :: nil);
    fn_body := thread_spawn_body
  |}.

    #define TOTAL_CPU 8
    #define TSTATE_RUN 1

    extern void fifobbq_pool_init(unsigned int);
    extern void set_curid_init(unsigned int);
    extern void set_state(unsigned int, unsigned int);
    extern unsigned int get_CPU_ID(void);
    extern void tcb_set_CPU_ID(unsigned int, unsigned int);

    void sched_init(unsigned int mbi_adr)
    {
        unsigned int cpuid;
        unsigned int i;
        fifobbq_pool_init(mbi_adr);

        i = 0;
        while (i < TOTAL_CPU){
            set_curid_init(i);
            i++;
        }
        set_state(0, TSTATE_RUN);
        cpuid = get_CPU_ID();
        tcb_set_CPU_ID(0, cpuid);
    }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let tmbi_adr: ident := 7.
Let tindex : ident := 8.
Let tcpuid : ident := 9.

Local Open Scope Z_scope.

Definition sched_init_while_loop_cond : expr :=
  (Ebinop Olt (Etempvar tindex tuint) (Econst_int (Int.repr TOTAL_CPU) tint) tint).

Definition sched_init_while_loop_body : statement :=
  (Ssequence
     (Scall None
            (Evar set_curid_init (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar tindex tuint) :: nil))
     (Sset tindex
           (Ebinop Oadd (Etempvar tindex tuint) (Econst_int (Int.repr 1) tint) tuint))).

Definition sched_init_body : statement :=
  (Ssequence
     (Scall None
            (Evar fifobbq_pool_init (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar tmbi_adr tuint) :: nil))
     (Ssequence
        (Sset tindex (Econst_int (Int.repr 0) tint))
        (Ssequence
           (Swhile sched_init_while_loop_cond
                   sched_init_while_loop_body)
           (Ssequence
              (Scall None
                     (Evar set_state (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                                cc_default))
                     ((Econst_int (Int.repr 0) tint) :: (Econst_int (Int.repr 1) tint) :: nil))
              (Ssequence
                    (Scall (Some tcpuid)
                           (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
                    (Scall None
                           (Evar tcb_set_CPU_ID (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                                           tvoid cc_default))
                           ((Econst_int (Int.repr 0) tint) :: (Etempvar tcpuid tuint) ::
                                                           nil))))))).

Definition f_sched_init :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_vars := nil;
    fn_params := ((tmbi_adr, tint) :: nil);
    fn_temps := ((tcpuid, tint) :: (tindex, tint):: nil);
    fn_body := sched_init_body
  |}.

      #define TSTATE_DEAD 3
      
      extern void set_state(unsigned int, unsigned int);
      extern void queue_rmv(unsigned int, unsigned int);
      extern void thread_free(unsigned int);
      
      void thread_kill(unsigned int proc_index, unsigned int chan_index)
      {
          set_state(proc_index, TSTATE_DEAD);
          queue_rmv(chan_index, proc_index);
          thread_free(proc_index);
      }
Function parameters and local temporaries used in the function
Local Open Scope positive_scope.
Let tproc_index: ident := 9.
Let tchan_index: ident := 10.

Local Open Scope Z_scope.

Definition thread_kill_body : statement :=
  (Ssequence
     (Scall None (Evar set_state (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
            ((Etempvar tproc_index tint) :: (Econst_int (Int.repr TSTATE_DEAD) tint) :: nil))
     (Ssequence
        (Scall None (Evar queue_rmv (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
               ((Etempvar tchan_index tint) :: (Etempvar tproc_index tint) :: nil))
        (Scall None (Evar thread_free (Tfunction (Tcons tint Tnil) tvoid cc_default))
               ((Etempvar tproc_index tint) :: nil)))).

Definition f_thread_kill :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_vars := nil;
    fn_params := ((tproc_index, tint) :: (tchan_index, tint) :: nil);
    fn_temps := nil;
    fn_body := thread_kill_body
  |}.

      #define TSTATE_READY 0
      #define num_proc 1024
      
      extern unsigned int dequeue_atomic(unsigned int);
      extern void set_state(unsigned int, unsigned int);
      extern void enqueue_atomic(unsigned int, unsigned int);
      extern void enqueue(unsigned int, unsigned int);
      extern unsigned int get_CPU_ID(void);
      extern unsigned int tcb_get_CPU_ID(unsigned int);
      extern void sleeper_dec(void);

      unsigned int thread_wakeup(unsigned int cv_index)
      {
          unsigned int proc_index, cpuid, tcb_cpuid;
          proc_index = dequeue_atomic(16 + cv_index);
          if(0 <= proc_index && proc_index < num_proc)
          {
              cpuid = get_CPU_ID();
              tcb_cpuid = tcb_get_CPU_ID(proc_index);
              if (cpuid == tcb_cpuid)
              {
                set_state(proc_index, TSTATE_READY);
                enqueue(cpuid, proc_index);
              }
              else
                enqueue_atomic(cpuid + 8, proc_index);
              return 1;
          }
          else
              return 0;
      }

Let _cv_index: ident := 11 % positive.
Let _curid: ident := 12 % positive.
Let _proc_index: ident := 13 % positive.
Let _tcb_cpuid: ident := 14 % positive.

Definition thread_wakeup_body : statement :=
  (Ssequence
    (Scall (Some _proc_index)
      (Evar dequeue_atomic (Tfunction (Tcons tuint Tnil) tuint cc_default))
      ((Ebinop Oadd (Econst_int (Int.repr 16) tint)
         (Etempvar _cv_index tuint) tuint) :: nil))
  (Ssequence
    (Sifthenelse (Ebinop Ole (Econst_int (Int.repr 0) tint)
                   (Etempvar _proc_index tuint) tint)
      (Ssequence
        (Sset 50%positive
          (Ecast
            (Ebinop Olt (Etempvar _proc_index tuint)
              (Econst_int (Int.repr num_proc) tint) tint) tbool))
        (Sset 50%positive (Ecast (Etempvar 50%positive tbool) tint)))
      (Sset 50%positive (Econst_int (Int.repr 0) tint)))
    (Sifthenelse (Etempvar 50%positive tint)
      (Ssequence
          (Scall (Some _cpuid)
            (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
        (Ssequence
            (Scall (Some _tcb_cpuid)
              (Evar tcb_get_CPU_ID (Tfunction (Tcons tuint Tnil) tuint
                                      cc_default))
              ((Etempvar _proc_index tuint) :: nil))
          (Ssequence
            (Sifthenelse (Ebinop Oeq (Etempvar _cpuid tuint)
                           (Etempvar _tcb_cpuid tuint) tint)
              (Ssequence
                (Scall None
                  (Evar set_state (Tfunction
                                     (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
                  ((Etempvar _proc_index tuint) ::
                   (Econst_int (Int.repr 0) tint) :: nil))
                  (Scall None
                    (Evar enqueue (Tfunction
                                     (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
                    ((Etempvar _cpuid tuint) ::
                     (Etempvar _proc_index tuint) :: nil)))
              (Scall None
                (Evar enqueue_atomic (Tfunction
                                        (Tcons tuint (Tcons tuint Tnil))
                                        tvoid cc_default))
                ((Ebinop Oadd (Etempvar _tcb_cpuid tuint)
                   (Econst_int (Int.repr 8) tint) tuint) ::
                 (Etempvar _proc_index tuint) :: nil)))
            (Sreturn (Some (Econst_int (Int.repr 1) tint))))))
      (Sreturn (Some (Econst_int (Int.repr 0) tint)))))).

Definition f_thread_wakeup :=
  {|
    fn_return := tuint;
    fn_callconv := cc_default;
    fn_params := ((_cv_index, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_proc_index, tuint) :: (_cpuid, tuint) ::
                                      (_tcb_cpuid, tuint) :: (50%positive, tuint) :: nil);
    fn_body := thread_wakeup_body
  |}.

    #define TOTAL_CPU 8
    #define READ_Q_START 0
    #define MSG_Q_START (READ_Q_START + TOTAL_CPU)
    #define TSTATE_READY 0
    #define num_proc 1204
    
    extern unsigned int get_CPU_ID(void);
    extern unsigned int dequeue_atomic(unsigned int);
    extern void set_state(unsigned int, unsigned int);
    extern void tcb_set_CPU_ID(unsigned int, unsigned int);
    extern void enqueue(unsigned int, unsigned int);
    extern void sleeper_dec(void);

    void thread_poll_pending(void)
    {
        unsigned int cpuid, proc_index;
        cpuid = get_CPU_ID();
        proc_index = dequeue_atomic(MSG_Q_START + cpuid);

        if (proc_index != num_proc){
            set_state(proc_index, TSTATE_READY);
            tcb_set_CPU_ID(proc_index, cpuid);
            enqueue(cpuid, proc_index);
            sleeper_dec();
        }   
    }

Definition f_thread_poll_pending_body :=
  (Ssequence
     (Scall (Some _cpuid)
            (Evar get_CPU_ID (Tfunction Tnil tuint cc_default)) nil)
     (Ssequence
        (Scall (Some _proc_index)
               (Evar dequeue_atomic (Tfunction (Tcons tuint Tnil) tuint cc_default))
               ((Ebinop Oadd
                        (Ebinop Oadd (Econst_int (Int.repr 0) tint)
                                (Econst_int (Int.repr 8) tint) tint) (Etempvar _cpuid tuint)
                        tuint) :: nil))
        (Sifthenelse (Ebinop One (Etempvar _proc_index tuint)
                             (Econst_int (Int.repr num_proc) tint) tint)
                     (Ssequence
                        (Scall None
                               (Evar set_state (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                                          cc_default))
                               ((Etempvar _proc_index tuint) :: (Econst_int (Int.repr 0) tint) ::
                                                             nil))
                        (Ssequence
                           (Scall None
                                  (Evar tcb_set_CPU_ID (Tfunction
                                                          (Tcons tuint (Tcons tuint Tnil)) tvoid
                                                          cc_default))
                                  ((Etempvar _proc_index tuint) :: (Etempvar _cpuid tuint) :: nil))
                           (Ssequence
                              (Scall None
                                     (Evar enqueue (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                                              tvoid cc_default))
                                     ((Etempvar _cpuid tuint) :: (Etempvar _proc_index tuint) ::
                                                              nil))
                              (Scall None (Evar sleeper_dec (Tfunction Tnil tvoid cc_default))
                                     nil))))
                     Sskip))).

Definition f_thread_poll_pending :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := nil;
    fn_vars := nil;
    fn_temps := ((_cpuid, tuint) :: (_proc_index, tuint) :: nil);
    fn_body := f_thread_poll_pending_body
  |}.