Require Import Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Pointers.
Require Import Events.
Require Import Globalenvs.
Require Import Libtactics.
Require Import TSOmachine.
Require Import TSOsimulation.
Require Cminor.
Require Import Cminorgen.
Require Import Cstacked.
Require Import Csharpminor.
Require Import Simulations.
Require Import Mem.
Require Import Memeq.
Require Import Memcomp.
Require Import Cstackedproofsimdef.
Require Import Permutation.
Section UNBUFFER_SIMS.
Variable cst_globenv :
genv *
gvarenv.
Variable csm_globenv :
genv *
gvarenv.
Let cshm_lts := (
mklts event_labels (
Comp.step tso_mm cs_sem csm_globenv)).
Let cst_lts := (
mklts event_labels (
Comp.step tso_mm cst_sem cst_globenv)).
Notation cont_related := (
cont_related cst_globenv).
Notation expr_cont_related := (
expr_cont_related cst_globenv).
Notation state_related := (
state_related cst_globenv).
Notation buffered_states_related := (
buffered_states_related cst_globenv).
Notation tso_pc_related_witt := (
tso_pc_related_witt cst_globenv).
Notation tso_pc_related := (
tso_pc_related cst_globenv).
Notation tso_pc_unsafe_related := (
tso_pc_unsafe_related cst_globenv).
Definition mem_agrees_on_scratch (
m :
mem)
(
m' :
mem)
(
rs :
list arange) :
Prop :=
forall r p c,
In r rs ->
range_inside (
range_of_chunk p c)
r ->
scratch_ptr p ->
load_ptr c m p =
load_ptr c m'
p.
Lemma env_related_load_inv:
forall tp sp smem smem'
te se,
env_related tp sp smem te se ->
mem_agrees_on_scratch smem smem'
sp ->
env_related tp sp smem'
te se.
Proof.
Lemma mem_agrees_on_scratch_app1:
forall m m'
s1 s2,
mem_agrees_on_scratch m m' (
s1 ++
s2) ->
mem_agrees_on_scratch m m'
s1.
Proof.
intros m m'
s1 s2 MAS r p c IN RI PS.
eapply MAS;
try edone.
apply in_or_app.
by left.
Qed.
Lemma mem_agrees_on_scratch_app2:
forall m m'
s1 s2,
mem_agrees_on_scratch m m' (
s1 ++
s2) ->
mem_agrees_on_scratch m m'
s2.
Proof.
intros m m'
s1 s2 MAS r p c IN RI PS.
eapply MAS;
try edone.
apply in_or_app.
by right.
Qed.
Lemma cont_related_load_inv:
forall tp sp smem smem'
te se,
cont_related tp sp smem te se ->
mem_agrees_on_scratch smem smem'
sp ->
cont_related tp sp smem'
te se.
Proof.
Lemma expr_cont_related_load_inv:
forall tp sp smem smem'
tps sps te se,
expr_cont_related tp sp smem tps sps te se ->
mem_agrees_on_scratch smem smem'
sp ->
expr_cont_related tp sp smem'
tps sps te se.
Proof.
intros tp sp smem smem'
tps sps te se C.
revert smem'.
(
expr_cont_related_cases (
induction C)
Case);
try (
eby intros;
econstructor;
try (
apply IHC);
try (
eapply cont_related_load_inv)).
Qed.
Lemma state_related_load_inv:
forall tp sp smem smem'
te se,
state_related tp sp smem te se ->
mem_agrees_on_scratch smem smem'
sp ->
state_related tp sp smem'
te se.
Proof.
Lemma mem_agrees_on_scratch_perm:
forall m m'
p p',
mem_agrees_on_scratch m m'
p ->
Permutation p p' ->
mem_agrees_on_scratch m m'
p'.
Proof.
Definition range_list_allocated (
p :
list arange)
(
m :
mem) :
Prop :=
forall r :
arange,
In r p ->
range_allocated r MObjStack m.
Lemma range_disjoint_remove:
forall p l,
range_list_disjoint l ->
range_list_disjoint (
range_remove p l).
Proof.
induction l as [|[
ph nh]
l IH].
done.
simpl.
intros [
DISJ RNI].
destruct (
Ptr.eq_dec ph p)
as [-> |
N].
done.
simpl.
split.
by apply IH.
intros []
IN'.
eby eapply RNI,
in_range_remove.
Qed.
Lemma range_list_disjoint_remove_not_in:
forall p l,
(
forall r,
In r l ->
range_non_empty r) ->
range_list_disjoint l ->
forall n, ~
In (
p,
n) (
range_remove p l).
Proof.
induction l as [|[
ph nh]
l IH];
simpl.
by intros.
intros RNE [
RD RNI]
n IN.
destruct (
Ptr.eq_dec ph p)
as [-> |
N].
assert (
PNE:
range_non_empty (
p,
n)).
apply RNE.
right.
done.
assert (
PHNE:
range_non_empty (
p,
nh))
by (
apply RNE;
left;
done).
apply RNI in IN.
by eapply non_empty_same_ptr_overlap in IN.
simpl in IN.
destruct IN as [
E |
IN].
by inv E.
by eapply IH;
try edone;
intros;
apply RNE;
right.
Qed.
Lemma part_update_range_list_disjoint_allocated:
forall bi sp smem sp'
smem',
apply_buffer_item bi smem =
Some smem' ->
part_update bi sp =
Some sp' ->
range_list_allocated sp smem ->
range_list_disjoint sp ->
range_list_allocated sp'
smem' /\
range_list_disjoint sp'.
Proof.
Lemma pointer_in_range_list_in:
forall p l,
pointer_in_range_list p l =
true ->
exists n,
In (
p,
n)
l.
Proof.
intros p.
induction l as [|[
p'
n']
l IH].
done.
simpl;
destruct (
Ptr.eq_dec p p')
as [-> |
N].
intro.
eexists.
left;
reflexivity.
intro H.
destruct (
IH H).
eexists;
right;
eassumption.
Qed.
Lemma mem_agrees_on_scratch_preserved_by_pv_update:
forall bi smem smem'
sp sp'
smemx smemx',
part_update bi sp =
Some sp' ->
range_list_disjoint sp ->
range_list_allocated sp smem ->
range_list_allocated sp smem' ->
apply_buffer_item bi smem =
Some smemx ->
apply_buffer_item bi smem' =
Some smemx' ->
mem_agrees_on_scratch smem smem'
sp ->
mem_agrees_on_scratch smemx smemx'
sp'.
Proof.
Lemma mem_agrees_on_scratch_preserved_by_pv_buffer_update:
forall b smem smem'
sp sp'
smemx smemx',
part_update_buffer b sp =
Some sp' ->
range_list_disjoint sp ->
range_list_allocated sp smem ->
range_list_allocated sp smemx ->
apply_buffer b smem =
Some smem' ->
apply_buffer b smemx =
Some smemx' ->
mem_agrees_on_scratch smem smemx sp ->
mem_agrees_on_scratch smem'
smemx'
sp'.
Proof.
Lemma buffered_states_related_prepend_tgt:
forall bi tb tp ts sb sp sm ss tp',
part_update bi tp' =
Some tp ->
(
buffered_states_related tb tp ts sb sp sm ss <->
buffered_states_related (
bi ::
tb)
tp'
ts sb sp sm ss).
Proof.
intros bi tb tp ts sb sp sm ss tp' PU.
split.
intros [sm' [sp' [tpx [ABI [PUBt [PUBs SR]]]]]].
exists sm'; exists sp'; exists tpx.
split. done.
split. by unfold part_update_buffer; simpl; rewrite PU.
by repeat (split; try done).
intros [sm' [sp' [tpx [ABI [PUBt [PUBs SR]]]]]].
exists sm'; exists sp'; exists tpx.
split. done.
split. by unfold part_update_buffer in *; simpl in *; rewrite PU in *.
by repeat (split; try done).
Qed.
Lemma buffered_states_related_prepend_src:
forall b tb tp ts sb sp sm ss sm'
sp',
part_update_buffer b sp' =
Some sp ->
apply_buffer b sm' =
Some sm ->
(
buffered_states_related tb tp ts sb sp sm ss <->
buffered_states_related tb tp ts (
b ++
sb)
sp'
sm'
ss).
Proof.
intros b tb tp ts sb sp sm ss sm'
sp'
PUB ABI.
split.
intros [
smx [
spx [
tpx [
ABIx [
PUBtx [
PUBsx SRx]]]]]].
exists smx;
exists spx;
exists tpx.
split.
by rewrite apply_buffer_app,
ABI.
split.
done.
split.
unfold part_update_buffer in *.
by rewrite fold_left_opt_app,
PUB.
done.
intros [
smx [
spx [
tpx [
ABIx [
PUBtx [
PUBsx SRx]]]]]].
exists smx;
exists spx;
exists tpx.
split.
by rewrite apply_buffer_app,
ABI in ABIx.
split.
done.
split.
unfold part_update_buffer in *.
by rewrite fold_left_opt_app,
PUB in PUBsx.
done.
Qed.
Lemma buffered_states_related_load_inv_gen:
forall tb tp ts b sb sp smem ss smem'
spx smemx smemx',
range_list_disjoint sp ->
range_list_allocated sp smem ->
range_list_allocated sp smem' ->
buffer_safe_for_mem (
b ++
flatten sb)
smem ->
buffer_safe_for_mem (
b ++
flatten sb)
smem' ->
mem_agrees_on_scratch smem smem'
sp ->
apply_buffer b smem =
Some smemx ->
apply_buffer b smem' =
Some smemx' ->
part_update_buffer b sp =
Some spx ->
buffers_related tb tp sb spx ->
buffered_states_related tb tp ts (
flatten sb)
spx smemx ss ->
buffered_states_related tb tp ts (
flatten sb)
spx smemx'
ss.
Proof.
intros tb tp ts b sb sp smem ss smem'
spx smemx smemx'.
intros RLD RLA RLA'
BS BS'
MAS AB AB'
PVU BR BSR.
revert smemx smemx'
b BS BS'
AB AB'
PVU BSR.
(
buffers_related_cases (
induction BR)
Case);
intros smemx smemx'
b BS BS'
SMAB SMAB'
PVU BSR.
Case "
buffers_related_empty".
destruct BSR as [
sm' [
sp' [
tp' [
ABI [
PUBt [
PUBs [
SR SCO]]]]]]].
simpl in BS,
BS'.
rewrite <-
app_nil_end in *.
eexists;
eexists;
eexists;
unfold part_update_buffer in *;
simpl in *;
inv PUBs.
do 3 (
split; [
edone|]).
split; [|
done].
eapply state_related_load_inv.
edone.
eapply mem_agrees_on_scratch_preserved_by_pv_buffer_update.
edone.
done.
apply RLA.
apply RLA'.
inv ABI;
done.
done.
done.
Case "
buffers_related_alloc".
simpl in BS,
BS'.
rewrite <-
app_ass in BS,
BS'.
destruct (
buffer_safe_for_mem_app1 _ _ _ BS)
as [
mx ABx].
destruct (
buffer_safe_for_mem_app1 _ _ _ BS')
as [
mx'
ABx'].
simpl.
apply ->
buffered_states_related_prepend_src.
apply ->
buffered_states_related_prepend_tgt.
eapply IHBR.
edone.
edone.
edone.
edone.
unfold part_update_buffer in *.
rewrite fold_left_opt_app,
PVU.
done.
apply <-
buffered_states_related_prepend_src.
apply <-
buffered_states_related_prepend_tgt.
edone.
simpl.
destruct valid_alloc_range_dec;
try done.
destruct range_in_dec as [[
r' [
INr RO]] |
RNI];
try done.
specialize (
RIN _ INr).
done.
unfold range_not_in in RIN.
by rewrite apply_buffer_app,
SMAB in ABx.
unfold part_update_buffer in *.
done.
simpl.
destruct valid_alloc_range_dec;
try done.
destruct range_in_dec as [[
r' [
INr RO]] |
RNI];
try done.
specialize (
RIN _ INr).
done.
by rewrite apply_buffer_app,
SMAB'
in ABx'.
done.
Case "
buffers_related_free".
simpl in BS,
BS'.
rewrite <-
app_ass in BS,
BS'.
destruct (
buffer_safe_for_mem_app1 _ _ _ BS)
as [
mx ABx].
destruct (
buffer_safe_for_mem_app1 _ _ _ BS')
as [
mx'
ABx'].
apply ->
buffered_states_related_prepend_src.
apply ->
buffered_states_related_prepend_tgt.
eapply IHBR.
edone.
edone.
edone.
edone.
unfold part_update_buffer in *.
rewrite fold_left_opt_app,
PVU.
done.
apply <-
buffered_states_related_prepend_src.
apply <-
buffered_states_related_prepend_tgt.
edone.
simpl.
by destruct (
Ptr.eq_dec p p).
by rewrite apply_buffer_app,
SMAB in ABx.
unfold part_update_buffer in *.
done.
simpl.
by destruct Ptr.eq_dec.
by rewrite apply_buffer_app,
SMAB'
in ABx'.
done.
Case "
buffers_related_other".
simpl in BS,
BS'.
rewrite app_comm_cons, <-
app_ass in BS,
BS'.
destruct (
buffer_safe_for_mem_app1 _ _ _ BS)
as [
mx ABx].
destruct (
buffer_safe_for_mem_app1 _ _ _ BS')
as [
mx'
ABx'].
apply ->
buffered_states_related_prepend_src.
apply ->
buffered_states_related_prepend_tgt.
eapply IHBR.
edone.
edone.
edone.
edone.
unfold part_update_buffer in *.
rewrite fold_left_opt_app,
PVU.
simpl.
rewrite (
buffer_item_irrelevant_part_update _ _ BIIR).
done.
apply <-
buffered_states_related_prepend_src.
apply <-
buffered_states_related_prepend_tgt.
edone.
simpl.
by rewrite (
buffer_item_irrelevant_part_update _ _ BIIR).
by rewrite apply_buffer_app,
SMAB in ABx.
unfold part_update_buffer in *.
simpl.
rewrite (
buffer_item_irrelevant_part_update _ _ BIIR).
done.
rewrite (
buffer_item_irrelevant_part_update _ _ BIIR).
done.
by rewrite apply_buffer_app,
SMAB'
in ABx'.
unfold part_update_buffer.
simpl.
rewrite (
buffer_item_irrelevant_part_update _ _ BIIR).
done.
Qed.
Lemma buffered_states_related_load_inv:
forall tb tp ts sb sp smem ss smem',
buffers_related tb tp sb sp ->
buffered_states_related tb tp ts (
flatten sb)
sp smem ss ->
range_list_disjoint sp ->
range_list_allocated sp smem ->
range_list_allocated sp smem' ->
buffer_safe_for_mem (
flatten sb)
smem ->
buffer_safe_for_mem (
flatten sb)
smem' ->
mem_agrees_on_scratch smem smem'
sp ->
buffered_states_related tb tp ts (
flatten sb)
sp smem'
ss.
Proof.
Lemma tso_consistent_safe_buffer_app:
forall stso sthr t bis rb,
Comp.consistent tso_mm cs_sem (
stso,
sthr) ->
stso.(
tso_buffers)
t =
bis ++
rb ->
buffer_safe_for_mem bis stso.(
tso_mem).
Proof.
Lemma alloc_ptr_tgt_preserves_load_rel:
forall cstm csmm cstm'
r k,
load_values_related cstm csmm ->
alloc_ptr r k cstm =
Some cstm' ->
load_values_related cstm'
csmm.
Proof.
intros cstm csmm cstm'
r k LVR AP.
intros p MP c.
specialize (
LVR p MP c).
destruct (
load_ptr c cstm p)
as [
csv|]
_eqn :
CSLD;
destruct (
load_ptr c csmm p)
as [
cmv|]
_eqn :
CMLD;
try done;
try by rewrite (
load_some_alloc CSLD AP).
by destruct (
load_ptr c cstm'
p).
Qed.
Lemma alloc_ptr_stack_preserves_mem_partitioning:
forall m m'
p n part t,
mem_related_with_partitioning m part ->
alloc_ptr (
p,
n)
MObjStack m =
Some m' ->
mem_related_with_partitioning m'
(
update_partitioning t ((
p,
n) :: (
part t))
part).
Proof.
Lemma alloc_ptr_non_stack_preserves_mem_partitioning:
forall m m'
p n k part t,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
alloc_ptr (
p,
n)
k m =
Some m' ->
mem_related_with_partitioning m'
(
update_partitioning t (
part t)
part).
Proof.
intros m m'
p n k part t [
PD [
LD MR]]
NS AP.
unfold update_partitioning.
split.
intros t1 t2 N r IN r'
IN'.
destruct (
peq t1 t)
as [-> |
Nt1];
destruct (
peq t2 t)
as [-> |
Nt2];
eby eapply (
PD _ _ N r IN r'
IN').
split.
intros t'.
destruct (
peq t'
t);
apply LD.
intro r.
split.
intros [
t'
IN].
destruct (
peq t'
t)
as [
_ |
N];
try (
apply (
alloc_preserves_allocated AP);
apply (
proj1 (
MR _));
eexists;
eassumption).
intro RA.
destruct (
alloc_preserves_allocated_back AP _ _ RA)
as [[-> <-] |
RAo];
try done.
destruct (
proj2 (
MR _)
RAo)
as [
t'
IN'].
exists t'.
destruct (
peq t'
t)
as [-> |
N];
try apply in_cons;
done.
Qed.
Lemma store_ptr_preserves_mem_partitioning:
forall m m'
c p v part,
mem_related_with_partitioning m part ->
store_ptr c m p v =
Some m' ->
mem_related_with_partitioning m'
part.
Proof.
Lemma store_ptr_preserves_mem_partitioning2:
forall m m'
c p v part t,
mem_related_with_partitioning m part ->
store_ptr c m p v =
Some m' ->
mem_related_with_partitioning m'
(
update_partitioning t (
part t)
part).
Proof.
intros m m'
c p v part t [
PD [
LD MR]]
ST.
unfold update_partitioning.
split.
intros x y NE.
destruct (
peq x t)
as [-> |
Nx];
destruct (
peq y t)
as [-> |
Ny];
apply (
PD _ _ NE).
split.
intro t'.
destruct (
peq t'
t);
apply LD.
intro r.
split.
intros [
t'
IN].
apply (
proj1 (
store_preserves_allocated_ranges ST _ _)).
apply (
proj1 (
MR _)).
destruct (
peq t'
t);
eby eexists.
intro RA.
apply (
proj2 (
store_preserves_allocated_ranges ST _ _))
in RA.
destruct (
proj2 (
MR _)
RA)
as [
t'
IN].
exists t'.
by destruct (
peq t'
t)
as [-> |
_].
Qed.
Lemma ranges_disjoint_dont_overlap:
forall r r',
ranges_disjoint r r' ->
ranges_overlap r r' ->
False.
Proof.
intros r r' D O. apply O, D. Qed.
Lemma free_ptr_preserves_mem_partitioning:
forall m m'
p k part t,
mem_related_with_partitioning m part ->
free_ptr p k m =
Some m' ->
(
exists n,
In (
p,
n) (
part t)) ->
mem_related_with_partitioning m'
(
update_partitioning t (
range_remove p (
part t))
part).
Proof.
intros m m'
p k part t [
PD [
LD MR]]
FP [
n INP].
unfold update_partitioning.
pose proof (
free_cond_spec p k m)
as Fspec.
rewrite FP in Fspec.
destruct Fspec as [
n'
Fspec].
assert (
INpe:
exists t,
In (
p,
n) (
part t)).
eby eexists.
destruct (
alloc_ranges_same Fspec (
proj1 (
MR _)
INpe))
as [-> ->].
split.
intros t1 t2 N r IN r'
IN'.
destruct (
peq t1 t)
as [-> |
Nt1];
destruct (
peq t2 t)
as [-> |
Nt2];
try done;
try (
eapply PD; [
apply N |
apply IN |
apply IN']).
destruct r as [
rp rn].
apply in_range_remove in IN.
eapply PD; [
apply N |
apply IN |
apply IN'].
destruct r'.
apply in_range_remove in IN'.
eapply PD; [
apply N |
apply IN |
apply IN'].
split.
intros t'.
destruct (
peq t'
t)
as [
_ |
N];
try apply range_disjoint_remove;
apply LD.
intro r.
split.
intros [
t'
IN].
destruct (
peq t'
t)
as [<- |
N].
destruct r as [
pr nr];
pose proof (
in_range_remove _ _ _ _ IN)
as IN2.
assert (
IN':
exists t,
In (
pr,
nr) (
part t)).
eexists;
eassumption.
apply (
proj1 (
MR _))
in IN'.
destruct (
free_preserves_allocated FP _ _ IN')
as [|[
E _]].
done.
simpl in E.
rewrite E in *.
byContradiction.
eapply (
range_list_disjoint_remove_not_in p (
part t')).
intros rp INp.
assert (
INrpe :
exists t,
In rp (
part t)).
eexists;
eassumption.
by apply (
proj1 (
MR _)),
allocated_range_valid,
valid_alloc_range_non_empty in INrpe.
apply LD.
simpl in E.
subst.
eassumption.
assert (
IN':
exists t,
In r (
part t)).
eexists;
eassumption.
apply (
proj1 (
MR _))
in IN'.
destruct r as [
pr nr].
destruct (
free_preserves_allocated FP _ _ IN')
as [|[
E _]].
done.
simpl in E.
subst.
byContradiction.
eapply ranges_disjoint_dont_overlap.
apply (
PD _ _ N _ IN _ INP).
eapply non_empty_same_ptr_overlap;
eapply valid_alloc_range_non_empty,
allocated_range_valid, (
proj1 (
MR _));
eexists;
eassumption.
intro RA.
pose proof (
free_preserves_allocated_back FP _ _ RA)
as RAo.
destruct (
proj2 (
MR _)
RAo)
as [
t'
IN'].
exists t'.
destruct (
peq t'
t)
as [-> |
N];
try done.
destruct r as [
pr nr].
destruct (
in_range_remove_back p _ _ _ IN')
as [<- |
RR].
destruct (
free_not_allocated FP _ _ RA).
done.
Qed.
Lemma free_ptr_non_stack_preserves_mem_partitioning:
forall m m'
p k part t,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
free_ptr p k m =
Some m' ->
mem_related_with_partitioning m'
(
update_partitioning t (
part t)
part).
Proof.
intros m m'
p k part t [
PD [
LD MR]]
NS FP.
unfold update_partitioning.
split.
intros t1 t2 N r IN r'
IN'.
destruct (
peq t1 t)
as [-> |
Nt1];
destruct (
peq t2 t)
as [-> |
Nt2];
eby eapply (
PD _ _ N r IN r'
IN').
split.
intros t'.
destruct (
peq t'
t);
apply LD.
intro r.
split.
intros [
t'
IN].
destruct (
peq t'
t)
as [<- |
N];
(
assert (
RA :
range_allocated r MObjStack m);
[
apply (
proj1 (
MR _));
eby eexists |
by destruct (
free_preserves_allocated FP _ _ RA)
as [
RA' | [<- <-]]]).
intro RA.
apply (
free_preserves_allocated_back FP)
in RA.
destruct (
proj2 (
MR _)
RA)
as [
t'
IN'].
exists t'.
destruct (
peq t'
t)
as [-> |
N];
try apply in_cons;
done.
Qed.
Lemma apply_buffer_item_preserves_mem_partitioning:
forall m m'
bi part part'
t,
mem_related_with_partitioning m part ->
apply_buffer_item bi m =
Some m' ->
part_update bi (
part t) =
Some part' ->
mem_related_with_partitioning m' (
update_partitioning t part'
part).
Proof.
Lemma mem_related_with_partitioning_ext:
forall m part part',
mem_related_with_partitioning m part ->
(
forall t,
part t =
part'
t) ->
mem_related_with_partitioning m part'.
Proof.
intros m part part' (
PD &
RLD &
MRWP)
E.
split.
intros t t'.
rewrite <- !
E.
apply PD.
split.
intro t;
rewrite <- !
E;
apply RLD.
intro r;
split.
intros [
t IN].
rewrite <-
E in IN.
apply (
proj1 (
MRWP r)).
eby eexists.
intro RA.
destruct (
proj2 (
MRWP r)
RA)
as [
t'
IN].
exists t'.
by rewrite <-
E.
Qed.
Lemma update_partitioning_s:
forall t p part,
update_partitioning t p part t =
p.
Proof.
by intros;
unfold update_partitioning;
destruct peq. Qed.
Lemma update_partitioning_o:
forall t'
t p part,
t' <>
t ->
update_partitioning t p part t' =
part t'.
Proof.
by intros;
unfold update_partitioning;
destruct peq. Qed.
Lemma apply_buffer_preserves_mem_partitioning:
forall b m m'
part part'
t,
mem_related_with_partitioning m part ->
apply_buffer b m =
Some m' ->
part_update_buffer b (
part t) =
Some part' ->
mem_related_with_partitioning m' (
update_partitioning t part'
part).
Proof.
Lemma store_ptr_mem_consistent:
forall m c p v m',
store_ptr c m p v =
Some m' ->
mrestr m (
Ptr.block p) =
true.
Proof.
Lemma apply_scratch_preserve_machine_allocs:
forall bi m m'
p n k,
apply_buffer_item bi m =
Some m' ->
is_item_scratch_update bi ->
machine_ptr p ->
(
range_allocated (
p,
n)
k m <->
range_allocated (
p,
n)
k m').
Proof.
Lemma apply_scratch_preserves_load_rel:
forall tmem bi m m',
apply_buffer_item bi m =
Some m' ->
is_item_scratch_update bi ->
load_values_related tmem m ->
load_values_related tmem m'.
Proof.
intros tmem bi m m'
ABI ISU LR p MP c.
replace (
load_ptr c m'
p)
with (
load_ptr c m p).
apply (
LR p MP c).
unfold apply_buffer_item in ABI.
buffer_item_cases (
destruct bi as [
p'
c'
v' |
p'
n'
k' |
p'
k'])
Case.
Case "
BufferedWrite".
eapply load_store_other.
apply ABI.
destruct p;
destruct p';
left.
intros ->.
simpl in *.
by rewrite MP in ISU.
Case "
BufferedAlloc".
eapply sym_eq,
load_alloc_other.
apply ABI.
destruct p;
destruct p';
left.
intros ->.
simpl in *.
destruct k';
try done.
by rewrite MP in ISU.
Case "
BufferedFree".
pose proof (
free_cond_spec p'
k'
m)
as Fspec.
rewrite ABI in Fspec.
destruct Fspec as [
n RA].
eapply sym_eq,
load_free_other.
apply ABI.
edone.
destruct p;
destruct p';
left.
intros ->.
simpl in *.
destruct k';
try done.
by rewrite MP in ISU.
Qed.
Lemma apply_scratch_buffer_preserves_load_rel:
forall b tmem m m',
apply_buffer b m =
Some m' ->
(
forall bi,
In bi b ->
is_item_scratch_update bi) ->
load_values_related tmem m ->
load_values_related tmem m'.
Proof.
Lemma allocs_related_buff_disjoint:
forall b p'
n'
k'
p n pi ni ki m m',
allocs_related p n b ->
apply_buffer b m =
Some m' ->
range_allocated (
p',
n')
k'
m ->
machine_ptr p' ->
In (
BufferedAlloc pi ni ki)
b ->
ranges_disjoint (
p',
n') (
pi,
ni).
Proof.
induction b as [|
bi b IH].
done.
intros p'
n'
k'
p n pi ni ki m m'
AR AB RA MP IN.
simpl in IN,
AB.
destruct (
apply_buffer_item bi m)
as [
mi|]
_eqn :
ABI;
simpl in AB; [|
done].
pose proof ABI as AP;
unfold apply_buffer_item in AP.
destruct IN as [-> |
IN].
pose proof (
alloc_cond_spec (
pi,
ni)
ki m)
as Aspec.
rewrite AP in Aspec.
destruct Aspec as (
_ &
_ &
_ &
OA).
destruct (
ranges_disjoint_dec (
p',
n') (
pi,
ni))
as [? |
OVER].
done.
apply ranges_overlap_comm in OVER.
destruct (
OA _ _ OVER RA).
eapply IH;
try edone.
intros bi'
IN'.
apply (
AR bi' (
in_cons _ _ _ IN')).
destruct (
AR _ (
in_eq bi b))
as [
SCRATCH |
STACK].
eby eapply (
apply_scratch_preserve_machine_allocs _ _ _ _ _ _ ABI SCRATCH MP).
destruct bi as [|
px nx []|];
try done.
eby eapply alloc_preserves_allocated.
Qed.
Definition non_conflicting_allocs_buffer (
b :
list buffer_item)
(
m :
mem) :
Prop :=
forall bi,
In bi b ->
match bi with
|
BufferedAlloc p'
n'
k' =>
scratch_ptr p' \/
k' =
MObjStack /\
forall r''
k'',
ranges_overlap r'' (
p',
n') ->
~
range_allocated r''
k''
m
|
BufferedFree p'
_ =>
scratch_ptr p'
|
BufferedWrite p'
_ _ =>
scratch_ptr p'
end.
Lemma non_conflicting_allocs_buffer_from_relation:
forall b smem tp sp p n k tmem tmem',
non_stack_mem_related tmem smem ->
mem_related_with_partitioning tmem tp ->
mem_related_with_partitioning smem sp ->
(
forall t,
partition_injective (
tp t) (
sp t)) ->
allocs_related p n b ->
alloc_ptr (
p,
n)
k tmem =
Some tmem' ->
non_conflicting_allocs_buffer b smem.
Proof.
intros b smem tp sp p n k tmem tmem'
NSMR [
_ [
_ MRt]] [
_ [
_ MRs]]
PIS AR AP.
intros bi IN.
destruct (
AR _ IN)
as [
SCRATCH |
INSIDE].
unfold is_item_scratch_update in SCRATCH.
destruct bi as [
pi ci vi|
pi ni []|
pi []];
try left;
done.
destruct bi as [|
pi ni []|];
try done.
destruct (
low_mem_restr (
Ptr.block pi))
as []
_eqn :
LMR;
[|
by left;
destruct pi;
simpl in *].
right.
split.
done.
intros [
p''
n'']
k''
ROVER RA.
assert (
MP :
machine_ptr pi).
by destruct pi;
simpl in *.
pose proof (
alloc_cond_spec (
p,
n)
k tmem)
as TAspec;
rewrite AP in TAspec.
destruct TAspec as (
_ &
_ &
_ &
UNAL).
assert (
ALI:
exists r',
exists k',
range_inside (
p'',
n'')
r' /\
range_allocated r'
k'
tmem).
pose proof (
NSMR (
p'',
n'')
k'')
as NSAL.
destruct k'';
try (
by apply NSAL in RA;
eexists;
eexists;
split;
[
apply range_inside_refl|
apply RA]).
destruct (
proj2 (
MRs (
p'',
n''))
RA)
as [
t INt].
assert (
MPp'' :
machine_ptr p'').
by destruct p'';
destruct pi;
destruct (
ranges_overlapD ROVER)
as [->
_];
simpl in *.
destruct (
PIS _ _ _ MPp''
INt)
as [
rt [
RI INtp]].
eexists;
eexists;
split.
apply RI.
eapply MRt.
eexists;
apply INtp.
destruct ALI as (
r' &
k' &
RI' &
RA').
eapply UNAL. 2:
apply RA'.
eapply overlap_inside_overlap.
2 :
apply INSIDE.
eapply ranges_overlap_comm,
overlap_inside_overlap.
apply ROVER.
done.
Qed.
Lemma allocs_related_preserves_alloc_load_rels:
forall b tmem smem smem'
sp sp'
p n,
allocs_related p n b ->
part_update_buffer b sp =
Some sp' ->
apply_buffer b smem =
Some smem' ->
mrestr smem =
no_mem_restr ->
(
forall p'
c',
range_inside (
range_of_chunk p'
c') (
p,
n) ->
chunk_allocated_and_aligned p'
c'
tmem ->
load_ptr c'
tmem p' =
Some Vundef) ->
non_conflicting_allocs_buffer b smem ->
load_values_related tmem smem ->
range_allocated (
p,
n)
MObjStack tmem ->
load_values_related tmem smem'.
Proof.
Lemma free_preserves_load_fail:
forall p k m m'
p'
c,
free_ptr p k m =
Some m' ->
load_ptr c m p' =
None ->
load_ptr c m'
p' =
None.
Proof.
Lemma free_src_preserves_load_rel:
forall p k sm sm'
tm,
free_ptr p k sm =
Some sm' ->
load_values_related tm sm ->
load_values_related tm sm'.
Proof.
Lemma frees_related_preserves_load_rel_src:
forall p n tm sm'
b sm,
frees_related p n b ->
apply_buffer b sm =
Some sm' ->
load_values_related tm sm ->
load_values_related tm sm'.
Proof.
Lemma free_preserves_load_back:
forall p k m m'
p'
c v,
free_ptr p k m =
Some m' ->
load_ptr c m'
p' =
Some v ->
load_ptr c m p' =
Some v.
Proof.
Lemma range_of_chunk_not_empty:
forall p c,
range_non_empty (
range_of_chunk p c).
Proof.
Lemma free_preserves_load_rel_tgt:
forall p n t tm tm'
sm sp tp,
free_ptr p MObjStack tm =
Some tm' ->
non_stack_mem_related tm sm ->
mem_related_with_partitioning sm sp ->
mem_related_with_partitioning tm tp ->
In (
p,
n) (
tp t) ->
(
forall t',
partition_injective (
tp t') (
sp t')) ->
(
forall r,
In r (
sp t) ->
ranges_disjoint r (
p,
n)) ->
load_values_related tm sm ->
load_values_related tm'
sm.
Proof.
Lemma update_part_scratch_preserves_partition_injectivity:
forall bi sp sp'
tp,
is_item_scratch_update bi ->
part_update bi sp =
Some sp' ->
partition_injective tp sp ->
partition_injective tp sp'.
Proof.
intros bi sp sp'
tp ISU PU PI p n MP IN.
unfold is_item_scratch_update,
part_update in ISU,
PU.
buffer_item_cases (
destruct bi as [
p'
c'
v'|
p'
n'
k'|
p'
k'])
Case.
Case "
BufferedWrite".
destruct (
low_mem_restr (
Ptr.block p'))
as []
_eqn :
LMR;
destruct (
chunk_inside_range_list p'
c'
sp);
try done;
inv PU;
apply (
PI p n MP IN).
Case "
BufferedAlloc".
destruct k';
try done.
destruct (
valid_alloc_range_dec (
p',
n')); [|
done].
destruct range_in_dec; [
done|].
inv PU.
simpl in IN.
destruct IN as [
E |
IN].
inv E.
by destruct p;
simpl in *;
rewrite MP in ISU.
apply (
PI p n MP IN).
Case "
BufferedFree".
destruct k';
try done.
destruct (
pointer_in_range_list p'
sp);
try done.
inv PU.
apply in_range_remove in IN.
apply (
PI p n MP IN).
Qed.
Lemma update_part_buffer_scratch_preserves_partition_injectivity:
forall b sp sp'
tp,
(
forall bi,
In bi b ->
is_item_scratch_update bi) ->
part_update_buffer b sp =
Some sp' ->
partition_injective tp sp ->
partition_injective tp sp'.
Proof.
Lemma allocs_related_item_preserves_partition_injectivity:
forall bi b p n sp sp'
tp,
allocs_related p n b ->
In bi b ->
part_update bi sp =
Some sp' ->
partition_injective ((
p,
n) ::
tp)
sp ->
partition_injective ((
p,
n) ::
tp)
sp'.
Proof.
Lemma allocs_related_preserves_partition_injectivity:
forall b p n sp sp'
tp,
allocs_related p n b ->
part_update_buffer b sp =
Some sp' ->
partition_injective ((
p,
n) ::
tp)
sp ->
partition_injective ((
p,
n) ::
tp)
sp'.
Proof.
induction b as [|
bi b IH];
intros p n sp sp'
tp AR PUB PI.
unfold part_update_buffer in PUB.
simpl in PUB.
inv PUB;
done.
unfold part_update_buffer in *;
simpl in PUB.
destruct (
part_update bi sp)
as [
spi|]
_eqn :
PU; [
simpl in PUB|
done].
eapply IH.
intros bi'
IN'.
apply (
AR bi' (
in_cons _ _ _ IN')).
eassumption.
eapply allocs_related_item_preserves_partition_injectivity;
try edone.
apply in_eq.
Qed.
Lemma frees_related_item_preserves_partition_injectivity:
forall bi b p n sp sp'
tp,
frees_related p n b ->
In bi b ->
part_update bi sp =
Some sp' ->
partition_injective tp sp ->
partition_injective tp sp'.
Proof.
Lemma frees_related_preserves_partition_injectivity:
forall b p n sp sp'
tp,
frees_related p n b ->
part_update_buffer b sp =
Some sp' ->
partition_injective tp sp ->
partition_injective tp sp'.
Proof.
induction b as [|
bi b IH];
intros p n sp sp'
tp FR PUB PI.
unfold part_update_buffer in PUB.
simpl in PUB.
inv PUB;
done.
unfold part_update_buffer in *;
simpl in PUB.
destruct (
part_update bi sp)
as [
spi|]
_eqn :
PU; [
simpl in PUB|
done].
eapply IH.
intros bi'
IN'.
apply (
FR bi' (
in_cons _ _ _ IN')).
eassumption.
eapply frees_related_item_preserves_partition_injectivity;
try edone.
apply in_eq.
Qed.
Lemma remove_disj_preserves_partition_injectivity:
forall tp sp p n,
(
forall r,
In r sp ->
ranges_disjoint r (
p,
n)) ->
(
forall r,
In r sp ->
range_non_empty r) ->
partition_injective ((
p,
n) ::
tp)
sp ->
partition_injective tp sp.
Proof.
Lemma mem_consistent_with_part_valid_alloc:
forall m p r t,
mem_related_with_partitioning m p ->
In r (
p t) ->
valid_alloc_range r.
Proof.
Lemma non_stack_mem_related_sym:
forall m m',
non_stack_mem_related m m' ->
non_stack_mem_related m'
m.
Proof.
intros m m'
NSR r k.
specialize (
NSR r k).
destruct k;
try done;
by apply iff_sym.
Qed.
Definition stack_or_write_item (
bi :
buffer_item) :
Prop :=
match bi with
|
BufferedAlloc _ _ MObjStack =>
True
|
BufferedFree _ MObjStack =>
True
|
BufferedWrite _ _ _ =>
True
|
_ =>
False
end.
Lemma non_stack_mem_rel_preserved_by_stack_or_write:
forall tm sm bi sm',
non_stack_mem_related tm sm ->
apply_buffer_item bi sm =
Some sm' ->
stack_or_write_item bi ->
non_stack_mem_related tm sm'.
Proof.
Lemma non_stack_mem_rel_preserved_by_stack_or_write_buffer:
forall b tm sm sm',
non_stack_mem_related tm sm ->
apply_buffer b sm =
Some sm' ->
(
forall bi,
In bi b ->
stack_or_write_item bi) ->
non_stack_mem_related tm sm'.
Proof.
Lemma non_stack_mem_rel_preserved_by_stack_or_write_tgt:
forall tm sm bi tm',
non_stack_mem_related tm sm ->
apply_buffer_item bi tm =
Some tm' ->
stack_or_write_item bi ->
non_stack_mem_related tm'
sm.
Proof.
Lemma allocs_related_impl_stack_or_write:
forall n p b,
allocs_related p n b ->
forall bi,
In bi b ->
stack_or_write_item bi.
Proof.
by intros n p b AR bi IN; destruct (AR bi IN);
destruct bi as [? ? ? | ? ? [] | ? []].
Qed.
Lemma frees_related_impl_stack_or_write:
forall n p b,
frees_related p n b ->
forall bi,
In bi b ->
stack_or_write_item bi.
Proof.
by intros n p b FR bi IN; destruct (FR bi IN);
destruct bi as [? ? ? | ? ? [] | ? []].
Qed.
Lemma scratch_impl_stack_or_write:
forall bi,
is_item_scratch_update bi ->
stack_or_write_item bi.
Proof.
by intros [? ? ? | ? ? [] | ? []]. Qed.
Lemma chunk_inside_range_list_spec:
forall p c l,
chunk_inside_range_list p c l =
true ->
exists r,
In r l /\
range_inside (
range_of_chunk p c)
r.
Proof.
intros p c l CIL.
induction l as [|
h l IH];
simpl in CIL.
done.
destruct (
range_inside_dec (
range_of_chunk p c)
h)
as [
RI |
NRI].
exists h.
split.
apply in_eq.
done.
destruct (
IH CIL)
as [
r [
IN RI]].
exists r.
split.
apply in_cons.
done.
done.
Qed.
Lemma unbuffering_other_item_agrees_on_scratch:
forall bi m m'
part part'
t t',
t' <>
t ->
mem_related_with_partitioning m part ->
apply_buffer_item bi m =
Some m' ->
part_update bi (
part t) =
Some part' ->
mem_agrees_on_scratch m m' (
part t').
Proof.
Lemma unbuffering_other_buffer_agrees_on_scratch:
forall b part t'
t m part'
m',
t' <>
t ->
mem_related_with_partitioning m part ->
apply_buffer b m =
Some m' ->
part_update_buffer b (
part t) =
Some part' ->
mem_agrees_on_scratch m m' (
part t').
Proof.
Lemma range_lists_disjoint_tail1:
forall h t l,
range_lists_disjoint (
h ::
t)
l ->
range_lists_disjoint t l.
Proof.
intros h t l RLD r IN r'
IN'.
eapply RLD;
try done.
by apply in_cons.
Qed.
Lemma range_lists_disjoint_tail2:
forall h t l,
range_lists_disjoint l (
h ::
t) ->
range_lists_disjoint l t.
Proof.
intros h t l RLD r IN r'
IN'.
eapply RLD;
try done.
by apply in_cons.
Qed.
Lemma buffer_scratch_ranges_are_scratch:
forall p n b,
In (
p,
n) (
buffer_scratch_ranges b) ->
scratch_ptr p.
Proof.
intros p n b IN.
induction b as [|
bi br IH].
done.
simpl in IN.
destruct bi as [? ? ? |
p' ? [] | ? []];
try (
by apply IH).
destruct (
low_mem_restr (
Ptr.block p'))
as []
_eqn :
LMR.
by apply IH.
simpl in IN.
destruct IN as [
E |
IN].
inv E.
by destruct p.
by apply IH.
Qed.
Lemma unbuffer_preserves_scratch_allocs_fresh:
forall bi sp spt'
bs t br,
part_update bi (
sp t) =
Some spt' ->
bs t =
bi ::
br ->
scratch_allocs_fresh bs sp ->
scratch_allocs_fresh
(
tupdate t br bs)
(
update_partitioning t spt'
sp).
Proof.
intros bi sp spt'
bs t br PU BS (
BDISJ &
BSDISJ &
BDISJP).
split.
intro t'.
specialize (
BDISJ t').
unfold tupdate.
destruct (
peq t'
t)
as [-> |
_]; [|
done].
rewrite BS in BDISJ.
simpl in BDISJ.
destruct bi as [
p c v |
p n [] |
p []];
try done.
destruct (
low_mem_restr (
Ptr.block p));
try done.
by destruct BDISJ.
split.
intros t'
t''
NE.
specialize (
BSDISJ t'
t''
NE).
unfold tupdate.
destruct (
peq t''
t)
as [-> |
N1];
destruct (
peq t'
t)
as [-> |
N2];
try done;
rewrite BS in BSDISJ;
simpl in BSDISJ;
destruct bi as [
p c v |
p n [] |
p []];
try done;
destruct (
low_mem_restr (
Ptr.block p));
try done.
eby eapply range_lists_disjoint_tail1.
eby eapply range_lists_disjoint_tail2.
intros t'
t''.
specialize (
BDISJP t'
t'').
specialize (
BDISJ t').
specialize (
BSDISJ t''
t').
unfold tupdate,
update_partitioning.
destruct (
peq t''
t)
as [-> |
N1];
destruct (
peq t'
t)
as [-> |
N2];
try done;
try rewrite BS in *;
simpl in BDISJP.
destruct bi as [
p c v |
p n [] |
p []];
try done;
simpl in PU;
simpl in BDISJ;
try destruct (
low_mem_restr (
Ptr.block p))
as []
_eqn :
LMR;
clarify;
try destruct (
chunk_inside_range_list p c (
sp t));
clarify;
try destruct valid_alloc_range_dec;
clarify;
try destruct range_in_dec as [
RIx |
RNIx];
clarify;
try (
destruct pointer_in_range_list; [|
done];
inv PU;
intros r IN r'
IN';
destruct r';
apply in_range_remove in IN';
eby eapply BDISJP).
intros r IN r'
IN'.
simpl in IN'.
destruct IN'
as [<- |
IN'].
destruct r as [
pr nr].
apply buffer_scratch_ranges_are_scratch in IN.
destruct p;
destruct pr;
left;
intro E;
rewrite E in *;
simpl in *;
by rewrite LMR in IN.
by eapply BDISJP.
simpl in *.
destruct BDISJ as [
BDISJ NIN].
intros r IN r'
IN'.
simpl in IN'.
destruct IN'
as [<- |
IN'].
by apply NIN,
ranges_disjoint_comm in IN.
eapply BDISJP;
try edone;
by apply in_cons.
destruct bi as [
p c v |
p n [] |
p []];
try done.
destruct low_mem_restr;
try done.
eby eapply range_lists_disjoint_tail1.
destruct bi as [
p c v |
p n [] |
p []];
try done;
simpl in PU;
simpl in BDISJ;
simpl in BSDISJ;
try destruct (
low_mem_restr (
Ptr.block p))
as []
_eqn :
LMR;
clarify;
try destruct (
chunk_inside_range_list p c (
sp t));
clarify;
try destruct valid_alloc_range_dec;
clarify;
try destruct range_in_dec as [
RIx |
RNIx];
clarify;
try (
destruct pointer_in_range_list; [|
done];
inv PU;
intros r IN r'
IN';
destruct r';
apply in_range_remove in IN';
eby eapply BDISJP).
intros r IN r'
IN'.
simpl in IN'.
destruct IN'
as [<- |
IN'].
destruct r as [
pr nr].
apply buffer_scratch_ranges_are_scratch in IN.
destruct p;
destruct pr;
left;
intro E;
rewrite E in *;
simpl in *;
by rewrite LMR in IN.
by eapply BDISJP.
simpl in *.
specialize (
BSDISJ N1).
intros r IN r'
IN'.
simpl in IN'.
destruct IN'
as [<- |
IN'].
eapply ranges_disjoint_comm,
BSDISJ.
apply in_eq.
done.
eapply BDISJP;
try edone;
by apply in_cons.
Qed.
Lemma scratch_allocs_fresh_ext:
forall b b'
sp sp',
scratch_allocs_fresh b sp ->
(
forall t,
sp t =
sp'
t) ->
(
forall t,
b t =
b'
t) ->
scratch_allocs_fresh b'
sp'.
Proof.
intros b b' sp sp' (BDISJ & BSDISJ & BDISJP) SPE BE.
split. intro t; rewrite <- BE; apply BDISJ.
split. intros t' t; rewrite <- ! BE; apply BSDISJ.
intros t' t. rewrite <- BE, <- SPE; apply BDISJP.
Qed.
Lemma scratch_allocs_fresh_apply_buffer:
forall b sp spt'
bs bs'
t,
part_update_buffer b (
sp t) =
Some spt' ->
bs t =
b ++ (
bs'
t) ->
(
forall t',
t' <>
t ->
bs t' =
bs'
t') ->
scratch_allocs_fresh bs sp ->
scratch_allocs_fresh bs' (
update_partitioning t spt'
sp).
Proof.
Lemma load_result_machine:
forall v c,
machine_val v ->
machine_val (
Val.load_result c v).
Proof.
by intros [] []. Qed.
Lemma apply_machine_item_preserves_machine_memory:
forall bi m m'
(
MBI:
machine_buffer_item bi)
(
ABI:
apply_buffer_item bi m =
Some m')
(
MCM:
mem_content_machine m),
mem_content_machine m'.
Proof.
Lemma apply_machine_buffer_preserves_machine_memory:
forall b m m'
(
MBI:
machine_buffer b)
(
AB:
apply_buffer b m =
Some m')
(
MCM:
mem_content_machine m),
mem_content_machine m'.
Proof.
Lemma unbuffer_alloc_preserves_tso_pc_witt:
forall p n smp smpt'
ttso tthr sbis tm'
t stso sm'
tbr sthr sbr bp tmp,
apply_buffer_item (
BufferedAlloc p n MObjStack)
ttso.(
tso_mem) =
Some tm' ->
allocs_related p n sbis ->
part_update_buffer sbis (
smp t) =
Some smpt' ->
apply_buffer sbis stso.(
tso_mem) =
Some sm' ->
ttso.(
tso_buffers)
t =
BufferedAlloc p n MObjStack ::
tbr ->
bp t =
sbis ::
sbr ->
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tmp smp ->
exists bp',
exists tmp',
exists smp',
exists stso',
apply_buffer_reachable t stso sbis stso' /\
stso'.(
tso_mem) =
sm' /\
stso'.(
tso_buffers)
t =
flatten sbr /\
tso_pc_related_witt (
mktsostate (
tupdate t tbr ttso.(
tso_buffers))
tm',
tthr)
(
stso',
sthr)
bp'
tmp'
smp'.
Proof.
Lemma unbuffer_free_preserves_tso_pc_witt:
forall p n smp smpt'
ttso tthr sbis tm'
t stso sm'
tbr sthr sbr bp tmp tr,
apply_buffer_item (
BufferedFree p MObjStack)
ttso.(
tso_mem) =
Some tm' ->
frees_related p n sbis ->
(
forall r,
In r smpt' ->
ranges_disjoint r (
p,
n)) ->
part_update_buffer sbis (
smp t) =
Some smpt' ->
apply_buffer sbis stso.(
tso_mem) =
Some sm' ->
ttso.(
tso_buffers)
t =
BufferedFree p MObjStack ::
tbr ->
tmp t = (
p,
n) ::
tr ->
bp t =
sbis ::
sbr ->
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tmp smp ->
exists bp',
exists tmp',
exists smp',
exists stso',
apply_buffer_reachable t stso sbis stso' /\
stso'.(
tso_mem) =
sm' /\
stso'.(
tso_buffers)
t =
flatten sbr /\
tso_pc_related_witt (
mktsostate (
tupdate t tbr ttso.(
tso_buffers))
tm',
tthr)
(
stso',
sthr)
bp'
tmp'
smp'.
Proof.
Lemma sim_non_stack_alloc_preserves_load_rel:
forall tm sm tm'
sm'
p n k,
load_values_related tm sm ->
alloc_ptr (
p,
n)
k tm =
Some tm' ->
alloc_ptr (
p,
n)
k sm =
Some sm' ->
match k with MObjStack =>
False |
_ =>
True end ->
load_values_related tm'
sm'.
Proof.
Lemma sim_non_stack_free_preserves_load_rel:
forall tm sm tm'
sm'
p k,
mrestr tm =
low_mem_restr ->
non_stack_mem_related tm sm ->
load_values_related tm sm ->
free_ptr p k tm =
Some tm' ->
free_ptr p k sm =
Some sm' ->
match k with MObjStack =>
False |
_ =>
True end ->
load_values_related tm'
sm'.
Proof.
Lemma sim_write_preserves_load_rel:
forall tm sm tm'
sm'
c p v,
mrestr tm =
low_mem_restr ->
load_values_related tm sm ->
store_ptr c tm p v =
Some tm' ->
store_ptr c sm p v =
Some sm' ->
machine_val v ->
load_values_related tm'
sm'.
Proof.
Lemma sim_irrelevant_preserves_load_rel:
forall tm sm tm'
sm'
bi,
mrestr tm =
low_mem_restr ->
non_stack_mem_related tm sm ->
load_values_related tm sm ->
buffer_item_irrelevant bi ->
apply_buffer_item bi tm =
Some tm' ->
apply_buffer_item bi sm =
Some sm' ->
load_values_related tm'
sm'.
Proof.
Lemma sim_alloc_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
p n k,
non_stack_mem_related tm sm ->
alloc_ptr (
p,
n)
k tm =
Some tm' ->
alloc_ptr (
p,
n)
k sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma sim_free_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
p k,
non_stack_mem_related tm sm ->
free_ptr p k tm =
Some tm' ->
free_ptr p k sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma sim_irrelevant_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
bi,
non_stack_mem_related tm sm ->
buffer_item_irrelevant bi ->
apply_buffer_item bi tm =
Some tm' ->
apply_buffer_item bi sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma unbuffer_other_preserves_tso_pc_witt:
forall smp smpt'
ttso tthr bi sbis tm'
t stso sm'
tbr sthr sbr bp tmp,
apply_buffer_item bi ttso.(
tso_mem) =
Some tm' ->
buffer_item_irrelevant bi ->
(
forall bi',
In bi'
sbis ->
is_item_scratch_update bi') ->
part_update_buffer sbis (
smp t) =
Some smpt' ->
apply_buffer (
bi ::
sbis)
stso.(
tso_mem) =
Some sm' ->
ttso.(
tso_buffers)
t =
bi ::
tbr ->
bp t = (
bi ::
sbis) ::
sbr ->
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tmp smp ->
exists bp',
exists tmp',
exists smp',
exists stso',
apply_buffer_reachable t stso (
bi ::
sbis)
stso' /\
stso'.(
tso_mem) =
sm' /\
stso'.(
tso_buffers)
t =
flatten sbr /\
tso_pc_related_witt (
mktsostate (
tupdate t tbr ttso.(
tso_buffers))
tm',
tthr)
(
stso',
sthr)
bp'
tmp'
smp'.
Proof.
intros smp smpt'
ttso tthr bi sbis tm'
t stso sm'
tbr sthr sbr bp tmp.
intros TABI BIIR SCR PUB SAB TBUFF BP TSOREL.
pose proof TABI as TAP.
unfold apply_buffer_item in TAP.
destruct TSOREL as (
MTB &
NSMR & (
MCRt &
MCRs &
LR &
MCM) &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL).
pose proof (
BPD t)
as BPFL.
rewrite BP in BPFL.
simpl in BPFL.
rewrite app_comm_cons in BPFL.
destruct (
TSO.unbuffer_to_tso_state _ _ _ _ _ BPFL SAB)
as [
stso' (
TAU &
BUFtstso &
BUFother &
MEMstso)].
pose proof SAB as SABsbis;
simpl in SABsbis.
destruct (
apply_buffer_item bi (
tso_mem stso))
as [
smx|]
_eqn :
SABI;
try done;
simpl in SABsbis.
pose proof (
buffer_item_irrelevant_part_update _ (
smp t)
BIIR)
as PU.
assert (
PUBwithbi:
part_update_buffer (
bi ::
sbis) (
smp t) =
Some smpt').
unfold part_update_buffer;
simpl.
rewrite PU.
apply PUB.
exists (
fun t' =>
if peq t'
t then sbr else bp t').
exists tmp.
exists (
update_partitioning t smpt'
smp).
exists stso'.
split.
apply TAU.
split.
apply MEMstso.
split.
done.
split;
simpl;
subst.
intros t'
bi'
IN.
apply (
MTB t'
bi').
simpl in IN|-*.
destruct (
peq t'
t)
as [-> |
N].
rewrite BUFtstso in IN.
rewrite BPFL.
apply in_or_app.
by right.
by rewrite <-
BUFother.
split.
simpl.
eapply non_stack_mem_rel_preserved_by_stack_or_write_buffer.
eby eapply sim_irrelevant_preserves_non_stack_mem_related.
edone.
intros bi'
IN'.
by apply scratch_impl_stack_or_write,
SCR.
split.
split.
eby erewrite mem_consistent_with_restr_apply_item.
split.
eby erewrite mem_consistent_with_restr_apply_buffer.
split.
eapply apply_scratch_buffer_preserves_load_rel.
apply SABsbis.
edone.
eby eapply sim_irrelevant_preserves_load_rel;
try edone.
eapply apply_machine_buffer_preserves_machine_memory; [|
apply SAB|
done].
intros bi'
IN'.
apply (
MTB t).
simpl.
rewrite BPD,
BP.
simpl in *.
destruct IN'.
by left.
by right;
rewrite in_app;
left.
split.
eby eapply TSO.apply_buffer_reachable_preserves_tso_consistency.
split.
intro t'.
destruct (
peq t'
t)
as [-> |
N].
done.
rewrite BUFother.
apply BPD.
done.
split.
intros t'
b IN.
apply (
BNE t').
destruct (
peq t'
t)
as [-> |
N].
rewrite BP.
by right.
done.
split.
eapply scratch_allocs_fresh_apply_buffer.
edone. 3 :
edone.
by rewrite BUFtstso,
BPD,
BP.
intros ? ?;
by rewrite BUFother.
split.
eapply mem_related_with_partitioning_ext.
eapply (
apply_buffer_item_preserves_mem_partitioning _ _ bi _ _ t).
apply MRPt.
apply TABI.
apply buffer_item_irrelevant_part_update.
done.
intros t'.
by unfold update_partitioning;
destruct (
peq t'
t)
as [-> |
N].
split.
eby eapply apply_buffer_preserves_mem_partitioning.
intro t'.
specialize (
TREL t').
destruct TREL as [
PI [
BREL BSREL]].
split.
unfold update_partitioning.
destruct (
peq t'
t)
as [-> |
N].
eby eapply update_part_buffer_scratch_preserves_partition_injectivity.
done.
simpl in BREL,
BSREL,
sthr,
tthr.
destruct (
peq t'
t)
as [-> |
N].
rewrite !
update_partitioning_s,
tupdate_s.
split.
rewrite TBUFF in BREL.
inv BREL;
try by simpl in BIIR.
by rewrite BP in *;
clarify;
rewrite PUB,
TBUFF in *;
clarify.
destruct (
sthr !
t)
as [
sst|];
destruct (
tthr !
t)
as [
tst|];
simpl in BSREL;
try done.
simpl.
rewrite TBUFF in BSREL.
rewrite BP in BSREL.
apply <-
buffered_states_related_prepend_tgt.
apply <-
buffered_states_related_prepend_src;
try edone.
by rewrite buffer_item_irrelevant_part_update.
destruct BSREL as (
_ &
_ &
E &
_).
by rewrite E in TBUFF.
rewrite !
update_partitioning_o,
tupdate_o;
try done.
split.
done.
destruct (
sthr !
t')
as [
sst|];
destruct (
tthr !
t')
as [
tst|];
simpl in BSREL;
try done.
simpl.
pose proof MRPs as X;
destruct X as [
PD [
RLD RLA]].
destruct (
apply_buffer_preserves_mem_partitioning _ _ _ _ _ _
MRPs SAB PUBwithbi)
as [
PR' [
RLD'
RLA']].
apply buffered_states_related_load_inv with (
smem :=
tso_mem stso);
try done.
intros r IN.
apply (
RLA r).
eby eexists.
intros r IN.
apply (
RLA'
r).
exists t'.
rewrite update_partitioning_o.
done.
done.
eapply tso_consistent_safe_buffer_app;
try edone.
rewrite <-
app_nil_end.
apply BPD.
eapply tso_consistent_safe_buffer_app;
try edone.
eby eapply TSO.apply_buffer_reachable_preserves_tso_consistency.
rewrite <-
app_nil_end.
rewrite BUFother.
apply BPD.
done.
eby eapply unbuffering_other_buffer_agrees_on_scratch.
Qed.
Lemma unbuffer_item_preserves_tso_pc_witt:
forall smp ttso tthr bi sbis tm'
t stso sm'
tbr sthr sbr bp tmp,
apply_buffer_item bi ttso.(
tso_mem) =
Some tm' ->
apply_buffer sbis stso.(
tso_mem) =
Some sm' ->
ttso.(
tso_buffers)
t =
bi ::
tbr ->
bp t =
sbis ::
sbr ->
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tmp smp ->
exists bp',
exists tmp',
exists smp',
exists stso',
apply_buffer_reachable t stso sbis stso' /\
stso'.(
tso_mem) =
sm' /\
stso'.(
tso_buffers)
t =
flatten sbr /\
tso_pc_related_witt (
mktsostate (
tupdate t tbr ttso.(
tso_buffers))
tm',
tthr)
(
stso',
sthr)
bp'
tmp'
smp'.
Proof.
intros smp ttso tthr bi sbis tm'
t stso sm'
tbr sthr sbr bp tmp.
intros TABI SAB TBUFF BPT TREL.
pose proof TREL as TREL'.
destruct TREL'
as (
MTB &
NSMR &
MR &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TSREL).
destruct (
TSREL t)
as [
_ [
BREL BSREL]].
simpl in BREL.
remember (
tso_buffers ttso t)
as tbuft.
remember (
tmp t)
as tmpt.
remember (
bp t)
as bpt.
remember (
smp t)
as smpt.
buffers_related_cases (
destruct BREL)
Case.
Case "
buffers_related_empty".
done.
Case "
buffers_related_alloc".
inv TBUFF.
inv BPT.
apply sym_eq in Heqbpt.
eby eapply unbuffer_alloc_preserves_tso_pc_witt.
Case "
buffers_related_free".
inv TBUFF.
inv BPT.
apply sym_eq in Heqtmpt.
apply sym_eq in Heqbpt.
eby eapply unbuffer_free_preserves_tso_pc_witt.
Case "
buffers_related_other".
inv TBUFF.
inv BPT.
apply sym_eq in Heqbpt.
eby eapply unbuffer_other_preserves_tso_pc_witt.
Qed.
Lemma tso_pc_buff_length_eq_to_bp:
forall ttso tthr stso sthr bp tmp smp t,
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tmp smp ->
length(
ttso.(
tso_buffers)
t) =
length (
bp t).
Proof.
intros ttso tthr stso sthr bp tmp smp t
(_ & _ & _ & _ & _ & _ & _ & _ & _ & TREL).
destruct (TREL t) as (_ & BREL & _). simpl in BREL.
induction BREL; try done; simpl; f_equal; done.
Qed.
Lemma unbuffer_unbuffer_safe_app:
forall b1 b2 tso t,
unbuffer_safe tso ->
tso.(
tso_buffers)
t =
b1 ++
b2 ->
exists m',
apply_buffer b1 tso.(
tso_mem) =
Some m'.
Proof.
induction b1 as [|
bi b1 IH].
intros.
exists (
tso_mem tso).
done.
intros b2 tso t US DC.
rewrite <-
app_comm_cons in DC.
destruct (
unbuffer_unbuffer_safe US DC)
as [
mi [
ABI US']].
specialize (
IH b2 _ t US').
simpl in IH.
rewrite tupdate_s in IH.
destruct (
IH (
refl_equal _))
as [
m'
AB].
exists m'.
simpl.
rewrite ABI.
done.
Qed.
Lemma tgt_tso_consistent_unbuffer:
forall ts t bi b m'
tthr,
ts.(
tso_buffers)
t =
bi ::
b ->
apply_buffer_item bi ts.(
tso_mem) =
Some m' ->
Comp.consistent tso_mm cst_sem (
ts,
tthr) ->
Comp.consistent tso_mm cst_sem
(
mktsostate (
tupdate t b (
tso_buffers ts))
m',
tthr).
Proof.
intros ts t bi b m'
tthr BD ABI [
BC US].
split.
intros t'
N';
simpl in *.
specialize (
BC t'
N').
simpl in BC.
unfold tupdate;
destruct (
peq t'
t)
as [-> |
Nt];
by try rewrite BC in *.
simpl.
destruct ts;
simpl in *;
eby eapply apply_item_unbuffer_safe.
Qed.
Lemma tgt_tso_consistent_tso_step:
forall ts ts'
tthr,
tso_step ts MMtau ts' ->
Comp.consistent tso_mm cst_sem (
ts,
tthr) ->
Comp.consistent tso_mm _ (
ts',
tthr).
Proof.
Lemma unbuffer_item_preserves_tso_pc_unsafe:
forall ttso t bi tbr tm'
tthr stso sthr,
ttso.(
tso_buffers)
t =
bi ::
tbr ->
apply_buffer_item bi ttso.(
tso_mem) =
Some tm' ->
tso_pc_unsafe_related (
ttso,
tthr) (
stso,
sthr) ->
exists stso',
exists b,
b <>
nil /\
apply_buffer_reachable t stso b stso' /\
tso_pc_unsafe_related
(
mktsostate (
tupdate t tbr ttso.(
tso_buffers))
tm',
tthr)
(
stso',
sthr).
Proof.
intros ttso t bi tbr tm'
tthr stso sthr BD ABI TREL.
destruct TREL as [
bp [
tp [
sp TREL]]].
generalize TREL;
intros (
_ &
_ &
_ & (
_ &
US) &
BP &
BNE &
_).
specialize (
BP t).
destruct (
bp t)
as [|
sbis sbr]
_eqn :
BPT.
pose proof (
tso_pc_buff_length_eq_to_bp _ _ _ _ _ _ _ t TREL)
as LE.
by rewrite BPT,
BD in LE.
simpl in BP.
destruct (
unbuffer_unbuffer_safe_app _ _ _ _ US BP)
as [
sm'
SAB].
destruct (
unbuffer_item_preserves_tso_pc_witt _ _ _ _ _ _ _ _ _ _ _ _ _ _
ABI SAB BD BPT TREL)
as [
bp' [
tmp' [
smp' [
stso' [
UBR [
MEq [
Beq TREL']]]]]]].
exists stso'.
exists sbis.
split.
apply (
BNE t).
rewrite BPT.
by left.
split.
done.
eexists;
eexists;
eexists.
edone.
Qed.
Lemma unbuffer_item_preserves_tso_pc_unsafe_tso_step:
forall ttso ttso'
tthr stsothr
(
TSOUB:
tso_step ttso MMtau ttso')
(
TREL:
tso_pc_unsafe_related (
ttso,
tthr)
stsothr),
exists stsothr',
taustep cshm_lts stsothr Etau stsothr' /\
tso_pc_unsafe_related (
ttso',
tthr)
stsothr'.
Proof.
Lemma unbuffer_item_preserves_tso_pc:
forall ttso ttso'
tthr stsothr,
tso_step ttso MMtau ttso' ->
tso_pc_related (
ttso,
tthr)
stsothr ->
exists stsothr',
taustep cshm_lts stsothr Etau stsothr' /\
tso_pc_related (
ttso',
tthr)
stsothr'.
Proof.
Lemma tso_pc_rel_load_eq:
forall ttso tthr stso sthr tm sm t p c,
machine_ptr p ->
tso_pc_related (
ttso,
tthr) (
stso,
sthr) ->
apply_buffer (
ttso.(
tso_buffers)
t)
ttso.(
tso_mem) =
Some tm ->
apply_buffer (
stso.(
tso_buffers)
t)
stso.(
tso_mem) =
Some sm ->
match load_ptr c tm p with
|
Some v =>
load_ptr c sm p =
Some v /\
machine_val v \/
load_ptr c sm p =
None
|
None =>
load_ptr c sm p =
None
end.
Proof.
intros ttso tthr stso sthr tm sm t p c
MP [
TC [
bp [
tmp [
smp TREL]]]]
TAB SAB.
remember (
tso_buffers ttso t)
as tbuff.
revert ttso tthr stso sthr bp smp tmp TC TREL Heqtbuff TAB SAB.
induction tbuff as [|
tbi tbr IH];
intros;
simpl in *.
clarify.
destruct (
bp t)
as [|?]
_eqn :
Bs.
destruct TREL as (
_ &
_ & (
_ &
_ &
LR &
MCM) &
_ &
BE &
_).
rewrite BE,
Bs in SAB.
inv SAB.
simpl in LR,
MCM.
specialize (
LR p MP c).
specialize (
MCM p c).
by destruct (
load_ptr c ttso.(
tso_mem)
p);
destruct (
load_ptr c stso.(
tso_mem)
p);
try done;
vauto.
pose proof (
tso_pc_buff_length_eq_to_bp _ _ _ _ _ _ _ t TREL)
as LE.
by rewrite Bs, <-
Heqtbuff in LE.
generalize TREL;
intros (
_ &
_ &
_ &
_ &
BP &
_);
specialize (
BP t);
simpl in *.
destruct (
bp t)
as [|
sbis sbr]
_eqn :
BPT.
pose proof (
tso_pc_buff_length_eq_to_bp _ _ _ _ _ _ _ t TREL)
as LE.
by rewrite BPT, <-
Heqtbuff in LE.
rewrite BP in SAB.
destruct (
apply_buffer_item tbi (
tso_mem ttso))
as [
tmi|]
_eqn :
TABI;
try done;
simpl in *.
rewrite apply_buffer_app in SAB.
destruct (
apply_buffer sbis (
tso_mem stso))
as [
smi|]
_eqn :
SABi;
try done;
simpl in SAB.
destruct (
unbuffer_item_preserves_tso_pc_witt _ _ _ _ _ _ _ _ _ _ _ _ _ _
TABI SABi (
sym_eq Heqtbuff)
BPT TREL)
as [
bp' [
tmp' [
smp' [
stso' [
TAU [
MEq [
Beq TREL']]]]]]].
eapply IH.
-
eby eapply tgt_tso_consistent_unbuffer;
try edone;
apply sym_eq.
-
apply TREL'.
-
by simpl;
rewrite tupdate_s.
-
done.
by rewrite MEq,
Beq.
Qed.
End UNBUFFER_SIMS.