Library mcertikos.proc.PCVOpCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import LoopProof.
Require Import AbstractDataType.
Require Import CalRealProcModule.
Require Import ObjCV.
Require Import PCVOpCSource.
Require Import PCVOp.
Require Import ThreadSchedGenSpec.
Module PCURIDCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SCHEDINIT.
Let L: compatlayer (cdata RData) :=
fifobbq_pool_init ↦ gensem fifobbq_pool_init_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ tcb_set_CPU_ID ↦ gensem set_abtcb_CPU_ID_spec
⊕ set_curid_init ↦ gensem set_curid_init_spec
⊕ set_state ↦ gensem set_state0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SchedInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import TacticsForTesting.
Require Import CommonTactic.
Require Import LoopProof.
Require Import AbstractDataType.
Require Import CalRealProcModule.
Require Import ObjCV.
Require Import PCVOpCSource.
Require Import PCVOp.
Require Import ThreadSchedGenSpec.
Module PCURIDCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SCHEDINIT.
Let L: compatlayer (cdata RData) :=
fifobbq_pool_init ↦ gensem fifobbq_pool_init_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ tcb_set_CPU_ID ↦ gensem set_abtcb_CPU_ID_spec
⊕ set_curid_init ↦ gensem set_curid_init_spec
⊕ set_state ↦ gensem set_state0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SchedInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
fifobbq_pool_init
Variable bfifobbq_pool_init: block.
Hypothesis hfifobbq_pool_init1 : Genv.find_symbol ge fifobbq_pool_init =
Some bfifobbq_pool_init.
Hypothesis hfifobbq_pool_init2 :
Genv.find_funct_ptr ge bfifobbq_pool_init =
Some (External (EF_external fifobbq_pool_init (signature_of_type
(Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
set_curid
Variable bset_curid_init: block.
Hypothesis hset_curid_init1 : Genv.find_symbol ge set_curid_init = Some bset_curid_init.
Hypothesis hset_curid_init2 :
Genv.find_funct_ptr ge bset_curid_init =
Some (External (EF_external set_curid_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
set_state
Variable bset_state: block.
Hypothesis hset_state1 : Genv.find_symbol ge set_state = Some bset_state.
Hypothesis hset_state2 :
Genv.find_funct_ptr ge bset_state =
Some (External (EF_external set_state (signature_of_type
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID (signature_of_type
Tnil tint cc_default)) Tnil tint cc_default).
tcb_set_CPU_ID
Variable btcb_set_CPU_ID: block.
Hypothesis htcb_set_CPU_ID1 : Genv.find_symbol ge tcb_set_CPU_ID = Some btcb_set_CPU_ID.
Hypothesis htcb_set_CPU_ID2 :
Genv.find_funct_ptr ge btcb_set_CPU_ID =
Some (External (EF_external tcb_set_CPU_ID
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Definition sched_init_mk_rdata (adt: RData) (index: Z) :=
adt {cid: Calculate_cidpool (Z.to_nat index) (cid adt)}.
Section sched_init_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Definition sched_init_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get tindex le = Some (Vint Int.zero) ∧
m = (minit, adt).
Definition sched_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, sched_init_mk_rdata adt (TOTAL_CPU - 1)).
Lemma sched_init_loop_correct_aux :
LoopProofSimpleWhile.t
sched_init_while_loop_cond
sched_init_while_loop_body ge (PTree.empty _)
(sched_init_loop_body_P)
(sched_init_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get tindex le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ TOTAL_CPU ∧
(Int.unsigned i = 0 ∧
m = (minit, adt) ∨
Int.unsigned i > 0 ∧
m = (minit, sched_init_mk_rdata adt (Int.unsigned i - 1))) ∧
w = TOTAL_CPU - Int.unsigned i
)
.
- apply Zwf_well_founded.
- intros.
unfold sched_init_loop_body_P in H.
destruct H as [tile msubst].
subst.
change (Int.zero) with (Int.repr 0) in tile.
esplit. esplit.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [icase nval].
subst.
unfold sched_init_while_loop_body.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
Caseeq ihigh.
+ Case "Int.unsigned i < TOTAL_CPU".
intro ihigh.
Caseeq icase.
× SCase "Int.unsigned i = 0".
intro tmpH; destruct tmpH as [ival mval].
injection mval; intros; subst.
rewrite ival in ×.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
repeat vcgen.
∃ 7.
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold sched_init_mk_rdata.
rewrite ival.
simpl.
reflexivity.
× SCase "Int.unsigned i > 0".
intro tmpH; destruct tmpH as [ival mval].
injection mval; intros; subst.
unfold sched_init_mk_rdata.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold set_curid_init_spec.
simpl.
rewrite ikern, ihost.
rewrite zle_lt_true.
repeat zdestruct.
reflexivity.
omega.
∃ (TOTAL_CPU - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
replace (Int.unsigned i + 1 - 1) with (Int.unsigned i - 1 + 1) by omega.
change (Int.unsigned i - 1 + 1) with (Z.succ(Int.unsigned i - 1)).
rewrite Z2Nat.inj_succ.
Opaque Z.to_nat Z.of_nat.
simpl.
rewrite <- Z2Nat.inj_succ.
unfold Z.succ.
rewrite Z2Nat.id.
replace (Int.unsigned i - 1 + 1) with (Int.unsigned i) by omega.
reflexivity.
omega.
omega.
omega.
+ Case "Int.unsigned i = num_proc".
intro ival.
rewrite ival.
esplit. esplit.
repeat vcgen.
unfold sched_init_loop_body_Q.
Caseeq icase; intro tmpH; destruct tmpH as [iv mval].
exfalso; rewrite iv in ival; omega.
rewrite ival in mval; assumption.
Qed.
End sched_init_loop_proof.
Lemma sched_init_loop_correct:
∀ m d d´ le,
PTree.get tindex le = Some (Vint Int.zero) →
ihost d = true →
ikern d = true →
d´ = sched_init_mk_rdata d (TOTAL_CPU - 1) →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) (Swhile sched_init_while_loop_cond
sched_init_while_loop_body) E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (sched_init_loop_correct_aux m d H0 H1).
unfold sched_init_loop_body_P.
unfold sched_init_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´´.
subst.
assumption.
auto.
Qed.
Require Import CalRealPT.
Require Import CalTicketLock.
Require Import CalRealIDPDE.
Require Import CalRealSMSPool.
Require Import DeviceStateDataType.
Opaque mkLApicData.
Lemma sched_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get tmbi_adr le = Some (Vint mbi_adr) →
sched_init_spec (Int.unsigned mbi_adr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sched_init_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold sched_init_body.
functional inversion H1.
subst.
destruct H2.
assert(tmp: 0 ≤ 0 < num_proc) by omega.
generalize (real_abtcb_valid (abtcb d) 0 tmp); intro.
unfold AbTCBCorrect in H.
destruct H as [s [c [b [tcbget brange]]]].
generalize (real_abtcb_notInQ (abtcb d) 0 s c b tmp tcbget); intro.
subst.
rename s into curst.
set (pre_loop :=
(((((((((((((((((d { ioapic / s :
ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)})
{ l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1))})
{ s : (ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {pg : true}) {LAT : real_LAT (LAT d)})
{nps : real_nps}) {AC : AC_init}) {init : true}) {PT : 0}) {ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)})
{lock : real_lock (lock d)}) {idpde : real_idpde (idpde d)})
{smspool : real_smspool (smspool d)}) {abtcb : real_abtcb (abtcb d)})
{abq : real_abq (abq d)}) {syncchpool : real_syncchpool (syncchpool d)}).
set (post_loop :=
((((((((((((((((((d { ioapic / s :
ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)})
{ l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1))})
{ s : (ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {pg : true}) {LAT : real_LAT (LAT d)})
{nps : real_nps}) {AC : AC_init}) {init : true}) {PT : 0}) {ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)})
{lock : real_lock (lock d)}) {idpde : real_idpde (idpde d)})
{smspool : real_smspool (smspool d)}) {abtcb : real_abtcb (abtcb d)})
{abq : real_abq (abq d)}) {syncchpool : real_syncchpool (syncchpool d)}) {cid : real_cidpool (cid d)}).
exploit (sched_init_loop_correct m pre_loop post_loop (PTree.set tindex (Vint (Int.repr 0))
(set_opttemp None Vundef le))).
- repeat vcgen.
- unfold pre_loop; simpl; auto.
- unfold pre_loop; simpl; auto.
- unfold post_loop; unfold pre_loop.
unfold sched_init_mk_rdata.
simpl.
unfold real_cidpool.
reflexivity.
Opaque real_cidpool.
- intros.
destruct H as (le´, H).
esplit.
unfold exec_stmt.
change E0 with (E0 ** E0).
econstructor.
{ d2 vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- vcgen.
unfold fifobbq_pool_init_spec; simpl.
rewrite H4, H5, H6, H7, H8, H9, H10, H11.
reflexivity. }
{ intros.
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen. }
change E0 with (E0 ** E0).
econstructor.
{ fold pre_loop.
eassumption. }
clear H.
clear pre_loop.
unfold post_loop.
clear post_loop.
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold set_state0_spec; simpl.
rewrite H7, H5, H6.
rewrite tcbget.
reflexivity. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold get_CPU_ID_spec.
simpl.
rewrite H7, H6.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr by omega.
reflexivity. }
repeat vcgen.
unfold set_abtcb_CPU_ID_spec; simpl.
simpl.
rewrite H7, H5, H6, zle_le_true by omega.
rewrite ZMap.gss.
unfold option_monad_ops.
set (partial :=
(((((((((((((((d { ioapic / s :
ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)})
{ l2 : l2 (lapic d)})
{ l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1))})
{ s : (ObjInterruptDriver.ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr
(s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}})
{vmxinfo : real_vmxinfo})
{pg : true}) {LAT : real_LAT (LAT d)}) {nps : real_nps})
{AC : AC_init}) {init : true}) {PT : 0})
{ptpool : real_pt (ptpool d)})
{multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde : real_idpde (idpde d)})
{smspool : real_smspool (smspool d)})).
unfold update_abtcb; simpl.
rewrite ZMap.set2.
unfold update_cid; simpl.
simpl.
reflexivity. }
Qed.
End SchedInitBody.
Theorem sched_init_code_correct:
spec_le (sched_init ↦ sched_init_spec_low) (〚sched_init ↦ f_sched_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sched_init_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sched_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_sched_init)))) H0.
Qed.
End SCHEDINIT.
Section THREADPOLLPENDING.
Let L: compatlayer (cdata RData) :=
set_state ↦ gensem set_state0_spec
⊕ tcb_set_CPU_ID ↦ gensem set_abtcb_CPU_ID_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ dequeue_atomic ↦ gensem dequeue_atomic_spec
⊕ enqueue ↦ gensem enqueue0_spec
⊕ sleeper_dec ↦ gensem sleeper_dec_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section THREADPOLLPENDINGBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_state
Variable bset_state: block.
Hypothesis hset_state1 : Genv.find_symbol ge set_state = Some bset_state.
Hypothesis hset_state2 : Genv.find_funct_ptr ge bset_state
= Some (External
(EF_external set_state
(signature_of_type
(Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
tcb_set_CPU_ID
Variable btcb_set_CPU_ID: block.
Hypothesis htcb_set_CPU_ID1 : Genv.find_symbol ge tcb_set_CPU_ID = Some btcb_set_CPU_ID.
Hypothesis htcb_set_CPU_ID2 :
Genv.find_funct_ptr ge btcb_set_CPU_ID =
Some (External (EF_external tcb_set_CPU_ID
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
enqueue
Variable benqueue: block.
Hypothesis henqueue1 : Genv.find_symbol ge enqueue = Some benqueue.
Hypothesis henqueue2 :
Genv.find_funct_ptr ge benqueue =
Some (External (EF_external enqueue (signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID (signature_of_type
Tnil tint cc_default)) Tnil tint cc_default).
dequeue_atomic
Variable bdequeue_atomic: block.
Hypothesis hdequeue_atomic1 : Genv.find_symbol ge dequeue_atomic = Some bdequeue_atomic.
Hypothesis hdequeue_atomic2 :
Genv.find_funct_ptr ge bdequeue_atomic =
Some (External (EF_external dequeue_atomic
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
sleeper_dec
Variable bsleeper_dec: block.
Hypothesis hsleeper_dec1 : Genv.find_symbol ge sleeper_dec = Some bsleeper_dec.
Hypothesis hsleeper_dec2 :
Genv.find_funct_ptr ge bsleeper_dec =
Some (External (EF_external sleeper_dec (signature_of_type
Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Lemma state_eq_lemma:
∀ r_tmp r cpuid z d,
((r_tmp
{abtcb : ZMap.set z (AbTCBValid READY cpuid (-1)) (abtcb r)})
{abtcb
: ZMap.set z (AbTCBValid READY (CPU_ID d) (-1)) (abtcb r)})
{abtcb
: ZMap.set z (AbTCBValid READY (CPU_ID d) (CPU_ID d)) (abtcb r)} =
r_tmp
{abtcb : ZMap.set z (AbTCBValid READY (CPU_ID d) (CPU_ID d)) (abtcb r)}.
Proof.
clearAll.
intros.
destruct r_tmp; destruct r; simpl.
reflexivity.
Qed.
Lemma thread_poll_pending_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
thread_poll_pending_spec d = Some d´→
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_thread_poll_pending_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold thread_poll_pending_spec in H0.
unfold dequeue_atomic_spec in H0.
unfold dequeue0_spec in H0.
subdestruct.
Opaque Z.add Z.mul.
- inv H0.
destruct H1 as (H1a, H1b).
unfold f_thread_poll_pending_body.
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
simpl.
rewrite H1a, H1b.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr.
reflexivity.
inv H2; subst.
omega.
+ unfold dequeue_atomic_spec.
unfold msg_q_id in Hdestruct0.
rewrite Int.unsigned_repr.
rewrite Hdestruct0.
unfold dequeue0_spec.
rewrite Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4.
rewrite zle_lt_true.
unfold msg_q_id in Hdestruct5.
rewrite Hdestruct5.
unfold msg_q_id in Hdestruct7.
rewrite Hdestruct7.
rewrite Int.unsigned_repr; eauto.
omega.
inv H2; omega.
inv H2; omega.
+ rewrite Int.unsigned_repr; inv H2; omega.
+ rewrite Int.unsigned_repr; inv H2; omega.
+ repeat vcgen.
+ omega.
+ omega.
+ repeat vcgen.
- inv H0.
destruct H1 as (H1a, H1b).
unfold f_thread_poll_pending_body.
esplit; repeat vcgen.
+ unfold get_CPU_ID_spec.
simpl.
rewrite H1a, H1b.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr.
reflexivity.
inv H2; subst.
omega.
+ unfold dequeue_atomic_spec.
unfold msg_q_id in Hdestruct0.
rewrite Int.unsigned_repr.
rewrite Hdestruct0.
unfold dequeue0_spec.
rewrite Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4.
rewrite zle_lt_true.
unfold msg_q_id in Hdestruct5.
rewrite Hdestruct5.
unfold msg_q_id in Hdestruct7.
rewrite Hdestruct7.
unfold msg_q_id in Hdestruct8.
rewrite Hdestruct8.
rewrite Int.unsigned_repr; eauto.
omega.
inv H2; omega.
inv H2; omega.
+ rewrite Int.unsigned_repr; inv H2; omega.
+ rewrite Int.unsigned_repr; inv H2; omega.
+ repeat vcgen.
+ omega.
+ omega.
+ unfold release_lock_ABTCB_spec in Hdestruct8.
subdestruct.
inv Hdestruct8; simpl in ×.
repeat vcgen.
× unfold set_state0_spec; simpl.
rewrite Hdestruct1, Hdestruct13, Hdestruct14, Hdestruct4.
rewrite zle_lt_true; try omega.
rewrite ZMap.gss.
rewrite ZMap.set2.
reflexivity.
× unfold set_abtcb_CPU_ID_spec; simpl.
rewrite Hdestruct1, Hdestruct13, Hdestruct14, Hdestruct4.
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite ZMap.gss.
reflexivity.
inv H2; omega.
omega.
× inv H2; omega.
× inv H2; omega.
× unfold enqueue0_spec; simpl.
rewrite Hdestruct1, Hdestruct13, Hdestruct14, Hdestruct4.
unfold Queue_arg.
rewrite zle_lt_true.
rewrite zle_lt_true.
unfold msg_q_id.
unfold rdy_q_id in Hdestruct12.
replace (0 + CPU_ID d) with (CPU_ID d) in Hdestruct12.
unfold msg_q_id in Hdestruct12.
rewrite Hdestruct12.
rewrite Hdestruct11.
rewrite ZMap.gss.
rewrite zeq_true.
reflexivity.
omega.
omega.
inv H2; omega.
× inv H2; omega.
× inv H2; omega.
× unfold sleeper_dec_spec.
simpl in ×.
rewrite Hdestruct1, Hdestruct13.
inv H2.
assert (cpu_id_same: CPU_ID d = CPU_ID r).
{ unfold acquire_lock_ABTCB_spec in Hdestruct0.
subdestruct; simpl.
+ inv Hdestruct0.
simpl; auto.
+ inv Hdestruct0.
simpl; auto. }
rewrite <- cpu_id_same in ×.
rewrite zle_lt_true; try eauto.
rewrite ZMap.set2.
unfold msg_q_id.
unfold rdy_q_id.
replace (0 + CPU_ID d) with (CPU_ID d); try omega.
rewrite ZMap.set2.
unfold ret.
simpl.
f_equal.
f_equal.
f_equal.
rewrite ZMap.set2.
eapply state_eq_lemma.
- inv H0; subst.
assert (high_level_invariant r).
{ eapply acquire_lock_ABTCB_high_level_inv; eauto. }
inv H.
unfold AbQCorrect_range in valid_TDQ.
unfold AbQCorrect in valid_TDQ.
unfold msg_q_id in a.
generalize a; intro range.
eapply valid_TDQ in range; eauto.
destruct range as (l & range1 & range2).
unfold msg_q_id in Hdestruct5.
rewrite Hdestruct5 in range1.
destruct l.
+ inv range1.
+ inv range1.
assert (0 ≤ z0 < num_proc).
{ eapply range2; simpl; auto. }
omega.
Qed.
End THREADPOLLPENDINGBODY.
Theorem thread_poll_pending_code_correct:
spec_le (thread_poll_pending ↦ thread_poll_pending_spec_low)
(〚thread_poll_pending ↦ f_thread_poll_pending 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (thread_poll_pending_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
b4 Hb4fs Hb4fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp b5 Hb5fs Hb5fp m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´
(fn_params f_thread_poll_pending)
nil
(create_undef_temps
(fn_temps f_thread_poll_pending)))) H0.
Qed.
End THREADPOLLPENDING.
Section THREADSPAWN.
Let L: compatlayer (cdata RData) := kctxt_new ↦ dnew_compatsem kctxt_new_spec
⊕ set_state ↦ gensem set_state0_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ tcb_set_CPU_ID ↦ gensem set_abtcb_CPU_ID_spec
⊕ enqueue ↦ gensem enqueue0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section ThreadSpawnBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
parameters
kctxt_new
Variable bkctxt_new: block.
Hypothesis hkctxt_new1 : Genv.find_symbol ge kctxt_new = Some bkctxt_new.
Hypothesis hkctxt_new2 :
Genv.find_funct_ptr ge bkctxt_new =
Some (External (EF_external kctxt_new (signature_of_type
(Tcons (tptr tvoid) (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons (tptr tvoid) (Tcons tint (Tcons tint Tnil))) tint cc_default).
set_state
Variable bset_state: block.
Hypothesis hset_state1 : Genv.find_symbol ge set_state = Some bset_state.
Hypothesis hset_state2 :
Genv.find_funct_ptr ge bset_state =
Some (External (EF_external set_state (signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
enqueue
Variable benqueue: block.
Hypothesis henqueue1 : Genv.find_symbol ge enqueue = Some benqueue.
Hypothesis henqueue2 :
Genv.find_funct_ptr ge benqueue =
Some (External (EF_external enqueue (signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID (signature_of_type
Tnil tint cc_default)) Tnil tint cc_default).
tcb_set_CPU_ID
Variable btcb_set_CPU_ID: block.
Hypothesis htcb_set_CPU_ID1 : Genv.find_symbol ge tcb_set_CPU_ID = Some btcb_set_CPU_ID.
Hypothesis htcb_set_CPU_ID2 :
Genv.find_funct_ptr ge btcb_set_CPU_ID =
Some (External (EF_external tcb_set_CPU_ID (signature_of_type
(Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma thread_spawn_body_correct:
∀ m d d´ env le b bstack_loc i ofs´,
env = PTree.empty _ → le ! _entry = Some (Vptr b ofs´) →
le ! _id = Some (Vint id) → le ! _quota = Some (Vint quota) →
thread_spawn_spec d bstack_loc b ofs´ (Int.unsigned id) (Int.unsigned quota)
= Some (d´, i) →
Genv.find_symbol ge STACK_LOC = Some bstack_loc →
(∃ fun_id : ident, Genv.find_symbol ge fun_id = Some b) →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) thread_spawn_body E0 le´ (m, d´)
(Out_return (Some (Vint (Int.repr i), tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold thread_spawn_body.
unfold thread_spawn_spec in H3.
subdestruct.
inv H3.
destruct H5.
destruct H6.
unfold AbTCBCorrect_range in valid_TCB.
unfold AbTCBCorrect in valid_TCB.
assert(tmprange: 0 ≤
Int.unsigned id × max_children + 1 +
Z.of_nat (length (cchildren (ZMap.get (Int.unsigned id) (AC d)))) < num_proc)
by omega.
generalize (valid_TCB Hdestruct (Int.unsigned id × max_children + 1 +
Z.of_nat (length (cchildren (ZMap.get (Int.unsigned id)
(AC d)))))
tmprange); intro tmpH.
destruct tmpH as [s´ tmpH].
destruct tmpH as [c´ tmpH].
destruct tmpH as [b´ tmpH].
destruct tmpH as [iget b´range].
esplit.
repeat vcgen.
unfold kctxt_new_spec; simpl.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct5,
Hdestruct6, Hdestruct7.
repeat (rewrite Int.unsigned_repr; try omega).
reflexivity.
erewrite <- stencil_matches_symbols; eauto.
erewrite <- stencil_matches_symbols; eauto.
unfold set_state0_spec; simpl.
rewrite Int.unsigned_repr; try omega.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2, iget.
rewrite zle_lt_true.
repeat (rewrite Int.unsigned_repr; try omega).
reflexivity.
omega.
unfold get_CPU_ID_spec; simpl.
rewrite Hdestruct0, Hdestruct1.
rewrite <- Int.unsigned_repr with (CPU_ID d).
reflexivity.
omega.
unfold enqueue0_spec; simpl.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
repeat (rewrite Int.unsigned_repr; try omega).
repeat rewrite ZMap.gss.
repeat rewrite ZMap.set2.
unfold Queue_arg.
rewrite zle_lt_true.
rewrite zle_lt_true.
unfold rdy_q_id in *; simpl in ×.
rewrite Hdestruct11.
rewrite Hdestruct8 in iget; inv iget.
rewrite zeq_true; auto.
omega.
omega.
unfold set_abtcb_CPU_ID_spec; simpl.
rewrite Hdestruct, Hdestruct0, Hdestruct1, Hdestruct2.
repeat (rewrite Int.unsigned_repr; try omega).
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite ZMap.gss.
rewrite ZMap.set2.
reflexivity.
omega.
omega.
Qed.
End ThreadSpawnBody.
Theorem thread_spawn_code_correct:
spec_le (thread_spawn ↦ thread_spawn_spec_low) (〚thread_spawn ↦ f_thread_spawn 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct H1.
fbigsteptest (thread_spawn_body_correct s (Genv.globalenv p) makeglobalenv id q
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b5 Hb5fs Hb5fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_thread_spawn)
(Vptr b´ ofs´ :: Vint id :: Vint q :: nil)
(create_undef_temps
(fn_temps f_thread_spawn)))) H2.
esplit; erewrite stencil_matches_symbols; eassumption.
intro stmt.
destruct stmt.
repeat fbigstep_post.
Qed.
End THREADSPAWN.
Section THREADWAKEUP.
Let L: compatlayer (cdata RData) :=
set_state ↦ gensem set_state0_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ sleeper_dec ↦ gensem sleeper_dec_spec
⊕ tcb_get_CPU_ID ↦ gensem get_abtcb_CPU_ID_spec
⊕ enqueue ↦ gensem enqueue0_spec
⊕ enqueue_atomic ↦ gensem enqueue_atomic_spec
⊕ dequeue_atomic ↦ gensem dequeue_atomic_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section ThreadWakeupBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_state
Variable bset_state: block.
Hypothesis hset_state1 : Genv.find_symbol ge set_state = Some bset_state.
Hypothesis hset_state2 :
Genv.find_funct_ptr ge bset_state =
Some (External (EF_external set_state
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
enqueue
Variable benqueue: block.
Hypothesis henqueue1 : Genv.find_symbol ge enqueue = Some benqueue.
Hypothesis henqueue2 :
Genv.find_funct_ptr ge benqueue =
Some (External (EF_external enqueue
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
enqueue_atomic
Variable benqueue_atomic: block.
Hypothesis henqueue_atomic1 : Genv.find_symbol ge enqueue_atomic = Some benqueue_atomic.
Hypothesis henqueue_atomic2 :
Genv.find_funct_ptr ge benqueue_atomic =
Some (External (EF_external enqueue_atomic
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
dequeue_atomic
Variable bdequeue_atomic: block.
Hypothesis hdequeue_atomic1 : Genv.find_symbol ge dequeue_atomic = Some bdequeue_atomic.
Hypothesis hdequeue_atomic2 :
Genv.find_funct_ptr ge bdequeue_atomic =
Some (External (EF_external dequeue_atomic
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
get_CPU_ID
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID (signature_of_type
Tnil tint cc_default)) Tnil tint cc_default).
tcb_get_CPU_ID
Variable btcb_get_CPU_ID: block.
Hypothesis htcb_get_CPU_ID1 : Genv.find_symbol ge tcb_get_CPU_ID = Some btcb_get_CPU_ID.
Hypothesis htcb_get_CPU_ID2 :
Genv.find_funct_ptr ge btcb_get_CPU_ID =
Some (External (EF_external tcb_get_CPU_ID (signature_of_type
(Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
sleeper_dec
Variable bsleeper_dec: block.
Hypothesis hsleeper_dec1 : Genv.find_symbol ge sleeper_dec = Some bsleeper_dec.
Hypothesis hsleeper_dec2 :
Genv.find_funct_ptr ge bsleeper_dec =
Some (External (EF_external sleeper_dec (signature_of_type
Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Lemma dequeue_atomic_preserve: ∀ x y d d´,
ikern d = true →
ihost d = true →
pg d = true →
ipt d = true →
dequeue_atomic_spec x d = Some (d´, y) →
ikern d´ = true ∧
ihost d´ = true ∧
pg d´ = true ∧
ipt d´ = true ∧
CPU_ID d = CPU_ID d´.
Proof.
intros.
functional inversion H3; subst.
functional inversion H8; subst.
simpl in ×.
split; auto.
split; auto.
functional inversion H7; unfold l´, cpu in *; subst;
unfold acquire_lock_ABTCB_spec in H6;
subdestruct; inv H6; eauto.
Qed.
Lemma thread_wakeup_body_correct:
∀ m d d´ env le cv_index val,
env = PTree.empty _ →
PTree.get _cv_index le = Some (Vint cv_index) →
True →
thread_wakeup_spec (Int.unsigned cv_index) d = Some (d´, Int.unsigned val) →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) thread_wakeup_body E0 le´ (m, d´)
(Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold thread_wakeup_body.
generalize H3; intro hinv.
inv H3.
functional inversion H2; subst.
{
rewrite <- Int.unsigned_repr with la in H9 by omega.
unfold rdyq, rdy_q_id, n, slp_q_id in ×.
generalize H9; intro tmp.
eapply dequeue_atomic_preserve in tmp; eauto.
destruct tmp as (ikern0 & ihost0 & pg0 & ipt0 & CPU_ID_eq).
esplit.
Opaque Z.mul Z.add.
repeat vcgen.
discharge_cmp.
discharge_cmp.
discharge_cmp.
rewrite <- Int.repr_unsigned with val.
rewrite <- H3.
repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite ikern0, ihost0, <- CPU_ID_eq.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr by omega.
reflexivity.
unfold get_abtcb_CPU_ID_spec; simpl.
rewrite ikern0, ihost0, pg0, ipt0, H11, H10.
rewrite <- _x2.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr by omega.
reflexivity.
discharge_cmp.
repeat vcgen.
unfold enqueue0_spec; simpl.
unfold Queue_arg.
rewrite ikern0, ihost0, pg0, ipt0, H10.
rewrite zle_lt_true by omega.
rewrite Z.add_0_l in H14.
rewrite _x2 in ×.
rewrite H14.
rewrite ZMap.gss.
rewrite H12.
assert(x1val: _x1 = -1).
{
functional inversion H9; simpl in *; subst.
functional inversion H18; functional inversion H17; unfold l´0, cpu in *;
subst; simpl in *; eauto.
rewrite Int.unsigned_repr in H26 by omega. omega.
rewrite Int.unsigned_repr in H11 by omega.
rewrite ZMap.gss in H11.
inv H11; auto.
}
rewrite x1val.
zdestruct.
rewrite Z.add_0_l.
rewrite CPU_ID_eq.
rewrite ZMap.set2.
reflexivity.
}
{
rewrite <- Int.unsigned_repr with la in H9 by omega.
unfold rdy_q_id, n, slp_q_id in ×.
generalize H9; intro tmp.
eapply dequeue_atomic_preserve in tmp; eauto.
destruct tmp as (ikern0 & ihost0 & pg0 & ipt0 & CPU_ID_eq).
esplit.
Opaque Z.mul Z.add.
repeat vcgen.
discharge_cmp.
discharge_cmp.
discharge_cmp.
rewrite <- Int.repr_unsigned with val.
rewrite <- H3.
repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite ikern0, ihost0, <- CPU_ID_eq.
instantiate (1:= (Int.repr (CPU_ID d))).
rewrite Int.unsigned_repr by omega.
reflexivity.
unfold get_abtcb_CPU_ID_spec; simpl.
rewrite ikern0, ihost0, pg0, ipt0, H11, H10.
instantiate (1:= (Int.repr cpu)).
rewrite Int.unsigned_repr by omega.
reflexivity.
unfold me in ×.
discharge_cmp.
repeat vcgen.
unfold msgq in ×.
unfold msg_q_id in ×.
rewrite Z.add_comm.
apply H15.
}
{
rewrite <- Int.unsigned_repr with la in H9 by omega.
unfold rdy_q_id, n, slp_q_id in ×.
generalize H9; intro tmp.
eapply dequeue_atomic_preserve in tmp; eauto.
destruct tmp as (ikern0 & ihost0 & pg0 & ipt0 & CPU_ID_eq).
esplit.
Opaque Z.mul Z.add.
repeat vcgen.
discharge_cmp.
discharge_cmp.
discharge_cmp.
rewrite <- Int.repr_unsigned with val.
rewrite <- H3.
repeat vcgen.
}
Qed.
End ThreadWakeupBody.
Theorem thread_wakeup_code_correct:
spec_le (thread_wakeup ↦ thread_wakeup_spec_low) (〚thread_wakeup ↦ f_thread_wakeup 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (thread_wakeup_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b4 Hb4fs Hb4fp b5 Hb5fs Hb5fp
b6 Hb6fs Hb6fp b1 Hb1fs Hb1fp b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´
(fn_params f_thread_wakeup)
(Vint n::nil)
(create_undef_temps
(fn_temps f_thread_wakeup)))) H0.
Qed.
End THREADWAKEUP.
End WithPrimitives.
End PCURIDCODE.