Require Import Coqlib Utf8.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require Import INJECT.
Require Import Classical.
Require Import Utils.
Require Import Emem Permissions MemoryMachine TSOMemoryMachine RefinesDefs RefinesUtils AllRefinesRulesAux.
Require Import RefinesRules.
Require Import RefinesRules2.
Import Bigstep.
Lemma refines_elim_fence:
refines (
Sfence false)
Sskip.
Proof.
unfold refines;
intros.
inv H.
inv H0.
rewrite <- (
app_nil_l (
tr0++
tr')).
econstructor;
eauto.
econstructor;
eauto.
Qed.
Lemma ext_trace_interleaved :
forall l st af s0 s1,
ext_trace st af s0 l s1 ->
ext_trace st Interleaved s0 l s1.
Proof.
induction l; intros.
inversion_clear H; clarify.
econstructor; eauto.
econstructor; eauto.
econstructor; eauto.
inversion H; clarify.
rewrite H0; auto.
Qed.
Lemma unbuf_perm :
forall st m b m'
b',
unbuffer st (
m,
b) (
m',
b') ->
perms m =
perms m'.
Proof.
intros.
inversion_clear H; clarify.
inversion HU3; clarify.
Qed.
Lemma star_perm :
forall st s0 s1,
star (
unbuffer st) (
s0) (
s1) ->
perms (
fst s0) =
perms (
fst s1).
Proof.
intros.
induction H;
clarify.
eapply (
unbuf_perm st _ (
snd x)
_ (
snd y));
eauto.
destruct x;
destruct y;
eauto.
congruence.
Qed.
Lemma flush_perm :
forall st b s0 s1,
flush st b s0 s1 ->
perms s0 =
perms s1.
Proof.
unfold flush;
intros.
exploit star_perm;
eauto.
Qed.
Definition has_no_perm (
t:
thread_id) (
d:
perm_map) :
Prop :=
forall p,
is_free t (
d p).
Lemma mem_same_perm :
forall t t'
l st0 st1 a p,
t <>
t' ->
mem_trace t'
a st0 l st1 ->
is_free t ((
perms st0)
p) ->
is_free t ((
perms st1)
p).
Proof.
induction 2;
intros;
clarify.
clear TM3.
exploit IHmem_trace;
eauto.
intro.
inversion TM2;
simpl in *;
clarify.
inversion ESD;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
unfold is_free;
unfold has_store_perm in ESD0.
destruct (
d p0);
clarify.
rewrite perm_gss;
simpl;
auto.
rewrite perm_gss;
simpl;
auto.
erewrite perm_gso;
eauto;
simpl;
auto.
inversion_clear ESD0;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
rewrite URP1 in H2.
rewrite perm_gss;
simpl;
auto.
erewrite perm_gso;
eauto;
simpl;
auto.
specialize (
ESP p);
inversion ESP;
clarify.
rewrite <-
H3 in H2.
unfold is_free in H2.
simpl;
eauto.
rewrite <-
H4 in H2;
unfold is_free in *.
rewrite Rset.mem_rmo;
eauto.
destruct released;
clarify.
inversion TM2;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
specialize (
ESP p0);
inversion ESP;
clarify.
rewrite ESD in H3;
congruence.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
specialize (
ESP0 p);
inversion ESP0;
clarify.
destruct (
eq_dec t t'0);
clarify.
rewrite <-
H3 in H2;
simpl in H2;
congruence.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
destruct released;
clarify.
inversion TM2;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
specialize (
ESP p0);
inversion ESP;
clarify.
rewrite <-
H3 in H2.
simpl in H2;
auto.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
specialize (
ESP0 p);
inversion ESP0;
clarify.
destruct (
eq_dec t t'0);
clarify.
rewrite <-
H3 in H2;
simpl in H2;
congruence.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
destruct r;
clarify.
inversion TM2;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
specialize (
ESP p0);
inversion ESP;
clarify.
rewrite <-
H3 in H2.
simpl in H2;
auto.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
specialize (
ESP0 p);
inversion ESP0;
clarify.
destruct (
eq_dec t t'0);
clarify.
rewrite <-
H3 in H2;
simpl in H2;
congruence.
rewrite <-
H4 in H2.
unfold is_free in *;
rewrite Rset.mem_rmo;
eauto.
Qed.
Lemma same_perm_ext :
forall t a st0 l st1 p,
ext_trace t a st0 l st1 ->
is_free t ((
perms (
fst st0))
p) ->
is_free t ((
perms (
fst st1))
p).
Proof.
intros.
induction H;
clarify.
simpl in *.
eapply (
IHext_trace);
eauto.
assert (
t <>
t0)
by auto.
eapply (
mem_same_perm t t0 e m1 m2 (
safe t b2)
p H2 H H0);
eauto.
eapply (
IHext_trace);
eauto.
simpl in *.
assert (
perms m1 =
perms m2)
by (
eapply unbuf_perm;
eauto).
rewrite <-
H2;
auto.
Qed.
Hint Resolve same_perm_ext.
Lemma mem_no_perm :
forall t t'
l st0 st1 a,
t <>
t' ->
has_no_perm t (
perms st1) ->
mem_trace t'
a st0 l st1 ->
has_no_perm t (
perms st0).
Proof.
induction 3;
intros;
clarify.
clear TM3.
eapply IHmem_trace;
clear IHmem_trace.
intro.
inversion TM2;
simpl in *;
clarify.
inversion ESD;
simpl in *;
clarify.
destruct (
Ptr.eq_dec p p0);
subst.
unfold is_free;
unfold has_store_perm in ESD0.
destruct (
d p0);
clarify.
destruct (
Rset.subset_singleton _ _ ESD0);
subst;
eauto.
unfold Rset.singleton;
erewrite Rset.add_mem_o;
eauto.
specialize (
H0 p);
rewrite perm_gso in H0;
auto.
inversion_clear TM2;
simpl in *;
clarify.
inversion_clear ESD0;
simpl in *;
clarify.
unfold is_free;
unfold has_no_perm in H0.
specialize (
H0 p);
destruct (
Ptr.eq_dec p p0);
subst;
auto.
rewrite perm_gss in H0;
auto.
destruct (
d p0);
clarify.
unfold is_free in H0;
erewrite Rset.add_mem_o in H0;
eauto.
rewrite perm_gso in H0;
auto.
inversion ESD;
clarify.
specialize (
ESP0 p).
destruct (
d p);
clarify.
inversion ESP0;
clarify.
destruct (
eq_dec t t0);
clarify.
specialize (
H0 p);
rewrite <-
H3 in H0;
congruence.
specialize (
H0 p).
destruct (
d'
p);
clarify.
inversion ESP0;
clarify.
inversion ESP0;
clarify.
unfold is_free in H0.
erewrite Rset.mem_rmo in H0;
eauto.
destruct released;
clarify.
inversion_clear TM2;
simpl in *;
clarify.
inversion_clear ESD0;
simpl in *;
clarify.
unfold is_free;
unfold has_no_perm in H0.
specialize (
ESP0 p).
specialize (
H0 p);
destruct (
Ptr.eq_dec p p0);
subst;
auto.
rewrite ESD in ESP0;
inversion ESP0.
rewrite H3 in ESP0;
congruence.
rewrite ESD;
simpl;
auto.
inversion ESP0;
clarify.
destruct (
eq_dec t t'0);
clarify.
rewrite <-
H3 in H0.
unfold is_free in H0;
congruence.
rewrite <-
H4 in H0.
unfold is_free in H0.
erewrite Rset.mem_rmo in H0;
eauto.
destruct released;
clarify.
inversion_clear TM2;
simpl in *;
clarify.
inversion_clear ESD0;
simpl in *;
clarify.
unfold is_free;
unfold has_no_perm in H0.
specialize (
ESP0 p).
specialize (
H0 p);
destruct (
Ptr.eq_dec p p0);
subst;
auto.
rewrite ESD1 in ESP0;
inversion ESP0.
rewrite <-
H3 in ESP0;
congruence.
rewrite ESD1 in H0;
rewrite <-
H4 in H0.
unfold is_free in H0.
erewrite Rset.mem_rmo in H0;
eauto.
inversion ESP0;
clarify.
destruct (
eq_dec t t'0);
clarify.
rewrite <-
H3 in H0.
unfold is_free in H0;
congruence.
rewrite <-
H4 in H0.
unfold is_free in H0.
erewrite Rset.mem_rmo in H0;
eauto.
destruct r;
clarify.
inversion_clear TM2;
simpl in *;
clarify.
inversion_clear ESD0;
simpl in *;
clarify.
unfold is_free;
unfold has_no_perm in H0.
specialize (
ESP0 p);
specialize (
H0 p);
destruct (
Ptr.eq_dec p p0);
subst;
auto.
destruct (
d p0);
clarify.
rewrite ESD in ESP0;
inversion ESP0;
clarify.
destruct (
d'
p0);
clarify.
assert (
t' <>
t)
by auto.
apply (
release_perm_o H2)
in ESP0.
rewrite ESP0;
auto.
inversion ESP0;
clarify.
rewrite <-
H3 in H0.
unfold is_free in H0;
auto.
rewrite <-
H4 in H0;
clarify.
unfold is_free in H0.
erewrite Rset.mem_rmo in H0;
eauto.
Qed.
Lemma no_perm_mem :
forall t t'
l st0 st1 a,
t <>
t' ->
has_no_perm t (
perms st0) ->
mem_trace t'
a st0 l st1 ->
has_no_perm t (
perms st1).
Proof.
induction l;
intros;
clarify.
inversion H1;
clarify.
inversion_clear H1;
clarify.
assert (
has_no_perm t m').
intro.
exploit IHl;
eauto.
destruct m'.
unfold has_no_perm in *;
intros.
inversion_clear TM2;
simpl;
clarify.
destruct ESD;
clarify.
simpl in *.
unfold upd_perm.
destruct (
Ptr.eq_dec p p0);
clarify.
inversion_clear ESD;
clarify.
unfold upd_perm.
destruct (
Ptr.eq_dec p p0);
clarify.
simpl.
simpl in H1.
assert (
is_free t (
d p0))
by auto.
unfold is_free in H2.
destruct (
d p0);
clarify.
rewrite <-
H2.
eapply Rset.add_mem_o;
eauto.
unfold release in ESP.
assert (
release_perm t' (
d p) (
d'
p))
by auto.
inversion H2.
rewrite H3;
auto.
unfold is_free.
simpl.
auto with datatypes.
unfold is_free.
assert (
is_free t (
d p))
by auto.
rewrite <-
H4 in H3;
simpl in H3.
rewrite <-
H3.
erewrite (
Rset.mem_rmo);
eauto.
unfold release in ESP.
destruct released;
clarify.
assert (
is_free t (
perms p))
by auto.
assert (
release_perm t' (
perms p) (
d'
p))
by auto.
inversion H3;
clarify.
rewrite <-
H4 in H2;
auto.
unfold is_free in *.
rewrite <-
H5 in H2.
rewrite <-
H2.
erewrite (
Rset.mem_rmo);
eauto.
unfold release in ESP.
destruct released;
clarify.
assert (
is_free t (
perms p))
by auto.
assert (
release_perm t' (
perms p) (
d'
p))
by auto.
inversion H3;
clarify.
rewrite <-
H4 in H2;
auto.
unfold is_free.
rewrite <-
H5 in H2.
unfold is_free in H2.
rewrite <-
H2.
erewrite (
Rset.mem_rmo);
eauto.
unfold release in ESP.
destruct r;
clarify.
assert (
is_free t (
perms p))
by auto.
assert (
release_perm t' (
perms p) (
d'
p))
by auto.
inversion H3;
clarify.
rewrite <-
H4 in H2;
auto.
unfold is_free.
rewrite <-
H5 in H2.
unfold is_free in H2.
rewrite <-
H2.
erewrite (
Rset.mem_rmo);
eauto.
Qed.
Lemma ext_no_perm :
forall t st0 l st1,
has_no_perm t (
perms (
fst st1)) ->
ext_trace t Interleaved st0 l st1 ->
has_no_perm t (
perms (
fst st0)).
Proof.
intros.
induction H0;
clarify.
simpl in *.
unfold has_no_perm in *.
inversion H0;
clarify.
eapply (
IHext_trace);
eauto.
specialize (
IHext_trace H).
eapply mem_no_perm;
eauto.
specialize (
IHext_trace H).
assert (
perms m1 =
perms m2)
by (
eapply unbuf_perm;
eauto).
destruct m1;
destruct m2;
simpl in *.
rewrite <-
H2 in IHext_trace;
auto.
Qed.
Lemma no_perm_ext :
forall t st0 l st1,
has_no_perm t (
perms (
fst st0)) ->
ext_trace t Interleaved st0 l st1 ->
has_no_perm t (
perms (
fst st1)).
Proof.
intros.
induction H0;
clarify.
simpl in *.
unfold has_no_perm in *.
intros.
eapply (
IHext_trace);
eauto.
assert (
t <>
t0)
by auto.
eapply (
no_perm_mem t t0 e m1 m2 (
safe t b2)
H2 H H0);
eauto.
eapply (
IHext_trace);
eauto.
unfold has_no_perm in *.
intro;
simpl in *.
assert (
perms m1 =
perms m2)
by (
eapply unbuf_perm;
eauto).
rewrite <-
H2;
auto.
Qed.
Lemma release_no_perm :
forall t m m',
mem_step t m (
MEperm PErelease)
m' ->
has_no_perm t m'.
Proof.
intros.
inversion_clear H;
clarify.
unfold has_no_perm;
simpl;
intros.
inversion_clear ESD;
clarify.
unfold release in ESP.
assert (
release_perm t (
d p) (
d'
p))
by auto;
inversion H;
clarify.
Qed.
Lemma no_perm_release :
forall t (
m:
mem),
has_no_perm t m ->
mem_step t m (
MEperm PErelease)
m.
Proof.
intros.
destruct m.
econstructor;
eauto.
econstructor;
eauto.
simpl in H.
eapply release_func.
eapply extensionality;
intro.
assert (
is_free t (
perms x))
by auto;
clear H.
unfold is_free in H0.
destruct (
perms x);
clarify.
destruct (
peq t t0);
clarify.
erewrite Rset.not_mem_remove_nop;
eauto.
rewrite H0;
auto.
Qed.
Lemma no_perm_freeperm :
forall t (
m:
mem),
has_no_perm t m ->
mem_step t m (
MEperm PEfreeperm)
m.
Proof.
intros.
destruct m.
econstructor; eauto.
econstructor; eauto.
Qed.
Lemma refines_skip_atomic :
forall f stmt,
refines
(
Sseq Sskip (
Satomic f stmt))
(
Satomic f (
Sseq Sskip stmt)).
Proof.
intros.
unfold refines;
intros.
inversion_clear H;
clarify.
inversion_clear H0;
clarify.
inversion_clear H;
clarify.
simpl.
econstructor;
eauto.
inversion_clear H2;
clarify.
econstructor;
eauto.
simpl;
split;
auto.
replace (
nil (
A := (
positive *
ext_event)))
with
((
nil (
A := (
positive *
ext_event))) ++ (
nil (
A := (
positive *
ext_event))))
by auto with datatypes.
econstructor;
eauto.
econstructor;
eauto.
inversion H;
clarify.
congruence.
Qed.
Lemma flush_empty :
forall t st st',
let m :=
fst st in
let b :=
snd st in
let c :=
snd st'
in
b =
empty_buffer ->
star (
unbuffer t)
st st' ->
c =
empty_buffer.
Proof.
intros.
induction H0.
subst.
replace x with (
m,
empty_buffer)
in H0.
inversion H0;
clarify.
destruct b';
clarify.
destruct x;
simpl;
auto.
simpl in *.
rewrite H.
replace m0 with m by eauto;
auto.
subst.
rewrite <-
H;
auto.
eapply IHclos_refl_trans2;
eauto.
Qed.
Lemma flush_empty' :
forall t st st',
let m :=
fst st in
let b :=
snd st in
let d :=
fst st'
in
let c :=
snd st'
in
b =
empty_buffer ->
star (
unbuffer t)
st st' ->
c =
empty_buffer /\
m =
d.
Proof.
intros.
induction H0.
subst.
replace x with (
m,
empty_buffer)
in H0.
inversion H0;
clarify.
destruct b';
clarify.
destruct x;
simpl;
auto.
simpl in *.
rewrite H.
replace m0 with m by eauto;
auto.
subst.
rewrite <-
H;
auto.
destruct IHclos_refl_trans1;
clarify.
destruct IHclos_refl_trans2;
clarify.
replace c with (
snd z)
by auto.
replace m with (
fst x)
by auto.
replace d with (
fst z)
by auto.
split;
auto.
rewrite H1;
auto.
Qed.
Lemma list_back :
forall (
A:
Type) (
a:
A)
b l l',
l ++ (
a ::
nil) =
l' ++ (
b ::
nil) ->
l =
l' /\
a =
b.
Proof.
Lemma unbuf_one :
forall t m b a n m'
b',
unbuffer_n'
t (
m,
b ++ (
a ::
nil)) (
S n) (
m',
b') ->
exists m'',
unbuffer_n'
t (
m,
b ++ (
a ::
nil)) 1 (
m'',
b) /\
unbuffer_n'
t (
m'',
b)
n (
m',
b').
Proof.
intros.
inversion_clear H;
clarify.
destruct mb2;
clarify.
inversion H0;
clarify.
destruct (
list_back _ _ _ _ _ H2);
clarify.
exists m0;
split;
auto.
econstructor;
eauto.
econstructor;
eauto.
Qed.
Lemma flush_ext_trace :
forall t m0 b m1,
flush t b m0 m1 ->
ext_trace t Interleaved (
m0,
b)
nil (
m1,
empty_buffer).
Proof.
intros.
assert (
unbuffer_n'
t (
m0,
b) (
length b) (
m1,
empty_buffer))
by (
eapply flush_unbuffer_n';
eauto);
clear H.
generalize m0 m1 empty_buffer H0;
clear H0.
apply (
rev_ind (
fun b =>
forall (
m2 m3 :
mem) (
b0 :
buffer),
unbuffer_n'
t (
m2,
b) (
length b) (
m3,
b0) ->
ext_trace t Interleaved (
m2,
b)
nil (
m3,
b0)));
intros;
clarify.
inversion H;
clarify.
econstructor;
eauto.
assert (
length (
l ++
x ::
nil) =
S (
length l)).
rewrite app_length;
simpl;
intuition.
rewrite H1 in H0;
clear H1.
destruct (
unbuf_one _ _ _ _ _ _ _ H0)
as [
m [
J1 Jl]].
econstructor;
eauto.
inversion J1;
clarify.
inversion H4;
clarify.
Qed.
Lemma unbufn_release :
forall n b t b0 m0 d0 m1 d1,
unbuffer_n'
t ((
MEM m0 d0),
b)
n ((
MEM m1 d0),
b0) ->
release t d0 d1 ->
unbuffer_n'
t ((
MEM m0 d1),
b)
n ((
MEM m1 d1),
b0).
Proof.
Lemma flush_release :
forall t m0 d0 b m1 d1,
flush t b (
MEM m0 d0) (
MEM m1 d0) ->
release t d0 d1 ->
flush t b (
MEM m0 d1) (
MEM m1 d1).
Proof.
intros.
assert (
unbuffer_n'
t ((
MEM m0 d0),
b) (
length b) ((
MEM m1 d0),
empty_buffer))
by (
eapply flush_unbuffer_n';
eauto);
clear H.
exploit unbufn_release;
eauto;
intro.
eapply unbuffer_n'
_star;
eauto.
Qed.
Lemma unbufn_release_neq :
forall n b t t'
b0 m0 d0 m1 d1,
t' <>
t ->
unbuffer_n'
t ((
MEM m0 d0),
b)
n ((
MEM m1 d0),
b0) ->
release t'
d0 d1 ->
unbuffer_n'
t ((
MEM m0 d1),
b)
n ((
MEM m1 d1),
b0).
Proof.
Lemma flush_release_neq :
forall t t'
m0 d0 b m1 d1,
t' <>
t ->
flush t b (
MEM m0 d0) (
MEM m1 d0) ->
release t'
d0 d1 ->
flush t b (
MEM m0 d1) (
MEM m1 d1).
Proof.
intros.
assert (
unbuffer_n'
t ((
MEM m0 d0),
b) (
length b) ((
MEM m1 d0),
empty_buffer))
by (
eapply flush_unbuffer_n';
eauto);
clear H0.
exploit unbufn_release_neq;
eauto;
intro.
eapply unbuffer_n'
_star;
eauto.
Qed.
Lemma ext_empty_ext :
forall t a st l st',
ext_trace t a st l st' ->
snd st =
empty_buffer ->
snd st' =
empty_buffer.
Proof.
induction 1; clarify.
intros.
apply IHext_trace.
simpl in *; subst.
inversion_clear H.
destruct b2; clarify.
Qed.
Lemma refines_depromotes_abort:
forall r msg,
refines
(
Satomic true (
Sabort Atomic false msg))
(
Sseq (
Sfence false) (
Sabort Interleaved r msg)).
Proof.
unfold refines;
intros.
inversion_clear H;
clarify.
inversion H0;
clarify.
inversion_clear H13;
clarify.
assert(
b'' =
empty_buffer).
replace b''
with (
snd (
m'',
b''))
by auto.
eapply ext_empty_ext;
eauto.
subst.
inv H0.
inv H13.
econstructor;
eauto.
rewrite <- (
app_nil_r tr0).
econstructor.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
econstructor 2.
Qed.
Lemma upd_perm_swap p q d u v :
q â‰
p →
upd_perm (
upd_perm d p u)
q v =
upd_perm (
upd_perm d q v)
p u.
Proof.
intros H.
apply extensionality.
intros x.
case (
eq_dec x q).
intros ->.
perm.
intros Q.
case (
eq_dec x p).
intros ->.
perm.
intros.
perm.
Qed.
Lemma upd_perm_release_swap t t'
p d dr d' :
t â‰
t' →
release t' (
upd_perm d p (
HiddenBy t))
d' →
release t'
d dr →
d' =
upd_perm dr p (
HiddenBy t).
Proof.
intros NE H K.
apply release_func in H.
apply release_func in K.
subst.
apply extensionality.
intros x.
case (
eq_dec p x).
intros ->.
perm.
repeat rewrite peq_false;
auto.
intros K.
perm.
Qed.
Lemma perm_request_mem_step {
t t'
ap a m n m'
e} :
t â‰
t' →
mem_step t m (
MEperm (
PErequest ap a))
n →
mem_step t'
n e m' →
∃
n',
mem_step t'
m e n' ∧
mem_step t n' (
MEperm (
PErequest ap a))
m'.
Proof.
intros NE A B.
inv B.
>
inv ESD.
>
inv A.
assert (
check_perm_store t'
d ap0 p).
inv ESD;
inv ESD0;
perm.
case (
eq_dec p a).
intros ->.
perm.
congruence.
intros.
perm.
vauto.
case (
eq_dec p a).
intros ->.
perm.
congruence.
intros.
perm.
vauto.
inv ESD1.
case (
eq_dec p a).
intros ->.
perm.
congruence.
intros.
perm.
vauto.
inv ESD1.
case (
eq_dec p a).
intros ->.
perm.
clarify.
apply False_ind.
destruct (
Rset.subset_singleton _ _ ALONE).
refine (
Rset.add_not_empty _).
eassumption.
absurd (
Rset.mem t (
Rset.singleton t')).
intros K.
pose proof (
Rset.mem_singleton K).
clarify.
rewrite <-
H.
apply Rset.add_mem.
intros.
perm.
vauto.
econstructor.
split;
vauto.
>
inv ESD0;
inv A;
econstructor;
split;
vauto.
econstructor.
econstructor.
econstructor.
inv ESD;
try inv ESD0;
inv RP;
unfold upd_perm in RP1;
destruct Ptr.eq_dec.
clarify.
vauto.
clarify.
econstructor.
eassumption.
erewrite <-
Rset.add_mem_o.
eassumption.
auto.
vauto.
inv ESD;
try inv ESD0;
unfold upd_perm in RP;
destruct Ptr.eq_dec;
econstructor;
vauto.
econstructor.
econstructor.
autorw'.
>
assert (
p<>
a).
intros ->.
inv A.
inv ESD.
perm.
inv ESD1.
perm.
destruct (
Rset.subset_singleton _ _ ESD0).
apply (
Rset.add_not_empty H).
absurd (
Rset.mem t (
Rset.singleton t')).
intros K.
pose proof (
Rset.mem_singleton K).
clarify.
rewrite <-
H.
apply Rset.add_mem.
destruct m.
inv A;
inv ESD.
perm.
eexists;
split.
vauto.
rewrite upd_perm_swap;
auto.
econstructor.
econstructor;
eauto.
perm.
inv ESD1.
perm.
eexists;
split;
vauto.
econstructor;
eauto.
econstructor;
auto.
econstructor;
eauto.
perm.
eassumption.
apply upd_perm_swap;
auto.
>
inv ESD0.
inv A.
inv ESD.
assert (
p<>
a).
intros ->.
perm.
clarify.
perm.
eexists.
split.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
rewrite upd_perm_swap;
auto.
econstructor;
eauto.
econstructor;
eauto.
perm.
inv ESD0.
case (
eq_dec a p).
intros ->.
perm.
clarify.
eexists.
split.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
perm.
apply extensionality.
intros q.
case (
eq_dec q p).
intros ->.
perm.
f_equal.
apply Rset.add_comm.
intros.
perm.
intros K.
perm.
eexists.
split.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
perm.
eassumption.
rewrite upd_perm_swap;
auto.
>
apply release_func in ESP;
subst.
destruct m as (
m' &
d').
eexists.
split.
econstructor.
econstructor.
apply release_func.
reflexivity.
inv A.
inv ESD.
econstructor.
erewrite upd_perm_release_swap.
econstructor;
eauto.
perm.
destruct (
d'
a).
clarify.
rewrite peq_false;
auto.
destruct (
Rset.subset_singleton _ _ ESD0);
subst.
rewrite Rset.not_mem_remove_nop.
auto.
apply Rset.empty_not_mem.
rewrite Rset.not_mem_remove_nop.
auto.
intros K;
pose proof (
Rset.mem_singleton K).
clarify.
eassumption.
apply release_func.
reflexivity.
apply release_func.
reflexivity.
inv ESD0.
econstructor.
econstructor;
auto.
econstructor.
autorw'.
apply extensionality.
intros x.
case (
eq_dec x a).
intros ->.
perm.
f_equal.
apply Rset.add_remove_comm;
auto.
intros.
perm.
>
destruct m as (
m &
d).
eexists;
split;
vauto.
econstructor;
eauto.
econstructor.
intros p;
generalize (
ESP p).
inv A.
inv ESD.
case (
eq_dec p a).
intros ->
_.
unfold is_free.
perm.
destruct (
d a).
congruence.
destruct (
Rset.subset_singleton _ _ ESD0);
subst.
auto.
unfold Rset.singleton.
rewrite Rset.add_mem_o;
auto.
intros.
perm.
inv ESD0.
case (
eq_dec p a).
intros ->.
perm.
autorw'.
simpl.
rewrite Rset.add_mem_o;
auto.
intros.
perm.
inv A.
inv ESD;
vauto.
>
assert (
p â‰
a).
intros ->.
inv A.
inv ESD0.
perm.
clarify.
inv ESD1.
perm.
clarify.
destruct released.
apply release_func in ESP;
subst.
inv A.
inv ESD0.
eexists.
split.
econstructor;
eauto. 2:
apply release_func;
reflexivity.
perm.
econstructor;
eauto.
erewrite upd_perm_release_swap.
econstructor;
eauto.
perm.
destruct (
d0 a).
clarify.
rewrite peq_false;
auto.
destruct (
Rset.subset_singleton _ _ ESD1);
subst.
rewrite Rset.not_mem_remove_nop.
auto.
apply Rset.empty_not_mem.
rewrite Rset.not_mem_remove_nop.
auto.
intros K;
pose proof (
Rset.mem_singleton K).
clarify.
eassumption.
apply release_func.
reflexivity.
apply release_func.
reflexivity.
inv ESD1.
perm.
eexists.
split.
econstructor;
eauto.
apply release_func.
reflexivity.
econstructor;
eauto.
econstructor;
eauto.
econstructor.
autorw'.
apply extensionality.
intros x.
case (
eq_dec x a).
intros ->.
perm.
f_equal.
apply Rset.add_remove_comm;
auto.
intros.
perm.
inv A.
inv ESD0.
eexists.
split;
vauto.
econstructor;
eauto.
perm.
inv ESD1.
perm.
eexists.
split;
vauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
>
inv ESP.
inv A.
inv ESD.
eexists.
split. 2:
vauto.
econstructor;
eauto.
econstructor;
eauto.
case (
eq_dec p a).
intros ->.
perm.
clarify.
intros.
perm.
inv ESD0.
case (
eq_dec p a).
intros ->.
perm.
clarify.
eexists.
split.
econstructor;
eauto.
econstructor;
eauto.
rewrite Rset.add_mem_o in RP2;
auto.
econstructor.
econstructor;
eauto.
vauto.
intros.
perm.
eexists.
split.
vauto.
econstructor;
eauto.
vauto.
>
inv ESD.
destruct released.
apply release_func in ESP;
subst.
assert (
p â‰
a).
intros ->.
inv A.
inv ESD.
perm.
rewrite peq_false in *;
auto.
clarify.
inv ESD1.
perm.
clarify.
rewrite Rset.subset_spec in ALONE.
assert (
Rset.mem t (
Rset.remove t' (
Rset.add t s0)))
as Q.
rewrite Rset.mem_rmo;
auto.
apply Rset.add_mem.
generalize (
ALONE _ Q).
unfold Rset.singleton.
rewrite Rset.add_mem_o;
auto.
apply Rset.empty_not_mem.
inv A.
inv ESD.
perm.
eexists.
split.
econstructor;
eauto. 2:
apply release_func;
reflexivity.
vauto.
econstructor;
eauto.
erewrite upd_perm_release_swap.
econstructor;
eauto.
unfold has_store_perm.
destruct (
d0 a).
clarify.
rewrite peq_false;
auto.
destruct (
Rset.subset_singleton _ _ ESD1);
subst.
rewrite Rset.not_mem_remove_nop.
auto.
apply Rset.empty_not_mem.
rewrite Rset.not_mem_remove_nop.
auto.
intros K;
pose proof (
Rset.mem_singleton K).
clarify.
eassumption.
apply release_func.
reflexivity.
apply release_func.
reflexivity.
inv ESD1.
perm.
eexists;
split.
econstructor;
eauto. 2:
apply release_func;
reflexivity.
vauto.
econstructor;
eauto.
econstructor;
auto.
econstructor.
autorw'.
apply extensionality.
intros x.
case (
eq_dec x a).
intros ->.
perm.
f_equal.
apply Rset.add_remove_comm;
auto.
intros.
perm.
subst.
inv A.
eexists;
split.
econstructor;
eauto.
econstructor.
eassumption.
case (
eq_dec a p).
intros ->.
inv ESD.
perm.
clarify.
inv ESD1.
perm.
clarify.
destruct (
Rset.subset_singleton _ _ ALONE)
as [
H|
H].
elim (
Rset.add_not_empty H).
absurd (
Rset.mem t (
Rset.singleton t')).
unfold Rset.singleton.
rewrite Rset.add_mem_o;
auto.
apply Rset.empty_not_mem.
rewrite <-
H.
apply Rset.add_mem.
intros K.
inv ESD.
perm.
inv ESD1.
perm.
vauto.
>
inv A.
eexists.
split.
econstructor;
eauto.
intros q Q.
specialize ESD with q.
case (
eq_dec p a).
intros ->.
inv ESD0.
perm.
autorw'.
intuition.
inv ESD1.
perm.
intros.
inv ESD0.
perm.
inv ESD1.
perm.
vauto.
>
inv A.
assert (
p â‰
a).
intros ->.
destruct r.
apply release_func in ESP.
subst.
inv ESD0.
perm.
rewrite peq_false in ESD;
auto.
clarify.
inv ESD1.
perm.
absurd (
Rset.mem t (
Rset.add t s)).
rewrite <- (@
Rset.mem_rmo _ _ _ NE).
generalize (@
Rset.empty_not_mem t).
unfold empty_perm in *.
congruence.
apply Rset.add_mem.
subst.
inv ESD0.
perm.
clarify.
inv ESD1.
perm.
elim (@
Rset.add_not_empty s t).
unfold empty_perm in *.
congruence.
destruct r.
apply release_func in ESP;
subst.
eexists.
split.
econstructor;
eauto.
apply release_func.
reflexivity.
simpl.
inv ESD0.
perm.
inv ESD1.
perm.
inv ESD0.
econstructor.
erewrite upd_perm_release_swap.
econstructor;
eauto.
perm.
destruct (
d0 a).
clarify.
rewrite peq_false;
auto.
destruct (
Rset.subset_singleton _ _ ESD1);
subst.
rewrite Rset.not_mem_remove_nop.
auto.
apply Rset.empty_not_mem.
rewrite Rset.not_mem_remove_nop.
auto.
intros K;
pose proof (
Rset.mem_singleton K).
clarify.
eassumption.
apply release_func.
reflexivity.
apply release_func.
reflexivity.
inv ESD1.
perm.
econstructor.
econstructor;
eauto.
econstructor;
eauto.
autorw'.
apply extensionality.
intros x.
case (
eq_dec x a).
intros ->.
perm.
f_equal.
apply Rset.add_remove_comm;
auto.
intros.
perm.
subst.
eexists.
split;
vauto.
econstructor;
eauto.
inv ESD0.
perm.
inv ESD1.
perm.
>
inv A.
eexists;
split. 2:
vauto.
econstructor;
eauto.
destruct ESF as (
A &
B).
split;
auto.
intros q H.
generalize (
B q H).
case (
eq_dec a q).
intros ->.
inv ESD.
perm.
intros K;
clarify.
inv ESD0.
perm.
intros K.
rewrite Rset.subset_spec in K.
absurd (
Rset.mem t (
Rset.singleton t')).
unfold Rset.singleton.
rewrite Rset.add_mem_o;
auto.
apply Rset.empty_not_mem.
apply K.
apply Rset.add_mem.
intros.
inv ESD.
perm.
inv ESD0.
perm.
>
inv A.
eexists.
split. 2:
vauto.
econstructor;
eauto.
destruct ESWF as (
A &
B).
split;
auto.
intros q H.
generalize (
B q H).
case (
eq_dec a q).
intros ->.
inv ESD.
perm.
intros K;
clarify.
inv ESD0.
perm.
intros K.
rewrite Rset.subset_spec in K.
absurd (
Rset.mem t (
Rset.singleton t')).
unfold Rset.singleton.
rewrite Rset.add_mem_o;
auto.
apply Rset.empty_not_mem.
apply K.
apply Rset.add_mem.
intros.
inv ESD.
perm.
inv ESD0.
perm.
Qed.
Lemma ext_trace_requestperm :
forall t af mb tr mb',
ext_trace t af mb tr mb' ->
let (
m,
b) :=
mb in
let (
m',
b') :=
mb'
in
forall m0 ap a,
safe t b m0 ->
mem_step t m0 (
MEperm (
PErequest ap a))
m ->
exists m1,
ext_trace t af (
m0,
b)
tr (
m1,
b') /\
mem_step t m1 (
MEperm (
PErequest ap a))
m'.
Proof.
induction 1;
simpl;
intros.
>
econstructor;
split;
vauto.
>
assert (
exists m4,
trace_mem_inv t0 (
safe t b2)
m0 (
rev e)
m4
/\
mem_step t m4 (
MEperm (
PErequest ap a))
m2
/\
safe t b2 m4)
as (
m5 &
M2 &
M1 &
Q5).
clear H0 IHext_trace.
generalize dependent m0.
apply trace_mem_inv_eq1 in H.
revert H.
generalize (
rev e);
intros tr.
induction 1;
intros.
>
econstructor;
split;
vauto.
>
destruct (
perm_request_mem_step (
not_eq_sym ET1)
H2 TM2)
as (
m5 &
Hm5 &
Hm5').
assert (
safe t b2 m')
as Q by (
inv H;
auto).
assert (
safe t b2 m5)
as Q5.
auto.
destruct (
IHtrace_mem_inv Q _ Q5 Hm5')
as (
m6 &
M6 &
M7).
exists m6;
split;
vauto.
apply trace_mem_inv_eq2 in M2.
rewrite (
rev_involutive e)
in *.
destruct (
IHext_trace _ _ _ Q5 M1)
as (
m6 &
M6 &
M7).
exists m6;
split;
vauto.
>
assert (
Hb:
exists m0',
unbuffer t (
m0,
b1) (
m0',
b2)).
inv H.
assert (
safe_le t m1 m0)
as LE.
eapply mem_step_le. 3:
eassumption.
congruence.
congruence.
destruct (
buf_step_safe_le LE HU3)
as (
n' &
e' &
ST &
LE').
vauto.
assert (
exists m',
unbuffer t (
m0,
b1) (
m',
b2)
/\
mem_step t m' (
MEperm (
PErequest ap a))
m2)
as (
mm &
M1 &
M2).
clear IHext_trace H0.
inv H;
inv H2.
destruct m2 as (
m2 &
d2).
exists (
MEM m2 d);
split.
destruct Hb as (
m0' &
Hb).
inv Hb.
app_inv.
destruct bi0;
inv HU3;
inv HU0;
econstructor;
eauto;
econstructor;
eauto.
econstructor;
eauto.
inv ESD;
try congruence.
destruct bi;
inv HU3;
econstructor;
eauto.
destruct bi;
inv HU3;
econstructor;
eauto.
end_assert mm.
assert (
safe t b2 mm)
as Q.
auto.
destruct (
IHext_trace _ _ _ Q M2)
as (
mmm &
M3 &
M4).
exists mmm;
split;
auto.
vauto.
Qed.
Lemma refines_request:
forall addr args ap stmt f,
refines
(
Sseq
(
Srequestperm ap addr args)
(
Satomic f stmt))
(
Satomic f
(
Sseq (
Srequestperm ap addr args)
stmt)).
Proof.
unfold refines;
intros.
inv H.
econstructor;
eauto;
clear H1.
inv H0.
inv H4.
inv H2.
assert (
S:
safe st b'0
m'2)
by eauto.
exploit (
ext_trace_requestperm _ _ _ _ _ H9);
eauto.
intros (
m1 &
M1 &
M2).
econstructor;
eauto.
simpl;
auto.
replace (@
nil (
positive*
ext_event))
with (
nil++@
nil (
positive*
ext_event))
by auto.
econstructor;
eauto.
econstructor;
eauto.
inv H3;
eelim H7;
eauto.
Qed.
Lemma refines_promotes_fence:
forall f r,
refines (
Sfence r) (
Satomic f (
if r then Srelease else Sskip)).
Proof.
unfold refines; intros.
inv H.
inv H0.
econstructor; eauto; clear H1.
econstructor; eauto.
destruct r; simpl; auto.
destruct r; subst; econstructor; eauto.
Qed.
Lemma ext_trace_keep_hidden_inv :
forall t af mb1 tr mb2,
ext_trace t af mb1 tr mb2 ->
forall p,
(
fst mb2).(
perms)
p =
HiddenBy t ->
(
fst mb1).(
perms)
p =
HiddenBy t.
Proof.
induction 1;
auto.
>
simpl in *;
intros.
exploit IHext_trace;
eauto.
clear IHext_trace H0 H1.
revert H;
induction 1;
auto.
intros;
apply IHmem_trace.
clear IHmem_trace H.
destruct m'
as (
m',
d');
destruct m''
as (
m'',
d'');
simpl in *.
assert (
Permissions.release t0 d'
d'' ->
d'
p =
HiddenBy t).
intro.
generalize (
H p);
intros T;
inv T;
unfold empty_perm in *;
try congruence.
inv TM2;
auto.
>
inv ESD;
auto.
>
unfold upd_perm in *;
destruct Ptr.eq_dec;
intuition congruence.
>
inv ESD0.
unfold upd_perm in *;
destruct Ptr.eq_dec;
intuition congruence.
>
destruct released;
auto;
congruence.
>
destruct released;
auto;
congruence.
>
destruct r;
auto;
congruence.
>
simpl in *;
intros.
inv H;
simpl in *.
inv HU3;
simpl in *;
auto.
Qed.
Lemma release_release:
forall t t'
d1 d2 d3,
t<>
t' ->
release t d1 d2 ->
release t'
d2 d3 ->
exists d2',
release t'
d1 d2' /\
release t d2'
d3.
Proof.
intros.
exists (
fun p =>
match d1 p with
|
FrozenBy s =>
FrozenBy (
Rset.remove t'
s)
|
HiddenBy t =>
if peq t'
t then empty_perm
else HiddenBy t
end).
split.
rewrite release_func;
auto.
rewrite release_func.
apply extensionality;
intros p.
rewrite release_func in H1;
subst.
rewrite release_func in H0;
subst.
case_eq (
d1 p);
intros.
destruct peq;
unfold empty_perm.
rewrite peq_false;
try congruence.
subst;
rewrite peq_true;
try congruence.
f_equal.
unfold Rset.remove,
Rset.empty;
simpl.
apply PTree.ext;
intros p0.
rewrite PTree.gempty.
rewrite PTree.grspec;
destruct peq;
auto.
rewrite PTree.gempty;
auto.
destruct peq;
try congruence.
f_equal.
unfold Rset.remove,
Rset.empty;
simpl.
apply PTree.ext;
intros p0.
rewrite PTree.gempty.
rewrite PTree.grspec;
destruct peq;
auto.
rewrite PTree.gempty;
auto.
rewrite peq_false;
auto.
rewrite Rset.remove_comm;
auto.
Qed.
Lemma release_mem_trace:
forall t b t'
m1 e m2,
trace_mem_inv t' (
safe t b)
m1 e m2 ->
forall m0,
t' <>
t ->
safe t b m0 ->
mem_step t m2 (
MEperm PErelease)
m0 ->
exists m',
trace_mem_inv t' (
safe t b)
m'
e m0 /\
mem_step t m1 (
MEperm PErelease)
m'.
Proof.
induction 1.
>
econstructor;
split;
eauto.
econstructor;
auto.
>
intros.
exploit IHtrace_mem_inv;
eauto;
clear IHtrace_mem_inv H2.
intros (
mm &
M1 &
M2).
assert (
exists m2,
mem_step t'
m2 e mm /\ (
mem_step t m (
MEperm PErelease)
m2)).
clear M1 H.
destruct mm as (
mm1,
d1).
destruct m'
as (
mm2,
d2).
destruct m as (
mm3,
d3).
inv M2.
inv ESD.
inv TM2.
>
inv ESD.
>
eexists.
split. 2:
vauto.
econstructor.
econstructor.
apply release_func in ESP.
subst.
inv ESD0;
econstructor;
autorw'.
destruct peq;
congruence.
destruct (
Rset.subset_singleton _ _ ALONE);
subst.
eapply Rset.subset_trans.
eapply Rset.remove_subset.
auto.
eapply Rset.remove_subset.
>
apply release_func in ESP.
subst.
inv ESD0.
inv RP.
eexists.
split.
econstructor.
econstructor.
econstructor.
econstructor.
autorw'.
rewrite Rset.mem_rmo;
auto.
econstructor.
econstructor.
apply release_func.
reflexivity.
eexists.
split.
econstructor.
econstructor.
econstructor.
destruct (
d2 p).
subst.
rewrite peq_false;
auto.
auto.
econstructor.
econstructor.
apply release_func.
reflexivity.
>
assert (
d1 p =
HiddenBy t').
rewrite release_func in ESP;
subst.
rewrite perm_gss;
auto.
rewrite peq_false;
auto.
set (
d3' :=
fun p =>
match d3 p with
|
FrozenBy s =>
FrozenBy (
Rset.remove t s)
|
HiddenBy t' =>
if peq t t'
then empty_perm
else HiddenBy t'
end).
exists (
MEM mm1 d3');
split;
constructor.
2:
econstructor;
rewrite release_func;
auto.
replace d1 with (
upd_perm d3'
p (
HiddenBy t')).
constructor;
auto.
unfold has_store_perm,
d3'
in *.
case_eq (
d3 p);
intros;
rewrite H2 in *.
rewrite peq_false;
try congruence.
apply Rset.subset_trans with (2:=
ESD0);
eauto.
apply Rset.remove_subset.
apply extensionality;
intros p0.
unfold upd_perm,
d3'.
destruct Ptr.eq_dec;
try congruence.
rewrite release_func in ESP;
subst.
rewrite perm_gso;
auto.
>
set (
d3' :=
fun p =>
match d3 p with
|
FrozenBy s =>
FrozenBy (
Rset.remove t s)
|
HiddenBy t' =>
if peq t t'
then empty_perm
else HiddenBy t'
end).
exists (
MEM mm1 d3');
split;
constructor.
2:
econstructor;
rewrite release_func;
auto.
constructor;
auto.
inv ESD0.
constructor 1
with (
Rset.remove t s);
auto.
unfold d3';
rewrite URP1;
auto.
apply extensionality;
intros p0.
unfold upd_perm,
d3'.
destruct Ptr.eq_dec;
subst.
rewrite release_func in ESP;
subst.
rewrite perm_gss;
auto.
unfold Rset.remove,
Rset.add.
f_equal.
apply PTree.ext;
intros p0.
rewrite PTree.gsspec.
repeat rewrite PTree.grspec.
rewrite PTree.gsspec.
destruct peq;
auto.
rewrite peq_false;
try congruence.
rewrite release_func in ESP;
subst.
rewrite perm_gso;
auto.
>
exploit release_release;
eauto;
intros (
d2' &
D1 &
D2).
exists (
MEM mm1 d2');
split;
econstructor;
constructor;
auto.
>
exists (
MEM mm1 d1);
split;
econstructor;
constructor;
auto.
intros p.
generalize (
ESP0 p);
unfold is_free;
intros.
rewrite release_func in ESP;
subst.
case_eq (
d2 p);
intros;
rewrite H2 in H;
try congruence.
destruct peq;
try congruence.
unfold empty_perm;
try congruence.
rewrite mem_empty;
congruence.
rewrite Rset.mem_rmo;
auto.
>
destruct released;
subst.
>
exploit release_release;
eauto;
intros (
d2' &
D1 &
D2).
exists (
MEM mm3 d2');
split;
econstructor;
eauto.
rewrite release_func in D1;
subst.
rewrite ESD.
rewrite peq_false;
auto.
constructor;
auto.
>
exists (
MEM mm3 d1);
split;
econstructor;
eauto.
rewrite release_func in ESP;
subst.
rewrite ESD.
rewrite peq_false;
auto.
constructor;
auto.
>
exists (
MEM mm1 d1);
split;
econstructor;
eauto.
rewrite release_func in ESP;
subst.
inv ESP0;
econstructor.
rewrite RP1;
eauto.
rewrite Rset.mem_rmo;
auto.
constructor;
auto.
>
destruct released;
subst.
>
exploit release_release;
eauto;
intros (
d2' &
D1 &
D2).
exists (
MEM mm3 d2');
split;
econstructor;
eauto.
inv ESD.
constructor 2
with (
Rset.remove t s).
apply Rset.subset_trans with (2:=
ALONE);
eauto.
apply Rset.remove_subset.
generalize (
ESP p);
intros T;
inv T;
try congruence.
constructor;
auto.
>
exists (
MEM mm3 d1);
split;
econstructor;
eauto.
inv ESD.
constructor 2
with (
Rset.remove t s).
apply Rset.subset_trans with (2:=
ALONE);
eauto.
apply Rset.remove_subset.
generalize (
ESP p);
intros T;
inv T;
try congruence.
constructor;
auto.
>
exists (
MEM mm1 d1);
split;
econstructor;
eauto.
intros.
generalize (
ESP p);
intros T;
inv T;
try congruence.
exploit ESD;
eauto;
intros;
subst.
congruence.
unfold empty_perm in *;
congruence.
constructor;
auto.
>
destruct r;
subst.
>
exploit release_release;
eauto;
intros (
d2' &
D1 &
D2).
exists (
MEM mm3 d2');
split;
econstructor;
eauto.
rewrite release_func in ESP;
subst.
rewrite ESD.
unfold empty_perm.
f_equal;
auto.
rewrite Rset.not_mem_remove_nop;
auto.
rewrite mem_empty;
congruence.
constructor;
auto.
>
exists (
MEM mm3 d1);
split;
econstructor;
eauto.
rewrite release_func in ESP;
subst.
rewrite ESD.
unfold empty_perm.
f_equal;
auto.
rewrite Rset.not_mem_remove_nop;
auto.
rewrite mem_empty;
congruence.
constructor;
auto.
>
exists (
MEM mm3 d1);
split;
econstructor;
eauto.
inv ESF;
split;
auto;
intros.
exploit H2;
eauto;
intros;
clear H3 H2.
unfold has_store_perm in *.
generalize (
ESP p0);
intros T;
inv T;
try congruence.
rewrite <-
H2 in *;
intuition.
unfold empty_perm;
eauto.
rewrite <-
H3 in *.
apply Rset.subset_trans with (2:=
H4);
eauto.
apply Rset.remove_subset.
constructor;
auto.
>
exists (
MEM mm3 d1);
split;
econstructor;
eauto.
inv ESWF;
split;
auto;
intros.
exploit H2;
eauto;
intros;
clear H3 H2.
unfold has_store_perm in *.
generalize (
ESP p0);
intros T;
inv T;
try congruence.
rewrite <-
H2 in *;
intuition.
unfold empty_perm;
eauto.
rewrite <-
H3 in *.
apply Rset.subset_trans with (2:=
H4);
eauto.
apply Rset.remove_subset.
constructor;
auto.
destruct H2 as (
m2 &
M3 &
M4).
exists m2;
split;
eauto.
econstructor;
eauto.
Qed.
Lemma release_ext_trace :
forall t af mb1 tr mb2,
ext_trace_inv t af mb1 tr mb2 ->
let (
m1,
b1) :=
mb1 in
let (
m2,
b2) :=
mb2 in
forall m0,
safe t b2 m0 ->
mem_step t m2 (
MEperm PErelease)
m0 ->
exists m',
ext_trace_inv t af (
m',
b1)
tr (
m0,
b2) /\
mem_step t m1 (
MEperm PErelease)
m'.
Proof.
induction 1;
intros.
>
econstructor;
split;
eauto.
econstructor;
auto.
>
apply trace_mem_inv_eq1 in H.
exploit (
release_mem_trace _ _ _ _ _ _ H m0);
eauto.
intros (
m' &
M1 &
M2).
exploit (
IHext_trace_inv m');
eauto.
intros (
m'' &
M3 &
M4).
apply trace_mem_inv_eq2 in M1.
exists m'';
split;
eauto.
rewrite rev_involutive in M1.
econstructor;
eauto.
>
inv H.
assert (
exists m',
exists e',
buf_step t m'
bi e'
m0 /\
mem_step t m2 (
MEperm PErelease)
m').
clear IHext_trace_inv H0.
inv HU3;
inv H2.
>
exists (
MEM m d').
exists (
MEwrite false Global p v).
split. 2:
vauto.
econstructor;
auto.
inv ESD0.
apply release_func in ESP.
subst.
inv ESD;
simpl in *.
econstructor.
apply Rset.empty_subset.
autorw'.
destruct peq.
reflexivity.
congruence.
econstructor. 2:
autorw'.
eapply Rset.subset_trans.
apply Rset.remove_subset.
easy.
>
exists (
MEM m d');
econstructor;
split;
try econstructor;
eauto.
inv ESF;
split;
auto;
intros.
exploit H0;
eauto;
intros;
clear H0 H2.
inv ESD.
unfold has_store_perm in *.
generalize (
ESP p0);
intros T;
inv T;
try congruence.
rewrite <-
H0 in *;
intuition.
unfold empty_perm;
eauto.
rewrite <-
H2 in *.
apply Rset.subset_trans with (2:=
H3);
eauto.
apply Rset.remove_subset.
>
exists (
MEM m d');
econstructor;
split;
try econstructor;
eauto.
inv ESWF;
split;
auto;
intros.
exploit H0;
eauto;
intros;
clear H0 H2.
inv ESD.
unfold has_store_perm in *.
generalize (
ESP p0);
intros T;
inv T;
try congruence.
rewrite <-
H0 in *;
intuition.
unfold empty_perm;
eauto.
rewrite <-
H2 in *.
apply Rset.subset_trans with (2:=
H3);
eauto.
apply Rset.remove_subset.
destruct H as (
m' &
e' &
M1 &
M2).
exploit (
IHext_trace_inv m');
auto.
>
intros (
m'' &
M3 &
M4).
exists m'';
split;
auto.
econstructor;
eauto.
econstructor;
eauto.
Qed.
Lemma refines_store_fence:
forall f r af addr args dst,
refines
(
Sseq (
Sstore false af addr args dst) (
Sfence r))
(
Satomic f (
Sstore r af addr args dst)).
Proof.
unfold refines;
intros.
inv H.
inv H0.
inv H3;
inv H5.
edestruct (
ext_trace_push_item _ _ _ _ _ H7)
as [(
T1 &
m1' &
m2' &
e' &
T2 &
tr1 &
tr2 &
T3 &
T4 &
T5)|(
b2' &
T1 &
T2)];
eauto;
clear H7.
>
subst.
repeat rewrite app_ass.
rewrite <- (
app_ass l1).
unfold empty_buffer in *.
destruct r.
>
apply ext_trace_inv_eq2 in T5.
exploit release_ext_trace;
eauto;
simpl;
intros T.
exploit T;
eauto;
clear T.
intros (
m5 &
M1 &
M2);
clear H11 T5.
apply ext_trace_inv_eq1 in M1;
rewrite rev_involutive in M1.
econstructor;
eauto;
clear M1 H1.
econstructor;
eauto.
>
simpl;
auto.
>
econstructor;
eauto.
inv T2;
inv M2.
inv ESD0.
inv H21;
econstructor;
eauto.
>
exploit (
ext_trace_hidden_perm_inv _ _ _ _ _ T4 a);
eauto;
simpl.
>
inv ESD.
>
subst;
exploit (
ext_trace_keep_hidden_inv _ _ _ _ _ T4 a);
eauto;
simpl;
auto.
congruence.
>
simpl in *.
generalize (
ESP a);
intros T;
inv T;
try congruence.
replace s1 with s0 in *
by congruence.
constructor 2
with (
Rset.remove st s0);
auto.
apply Rset.subset_trans with (2:=
ALONE0).
apply Rset.remove_subset.
>
subst;
econstructor;
eauto.
clear T5 H1.
inv T2.
econstructor;
eauto.
>
simpl;
auto.
>
econstructor;
eauto.
inv H21;
econstructor;
eauto.
>
exploit (
ext_trace_hidden_perm_inv _ _ _ _ _ T4 a);
eauto;
simpl.
>
inv ESD.
>
subst;
exploit (
ext_trace_keep_hidden_inv _ _ _ _ _ T4 a);
eauto;
simpl;
auto.
congruence.
>
clear ALONE;
econstructor;
eauto.
>
inv T1.
>
inv H4;
eelim H8;
eauto.
Qed.
Lemma refines_remove_freeperm_right:
forall stmt,
refines (
Sseq stmt Sfreeperm)
stmt.
Proof.
unfold refines;
intros.
inversion_clear H;
inversion_clear H0;
clarify.
inversion_clear H2;
clarify.
exploit ext_trace_app;
eauto;
intro.
rewrite app_ass.
econstructor;
eauto.
vauto.
Qed.
Lemma ext_trace_keep_step_freeperm :
forall tid m l m'
af,
ext_trace tid af m l m' ->
mem_step tid (
fst m) (
MEperm PErelease) (
fst m) ->
mem_step tid (
fst m') (
MEperm PErelease) (
fst m').
Proof.
Hint Resolve ext_trace_keep_step_freeperm.
Lemma ext_trace_keep_step_freeperm2 :
forall tid m l m'
af,
ext_trace tid af m'
l m ->
mem_step tid (
fst m) (
MEperm PErelease) (
fst m) ->
mem_step tid (
fst m') (
MEperm PErelease) (
fst m').
Proof.
Hint Resolve ext_trace_keep_step_freeperm2.
Lemma no_atomic_in_statement_remove_perm :
forall body,
INJECT.no_atomic_in_statement body ->
INJECT.no_atomic_in_statement (
remove_perm body).
Proof.
induction body; simpl; intuition.
Qed.
Hint Resolve no_atomic_in_statement_remove_perm.
Lemma release_useless:
forall tid d d',
release tid d d' ->
(
forall p :
pointer,
is_free tid (
d p)) ->
d =
d'.
Proof.
intros.
apply extensionality;
intros p.
generalize (
H p);
intros.
inv H1;
auto.
generalize (
H0 p);
rewrite <-
H3;
simpl;
intuition.
generalize (
H0 p);
rewrite <-
H3;
simpl;
intros.
rewrite Rset.not_mem_remove_nop;
auto;
congruence.
Qed.
Lemma rset_mem_remove:
forall tid s,
~
Rset.mem tid (
Rset.remove tid s).
Proof.
unfold Rset.mem, Rset.remove; intros.
rewrite PTree.grspec; destruct peq; congruence.
Qed.
Hint Resolve rset_mem_remove.
Lemma release_functional:
forall tid d d1 d2,
release tid d d1 ->
release tid d d2 ->
d1=
d2.
Proof.
intros.
apply extensionality.
intros p; generalize (H p); generalize (H0 p); intros.
inv H1; inv H2; try congruence.
Qed.
Lemma free_release:
forall tid d,
(
forall p :
pointer,
is_free tid (
d p)) ->
release tid d d.
Proof.
intros.
intros p.
generalize (
H p);
intros E;
clear H.
destruct (
d p) ;
simpl in E.
econstructor;
auto.
pattern s at 2.
replace s with (
Rset.remove tid s).
econstructor;
eauto.
apply Rset.not_mem_remove_nop.
rewrite E;
congruence.
Qed.
Hint Resolve free_release.
Lemma release_is_free:
forall tid d d',
release tid d d' ->
forall p,
is_free tid (
d'
p).
Proof.
intros.
generalize (H p); intros ;clear H.
inv H0; simpl; auto.
Qed.
Hint Resolve release_is_free.
Lemma freeperm_implies_release:
forall tid m,
mem_step tid m (
MEperm PEfreeperm)
m ->
mem_step tid m (
MEperm PErelease)
m.
Proof.
intros.
inv H; inv ESD; constructor; auto.
econstructor; eauto.
Qed.
Hint Resolve freeperm_implies_release.
Lemma release_frozen:
forall tid s1 s2,
s2 =
Rset.remove tid s1 ->
release_perm tid (
FrozenBy s1) (
FrozenBy s2).
Proof.
intros; subst; constructor.
Qed.
Lemma release_diamond:
forall d'
d''
t tid d,
release tid d d' ->
release t d d'' ->
exists d0,
release t d'
d0 /\
release tid d''
d0.
Proof.
Lemma mem_step_release:
forall tid t m M m'
e,
mem_step tid m (
MEperm PErelease)
M ->
mem_step t m e m' ->
t<>
tid ->
exists M',
mem_step tid m' (
MEperm PErelease)
M' /\
mem_step t M e M'.
Proof.
Lemma trace_mem_release:
forall t m b m'
l t',
trace_mem_inv t (
safe t'
b)
m l m' ->
forall M tid,
tid <>
t ->
mem_step tid m (
MEperm PErelease)
M ->
exists M',
mem_step tid m' (
MEperm PErelease)
M' /\
trace_mem_inv t (
safe t'
b)
M l M'.
Proof.
induction 1;
intros.
exists M;
split; [
auto |
econstructor;
eauto].
exploit (
mem_step_release tid t);
eauto.
intros (
M' &
M1 &
M2).
exploit IHtrace_mem_inv;
eauto.
intros (
M'' &
M1' &
M2').
econstructor;
split;
eauto.
econstructor;
eauto.
Qed.
Lemma ext_trace_inv_release:
forall tid m l m'
af,
ext_trace_inv tid af m l m' ->
forall b0 b1,
b0 =
snd m ->
b1 =
snd m' ->
forall M,
mem_step tid (
fst m) (
MEperm PErelease)
M ->
exists M',
mem_step tid (
fst m') (
MEperm PErelease)
M' /\
ext_trace_inv tid af (
M,
b0)
l (
M',
b1).
Proof.
induction 1;
intros.
simpl in *;
clarify.
exists M;
split; [
eauto|
econstructor;
eauto].
simpl in *;
clarify.
apply trace_mem_inv_eq1 in H.
exploit IHext_trace_inv;
eauto.
intros (
M' &
M1 &
M2).
exploit trace_mem_release;
eauto.
intros (
M'' &
M1' &
M2').
econstructor;
split;
eauto.
econstructor;
eauto.
apply trace_mem_inv_eq2 in M2'.
rewrite rev_involutive in M2';
auto.
simpl in *;
clarify.
exploit IHext_trace_inv;
eauto;
clear IHext_trace_inv.
intros (
M' &
M1 &
M2).
assert (
unbuffer_n'
tid (
m2,
b2) 1 (
m3,
b3))
by (
repeat (
econstructor;
eauto)).
destruct m2;
destruct m3;
clarify.
pose (
unbuf_perm _ _ _ _ _ H).
inversion e;
clarify;
clear e.
inversion H1;
clarify;
clear H1.
inversion H6;
clarify;
clear H6.
inversion M1;
clarify.
exists (
MEM mem_rtl0 d');
split; [
econstructor;
eauto|
econstructor;
eauto].
inversion H4;
clarify;
clear H4.
inversion ESD;
clarify.
inversion HU3;
clarify;
clear HU3.
specialize (
ESP p).
assert (
check_perm_store tid {|
mem_rtl :=
mem_rtl;
perms :=
d' |}
Global p).
inversion ESD0;
clarify.
simpl in *.
rewrite ESD1 in ESP;
inversion ESP;
clarify.
assert (
Rset.subset Rset.empty (
Rset.singleton tid))
by auto.
econstructor;
eauto.
simpl in *.
rewrite ESD1 in ESP;
inversion ESP;
clarify.
destruct (
Rset.subset_singleton _ _ ALONE);
clarify.
erewrite Rset.not_mem_remove_nop in H4; [|
apply Rset.empty_not_mem].
econstructor;
eauto.
unfold Rset.singleton in H4;
rewrite Rset.remove_add_remove in H4.
erewrite Rset.not_mem_remove_nop in H4; [|
apply Rset.empty_not_mem].
assert (
Rset.subset Rset.empty (
Rset.singleton tid))
by auto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
inversion ESF;
clarify.
econstructor;
eauto.
intros p0 range.
exploit H2;
eauto;
clear H2;
intro.
specialize (
ESP p0).
unfold has_store_perm in *;
destruct (
perms0 p0);
clarify.
inversion ESP;
clarify.
inversion ESP;
clarify.
destruct (
Rset.subset_singleton _ _ H2);
clarify.
assert (~
Rset.mem tid Rset.empty)
by apply Rset.empty_not_mem.
erewrite (
Rset.not_mem_remove_nop);
eauto.
unfold Rset.singleton;
erewrite Rset.remove_add;
eauto.
eapply Rset.empty_not_mem.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
inversion ESWF;
clarify.
intros p0 range.
specialize (
ESP p0).
inversion ESWF;
clarify.
exploit H2;
eauto;
intro.
unfold has_store_perm in *;
destruct (
perms0 p0);
clarify.
inversion ESP;
clarify.
inversion ESP;
clarify.
destruct (
Rset.subset_singleton _ _ H4);
clarify.
erewrite (
Rset.not_mem_remove_nop);
eauto.
eapply Rset.empty_not_mem.
unfold Rset.singleton;
erewrite Rset.remove_add;
eauto.
eapply Rset.empty_not_mem.
Qed.
Lemma ext_trace_release:
forall tid m M m'
l af b0 b1,
mem_step tid m (
MEperm PErelease)
M ->
ext_trace tid af (
m,
b0)
l (
m',
b1) ->
exists M1,
mem_step tid m' (
MEperm PErelease)
M1 /\
ext_trace tid af (
M,
b0)
l (
M1,
b1).
Proof.
Lemma empty_flush :
forall t m,
flush t empty_buffer m m.
Proof.
Lemma atomic_empty' :
forall stmt ge sp tid st st'
l af,
bigstep ge sp tid st stmt af l st' ->
af =
Atomic →
snd (
fst st) =
empty_buffer →
snd (
fst st') =
empty_buffer.
Proof.
induction 1; simpl; trivial; repeat intros ->;
(try now inv H); simpl in *.
apply IHbigstep2; trivial. apply IHbigstep1; trivial.
intros. apply IHbigstep2; trivial. apply IHbigstep1; trivial.
intros. apply IHbigstep2; trivial. apply IHbigstep1; trivial.
Qed.
Corollary atomic_empty :
forall stmt ge sp tid m m'
b rs rs'
l,
bigstep ge sp tid (
m,
empty_buffer,
rs)
stmt Atomic l (
m',
b,
rs') ->
b =
empty_buffer.
Proof.
intros. exploit atomic_empty'; eauto. Qed.
Lemma bigstep_remove_perm :
forall ge sp tid st stmt tr st'
af,
bigstep ge sp tid st stmt af tr st' ->
let (
m,
rs) :=
st in
let (
m0,
b) :=
m in
safe tid b m0 ->
let (
m',
rs') :=
st'
in
let (
m1,
b1) :=
m'
in
forall M,
mem_step tid (
fst m) (
MEperm PErelease) (
fst M) ->
(
snd M) =
b ->
exists M',
RefinesDefs.bigstep ge sp tid (
M,
rs) (
remove_perm stmt)
af tr (
M',
rs') /\
mem_step tid (
fst m') (
MEperm PErelease) (
fst M') /\ (
snd M' =
b1).
Proof.
induction 1;
simpl;
try (
intros SAFE M HM;
exists M;
destruct M;
split;
[
eapply bigstep_simpl; [
eauto;
econstructor;
eauto |
simpl in *;
subst;
eauto |
simpl in *;
subst;
eauto] |
auto];
fail).
>
intro SAFE;
intros.
destruct r;
clarify.
>
destruct (
ext_trace_release _ _ _ _ _ _ _ _ H1 H)
as [
M'' [
REL EXT]].
exists (
M'',
nil);
split;
intuition;
eauto.
replace l with (
l++
nil)
by auto with datatypes.
destruct M;
econstructor;
eauto.
econstructor;
eauto.
simpl in *;
clarify.
inversion H0;
inversion REL;
clarify.
inversion ESD;
inversion ESD0;
clarify.
assert (
d' =
d'0)
by (
eapply release_deterministe;
eauto);
clarify.
pose (
release_no_perm _ _ _ REL).
eapply no_perm_release;
eauto.
>
destruct (
ext_trace_release _ _ _ _ _ _ _ _ H1 H)
as [
M'' [
REL EXT]].
exists (
M'',
nil);
split;
eauto.
replace l with (
l++
nil)
by auto with datatypes.
destruct M;
econstructor;
eauto.
econstructor;
eauto.
>
intro SAFE;
destruct M;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
assert (
safe tid empty_buffer m')
by auto.
exploit (
IHbigstep H4 (
M',
empty_buffer));
eauto;
clear IHbigstep.
simpl in *.
intros (
M'' &
HM1' &
HM2').
exists M'';
split; [
idtac|
eassumption].
simpl in *;
clarify.
inversion HM1';
clarify.
exploit app_eq_nil;
eauto;
destruct 1;
subst.
assert (
b' =
empty_buffer)
by (
eapply atomic_empty;
eauto);
clarify.
inversion H13;
clarify.
replace l with (
l++
nil)
by auto with datatypes.
econstructor;
eauto.
econstructor;
eauto.
>
intro SAFE;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
exists (
M',
b');
split; [
idtac|
split;[
eassumption|
intuition]].
replace l with (
nil++
l)
by auto with datatypes.
destruct M;
destruct M';
econstructor;
eauto.
econstructor;
eauto.
simpl in *;
clarify.
econstructor;
eauto.
pose (
release_no_perm _ _ _ H1).
eapply no_perm_freeperm;
eauto.
>
intro SAFE;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
exists (
M',
b');
split;[|
intuition].
replace l with (
nil++
l)
by auto with datatypes.
simpl in *;
clarify.
replace (
fst M,
snd M)
with M in HM2 by (
destruct M;
auto).
replace l with (
nil++
l)
by auto with datatypes.
destruct M;
econstructor;
eauto.
econstructor.
simpl.
assert (
m'' =
M').
destruct m'';
destruct M'.
inversion H0;
clarify.
inversion ESD;
clarify.
inversion HM1;
clarify.
inversion ESD0;
clarify.
assert (
perms =
perms0)
by (
eapply release_deterministe;
eauto);
clarify.
subst.
pose (
release_no_perm _ _ _ H0).
eapply no_perm_release;
eauto.
>
intro SAFE;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
exists (
M',
b');
split; [|
intuition].
replace l with (
nil++
l)
by auto with datatypes.
simpl in *;
clarify.
replace (
fst M,
snd M)
with M in HM2 by (
destruct M;
auto).
replace l with (
nil++
l)
by auto with datatypes.
destruct M;
econstructor;
eauto.
econstructor.
simpl.
destruct M;
destruct m';
destruct m'';
destruct M';
simpl in *;
clarify.
inversion H1;
inversion HM1;
clarify.
subst.
econstructor;
eauto.
econstructor;
eauto.
intro.
destruct (
Ptr.eq_dec p a);
clarify.
inversion ESD;
inversion H1;
clarify.
inversion ESD0;
clarify.
specialize (
ESP a);
inversion ESP;
clarify.
unfold has_store_perm in ESD1;
rewrite <-
H3 in ESD1;
inversion ESD1;
congruence.
rewrite perm_gss.
econstructor;
eauto.
unfold has_store_perm in ESD1;
rewrite <-
H4 in ESD1;
inversion ESD1.
destruct (
Rset.subset_singleton _ _ H6);
clarify.
rewrite perm_gss.
assert (
Rset.remove tid Rset.empty =
Rset.empty).
assert (~
Rset.mem tid Rset.empty)
by apply Rset.empty_not_mem.
erewrite Rset.not_mem_remove_nop;
eauto.
rewrite H3.
econstructor;
eauto.
rewrite perm_gss.
assert (
Rset.remove tid (
Rset.singleton tid) =
Rset.empty).
unfold Rset.singleton;
rewrite Rset.remove_add;
eauto.
apply Rset.empty_not_mem.
rewrite H3.
econstructor;
eauto.
inversion ESD1;
clarify.
rewrite perm_gss.
inversion HM1;
inversion ESD3;
clarify.
specialize (
ESP a);
inversion ESP;
clarify.
congruence.
congruence.
assert (
s =
s0)
by congruence;
subst.
assert (
Rset.remove tid s0 =
Rset.remove tid (
Rset.add tid s0)).
rewrite <-
H4 in ESP;
rewrite <-
H5 in ESP.
apply sym_eq;
apply Rset.remove_add_remove.
rewrite H3.
econstructor;
eauto.
inversion ESD;
clarify.
erewrite perm_gso;
eauto.
inversion ESD0;
clarify.
inversion ESD1;
clarify.
erewrite perm_gso;
eauto.
inversion ESD0;
clarify.
>
intro SAFE;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
exists (
M',
b');
split; [|
intuition].
replace l with (
l++
nil)
by auto with datatypes.
destruct M;
destruct M'.
econstructor;
eauto.
econstructor;
eauto.
simpl in *;
subst;
eapply HM2.
inv HM1.
inv ESD.
apply release_func in ESP.
subst.
bif2.
simpl in *.
intuition.
inv H5.
simpl in *.
destruct ap.
inv H8.
autorw'.
destruct (
d a).
destruct peq;
clarify.
eauto.
clarify.
inv H0;
econstructor;
eauto;
intros t'
T.
inv ESP.
autorw'.
destruct (
d a).
destruct peq;
clarify.
eauto.
clarify.
>
intro SAFE;
intros.
destruct r.
exists (
m'',
b'');
clarify.
destruct (
ext_trace_release _ _ _ _ _ _ _ _ H6 H)
as [
M' [
REL EXT]].
split; [(
simpl in *;
clarify)|
intuition].
replace l with (
l++
nil)
by auto with datatypes.
assert (
m'' =
M').
inversion H0;
inversion REL;
clarify.
inversion ESD;
inversion ESD0;
clarify.
assert (
d' =
d'0)
by (
eapply release_deterministe;
eauto);
clarify.
clarify.
destruct M;
destruct M';
econstructor;
eauto.
simpl in *.
econstructor;
eauto.
inversion H0;
inversion ESD;
clarify.
inversion H4;
clarify.
simpl in *.
specialize (
ESP a);
rewrite ESD0 in ESP.
inversion ESP;
clarify.
econstructor;
eauto.
eapply Rset.empty_subset.
inversion H0;
inversion ESD;
clarify.
inversion H4;
clarify.
simpl in *.
specialize (
ESP0 a);
rewrite ESD2 in ESP0.
destruct (
Rset.subset_singleton _ _ ALONE0);
clarify.
inversion ESP0;
clarify.
assert (
not (
Rset.mem tid Rset.empty))
by (
eapply Rset.empty_not_mem).
replace (
Rset.remove tid Rset.empty)
with Rset.empty in H6 by
(
apply sym_eq;
eapply Rset.not_mem_remove_nop;
eauto).
econstructor;
eauto.
inversion ESP0;
clarify.
assert (
FrozenBy Rset.empty =
perms a).
destruct (
Rset.subset_singleton _ _ ALONE);
clarify.
specialize (
ESP a);
rewrite ESD0 in ESP;
inversion ESP;
clarify.
assert (~
Rset.mem tid Rset.empty)
by apply Rset.empty_not_mem.
erewrite Rset.not_mem_remove_nop;
eauto.
specialize (
ESP a);
rewrite ESD0 in ESP;
inversion ESP;
clarify.
unfold Rset.singleton;
erewrite Rset.remove_add;
eauto.
rewrite Rset.not_mem_remove_nop;
eauto.
inversion ESD1;
clarify.
specialize (
ESP1 a);
rewrite ESD2 in ESP1;
inversion ESP1;
clarify.
unfold Rset.singleton in H7;
rewrite Rset.remove_add_remove in H7.
assert (~
Rset.mem tid Rset.empty)
by apply Rset.empty_not_mem.
rewrite Rset.not_mem_remove_nop in H7;
eauto.
assert (
Rset.subset Rset.empty (
Rset.singleton tid))
by auto.
econstructor;
eauto.
assert (
has_no_perm tid m'')
by (
eapply release_no_perm;
eauto).
eapply no_perm_release;
eauto.
destruct (
ext_trace_release _ _ _ _ _ _ _ _ H6 H)
as [
M' [
REL EXT]].
exists (
M',
b'');
clarify.
split;
simpl in *;
clarify.
replace l with (
l++
nil)
by auto with datatypes.
destruct M;
destruct M';
econstructor;
eauto.
simpl in *.
econstructor;
eauto.
inversion REL;
inversion ESD;
clarify.
inversion H4;
clarify.
simpl in *.
specialize (
ESP a);
rewrite ESD0 in ESP.
inversion ESP;
clarify.
econstructor;
eauto.
eapply Rset.empty_subset.
destruct (
Rset.subset_singleton _ _ ALONE);
clarify.
simpl in *.
specialize (
ESP a);
rewrite ESD0 in ESP.
inversion ESP;
clarify.
assert (
not (
Rset.mem tid Rset.empty))
by (
eapply Rset.empty_not_mem).
replace (
Rset.remove tid Rset.empty)
with Rset.empty in H3 by
(
apply sym_eq;
eapply Rset.not_mem_remove_nop;
eauto).
econstructor;
eauto.
assert (
FrozenBy Rset.empty =
perms a).
simpl in *.
specialize (
ESP a);
rewrite ESD0 in ESP;
inversion ESP;
clarify.
unfold Rset.singleton;
erewrite Rset.remove_add;
eauto.
apply Rset.empty_not_mem.
assert (
Rset.subset Rset.empty (
Rset.singleton tid))
by
(
eapply Rset.empty_subset);
clear ALONE.
econstructor;
eauto.
>
intro SAFE;
intros.
subst.
inv H1.
destruct M;
destruct m;
simpl in *;
clarify.
exists ((
MEM m'0
perms),
empty_buffer);
split;[|
intuition].
replace (@
nil (
positive*
ext_event))
with (
nil++@
nil (
positive*
ext_event))
by auto.
econstructor;
eauto.
econstructor;
eauto.
inversion H3;
clarify.
econstructor;
eauto.
inversion ESD0;
clarify.
destruct r.
assert (
d' =
perms)
by (
eapply release_deterministe;
eauto);
clarify.
specialize (
ESP0 a);
rewrite ESD in ESP0.
inversion ESP0;
clarify.
econstructor;
eauto.
eapply (
Rset.empty_subset);
eauto.
subst.
specialize (
ESP0 a);
rewrite ESD in ESP0.
inversion ESP0;
clarify.
econstructor;
eauto.
eapply (
Rset.empty_subset);
eauto.
inversion H3;
clarify.
inversion ESD0;
clarify.
pose (
release_no_perm _ _ _ H3).
simpl in h.
destruct r.
assert (
d' =
perms)
by (
eapply release_deterministe;
eauto);
clarify.
specialize (
ESP0 a);
rewrite ESD in ESP0.
inversion ESP0;
clarify.
eapply no_perm_release;
eauto.
subst;
simpl.
inversion H3;
econstructor;
eauto.
destruct M;
destruct m;
simpl in *;
clarify.
exists ((
MEM m'0
perms),
empty_buffer);
split.
replace (@
nil (
positive*
ext_event))
with (
nil++@
nil (
positive*
ext_event))
by auto.
econstructor;
eauto.
econstructor;
eauto.
inversion H3;
clarify.
econstructor;
eauto.
inversion ESD0;
clarify.
destruct r;
clarify.
assert (
d' =
perms)
by (
eapply release_deterministe;
eauto);
clarify.
inversion ESD;
clarify.
specialize (
ESP0 a);
rewrite ESD1 in ESP0.
inversion ESP0;
clarify.
destruct (
Rset.subset_singleton _ _ ALONE);
clarify.
econstructor;
eauto.
rewrite <-
H2.
assert (
not (
Rset.mem tid Rset.empty))
by (
eapply Rset.empty_not_mem).
erewrite Rset.not_mem_remove_nop;
eauto.
eapply check_perm_gobalstore with (
s:=
Rset.empty);
eauto.
unfold Rset.singleton in H2;
rewrite Rset.remove_add in H2;
auto.
apply Rset.empty_not_mem.
inversion H3;
clarify.
inversion ESD0;
clarify.
pose (
release_no_perm _ _ _ H3).
simpl in h.
destruct r.
assert (
d' =
perms)
by (
eapply release_deterministe;
eauto);
clarify.
simpl.
split; [|
intuition].
eapply no_perm_release;
eauto.
split; [|
intuition].
subst;
simpl.
inversion H3;
econstructor;
eauto.
>
intro SAFE;
intros.
exploit ext_trace_release;
eauto;
intros (
M' &
HM1 &
HM2).
inv H1.
>
assert (
exists M'',
mem_step tid M' (
MErmw false p v (
rmw_CAS o n))
M''
/\
mem_step tid m'' (
MEperm PErelease)
M'').
inv HM1;
inv H0;
simpl in *.
destruct release.
inversion ESD.
assert (
d'0=
d')
by (
eapply release_functional;
eauto);
clarify.
exists (
MEM m'
d');
split;
constructor;
eauto.
econstructor;
eauto.
exists (
MEM m'
d');
split;
constructor;
eauto.
inversion ESD.
subst.
specialize (
ESP0 p).
inv ESP0;
clarify.
rewrite ESD0 in H0;
inv H0.
rewrite ESD0 in H1;
inv H1.
rewrite Rset.not_mem_remove_nop;
auto.
apply Rset.empty_not_mem.
rewrite <-
ESP;
assumption.
destruct H1 as (
M'' &
M1 &
M2).
destruct M.
exists (
M'',
empty_buffer);
split; [
idtac| (
split;[
eassumption|
intuition])].
apply bigstep_simpl;
eauto.
econstructor;
eauto.
rewrite <-
H8;
econstructor;
eauto.
>
destruct st;
destruct p;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep.
intros (
M' &
HM1 &
HM2).
econstructor;
split; [
idtac|
eassumption].
inv HM1;
econstructor;
eauto.
econstructor;
eauto.
>
destruct st;
destruct p;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_if_false;
eauto.
>
destruct st'';
destruct p;
intro SAFE;
intros.
exploit IHbigstep1;
eauto;
clear IHbigstep1 H0.
intros (
M' &
HM1 &
HM2 &
HM3).
exploit (
IHbigstep2 H2);
eauto;
clear IHbigstep2 H1.
intros (
M'' &
HM1' &
HM2').
inv HM1;
inv HM1'.
exists (
m''0,
b''0);
split; [|
auto].
eapply bigstep_left_ext in H8;
eauto.
instantiate (1:=
tr')
in H8.
simpl in *.
exploit H8;
eauto;
intro;
clear H8.
inversion H0;
clarify;
clear H0.
repeat rewrite app_ass.
rewrite <- (
app_ass tr').
rewrite <-
H4.
rewrite <-
app_ass.
rewrite app_ass.
rewrite app_ass.
rewrite <-
app_ass.
econstructor;
eauto.
econstructor;
eauto.
>
destruct st;
destruct p;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_while_true_abrupt;
eauto.
red;
intros.
inv H3;
eelim H1;
eauto.
>
intro SAFE;
intros.
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
replace (@
nil (
positive*
ext_event))
with (
nil++@
nil (
positive*
ext_event))
by auto.
destruct M.
econstructor;
eauto.
simpl in *;
subst.
inversion H0;
inversion ESD;
clarify.
eapply exec_while_false;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep H.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split; [
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
econstructor;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep1;
eauto;
clear IHbigstep1 H.
intros (
M' &
HM1 &
HM2 &
HM3).
exploit IHbigstep2;
eauto;
clear IHbigstep2 H0.
intros (
M'' &
HM4 &
HM5 &
HM6).
econstructor;
eauto;
split; [
idtac|
eauto].
inv HM1;
inv HM4.
eapply bigstep_left_ext in H7;
eauto.
instantiate (1:=
tr')
in H7.
exploit H7;
eauto;
intro.
inv H.
rewrite app_ass.
rewrite <- (
app_ass tr').
rewrite <-
H11.
rewrite app_ass.
rewrite <-
app_ass.
econstructor;
eauto.
econstructor;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep H.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eauto|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_seq_abrupt;
eauto.
red;
intros.
inv H;
eelim H0;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep H.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_branch_left;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep H.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_branch_right;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep1;
eauto;
clear IHbigstep1 H.
intros (
M' &
HM1 &
HM2 &
HM5).
exploit IHbigstep2;
eauto;
clear IHbigstep2 H0.
intros (
M'' &
HM3 &
HM4).
econstructor;
split; [
idtac|
eassumption].
inv HM1;
inv HM3.
eapply bigstep_left_ext in H7;
eauto.
exploit H7;
eauto;
intro.
inv H.
rewrite app_ass.
rewrite <- (
app_ass tr').
rewrite <-
H11.
rewrite app_ass.
rewrite <-
app_ass.
econstructor;
eauto.
econstructor;
eauto.
>
destruct st;
destruct st';
destruct p;
destruct p0;
intro SAFE;
intros.
exploit IHbigstep;
eauto;
clear IHbigstep H.
intros (
M' &
HM1 &
HM2 &
HM3).
econstructor;
split; [
idtac|(
split;[
eassumption|
intuition])].
inv HM1;
econstructor;
eauto.
eapply exec_loop_next_abrupt;
eauto.
red;
intros.
inv H;
eelim H0;
eauto.
Qed.
Lemma release_no_perm' :
forall t d d',
release t d d' ->
has_no_perm t d'.
Proof.
intros.
intro.
specialize (H p); inversion H; clarify.
Qed.
Lemma no_perm_release' :
forall t d,
has_no_perm t d ->
release t d d.
Proof.
intros.
intro.
specialize (
H p).
unfold is_free in H.
destruct (
d p);
clarify.
econstructor;
eauto.
assert (
Rset.remove t s =
s).
eapply Rset.not_mem_remove_nop;
eauto.
congruence.
rewrite <-
H0 at 2.
econstructor;
eauto.
Qed.
Lemma release_is_free' :
forall t p m m',
mem_step t m (
MEperm PErelease)
m' ->
is_free t (
perms m'
p).
Proof.
intros.
inversion H; inversion ESD; eauto.
Qed.
Hint Resolve release_is_free'.
Lemma free_ext_free :
forall tid m m'
p l b b',
is_free tid ((
perms m)
p) ->
ext_trace tid Interleaved (
m,
b)
l (
m',
b') ->
is_free tid ((
perms m')
p).
Proof.
intros.
destruct m;
destruct m';
clarify.
replace (
MEM mem_rtl0 perms0)
with (
fst ((
MEM mem_rtl0 perms0),
b'))
by auto.
replace (
MEM mem_rtl perms)
with (
fst ((
MEM mem_rtl perms),
b))
in H by auto.
eapply same_perm_ext;
eauto.
Qed.
Hint Resolve free_ext_free.
Lemma bigste_no_perm_update :
forall ge sp tid st stmt tr st'
af,
bigstep ge sp tid st stmt af tr st' ->
no_perm_update stmt ->
let (
m,
_) :=
fst st in
let (
m',
_) :=
fst st'
in
forall p,
is_free tid (
perms m p) ->
is_free tid (
perms m'
p).
Proof.
induction 1;
simpl;
intros;
(
try destruct r;
clarify);
(
try destruct st);
(
try destruct st');
(
try destruct st'');
(
try congruence);
eauto.
exploit IHbigstep;
eauto.
Existential 1 :=
nil.
inversion H1;
clarify.
destruct release.
simpl in H4;
congruence.
inversion H1;
clarify.
inversion H0;
clarify.
exploit free_ext_free;
eauto.
destruct p;
simpl;
intros.
unfold is_true in *;
rewrite andb_true_iff in H1;
destruct H1;
auto.
exploit IHbigstep;
eauto.
unfold is_true in *;
rewrite andb_true_iff in H1;
destruct H1;
auto.
exploit IHbigstep;
eauto.
destruct p;
simpl;
intros.
exploit IHbigstep2;
eauto.
exploit IHbigstep1;
eauto.
destruct p;
simpl;
intros.
exploit IHbigstep;
eauto.
destruct p;
destruct p0;
simpl;
intros.
exploit IHbigstep;
eauto.
simpl;
eapply andb_true_iff;
auto.
destruct p;
destruct p0;
simpl;
intros.
unfold is_true in *;
rewrite andb_true_iff in H2;
destruct H2;
auto.
exploit IHbigstep2;
eauto.
exploit IHbigstep1;
eauto.
destruct p;
destruct p0;
simpl;
intros.
unfold is_true in *;
rewrite andb_true_iff in H1;
destruct H1;
auto.
exploit IHbigstep;
eauto.
destruct p;
destruct p0;
simpl;
intros.
unfold is_true in *;
rewrite andb_true_iff in H0;
destruct H0;
auto.
exploit IHbigstep;
eauto.
destruct p;
destruct p0;
simpl;
intros.
unfold is_true in *;
rewrite andb_true_iff in H0;
destruct H0;
auto.
exploit IHbigstep;
eauto.
destruct p;
destruct p0;
simpl;
intros.
exploit IHbigstep2;
eauto.
exploit IHbigstep1;
eauto.
destruct p;
destruct p0;
simpl;
intros.
exploit IHbigstep;
eauto.
Qed.
Lemma if_abrupt_release_correct:
forall tid ge sp st stmt tr st'
af,
bigstep ge sp tid st stmt af tr st' ->
if_abrupt_release stmt =
true ->
(
forall m'
rs',
st' <> (
m',
SIntra rs')) ->
mem_step tid (
fst (
fst st')) (
MEperm PErelease) (
fst (
fst st')).
Proof.
induction 1;
simpl;
auto;
intros E T;
try (
eelim T;
eauto;
fail);
try (
rewrite andb_true_iff in *;
intuition;
fail).
>
exploit IHbigstep;
eauto.
simpl.
rewrite E;
simpl.
destruct body;
auto.
destruct release;
auto.
> (
destruct (
if_abrupt_release stmt1));
(
destruct (
if_abrupt_release stmt2));
simpl in E;
clarify.
>
destruct stmt1;
simpl in E;
auto.
>
destruct stmt1;
simpl in E;
auto.
>
destruct release;
try congruence.
destruct stmt2;
try congruence.
inv H0;
inv H;
clarify.
simpl in *.
pose (
release_no_perm _ _ _ H9).
exploit no_perm_release;
eauto.
>
destruct stmt2;
try congruence.
inv H0;
inv H;
clarify.
simpl in *.
pose (
release_no_perm _ _ _ H8).
exploit no_perm_release;
eauto.
>
inv H0;
inv H;
clarify.
simpl in *.
pose (
release_no_perm _ _ _ H8).
exploit no_perm_release;
eauto.
>
destruct stmt1;
simpl in E;
auto.
>
destruct stmt1;
try congruence.
>
destruct release;
try congruence.
>
destruct stmt2;
try congruence.
inv H;
inv H0;
clarify;
simpl.
pose (
release_no_perm _ _ _ H10).
exploit no_perm_release;
eauto.
>
destruct stmt2;
try congruence.
inv H;
inv H0;
clarify;
simpl.
pose (
release_no_perm _ _ _ H9).
exploit no_perm_release;
eauto.
>
inv H0;
inv H;
clarify.
simpl in *.
pose (
release_no_perm _ _ _ H8).
exploit no_perm_release;
eauto.
> (
destruct (
if_abrupt_release stmt1)); (
destruct (
if_abrupt_release stmt2));
simpl in E;
clarify.
destruct stmt1;
simpl in E;
auto.
destruct stmt1;
simpl in E;
auto.
destruct stmt1;
simpl in E;
auto.
destruct release;
try congruence.
inversion H;
eelim T;
eauto.
inversion H;
eelim T;
eauto.
destruct stmt1;
simpl in E;
auto.
inversion H;
eelim T;
eauto.
inversion H;
eelim T;
eauto.
congruence.
congruence.
Qed.
Lemma bigstep_release_point:
forall ge sp tid st stmt l2 st'
af,
bigstep ge sp tid st stmt af l2 st' ->
release_point stmt ->
let (
M,
s) :=
st'
in
let (
m',
b) :=
M in
mem_step tid m' (
MEperm PErelease)
m'.
Proof.
induction 1;
simpl;
intros;
try congruence;
unfold is_true in *.
clarify.
pose (
release_no_perm _ _ _ H0).
eapply no_perm_release;
eauto.
exploit IHbigstep;
eauto.
pose (
release_no_perm _ _ _ H0).
eapply no_perm_release;
eauto.
clarify.
pose (
release_no_perm _ _ _ H0).
eapply no_perm_release;
eauto.
clarify;
inv H1.
econstructor;
eauto.
econstructor;
eauto.
pose (
release_no_perm'
_ _ _ ESP).
econstructor;
eauto.
econstructor;
eauto.
subst.
inversion H1;
clarify.
inversion H0;
clarify.
econstructor;
eauto.
econstructor;
eauto.
rewrite andb_true_iff in H1;
destruct H1;
eapply IHbigstep;
eauto.
rewrite andb_true_iff in H1;
destruct H1;
eapply IHbigstep;
eauto.
apply orb_prop in H2;
destruct H2.
destruct st';
auto.
rewrite andb_true_iff in H2;
destruct H2;
destruct st ;
auto.
eapply IHbigstep2;
eauto.
destruct st';
intros.
destruct p;
intros.
exploit bigste_no_perm_update;
eauto.
rewrite andb_true_iff in H2;
destruct H2;
auto.
intros.
simpl in H3;
clarify.
destruct m;
econstructor.
econstructor.
intro.
specialize (
H3 p).
rewrite andb_true_iff in H2;
destruct H2;
auto.
specialize (
IHbigstep1 H2).
assert (
has_no_perm tid m')
by (
eapply release_no_perm;
eauto).
specialize (
H5 p);
specialize (
H3 H5).
destruct m';
simpl in *.
destruct (
perms p);
clarify.
unfold is_free in H3.
econstructor;
eauto.
unfold is_free in H3.
assert (
Rset.remove tid s =
s )
by
(
eapply Rset.not_mem_remove_nop;
eauto;
congruence).
rewrite <-
H6 at 2.
econstructor;
eauto.
apply orb_prop in H1;
destruct H1.
destruct st';
destruct p;
auto.
rewrite andb_true_iff in H1;
destruct H1;
destruct st ;
auto.
exploit if_abrupt_release_correct;
eauto;
intros.
rewrite andb_true_iff in H1;
destruct H1;
destruct st ;
auto.
exploit IHbigstep;
eauto.
rewrite andb_true_iff in H0;
destruct H0;
destruct st ;
auto.
exploit IHbigstep;
eauto.
rewrite andb_true_iff in H0;
destruct H0;
destruct st ;
auto.
exploit IHbigstep;
eauto.
Qed.
Lemma refines_remove_perm:
forall stmt,
release_point stmt =
true ->
refines (
Sseq Sfreeperm stmt) (
Sseq (
remove_perm stmt)
Sfreeperm).
Proof.