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.
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;
}
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
|}.
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);
}
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
|}.
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);
}
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
|}.
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
|}.