Library mcertikos.mcslock.MMCSLockAbsIntroCodeMCSPassLock
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
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 CommonTactic.
Require Import TacticsForTesting.
Require Import MMCSLockAbsIntroCSource.
Require Import MMCSLockAbsIntro.
Require Import MCSLockOpGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Lemma multi_log_double_update:
∀ d ml1 ml2,
(d {multi_log: ml1}) {multi_log: ml2} = d {multi_log: ml2}.
Proof.
intros.
unfold update_multi_log; simpl.
reflexivity.
Qed.
Lemma ikern_remain :
∀ d ml, ikern d = ikern (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma ihost_remain:
∀ d ml, ihost d = ihost (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma oracle_remain:
∀ d ml,
multi_oracle d = multi_oracle (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma lock_AT_start_val: lock_AT_start = 0%Z.
Proof. reflexivity. Qed.
Lemma ID_AT_range_val: ID_AT_range = 1%Z.
Proof. unfold ID_AT_range; reflexivity. Qed.
Lemma lock_TCB_start_val : lock_TCB_start = 1%Z.
Proof. unfold lock_TCB_start; reflexivity. Qed.
Lemma num_chan_val: num_chan = num_chan.
Proof. reflexivity. Qed.
Lemma ID_TCB_range_val: ID_TCB_range = num_chan.
Proof. unfold ID_TCB_range; reflexivity. Qed.
Lemma lock_TCB_range_val: lock_TCB_range = (num_chan + 1)%Z.
Proof. unfold lock_TCB_range; simpl; reflexivity. Qed.
Lemma lock_SC_start_val: lock_SC_start = (num_chan + 1)%Z.
Proof. unfold lock_SC_start. rewrite lock_TCB_range_val. reflexivity. Qed.
Lemma lock_range_val: lock_range = (num_chan + num_chan + 1)%Z.
Proof.
unfold lock_range; simpl; reflexivity.
Qed.
Lemma t_struct_mcs_lock_size:
sizeof t_struct_mcs_lock = 576%Z.
Proof.
simpl.
unfold align; simpl; omega.
Qed.
Lemma t_struct_mcs_node_size:
sizeof t_struct_mcs_node = 64%Z.
Proof.
simpl.
unfold align; simpl; omega.
Qed.
Module MMCSLOCKABSINTROCODEMCSPASSLOCK.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{wait_time: WaitTime}.
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}.
Local Open Scope Z_scope.
Section MCSPASSLOCK.
Let L: compatlayer (cdata RData) :=
get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ mcs_get_next ↦ gensem mcs_get_next_spec
⊕ mcs_set_busy ↦ gensem mcs_set_busy_spec
⊕ mcs_cas_tail ↦ gensem mcs_cas_tail_spec
⊕ mcs_lock_get_index ↦ gensem mcs_lock_get_index_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Fixpoint CalMCS_RelWaitAux (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK mcstail mcsnp _) ⇒
match ZMap.get i mcsnp with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWaitAux n´ i l´ to
else Some l´
end
| _ ⇒ None
end
end.
Definition get_current_next_value (i : Z) (l : MultiLog) : option Z :=
match CalMCSLock l with
| Some (MCSLOCK _ cur_np _) ⇒
match ZMap.get i cur_np with
(_, cur_nt) ⇒ Some cur_nt
end
| _ ⇒ None
end.
Definition get_current_next_prop (i : Z) (l : MultiLog) : Prop :=
match get_current_next_value i l with
| Some cur_nt ⇒ if zeq cur_nt NULL then False else True
| _ ⇒ False
end.
Lemma CalMCS_RelWait_implies_CalMCS_RelWaitAux:
∀ n i l to l´,
CalMCS_RelWait n i l to = Some l´→
∃ l´´,
CalMCS_RelWaitAux n i l to = Some l´´ ∧ l´ = (TEVENT i (TTICKET SET_BUSY))::(to i l´´ ++ l´´) ∧
get_current_next_prop i (to i l´´ ++ l´´).
Proof.
induction n; simpl; intros.
- inv H.
- Transparent CalMCS_RelWait.
simpl in ×.
subdestruct.
+ simpl.
inversion Hdestruct0; subst.
eapply IHn in H.
destruct H as (l´´, (Ha, Hb)).
∃ l´´; tauto.
+ inv H.
esplit; repeat (split; eauto).
unfold get_current_next_prop.
unfold get_current_next_value.
rewrite Hdestruct3.
rewrite Hdestruct5.
rewrite Hdestruct6.
trivial.
Qed.
Lemma CalMCS_RelWaitAux_has_prefix :
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ l´´, l´ = l´´++l.
Proof.
clearAll.
induction m.
- simpl; intros; inv H.
- intros.
simpl in H.
subdestruct.
+ simpl in H.
eapply IHm in H.
destruct H.
∃ ( x ++ TEVENT i (TTICKET GET_NEXT) :: to i l).
rewrite app_assoc_reverse; simpl.
assumption.
+ inv H.
∃ (TEVENT i (TTICKET GET_NEXT) :: to i l); eauto.
Qed.
Lemma CalMCS_RelWaitAux_implies_some_mcs:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ mlock, CalMCSLock l´ = Some mlock.
Proof.
clearAll.
induction m; simpl; intros; [ inv H | ].
subdestruct.
- eapply IHm in H.
eassumption.
- Transparent CalMCSLock.
simpl in ×.
subdestruct.
inv H.
inv Hdestruct.
∃ (MCSLOCK tail lock_array bounds); simpl.
rewrite Hdestruct3.
reflexivity.
Qed.
Lemma CalMCSLock_prefix_has_CalMCSLock_aux:
∀ l a l´ mlock,
l = a::l´ →
CalMCSLock l = Some mlock →
∃ mlock´, CalMCSLock l´ = Some mlock´.
Proof.
clearAll.
intros; inv H; simpl in H0.
subdestruct; esplit; eauto.
Qed.
Lemma CalMCSLock_prefix_has_CalMCSLock:
∀ l´ l l´´ mlock,
l = l´ ++ l´´ →
CalMCSLock l = Some mlock →
∃ mlock´´, CalMCSLock l´´ = Some mlock´´.
Proof.
clearAll.
induction l´.
- intros; rewrite app_nil_l in H; subst.
∃ mlock; trivial.
- intros.
simpl in H.
destruct l; try (inv H; fail).
assert (m = a).
{ clearAllExceptOne H.
inv H; reflexivity. }
subst.
edestruct CalMCSLock_prefix_has_CalMCSLock_aux
with (2:= H0) as (mlock´, H1); eauto.
Qed.
Lemma CalMCSLock_fun :
∀ l mlock mlock´,
CalMCSLock l = Some mlock →
CalMCSLock l = Some mlock´ →
mlock = mlock´.
Proof.
clearAll.
destruct l.
- intros; simpl in ×.
inv H; inv H0; reflexivity.
- intros.
simpl in H; simpl in H0; subdestruct; try (inv H; inv H0; auto; fail).
Qed.
Fixpoint CalMCS_RelWaitAuxPre (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ Some l
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK mcstail mcsnp _) ⇒
match ZMap.get i mcsnp with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWaitAuxPre n´ i l´ to
else Some l´
end
| _ ⇒ None
end
end.
Lemma CalMCS_RelWaitAuxStops:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ k,
(k ≤ m)%nat ∧
(∀ n,
(0 ≤ n < k)%nat → CalMCS_RelWaitAux n i l to = None) ∧
CalMCS_RelWaitAux k i l to = Some l´ ∧
∀ j, (k ≤ j)%nat → CalMCS_RelWaitAuxPre j i l to = Some l´.
Proof.
clearAll.
induction m; simpl; intros; [inv H | ].
subdestruct.
- eapply IHm in H; eauto.
destruct H as (x & H & H0 & H1).
∃ (S x); split; [omega | split].
+ intros.
assert(n0case: n = O ∨ n ≠ O) by omega.
Caseeq n0case; intros.
× subst; reflexivity.
× eapply NPeano.Nat.succ_pred in H3.
rewrite <- H3; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply H0; eauto.
omega.
+ simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2; split; intros.
× apply H1.
× assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H3.
rewrite <- H3; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply H1; eauto; omega.
- subst; inv H.
∃ 1%nat.
split; [omega | split; intros ].
+ assert ((n0 = 0)%nat) by omega.
subst; simpl; reflexivity.
+ simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
split; [reflexivity |].
intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H0.
rewrite <- H0; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
Qed.
Lemma CalMCS_RelWaitAuxToPre:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
CalMCS_RelWaitAuxPre m i l to = Some l´.
Proof.
clearAll.
induction m; simpl; intros; [inv H |].
simpl; intros.
subdestruct.
- eapply IHm; eauto.
- apply H.
Qed.
Lemma CalMCS_RelWaitAuxToPreCons:
∀ m m´ i l to l´,
CalMCS_RelWaitAuxPre m i l to = Some l´ →
(m´ ≤ m)%nat →
∃ l´´,
CalMCS_RelWaitAuxPre m´ i l to = Some l´´.
Proof.
clearAll.
induction m; simpl; intros.
- assert(m´ = O) by omega.
subst; esplit; reflexivity.
- simpl; intros; subdestruct.
+ assert(m´ = O ∨ m´ ≠ O) by omega.
Caseeq H1; intros; subst; simpl.
esplit; reflexivity.
eapply NPeano.Nat.succ_pred in H1.
rewrite <- H1; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply IHm; eauto; omega.
+ inv H.
assert(m´ = O ∨ m´ ≠ O) by omega.
Caseeq H; intros; subst; simpl.
esplit; reflexivity.
eapply NPeano.Nat.succ_pred in H.
rewrite <- H; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
esplit; reflexivity.
Qed.
Lemma CalMCS_RelWaitAuxPreInv:
∀ m i l to l´,
CalMCS_RelWaitAuxPre (S m) i l to = Some l´ →
(∀ j, (j < (S m))%nat → CalMCS_RelWaitAux j i l to = None) →
∃ l´´,
CalMCS_RelWaitAuxPre m i l to = Some l´´ ∧
CalMCS_RelWaitAuxPre 1 i l´´ to = Some l´.
Proof.
clearAll.
induction m; simpl; intros.
- subdestruct.
+ inv H; esplit.
split; try reflexivity.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
+ inv H; esplit.
split; try reflexivity.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
- simpl in *; intros; subdestruct.
+ eapply IHm.
× rewrite Hdestruct3, Hdestruct5, Hdestruct6.
apply H.
× intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H2.
simpl in H2.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H2.
apply H2.
+ inv H.
eapply IHm.
rewrite Hdestruct3, Hdestruct5, Hdestruct6.
× reflexivity.
× intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H1.
simpl in H1.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H1.
apply H1.
+ inv H.
assert ((1 < S (S m))%nat) by omega.
eapply H0 in H.
simpl in H.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H.
inv H.
Qed.
Lemma CalMCS_RelWaitAuxPreNeq:
∀ m i l l´ to mlock mcstail mcsnp mcsbounds bs nt,
CalMCS_RelWaitAux m i l to = None →
CalMCS_RelWaitAuxPre m i l to = Some l´ →
(m > 0)%nat →
CalMCSLock l´ = Some mlock →
mlock = MCSLOCK mcstail mcsnp mcsbounds→
ZMap.get i mcsnp = (bs, nt) →
nt = NULL.
Proof.
clearAll.
induction m.
- simpl; intros; omega.
- simpl; intros.
subdestruct.
subst.
assert (m = O ∨ (m > O)%nat) by omega.
Caseeq H3; intros.
× subst.
inv H0.
simpl in H2.
subdestruct.
inv H2; inv Hdestruct.
rewrite Hdestruct1 in H4; inv H4.
reflexivity.
× eapply IHm; eauto.
Qed.
Lemma CalMCS_RelWaitAuxEq:
∀ m i l to l´ mlock mcstail mcsnp mcsbounds bs nt,
CalMCS_RelWaitAux m i l to = Some l´ →
CalMCSLock l´ = Some mlock →
mlock = MCSLOCK mcstail mcsnp mcsbounds →
ZMap.get i mcsnp = (bs, nt) →
nt ≠ NULL.
Proof.
clearAll.
induction m.
- simpl; intros.
inv H.
- simpl; intros.
subdestruct; subst.
× eapply IHm; eauto.
× inv H.
simpl in H0.
subdestruct.
inv H0; inv Hdestruct.
rewrite Hdestruct1 in H2; inv H2.
assumption.
Qed.
Lemma loop_pre_log_term_satisfies_hinv:
∀ adt lock_index l pre_log,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log = ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
clearAll; intros.
subst; inv H2.
constructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
- intros; subst.
rewrite ZMap.gss in Hdef; eauto; inv Hdef.
unfold valid_MCS_log.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log l) by (eapply valid_multi_log_pool_mcs_inv; eauto).
assert (valid_MCS_log (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l++l)).
{ unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv; eauto. }
assert (valid_MCS_log (TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)).
{ unfold valid_MCS_log; intros.
unfold MCSCorrect_range.
intros.
simpl in H6.
subdestruct.
inv H6.
inv H8.
unfold valid_MCS_log in H5.
unfold MCSCorrect_range in H5.
eapply H5 in Hdestruct; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv; eauto.
- intros; subst.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma loop_pre_log_satisfies_hinv:
∀ adt lock_index l pre_log,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log =
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
clearAll; intros.
subst; inv H2.
constructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
- intros; subst.
rewrite ZMap.gss in Hdef; eauto; inv Hdef.
unfold valid_MCS_log.
simpl.
intros.
subdestruct.
inv Hdestruct.
inv H4.
remember (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) as pre_log´.
eapply loop_pre_log_term_satisfies_hinv in Heqpre_log´; eauto; [ | constructor; auto].
inv Heqpre_log´; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv0.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
eapply valid_multi_log_pool_mcs_inv0; eauto.
rewrite ZMap.gss; auto.
- intros; subst.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma loop_CalMCS_RelWaitAuxPre_satisfies_hinv´:
∀ cur_index adt lock_index l m0,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
ZMap.get lock_index (multi_log adt) = MultiDef l →
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) l
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
induction cur_index; intros.
- intros.
simpl in H4; inv H4.
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool; intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv; eauto.
case_eq (zeq i lock_index).
+ intros; subst.
rewrite ZMap.gss in Hdef; inv Hdef; auto.
+ intros.
rewrite ZMap.gso in Hdef; eauto.
- simpl in H4.
subdestruct.
+ eapply IHcur_index
with (adt := adt {multi_log :
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
(multi_log adt)}) in H4; simpl in H4;
try (rewrite ZMap.set2 in H4; rewrite multi_log_double_update in H4);
try rewrite multi_log_double_update in H4;
try assumption; try (rewrite ZMap.gss; eauto);
try (inv H2; econstructor; simpl; eauto);
try (simpl; rewrite ZMap.gss; eauto).
intros.
unfold valid_MCS_log_pool; intros.
case_eq (zeq i lock_index); intros; subst.
× rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
intros.
eapply valid_multi_log_pool_mcs_inv in H3; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (1:= H1) (i0 := (CPU_ID adt)) in H3; eauto.
unfold valid_MCS_log in H3.
unfold MCSCorrect_range in H3.
simpl in H5; subdestruct.
inv H5.
unfold MCSCorrect_range.
intros.
inv Hmcs; inv Hdestruct.
eapply H3; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4; simpl in ×.
inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize H1; intros tmp_prop.
eapply valid_multi_log_pool_mcs_inv in tmp_prop; try (rewrite ZMap.gss; eauto); try exact H3; try exact H3.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID adt)) in tmp_prop; try assumption.
constructor; simpl; eauto; intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
× intros; subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
unfold valid_MCS_log; simpl; intros.
subdestruct.
inv H4.
inv Hdestruct.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in tmp_prop.
unfold MCSCorrect_range in tmp_prop.
eapply tmp_prop; eauto.
× intros.
rewrite ZMap.gso in Hdef; try eassumption.
inv H3; eauto.
Qed.
Lemma loop_CalMCS_RelWaitAuxPre_satisfies_hinv:
∀ cur_index adt lock_index l pre_log m0,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log =
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) →
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
intros.
assert (high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
{ generalize loop_pre_log_satisfies_hinv; eauto. }
assert (ZMap.get lock_index (multi_log (adt
{multi_log
: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}))
= MultiDef pre_log).
{ simpl; rewrite ZMap.gss; auto. }
generalize loop_CalMCS_RelWaitAuxPre_satisfies_hinv´;
intros.
eapply H8 with (4:= H6) (5:= H7) (6:= H5) in H1; try (simpl; assumption).
simpl in H1; rewrite ZMap.set2 in H1; rewrite multi_log_double_update in H1; auto.
Qed.
Section MCSPASSLOCKBODY.
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 MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
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 CommonTactic.
Require Import TacticsForTesting.
Require Import MMCSLockAbsIntroCSource.
Require Import MMCSLockAbsIntro.
Require Import MCSLockOpGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Lemma multi_log_double_update:
∀ d ml1 ml2,
(d {multi_log: ml1}) {multi_log: ml2} = d {multi_log: ml2}.
Proof.
intros.
unfold update_multi_log; simpl.
reflexivity.
Qed.
Lemma ikern_remain :
∀ d ml, ikern d = ikern (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma ihost_remain:
∀ d ml, ihost d = ihost (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma oracle_remain:
∀ d ml,
multi_oracle d = multi_oracle (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma lock_AT_start_val: lock_AT_start = 0%Z.
Proof. reflexivity. Qed.
Lemma ID_AT_range_val: ID_AT_range = 1%Z.
Proof. unfold ID_AT_range; reflexivity. Qed.
Lemma lock_TCB_start_val : lock_TCB_start = 1%Z.
Proof. unfold lock_TCB_start; reflexivity. Qed.
Lemma num_chan_val: num_chan = num_chan.
Proof. reflexivity. Qed.
Lemma ID_TCB_range_val: ID_TCB_range = num_chan.
Proof. unfold ID_TCB_range; reflexivity. Qed.
Lemma lock_TCB_range_val: lock_TCB_range = (num_chan + 1)%Z.
Proof. unfold lock_TCB_range; simpl; reflexivity. Qed.
Lemma lock_SC_start_val: lock_SC_start = (num_chan + 1)%Z.
Proof. unfold lock_SC_start. rewrite lock_TCB_range_val. reflexivity. Qed.
Lemma lock_range_val: lock_range = (num_chan + num_chan + 1)%Z.
Proof.
unfold lock_range; simpl; reflexivity.
Qed.
Lemma t_struct_mcs_lock_size:
sizeof t_struct_mcs_lock = 576%Z.
Proof.
simpl.
unfold align; simpl; omega.
Qed.
Lemma t_struct_mcs_node_size:
sizeof t_struct_mcs_node = 64%Z.
Proof.
simpl.
unfold align; simpl; omega.
Qed.
Module MMCSLOCKABSINTROCODEMCSPASSLOCK.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{wait_time: WaitTime}.
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}.
Local Open Scope Z_scope.
Section MCSPASSLOCK.
Let L: compatlayer (cdata RData) :=
get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ mcs_get_next ↦ gensem mcs_get_next_spec
⊕ mcs_set_busy ↦ gensem mcs_set_busy_spec
⊕ mcs_cas_tail ↦ gensem mcs_cas_tail_spec
⊕ mcs_lock_get_index ↦ gensem mcs_lock_get_index_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Fixpoint CalMCS_RelWaitAux (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ None
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK mcstail mcsnp _) ⇒
match ZMap.get i mcsnp with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWaitAux n´ i l´ to
else Some l´
end
| _ ⇒ None
end
end.
Definition get_current_next_value (i : Z) (l : MultiLog) : option Z :=
match CalMCSLock l with
| Some (MCSLOCK _ cur_np _) ⇒
match ZMap.get i cur_np with
(_, cur_nt) ⇒ Some cur_nt
end
| _ ⇒ None
end.
Definition get_current_next_prop (i : Z) (l : MultiLog) : Prop :=
match get_current_next_value i l with
| Some cur_nt ⇒ if zeq cur_nt NULL then False else True
| _ ⇒ False
end.
Lemma CalMCS_RelWait_implies_CalMCS_RelWaitAux:
∀ n i l to l´,
CalMCS_RelWait n i l to = Some l´→
∃ l´´,
CalMCS_RelWaitAux n i l to = Some l´´ ∧ l´ = (TEVENT i (TTICKET SET_BUSY))::(to i l´´ ++ l´´) ∧
get_current_next_prop i (to i l´´ ++ l´´).
Proof.
induction n; simpl; intros.
- inv H.
- Transparent CalMCS_RelWait.
simpl in ×.
subdestruct.
+ simpl.
inversion Hdestruct0; subst.
eapply IHn in H.
destruct H as (l´´, (Ha, Hb)).
∃ l´´; tauto.
+ inv H.
esplit; repeat (split; eauto).
unfold get_current_next_prop.
unfold get_current_next_value.
rewrite Hdestruct3.
rewrite Hdestruct5.
rewrite Hdestruct6.
trivial.
Qed.
Lemma CalMCS_RelWaitAux_has_prefix :
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ l´´, l´ = l´´++l.
Proof.
clearAll.
induction m.
- simpl; intros; inv H.
- intros.
simpl in H.
subdestruct.
+ simpl in H.
eapply IHm in H.
destruct H.
∃ ( x ++ TEVENT i (TTICKET GET_NEXT) :: to i l).
rewrite app_assoc_reverse; simpl.
assumption.
+ inv H.
∃ (TEVENT i (TTICKET GET_NEXT) :: to i l); eauto.
Qed.
Lemma CalMCS_RelWaitAux_implies_some_mcs:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ mlock, CalMCSLock l´ = Some mlock.
Proof.
clearAll.
induction m; simpl; intros; [ inv H | ].
subdestruct.
- eapply IHm in H.
eassumption.
- Transparent CalMCSLock.
simpl in ×.
subdestruct.
inv H.
inv Hdestruct.
∃ (MCSLOCK tail lock_array bounds); simpl.
rewrite Hdestruct3.
reflexivity.
Qed.
Lemma CalMCSLock_prefix_has_CalMCSLock_aux:
∀ l a l´ mlock,
l = a::l´ →
CalMCSLock l = Some mlock →
∃ mlock´, CalMCSLock l´ = Some mlock´.
Proof.
clearAll.
intros; inv H; simpl in H0.
subdestruct; esplit; eauto.
Qed.
Lemma CalMCSLock_prefix_has_CalMCSLock:
∀ l´ l l´´ mlock,
l = l´ ++ l´´ →
CalMCSLock l = Some mlock →
∃ mlock´´, CalMCSLock l´´ = Some mlock´´.
Proof.
clearAll.
induction l´.
- intros; rewrite app_nil_l in H; subst.
∃ mlock; trivial.
- intros.
simpl in H.
destruct l; try (inv H; fail).
assert (m = a).
{ clearAllExceptOne H.
inv H; reflexivity. }
subst.
edestruct CalMCSLock_prefix_has_CalMCSLock_aux
with (2:= H0) as (mlock´, H1); eauto.
Qed.
Lemma CalMCSLock_fun :
∀ l mlock mlock´,
CalMCSLock l = Some mlock →
CalMCSLock l = Some mlock´ →
mlock = mlock´.
Proof.
clearAll.
destruct l.
- intros; simpl in ×.
inv H; inv H0; reflexivity.
- intros.
simpl in H; simpl in H0; subdestruct; try (inv H; inv H0; auto; fail).
Qed.
Fixpoint CalMCS_RelWaitAuxPre (n: nat) (i : Z) (l: MultiLog) (to: MultiOracle) : option MultiLog :=
match n with
| O ⇒ Some l
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NEXT)) :: (to i l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK mcstail mcsnp _) ⇒
match ZMap.get i mcsnp with
| (_, p) ⇒ if zeq p NULL
then CalMCS_RelWaitAuxPre n´ i l´ to
else Some l´
end
| _ ⇒ None
end
end.
Lemma CalMCS_RelWaitAuxStops:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
∃ k,
(k ≤ m)%nat ∧
(∀ n,
(0 ≤ n < k)%nat → CalMCS_RelWaitAux n i l to = None) ∧
CalMCS_RelWaitAux k i l to = Some l´ ∧
∀ j, (k ≤ j)%nat → CalMCS_RelWaitAuxPre j i l to = Some l´.
Proof.
clearAll.
induction m; simpl; intros; [inv H | ].
subdestruct.
- eapply IHm in H; eauto.
destruct H as (x & H & H0 & H1).
∃ (S x); split; [omega | split].
+ intros.
assert(n0case: n = O ∨ n ≠ O) by omega.
Caseeq n0case; intros.
× subst; reflexivity.
× eapply NPeano.Nat.succ_pred in H3.
rewrite <- H3; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply H0; eauto.
omega.
+ simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2; split; intros.
× apply H1.
× assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H3.
rewrite <- H3; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply H1; eauto; omega.
- subst; inv H.
∃ 1%nat.
split; [omega | split; intros ].
+ assert ((n0 = 0)%nat) by omega.
subst; simpl; reflexivity.
+ simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
split; [reflexivity |].
intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H0.
rewrite <- H0; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
Qed.
Lemma CalMCS_RelWaitAuxToPre:
∀ m i l to l´,
CalMCS_RelWaitAux m i l to = Some l´ →
CalMCS_RelWaitAuxPre m i l to = Some l´.
Proof.
clearAll.
induction m; simpl; intros; [inv H |].
simpl; intros.
subdestruct.
- eapply IHm; eauto.
- apply H.
Qed.
Lemma CalMCS_RelWaitAuxToPreCons:
∀ m m´ i l to l´,
CalMCS_RelWaitAuxPre m i l to = Some l´ →
(m´ ≤ m)%nat →
∃ l´´,
CalMCS_RelWaitAuxPre m´ i l to = Some l´´.
Proof.
clearAll.
induction m; simpl; intros.
- assert(m´ = O) by omega.
subst; esplit; reflexivity.
- simpl; intros; subdestruct.
+ assert(m´ = O ∨ m´ ≠ O) by omega.
Caseeq H1; intros; subst; simpl.
esplit; reflexivity.
eapply NPeano.Nat.succ_pred in H1.
rewrite <- H1; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
eapply IHm; eauto; omega.
+ inv H.
assert(m´ = O ∨ m´ ≠ O) by omega.
Caseeq H; intros; subst; simpl.
esplit; reflexivity.
eapply NPeano.Nat.succ_pred in H.
rewrite <- H; simpl.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
esplit; reflexivity.
Qed.
Lemma CalMCS_RelWaitAuxPreInv:
∀ m i l to l´,
CalMCS_RelWaitAuxPre (S m) i l to = Some l´ →
(∀ j, (j < (S m))%nat → CalMCS_RelWaitAux j i l to = None) →
∃ l´´,
CalMCS_RelWaitAuxPre m i l to = Some l´´ ∧
CalMCS_RelWaitAuxPre 1 i l´´ to = Some l´.
Proof.
clearAll.
induction m; simpl; intros.
- subdestruct.
+ inv H; esplit.
split; try reflexivity.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
+ inv H; esplit.
split; try reflexivity.
rewrite Hdestruct, Hdestruct1, Hdestruct2.
reflexivity.
- simpl in *; intros; subdestruct.
+ eapply IHm.
× rewrite Hdestruct3, Hdestruct5, Hdestruct6.
apply H.
× intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H2.
simpl in H2.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H2.
apply H2.
+ inv H.
eapply IHm.
rewrite Hdestruct3, Hdestruct5, Hdestruct6.
× reflexivity.
× intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H1.
simpl in H1.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H1.
apply H1.
+ inv H.
assert ((1 < S (S m))%nat) by omega.
eapply H0 in H.
simpl in H.
rewrite Hdestruct, Hdestruct1, Hdestruct2 in H.
inv H.
Qed.
Lemma CalMCS_RelWaitAuxPreNeq:
∀ m i l l´ to mlock mcstail mcsnp mcsbounds bs nt,
CalMCS_RelWaitAux m i l to = None →
CalMCS_RelWaitAuxPre m i l to = Some l´ →
(m > 0)%nat →
CalMCSLock l´ = Some mlock →
mlock = MCSLOCK mcstail mcsnp mcsbounds→
ZMap.get i mcsnp = (bs, nt) →
nt = NULL.
Proof.
clearAll.
induction m.
- simpl; intros; omega.
- simpl; intros.
subdestruct.
subst.
assert (m = O ∨ (m > O)%nat) by omega.
Caseeq H3; intros.
× subst.
inv H0.
simpl in H2.
subdestruct.
inv H2; inv Hdestruct.
rewrite Hdestruct1 in H4; inv H4.
reflexivity.
× eapply IHm; eauto.
Qed.
Lemma CalMCS_RelWaitAuxEq:
∀ m i l to l´ mlock mcstail mcsnp mcsbounds bs nt,
CalMCS_RelWaitAux m i l to = Some l´ →
CalMCSLock l´ = Some mlock →
mlock = MCSLOCK mcstail mcsnp mcsbounds →
ZMap.get i mcsnp = (bs, nt) →
nt ≠ NULL.
Proof.
clearAll.
induction m.
- simpl; intros.
inv H.
- simpl; intros.
subdestruct; subst.
× eapply IHm; eauto.
× inv H.
simpl in H0.
subdestruct.
inv H0; inv Hdestruct.
rewrite Hdestruct1 in H2; inv H2.
assumption.
Qed.
Lemma loop_pre_log_term_satisfies_hinv:
∀ adt lock_index l pre_log,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log = ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
clearAll; intros.
subst; inv H2.
constructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
- intros; subst.
rewrite ZMap.gss in Hdef; eauto; inv Hdef.
unfold valid_MCS_log.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log l) by (eapply valid_multi_log_pool_mcs_inv; eauto).
assert (valid_MCS_log (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l++l)).
{ unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv; eauto. }
assert (valid_MCS_log (TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)).
{ unfold valid_MCS_log; intros.
unfold MCSCorrect_range.
intros.
simpl in H6.
subdestruct.
inv H6.
inv H8.
unfold valid_MCS_log in H5.
unfold MCSCorrect_range in H5.
eapply H5 in Hdestruct; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv; eauto.
- intros; subst.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma loop_pre_log_satisfies_hinv:
∀ adt lock_index l pre_log,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log =
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
clearAll; intros.
subst; inv H2.
constructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
- intros; subst.
rewrite ZMap.gss in Hdef; eauto; inv Hdef.
unfold valid_MCS_log.
simpl.
intros.
subdestruct.
inv Hdestruct.
inv H4.
remember (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) as pre_log´.
eapply loop_pre_log_term_satisfies_hinv in Heqpre_log´; eauto; [ | constructor; auto].
inv Heqpre_log´; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv0.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
eapply valid_multi_log_pool_mcs_inv0; eauto.
rewrite ZMap.gss; auto.
- intros; subst.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma loop_CalMCS_RelWaitAuxPre_satisfies_hinv´:
∀ cur_index adt lock_index l m0,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
ZMap.get lock_index (multi_log adt) = MultiDef l →
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) l
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
induction cur_index; intros.
- intros.
simpl in H4; inv H4.
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool; intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv; eauto.
case_eq (zeq i lock_index).
+ intros; subst.
rewrite ZMap.gss in Hdef; inv Hdef; auto.
+ intros.
rewrite ZMap.gso in Hdef; eauto.
- simpl in H4.
subdestruct.
+ eapply IHcur_index
with (adt := adt {multi_log :
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
(multi_log adt)}) in H4; simpl in H4;
try (rewrite ZMap.set2 in H4; rewrite multi_log_double_update in H4);
try rewrite multi_log_double_update in H4;
try assumption; try (rewrite ZMap.gss; eauto);
try (inv H2; econstructor; simpl; eauto);
try (simpl; rewrite ZMap.gss; eauto).
intros.
unfold valid_MCS_log_pool; intros.
case_eq (zeq i lock_index); intros; subst.
× rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
intros.
eapply valid_multi_log_pool_mcs_inv in H3; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (1:= H1) (i0 := (CPU_ID adt)) in H3; eauto.
unfold valid_MCS_log in H3.
unfold MCSCorrect_range in H3.
simpl in H5; subdestruct.
inv H5.
unfold MCSCorrect_range.
intros.
inv Hmcs; inv Hdestruct.
eapply H3; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4; simpl in ×.
inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize H1; intros tmp_prop.
eapply valid_multi_log_pool_mcs_inv in tmp_prop; try (rewrite ZMap.gss; eauto); try exact H3; try exact H3.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID adt)) in tmp_prop; try assumption.
constructor; simpl; eauto; intros.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i lock_index).
× intros; subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
unfold valid_MCS_log; simpl; intros.
subdestruct.
inv H4.
inv Hdestruct.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in tmp_prop.
unfold MCSCorrect_range in tmp_prop.
eapply tmp_prop; eauto.
× intros.
rewrite ZMap.gso in Hdef; try eassumption.
inv H3; eauto.
Qed.
Lemma loop_CalMCS_RelWaitAuxPre_satisfies_hinv:
∀ cur_index adt lock_index l pre_log m0,
ikern adt = true →
ihost adt = true →
0 ≤ lock_index < lock_range →
high_level_invariant adt →
(ZMap.get lock_index (multi_log adt)) = MultiDef l →
pre_log =
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) →
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
intros.
assert (high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
{ generalize loop_pre_log_satisfies_hinv; eauto. }
assert (ZMap.get lock_index (multi_log (adt
{multi_log
: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}))
= MultiDef pre_log).
{ simpl; rewrite ZMap.gss; auto. }
generalize loop_CalMCS_RelWaitAuxPre_satisfies_hinv´;
intros.
eapply H8 with (4:= H6) (5:= H7) (6:= H5) in H1; try (simpl; assumption).
simpl in H1; rewrite ZMap.set2 in H1; rewrite multi_log_double_update in H1; auto.
Qed.
Section MCSPASSLOCKBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
get_curid
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 tuint cc_default))
Tnil tuint cc_default).
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 tuint cc_default))
Tnil tuint cc_default).
mcs_get_next
Variable bmcs_get_next: block.
Hypothesis hmcs_get_next1 : Genv.find_symbol ge mcs_get_next = Some bmcs_get_next.
Hypothesis hmcs_get_next2 :
Genv.find_funct_ptr ge bmcs_get_next =
Some (External (EF_external mcs_get_next
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
Hypothesis hmcs_get_next1 : Genv.find_symbol ge mcs_get_next = Some bmcs_get_next.
Hypothesis hmcs_get_next2 :
Genv.find_funct_ptr ge bmcs_get_next =
Some (External (EF_external mcs_get_next
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
mcs_set_busy
Variable bmcs_set_busy: block.
Hypothesis hmcs_set_busy1 : Genv.find_symbol ge mcs_set_busy = Some bmcs_set_busy.
Hypothesis hmcs_set_busy2 :
Genv.find_funct_ptr ge bmcs_set_busy =
Some (External (EF_external mcs_set_busy
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Hypothesis hmcs_set_busy1 : Genv.find_symbol ge mcs_set_busy = Some bmcs_set_busy.
Hypothesis hmcs_set_busy2 :
Genv.find_funct_ptr ge bmcs_set_busy =
Some (External (EF_external mcs_set_busy
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
mcs_cas_tail
Variable bmcs_cas_tail: block.
Hypothesis hmcs_cas_tail1 : Genv.find_symbol ge mcs_cas_tail = Some bmcs_cas_tail.
Hypothesis hmcs_cas_tail2 :
Genv.find_funct_ptr ge bmcs_cas_tail =
Some (External (EF_external mcs_cas_tail
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
Hypothesis hmcs_cas_tail1 : Genv.find_symbol ge mcs_cas_tail = Some bmcs_cas_tail.
Hypothesis hmcs_cas_tail2 :
Genv.find_funct_ptr ge bmcs_cas_tail =
Some (External (EF_external mcs_cas_tail
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
mcs_lock_get_index
Variable bmcs_lock_get_index: block.
Hypothesis hmcs_lock_get_index1 : Genv.find_symbol ge mcs_lock_get_index = Some bmcs_lock_get_index.
Hypothesis hmcs_lock_get_index2 :
Genv.find_funct_ptr ge bmcs_lock_get_index =
Some (External (EF_external mcs_lock_get_index
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
Section mcs_pass_lock_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable K: nat. Variable cal_time : nat. Variable l : MultiLog. Variable l1: MultiLog.
Variable lock_index : Z. Variable current_next : Z.
Hypothesis iihost: ihost adt = true.
Hypothesis iikern: ikern adt = true.
Hypothesis hinv: high_level_invariant adt.
Hypothesis cur_id_range : 0 ≤ (CPU_ID adt) < TOTAL_CPU.
Hypothesis lock_index_range : 0 ≤ lock_index < lock_range.
Hypothesis Krange: (0 < K < cal_time)%nat.
Hypothesis initlist: (ZMap.get lock_index (multi_log adt)) = MultiDef l.
Notation pre_log :=
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l).
Definition Calculate_MCSPassLock (i: nat) :=
match CalMCS_RelWaitAuxPre i (CPU_ID adt) pre_log (ZMap.get lock_index (multi_oracle adt)) with
| Some l´ ⇒
Some (adt {multi_log : ZMap.set lock_index (MultiDef l´) (multi_log adt)})
| _ ⇒ None
end.
Definition get_current_next (d: RData) :=
match ZMap.get lock_index (multi_log d) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ cur_np _) ⇒
match ZMap.get (CPU_ID adt) cur_np with
(_, cur_nt) ⇒ Some cur_nt
end
| _ ⇒ None
end
| _ ⇒ None
end.
Hypothesis init_current_next:
current_next = NULL.
Hypothesis CalcWait:
CalMCS_RelWaitAux (pred cal_time) (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis Kpre: ∀ n,
(0 ≤ n < K)%nat →
CalMCS_RelWaitAux n (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = None.
Hypothesis Klast: CalMCS_RelWaitAux K (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis Klastpre: ∀ j,
(K ≤ j)%nat →
CalMCS_RelWaitAuxPre j (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis next_at_while_begin:
get_current_next (adt {multi_log : ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}) = Some NULL.
Definition pass_lock_loop_body_P (le: temp_env) (m : mem): Prop :=
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr current_next)) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
(get_current_next adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)})
= Some current_next ∧
m = (minit, adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
Definition pass_lock_loop_body_Q (le: temp_env) (m : mem): Prop :=
∃ d new_next,
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr (new_next))) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
(get_current_next d) = Some new_next ∧
new_next ≠ NULL ∧
Calculate_MCSPassLock (pred cal_time) = Some d∧
m = (minit, d).
Lemma pre_log_satisfies_hinv:
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
generalize loop_pre_log_satisfies_hinv; eauto.
Qed.
Lemma CalMCS_RelWaitAuxPre_satisfies_hinv:
∀ cur_index m0,
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
generalize loop_CalMCS_RelWaitAuxPre_satisfies_hinv; eauto.
Qed.
Lemma pass_lock_loop_correct_aux:
LoopProofSimpleWhile.t
f_mcs_pass_lock_while_condition
f_mcs_pass_lock_while_body
ge (PTree.empty _)
pass_lock_loop_body_P
pass_lock_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 new_next d´,
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr new_next)) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
get_current_next d´ = Some new_next ∧
(( i = O ∧ new_next = NULL ∧
d´ = adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}) ∨
(((0 < i < K)%nat ∧ new_next = NULL ∨ i = K ∧ new_next ≠ NULL) ∧
Calculate_MCSPassLock i = Some d´)) ∧
w = Z.of_nat K - Z.of_nat i ∧
m = (minit, d´)
).
- apply Zwf_well_founded.
- intros le m Hp.
destruct Hp as (Hle1 & Hle2 & Hle3 & Hle4 & Hc_next & Hm).
∃ (Z.of_nat K), O, NULL.
∃ (adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
rewrite init_current_next in Hle3.
repeat vcgen.
+ rewrite <- Nat2Z.inj_sub.
rewrite NPeano.Nat.sub_0_r.
reflexivity.
omega.
- intros le m n Hp.
destruct Hp as (cur_index & new_next & new_d &
Hle1 & Hle2 & Hle3 & Hle4 & Hc_next & Hcond & Hw & Hm).
Caseeq Hcond.
+
intros (ival & new & nd); subst.
unfold get_current_next in Hc_next; simpl in Hc_next.
subdestruct.
inversion Hc_next.
rewrite H0 in ×.
esplit; esplit.
repeat vcgen; try (subst; repeat vcgen; fail); subst.
× unfold Int.eq in H.
unfold Int.one, Int.zero in H.
rewrite Int.unsigned_repr in H; try omega.
rewrite Int.unsigned_repr in H; try omega.
simpl in H; inv H.
× assert (tmp: ∃ mcs,
CalMCSLock (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) pre_log ++ pre_log) = Some mcs).
{ assert (kneq0: K ≠ O) by omega.
apply NPeano.Nat.succ_pred in kneq0.
rewrite <- kneq0 in Klast.
simpl in Klast.
subdestruct; esplit; rewrite Hdestruct1; reflexivity. }
destruct tmp as (mcs´, tmp).
assert (tmp´: CalMCSLock
(ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) pre_log ++ pre_log) = Some mcs´).
{ simpl in tmp; subdestruct; try (inv tmp; fail).
assumption. }
assert (tmp_next: ∃ tmp_next,
get_current_next (adt {multi_log:
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) pre_log ++ pre_log))
(multi_log adt)}) = Some tmp_next).
{ unfold get_current_next.
simpl.
rewrite ZMap.gss.
rewrite tmp.
destruct mcs´.
∃ (snd (ZMap.get (CPU_ID adt) lock_array0)).
destruct (ZMap.get (CPU_ID adt) lock_array0).
simpl; reflexivity. }
destruct tmp_next as (tmp_next, tmp_next_prop).
esplit; esplit; repeat vcgen.
{ unfold mcs_get_next_spec; subst.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite iikern, iihost.
rewrite zle_lt_true; try eauto.
rewrite zle_lt_true; try eauto.
simpl; rewrite ZMap.gss.
rewrite tmp´.
instantiate (1:= (Int.repr tmp_next)).
assert (0 ≤ tmp_next < TOTAL_CPU ∨ tmp_next = NULL).
{ assert (0 ≤ tmp_next ≤ TOTAL_CPU).
{ unfold get_current_next in tmp_next_prop.
subdestruct.
generalize pre_log_satisfies_hinv; intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= pre_log) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID adt)) in lock_index_range´; eauto.
subdestruct.
inv Hdestruct6; eauto.
destruct mcs´.
inv tmp.
clear tmp´.
inv tmp_next_prop.
rewrite ZMap.gss in Hdestruct1; eauto.
inv Hdestruct1.
simpl in Hdestruct3.
subdestruct.
inv Hdestruct3.
inv Hdestruct4.
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H1 in CPU_ID_range.
rewrite Hdestruct5 in CPU_ID_range; simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL; omega. }
rewrite Int.unsigned_repr; [ | rewrite max_unsigned_val; unfold NULL in H0; destruct H0; omega].
destruct mcs´.
unfold get_current_next in tmp_next_prop; subdestruct.
simpl in Hdestruct1.
rewrite ZMap.gss in Hdestruct1.
inv Hdestruct1.
rewrite tmp in Hdestruct3.
inv Hdestruct3.
inv tmp_next_prop.
rewrite Hdestruct5.
repeat vcgen. }
{ rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega. }
{
∃ (Z.of_nat K - 1).
repeat vcgen.
∃ 1%nat.
esplit.
rewrite multi_log_double_update.
esplit; repeat vcgen.
- right.
assert (Kcase: (1 = K ∨ 1 < K)%nat) by omega.
Caseeq Kcase; intros.
+
rewrite <- H0.
split; [right | ].
× split; auto.
rewrite <- H0 in Klast.
simpl in Klast.
subdestruct; subst.
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct3.
rewrite ZMap.gss in Hdestruct3.
inv Hdestruct3.
inv Klast.
simpl in Hdestruct6.
subdestruct; try (inv Hdestruct6; fail); subst.
rewrite Hdestruct1 in Hdestruct6.
inv tmp_next_prop.
inv Hdestruct6.
inv tmp.
rewrite Hdestruct8 in Hdestruct4.
inv Hdestruct4.
auto.
× unfold Calculate_MCSPassLock; subst.
simpl in Klast.
subdestruct; subst.
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct3.
rewrite ZMap.gss in Hdestruct3.
inv Hdestruct3.
inv Klast.
simpl in Hdestruct6.
subdestruct; try (inv Hdestruct6; fail); subst.
rewrite Hdestruct1 in Hdestruct6.
inv tmp_next_prop.
inv Hdestruct6.
inv tmp.
rewrite Hdestruct8 in Hdestruct4.
inv Hdestruct4.
inv Hdestruct1.
rewrite Hdestruct8.
rewrite Hdestruct5.
reflexivity.
+
split.
× left.
split; try omega.
assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply Kpre in onerange.
simpl in onerange.
subdestruct.
unfold get_current_next in tmp_next_prop; subdestruct.
subst.
inv tmp_next_prop.
simpl in Hdestruct6.
rewrite ZMap.gss in Hdestruct6.
inv Hdestruct6.
simpl in Hdestruct7.
subdestruct; try (inv Hdestruct7; fail).
inversion Hdestruct7.
inv tmp´.
inv Hdestruct1.
rewrite Hdestruct9 in Hdestruct4.
inv Hdestruct4.
reflexivity.
× assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply Kpre in onerange.
simpl in onerange.
subdestruct.
unfold get_current_next in tmp_next_prop; subdestruct.
subst.
inv tmp_next_prop.
simpl in Hdestruct6.
rewrite ZMap.gss in Hdestruct6.
inv Hdestruct6.
simpl in Hdestruct7.
subdestruct; try (inv Hdestruct7; fail).
inversion Hdestruct7.
inv tmp´.
inv Hdestruct1.
rewrite Hdestruct9 in Hdestruct4.
inv Hdestruct4.
unfold Calculate_MCSPassLock; subst.
simpl.
simpl in tmp.
subdestruct; try (inv tmp; fail); subst.
inv tmp.
rewrite Hdestruct9.
simpl.
reflexivity.
- rewrite ZMap.set2.
reflexivity. }
+ intro tmp; destruct tmp as [icond Hcalc].
Caseeq icond.
×
intros (irange & neq).
unfold Calculate_MCSPassLock in Hcalc.
subdestruct.
inv Hcalc.
assert (tmp: ∃ mlock,
CalMCSLock (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)::(ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) m0 ++ m0) = Some mlock).
{ eapply CalMCS_RelWaitAuxToPre in Klast.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
eapply CalMCS_RelWaitAuxPreInv in H0; eauto.
- destruct H0.
destruct H0.
rewrite Hdestruct in H0.
inv H0.
simpl in H1.
subdestruct; rewrite Hdestruct0; esplit; reflexivity.
- intros.
eapply Kpre; eauto.
omega. }
destruct tmp as (mcs´, tmp).
assert (tmp´: CalMCSLock (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) m0 ++ m0) = Some mcs´).
{ simpl in tmp; subdestruct; try (inv tmp; fail).
assumption. }
assert (tmp_next: ∃ tmp_next,
get_current_next (adt {multi_log:
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) m0 ++ m0))
(multi_log adt)}) = Some tmp_next).
{ unfold get_current_next.
simpl.
rewrite ZMap.gss.
rewrite tmp.
destruct mcs´.
∃ (snd (ZMap.get (CPU_ID adt) lock_array)).
destruct (ZMap.get (CPU_ID adt) lock_array).
simpl; reflexivity. }
destruct tmp_next as (tmp_next, tmp_next_prop).
esplit; esplit; repeat vcgen.
{ unfold Int.eq in H.
unfold Int.one, Int.zero in H.
rewrite Int.unsigned_repr in H; try omega.
rewrite Int.unsigned_repr in H; try omega.
simpl in H; inv H. }
{ esplit; esplit.
repeat vcgen.
- unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite iikern, iihost.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl; rewrite ZMap.gss.
rewrite tmp´.
instantiate (1:= (Int.repr tmp_next)).
assert (0 ≤ tmp_next < TOTAL_CPU ∨ tmp_next = NULL).
{ assert (0 ≤ tmp_next ≤ TOTAL_CPU).
{ unfold get_current_next in tmp_next_prop.
subdestruct.
generalize (CalMCS_RelWaitAuxPre_satisfies_hinv cur_index m0 Hdestruct); intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= m0) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID adt)) in lock_index_range´; eauto.
subdestruct.
inv Hdestruct4; eauto.
destruct mcs´.
inv tmp.
clear tmp´.
inv tmp_next_prop.
rewrite ZMap.gss in Hdestruct0; eauto.
inv Hdestruct0.
simpl in Hdestruct1.
subdestruct.
inv Hdestruct1.
inv Hdestruct2.
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct0; eauto.
destruct Hdestruct0.
eapply H1 in CPU_ID_range.
rewrite Hdestruct3 in CPU_ID_range; simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL; omega. }
rewrite Int.unsigned_repr; [ | rewrite max_unsigned_val; unfold NULL in H0; destruct H0; omega].
destruct mcs´.
unfold get_current_next in tmp_next_prop; subdestruct.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite tmp in Hdestruct1.
inv Hdestruct1.
inv tmp_next_prop.
rewrite Hdestruct3.
repeat vcgen.
- rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega.
-
∃ (Z.of_nat K - Z.of_nat cur_index - 1).
repeat vcgen.
esplit; esplit; esplit.
repeat vcgen.
+ instantiate (1:= (S cur_index)).
right.
split.
× assert (icase: (S cur_index = K ∨ S cur_index < K)%nat) by omega.
Caseeq icase; intros.
{ right; split; auto.
assert((K ≤ K)%nat) by omega.
eapply Klastpre in H1.
rewrite <- H0 in H1.
assert (CalMCSLock l1 = Some mcs´).
{ eapply CalMCS_RelWaitAuxPreInv in H1; eauto.
- destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
+ inv H2.
simpl.
rewrite Hdestruct0.
eauto.
+ inv H2.
simpl.
rewrite Hdestruct0.
eauto.
- intros.
eapply Kpre; eauto.
omega. }
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite Hdestruct1 in tmp.
inv tmp.
inv tmp_next_prop.
eapply CalMCS_RelWaitAuxEq with (1:= Klast) (2:= H2); try eauto. }
{ left.
split; try omega.
assert ((0 ≤ S cur_index < K)%nat) by omega.
eapply Kpre in H1.
eapply CalMCS_RelWaitAuxToPre in Klast; eauto.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
assert (CalMCSLock x = Some mcs´).
{ eapply CalMCS_RelWaitAuxPreInv in H3; eauto.
- destruct H3.
destruct H3.
rewrite Hdestruct in H3.
inv H3.
simpl in H4.
subdestruct.
+ inv H4.
simpl.
rewrite Hdestruct0.
eauto.
+ inv H4.
simpl.
rewrite Hdestruct0.
eauto.
- intros.
eapply Kpre; eauto.
omega. }
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite Hdestruct1 in tmp.
inv tmp.
inv tmp_next_prop.
eapply CalMCS_RelWaitAuxPreNeq; try eauto.
omega. }
× unfold Calculate_MCSPassLock.
eapply CalMCS_RelWaitAuxToPre in Klast; eauto.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
rewrite H1.
eapply CalMCS_RelWaitAuxPreInv in H1; eauto.
{ destruct H1; destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
- inv H2.
reflexivity.
- inv H2.
reflexivity. }
{ intros.
eapply Kpre; eauto.
omega. }
+ rewrite Nat2Z.inj_succ.
unfold Z.succ.
omega.
+ rewrite ZMap.set2.
reflexivity. }
×
intros.
destruct H as (ci_val & cn_val).
assert (0 ≤ new_next < TOTAL_CPU).
{ unfold Calculate_MCSPassLock in Hcalc.
subdestruct.
inv Hcalc.
unfold get_current_next in Hc_next.
subdestruct.
inv Hc_next.
generalize (CalMCS_RelWaitAuxPre_satisfies_hinv K m0 Hdestruct); intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= m0) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
rewrite ZMap.gss in Hdestruct0; eauto; inv Hdestruct0.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H0 in CPU_ID_range.
rewrite Hdestruct3 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in cn_val.
omega. }
unfold NULL in ×.
esplit; esplit; repeat vcgen.
{ unfold pass_lock_loop_body_Q.
∃ new_d.
esplit.
repeat vcgen.
assert ((S K ≤ cal_time)%nat) by omega.
assert ((K ≤ (pred cal_time))%nat) by omega.
unfold Calculate_MCSPassLock in ×.
assert ((K ≤ K)%nat) by omega.
erewrite Klastpre in Hcalc; eauto; try omega.
erewrite Klastpre; eauto. }
Qed.
End mcs_pass_lock_loop_proof.
Lemma mcs_pass_lock_body_correct:
∀ m d d´ env le index ofs,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint index) →
PTree.get _offset le = Some (Vint ofs) →
kernel_mode d →
high_level_invariant d →
mcs_pass_lock_spec (Int.unsigned index) (Int.unsigned ofs) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_pass_lock_body E0 le´ (m, d´) (Out_return None).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize lock_AT_start_val; intros lat_val.
generalize ID_AT_range_val; intros iar_val.
generalize lock_TCB_start_val; intros lts_val.
generalize ID_TCB_range_val; intros itr_val.
generalize num_chan_val; intros nc_val.
generalize lock_TCB_range_val; intros ltr_val.
generalize lock_SC_start_val; intros lss_val.
generalize lock_range_val; intros lr_val.
generalize t_struct_mcs_lock_size; intros t_st_ml_size.
generalize t_struct_mcs_node_size; intros t_st_mn_size.
unfold f_mcs_pass_lock_body; subst.
unfold mcs_pass_lock_spec in H4.
destruct H2 as (H2a & H2b).
rewrite H2a, H2b in H4.
remember (index2Z (Int.unsigned index) (Int.unsigned ofs)) as lock_index.
destruct lock_index; try (inv H4; fail).
Opaque Z.add Z.mul.
assert (lock_index_range: 0 ≤ z < lock_range).
{ clearAllExceptTwo Heqlock_index lock_range_val.
assert (lock_id_val: (Int.unsigned index) = ID_AT ∨
(Int.unsigned index) = ID_TCB ∨
(Int.unsigned index) = ID_SC).
{ unfold index2Z in Heqlock_index.
unfold index_range in ×.
destruct (Int.unsigned index); try tauto; try (inversion Heqlock_index; fail).
destruct p; try tauto; try (inversion Heqlock_index; fail).
destruct p; try tauto; try (inversion Heqlock_index). }
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]];
rewrite lock_id_val in Heqlock_index; unfold index2Z in Heqlock_index; simpl in *; subdestruct;
inv Heqlock_index; rewrite lock_range_val.
- unfold ID_AT_range in *; omega.
- unfold ID_TCB_range, ID_AT_range in *; omega.
- unfold lock_TCB_range, ID_SC_range, ID_AT_range, ID_TCB_range in *; omega. }
symmetry in Heqlock_index.
assert (cid_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H3; omega. }
Transparent Z.add Z.mul.
Opaque CalMCSLock CalMCS_RelWait.
subdestruct.
- esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct; subst.
rewrite Hdestruct0.
rewrite zeq_true; eauto.
instantiate (1:= Int.one).
reflexivity. }
{
rewrite <- repr_one.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
simpl; repeat vcgen.
inv H4.
instantiate
(1:=
(PTree.set _cas_res (Vint Int.one)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))).
repeat vcgen. }
-
generalize Hdestruct3.
intro CalMCS_RelWait_Prop.
apply CalMCS_RelWait_implies_CalMCS_RelWaitAux in Hdestruct3.
destruct Hdestruct3 as (l´´, (Hdestruct3, (Hdestruct9, get_current_next_property))).
unfold CalPassLockTime in ×.
assert ((CalPassLockLoopTime > 0)%nat).
{ assert ((CalPassLockLoopTime ≠ 0)%nat).
intro.
rewrite H in Hdestruct3; simpl in Hdestruct3.
inv Hdestruct3.
omega. }
Opaque CalPassLockLoopTime.
rewrite <- NPeano.Nat.succ_pred_pos with (n:= CalPassLockLoopTime) in Hdestruct3 by omega.
simpl in Hdestruct3.
Transparent CalMCS_RelWaitAux.
simpl in Hdestruct3.
subdestruct; subst.
+
inv H4.
unfold NULL in ×.
Transparent CalMCSLock.
simpl in Hdestruct3.
generalize Hdestruct3; intro HcalcWait.
generalize HcalcWait; intro Hcalctmp.
eapply CalMCS_RelWaitAuxToPre in HcalcWait; eauto.
eapply CalMCS_RelWaitAuxStops in Hdestruct3; eauto.
destruct Hdestruct3 as [K [Krange [KPre [KPost KPostPre]]]].
assert (Kgt0: (0 < K)%nat).
{ assert (K = O → False).
intro.
subst.
inv KPost.
omega. }
assert (Krangelt: (0 < K < CalPassLockLoopTime)%nat) by omega.
remember NULL as current_next.
fold NULL in Hdestruct7.
rewrite <- Heqcurrent_next in Hdestruct7.
assert (gc_next :
get_current_next d z
(d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})
= Some NULL).
{ unfold get_current_next; simpl.
rewrite ZMap.gss.
rewrite Hdestruct5.
rewrite Hdestruct7.
f_equal; assumption. }
generalize (pass_lock_loop_correct_aux m _ K CalPassLockLoopTime _ _ z current_next
H2b H2a H3
cid_range lock_index_range Krangelt
Hdestruct Heqcurrent_next Hcalctmp KPre KPost KPostPre gc_next).
intros LP.
eapply LoopProofSimpleWhile.termination
with (condition := f_mcs_pass_lock_while_condition)
(body := f_mcs_pass_lock_while_body)
(P := pass_lock_loop_body_P m d l z current_next)
(Q := pass_lock_loop_body_Q m d CalPassLockLoopTime l z)
(le0 := (PTree.set
_current_next (Vint (Int.repr TOTAL_CPU))
(PTree.set
_null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set
_cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le))))))
(m0 := (m, (d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})))
in LP.
destruct LP as (while_le´, (while_m´, (LP1 & LP2))).
unfold pass_lock_loop_body_Q in LP2.
destruct LP2 as (while_d´, (while_new´, LP2)).
×
esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct.
rewrite Hdestruct0.
rewrite Hdestruct2.
instantiate (1:= Int.zero).
reflexivity. }
{
rewrite <- repr_zero.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
change E0 with (E0 ** E0).
econstructor; [repeat vcgen | ].
change E0 with (E0 ** E0).
econstructor.
-
repeat vcgen.
unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite multi_log_double_update.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
inv Hdestruct3; inv Hdestruct5.
rewrite Hdestruct7.
instantiate (1:= Int.repr TOTAL_CPU).
rewrite Int.unsigned_repr; [ | omega ].
repeat vcgen.
- change E0 with (E0 ** E0).
unfold set_opttemp.
econstructor.
+
eassumption.
+
idtac.
destruct LP2 as (LP21 & LP22 & LP23 & LP24 & LP25 & LP26 & LP27 & LP28).
instantiate (1:= while_le´).
inv LP28; subst.
repeat vcgen.
unfold mcs_set_busy_spec.
unfold Calculate_MCSPassLock in LP27.
rewrite HcalcWait in LP27.
inv LP27.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
simpl in Hdestruct4.
subdestruct; try (inv Hdestruct4; fail).
assert (0 ≤ z0 < TOTAL_CPU).
{ assert (high_level_invariant (d {multi_log: ZMap.set z (MultiDef l´´) (multi_log d)}))
by eauto using loop_CalMCS_RelWaitAuxPre_satisfies_hinv.
inv H2.
simpl in CPU_ID_range, valid_curid, valid_multi_log_pool_mcs_inv, valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l´´).
{ eapply valid_multi_log_pool_mcs_inv in lock_index_range; eauto.
rewrite ZMap.gss; auto. }
eapply valid_multi_oracle_pool_mcs_inv with (i0 := CPU_ID d) in H2; eauto.
unfold valid_MCS_log in H2.
unfold MCSCorrect_range in H2.
generalize Hdestruct1; intro prop.
eapply H2 in prop; eauto.
destruct prop.
eapply H5 in CPU_ID_range.
rewrite Hdestruct6 in CPU_ID_range.
simpl in CPU_ID_range.
unfold get_current_next_prop in get_current_next_property.
unfold get_current_next_value in get_current_next_property.
subdestruct; subst.
- contradiction.
- inv Hdestruct1.
rewrite Hdestruct6 in Hdestruct11.
inv Hdestruct11.
unfold NULL in n0.
clearAllExceptTwo n0 CPU_ID_range.
omega. }
rewrite zle_lt_true; try omega.
reflexivity. }
× unfold pass_lock_loop_body_P.
rewrite Heqcurrent_next; subst.
unfold NULL in ×.
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; auto.
+
inv H4; subst; inv Hdestruct4; subst.
esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct.
rewrite Hdestruct0.
rewrite Hdestruct2.
instantiate (1:= Int.zero).
reflexivity. }
{
rewrite <- repr_zero.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
change E0 with (E0 ** E0).
econstructor; [repeat vcgen | ].
change E0 with (E0 ** E0).
econstructor.
-
repeat vcgen.
unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite multi_log_double_update.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
inv Hdestruct3; inv Hdestruct5.
rewrite Hdestruct7.
instantiate (1:= Int.repr z0).
assert (0 ≤ z0 < TOTAL_CPU).
{ remember (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intros tmp_prop.
eapply loop_pre_log_term_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv in Hdestruct10; eauto; [ | rewrite ZMap.gss; auto].
destruct Hdestruct10.
apply H5 in CPU_ID_range.
rewrite Hdestruct7 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in n0.
omega. }
repeat vcgen.
- change E0 with (E0 ** E0).
unfold set_opttemp.
assert (0 ≤ z0 < TOTAL_CPU).
{ remember (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intros tmp_prop.
eapply loop_pre_log_term_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv.
simpl in Hdestruct5.
subdestruct.
inv Hdestruct3.
inv Hdestruct5.
eapply valid_multi_log_pool_mcs_inv in Hdestruct1; eauto; [ | rewrite ZMap.gss; auto].
destruct Hdestruct1.
apply H5 in CPU_ID_range.
rewrite Hdestruct7 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in n0; omega. }
instantiate (1:= (PTree.set _current_next (Vint (Int.repr z0))
(PTree.set _null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set _cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))))).
econstructor.
+
unfold f_mcs_pass_lock_while_condition, f_mcs_pass_lock_while_body.
instantiate (2:= (PTree.set
_current_next (Vint (Int.repr z0))
(PTree.set _null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set _cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))))).
unfold NULL in ×.
eapply ClightBigstep.exec_Sloop_stop1.
eapply exec_Sseq_2.
repeat vcgen.
{ intros contra.
inv contra. }
{ econstructor. }
+
repeat vcgen.
unfold mcs_set_busy_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
assert (0 ≤ z1 < TOTAL_CPU).
{ subst.
inv Hdestruct3.
assert (z1 ≠ NULL).
{ set (pre_log := (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
fold pre_log in CalMCS_RelWait_Prop.
fold pre_log in Hdestruct1.
fold pre_log in get_current_next_property.
unfold get_current_next_prop in get_current_next_property.
unfold get_current_next_value in get_current_next_property.
rewrite Hdestruct1 in get_current_next_property.
rewrite Hdestruct6 in get_current_next_property.
subdestruct; try contradiction; try auto. }
assert (0 ≤ z1 ≤ TOTAL_CPU).
{ remember (TEVENT (CPU_ID d) (TTICKET GET_NEXT)::ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intro tmp_prop.
eapply loop_pre_log_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv in lock_index_range; eauto; [ | rewrite ZMap.gss; reflexivity].
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in lock_index_range; eauto.
unfold valid_MCS_log in lock_index_range.
unfold MCSCorrect_range in lock_index_range.
eapply lock_index_range in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H7 in CPU_ID_range.
rewrite Hdestruct6 in CPU_ID_range.
simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL in H5.
omega. }
rewrite zle_lt_true; try omega.
reflexivity. }
Qed.
End MCSPASSLOCKBODY.
Theorem mcs_pass_lock_code_correct:
spec_le (pass_lock ↦ mcs_pass_lock_spec_low) (〚pass_lock ↦ f_mcs_pass_lock 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (mcs_pass_lock_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_pass_lock)
(Vint i::Vint ofs::nil)
(create_undef_temps (fn_temps f_mcs_pass_lock)))) muval.
Qed.
End MCSPASSLOCK.
End WithPrimitives.
End MMCSLOCKABSINTROCODEMCSPASSLOCK.
Hypothesis hmcs_lock_get_index1 : Genv.find_symbol ge mcs_lock_get_index = Some bmcs_lock_get_index.
Hypothesis hmcs_lock_get_index2 :
Genv.find_funct_ptr ge bmcs_lock_get_index =
Some (External (EF_external mcs_lock_get_index
(signature_of_type (Tcons tint (Tcons tint Tnil)) tuint cc_default))
(Tcons tint (Tcons tint Tnil)) tuint cc_default).
Section mcs_pass_lock_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable K: nat. Variable cal_time : nat. Variable l : MultiLog. Variable l1: MultiLog.
Variable lock_index : Z. Variable current_next : Z.
Hypothesis iihost: ihost adt = true.
Hypothesis iikern: ikern adt = true.
Hypothesis hinv: high_level_invariant adt.
Hypothesis cur_id_range : 0 ≤ (CPU_ID adt) < TOTAL_CPU.
Hypothesis lock_index_range : 0 ≤ lock_index < lock_range.
Hypothesis Krange: (0 < K < cal_time)%nat.
Hypothesis initlist: (ZMap.get lock_index (multi_log adt)) = MultiDef l.
Notation pre_log :=
(TEVENT (CPU_ID adt) (TTICKET GET_NEXT) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (CAS_TAIL false)) ::
(ZMap.get lock_index (multi_oracle adt)) (CPU_ID adt) l ++ l).
Definition Calculate_MCSPassLock (i: nat) :=
match CalMCS_RelWaitAuxPre i (CPU_ID adt) pre_log (ZMap.get lock_index (multi_oracle adt)) with
| Some l´ ⇒
Some (adt {multi_log : ZMap.set lock_index (MultiDef l´) (multi_log adt)})
| _ ⇒ None
end.
Definition get_current_next (d: RData) :=
match ZMap.get lock_index (multi_log d) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ cur_np _) ⇒
match ZMap.get (CPU_ID adt) cur_np with
(_, cur_nt) ⇒ Some cur_nt
end
| _ ⇒ None
end
| _ ⇒ None
end.
Hypothesis init_current_next:
current_next = NULL.
Hypothesis CalcWait:
CalMCS_RelWaitAux (pred cal_time) (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis Kpre: ∀ n,
(0 ≤ n < K)%nat →
CalMCS_RelWaitAux n (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = None.
Hypothesis Klast: CalMCS_RelWaitAux K (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis Klastpre: ∀ j,
(K ≤ j)%nat →
CalMCS_RelWaitAuxPre j (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis next_at_while_begin:
get_current_next (adt {multi_log : ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}) = Some NULL.
Definition pass_lock_loop_body_P (le: temp_env) (m : mem): Prop :=
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr current_next)) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
(get_current_next adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)})
= Some current_next ∧
m = (minit, adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
Definition pass_lock_loop_body_Q (le: temp_env) (m : mem): Prop :=
∃ d new_next,
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr (new_next))) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
(get_current_next d) = Some new_next ∧
new_next ≠ NULL ∧
Calculate_MCSPassLock (pred cal_time) = Some d∧
m = (minit, d).
Lemma pre_log_satisfies_hinv:
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef pre_log)
(multi_log adt)}.
Proof.
generalize loop_pre_log_satisfies_hinv; eauto.
Qed.
Lemma CalMCS_RelWaitAuxPre_satisfies_hinv:
∀ cur_index m0,
CalMCS_RelWaitAuxPre cur_index (CPU_ID adt) pre_log
(ZMap.get lock_index (multi_oracle adt)) =
Some m0 →
high_level_invariant
adt {multi_log
: ZMap.set lock_index (MultiDef m0)
(multi_log adt)}.
Proof.
generalize loop_CalMCS_RelWaitAuxPre_satisfies_hinv; eauto.
Qed.
Lemma pass_lock_loop_correct_aux:
LoopProofSimpleWhile.t
f_mcs_pass_lock_while_condition
f_mcs_pass_lock_while_body
ge (PTree.empty _)
pass_lock_loop_body_P
pass_lock_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 new_next d´,
le ! _lock_index = Some (Vint (Int.repr lock_index)) ∧
le ! _cpuid = Some (Vint (Int.repr (CPU_ID adt))) ∧
le ! _current_next = Some (Vint (Int.repr new_next)) ∧
le ! _null_var = Some (Vint (Int.repr NULL)) ∧
get_current_next d´ = Some new_next ∧
(( i = O ∧ new_next = NULL ∧
d´ = adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}) ∨
(((0 < i < K)%nat ∧ new_next = NULL ∨ i = K ∧ new_next ≠ NULL) ∧
Calculate_MCSPassLock i = Some d´)) ∧
w = Z.of_nat K - Z.of_nat i ∧
m = (minit, d´)
).
- apply Zwf_well_founded.
- intros le m Hp.
destruct Hp as (Hle1 & Hle2 & Hle3 & Hle4 & Hc_next & Hm).
∃ (Z.of_nat K), O, NULL.
∃ (adt {multi_log: ZMap.set lock_index (MultiDef pre_log) (multi_log adt)}).
rewrite init_current_next in Hle3.
repeat vcgen.
+ rewrite <- Nat2Z.inj_sub.
rewrite NPeano.Nat.sub_0_r.
reflexivity.
omega.
- intros le m n Hp.
destruct Hp as (cur_index & new_next & new_d &
Hle1 & Hle2 & Hle3 & Hle4 & Hc_next & Hcond & Hw & Hm).
Caseeq Hcond.
+
intros (ival & new & nd); subst.
unfold get_current_next in Hc_next; simpl in Hc_next.
subdestruct.
inversion Hc_next.
rewrite H0 in ×.
esplit; esplit.
repeat vcgen; try (subst; repeat vcgen; fail); subst.
× unfold Int.eq in H.
unfold Int.one, Int.zero in H.
rewrite Int.unsigned_repr in H; try omega.
rewrite Int.unsigned_repr in H; try omega.
simpl in H; inv H.
× assert (tmp: ∃ mcs,
CalMCSLock (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) pre_log ++ pre_log) = Some mcs).
{ assert (kneq0: K ≠ O) by omega.
apply NPeano.Nat.succ_pred in kneq0.
rewrite <- kneq0 in Klast.
simpl in Klast.
subdestruct; esplit; rewrite Hdestruct1; reflexivity. }
destruct tmp as (mcs´, tmp).
assert (tmp´: CalMCSLock
(ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) pre_log ++ pre_log) = Some mcs´).
{ simpl in tmp; subdestruct; try (inv tmp; fail).
assumption. }
assert (tmp_next: ∃ tmp_next,
get_current_next (adt {multi_log:
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) pre_log ++ pre_log))
(multi_log adt)}) = Some tmp_next).
{ unfold get_current_next.
simpl.
rewrite ZMap.gss.
rewrite tmp.
destruct mcs´.
∃ (snd (ZMap.get (CPU_ID adt) lock_array0)).
destruct (ZMap.get (CPU_ID adt) lock_array0).
simpl; reflexivity. }
destruct tmp_next as (tmp_next, tmp_next_prop).
esplit; esplit; repeat vcgen.
{ unfold mcs_get_next_spec; subst.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite iikern, iihost.
rewrite zle_lt_true; try eauto.
rewrite zle_lt_true; try eauto.
simpl; rewrite ZMap.gss.
rewrite tmp´.
instantiate (1:= (Int.repr tmp_next)).
assert (0 ≤ tmp_next < TOTAL_CPU ∨ tmp_next = NULL).
{ assert (0 ≤ tmp_next ≤ TOTAL_CPU).
{ unfold get_current_next in tmp_next_prop.
subdestruct.
generalize pre_log_satisfies_hinv; intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= pre_log) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID adt)) in lock_index_range´; eauto.
subdestruct.
inv Hdestruct6; eauto.
destruct mcs´.
inv tmp.
clear tmp´.
inv tmp_next_prop.
rewrite ZMap.gss in Hdestruct1; eauto.
inv Hdestruct1.
simpl in Hdestruct3.
subdestruct.
inv Hdestruct3.
inv Hdestruct4.
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H1 in CPU_ID_range.
rewrite Hdestruct5 in CPU_ID_range; simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL; omega. }
rewrite Int.unsigned_repr; [ | rewrite max_unsigned_val; unfold NULL in H0; destruct H0; omega].
destruct mcs´.
unfold get_current_next in tmp_next_prop; subdestruct.
simpl in Hdestruct1.
rewrite ZMap.gss in Hdestruct1.
inv Hdestruct1.
rewrite tmp in Hdestruct3.
inv Hdestruct3.
inv tmp_next_prop.
rewrite Hdestruct5.
repeat vcgen. }
{ rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega. }
{
∃ (Z.of_nat K - 1).
repeat vcgen.
∃ 1%nat.
esplit.
rewrite multi_log_double_update.
esplit; repeat vcgen.
- right.
assert (Kcase: (1 = K ∨ 1 < K)%nat) by omega.
Caseeq Kcase; intros.
+
rewrite <- H0.
split; [right | ].
× split; auto.
rewrite <- H0 in Klast.
simpl in Klast.
subdestruct; subst.
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct3.
rewrite ZMap.gss in Hdestruct3.
inv Hdestruct3.
inv Klast.
simpl in Hdestruct6.
subdestruct; try (inv Hdestruct6; fail); subst.
rewrite Hdestruct1 in Hdestruct6.
inv tmp_next_prop.
inv Hdestruct6.
inv tmp.
rewrite Hdestruct8 in Hdestruct4.
inv Hdestruct4.
auto.
× unfold Calculate_MCSPassLock; subst.
simpl in Klast.
subdestruct; subst.
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct3.
rewrite ZMap.gss in Hdestruct3.
inv Hdestruct3.
inv Klast.
simpl in Hdestruct6.
subdestruct; try (inv Hdestruct6; fail); subst.
rewrite Hdestruct1 in Hdestruct6.
inv tmp_next_prop.
inv Hdestruct6.
inv tmp.
rewrite Hdestruct8 in Hdestruct4.
inv Hdestruct4.
inv Hdestruct1.
rewrite Hdestruct8.
rewrite Hdestruct5.
reflexivity.
+
split.
× left.
split; try omega.
assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply Kpre in onerange.
simpl in onerange.
subdestruct.
unfold get_current_next in tmp_next_prop; subdestruct.
subst.
inv tmp_next_prop.
simpl in Hdestruct6.
rewrite ZMap.gss in Hdestruct6.
inv Hdestruct6.
simpl in Hdestruct7.
subdestruct; try (inv Hdestruct7; fail).
inversion Hdestruct7.
inv tmp´.
inv Hdestruct1.
rewrite Hdestruct9 in Hdestruct4.
inv Hdestruct4.
reflexivity.
× assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply Kpre in onerange.
simpl in onerange.
subdestruct.
unfold get_current_next in tmp_next_prop; subdestruct.
subst.
inv tmp_next_prop.
simpl in Hdestruct6.
rewrite ZMap.gss in Hdestruct6.
inv Hdestruct6.
simpl in Hdestruct7.
subdestruct; try (inv Hdestruct7; fail).
inversion Hdestruct7.
inv tmp´.
inv Hdestruct1.
rewrite Hdestruct9 in Hdestruct4.
inv Hdestruct4.
unfold Calculate_MCSPassLock; subst.
simpl.
simpl in tmp.
subdestruct; try (inv tmp; fail); subst.
inv tmp.
rewrite Hdestruct9.
simpl.
reflexivity.
- rewrite ZMap.set2.
reflexivity. }
+ intro tmp; destruct tmp as [icond Hcalc].
Caseeq icond.
×
intros (irange & neq).
unfold Calculate_MCSPassLock in Hcalc.
subdestruct.
inv Hcalc.
assert (tmp: ∃ mlock,
CalMCSLock (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)::(ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) m0 ++ m0) = Some mlock).
{ eapply CalMCS_RelWaitAuxToPre in Klast.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
eapply CalMCS_RelWaitAuxPreInv in H0; eauto.
- destruct H0.
destruct H0.
rewrite Hdestruct in H0.
inv H0.
simpl in H1.
subdestruct; rewrite Hdestruct0; esplit; reflexivity.
- intros.
eapply Kpre; eauto.
omega. }
destruct tmp as (mcs´, tmp).
assert (tmp´: CalMCSLock (ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) m0 ++ m0) = Some mcs´).
{ simpl in tmp; subdestruct; try (inv tmp; fail).
assumption. }
assert (tmp_next: ∃ tmp_next,
get_current_next (adt {multi_log:
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) m0 ++ m0))
(multi_log adt)}) = Some tmp_next).
{ unfold get_current_next.
simpl.
rewrite ZMap.gss.
rewrite tmp.
destruct mcs´.
∃ (snd (ZMap.get (CPU_ID adt) lock_array)).
destruct (ZMap.get (CPU_ID adt) lock_array).
simpl; reflexivity. }
destruct tmp_next as (tmp_next, tmp_next_prop).
esplit; esplit; repeat vcgen.
{ unfold Int.eq in H.
unfold Int.one, Int.zero in H.
rewrite Int.unsigned_repr in H; try omega.
rewrite Int.unsigned_repr in H; try omega.
simpl in H; inv H. }
{ esplit; esplit.
repeat vcgen.
- unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite iikern, iihost.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl; rewrite ZMap.gss.
rewrite tmp´.
instantiate (1:= (Int.repr tmp_next)).
assert (0 ≤ tmp_next < TOTAL_CPU ∨ tmp_next = NULL).
{ assert (0 ≤ tmp_next ≤ TOTAL_CPU).
{ unfold get_current_next in tmp_next_prop.
subdestruct.
generalize (CalMCS_RelWaitAuxPre_satisfies_hinv cur_index m0 Hdestruct); intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= m0) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID adt)) in lock_index_range´; eauto.
subdestruct.
inv Hdestruct4; eauto.
destruct mcs´.
inv tmp.
clear tmp´.
inv tmp_next_prop.
rewrite ZMap.gss in Hdestruct0; eauto.
inv Hdestruct0.
simpl in Hdestruct1.
subdestruct.
inv Hdestruct1.
inv Hdestruct2.
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct0; eauto.
destruct Hdestruct0.
eapply H1 in CPU_ID_range.
rewrite Hdestruct3 in CPU_ID_range; simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL; omega. }
rewrite Int.unsigned_repr; [ | rewrite max_unsigned_val; unfold NULL in H0; destruct H0; omega].
destruct mcs´.
unfold get_current_next in tmp_next_prop; subdestruct.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite tmp in Hdestruct1.
inv Hdestruct1.
inv tmp_next_prop.
rewrite Hdestruct3.
repeat vcgen.
- rewrite max_unsigned_val; rewrite lock_range_val in lock_index_range; omega.
-
∃ (Z.of_nat K - Z.of_nat cur_index - 1).
repeat vcgen.
esplit; esplit; esplit.
repeat vcgen.
+ instantiate (1:= (S cur_index)).
right.
split.
× assert (icase: (S cur_index = K ∨ S cur_index < K)%nat) by omega.
Caseeq icase; intros.
{ right; split; auto.
assert((K ≤ K)%nat) by omega.
eapply Klastpre in H1.
rewrite <- H0 in H1.
assert (CalMCSLock l1 = Some mcs´).
{ eapply CalMCS_RelWaitAuxPreInv in H1; eauto.
- destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
+ inv H2.
simpl.
rewrite Hdestruct0.
eauto.
+ inv H2.
simpl.
rewrite Hdestruct0.
eauto.
- intros.
eapply Kpre; eauto.
omega. }
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite Hdestruct1 in tmp.
inv tmp.
inv tmp_next_prop.
eapply CalMCS_RelWaitAuxEq with (1:= Klast) (2:= H2); try eauto. }
{ left.
split; try omega.
assert ((0 ≤ S cur_index < K)%nat) by omega.
eapply Kpre in H1.
eapply CalMCS_RelWaitAuxToPre in Klast; eauto.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
assert (CalMCSLock x = Some mcs´).
{ eapply CalMCS_RelWaitAuxPreInv in H3; eauto.
- destruct H3.
destruct H3.
rewrite Hdestruct in H3.
inv H3.
simpl in H4.
subdestruct.
+ inv H4.
simpl.
rewrite Hdestruct0.
eauto.
+ inv H4.
simpl.
rewrite Hdestruct0.
eauto.
- intros.
eapply Kpre; eauto.
omega. }
unfold get_current_next in tmp_next_prop.
subdestruct; subst.
simpl in Hdestruct0.
rewrite ZMap.gss in Hdestruct0.
inv Hdestruct0.
rewrite Hdestruct1 in tmp.
inv tmp.
inv tmp_next_prop.
eapply CalMCS_RelWaitAuxPreNeq; try eauto.
omega. }
× unfold Calculate_MCSPassLock.
eapply CalMCS_RelWaitAuxToPre in Klast; eauto.
assert ((S cur_index ≤ K)%nat) by omega.
eapply CalMCS_RelWaitAuxToPreCons in Klast; eauto.
destruct Klast.
rewrite H1.
eapply CalMCS_RelWaitAuxPreInv in H1; eauto.
{ destruct H1; destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
- inv H2.
reflexivity.
- inv H2.
reflexivity. }
{ intros.
eapply Kpre; eauto.
omega. }
+ rewrite Nat2Z.inj_succ.
unfold Z.succ.
omega.
+ rewrite ZMap.set2.
reflexivity. }
×
intros.
destruct H as (ci_val & cn_val).
assert (0 ≤ new_next < TOTAL_CPU).
{ unfold Calculate_MCSPassLock in Hcalc.
subdestruct.
inv Hcalc.
unfold get_current_next in Hc_next.
subdestruct.
inv Hc_next.
generalize (CalMCS_RelWaitAuxPre_satisfies_hinv K m0 Hdestruct); intros hinv´.
inv hinv´; simpl in ×.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv with (q:= m0) in lock_index_range´;
try (rewrite ZMap.gss; eauto; fail).
unfold valid_MCS_log in lock_index_range´.
unfold MCSCorrect_range in lock_index_range´.
rewrite ZMap.gss in Hdestruct0; eauto; inv Hdestruct0.
unfold MCSCorrect_range in lock_index_range´.
eapply lock_index_range´ in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H0 in CPU_ID_range.
rewrite Hdestruct3 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in cn_val.
omega. }
unfold NULL in ×.
esplit; esplit; repeat vcgen.
{ unfold pass_lock_loop_body_Q.
∃ new_d.
esplit.
repeat vcgen.
assert ((S K ≤ cal_time)%nat) by omega.
assert ((K ≤ (pred cal_time))%nat) by omega.
unfold Calculate_MCSPassLock in ×.
assert ((K ≤ K)%nat) by omega.
erewrite Klastpre in Hcalc; eauto; try omega.
erewrite Klastpre; eauto. }
Qed.
End mcs_pass_lock_loop_proof.
Lemma mcs_pass_lock_body_correct:
∀ m d d´ env le index ofs,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint index) →
PTree.get _offset le = Some (Vint ofs) →
kernel_mode d →
high_level_invariant d →
mcs_pass_lock_spec (Int.unsigned index) (Int.unsigned ofs) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_pass_lock_body E0 le´ (m, d´) (Out_return None).
Proof.
intros.
generalize max_unsigned_val; intros muval.
generalize lock_AT_start_val; intros lat_val.
generalize ID_AT_range_val; intros iar_val.
generalize lock_TCB_start_val; intros lts_val.
generalize ID_TCB_range_val; intros itr_val.
generalize num_chan_val; intros nc_val.
generalize lock_TCB_range_val; intros ltr_val.
generalize lock_SC_start_val; intros lss_val.
generalize lock_range_val; intros lr_val.
generalize t_struct_mcs_lock_size; intros t_st_ml_size.
generalize t_struct_mcs_node_size; intros t_st_mn_size.
unfold f_mcs_pass_lock_body; subst.
unfold mcs_pass_lock_spec in H4.
destruct H2 as (H2a & H2b).
rewrite H2a, H2b in H4.
remember (index2Z (Int.unsigned index) (Int.unsigned ofs)) as lock_index.
destruct lock_index; try (inv H4; fail).
Opaque Z.add Z.mul.
assert (lock_index_range: 0 ≤ z < lock_range).
{ clearAllExceptTwo Heqlock_index lock_range_val.
assert (lock_id_val: (Int.unsigned index) = ID_AT ∨
(Int.unsigned index) = ID_TCB ∨
(Int.unsigned index) = ID_SC).
{ unfold index2Z in Heqlock_index.
unfold index_range in ×.
destruct (Int.unsigned index); try tauto; try (inversion Heqlock_index; fail).
destruct p; try tauto; try (inversion Heqlock_index; fail).
destruct p; try tauto; try (inversion Heqlock_index). }
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]];
rewrite lock_id_val in Heqlock_index; unfold index2Z in Heqlock_index; simpl in *; subdestruct;
inv Heqlock_index; rewrite lock_range_val.
- unfold ID_AT_range in *; omega.
- unfold ID_TCB_range, ID_AT_range in *; omega.
- unfold lock_TCB_range, ID_SC_range, ID_AT_range, ID_TCB_range in *; omega. }
symmetry in Heqlock_index.
assert (cid_range: 0 ≤ (CPU_ID d) < TOTAL_CPU).
{ inv H3; omega. }
Transparent Z.add Z.mul.
Opaque CalMCSLock CalMCS_RelWait.
subdestruct.
- esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct; subst.
rewrite Hdestruct0.
rewrite zeq_true; eauto.
instantiate (1:= Int.one).
reflexivity. }
{
rewrite <- repr_one.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
simpl; repeat vcgen.
inv H4.
instantiate
(1:=
(PTree.set _cas_res (Vint Int.one)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))).
repeat vcgen. }
-
generalize Hdestruct3.
intro CalMCS_RelWait_Prop.
apply CalMCS_RelWait_implies_CalMCS_RelWaitAux in Hdestruct3.
destruct Hdestruct3 as (l´´, (Hdestruct3, (Hdestruct9, get_current_next_property))).
unfold CalPassLockTime in ×.
assert ((CalPassLockLoopTime > 0)%nat).
{ assert ((CalPassLockLoopTime ≠ 0)%nat).
intro.
rewrite H in Hdestruct3; simpl in Hdestruct3.
inv Hdestruct3.
omega. }
Opaque CalPassLockLoopTime.
rewrite <- NPeano.Nat.succ_pred_pos with (n:= CalPassLockLoopTime) in Hdestruct3 by omega.
simpl in Hdestruct3.
Transparent CalMCS_RelWaitAux.
simpl in Hdestruct3.
subdestruct; subst.
+
inv H4.
unfold NULL in ×.
Transparent CalMCSLock.
simpl in Hdestruct3.
generalize Hdestruct3; intro HcalcWait.
generalize HcalcWait; intro Hcalctmp.
eapply CalMCS_RelWaitAuxToPre in HcalcWait; eauto.
eapply CalMCS_RelWaitAuxStops in Hdestruct3; eauto.
destruct Hdestruct3 as [K [Krange [KPre [KPost KPostPre]]]].
assert (Kgt0: (0 < K)%nat).
{ assert (K = O → False).
intro.
subst.
inv KPost.
omega. }
assert (Krangelt: (0 < K < CalPassLockLoopTime)%nat) by omega.
remember NULL as current_next.
fold NULL in Hdestruct7.
rewrite <- Heqcurrent_next in Hdestruct7.
assert (gc_next :
get_current_next d z
(d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})
= Some NULL).
{ unfold get_current_next; simpl.
rewrite ZMap.gss.
rewrite Hdestruct5.
rewrite Hdestruct7.
f_equal; assumption. }
generalize (pass_lock_loop_correct_aux m _ K CalPassLockLoopTime _ _ z current_next
H2b H2a H3
cid_range lock_index_range Krangelt
Hdestruct Heqcurrent_next Hcalctmp KPre KPost KPostPre gc_next).
intros LP.
eapply LoopProofSimpleWhile.termination
with (condition := f_mcs_pass_lock_while_condition)
(body := f_mcs_pass_lock_while_body)
(P := pass_lock_loop_body_P m d l z current_next)
(Q := pass_lock_loop_body_Q m d CalPassLockLoopTime l z)
(le0 := (PTree.set
_current_next (Vint (Int.repr TOTAL_CPU))
(PTree.set
_null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set
_cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le))))))
(m0 := (m, (d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})))
in LP.
destruct LP as (while_le´, (while_m´, (LP1 & LP2))).
unfold pass_lock_loop_body_Q in LP2.
destruct LP2 as (while_d´, (while_new´, LP2)).
×
esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct.
rewrite Hdestruct0.
rewrite Hdestruct2.
instantiate (1:= Int.zero).
reflexivity. }
{
rewrite <- repr_zero.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
change E0 with (E0 ** E0).
econstructor; [repeat vcgen | ].
change E0 with (E0 ** E0).
econstructor.
-
repeat vcgen.
unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite multi_log_double_update.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
inv Hdestruct3; inv Hdestruct5.
rewrite Hdestruct7.
instantiate (1:= Int.repr TOTAL_CPU).
rewrite Int.unsigned_repr; [ | omega ].
repeat vcgen.
- change E0 with (E0 ** E0).
unfold set_opttemp.
econstructor.
+
eassumption.
+
idtac.
destruct LP2 as (LP21 & LP22 & LP23 & LP24 & LP25 & LP26 & LP27 & LP28).
instantiate (1:= while_le´).
inv LP28; subst.
repeat vcgen.
unfold mcs_set_busy_spec.
unfold Calculate_MCSPassLock in LP27.
rewrite HcalcWait in LP27.
inv LP27.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
simpl in Hdestruct4.
subdestruct; try (inv Hdestruct4; fail).
assert (0 ≤ z0 < TOTAL_CPU).
{ assert (high_level_invariant (d {multi_log: ZMap.set z (MultiDef l´´) (multi_log d)}))
by eauto using loop_CalMCS_RelWaitAuxPre_satisfies_hinv.
inv H2.
simpl in CPU_ID_range, valid_curid, valid_multi_log_pool_mcs_inv, valid_multi_oracle_pool_mcs_inv.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l´´).
{ eapply valid_multi_log_pool_mcs_inv in lock_index_range; eauto.
rewrite ZMap.gss; auto. }
eapply valid_multi_oracle_pool_mcs_inv with (i0 := CPU_ID d) in H2; eauto.
unfold valid_MCS_log in H2.
unfold MCSCorrect_range in H2.
generalize Hdestruct1; intro prop.
eapply H2 in prop; eauto.
destruct prop.
eapply H5 in CPU_ID_range.
rewrite Hdestruct6 in CPU_ID_range.
simpl in CPU_ID_range.
unfold get_current_next_prop in get_current_next_property.
unfold get_current_next_value in get_current_next_property.
subdestruct; subst.
- contradiction.
- inv Hdestruct1.
rewrite Hdestruct6 in Hdestruct11.
inv Hdestruct11.
unfold NULL in n0.
clearAllExceptTwo n0 CPU_ID_range.
omega. }
rewrite zle_lt_true; try omega.
reflexivity. }
× unfold pass_lock_loop_body_P.
rewrite Heqcurrent_next; subst.
unfold NULL in ×.
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; auto.
+
inv H4; subst; inv Hdestruct4; subst.
esplit; repeat vcgen.
{
unfold mcs_lock_get_index_spec.
instantiate (1:= Int.repr z).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b, Heqlock_index.
reflexivity. }
{
unfold get_CPU_ID_spec.
instantiate (1:= Int.repr (CPU_ID d)).
rewrite Int.unsigned_repr; try omega.
rewrite H2a, H2b.
reflexivity. }
{
unfold mcs_cas_tail_spec.
rewrite H2a, H2b.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Int.unsigned_repr; try omega.
rewrite zle_lt_true; try omega.
rewrite Hdestruct.
rewrite Hdestruct0.
rewrite Hdestruct2.
instantiate (1:= Int.zero).
reflexivity. }
{
rewrite <- repr_zero.
rewrite Int.unsigned_repr; try omega.
repeat vcgen. }
{
change E0 with (E0 ** E0).
econstructor; [repeat vcgen | ].
change E0 with (E0 ** E0).
econstructor.
-
repeat vcgen.
unfold mcs_get_next_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite ZMap.set2.
rewrite multi_log_double_update.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
inv Hdestruct3; inv Hdestruct5.
rewrite Hdestruct7.
instantiate (1:= Int.repr z0).
assert (0 ≤ z0 < TOTAL_CPU).
{ remember (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intros tmp_prop.
eapply loop_pre_log_term_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv in Hdestruct10; eauto; [ | rewrite ZMap.gss; auto].
destruct Hdestruct10.
apply H5 in CPU_ID_range.
rewrite Hdestruct7 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in n0.
omega. }
repeat vcgen.
- change E0 with (E0 ** E0).
unfold set_opttemp.
assert (0 ≤ z0 < TOTAL_CPU).
{ remember (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intros tmp_prop.
eapply loop_pre_log_term_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_MCS_log in valid_multi_log_pool_mcs_inv.
unfold MCSCorrect_range in valid_multi_log_pool_mcs_inv.
simpl in Hdestruct5.
subdestruct.
inv Hdestruct3.
inv Hdestruct5.
eapply valid_multi_log_pool_mcs_inv in Hdestruct1; eauto; [ | rewrite ZMap.gss; auto].
destruct Hdestruct1.
apply H5 in CPU_ID_range.
rewrite Hdestruct7 in CPU_ID_range.
simpl in CPU_ID_range.
unfold NULL in n0; omega. }
instantiate (1:= (PTree.set _current_next (Vint (Int.repr z0))
(PTree.set _null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set _cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))))).
econstructor.
+
unfold f_mcs_pass_lock_while_condition, f_mcs_pass_lock_while_body.
instantiate (2:= (PTree.set
_current_next (Vint (Int.repr z0))
(PTree.set _null_var (Vint (Int.repr TOTAL_CPU))
(PTree.set _cas_res (Vint Int.zero)
(PTree.set _cpuid (Vint (Int.repr (CPU_ID d)))
(PTree.set _lock_index (Vint (Int.repr z)) le)))))).
unfold NULL in ×.
eapply ClightBigstep.exec_Sloop_stop1.
eapply exec_Sseq_2.
repeat vcgen.
{ intros contra.
inv contra. }
{ econstructor. }
+
repeat vcgen.
unfold mcs_set_busy_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H2a, H2b.
rewrite zle_lt_true; try omega.
rewrite zle_lt_true; try omega.
simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
simpl in Hdestruct5.
subdestruct; try (inv Hdestruct5; fail).
assert (0 ≤ z1 < TOTAL_CPU).
{ subst.
inv Hdestruct3.
assert (z1 ≠ NULL).
{ set (pre_log := (ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
fold pre_log in CalMCS_RelWait_Prop.
fold pre_log in Hdestruct1.
fold pre_log in get_current_next_property.
unfold get_current_next_prop in get_current_next_property.
unfold get_current_next_value in get_current_next_property.
rewrite Hdestruct1 in get_current_next_property.
rewrite Hdestruct6 in get_current_next_property.
subdestruct; try contradiction; try auto. }
assert (0 ≤ z1 ≤ TOTAL_CPU).
{ remember (TEVENT (CPU_ID d) (TTICKET GET_NEXT)::ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) ++
TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l) as pre_log.
generalize Heqpre_log; intro tmp_prop.
eapply loop_pre_log_satisfies_hinv in tmp_prop; eauto.
inv tmp_prop; simpl in ×.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_index_range; intro lock_index_range´.
eapply valid_multi_log_pool_mcs_inv in lock_index_range; eauto; [ | rewrite ZMap.gss; reflexivity].
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i0 := (CPU_ID d)) in lock_index_range; eauto.
unfold valid_MCS_log in lock_index_range.
unfold MCSCorrect_range in lock_index_range.
eapply lock_index_range in Hdestruct1; eauto.
destruct Hdestruct1.
eapply H7 in CPU_ID_range.
rewrite Hdestruct6 in CPU_ID_range.
simpl in CPU_ID_range.
exact CPU_ID_range. }
unfold NULL in H5.
omega. }
rewrite zle_lt_true; try omega.
reflexivity. }
Qed.
End MCSPASSLOCKBODY.
Theorem mcs_pass_lock_code_correct:
spec_le (pass_lock ↦ mcs_pass_lock_spec_low) (〚pass_lock ↦ f_mcs_pass_lock 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (mcs_pass_lock_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_pass_lock)
(Vint i::Vint ofs::nil)
(create_undef_temps (fn_temps f_mcs_pass_lock)))) muval.
Qed.
End MCSPASSLOCK.
End WithPrimitives.
End MMCSLOCKABSINTROCODEMCSPASSLOCK.