Library mcertikos.ipc.PHThreadCSource

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

extern void acquire_lock_SC(unsigned int);
extern unsigned int get_sync_chan_busy(unsigned int);
extern void set_sync_chan_busy(unsigned int, unsigned int);
extern void thread_sleep(unsigned int);

void
syncsendto_chan_pre (unsigned int chid)
{
  unsigned int chanid;
  chanid = SLEEP_Q_START + chid;
  acquire_lock_CHAN (chanid);
  if (get_syncchan_busy (chanid) == 0)
  {
    set_syncchan_busy (chanid, 1);
  }
  else
  {
    thread_sleep (chid);
    acquire_lock_CHAN (chanid);
  }
}

Local Open Scope positive_scope.
Let _chid : ident := 1.
Let _chanid : ident := 101.

Local Open Scope Z_scope.

Definition syncsendto_chan_pre_body : statement :=
(Ssequence
  (Sset _chanid
    (Ebinop Oadd
      (Ebinop Oadd
        (Ebinop Oadd (Econst_int (Int.repr 0) tint)
          (Econst_int (Int.repr 8) tint) tint) (Econst_int (Int.repr 8) tint)
        tint) (Etempvar _chid tuint) tuint))
  (Ssequence
    (Scall None
      (Evar acquire_lock_CHAN (Tfunction (Tcons tuint Tnil) tvoid
                                 cc_default))
      ((Etempvar _chanid tuint) :: nil))
    (Ssequence
      (Scall (Some 41%positive)
        (Evar get_sync_chan_busy (Tfunction (Tcons tuint Tnil) tuint
                                   cc_default))
        ((Etempvar _chanid tuint) :: nil))
      (Sifthenelse (Ebinop Oeq (Etempvar 41%positive tuint)
                     (Econst_int (Int.repr 0) tint) tint)
        (Scall None
          (Evar set_sync_chan_busy (Tfunction
                                     (Tcons tuint (Tcons tuint Tnil)) tvoid
                                     cc_default))
          ((Etempvar _chanid tuint) :: (Econst_int (Int.repr 1) tint) :: nil))
        (Ssequence
          (Scall None
            (Evar thread_sleep (Tfunction (Tcons tuint Tnil) tvoid
                                  cc_default))
            ((Etempvar _chid tuint) :: nil))
          (Scall None
            (Evar acquire_lock_CHAN (Tfunction (Tcons tuint Tnil) tvoid
                                       cc_default))
            ((Etempvar _chanid tuint) :: nil))))))).

Definition f_syncsendto_chan_pre := {|
                                     fn_return := tvoid;
                                     fn_callconv := cc_default;
                                     fn_params := ((_chid, tuint) :: nil);
                                     fn_vars := nil;
                                     fn_temps := ((_chanid, tuint) :: (41%positive, tuint) :: nil);
                                     fn_body := syncsendto_chan_pre_body
                                   |}.

extern unsigned int get_sync_chan_busy(unsigned int);
extern unsigned int ipc_receive_body(unsigned int, unsigned int, unsigned int);
extern unsigned int thread_wakeup(unsigned int);
extern void set_sync_chan_busy(unsigned int, unsigned int);


unsigned int
tryreceive_chan (unsigned int chanid, unsigned int vaddr, unsigned int rcount)
{
  unsigned int res;
  unsigned int chid;
  chid = SLEEP_Q_START + chanid;
  if (get_sync_chan_busy (chid) == 0)
  {
    return 0;
  }
  else
  {
    res = ipc_receive_body (chid, vaddr, rcount);
    if (thread_wakeup (chanid) == 0)
    {
      set_sync_chan_busy (chid, 0);
    }
    return res;
  }
}

Local Open Scope positive_scope.

Let _vaddr : ident := 2.
Let _rcount : ident := 3.
Let _res : ident := 4.

Local Open Scope Z_scope.

Definition tryreceive_chan_body : statement :=
  (Ssequence
    (Sset _chid
    (Ebinop Oadd
      (Ebinop Oadd
        (Ebinop Oadd (Econst_int (Int.repr 0) tint)
          (Econst_int (Int.repr 8) tint) tint) (Econst_int (Int.repr 8) tint)
        tint) (Etempvar _chanid tuint) tuint))
    (Ssequence
      (Scall (Some 48%positive)
        (Evar get_sync_chan_busy (Tfunction (Tcons tuint Tnil) tuint
                                    cc_default))
        ((Etempvar _chid tuint) :: nil))
      (Sifthenelse (Ebinop Oeq (Etempvar 48%positive tuint)
                     (Econst_int (Int.repr 0) tint) tint)
        (Sreturn (Some (Econst_int (Int.repr 0) tint)))
        (Ssequence
            (Scall (Some _res)
              (Evar ipc_receive_body (Tfunction
                                        (Tcons tuint
                                          (Tcons tuint (Tcons tuint Tnil)))
                                        tuint cc_default))
              ((Etempvar _chid tuint) :: (Etempvar _vaddr tuint) ::
               (Etempvar _rcount tuint) :: nil))
          (Ssequence
            (Ssequence
              (Scall (Some 47%positive)
                (Evar thread_wakeup (Tfunction (Tcons tuint Tnil) tuint
                                       cc_default))
                ((Etempvar _chanid tuint) :: nil))
              (Sifthenelse (Ebinop Oeq (Etempvar 47%positive tuint)
                             (Econst_int (Int.repr 0) tint) tint)
                (Scall None
                  (Evar set_sync_chan_busy (Tfunction
                                              (Tcons tuint
                                                (Tcons tuint Tnil)) tvoid
                                              cc_default))
                  ((Etempvar _chid tuint) ::
                   (Econst_int (Int.repr 0) tint) :: nil))
                Sskip))
            (Sreturn (Some (Etempvar _res tuint)))))))).

Definition f_tryreceive_chan := {|
                                 fn_return := tuint;
                                 fn_callconv := cc_default;
                                 fn_params := ((_chanid, tuint) :: (_vaddr, tuint) :: (_rcount, tuint) :: nil);
                                 fn_vars := nil;
                                 fn_temps := ((_res, tuint) :: (_chid, tuint) ::
                                                            (48%positive, tuint) :: (47%positive, tuint) :: nil);
                                 fn_body := tryreceive_chan_body

                               |}.