Library mcertikos.ticketlog.MCurIDCode
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 TacticsForTesting.
Require Import TicketLockIntroGenSpec.
Require Import MCurIDCSource.
Require Import MCurID.
Require Import AbstractDataType.
Module MCURIDCODE.
Lemma structsize: sizeof t_ticket_lock_struct = 8%Z.
Proof.
generalize max_unsigned_val; intro muval.
simpl. unfold align. simpl; trivial.
Qed.
Lemma zle_max: (0 ≤ Int.max_unsigned)%Z.
Proof.
generalize max_unsigned_val; intro muval.
omega.
Qed.
Lemma ID_AT_range_val : ID_AT_range = 1%Z.
Proof.
unfold ID_AT_range; reflexivity.
Qed.
Lemma num_chan_val : num_chan = 1040%Z.
Proof.
simpl. reflexivity.
Qed.
Lemma ID_TCB_range_val : ID_TCB_range = num_chan.
Proof.
simpl; reflexivity.
Qed.
Lemma num_cv_val : num_cv = 1024%Z.
Proof.
simpl; reflexivity.
Qed.
Lemma ID_SC_range_val : ID_SC_range = num_chan.
Proof.
simpl; unfold ID_SC_range.
reflexivity.
Qed.
Lemma size_of_struct_array: sizeof (Tarray t_ticket_lock_struct lock_range noattr) = (lock_range × 8)%Z.
Proof.
unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range.
simpl.
reflexivity.
Qed.
Lemma lock_range_val : lock_range = (1 + 1040 + 1040)%Z.
Proof.
unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range; simpl.
reflexivity.
Qed.
Opaque Z.add Z.sub Z.mul Z.div sizeof align.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{oracle_prop: MultiOracleProp}.
Context `{Hmwd: UseMemWithData memb}.
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 INCRNOW.
Let L: compatlayer (cdata RData) := TICKET_LOCK_LOC ↦ ticket_lock_type
⊕ log_incr ↦ gensem log_incr_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section IncrNowBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variables bticket_lock_loc : block.
Hypothesis bticket_lock_loc1 : Genv.find_symbol ge TICKET_LOCK_LOC = Some bticket_lock_loc.
Variable blog_incr: block.
Hypothesis hlog_incr1 : Genv.find_symbol ge log_incr = Some blog_incr.
Hypothesis hlog_incr2 :
Genv.find_funct_ptr ge blog_incr =
Some (External (EF_external log_incr
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma incr_now_body_correct: ∀ m m´ d d´ env le lock_id offset n pos,
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 →
high_level_invariant d →
log_incr_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some pos →
Mem.loadv Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4 ))) = Some (Vint n) →
Mem.storev Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4))) (Vint (Int.add n Int.one))
= Some (m´, d´) →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_incr_now_body E0 le´ ((m´, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize structsize; intro strsz.
generalize zle_max; intro zle_mint.
generalize size_of_struct_array; intro sizeof_sa.
generalize tintsize; intro tintsize.
intros; subst.
assert (IdRange: 0 ≤ Int.unsigned lock_id < ID_range).
{ clearAllExceptOne H6.
unfold index2Z in H6.
unfold index_range in H6.
destruct (Int.unsigned lock_id); try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail). }
assert (IdVal: Int.unsigned lock_id = 0 ∨
Int.unsigned lock_id = 1 ∨
Int.unsigned lock_id = 2).
{ clearAllExceptOne IdRange; omega. }
assert (SizeRange1: 0 ≤ sizeof t_ticket_lock_struct) by omega.
assert (SizeRange2: 0 ≤ sizeof t_ticket_lock_struct × Int.unsigned lock_id).
{ rewrite strsz in *; omega. }
assert (SizeRange3: sizeof t_ticket_lock_struct × Int.unsigned lock_id ≤ Int.max_unsigned).
{ rewrite strsz in *; omega. }
destruct IdVal as [IdVal0 | [IdVal1 | IdVal2]].
-
assert (offsetRange: 0 ≤ Int.unsigned offset < 1).
{ clearAllExceptTwo H6 IdVal0.
unfold index2Z in H6. rewrite IdVal0 in H6. simpl in H6.
unfold ID_AT_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) 1); [ | inv H6].
omega. }
assert (posVal: pos = (Int.unsigned offset)).
{ clearAllExceptTwo H6 IdVal0.
rewrite IdVal0 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H7.
× repeat vcgen.
× repeat vcgen.
× rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H8.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal1.
unfold index2Z in H6. rewrite IdVal1 in H6. simpl in H6.
unfold ID_TCB_range in H6; simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = ID_AT_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal1.
rewrite IdVal1 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H7.
× repeat vcgen.
× repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H8.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal2.
unfold index2Z in H6. rewrite IdVal2 in H6.
simpl in H6.
unfold ID_SC_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = lock_TCB_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal2.
rewrite IdVal2 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
exact H7.
× repeat vcgen.
× repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
exact H8.
Qed.
End IncrNowBody.
Theorem incr_now_code_correct:
spec_le (incr_now ↦ incr_now_spec_low) (〚incr_now ↦ f_incr_now 〛L).
Proof.
fbigstep_pre L.
destruct Hkern.
simpl in ×.
generalize hinv; intros.
inv hinv.
generalize Hspec; intro.
assert (posRange: 0 ≤ pos < lock_range).
{ clearAllExceptOne Hpos.
unfold index2Z in Hpos.
unfold index_range in Hpos.
destruct (Int.unsigned i).
unfold index_incrange in Hpos.
destruct (index_incrange 0); [ | inv Hpos].
destruct (zle_lt 0 (Int.unsigned ofs) ID_AT_range); [ | inv Hpos].
unfold ID_AT_range in ×. inv Hpos. unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
destruct (zle_lt 0 (Int.unsigned ofs) (ID_AT_range)).
inv H0. unfold ID_AT_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv H0.
destruct p; try (inv Hpos; fail).
destruct p; try (inv Hpos; fail).
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_SC_range) in Hpos.
inv Hpos.
unfold ID_SC_range, lock_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_TCB_range) in Hpos.
inv Hpos.
unfold ID_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
inv Hpos. }
generalize lock_range_val; intros lock_range_val.
fbigsteptest (incr_now_body_correct s (Genv.globalenv p) makeglobalenv b Hsymbol
b2 Hb2fs Hb2fp m0 m´0 d d´
(PTree.empty _) (bind_parameter_temps´
(fn_params f_incr_now)
(Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_incr_now)))) valid_curid;
try reflexivity.
rewrite Hstore1; eauto.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End INCRNOW.
Section INITTICKET.
Let L: compatlayer (cdata RData) := TICKET_LOCK_LOC ↦ ticket_lock_type
⊕ log_init ↦ gensem log_init_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section InitTicketBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variables bticket_lock_loc : block.
Hypothesis bticket_lock_loc1 : Genv.find_symbol ge TICKET_LOCK_LOC = Some bticket_lock_loc.
Variable blog_init: block.
Hypothesis hlog_init1 : Genv.find_symbol ge log_init = Some blog_init.
Hypothesis hlog_init2 :
Genv.find_funct_ptr ge blog_init =
Some (External (EF_external log_init
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma init_ticket_body_correct: ∀ m m0 m´ d d´ env le lock_id offset pos,
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 →
high_level_invariant d →
log_init_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some pos →
Mem.storev Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 0 ))) Vzero = Some (m0, d´) →
Mem.storev Mint32 ((m0, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4))) Vzero = Some (m´, d´) →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_init_ticket_body E0 le´ ((m´, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize structsize; intro strsz.
generalize zle_max; intro zle_mint.
generalize size_of_struct_array; intro sizeof_sa.
generalize tintsize; intro tintsize.
intros; subst.
assert (IdRange: 0 ≤ Int.unsigned lock_id < ID_range).
{ clearAllExceptOne H6.
unfold index2Z in H6.
unfold index_range in H6.
destruct (Int.unsigned lock_id); try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail). }
assert (IdVal: Int.unsigned lock_id = 0 ∨
Int.unsigned lock_id = 1 ∨
Int.unsigned lock_id = 2).
{ clearAllExceptOne IdRange; omega. }
assert (SizeRange1: 0 ≤ sizeof t_ticket_lock_struct) by omega.
assert (SizeRange2: 0 ≤ sizeof t_ticket_lock_struct × Int.unsigned lock_id).
{ rewrite strsz in ×. omega. }
assert (SizeRange3: sizeof t_ticket_lock_struct × Int.unsigned lock_id ≤ Int.max_unsigned).
{ rewrite strsz in ×. omega. }
destruct IdVal as [IdVal0 | [IdVal1 | IdVal2]].
-
assert (offsetRange: 0 ≤ Int.unsigned offset < 1).
{ clearAllExceptTwo H6 IdVal0.
unfold index2Z in H6. rewrite IdVal0 in H6. simpl in H6.
unfold ID_AT_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) 1); [ | inv H6].
omega. }
assert (posVal: pos = (Int.unsigned offset)).
{ clearAllExceptTwo H6 IdVal0.
rewrite IdVal0 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× rewrite <- posVal. rewrite strsz. rewrite Z.mul_comm.
eassumption.
× apply align_le. omega.
× rewrite <- posVal. rewrite strsz. rewrite Z.mul_comm.
eassumption.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal1.
unfold index2Z in H6. rewrite IdVal1 in H6. simpl in H6.
unfold ID_TCB_range in H6; simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = ID_AT_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal1.
rewrite IdVal1 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz. rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
eassumption.
× apply align_le. omega.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz. rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
eassumption.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal2.
unfold index2Z in H6. rewrite IdVal2 in H6.
unfold ID_SC_range in H6.
unfold index_range in H6.
unfold index_incrange in H6.
unfold ID_SC_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = lock_TCB_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal2.
rewrite IdVal2 in H6.
unfold index2Z in H6.
unfold index_range in H6.
unfold index_incrange in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
repeat vcgen.
× apply align_le. omega.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
repeat vcgen.
Qed.
End InitTicketBody.
Theorem init_ticket_code_correct:
spec_le (init_ticket ↦ init_ticket_spec_low) (〚init_ticket ↦ f_init_ticket 〛L).
Proof.
fbigstep_pre L.
destruct Hkern.
simpl in ×.
generalize hinv; intro.
inv hinv.
assert (posRange: 0 ≤ pos < lock_range).
{
clearAllExceptOne Hpos.
unfold index2Z in Hpos.
unfold index_range in Hpos.
destruct (Int.unsigned i).
unfold index_incrange in Hpos.
destruct (index_incrange 0); [ | inv Hpos].
destruct (zle_lt 0 (Int.unsigned ofs) ID_AT_range); [ | inv Hpos].
unfold ID_AT_range in ×. inv Hpos. unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
destruct (zle_lt 0 (Int.unsigned ofs) (ID_AT_range)).
inv H0. unfold ID_AT_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv H0.
destruct p; try (inv Hpos; fail).
destruct p; try (inv Hpos; fail).
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_SC_range) in Hpos.
inv Hpos.
unfold ID_SC_range, lock_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_TCB_range) in Hpos.
inv Hpos.
unfold ID_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
inv Hpos.
}
assert (lockRangeVal: lock_range = num_chan + num_chan + 1).
{ unfold lock_range; reflexivity. }
fbigsteptest (init_ticket_body_correct s (Genv.globalenv p) makeglobalenv b Hsymbol b2 Hb2fs Hb2fp m0 m1 m´0 d d´
(PTree.empty _) (bind_parameter_temps´
(fn_params f_init_ticket)
(Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_init_ticket)))) valid_curid;
try reflexivity.
replace (pos × 8 + 0) with (pos × 8); try omega.
rewrite Hstore0; reflexivity.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End INITTICKET.
End WithPrimitives.
Transparent Z.add Z.sub Z.mul Z.div sizeof align.
End MCURIDCODE.
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 TacticsForTesting.
Require Import TicketLockIntroGenSpec.
Require Import MCurIDCSource.
Require Import MCurID.
Require Import AbstractDataType.
Module MCURIDCODE.
Lemma structsize: sizeof t_ticket_lock_struct = 8%Z.
Proof.
generalize max_unsigned_val; intro muval.
simpl. unfold align. simpl; trivial.
Qed.
Lemma zle_max: (0 ≤ Int.max_unsigned)%Z.
Proof.
generalize max_unsigned_val; intro muval.
omega.
Qed.
Lemma ID_AT_range_val : ID_AT_range = 1%Z.
Proof.
unfold ID_AT_range; reflexivity.
Qed.
Lemma num_chan_val : num_chan = 1040%Z.
Proof.
simpl. reflexivity.
Qed.
Lemma ID_TCB_range_val : ID_TCB_range = num_chan.
Proof.
simpl; reflexivity.
Qed.
Lemma num_cv_val : num_cv = 1024%Z.
Proof.
simpl; reflexivity.
Qed.
Lemma ID_SC_range_val : ID_SC_range = num_chan.
Proof.
simpl; unfold ID_SC_range.
reflexivity.
Qed.
Lemma size_of_struct_array: sizeof (Tarray t_ticket_lock_struct lock_range noattr) = (lock_range × 8)%Z.
Proof.
unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range.
simpl.
reflexivity.
Qed.
Lemma lock_range_val : lock_range = (1 + 1040 + 1040)%Z.
Proof.
unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range; simpl.
reflexivity.
Qed.
Opaque Z.add Z.sub Z.mul Z.div sizeof align.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{oracle_prop: MultiOracleProp}.
Context `{Hmwd: UseMemWithData memb}.
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 INCRNOW.
Let L: compatlayer (cdata RData) := TICKET_LOCK_LOC ↦ ticket_lock_type
⊕ log_incr ↦ gensem log_incr_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section IncrNowBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variables bticket_lock_loc : block.
Hypothesis bticket_lock_loc1 : Genv.find_symbol ge TICKET_LOCK_LOC = Some bticket_lock_loc.
Variable blog_incr: block.
Hypothesis hlog_incr1 : Genv.find_symbol ge log_incr = Some blog_incr.
Hypothesis hlog_incr2 :
Genv.find_funct_ptr ge blog_incr =
Some (External (EF_external log_incr
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma incr_now_body_correct: ∀ m m´ d d´ env le lock_id offset n pos,
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 →
high_level_invariant d →
log_incr_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some pos →
Mem.loadv Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4 ))) = Some (Vint n) →
Mem.storev Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4))) (Vint (Int.add n Int.one))
= Some (m´, d´) →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_incr_now_body E0 le´ ((m´, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize structsize; intro strsz.
generalize zle_max; intro zle_mint.
generalize size_of_struct_array; intro sizeof_sa.
generalize tintsize; intro tintsize.
intros; subst.
assert (IdRange: 0 ≤ Int.unsigned lock_id < ID_range).
{ clearAllExceptOne H6.
unfold index2Z in H6.
unfold index_range in H6.
destruct (Int.unsigned lock_id); try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail). }
assert (IdVal: Int.unsigned lock_id = 0 ∨
Int.unsigned lock_id = 1 ∨
Int.unsigned lock_id = 2).
{ clearAllExceptOne IdRange; omega. }
assert (SizeRange1: 0 ≤ sizeof t_ticket_lock_struct) by omega.
assert (SizeRange2: 0 ≤ sizeof t_ticket_lock_struct × Int.unsigned lock_id).
{ rewrite strsz in *; omega. }
assert (SizeRange3: sizeof t_ticket_lock_struct × Int.unsigned lock_id ≤ Int.max_unsigned).
{ rewrite strsz in *; omega. }
destruct IdVal as [IdVal0 | [IdVal1 | IdVal2]].
-
assert (offsetRange: 0 ≤ Int.unsigned offset < 1).
{ clearAllExceptTwo H6 IdVal0.
unfold index2Z in H6. rewrite IdVal0 in H6. simpl in H6.
unfold ID_AT_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) 1); [ | inv H6].
omega. }
assert (posVal: pos = (Int.unsigned offset)).
{ clearAllExceptTwo H6 IdVal0.
rewrite IdVal0 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H7.
× repeat vcgen.
× repeat vcgen.
× rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H8.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal1.
unfold index2Z in H6. rewrite IdVal1 in H6. simpl in H6.
unfold ID_TCB_range in H6; simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = ID_AT_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal1.
rewrite IdVal1 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H7.
× repeat vcgen.
× repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz.
rewrite Z.mul_comm.
exact H8.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal2.
unfold index2Z in H6. rewrite IdVal2 in H6.
simpl in H6.
unfold ID_SC_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = lock_TCB_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal2.
rewrite IdVal2 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
exact H7.
× repeat vcgen.
× repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
exact H8.
Qed.
End IncrNowBody.
Theorem incr_now_code_correct:
spec_le (incr_now ↦ incr_now_spec_low) (〚incr_now ↦ f_incr_now 〛L).
Proof.
fbigstep_pre L.
destruct Hkern.
simpl in ×.
generalize hinv; intros.
inv hinv.
generalize Hspec; intro.
assert (posRange: 0 ≤ pos < lock_range).
{ clearAllExceptOne Hpos.
unfold index2Z in Hpos.
unfold index_range in Hpos.
destruct (Int.unsigned i).
unfold index_incrange in Hpos.
destruct (index_incrange 0); [ | inv Hpos].
destruct (zle_lt 0 (Int.unsigned ofs) ID_AT_range); [ | inv Hpos].
unfold ID_AT_range in ×. inv Hpos. unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
destruct (zle_lt 0 (Int.unsigned ofs) (ID_AT_range)).
inv H0. unfold ID_AT_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv H0.
destruct p; try (inv Hpos; fail).
destruct p; try (inv Hpos; fail).
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_SC_range) in Hpos.
inv Hpos.
unfold ID_SC_range, lock_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_TCB_range) in Hpos.
inv Hpos.
unfold ID_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
inv Hpos. }
generalize lock_range_val; intros lock_range_val.
fbigsteptest (incr_now_body_correct s (Genv.globalenv p) makeglobalenv b Hsymbol
b2 Hb2fs Hb2fp m0 m´0 d d´
(PTree.empty _) (bind_parameter_temps´
(fn_params f_incr_now)
(Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_incr_now)))) valid_curid;
try reflexivity.
rewrite Hstore1; eauto.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End INCRNOW.
Section INITTICKET.
Let L: compatlayer (cdata RData) := TICKET_LOCK_LOC ↦ ticket_lock_type
⊕ log_init ↦ gensem log_init_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section InitTicketBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variables bticket_lock_loc : block.
Hypothesis bticket_lock_loc1 : Genv.find_symbol ge TICKET_LOCK_LOC = Some bticket_lock_loc.
Variable blog_init: block.
Hypothesis hlog_init1 : Genv.find_symbol ge log_init = Some blog_init.
Hypothesis hlog_init2 :
Genv.find_funct_ptr ge blog_init =
Some (External (EF_external log_init
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Lemma init_ticket_body_correct: ∀ m m0 m´ d d´ env le lock_id offset pos,
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 →
high_level_invariant d →
log_init_spec (Int.unsigned lock_id) (Int.unsigned offset) d = Some d´ →
index2Z (Int.unsigned lock_id) (Int.unsigned offset) = Some pos →
Mem.storev Mint32 ((m, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 0 ))) Vzero = Some (m0, d´) →
Mem.storev Mint32 ((m0, d´): mem) (Vptr bticket_lock_loc (Int.repr (pos × 8 + 4))) Vzero = Some (m´, d´) →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_init_ticket_body E0 le´ ((m´, d´): mem) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize structsize; intro strsz.
generalize zle_max; intro zle_mint.
generalize size_of_struct_array; intro sizeof_sa.
generalize tintsize; intro tintsize.
intros; subst.
assert (IdRange: 0 ≤ Int.unsigned lock_id < ID_range).
{ clearAllExceptOne H6.
unfold index2Z in H6.
unfold index_range in H6.
destruct (Int.unsigned lock_id); try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail).
destruct p; try omega; try (inv H6; fail). }
assert (IdVal: Int.unsigned lock_id = 0 ∨
Int.unsigned lock_id = 1 ∨
Int.unsigned lock_id = 2).
{ clearAllExceptOne IdRange; omega. }
assert (SizeRange1: 0 ≤ sizeof t_ticket_lock_struct) by omega.
assert (SizeRange2: 0 ≤ sizeof t_ticket_lock_struct × Int.unsigned lock_id).
{ rewrite strsz in ×. omega. }
assert (SizeRange3: sizeof t_ticket_lock_struct × Int.unsigned lock_id ≤ Int.max_unsigned).
{ rewrite strsz in ×. omega. }
destruct IdVal as [IdVal0 | [IdVal1 | IdVal2]].
-
assert (offsetRange: 0 ≤ Int.unsigned offset < 1).
{ clearAllExceptTwo H6 IdVal0.
unfold index2Z in H6. rewrite IdVal0 in H6. simpl in H6.
unfold ID_AT_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) 1); [ | inv H6].
omega. }
assert (posVal: pos = (Int.unsigned offset)).
{ clearAllExceptTwo H6 IdVal0.
rewrite IdVal0 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× rewrite <- posVal. rewrite strsz. rewrite Z.mul_comm.
eassumption.
× apply align_le. omega.
× rewrite <- posVal. rewrite strsz. rewrite Z.mul_comm.
eassumption.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal1.
unfold index2Z in H6. rewrite IdVal1 in H6. simpl in H6.
unfold ID_TCB_range in H6; simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = ID_AT_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal1.
rewrite IdVal1 in H6.
unfold index2Z in H6.
simpl in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz. rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
eassumption.
× apply align_le. omega.
× unfold ID_AT_range in posVal.
change (0 + 1 + Int.unsigned offset) with (1 + Int.unsigned offset).
rewrite <- posVal.
rewrite strsz. rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
eassumption.
-
assert (offsetRange: 0 ≤ Int.unsigned offset < num_chan).
{ clearAllExceptTwo H6 IdVal2.
unfold index2Z in H6. rewrite IdVal2 in H6.
unfold ID_SC_range in H6.
unfold index_range in H6.
unfold index_incrange in H6.
unfold ID_SC_range in H6.
destruct (zle_lt 0 (Int.unsigned offset) num_chan); [ | inv H6].
omega. }
assert (posVal: pos = lock_TCB_range + Int.unsigned offset).
{ clearAllExceptTwo H6 IdVal2.
rewrite IdVal2 in H6.
unfold index2Z in H6.
unfold index_range in H6.
unfold index_incrange in H6.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range); [ | inv H6].
inv H6; reflexivity. }
esplit.
repeat vcgen.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
repeat vcgen.
× apply align_le. omega.
× unfold lock_TCB_range in posVal.
unfold ID_AT_range, ID_TCB_range in posVal.
rewrite strsz.
change (0 + 1 + num_chan + Int.unsigned offset) with (1 + num_chan + Int.unsigned offset).
rewrite <- posVal.
rewrite Z.mul_comm.
change (0 + pos × 8) with (pos × 8).
repeat vcgen.
Qed.
End InitTicketBody.
Theorem init_ticket_code_correct:
spec_le (init_ticket ↦ init_ticket_spec_low) (〚init_ticket ↦ f_init_ticket 〛L).
Proof.
fbigstep_pre L.
destruct Hkern.
simpl in ×.
generalize hinv; intro.
inv hinv.
assert (posRange: 0 ≤ pos < lock_range).
{
clearAllExceptOne Hpos.
unfold index2Z in Hpos.
unfold index_range in Hpos.
destruct (Int.unsigned i).
unfold index_incrange in Hpos.
destruct (index_incrange 0); [ | inv Hpos].
destruct (zle_lt 0 (Int.unsigned ofs) ID_AT_range); [ | inv Hpos].
unfold ID_AT_range in ×. inv Hpos. unfold lock_range.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
destruct (zle_lt 0 (Int.unsigned ofs) (ID_AT_range)).
inv H0. unfold ID_AT_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv H0.
destruct p; try (inv Hpos; fail).
destruct p; try (inv Hpos; fail).
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_SC_range) in Hpos.
inv Hpos.
unfold ID_SC_range, lock_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
unfold index_incrange in Hpos.
destruct ( zle_lt 0 (Int.unsigned ofs) ID_TCB_range) in Hpos.
inv Hpos.
unfold ID_TCB_range, lock_range in ×.
unfold ID_AT_range, ID_TCB_range, ID_SC_range. omega.
inv Hpos.
inv Hpos.
}
assert (lockRangeVal: lock_range = num_chan + num_chan + 1).
{ unfold lock_range; reflexivity. }
fbigsteptest (init_ticket_body_correct s (Genv.globalenv p) makeglobalenv b Hsymbol b2 Hb2fs Hb2fp m0 m1 m´0 d d´
(PTree.empty _) (bind_parameter_temps´
(fn_params f_init_ticket)
(Vint i::(Vint ofs::nil))
(create_undef_temps (fn_temps f_init_ticket)))) valid_curid;
try reflexivity.
replace (pos × 8 + 0) with (pos × 8); try omega.
rewrite Hstore0; reflexivity.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End INITTICKET.
End WithPrimitives.
Transparent Z.add Z.sub Z.mul Z.div sizeof align.
End MCURIDCODE.