Library mcertikos.ticketlog.MTicketLockIntroCode
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 TicketLockOpGenSpec.
Require Import MTicketLockIntroCSource.
Require Import MTicketLockIntro.
Require Import CalTicketLock.
Require Import AbstractDataType.
Module MTICKETLOCKINTRO.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{fairness: 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}.
Opaque PTree.get PTree.set.
Local Open Scope Z_scope.
Section PASSLOCK.
Let L: compatlayer (cdata RData) := incr_now ↦ gensem incr_now_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PassLockBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bincr_now: block.
Hypothesis hincr_now1 : Genv.find_symbol ge incr_now = Some bincr_now.
Hypothesis hincr_now2 :
Genv.find_funct_ptr ge bincr_now =
Some (External (EF_external incr_now
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma pass_lock_body_correct: ∀ m d d´ env le lock_id offset,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
ikern d = true →
ihost d = true →
incr_now_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_pass_lock_body E0 le´ ((m, d´): mem) Out_normal.
Proof.
intros.
subst.
esplit.
unfold f_pass_lock_body.
repeat vcgen.
Qed.
End PassLockBody.
Theorem pass_lock_code_correct:
spec_le (pass_lock ↦ pass_lock_spec_low) (〚pass_lock ↦ f_pass_lock 〛L).
Proof.
fbigstep_pre L.
destruct H0.
generalize hinv; intro.
inv hinv.
fbigstep (pass_lock_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´
(fn_params f_pass_lock) (Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_pass_lock)))) valid_curid.
Qed.
End PASSLOCK.
Section WAITLOCK.
Let L: compatlayer (cdata RData) := incr_ticket ↦ gensem incr_ticket_spec
⊕ get_now ↦ gensem get_now_spec
⊕ log_hold ↦ gensem log_hold_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section WaitLockBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bincr_ticket: block.
Hypothesis hincr_ticket1 : Genv.find_symbol ge incr_ticket = Some bincr_ticket.
Hypothesis hincr_ticket2 :
Genv.find_funct_ptr ge bincr_ticket =
Some (External (EF_external incr_ticket
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Variable bget_now: block.
Hypothesis hget_now1 : Genv.find_symbol ge get_now = Some bget_now.
Hypothesis hget_now2 :
Genv.find_funct_ptr ge bget_now =
Some (External (EF_external get_now
(signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable blog_hold: block.
Hypothesis hlog_hold1 : Genv.find_symbol ge log_hold = Some blog_hold.
Hypothesis hlog_hold2 :
Genv.find_funct_ptr ge blog_hold =
Some (External (EF_external log_hold
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
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.
Fixpoint CalTicketWaitWraparoundPre (n: nat) (i t: Z) (l: MultiLog) (to: MultiOracle):=
match n with
| O ⇒ Some l
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
match CalTicketLockWraparound l´ with
| Some (_, n0, _) ⇒
if zeq t n0 then Some l´
else
CalTicketWaitWraparoundPre n´ i t l´ to
| _ ⇒ None
end
end.
Transparent CalTicketWaitWraparound.
Lemma CalTicketWaitWraparoundStops:
∀ m i t l to l´,
CalTicketWaitWraparound m i t l to = Some l´ →
∃ k,
(k ≤ m)%nat ∧
(∀ n,
(0 ≤ n < k)%nat → CalTicketWaitWraparound n i t l to = None) ∧
CalTicketWaitWraparound k i t l to = Some l´ ∧
∀ j, (k ≤ j)%nat → CalTicketWaitWraparoundPre j i t l to = Some l´.
Proof.
induction m; simpl; intros; [inv H |].
subdestruct.
- subst.
inv H.
∃ 1%nat.
split; [omega | ].
split; intros.
+ assert(n = O) by omega; subst.
reflexivity.
+ simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
split.
× reflexivity.
× intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H0.
rewrite <- H0.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
- eapply IHm in H; eauto.
destruct H.
destruct H.
destruct H0.
destruct H1.
∃ (S x).
split; [omega |].
split.
+ intros.
assert(n0case: n0 = O ∨ n0 ≠ O) by omega.
Caseeq n0case; intros.
subst.
reflexivity.
eapply NPeano.Nat.succ_pred in H4.
rewrite <- H4.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
eapply H0; eauto.
omega.
+ simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
split.
apply H1.
intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H4.
rewrite <- H4.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
eapply H2; eauto.
omega.
Qed.
Lemma CalTicketWaitWraparoundToPre:
∀ m i t l to l´,
CalTicketWaitWraparound m i t l to = Some l´ →
CalTicketWaitWraparoundPre m i t l to = Some l´.
Proof.
induction m; simpl; intros; [inv H |].
simpl.
intros.
subdestruct.
apply H.
eapply IHm; eauto.
Qed.
Lemma CalTicketWaitWraparoundToPreCons:
∀ m m´ i t l to l´,
CalTicketWaitWraparoundPre m i t l to = Some l´ →
(m´ ≤ m)%nat →
∃ l´´,
CalTicketWaitWraparoundPre m´ i t l to = Some l´´.
Proof.
induction m.
- simpl.
intros.
assert(m´ = O) by omega.
subst.
esplit.
reflexivity.
- simpl.
intros.
subdestruct.
+ 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, Hdestruct2.
esplit.
reflexivity.
+ 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, Hdestruct2.
eapply IHm; eauto.
omega.
Qed.
Lemma CalTicketWaitWraparoundPreInv: ∀ m i t l to l´,
CalTicketWaitWraparoundPre (S m) i t l to = Some l´ →
(∀ j, (j < (S m))%nat → CalTicketWaitWraparound j i t l to = None) →
∃ l´´,
CalTicketWaitWraparoundPre m i t l to = Some l´´ ∧
CalTicketWaitWraparoundPre 1 i t l´´ to = Some l´.
Proof.
induction m; simpl; intros.
- subdestruct.
+ inv H; esplit; split; [reflexivity | ].
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
+ inv H; esplit; split; [reflexivity | ].
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
- simpl in ×.
intros; subdestruct.
{ inv H.
assert ((1 < S (S m))%nat) by omega.
eapply H0 in H.
simpl in H.
rewrite Hdestruct in H.
rewrite Hdestruct2 in H.
inv H. }
{ inv H.
eapply IHm.
- rewrite Hdestruct3.
rewrite Hdestruct6.
reflexivity.
- intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H1.
simpl in H1.
rewrite Hdestruct in H1.
rewrite Hdestruct2 in H1.
apply H1. }
{ eapply IHm.
- rewrite Hdestruct3.
rewrite Hdestruct6.
apply H.
- intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H2.
simpl in H2.
rewrite Hdestruct in H2.
rewrite Hdestruct2 in H2.
apply H2. }
Qed.
Transparent CalTicketLockWraparound CalTicketWaitWraparound CalTicketWaitWraparoundPre.
Lemma CalTicketWaitWraparoundPreNeq: ∀ m i ticket l l´ to t n tl,
CalTicketWaitWraparound m i ticket l to = None →
CalTicketWaitWraparoundPre m i ticket l to = Some l´ →
(m > 0)%nat →
CalTicketLockWraparound l´ = Some (t, n, tl) →
n ≠ ticket.
Proof.
induction m; simpl; intros; try omega.
subdestruct; subst.
assert (mcase: m = O ∨ (m > O)%nat) by omega.
Caseeq mcase; intros; subst.
- simpl in ×.
inv H0.
simpl in H2.
rewrite Hdestruct in H2.
inv H2.
intros contra; elim n0; symmetry; auto.
- eapply IHm; eauto.
Qed.
Lemma CalTicketWaitWraparoundEq: ∀ m i t l to l´ t´ n´ tl,
CalTicketWaitWraparound m i t l to = Some l´ →
CalTicketLockWraparound l´ = Some (t´, n´, tl) →
n´ = t.
Proof.
induction m; simpl; intros; [inv H | ].
- subdestruct; subst.
+ inv H.
simpl in H0.
rewrite Hdestruct in H0.
inv H0.
auto.
+ eapply IHm; eauto.
Qed.
Section wait_lock_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable my_ticket : Z.
Variable init_now : Z.
Variable prev_ticket : Z.
Variable prev_now : Z.
Variable bound : int.
Variable cal_time: nat.
Variable tq_init: list nat.
Variable tq_prev: list nat.
Variable lock_id : int.
Variable offset : int.
Variable lock_index : Z.
Variable l : MultiLog.
Variable K: nat.
Variable l1: MultiLog.
Hypothesis init_neq: my_ticket ≠ prev_now.
Hypothesis index2zp: index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some lock_index.
Hypothesis initlist: (ZMap.get lock_index (multi_log adt)) = MultiDef l.
Hypothesis initlock: CalTicketLockWraparound
(ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) =
Some (my_ticket, init_now, tq_init).
Hypothesis lock_after_inc: CalTicketLockWraparound
(ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
= Some (prev_ticket, prev_now, tq_prev).
Hypothesis Krange: (0 < K < cal_time)%nat.
Hypothesis calcWait : CalTicketWaitWraparound (pred cal_time) (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (ZMap.get lock_index (multi_oracle adt)) =
Some l1.
Hypothesis KPre : ∀ n : nat,
(0 ≤ n < K)%nat →
CalTicketWaitWraparound n (CPU_ID adt) my_ticket (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
(ZMap.get lock_index (multi_oracle adt)) = None.
Hypothesis KPost : CalTicketWaitWraparound K (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW) :: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) (TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis KPostPre : ∀ j : nat,
(K ≤ j)%nat →
CalTicketWaitWraparoundPre j (CPU_ID adt) my_ticket (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt)(CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis iihost: ihost adt = true.
Hypothesis iikern: ikern adt = true.
Hypothesis my_ticket_range: 0 ≤ my_ticket ≤ Int.max_unsigned.
Hypothesis prev_now_range: 0 ≤ prev_now ≤ Int.max_unsigned.
Definition wait_lock_loop_body_P (le: temp_env) (m : mem): Prop :=
le ! _current_ticket = Some (Vint (Int.repr prev_now)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
m = (minit,
adt {multi_log
: ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l)) (multi_log adt)}).
Definition calculate_wait_lock (i: nat) :=
match CalTicketWaitWraparoundPre i (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (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_ticket (d: RData) :=
match ZMap.get lock_index (multi_log d) with
| MultiDef l´ ⇒
match CalTicketLockWraparound l´ with
| Some (_, n, _) ⇒ Some n
| _ ⇒ None
end
| _ ⇒ None
end.
Definition wait_lock_loop_body_Q (le: temp_env) (m : mem): Prop :=
∃ d,
le ! _current_ticket = Some (Vint (Int.repr my_ticket)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
calculate_wait_lock (pred cal_time) = Some d∧
m = (minit, d).
Lemma wait_lock_loop_correct_aux:
LoopProofSimpleWhile.t
f_wait_lock_while_condition
f_wait_lock_while_body
ge (PTree.empty _)
wait_lock_loop_body_P
wait_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_now d´,
le ! _current_ticket = Some (Vint (Int.repr new_now)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
(( i = O ∧ new_now ≠ my_ticket ∧
d´ = adt {multi_log :
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt)
(TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l)) (multi_log adt)}) ∨
(((0 < i < K)%nat ∧ new_now ≠ my_ticket∨
i = K ∧ new_now = my_ticket) ∧
calculate_wait_lock i = Some d´)) ∧
get_current_ticket d´ = Some new_now ∧
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 & Hle5 & Hm).
∃ (Z.of_nat K), O, prev_now.
esplit.
repeat vcgen.
unfold get_current_ticket; simpl.
rewrite ZMap.gss.
Transparent CalTicketLockWraparound.
simpl.
rewrite lock_after_inc.
rewrite Int.unsigned_repr by omega.
reflexivity.
Transparent CalTicketLockWraparound.
simpl.
omega.
- unfold f_wait_lock_while_condition, f_wait_lock_while_body.
intros le m w Hi.
destruct Hi as (i & new_ticket & newd & Hle1 & Hle2 & Hle3 & Hle4 & Hle5 & Hicond & Hcur & Hw & Hm).
Caseeq Hicond.
+
intros (ival & new & nd).
subst.
unfold get_current_ticket in Hcur; simpl in Hcur.
rewrite ZMap.gss in Hcur.
subdestruct.
inv Hcur.
assert (tmp: ∃ tmp_ticket tmp_now tmp_post,
CalTicketLockWraparound
(((ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
++ (TEVENT (CPU_ID adt) (TTICKET GET_NOW) :: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) (TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
= Some (tmp_ticket, tmp_now, tmp_post)).
{ assert(Kneq0: K ≠ O) by omega.
apply NPeano.Nat.succ_pred in Kneq0.
rewrite <- Kneq0 in KPost.
simpl in KPost.
subdestruct.
- ∃ z0, z1, l2; reflexivity.
- ∃ z0, z1, l2; reflexivity. }
destruct tmp as [tmp_ticket [tmp_now [tmp_post tmp_cal]]].
assert (0 ≤ new_ticket ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in Hdestruct.
omega.
}
assert (0 ≤ tmp_now ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in tmp_cal.
omega.
}
esplit; esplit.
repeat vcgen.
esplit; esplit.
repeat vcgen.
× unfold get_now_spec; simpl.
rewrite iihost, iikern, index2zp.
rewrite ZMap.gss.
rewrite tmp_cal.
rewrite ZMap.set2.
instantiate (1:= (Int.repr tmp_now)).
rewrite Int.unsigned_repr.
reflexivity.
omega.
×
∃ (Z.of_nat K - 1).
repeat vcgen.
∃ 1%nat.
esplit; esplit.
repeat vcgen.
{ right.
split.
assert (Kcase: (1 = K ∨ 1 < K)%nat) by omega.
Caseeq Kcase; intros.
{ rewrite <- H2.
right; split; [reflexivity | ].
rewrite <- H2 in KPost.
simpl in KPost.
subdestruct; subst.
inv tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity. }
{ left; split; try omega.
assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply KPre in onerange.
simpl in onerange.
subdestruct.
inv tmp_cal; eauto.
clear Hdestruct3.
rewrite Int.unsigned_repr in n by omega.
omega.
}
{ unfold calculate_wait_lock; simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
destruct (zeq my_ticket tmp_now); reflexivity. } }
{ unfold get_current_ticket; simpl.
rewrite ZMap.gss.
Transparent CalTicketLockWraparound.
simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity. }
+ intro tmp; destruct tmp as [icond Hcalc].
Caseeq icond.
×
intros (irange & neq).
unfold calculate_wait_lock in Hcalc; simpl in Hcalc.
subdestruct.
inv Hcalc.
assert (tmp: ∃ tmp_ticket tmp_now tq_tmp,
CalTicketLockWraparound ((ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) m0 ++ m0) = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
eapply CalTicketWaitWraparoundPreInv in H0; eauto.
- destruct H0.
destruct H0.
rewrite Hdestruct in H0.
inv H0.
simpl in H1.
subdestruct.
+ ∃ z, z0, l0; reflexivity.
+ ∃ z, z0, l0; reflexivity.
- intros.
eapply KPre; eauto.
omega. }
destruct tmp as [tmp_ticket [tmp_now [tq_tmp tmp_cal]]].
assert (tmp_now_range: 0 ≤ tmp_now ≤ Int.max_unsigned).
{
apply CalTicketLockWraparoundRange in tmp_cal.
destruct tmp_cal; auto.
}
assert (tmp_ticket_range: 0 ≤ tmp_ticket ≤ Int.max_unsigned).
{
apply CalTicketLockWraparoundRange in tmp_cal.
destruct tmp_cal; auto.
}
assert (new_ticket_range: 0 ≤ new_ticket ≤ Int.max_unsigned).
{
unfold get_current_ticket in Hcur.
simpl in Hcur.
rewrite ZMap.gss in Hcur.
subdestruct.
inv Hcur.
apply CalTicketLockWraparoundRange in Hdestruct0.
destruct Hdestruct0; auto.
}
esplit; esplit.
repeat vcgen.
esplit; esplit.
repeat vcgen.
{ unfold get_now_spec; simpl.
rewrite iihost, iikern, index2zp.
rewrite ZMap.gss.
rewrite tmp_cal.
instantiate (1:= (Int.repr tmp_now)).
rewrite Int.unsigned_repr.
reflexivity.
omega. }
{
∃ (Z.of_nat K - Z.of_nat i - 1).
repeat vcgen.
esplit; esplit; esplit.
repeat vcgen.
instantiate (1:= (S i)).
right.
split.
- assert (icase: (S i = K ∨ S i < K)%nat) by omega.
Caseeq icase; intros.
+ right.
split; auto.
assert((K ≤ K)%nat) by omega.
eapply KPostPre in H1.
rewrite <- H0 in H1.
assert (CalTicketLockWraparound l1 = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundPreInv in H1; eauto.
- destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
+ inv tmp_cal.
inv H2.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
+ inv tmp_cal.
inv H2.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
- intros.
eapply KPre; eauto.
omega. }
eapply CalTicketWaitWraparoundEq; eauto.
+ left.
split; try omega.
assert ((0 ≤ S i < K)%nat) by omega.
eapply KPre in H1.
eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
assert (CalTicketLockWraparound x = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundPreInv in H3; eauto.
- destruct H3.
destruct H3.
rewrite Hdestruct in H3.
inv H3.
simpl in H4.
subdestruct.
+ inv tmp_cal.
inv H4.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
+ inv tmp_cal.
inv H4.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
- intros.
eapply KPre; eauto.
omega. }
eapply CalTicketWaitWraparoundPreNeq in H3; eauto.
omega.
- unfold calculate_wait_lock.
eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
rewrite H1.
eapply CalTicketWaitWraparoundPreInv in H1; eauto.
+ destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
× inv tmp_cal.
inv H2.
rewrite ZMap.set2.
reflexivity.
× inv tmp_cal.
inv H2.
rewrite ZMap.set2.
reflexivity.
+ intros.
eapply KPre; eauto.
omega.
- unfold get_current_ticket; simpl.
rewrite ZMap.gss.
simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity.
- rewrite Nat2Z.inj_succ; unfold Z.succ.
omega. }
×
intros (ival & ticketseq).
subst.
esplit. esplit.
repeat vcgen.
unfold wait_lock_loop_body_Q.
∃ newd.
repeat (split; eauto).
assert ((K ≤ (pred cal_time))%nat) by omega.
unfold calculate_wait_lock in ×.
assert ((K ≤ K)%nat) by omega.
erewrite KPostPre in Hcalc; eauto.
erewrite KPostPre; eauto.
Qed.
End wait_lock_loop_proof.
Lemma wait_lock_body_correct: ∀ m d d´ env le bound lock_id offset,
env = PTree.empty _ →
PTree.get _bound le = Some (Vint bound) →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
ikern d = true →
ihost d = true →
high_level_invariant d →
wait_lock_spec_wraparound (Int.unsigned bound) (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_wait_lock_body E0 le´ ((m, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold f_wait_lock_body; subst.
unfold wait_lock_spec_wraparound in H6; subst.
rewrite H3, H4 in H6.
Opaque CalTicketLockWraparound CalWaitTime.
subdestruct; subst.
assert (cal_time_range: (CalWaitTime l0 > 0)%nat).
{ assert ((CalWaitTime l0 ≠ 0)%nat).
{ Transparent CalWaitTime.
intro.
unfold CalWaitTime in ×.
inv H. }
omega.
Opaque CalWaitTime. }
set (cal_time:= CalWaitTime l0).
fold cal_time in cal_time_range, Hdestruct4.
rewrite <- NPeano.Nat.succ_pred_pos with (n:= cal_time) in Hdestruct4 by omega.
remember z as lock_index; symmetry in Heqlock_index; subst.
remember z0 as t_prev; symmetry in Heqt_prev; subst.
remember z1 as n_prev; symmetry in Heqn_prev; subst.
remember l0 as tq_prev; symmetry in Heqtq_prev; subst.
assert (init_lock_st: ∃ t_init n_init tq_init,
CalTicketLockWraparound
((ZMap.get lock_index (multi_oracle d)) (CPU_ID d) l ++ l) = Some (t_init, n_init, tq_init)).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct1.
subdestruct; subst.
∃ z, z0, l0; reflexivity.
Opaque CalTicketLockWraparound. }
destruct init_lock_st as [t_init [n_init [tq_init init_lock_st]]].
assert (ticket_lock_vals:
Int.unsigned (Int.repr (t_init + 1)) = t_prev ∧ n_init = n_prev ∧ tq_init++((Z.to_nat (Int.unsigned bound))::nil) = tq_prev).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct1.
subdestruct; simpl; subst.
clear Hdestruct4 cal_time_range Hdestruct4 cal_time.
inv init_lock_st; inv Hdestruct1.
split. reflexivity.
rewrite Int.unsigned_repr.
tauto.
eapply CalTicketLockWraparoundRange; eauto.
Opaque CalTicketLockWraparound. }
destruct ticket_lock_vals as [? [? ?]].
symmetry in H; rewrite H in *; clear H.
symmetry in H7; rewrite H7 in *; clear H7.
symmetry in H8; rewrite H8 in *; clear H8.
simpl in Hdestruct4.
assert (0 ≤ t_init ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in init_lock_st;
destruct init_lock_st; auto.
}
subdestruct.
-
inv Hdestruct4; subst.
inv H6; subst.
esplit; repeat vcgen.
+
unfold incr_ticket_spec.
rewrite H3, H4, Hdestruct, Hdestruct0.
rewrite init_lock_st.
instantiate (1:= Int.repr t_init).
rewrite Int.unsigned_repr; try omega.
unfold ret; unfold option_monad_ops; repeat f_equal.
+
unfold get_now_spec.
simpl.
rewrite H3, H4, Hdestruct.
rewrite ZMap.gss.
rewrite Hdestruct2.
rewrite ZMap.set2.
assert (Int.unsigned (Int.repr (Int.unsigned (Int.repr (t_init + 1)) - 1)) = t_init).
{
assert(tcase: t_init = Int.max_unsigned ∨ t_init < Int.max_unsigned) by omega.
Caseeq tcase; intros.
rewrite H6.
Transparent Int.repr.
rewrite muval.
reflexivity.
Opaque Int.repr.
rewrite Int.unsigned_repr.
rewrite Int.unsigned_repr.
omega.
omega.
rewrite Int.unsigned_repr; omega.
}
rewrite H6.
instantiate (1:= Int.repr t_init).
rewrite Int.unsigned_repr by omega.
reflexivity.
+
rewrite multi_log_double_update; subst.
instantiate (2:=
(set_opttemp (Some 45%positive) (Vint (Int.repr t_init))
(set_opttemp (Some 44%positive) (Vint (Int.repr t_init)) le))).
unfold set_opttemp.
instantiate (1:=
d {multi_log
: ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}).
unfold f_wait_lock_while_condition, f_wait_lock_while_body.
eapply exec_Sloop_stop1.
eapply exec_Sseq_2.
repeat vcgen.
intro contra; inv contra.
econstructor.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ unfold log_hold_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H3, H4, Hdestruct; simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update; subst; simpl.
rewrite ZMap.set2.
unfold ret; unfold option_monad_ops; repeat f_equal.
-
inv H6; subst.
assert (0 ≤ z0 ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange; eauto.
}
assert (before_get_now: CalTicketLockWraparound (ZMap.get lock_index (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d) l ++ l) ++ TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) = Some (z, z0, l0)).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct2.
Opaque CalTicketLockWraparound.
subdestruct.
rewrite Int.unsigned_repr in Hdestruct2.
rewrite Int.unsigned_repr in Hdestruct2.
inv Hdestruct2; reflexivity.
eapply CalTicketLockWraparoundRange; eauto.
eapply CalTicketLockWraparoundRange in Hdestruct3; destruct Hdestruct3; eauto.
}
generalize Hdestruct4; intro HcalcWait.
generalize HcalcWait; intro Hcalctmp.
eapply CalTicketWaitWraparoundToPre in HcalcWait; eauto.
eapply CalTicketWaitWraparoundStops in Hdestruct4; eauto.
destruct Hdestruct4 as [K [Krange [KPre [KPost KPostPre]]]].
assert (Kgt0: (0 < K)%nat).
{ assert (K = O → False).
intro.
subst.
inv KPost.
omega. }
assert (Krangelt: (0 < K < cal_time)%nat) by omega.
set (my_ticket := t_init + 1 - 1).
fold my_ticket in Hcalctmp, HcalcWait, KPostPre, KPost, KPre, n, Hdestruct6.
assert (my_ticket_prop1: t_init + 1 = my_ticket + 1).
{ unfold my_ticket; ring. }
assert (my_ticket_prop2: t_init = my_ticket).
{ unfold my_ticket; ring. }
rewrite my_ticket_prop1 in Hdestruct1.
rewrite my_ticket_prop2 in init_lock_st, H.
rename z0 into prev_now.
rename z into prev_ticket.
rename tq_prev into tq_caltime.
rename l0 into tq_prev.
clear Hdestruct6.
assert (tiniteq: Int.unsigned (Int.repr (Int.unsigned (Int.repr (t_init + 1)) - 1)) = t_init).
{
assert(tcase: t_init = Int.max_unsigned ∨ t_init < Int.max_unsigned) by omega.
Caseeq tcase; intros.
rewrite H7.
Transparent Int.repr.
rewrite muval.
reflexivity.
Opaque Int.repr.
rewrite Int.unsigned_repr.
rewrite Int.unsigned_repr.
omega.
omega.
rewrite Int.unsigned_repr; omega.
}
rewrite tiniteq in ×.
rewrite my_ticket_prop2 in ×.
generalize (wait_lock_loop_correct_aux m d my_ticket n_init prev_ticket prev_now bound
cal_time tq_init tq_prev lock_id offset lock_index l K l1
n Hdestruct init_lock_st before_get_now Krangelt
Hcalctmp KPre KPost KPostPre H4 H3 H H6).
intros LP.
eapply LoopProofSimpleWhile.termination
with (condition := f_wait_lock_while_condition)
(body := f_wait_lock_while_body)
(P := wait_lock_loop_body_P m d my_ticket prev_now bound lock_id offset lock_index l)
(Q := wait_lock_loop_body_Q m d my_ticket bound cal_time lock_id offset lock_index l)
(le0 := (PTree.set 45 (Vint (Int.repr prev_now))
(PTree.set 44 (Vint (Int.repr my_ticket)) le)))
(m0 := (m, d {multi_log :
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l))
(multi_log d)})) in LP.
destruct LP as (while_le´, (while_m´, (LP1 & LP2))).
unfold wait_lock_loop_body_Q in LP2.
destruct LP2 as (while_d´, LP2).
destruct LP2 as (LP21 & LP22 & LP23 & LP24 & LP25 & LP26 & LP27).
destruct while_m´ as (while_tmp_m, while_tmp_d´).
esplit; repeat vcgen.
+
unfold incr_ticket_spec.
rewrite H3, H4, Hdestruct, Hdestruct0.
rewrite init_lock_st.
rewrite Int.unsigned_repr; try omega.
unfold ret; unfold option_monad_ops; repeat f_equal.
+
unfold get_now_spec.
simpl.
rewrite H3, H4, Hdestruct.
rewrite ZMap.gss.
rewrite Hdestruct2.
rewrite Int.unsigned_repr; try omega.
rewrite ZMap.set2.
rewrite multi_log_double_update.
reflexivity.
+ unfold log_hold_spec.
unfold calculate_wait_lock in LP26.
subdestruct.
inversion LP26.
inversion HcalcWait.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H3, H4, Hdestruct.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
reflexivity.
+ unfold wait_lock_loop_body_P.
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
reflexivity.
Qed.
End WaitLockBody.
Theorem wait_lock_code_correct:
spec_le (wait_lock ↦ wait_lock_spec_low) (〚wait_lock ↦ f_wait_lock 〛L).
Proof.
fbigstep_pre L.
fbigstep (wait_lock_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´
(fn_params f_wait_lock) (Vint bound::Vint i::Vint ofs::nil)
(create_undef_temps (fn_temps f_wait_lock)))) H0.
Qed.
End WAITLOCK.
End WithPrimitives.
End MTICKETLOCKINTRO.
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 TicketLockOpGenSpec.
Require Import MTicketLockIntroCSource.
Require Import MTicketLockIntro.
Require Import CalTicketLock.
Require Import AbstractDataType.
Module MTICKETLOCKINTRO.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{fairness: 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}.
Opaque PTree.get PTree.set.
Local Open Scope Z_scope.
Section PASSLOCK.
Let L: compatlayer (cdata RData) := incr_now ↦ gensem incr_now_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PassLockBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bincr_now: block.
Hypothesis hincr_now1 : Genv.find_symbol ge incr_now = Some bincr_now.
Hypothesis hincr_now2 :
Genv.find_funct_ptr ge bincr_now =
Some (External (EF_external incr_now
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma pass_lock_body_correct: ∀ m d d´ env le lock_id offset,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
ikern d = true →
ihost d = true →
incr_now_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_pass_lock_body E0 le´ ((m, d´): mem) Out_normal.
Proof.
intros.
subst.
esplit.
unfold f_pass_lock_body.
repeat vcgen.
Qed.
End PassLockBody.
Theorem pass_lock_code_correct:
spec_le (pass_lock ↦ pass_lock_spec_low) (〚pass_lock ↦ f_pass_lock 〛L).
Proof.
fbigstep_pre L.
destruct H0.
generalize hinv; intro.
inv hinv.
fbigstep (pass_lock_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´
(fn_params f_pass_lock) (Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_pass_lock)))) valid_curid.
Qed.
End PASSLOCK.
Section WAITLOCK.
Let L: compatlayer (cdata RData) := incr_ticket ↦ gensem incr_ticket_spec
⊕ get_now ↦ gensem get_now_spec
⊕ log_hold ↦ gensem log_hold_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section WaitLockBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bincr_ticket: block.
Hypothesis hincr_ticket1 : Genv.find_symbol ge incr_ticket = Some bincr_ticket.
Hypothesis hincr_ticket2 :
Genv.find_funct_ptr ge bincr_ticket =
Some (External (EF_external incr_ticket
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Variable bget_now: block.
Hypothesis hget_now1 : Genv.find_symbol ge get_now = Some bget_now.
Hypothesis hget_now2 :
Genv.find_funct_ptr ge bget_now =
Some (External (EF_external get_now
(signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable blog_hold: block.
Hypothesis hlog_hold1 : Genv.find_symbol ge log_hold = Some blog_hold.
Hypothesis hlog_hold2 :
Genv.find_funct_ptr ge blog_hold =
Some (External (EF_external log_hold
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
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.
Fixpoint CalTicketWaitWraparoundPre (n: nat) (i t: Z) (l: MultiLog) (to: MultiOracle):=
match n with
| O ⇒ Some l
| S n´ ⇒
let l´ := (TEVENT i (TTICKET GET_NOW)) :: (to i l) ++ l in
match CalTicketLockWraparound l´ with
| Some (_, n0, _) ⇒
if zeq t n0 then Some l´
else
CalTicketWaitWraparoundPre n´ i t l´ to
| _ ⇒ None
end
end.
Transparent CalTicketWaitWraparound.
Lemma CalTicketWaitWraparoundStops:
∀ m i t l to l´,
CalTicketWaitWraparound m i t l to = Some l´ →
∃ k,
(k ≤ m)%nat ∧
(∀ n,
(0 ≤ n < k)%nat → CalTicketWaitWraparound n i t l to = None) ∧
CalTicketWaitWraparound k i t l to = Some l´ ∧
∀ j, (k ≤ j)%nat → CalTicketWaitWraparoundPre j i t l to = Some l´.
Proof.
induction m; simpl; intros; [inv H |].
subdestruct.
- subst.
inv H.
∃ 1%nat.
split; [omega | ].
split; intros.
+ assert(n = O) by omega; subst.
reflexivity.
+ simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
split.
× reflexivity.
× intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H0.
rewrite <- H0.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
- eapply IHm in H; eauto.
destruct H.
destruct H.
destruct H0.
destruct H1.
∃ (S x).
split; [omega |].
split.
+ intros.
assert(n0case: n0 = O ∨ n0 ≠ O) by omega.
Caseeq n0case; intros.
subst.
reflexivity.
eapply NPeano.Nat.succ_pred in H4.
rewrite <- H4.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
eapply H0; eauto.
omega.
+ simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
split.
apply H1.
intros.
assert (j ≠ O) by omega.
eapply NPeano.Nat.succ_pred in H4.
rewrite <- H4.
simpl.
rewrite Hdestruct.
rewrite Hdestruct2.
eapply H2; eauto.
omega.
Qed.
Lemma CalTicketWaitWraparoundToPre:
∀ m i t l to l´,
CalTicketWaitWraparound m i t l to = Some l´ →
CalTicketWaitWraparoundPre m i t l to = Some l´.
Proof.
induction m; simpl; intros; [inv H |].
simpl.
intros.
subdestruct.
apply H.
eapply IHm; eauto.
Qed.
Lemma CalTicketWaitWraparoundToPreCons:
∀ m m´ i t l to l´,
CalTicketWaitWraparoundPre m i t l to = Some l´ →
(m´ ≤ m)%nat →
∃ l´´,
CalTicketWaitWraparoundPre m´ i t l to = Some l´´.
Proof.
induction m.
- simpl.
intros.
assert(m´ = O) by omega.
subst.
esplit.
reflexivity.
- simpl.
intros.
subdestruct.
+ 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, Hdestruct2.
esplit.
reflexivity.
+ 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, Hdestruct2.
eapply IHm; eauto.
omega.
Qed.
Lemma CalTicketWaitWraparoundPreInv: ∀ m i t l to l´,
CalTicketWaitWraparoundPre (S m) i t l to = Some l´ →
(∀ j, (j < (S m))%nat → CalTicketWaitWraparound j i t l to = None) →
∃ l´´,
CalTicketWaitWraparoundPre m i t l to = Some l´´ ∧
CalTicketWaitWraparoundPre 1 i t l´´ to = Some l´.
Proof.
induction m; simpl; intros.
- subdestruct.
+ inv H; esplit; split; [reflexivity | ].
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
+ inv H; esplit; split; [reflexivity | ].
rewrite Hdestruct.
rewrite Hdestruct2.
reflexivity.
- simpl in ×.
intros; subdestruct.
{ inv H.
assert ((1 < S (S m))%nat) by omega.
eapply H0 in H.
simpl in H.
rewrite Hdestruct in H.
rewrite Hdestruct2 in H.
inv H. }
{ inv H.
eapply IHm.
- rewrite Hdestruct3.
rewrite Hdestruct6.
reflexivity.
- intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H1.
simpl in H1.
rewrite Hdestruct in H1.
rewrite Hdestruct2 in H1.
apply H1. }
{ eapply IHm.
- rewrite Hdestruct3.
rewrite Hdestruct6.
apply H.
- intros.
assert ((S j < S (S m))%nat) by omega.
eapply H0 in H2.
simpl in H2.
rewrite Hdestruct in H2.
rewrite Hdestruct2 in H2.
apply H2. }
Qed.
Transparent CalTicketLockWraparound CalTicketWaitWraparound CalTicketWaitWraparoundPre.
Lemma CalTicketWaitWraparoundPreNeq: ∀ m i ticket l l´ to t n tl,
CalTicketWaitWraparound m i ticket l to = None →
CalTicketWaitWraparoundPre m i ticket l to = Some l´ →
(m > 0)%nat →
CalTicketLockWraparound l´ = Some (t, n, tl) →
n ≠ ticket.
Proof.
induction m; simpl; intros; try omega.
subdestruct; subst.
assert (mcase: m = O ∨ (m > O)%nat) by omega.
Caseeq mcase; intros; subst.
- simpl in ×.
inv H0.
simpl in H2.
rewrite Hdestruct in H2.
inv H2.
intros contra; elim n0; symmetry; auto.
- eapply IHm; eauto.
Qed.
Lemma CalTicketWaitWraparoundEq: ∀ m i t l to l´ t´ n´ tl,
CalTicketWaitWraparound m i t l to = Some l´ →
CalTicketLockWraparound l´ = Some (t´, n´, tl) →
n´ = t.
Proof.
induction m; simpl; intros; [inv H | ].
- subdestruct; subst.
+ inv H.
simpl in H0.
rewrite Hdestruct in H0.
inv H0.
auto.
+ eapply IHm; eauto.
Qed.
Section wait_lock_loop_proof.
Variable minit: memb.
Variable adt: RData.
Variable my_ticket : Z.
Variable init_now : Z.
Variable prev_ticket : Z.
Variable prev_now : Z.
Variable bound : int.
Variable cal_time: nat.
Variable tq_init: list nat.
Variable tq_prev: list nat.
Variable lock_id : int.
Variable offset : int.
Variable lock_index : Z.
Variable l : MultiLog.
Variable K: nat.
Variable l1: MultiLog.
Hypothesis init_neq: my_ticket ≠ prev_now.
Hypothesis index2zp: index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some lock_index.
Hypothesis initlist: (ZMap.get lock_index (multi_log adt)) = MultiDef l.
Hypothesis initlock: CalTicketLockWraparound
(ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) =
Some (my_ticket, init_now, tq_init).
Hypothesis lock_after_inc: CalTicketLockWraparound
(ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
= Some (prev_ticket, prev_now, tq_prev).
Hypothesis Krange: (0 < K < cal_time)%nat.
Hypothesis calcWait : CalTicketWaitWraparound (pred cal_time) (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (ZMap.get lock_index (multi_oracle adt)) =
Some l1.
Hypothesis KPre : ∀ n : nat,
(0 ≤ n < K)%nat →
CalTicketWaitWraparound n (CPU_ID adt) my_ticket (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt) (TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
(ZMap.get lock_index (multi_oracle adt)) = None.
Hypothesis KPost : CalTicketWaitWraparound K (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW) :: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) (TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l)
(ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis KPostPre : ∀ j : nat,
(K ≤ j)%nat →
CalTicketWaitWraparoundPre j (CPU_ID adt) my_ticket (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt)(CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (ZMap.get lock_index (multi_oracle adt)) = Some l1.
Hypothesis iihost: ihost adt = true.
Hypothesis iikern: ikern adt = true.
Hypothesis my_ticket_range: 0 ≤ my_ticket ≤ Int.max_unsigned.
Hypothesis prev_now_range: 0 ≤ prev_now ≤ Int.max_unsigned.
Definition wait_lock_loop_body_P (le: temp_env) (m : mem): Prop :=
le ! _current_ticket = Some (Vint (Int.repr prev_now)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
m = (minit,
adt {multi_log
: ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l)) (multi_log adt)}).
Definition calculate_wait_lock (i: nat) :=
match CalTicketWaitWraparoundPre i (CPU_ID adt) my_ticket
(TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt) (TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l) (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_ticket (d: RData) :=
match ZMap.get lock_index (multi_log d) with
| MultiDef l´ ⇒
match CalTicketLockWraparound l´ with
| Some (_, n, _) ⇒ Some n
| _ ⇒ None
end
| _ ⇒ None
end.
Definition wait_lock_loop_body_Q (le: temp_env) (m : mem): Prop :=
∃ d,
le ! _current_ticket = Some (Vint (Int.repr my_ticket)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
calculate_wait_lock (pred cal_time) = Some d∧
m = (minit, d).
Lemma wait_lock_loop_correct_aux:
LoopProofSimpleWhile.t
f_wait_lock_while_condition
f_wait_lock_while_body
ge (PTree.empty _)
wait_lock_loop_body_P
wait_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_now d´,
le ! _current_ticket = Some (Vint (Int.repr new_now)) ∧
le ! _my_ticket = Some (Vint (Int.repr (my_ticket))) ∧
le ! _lock_id = Some (Vint lock_id) ∧
le ! _offset = Some (Vint offset) ∧
le ! _bound = Some (Vint bound) ∧
(( i = O ∧ new_now ≠ my_ticket ∧
d´ = adt {multi_log :
ZMap.set lock_index
(MultiDef (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt)
(TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++
TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++
l)) (multi_log adt)}) ∨
(((0 < i < K)%nat ∧ new_now ≠ my_ticket∨
i = K ∧ new_now = my_ticket) ∧
calculate_wait_lock i = Some d´)) ∧
get_current_ticket d´ = Some new_now ∧
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 & Hle5 & Hm).
∃ (Z.of_nat K), O, prev_now.
esplit.
repeat vcgen.
unfold get_current_ticket; simpl.
rewrite ZMap.gss.
Transparent CalTicketLockWraparound.
simpl.
rewrite lock_after_inc.
rewrite Int.unsigned_repr by omega.
reflexivity.
Transparent CalTicketLockWraparound.
simpl.
omega.
- unfold f_wait_lock_while_condition, f_wait_lock_while_body.
intros le m w Hi.
destruct Hi as (i & new_ticket & newd & Hle1 & Hle2 & Hle3 & Hle4 & Hle5 & Hicond & Hcur & Hw & Hm).
Caseeq Hicond.
+
intros (ival & new & nd).
subst.
unfold get_current_ticket in Hcur; simpl in Hcur.
rewrite ZMap.gss in Hcur.
subdestruct.
inv Hcur.
assert (tmp: ∃ tmp_ticket tmp_now tmp_post,
CalTicketLockWraparound
(((ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) (TEVENT (CPU_ID adt) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt)
(TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
++ (TEVENT (CPU_ID adt) (TTICKET GET_NOW) :: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) (TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt)
(CPU_ID adt) l ++ l) ++ TEVENT (CPU_ID adt)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle adt) (CPU_ID adt) l ++ l))
= Some (tmp_ticket, tmp_now, tmp_post)).
{ assert(Kneq0: K ≠ O) by omega.
apply NPeano.Nat.succ_pred in Kneq0.
rewrite <- Kneq0 in KPost.
simpl in KPost.
subdestruct.
- ∃ z0, z1, l2; reflexivity.
- ∃ z0, z1, l2; reflexivity. }
destruct tmp as [tmp_ticket [tmp_now [tmp_post tmp_cal]]].
assert (0 ≤ new_ticket ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in Hdestruct.
omega.
}
assert (0 ≤ tmp_now ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in tmp_cal.
omega.
}
esplit; esplit.
repeat vcgen.
esplit; esplit.
repeat vcgen.
× unfold get_now_spec; simpl.
rewrite iihost, iikern, index2zp.
rewrite ZMap.gss.
rewrite tmp_cal.
rewrite ZMap.set2.
instantiate (1:= (Int.repr tmp_now)).
rewrite Int.unsigned_repr.
reflexivity.
omega.
×
∃ (Z.of_nat K - 1).
repeat vcgen.
∃ 1%nat.
esplit; esplit.
repeat vcgen.
{ right.
split.
assert (Kcase: (1 = K ∨ 1 < K)%nat) by omega.
Caseeq Kcase; intros.
{ rewrite <- H2.
right; split; [reflexivity | ].
rewrite <- H2 in KPost.
simpl in KPost.
subdestruct; subst.
inv tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity. }
{ left; split; try omega.
assert (onerange: (0 ≤ 1 < K)%nat) by omega.
eapply KPre in onerange.
simpl in onerange.
subdestruct.
inv tmp_cal; eauto.
clear Hdestruct3.
rewrite Int.unsigned_repr in n by omega.
omega.
}
{ unfold calculate_wait_lock; simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
destruct (zeq my_ticket tmp_now); reflexivity. } }
{ unfold get_current_ticket; simpl.
rewrite ZMap.gss.
Transparent CalTicketLockWraparound.
simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity. }
+ intro tmp; destruct tmp as [icond Hcalc].
Caseeq icond.
×
intros (irange & neq).
unfold calculate_wait_lock in Hcalc; simpl in Hcalc.
subdestruct.
inv Hcalc.
assert (tmp: ∃ tmp_ticket tmp_now tq_tmp,
CalTicketLockWraparound ((ZMap.get lock_index (multi_oracle adt))
(CPU_ID adt) m0 ++ m0) = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
eapply CalTicketWaitWraparoundPreInv in H0; eauto.
- destruct H0.
destruct H0.
rewrite Hdestruct in H0.
inv H0.
simpl in H1.
subdestruct.
+ ∃ z, z0, l0; reflexivity.
+ ∃ z, z0, l0; reflexivity.
- intros.
eapply KPre; eauto.
omega. }
destruct tmp as [tmp_ticket [tmp_now [tq_tmp tmp_cal]]].
assert (tmp_now_range: 0 ≤ tmp_now ≤ Int.max_unsigned).
{
apply CalTicketLockWraparoundRange in tmp_cal.
destruct tmp_cal; auto.
}
assert (tmp_ticket_range: 0 ≤ tmp_ticket ≤ Int.max_unsigned).
{
apply CalTicketLockWraparoundRange in tmp_cal.
destruct tmp_cal; auto.
}
assert (new_ticket_range: 0 ≤ new_ticket ≤ Int.max_unsigned).
{
unfold get_current_ticket in Hcur.
simpl in Hcur.
rewrite ZMap.gss in Hcur.
subdestruct.
inv Hcur.
apply CalTicketLockWraparoundRange in Hdestruct0.
destruct Hdestruct0; auto.
}
esplit; esplit.
repeat vcgen.
esplit; esplit.
repeat vcgen.
{ unfold get_now_spec; simpl.
rewrite iihost, iikern, index2zp.
rewrite ZMap.gss.
rewrite tmp_cal.
instantiate (1:= (Int.repr tmp_now)).
rewrite Int.unsigned_repr.
reflexivity.
omega. }
{
∃ (Z.of_nat K - Z.of_nat i - 1).
repeat vcgen.
esplit; esplit; esplit.
repeat vcgen.
instantiate (1:= (S i)).
right.
split.
- assert (icase: (S i = K ∨ S i < K)%nat) by omega.
Caseeq icase; intros.
+ right.
split; auto.
assert((K ≤ K)%nat) by omega.
eapply KPostPre in H1.
rewrite <- H0 in H1.
assert (CalTicketLockWraparound l1 = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundPreInv in H1; eauto.
- destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
+ inv tmp_cal.
inv H2.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
+ inv tmp_cal.
inv H2.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
- intros.
eapply KPre; eauto.
omega. }
eapply CalTicketWaitWraparoundEq; eauto.
+ left.
split; try omega.
assert ((0 ≤ S i < K)%nat) by omega.
eapply KPre in H1.
eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
assert (CalTicketLockWraparound x = Some (tmp_ticket, tmp_now, tq_tmp)).
{ eapply CalTicketWaitWraparoundPreInv in H3; eauto.
- destruct H3.
destruct H3.
rewrite Hdestruct in H3.
inv H3.
simpl in H4.
subdestruct.
+ inv tmp_cal.
inv H4.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
+ inv tmp_cal.
inv H4.
simpl.
rewrite Hdestruct0.
rewrite Int.unsigned_repr by omega.
rewrite Int.unsigned_repr by omega.
reflexivity.
- intros.
eapply KPre; eauto.
omega. }
eapply CalTicketWaitWraparoundPreNeq in H3; eauto.
omega.
- unfold calculate_wait_lock.
eapply CalTicketWaitWraparoundToPre in KPost; eauto.
assert ((S i ≤ K)%nat) by omega.
eapply CalTicketWaitWraparoundToPreCons in KPost; eauto.
destruct KPost.
rewrite H1.
eapply CalTicketWaitWraparoundPreInv in H1; eauto.
+ destruct H1.
destruct H1.
rewrite Hdestruct in H1.
inv H1.
simpl in H2.
subdestruct.
× inv tmp_cal.
inv H2.
rewrite ZMap.set2.
reflexivity.
× inv tmp_cal.
inv H2.
rewrite ZMap.set2.
reflexivity.
+ intros.
eapply KPre; eauto.
omega.
- unfold get_current_ticket; simpl.
rewrite ZMap.gss.
simpl.
rewrite tmp_cal.
rewrite Int.unsigned_repr by omega.
reflexivity.
- rewrite Nat2Z.inj_succ; unfold Z.succ.
omega. }
×
intros (ival & ticketseq).
subst.
esplit. esplit.
repeat vcgen.
unfold wait_lock_loop_body_Q.
∃ newd.
repeat (split; eauto).
assert ((K ≤ (pred cal_time))%nat) by omega.
unfold calculate_wait_lock in ×.
assert ((K ≤ K)%nat) by omega.
erewrite KPostPre in Hcalc; eauto.
erewrite KPostPre; eauto.
Qed.
End wait_lock_loop_proof.
Lemma wait_lock_body_correct: ∀ m d d´ env le bound lock_id offset,
env = PTree.empty _ →
PTree.get _bound le = Some (Vint bound) →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
ikern d = true →
ihost d = true →
high_level_invariant d →
wait_lock_spec_wraparound (Int.unsigned bound) (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_wait_lock_body E0 le´ ((m, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold f_wait_lock_body; subst.
unfold wait_lock_spec_wraparound in H6; subst.
rewrite H3, H4 in H6.
Opaque CalTicketLockWraparound CalWaitTime.
subdestruct; subst.
assert (cal_time_range: (CalWaitTime l0 > 0)%nat).
{ assert ((CalWaitTime l0 ≠ 0)%nat).
{ Transparent CalWaitTime.
intro.
unfold CalWaitTime in ×.
inv H. }
omega.
Opaque CalWaitTime. }
set (cal_time:= CalWaitTime l0).
fold cal_time in cal_time_range, Hdestruct4.
rewrite <- NPeano.Nat.succ_pred_pos with (n:= cal_time) in Hdestruct4 by omega.
remember z as lock_index; symmetry in Heqlock_index; subst.
remember z0 as t_prev; symmetry in Heqt_prev; subst.
remember z1 as n_prev; symmetry in Heqn_prev; subst.
remember l0 as tq_prev; symmetry in Heqtq_prev; subst.
assert (init_lock_st: ∃ t_init n_init tq_init,
CalTicketLockWraparound
((ZMap.get lock_index (multi_oracle d)) (CPU_ID d) l ++ l) = Some (t_init, n_init, tq_init)).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct1.
subdestruct; subst.
∃ z, z0, l0; reflexivity.
Opaque CalTicketLockWraparound. }
destruct init_lock_st as [t_init [n_init [tq_init init_lock_st]]].
assert (ticket_lock_vals:
Int.unsigned (Int.repr (t_init + 1)) = t_prev ∧ n_init = n_prev ∧ tq_init++((Z.to_nat (Int.unsigned bound))::nil) = tq_prev).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct1.
subdestruct; simpl; subst.
clear Hdestruct4 cal_time_range Hdestruct4 cal_time.
inv init_lock_st; inv Hdestruct1.
split. reflexivity.
rewrite Int.unsigned_repr.
tauto.
eapply CalTicketLockWraparoundRange; eauto.
Opaque CalTicketLockWraparound. }
destruct ticket_lock_vals as [? [? ?]].
symmetry in H; rewrite H in *; clear H.
symmetry in H7; rewrite H7 in *; clear H7.
symmetry in H8; rewrite H8 in *; clear H8.
simpl in Hdestruct4.
assert (0 ≤ t_init ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange in init_lock_st;
destruct init_lock_st; auto.
}
subdestruct.
-
inv Hdestruct4; subst.
inv H6; subst.
esplit; repeat vcgen.
+
unfold incr_ticket_spec.
rewrite H3, H4, Hdestruct, Hdestruct0.
rewrite init_lock_st.
instantiate (1:= Int.repr t_init).
rewrite Int.unsigned_repr; try omega.
unfold ret; unfold option_monad_ops; repeat f_equal.
+
unfold get_now_spec.
simpl.
rewrite H3, H4, Hdestruct.
rewrite ZMap.gss.
rewrite Hdestruct2.
rewrite ZMap.set2.
assert (Int.unsigned (Int.repr (Int.unsigned (Int.repr (t_init + 1)) - 1)) = t_init).
{
assert(tcase: t_init = Int.max_unsigned ∨ t_init < Int.max_unsigned) by omega.
Caseeq tcase; intros.
rewrite H6.
Transparent Int.repr.
rewrite muval.
reflexivity.
Opaque Int.repr.
rewrite Int.unsigned_repr.
rewrite Int.unsigned_repr.
omega.
omega.
rewrite Int.unsigned_repr; omega.
}
rewrite H6.
instantiate (1:= Int.repr t_init).
rewrite Int.unsigned_repr by omega.
reflexivity.
+
rewrite multi_log_double_update; subst.
instantiate (2:=
(set_opttemp (Some 45%positive) (Vint (Int.repr t_init))
(set_opttemp (Some 44%positive) (Vint (Int.repr t_init)) le))).
unfold set_opttemp.
instantiate (1:=
d {multi_log
: ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}).
unfold f_wait_lock_while_condition, f_wait_lock_while_body.
eapply exec_Sloop_stop1.
eapply exec_Sseq_2.
repeat vcgen.
intro contra; inv contra.
econstructor.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ unfold log_hold_spec.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H3, H4, Hdestruct; simpl.
rewrite ZMap.gss.
rewrite multi_log_double_update; subst; simpl.
rewrite ZMap.set2.
unfold ret; unfold option_monad_ops; repeat f_equal.
-
inv H6; subst.
assert (0 ≤ z0 ≤ Int.max_unsigned).
{
eapply CalTicketLockWraparoundRange; eauto.
}
assert (before_get_now: CalTicketLockWraparound (ZMap.get lock_index (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d) l ++ l) ++ TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) = Some (z, z0, l0)).
{ Transparent CalTicketLockWraparound.
simpl in Hdestruct2.
Opaque CalTicketLockWraparound.
subdestruct.
rewrite Int.unsigned_repr in Hdestruct2.
rewrite Int.unsigned_repr in Hdestruct2.
inv Hdestruct2; reflexivity.
eapply CalTicketLockWraparoundRange; eauto.
eapply CalTicketLockWraparoundRange in Hdestruct3; destruct Hdestruct3; eauto.
}
generalize Hdestruct4; intro HcalcWait.
generalize HcalcWait; intro Hcalctmp.
eapply CalTicketWaitWraparoundToPre in HcalcWait; eauto.
eapply CalTicketWaitWraparoundStops in Hdestruct4; eauto.
destruct Hdestruct4 as [K [Krange [KPre [KPost KPostPre]]]].
assert (Kgt0: (0 < K)%nat).
{ assert (K = O → False).
intro.
subst.
inv KPost.
omega. }
assert (Krangelt: (0 < K < cal_time)%nat) by omega.
set (my_ticket := t_init + 1 - 1).
fold my_ticket in Hcalctmp, HcalcWait, KPostPre, KPost, KPre, n, Hdestruct6.
assert (my_ticket_prop1: t_init + 1 = my_ticket + 1).
{ unfold my_ticket; ring. }
assert (my_ticket_prop2: t_init = my_ticket).
{ unfold my_ticket; ring. }
rewrite my_ticket_prop1 in Hdestruct1.
rewrite my_ticket_prop2 in init_lock_st, H.
rename z0 into prev_now.
rename z into prev_ticket.
rename tq_prev into tq_caltime.
rename l0 into tq_prev.
clear Hdestruct6.
assert (tiniteq: Int.unsigned (Int.repr (Int.unsigned (Int.repr (t_init + 1)) - 1)) = t_init).
{
assert(tcase: t_init = Int.max_unsigned ∨ t_init < Int.max_unsigned) by omega.
Caseeq tcase; intros.
rewrite H7.
Transparent Int.repr.
rewrite muval.
reflexivity.
Opaque Int.repr.
rewrite Int.unsigned_repr.
rewrite Int.unsigned_repr.
omega.
omega.
rewrite Int.unsigned_repr; omega.
}
rewrite tiniteq in ×.
rewrite my_ticket_prop2 in ×.
generalize (wait_lock_loop_correct_aux m d my_ticket n_init prev_ticket prev_now bound
cal_time tq_init tq_prev lock_id offset lock_index l K l1
n Hdestruct init_lock_st before_get_now Krangelt
Hcalctmp KPre KPost KPostPre H4 H3 H H6).
intros LP.
eapply LoopProofSimpleWhile.termination
with (condition := f_wait_lock_while_condition)
(body := f_wait_lock_while_body)
(P := wait_lock_loop_body_P m d my_ticket prev_now bound lock_id offset lock_index l)
(Q := wait_lock_loop_body_Q m d my_ticket bound cal_time lock_id offset lock_index l)
(le0 := (PTree.set 45 (Vint (Int.repr prev_now))
(PTree.set 44 (Vint (Int.repr my_ticket)) le)))
(m0 := (m, d {multi_log :
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NOW)
:: ZMap.get lock_index (multi_oracle d)
(CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l) ++
TEVENT (CPU_ID d)
(TTICKET (INC_TICKET (Z.to_nat (Int.unsigned bound))))
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d) l ++
l))
(multi_log d)})) in LP.
destruct LP as (while_le´, (while_m´, (LP1 & LP2))).
unfold wait_lock_loop_body_Q in LP2.
destruct LP2 as (while_d´, LP2).
destruct LP2 as (LP21 & LP22 & LP23 & LP24 & LP25 & LP26 & LP27).
destruct while_m´ as (while_tmp_m, while_tmp_d´).
esplit; repeat vcgen.
+
unfold incr_ticket_spec.
rewrite H3, H4, Hdestruct, Hdestruct0.
rewrite init_lock_st.
rewrite Int.unsigned_repr; try omega.
unfold ret; unfold option_monad_ops; repeat f_equal.
+
unfold get_now_spec.
simpl.
rewrite H3, H4, Hdestruct.
rewrite ZMap.gss.
rewrite Hdestruct2.
rewrite Int.unsigned_repr; try omega.
rewrite ZMap.set2.
rewrite multi_log_double_update.
reflexivity.
+ unfold log_hold_spec.
unfold calculate_wait_lock in LP26.
subdestruct.
inversion LP26.
inversion HcalcWait.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H3, H4, Hdestruct.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
rewrite ZMap.set2.
reflexivity.
+ unfold wait_lock_loop_body_P.
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
split; [repeat vcgen | ].
reflexivity.
Qed.
End WaitLockBody.
Theorem wait_lock_code_correct:
spec_le (wait_lock ↦ wait_lock_spec_low) (〚wait_lock ↦ f_wait_lock 〛L).
Proof.
fbigstep_pre L.
fbigstep (wait_lock_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´
(fn_params f_wait_lock) (Vint bound::Vint i::Vint ofs::nil)
(create_undef_temps (fn_temps f_wait_lock)))) H0.
Qed.
End WAITLOCK.
End WithPrimitives.
End MTICKETLOCKINTRO.