Require Import Coqlib Maps Integers Values Memdata.
Require Import Blockset Memory Injections InjRels.
Import Mem.
Memory Closures
This file defines closures on memory
Local Notation "
a #
b" := (
PMap.get b a) (
at level 1).
Inductive reach' (
m:
mem) (
B:
Bset.t) :
list (
block *
ptrofs) ->
block ->
Prop :=
|
reach_nil:
forall b,
Bset.belongsto B b ->
reach'
m B nil b
|
reach_cons:
forall b L b'
z ofs q n,
reach'
m B L b' ->
perm m b'
z Max Readable ->
ZMap.get z (
mem_contents m)!!
b' =
Fragment (
Vptr b ofs)
q n->
reach'
m B ((
b',
ofs)::
L)
b.
Inductive reachable :
mem ->
Bset.t ->
block ->
Prop :=
Reachable :
forall m bs b L,
reach'
m bs L b ->
reachable m bs b.
MODIFICATION:
strengthen reach_closed, requiring memory contains no Vundef / Undef values within block set of interest
Record reach_closed (
m:
mem) (
B:
Bset.t) :
Prop :=
{
reachable_closure:
forall b,
reachable m B b ->
Bset.belongsto B b;
no_undef:
forall b z,
Bset.belongsto B b ->
perm m b z Max Readable ->
(~
ZMap.get z (
mem_contents m) !!
b =
Undef);
no_vundef:
forall b z q n,
Bset.belongsto B b ->
perm m b z Max Readable ->
(~
ZMap.get z (
mem_contents m) !!
b =
Fragment Vundef q n);
}.
Lemma reach_closed_belongsto:
forall m B b,
reach_closed m B ->
reachable m B b ->
Bset.belongsto B b.
Proof.
intros. inv H. inv H0. apply reachable_closure0.
econstructor; eauto.
Qed.
Lemma bset_eq_reach'
_local:
forall bs1 bs2,
(
forall b,
bs1 b <->
bs2 b) ->
forall m L b,
reach'
m bs1 L b <->
reach'
m bs2 L b.
Proof.
intros bs1 bs2 EQ m.
induction L.
-
split;
intro H;
inversion H;
constructor;
unfold Bset.belongsto in *;
apply EQ;
auto.
-
split;
intros H;
inversion H;
subst;
simpl in *.
econstructor;
eauto.
apply IHL.
auto.
econstructor;
eauto.
apply IHL.
auto.
Qed.
Lemma bset_eq_reachable_local:
forall bs1 bs2 m,
(
forall b,
bs1 b <->
bs2 b) ->
(
forall b,
reachable m bs1 b <->
reachable m bs2 b).
Proof.
clear. intros.
split; intros.
- inversion H0. subst.
rewrite bset_eq_reach'_local in H1; eauto.
econstructor; eauto.
- inversion H0. subst.
rewrite bset_eq_reach'_local in H1; eauto.
econstructor; eauto. firstorder.
Qed.
Lemma bset_eq_reach_closed_local:
forall bs1 bs2 m,
(
forall b,
bs1 b <->
bs2 b) ->
reach_closed m bs1 <->
reach_closed m bs2.
Proof.
clear.
intros.
split;
intros.
-
inversion H0.
constructor.
intros.
erewrite bset_eq_reachable_local in H1;
eauto.
eapply H.
eapply reachable_closure0.
eauto.
split;
intro;
apply H;
auto.
intros.
rewrite <-
H in H1.
eauto.
intros.
rewrite <-
H in H1.
eauto.
-
inversion H0.
constructor.
intros.
erewrite bset_eq_reachable_local in H1;
eauto.
rewrite H.
apply reachable_closure0.
auto.
intros.
rewrite H in H1.
eauto.
intros.
rewrite H in H1.
eauto.
Qed.
TODO: move to LDSimDefs_local?
Lemma sep_inject_rc_inject:
forall mu j m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
sep_inject (
Bset.inj_to_meminj (
inj mu))
j ->
inject j m m' ->
reach_closed m (
SharedSrc mu) ->
inject (
Bset.inj_to_meminj (
inj mu))
m m'.
Proof.
intros mu j m m'
INJECT INCR SEPINJ MEMINJ RC.
constructor.
*
constructor.
**
intros.
eapply mi_perm.
inv MEMINJ;
eauto.
eapply INCR;
eauto.
auto.
**
intros.
eapply mi_align.
inv MEMINJ;
eauto.
eapply INCR;
eauto.
eauto.
**
intros.
exploit mi_memval.
inv MEMINJ;
eauto.
eapply INCR;
eauto.
eauto.
intro MEMVALINJ.
inv MEMVALINJ;
try constructor.
inv H3;
try constructor.
simpl.
econstructor;
eauto.
exploit reachable_closure;
eauto.
econstructor.
instantiate (2:=(
b1,
ofs1)::
nil).
econstructor.
constructor.
eapply Bset.inj_dom'.
inv INJECT;
eauto.
unfold Bset.inj_to_meminj in H.
destruct (
inj mu b1);
inv H;
eauto.
eauto.
eauto.
intro.
exploit Bset.inj_dom;
eauto.
intros [
b'
INJ].
unfold Bset.inj_to_meminj in *.
destruct (
inj mu b0)
eqn:?;
inv INJ.
exploit INCR.
rewrite Heqo;
eauto.
intro.
rewrite H4 in H5;
inv H5;
auto.
*
intros.
unfold Bset.inj_to_meminj;
destruct (
inj mu b)
eqn:
INJ;
auto.
exfalso.
eapply mi_freeblocks in H;
eauto.
exploit INCR.
unfold Bset.inj_to_meminj;
rewrite INJ;
eauto.
congruence.
*
inv MEMINJ.
eauto.
*
inv MEMINJ.
unfold meminj_no_overlap in *;
intros;
eauto.
*
inv MEMINJ.
eauto.
*
inv MEMINJ.
eauto.
Qed.
Lemma sep_inject_rely_inject:
forall mu j m1 m1'
m2 m2',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
sep_inject (
Bset.inj_to_meminj (
inj mu))
j ->
inject j m1 m1' ->
unchanged_on (
fun b _ => ~
SharedSrc mu b)
m1 m2 ->
reach_closed m2 (
SharedSrc mu) ->
unchanged_on (
fun b _ => ~
SharedTgt mu b)
m1'
m2' ->
reach_closed m2' (
SharedTgt mu) ->
inject (
Bset.inj_to_meminj (
inj mu))
m2 m2' ->
inject j m2 m2'.
Proof.
Lemma unchanged_on_reach_closed:
forall m B m',
reach_closed m B ->
Mem.unchanged_on (
fun b _ =>
B b)
m m' ->
(
forall b,
Bset.belongsto B b ->
Mem.valid_block m b) ->
reach_closed m'
B.
Proof.
intros.
constructor;
intros.
*
destruct H as [
CLOSED _ _].
apply CLOSED.
inv H2.
apply Reachable with L.
revert L b H.
induction L.
intros.
constructor;
inv H;
auto.
intros.
inv H.
destruct H0 as [
NEXT PERM CONTENT].
rewrite <-
PERM in H5;[|
apply CLOSED;
auto|].
rewrite CONTENT in H7;
auto.
econstructor;
eauto.
apply CLOSED.
econstructor.
eauto.
econstructor;
eauto.
apply H1.
apply CLOSED.
econstructor;
eauto.
*
erewrite <-
unchanged_on_perm in H3;
eauto.
erewrite unchanged_on_contents;
eauto.
inv H;
eauto.
*
erewrite <-
unchanged_on_perm in H3;
eauto.
erewrite unchanged_on_contents;
eauto.
inv H;
eauto.
Qed.
Lemma unchanged_on_reach_closed_inverse:
forall m B m',
reach_closed m'
B ->
Mem.unchanged_on (
fun b _ =>
B b)
m m' ->
(
forall b,
Bset.belongsto B b ->
Mem.valid_block m b) ->
reach_closed m B.
Proof.
intros.
constructor;
intros.
*
destruct H as [
CLOSED _ _].
apply CLOSED.
inv H2.
apply Reachable with L.
revert L b H.
induction L.
intros.
constructor;
inv H;
auto.
intros.
inv H.
destruct H0 as [
NEXT PERM CONTENT].
pose proof H5 as READABLE.
rewrite PERM in H5;[|
apply CLOSED;
auto|].
rewrite <-
CONTENT in H7;
auto.
econstructor;
eauto.
apply CLOSED.
econstructor.
eauto.
econstructor;
eauto.
apply H1.
apply CLOSED.
econstructor;
eauto.
*
pose proof H3 as READABLE.
erewrite unchanged_on_perm in H3;
eauto.
erewrite <-
unchanged_on_contents;
eauto.
inv H;
eauto.
*
pose proof H3 as READABLE.
erewrite unchanged_on_perm in H3;
eauto.
erewrite <-
unchanged_on_contents;
eauto.
inv H;
eauto.
Qed.
An invariant for RC preservation
Record unmapped_closed (
mu:
Mu) (
m m':
mem) :
Prop :=
{
unmapped_closure:
forall b'
z b0 ofs0 q n,
Bset.belongsto (
SharedTgt mu)
b' ->
(
forall b, (
inj mu)
b =
Some b' -> ~
perm m b z Max Readable) ->
perm m'
b'
z Max Readable ->
ZMap.get z (
mem_contents m') !!
b' =
Fragment (
Vptr b0 ofs0)
q n ->
Bset.belongsto (
SharedTgt mu)
b0;
unmapped_no_undef:
forall b'
z,
Bset.belongsto (
SharedTgt mu)
b' ->
(
forall b, (
inj mu)
b =
Some b' -> ~
perm m b z Max Readable) ->
perm m'
b'
z Max Readable ->
ZMap.get z (
mem_contents m') !!
b' <>
Undef;
unmapped_no_vundef:
forall b'
z q n,
Bset.belongsto (
SharedTgt mu)
b' ->
(
forall b, (
inj mu)
b =
Some b' -> ~
perm m b z Max Readable) ->
perm m'
b'
z Max Readable ->
ZMap.get z (
mem_contents m') !!
b' <>
Fragment Vundef q n;
}.
Lemma reach_closed_unmapped_closed:
forall mu m m',
reach_closed m' (
SharedTgt mu) ->
unmapped_closed mu m m'.
Proof.
intros.
constructor;
inv H;
auto.
intros.
eapply reachable_closure0.
econstructor.
instantiate(1:=(
b',
ofs0)::
nil).
econstructor;
eauto.
constructor;
auto.
Qed.
Lemma inject_shared_src_valid:
forall mu j m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
inject j m m' ->
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m b).
Proof.
Lemma inject_shared_tgt_valid:
forall mu j m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
inject j m m' ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m'
b).
Proof.
Lemma unmapped_closed_reach_closed_preserved_by_extends:
forall mu m m',
inject_incr (
Bset.inj_to_meminj (
inj mu))
inject_id ->
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
valid_block m b) ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
valid_block m'
b) ->
extends m m' ->
unmapped_closed mu m m' ->
reach_closed m (
SharedSrc mu) ->
reach_closed m' (
SharedTgt mu).
Proof.
intros.
assert (
EQS:
forall b,
SharedSrc mu b <->
SharedTgt mu b).
{
intro.
inv H0.
split;
intro SHARED.
eapply inj_dom in SHARED.
destruct SHARED as [
b'
A].
exploit H.
unfold Bset.inj_to_meminj;
rewrite A;
eauto.
intro.
inv H0.
eapply Bset.inj_range';
eauto.
eapply Bset.inj_range in SHARED;
eauto.
destruct SHARED as [
b'
A].
exploit H.
unfold Bset.inj_to_meminj;
rewrite A;
eauto.
intro.
inv H0.
eapply Bset.inj_dom';
eauto. }
constructor.
*
intros.
inv H6.
revert L b H7.
induction L;
intros.
inv H7.
auto.
inv H7.
apply IHL in H9.
clear IHL.
exploit Bset.inj_range;
eauto.
inv H0;
eauto.
intros (
b'0 &
INJ).
destruct (
perm_dec m b'0
z Max Readable).
mapped *)
exploit mi_memval.
inv H3;
eauto.
eapply H.
unfold Bset.inj_to_meminj;
rewrite INJ.
eauto.
eauto.
rewrite Z.add_0_r,
H12.
intro INJVAL;
inv INJVAL.
inv H8.
inv H14.
exploit H.
unfold Bset.inj_to_meminj.
rewrite INJ.
eauto.
intro A;
inv A.
eapply EQS.
eapply reachable_closure;
eauto.
apply Reachable with ((
b',
ofs1)::
nil).
econstructor;
eauto.
constructor.
apply EQS.
auto.
exfalso.
eapply no_vundef;
eauto.
eapply Bset.inj_dom';
eauto.
inv H0;
eauto.
exfalso.
eapply no_undef;
eauto.
eapply Bset.inj_dom';
eauto.
inv H0;
eauto.
unmapped *)
eapply unmapped_closure;
eauto.
intros.
exploit Bset.inj_injective.
inv H0;
eauto.
exact INJ.
exact H6.
intro EQ;
subst;
auto.
*
intros.
exploit Bset.inj_range;
eauto.
inv H0;
eauto.
intros (
b0 &
INJ).
destruct (
perm_dec m b0 z Max Readable).
exploit mi_memval.
inv H3;
eauto.
eapply H.
unfold Bset.inj_to_meminj;
rewrite INJ.
eauto.
eauto.
rewrite Z.add_0_r.
intro INJVAL;
inv INJVAL;
try discriminate.
exfalso.
eapply no_undef;
eauto.
eapply Bset.inj_dom';
eauto.
inv H0;
eauto.
eapply unmapped_no_undef;
eauto.
intros.
exploit Bset.inj_injective.
inv H0;
eauto.
exact INJ.
exact H8.
intro EQ;
subst;
auto.
*
intros.
exploit Bset.inj_range;
eauto.
inv H0;
eauto.
intros (
b0 &
INJ).
destruct (
perm_dec m b0 z Max Readable).
exploit mi_memval.
inv H3;
eauto.
eapply H.
unfold Bset.inj_to_meminj;
rewrite INJ.
eauto.
eauto.
rewrite Z.add_0_r.
intro INJVAL;
inv INJVAL;
try discriminate.
inv H10;
try discriminate.
exfalso.
eapply no_vundef;
eauto.
eapply Bset.inj_dom';
eauto.
inv H0;
eauto.
exfalso.
eapply no_undef;
eauto.
eapply Bset.inj_dom';
eauto.
inv H0;
eauto.
eapply unmapped_no_vundef;
eauto.
intros.
exploit Bset.inj_injective.
inv H0;
eauto.
exact INJ.
exact H8.
intro EQ;
subst;
auto.
Qed.
Lemma unmapped_closed_reach_closed_preserved_by_injection:
forall mu m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
valid_block m b) ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
valid_block m'
b) ->
inject (
Bset.inj_to_meminj (
inj mu))
m m' ->
unmapped_closed mu m m' ->
reach_closed m (
SharedSrc mu) ->
reach_closed m' (
SharedTgt mu).
Proof.
Lemma unmapped_closed_reach_closed_preserved_by_injection':
forall mu m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject (
Bset.inj_to_meminj (
inj mu))
m m' ->
unmapped_closed mu m m' ->
reach_closed m (
SharedSrc mu) ->
reach_closed m' (
SharedTgt mu).
Proof.
Lemma unmapped_closed_reach_closed_preserved_by_injection'':
forall mu j m m',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
sep_inject (
Bset.inj_to_meminj (
inj mu))
j ->
inject j m m' ->
unmapped_closed mu m m' ->
reach_closed m (
SharedSrc mu) ->
reach_closed m' (
SharedTgt mu).
Proof.
intros;
eapply unmapped_closed_reach_closed_preserved_by_injection';
eauto.
eapply sep_inject_rc_inject;
eauto.
Qed.
Lemma unchanged_on_unmapped_closed_preserved:
forall mu m1 m1'
m2 m2',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
valid_block m1 b) ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
valid_block m1'
b) ->
unmapped_closed mu m1 m1' ->
unchanged_on (
fun b _ =>
SharedSrc mu b)
m1 m2 ->
unchanged_on (
fun b _ =>
SharedTgt mu b)
m1'
m2' ->
unmapped_closed mu m2 m2'.
Proof.
Lemma unchanged_on_reach_closed_preserved:
forall mu m1 m1'
m2 m2',
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
valid_block m1 b) ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
valid_block m1'
b) ->
(
reach_closed m1 (
SharedSrc mu) ->
reach_closed m1' (
SharedTgt mu)) ->
unchanged_on (
fun b _ =>
SharedSrc mu b)
m1 m2 ->
unchanged_on (
fun b _ =>
SharedTgt mu b)
m1'
m2' ->
(
reach_closed m2 (
SharedSrc mu) ->
reach_closed m2' (
SharedTgt mu)).
Proof.
Lemma store_val_inject_unmapped_closed_preserved:
forall mu m1 m1'
chunk j b ofs v m2 b'
delta v'
m2',
Bset.inject (
inj mu) (
SharedSrc mu) (
SharedTgt mu) ->
(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
valid_block m1 b) ->
(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
valid_block m1'
b) ->
inject_incr (
Bset.inj_to_meminj (
inj mu))
j ->
sep_inject (
Bset.inj_to_meminj (
inj mu))
j ->
unmapped_closed mu m1 m1' ->
store chunk m1 b ofs v =
Some m2 ->
j b =
Some (
b',
delta) ->
store chunk m1'
b' (
ofs +
delta)
v' =
Some m2' ->
unmapped_closed mu m2 m2'.
Proof.
Lemma free_inject_unmapped_closed_preserved:
forall mu m1 m1'
j b lo hi m2 b'
delta lo'
hi'
m2',
Bset.inject (
Injections.inj mu) (
Injections.SharedSrc mu) (
Injections.SharedTgt mu) ->
(
forall b0 :
block,
Bset.belongsto (
Injections.SharedSrc mu)
b0 ->
Mem.valid_block m1 b0) ->
(
forall b0 :
block,
Bset.belongsto (
Injections.SharedTgt mu)
b0 ->
Mem.valid_block m1'
b0) ->
inject_incr (
Bset.inj_to_meminj (
Injections.inj mu))
j ->
sep_inject (
Bset.inj_to_meminj (
Injections.inj mu))
j ->
unmapped_closed mu m1 m1' ->
Mem.free m1 b lo hi =
Some m2 ->
j b =
Some (
b',
delta) ->
lo' <= (
lo +
delta) ->
(
hi +
delta) <=
hi' ->
Mem.free m1'
b'
lo'
hi' =
Some m2' ->
unmapped_closed mu m2 m2'.
Proof.