Library mcertikos.ticketlog.MTicketLockIntroCSource

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

Notation _offset := 40%positive.
Notation _lock_id := 41%positive.
Notation _mbi_addr := 42%positive.
Notation _i := 43%positive.


Definition f_ticket_lock_init_fst_while_condition :=
  (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr num_chan) tint)
          tint).

Definition f_ticket_lock_init_fst_while_body :=
  (Ssequence
     (Scall None
            (Evar init_ticket (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                         tvoid cc_default))
            ((Econst_int (Int.repr 1) tint) :: (Etempvar _i tint) :: nil))
     (Sset _i
           (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint)
                   tint))).

Definition f_ticket_lock_init_snd_while_condition :=
  (Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr num_chan) tint)
          tint).

Definition f_ticket_lock_init_snd_while_body :=
  (Ssequence
     (Scall None
            (Evar init_ticket (Tfunction
                                 (Tcons tuint (Tcons tuint Tnil)) tvoid
                                 cc_default))
            ((Econst_int (Int.repr 2) tint) :: (Etempvar _i tint) :: nil))
     (Sset _i
           (Ebinop Oadd (Etempvar _i tint)
                   (Econst_int (Int.repr 1) tint) tint))).

Definition f_ticket_lock_init_body :=
  (Ssequence
     (Scall None
            (Evar boot_loader (Tfunction (Tcons tuint Tnil) tvoid cc_default))
            ((Etempvar _mbi_addr tuint) :: nil))
     (Ssequence
        (Scall None
               (Evar init_ticket (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                                            cc_default))
               ((Econst_int (Int.repr 0) tint) :: (Econst_int (Int.repr 0) tint) ::
                                               nil))
        (Ssequence
           (Sset _i (Econst_int (Int.repr 0) tint))
           (Ssequence
              (Swhile f_ticket_lock_init_fst_while_condition
                      f_ticket_lock_init_fst_while_body)
              (Ssequence
                 (Sset _i (Econst_int (Int.repr 0) tint))
                 (Swhile f_ticket_lock_init_snd_while_condition
                         f_ticket_lock_init_snd_while_body)
  ))))).

Definition f_ticket_lock_init :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_mbi_addr, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_i, tint) :: nil);
    fn_body := f_ticket_lock_init_body
  |}.


Definition f_pass_lock_body :=
  (Scall None (Evar incr_now (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid cc_default))
         ((Etempvar _lock_id tuint) :: (Etempvar _offset tuint) :: nil)).

Definition f_pass_lock :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_lock_id, tuint) :: (_offset, tuint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := f_pass_lock_body
  |}.

Notation _bound := 46%positive.
Notation _my_ticket := 44%positive.
Notation _current_ticket := 45%positive.

Definition f_wait_lock_while_condition :=
  (Ebinop One (Etempvar _my_ticket tuint)
          (Etempvar _current_ticket tuint) tint).

Definition f_wait_lock_while_body :=
  (Scall (Some _current_ticket)
         (Evar get_now (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint cc_default))
         ((Etempvar _lock_id tuint) :: (Etempvar _offset tuint) :: nil)).

Definition f_wait_lock_body :=
  (Ssequence
     (Scall (Some _my_ticket)
            (Evar incr_ticket (Tfunction (Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tuint cc_default))
            ((Etempvar _bound tuint) :: (Etempvar _lock_id tuint) :: (Etempvar _offset tuint) :: nil))
     (Ssequence
        (Scall (Some _current_ticket)
               (Evar get_now (Tfunction (Tcons tuint (Tcons tuint Tnil)) tuint cc_default))
               ((Etempvar _lock_id tuint) :: (Etempvar _offset tuint):: nil))
        (Ssequence
           (Swhile f_wait_lock_while_condition f_wait_lock_while_body)
           (Scall None
                  (Evar log_hold (Tfunction (Tcons tuint (Tcons tuint Tnil))
                                            tvoid cc_default))
                  ((Etempvar _lock_id tint) :: (Etempvar _offset tint) :: nil))))).

Definition f_wait_lock :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_bound, tuint) ::(_lock_id, tuint) :: (_offset, tuint) :: nil);
    fn_vars := nil;
    fn_temps := ((_my_ticket, tuint) :: (_current_ticket, tuint) :: nil);
    fn_body := f_wait_lock_body
  |}.