Library mcertikos.proc.ThreadGenAsmData
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.
Require Import PThreadSched.
Require Import ThreadGenAsmSource.
Require Import AbstractDataType.
Section ASM_DATA.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := pthreadsched_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.
Section ThreadKill.
Lemma threadkill_generate:
∀ r´ (m0: mem) labd labd´ r´0,
thread_kill_spec labd ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
→ low_level_invariant (Mem.nextblock m0) labd
→ high_level_invariant labd
→ ∃ labd0,
get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))
∧ set_state1_spec (ZMap.get (CPU_ID labd) (cid labd)) (Int.unsigned (Int.repr 3)) labd = Some labd0
∧ thread_sched_spec labd0 ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
∧ (∀ v r, ZtoPreg v = Some r → Val.has_type (r´0 r) Tint)
∧ (∀ v r, ZtoPreg v = Some r → val_inject (Mem.flat_inj (Mem.nextblock m0)) (r´0 r) (r´0 r))
∧ ikern labd = true
∧ ihost labd = true
∧ ikern labd0 = true
∧ ihost labd0 = true
∧ 0≤ (ZMap.get (CPU_ID labd) (cid labd)) < num_proc.
Proof.
intros. inv H0.
assert (HOS´: 0 ≤ num_proc ≤ Int.max_unsigned)
by (rewrite int_max; omega).
rename H1 into Hhigh.
assert (HIK: ikern labd = true∧
ihost labd = true ∧
ipt labd = true∧
pg labd = true).
{
specialize (valid_iptt labd Hhigh). intros HR.
functional inversion H. rewrite HR; auto.
}
unfold thread_kill_spec in ×.
destruct HIK as [HIK1 [HIH1 [HIPT1 HPE1]]].
generalize Hhigh.
intro Hhigh´; inv Hhigh´.
assert (HEX1: get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))).
{
unfold get_curid_spec in ×.
rewrite HIK1, HIH1.
trivial.
}
subdestruct.
inv H.
simpl in ×.
unfold set_state1_spec.
subrewrite´.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
simpl.
assert (DEAD ≠ RUN).
{ intro contra.
inv contra. }
destruct (ThreadState_dec DEAD RUN); try contradiction.
esplit.
split.
reflexivity.
split.
reflexivity.
assert(HNL: ZMap.get (CPU_ID labd) (cid labd) ≠ z).
{
unfold InQ in valid_inQ.
assert(jrange: 0 ≤ (rdy_q_id (CPU_ID labd)) < num_chan).
{
unfold rdy_q_id.
omega.
}
assert(zin: In z (z :: l0)).
{
constructor; auto.
}
specialize (valid_inQ HPE1 z (rdy_q_id (CPU_ID labd)) _ a jrange Hdestruct3 zin).
intro.
rewrite <- H0 in valid_inQ.
destruct valid_inQ as [s´´ [c´´ zget´´]].
rewrite Hdestruct9 in zget´´.
inv zget´´.
unfold rdy_q_id in H4.
omega.
}
unfold thread_sched_spec.
simpl.
unfold rdy_q_id in *; rewrite Z.add_0_l in ×.
subrewrite´.
rewrite ZMap.gss.
rewrite ZMap.gso; auto.
subrewrite´.
split.
reflexivity.
generalize kctxt_INJECT.
intros kctxt_INJECT_cond.
unfold kctxt_inject_neutral in kctxt_INJECT_cond.
try (repeat split; eauto); try omega; intros; eauto.
clear Hdestruct6.
eapply kctxt_INJECT_cond in a.
destruct a; eassumption.
exact H0.
clear Hdestruct6.
eapply kctxt_INJECT_cond in a.
destruct a; eassumption.
exact H0.
Qed.
End ThreadKill.
Section ThreadSleep.
Lemma Hneq:
∀ n v v´,
v´ ≤ n < v →
v ≠ n.
Proof.
intros. omega.
Qed.
Lemma threadsleep_generate:
∀ r´ (m0: mem) labd labd´ r´0 n,
thread_sleep_spec labd ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) (Int.unsigned n) = Some (labd´, r´0)
→ low_level_invariant (Mem.nextblock m0) labd
→ high_level_invariant labd
→ ∃ labd0 labd1 labd2 labd3,
get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))
∧ enqueue_atomic_spec (slp_q_id (Int.unsigned n) 0)
(ZMap.get (CPU_ID labd) (cid labd)) labd = Some labd0
∧ release_lock_SC_spec (slp_q_id (Int.unsigned n) 0) labd0 = Some labd1
∧ set_state1_spec (ZMap.get (CPU_ID labd) (cid labd)) (Int.unsigned (Int.repr 2)) labd1 = Some labd2
∧ sleeper_inc_spec labd2 = Some labd3
∧ thread_sched_spec labd3 ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
∧ (∀ v r, ZtoPreg v = Some r → Val.has_type (r´0 r) Tint)
∧ (∀ v r, ZtoPreg v = Some r → val_inject (Mem.flat_inj (Mem.nextblock m0)) (r´0 r) (r´0 r))
∧ ikern labd = true
∧ ihost labd = true
∧ ikern labd0 = true
∧ ihost labd0 = true
∧ ikern labd1 = true
∧ ihost labd1 = true
∧ ikern labd2 = true
∧ ihost labd2 = true
∧ ikern labd3 = true
∧ ihost labd3 = true
∧ 0≤ (ZMap.get (CPU_ID labd) (cid labd)) < num_proc.
Proof.
intros. inv H0.
rename H1 into Hhigh.
assert (HIK: ikern labd = true∧
ihost labd = true ∧
ipt labd = true∧
pg labd = true).
{
specialize (valid_iptt _ Hhigh). intros HR.
functional inversion H. rewrite HR; auto.
}
unfold thread_sleep_spec in ×.
destruct HIK as [HIK1 [HIH1 [HIPT1 HPE1]]].
specialize (CPU_ID_range labd Hhigh). intro HCPU_range.
rewrite HIK1, HIH1, HIPT1, HPE1 in ×.
specialize (valid_curid labd Hhigh). intros HCID_range.
assert (HEX1: get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))).
{
unfold get_curid_spec in ×.
rewrite HIK1, HIH1.
trivial.
}
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (HIK: ikern r = true∧
ihost r = true ∧
ipt r = true ∧
pg r = true ∧
CPU_ID r = CPU_ID labd ∧ cid r = cid labd ∧ kctxt r = kctxt labd).
{
functional inversion Hdestruct1; simpl in *; eauto.
functional inversion H0; functional inversion H2; unfold acquire_lock_ABTCB_spec in H1; subdestruct; inversion H1; simpl in *;
repeat (split; auto).
}
destruct HIK as (HIK2 & HIH2 & HIPT2 & HPE2 & HCPU & Hcid & Hkctxt).
unfold release_lock_SC_spec in ×.
unfold set_state1_spec.
unfold sleeper_inc_spec.
rewrite HIK2, HIH2 in ×.
exploit enqueue_atomic_high_level_inv; eauto.
intros Hhigh´.
specialize (valid_TCB r Hhigh´). intros HBrange.
specialize (valid_TDQ r Hhigh´). intros HTrange.
specialize (HBrange HPE2).
specialize (HTrange HPE2).
subdestruct. inv H.
unfold AbTCBCorrect_range, AbQCorrect_range, AbQCorrect, AbTCBCorrect in ×.
assert (HOS: 0 ≤ rdy_q_id (CPU_ID labd) < num_chan).
{
unfold rdy_q_id. omega.
}
pose proof a2 as Hrange.
assert (He: ∃ st, ZMap.get (ZMap.get (CPU_ID labd) (cid labd)) (abtcb r)
= AbTCBValid st (CPU_ID labd) (slp_q_id (Int.unsigned n) 0)).
{
functional inversion Hdestruct1; simpl in ×.
functional inversion H; functional inversion H1; simpl.
rewrite ZMap.gss.
unfold acquire_lock_ABTCB_spec in H0; subdestruct; unfold l´, cpu in *;
inv H0; simpl in *;
esplit;
f_equal;
rewrite ZMap.gss in Hdestruct11; inv Hdestruct11; eauto.
}
destruct He as (st & Heq).
assert (He: ∃ st´ c´ b´, ZMap.get z (abtcb r) = AbTCBValid st´ c´ b´).
{
eapply HBrange in Hrange.
destruct Hrange as (st´ & c´ & b´ & Heq´ & _).
refine_split´; eauto.
}
destruct He as (st´ & c´ & b´ & Heq´).
esplit; esplit; esplit; esplit. split; trivial. split; trivial.
subrewrite´.
rewrite zle_lt_true; trivial.
change (Int.unsigned (Int.repr 2)) with 2. simpl.
destruct (ThreadState_dec SLEEP RUN); contra_inv.
split; trivial; simpl.
subrewrite´.
rewrite zlt_lt_true.
split; trivial; simpl.
subrewrite´.
split; trivial.
unfold thread_sched_spec; simpl.
subrewrite´.
assert(HNL: ZMap.get (CPU_ID labd) (cid labd) ≠ z).
{
exploit enqueue_atomic_high_level_inv; eauto. intro hinvr.
inv hinvr.
unfold InQ in valid_inQ.
assert(jrange: 0 ≤ (rdy_q_id (CPU_ID labd)) < num_chan).
{
unfold rdy_q_id.
omega.
}
assert(zin: In z (z :: l1)).
{
constructor; auto.
}
specialize (valid_inQ Hdestruct2 z (rdy_q_id (CPU_ID labd)) _ Hrange jrange Hdestruct8 zin).
intro.
rewrite <- H in valid_inQ.
destruct valid_inQ as [s´´ [c´´ zget´´]].
rewrite Heq in zget´´.
inv zget´´.
unfold slp_q_id, rdy_q_id in H3.
generalize HCPU_range, H3.
repeat match goal with [H: _ |- _] ⇒ clear H end.
intros.
generalize (Int.unsigned_range n); intro.
unfold Int.modulus, two_power_nat, shift_nat in H.
simpl in H.
omega.
}
rewrite ZMap.gso; auto.
rewrite ZMap.gss.
rewrite Heq´.
rewrite Hdestruct15 in Heq´.
inv Heq´.
rewrite zeq_true; auto.
rewrite zeq_false; auto.
repeat (split; trivial); try eapply kctxt_INJECT; trivial.
simpl.
rewrite HCPU.
assumption.
Qed.
End ThreadSleep.
Section ThreadYield.
Lemma threadyield_generate:
∀ r´ (m0: mem) labd labd´ r´0,
thread_yield_spec labd ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
→ low_level_invariant (Mem.nextblock m0) labd
→ high_level_invariant labd
→ ∃ labd0 labd1 labd2,
get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))
∧ thread_poll_pending_spec labd = Some labd0
∧ set_state1_spec (ZMap.get (CPU_ID labd) (cid labd)) (Int.unsigned (Int.repr 0)) labd0 = Some labd1
∧ enqueue0_spec (CPU_ID labd) (ZMap.get (CPU_ID labd) (cid labd)) labd1 = Some labd2
∧ thread_sched_spec labd2 ((Pregmap.init Vundef) # ESP <- (r´ ESP) # EDI <- (r´ EDI)
# ESI <- (r´ ESI) # EBX <- (r´ EBX) # EBP <-
(r´ EBP) # RA <- (r´ RA)) = Some (labd´, r´0)
∧ (∀ v r, ZtoPreg v = Some r → Val.has_type (r´0 r) Tint)
∧ (∀ v r, ZtoPreg v = Some r → val_inject (Mem.flat_inj (Mem.nextblock m0)) (r´0 r) (r´0 r))
∧ ikern labd = true
∧ ihost labd = true
∧ ikern labd0 = true
∧ ihost labd0 = true
∧ ikern labd1 = true
∧ ihost labd1 = true
∧ ikern labd2 = true
∧ ihost labd2 = true
∧ 0≤ (ZMap.get (CPU_ID labd) (cid labd)) < num_proc.
Proof.
intros. inv H0.
assert (HOS´: 0 ≤ 64 ≤ Int.max_unsigned)
by (rewrite int_max; omega).
rename H1 into Hhigh.
assert (HIK: ikern labd = true∧
ihost labd = true ∧
ipt labd = true∧
pg labd = true).
{
specialize (valid_iptt labd Hhigh). intros HR.
functional inversion H. rewrite HR; auto.
}
unfold thread_yield_spec in ×.
destruct HIK as [HIK1 [HIH1 [HIPT1 HPE1]]].
generalize Hhigh.
intro Hhigh´; inv Hhigh´.
assert (HEX1: get_curid_spec labd = Some (ZMap.get (CPU_ID labd) (cid labd))).
{
unfold get_curid_spec in ×.
rewrite HIK1, HIH1.
trivial.
}
subdestruct.
inv H.
generalize valid_TCB; intros tmp.
unfold AbTCBCorrect_range in tmp.
unfold AbTCBCorrect in tmp.
assert (HIK: ikern r = true∧
ihost r = true ∧
ipt r = true ∧
pg r = true ∧
CPU_ID r = CPU_ID labd ∧ cid r = cid labd ∧ kctxt r = kctxt labd).
{
functional inversion Hdestruct3; simpl in *; eauto.
functional inversion H0; simpl in *; eauto.
functional inversion H9; functional inversion H8; unfold acquire_lock_ABTCB_spec in H7; subdestruct; simpl in *; unfold n, l´0, cpu0 in *; inv H7; try rewrite <- H28 in *; simpl in *;
repeat (split; auto).
functional inversion H0; simpl in *; eauto.
functional inversion H6; functional inversion H5; unfold acquire_lock_ABTCB_spec in H4; subdestruct; simpl in *; unfold cpu0, l´, cpu0 in *; inv H4; try rewrite <- H25 in *; simpl in *;
repeat (split; auto).
}
destruct HIK as (HIK2 & HIH2 & HIPT2 & HPE2 & HCPU & Hcid & Hkctxt).
generalize valid_curid; intros valid_TCB´.
eapply tmp in valid_TCB´; eauto; clear tmp.
destruct valid_TCB´ as (thread_st, (c_v, (b_v, (valid_TCB´a, valid_TCB´b)))).
assert ((ZtoThreadState 0) = Some READY).
{ simpl; auto. }
∃ r.
destruct thread_poll_pending_inv.
unfold semof in semprops_high_level_invariant; simpl in semprops_high_level_invariant.
eapply semprops_high_level_invariant in Hhigh; [|econstructor; eauto].
inv Hhigh.
generalize valid_TCB0; intros tmp.
unfold AbTCBCorrect_range in tmp.
unfold AbTCBCorrect in tmp.
specialize (tmp HPE2 (ZMap.get (CPU_ID labd) (cid labd)) valid_curid).
destruct tmp as [s´ [c´ [b´ (zget & tcbvalid & brange)]]].
∃ (r {abtcb
: ZMap.set (ZMap.get (CPU_ID labd) (cid labd))
(AbTCBValid READY c´ b´) (abtcb r)}).
esplit; try eauto.
esplit; try eauto.
esplit; try eauto.
simpl in ×.
unfold set_state1_spec.
subrewrite´.
simpl.
subrewrite´.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
simpl.
assert (READY ≠ RUN).
{ intro contra.
inv contra. }
destruct (ThreadState_dec READY RUN); try contradiction.
split.
reflexivity.
assert(HNL: ZMap.get (CPU_ID labd) (cid labd) ≠ z).
{
unfold InQ in valid_inQ0.
assert(jrange: 0 ≤ (rdy_q_id (CPU_ID labd)) < num_chan).
{
unfold rdy_q_id.
omega.
}
assert(zin: In z (z :: l0)).
{
constructor; auto.
}
specialize (valid_inQ0 HPE2 z (rdy_q_id (CPU_ID labd)) _ a jrange Hdestruct5 zin).
intro.
rewrite <- H1 in valid_inQ0.
destruct valid_inQ0 as [s´´ [c´´ zget´´]].
rewrite Hdestruct8 in zget´´.
inv zget´´.
unfold rdy_q_id in H5.
omega.
}
split.
unfold enqueue0_spec; simpl.
subrewrite´.
unfold Queue_arg. simpl.
rewrite zle_lt_true; [|omega].
rewrite zle_lt_true; [|omega].
rewrite ZMap.gss.
rewrite ZMap.set2.
unfold rdy_q_id in Hdestruct5.
rewrite Z.add_0_l in Hdestruct5.
rewrite Hdestruct5.
rewrite Hdestruct8 in zget; inv zget.
rewrite zeq_true; auto.
rewrite Hdestruct8 in zget; inv zget.
unfold thread_sched_spec.
simpl.
unfold rdy_q_id; rewrite Z.add_0_l.
subrewrite´.
rewrite ZMap.gss.
rewrite ZMap.gso; auto.
rewrite ZMap.gss.
rewrite Hdestruct13.
rewrite zeq_true; auto.
rewrite zeq_false; auto.
split.
rewrite Z.add_0_l.
rewrite ZMap.set2.
reflexivity.
generalize kctxt_INJECT.
intros kctxt_INJECT_cond.
unfold kctxt_inject_neutral in kctxt_INJECT_cond.
try (repeat split; eauto); try omega; intros; eauto.
clear Hdestruct7.
eapply kctxt_INJECT_cond in a.
destruct a; eassumption.
exact H1.
clear Hdestruct7.
eapply kctxt_INJECT_cond in a.
destruct a; eassumption.
exact H1.
Qed.
End ThreadYield.
Lemma Hget_curid:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_get_curid, Genv.find_symbol ge get_curid = Some b_get_curid
∧ Genv.find_funct_ptr ge b_get_curid =
Some (External (EF_external get_curid get_curid_sig)))
∧ get_layer_primitive get_curid pthreadsched = OK (Some (gensem get_curid_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive get_curid pthreadsched = OK (Some (gensem get_curid_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hset_state:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_set_state, Genv.find_symbol ge set_state = Some b_set_state
∧ Genv.find_funct_ptr ge b_set_state =
Some (External (EF_external set_state set_state_sig)))
∧ get_layer_primitive set_state pthreadsched = OK (Some (gensem set_state1_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive set_state pthreadsched = OK (Some (gensem set_state1_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Henqueue_atomic:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_enqueue_atomic, Genv.find_symbol ge enqueue_atomic = Some b_enqueue_atomic
∧ Genv.find_funct_ptr ge b_enqueue_atomic =
Some (External (EF_external enqueue_atomic enqueue_atomic_sig)))
∧ get_layer_primitive enqueue_atomic pthreadsched = OK (Some (gensem enqueue_atomic_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive enqueue_atomic pthreadsched = OK (Some (gensem enqueue_atomic_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Henqueue:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_enqueue, Genv.find_symbol ge enqueue = Some b_enqueue
∧ Genv.find_funct_ptr ge b_enqueue =
Some (External (EF_external enqueue enqueue_sig)))
∧ get_layer_primitive enqueue pthreadsched = OK (Some (gensem enqueue0_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive enqueue pthreadsched = OK (Some (gensem enqueue0_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hthread_poll_pending:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_thread_poll_pending, Genv.find_symbol ge thread_poll_pending = Some b_thread_poll_pending
∧ Genv.find_funct_ptr ge b_thread_poll_pending =
Some (External (EF_external thread_poll_pending thread_poll_pending_sig)))
∧ get_layer_primitive thread_poll_pending pthreadsched = OK (Some (gensem thread_poll_pending_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_poll_pending pthreadsched = OK (Some (gensem thread_poll_pending_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hrelease_lock_CHAN:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_release_lock_CHAN, Genv.find_symbol ge release_lock_CHAN = Some b_release_lock_CHAN
∧ Genv.find_funct_ptr ge b_release_lock_CHAN =
Some (External (EF_external release_lock_CHAN release_lock_CHAN_sig)))
∧ get_layer_primitive release_lock_CHAN pthreadsched = OK (Some (gensem release_lock_SC_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive release_lock_CHAN pthreadsched = OK (Some (gensem release_lock_SC_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hsleeper_inc:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_sleeper_inc, Genv.find_symbol ge sleeper_inc = Some b_sleeper_inc
∧ Genv.find_funct_ptr ge b_sleeper_inc =
Some (External (EF_external sleeper_inc sleeper_inc_sig)))
∧ get_layer_primitive sleeper_inc pthreadsched = OK (Some (gensem sleeper_inc_spec)).
Proof.
intros.
assert (Hprim: get_layer_primitive sleeper_inc pthreadsched = OK (Some (gensem sleeper_inc_spec)))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hthread_sched:
∀ MCode_Asm s ge,
make_globalenv s MCode_Asm pthreadsched = ret ge →
(∃ b_thread_sched, Genv.find_symbol ge thread_sched = Some b_thread_sched
∧ Genv.find_funct_ptr ge b_thread_sched =
Some (External (EF_external thread_sched null_signature)))
∧ get_layer_primitive thread_sched pthreadsched = OK (Some (primcall_thread_schedule_compatsem
thread_sched_spec
(prim_ident:= thread_sched))).
Proof.
intros.
assert (Hprim: get_layer_primitive thread_sched pthreadsched = OK (Some (primcall_thread_schedule_compatsem
thread_sched_spec
(prim_ident:= thread_sched))))
by (unfold pthreadsched; reflexivity).
split; try assumption.
eapply make_globalenv_get_layer_primitive; eauto.
Qed.
Lemma Hthread_yield:
∀ ge s b,
make_globalenv s (thread_yield ↦ threadyield_function) pthreadsched = ret ge →
find_symbol s thread_yield = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal threadyield_function).
Proof.
intros.
assert (Hmodule: get_module_function thread_yield (thread_yield ↦ threadyield_function)
= OK (Some threadyield_function)) by
reflexivity.
assert (HInternal: make_internal threadyield_function = OK (AST.Internal threadyield_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
Lemma Hthread_sleep:
∀ ge s b,
make_globalenv s (thread_sleep ↦ threadsleep_function) pthreadsched = ret ge →
find_symbol s thread_sleep = Some b →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (Internal threadsleep_function).
Proof.
intros.
assert (Hmodule: get_module_function thread_sleep (thread_sleep ↦ threadsleep_function) = OK (Some threadsleep_function)) by
reflexivity.
assert (HInternal: make_internal threadsleep_function = OK (AST.Internal threadsleep_function)) by reflexivity.
eapply make_globalenv_get_module_function in H; eauto.
destruct H as [?[Hsymbol ?]].
inv H1.
rewrite stencil_matches_symbols in Hsymbol.
rewrite H0 in Hsymbol. inv Hsymbol.
assumption.
Qed.
End WITHMEM.
End ASM_DATA.