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 Cstackedproofunbuffer.
Require Import Permutation.
Section ALLOC_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)).
Hypothesis function_stacksize_limit:
forall p f cenv,
Genv.find_funct (
Cstacked.ge cst_globenv)
p =
Some (
Internal f) ->
snd (
build_compilenv cenv f) <=
Int.max_unsigned.
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 buffered_ostates_related := (
buffered_ostates_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).
Inductive unbuffer_reachable :
tso_state ->
tso_state ->
Prop :=
|
unbuffer_reachable_refl:
forall tso,
unbuffer_reachable tso tso
|
unbuffer_reachable_step:
forall tso t bi b m'
tso'
tso'',
tso.(
tso_buffers)
t =
bi ::
b ->
apply_buffer_item bi tso.(
tso_mem) =
Some m' ->
tso' =
mktsostate (
tupdate t b tso.(
tso_buffers))
m' ->
unbuffer_reachable tso'
tso'' ->
unbuffer_reachable tso tso''.
Lemma unbuffer_safe_reachable_safe:
forall tso,
unbuffer_safe tso ->
(
forall tso'
t bi b,
unbuffer_reachable tso tso' ->
tso'.(
tso_buffers)
t =
bi ::
b ->
apply_buffer_item bi tso'.(
tso_mem) <>
None).
Proof.
intros tso US.
induction US as [tso ABI US IH].
intros tso' t bi b R BD.
destruct R as [tso' | tso' t' bi' b' m' tso'' tso''' BD' ABI' Etso''].
by destruct (ABI t bi b BD) as [m' ->].
eapply IH; try edone. by rewrite <- Etso''.
Qed.
Inductive buffers_ss_rel:
list buffer_item ->
list arange ->
list (
list buffer_item) ->
list arange ->
Prop :=
|
buffers_ss_rel_coarse:
forall tb tp sb sp
(
BSR :
buffers_related tb tp sb sp),
buffers_ss_rel tb tp sb sp
|
buffers_ss_rel_scratch:
forall tb tp sb sbr sp sp'
(
SCR:
forall bi,
In bi sb ->
is_item_scratch_update bi)
(
PUB:
part_update_buffer sb sp =
Some sp')
(
BSR:
buffers_related tb tp sbr sp'),
buffers_ss_rel tb tp (
sb ::
sbr)
sp
|
buffers_ss_rel_alloc:
forall p n tb tp sb sbr sp sp'
(
AR:
allocs_related p n sb)
(
PUB:
part_update_buffer sb sp =
Some sp')
(
BSR:
buffers_related tb ((
p,
n) ::
tp)
sbr sp'),
buffers_ss_rel tb ((
p,
n) ::
tp) (
sb ::
sbr)
sp.
Tactic Notation "
buffers_ss_rel_cases"
tactic(
first)
tactic(
c) :=
first; [
c "
buffers_ss_rel_coarse" |
c "
buffers_ss_rel_scratch" |
c "
buffers_ss_rel_alloc"].
Inductive tso_pc_ss_rel_witt (
ts :
tso_state)
(
ss :
tso_state)
(
bp :
thread_id ->
list (
list buffer_item))
(
tp :
partitioning)
(
sp :
partitioning) :
Prop :=
|
tso_pc_ss_rel_witt_intro:
forall
(
MB:
machine_thread_buffers ss.(
tso_buffers))
(
NSMR:
non_stack_mem_related ts.(
tso_mem)
ss.(
tso_mem))
(
MCWRt:
mrestr ts.(
tso_mem) =
low_mem_restr)
(
MCWRs:
mrestr ss.(
tso_mem) =
no_mem_restr)
(
TFS:
tso_fin_sup ts)
(
SFS:
tso_fin_sup ss)
(
TUS:
unbuffer_safe ts)
(
BPART:
forall t,
ss.(
tso_buffers)
t =
flatten (
bp t))
(
SAF:
scratch_allocs_fresh ss.(
tso_buffers)
sp)
(
MRWPt:
mem_related_with_partitioning ts.(
tso_mem)
tp)
(
MRWPs:
mem_related_with_partitioning ss.(
tso_mem)
sp)
(
TREL:
forall t,
partition_injective (
tp t) (
sp t) /\
buffers_ss_rel (
ts.(
tso_buffers)
t) (
tp t)
(
bp t) (
sp t)),
tso_pc_ss_rel_witt ts ss bp tp sp.
Definition tso_pc_ss_rel (
ts :
tso_state)
(
ss :
tso_state) :
Prop :=
exists bp,
exists tp,
exists sp,
tso_pc_ss_rel_witt ts ss bp tp sp.
Lemma buffered_states_related_length_eq:
forall tb tp sb sp,
buffers_related tb tp sb sp ->
length tb =
length sb.
Proof.
intros tb tp sb sp BREL.
induction BREL; try done; by simpl; rewrite IHBREL.
Qed.
Lemma ss_rel_preservation_free_nil:
forall ttso stso bp tb tp tpr bsr smp p n t tm',
tso_pc_ss_rel_witt ttso stso bp tp smp ->
tso_buffers ttso t =
BufferedFree p MObjStack ::
tb ->
bp t =
nil ::
bsr ->
tp t = (
p,
n) ::
tpr ->
length tb =
length bsr ->
apply_buffer_item (
BufferedFree p MObjStack) (
tso_mem ttso) =
Some tm' ->
tso_pc_ss_rel_witt
(
mktsostate
(
tupdate t tb (
tso_buffers ttso))
tm')
stso
(
fun t' =>
if peq t'
t then bsr else bp t')
(
update_partitioning t tpr tp)
smp.
Proof.
Lemma ss_rel_preservation_free_cons:
forall ttso stso bp bi bis tb tp bsr sp spt'
p t sm',
tso_pc_ss_rel_witt ttso stso bp tp sp ->
tso_buffers ttso t =
BufferedFree p MObjStack ::
tb ->
bp t = (
bi ::
bis) ::
bsr ->
length tb =
length bsr ->
apply_buffer_item bi (
tso_mem stso) =
Some sm' ->
part_update bi (
sp t) =
Some spt' ->
tso_pc_ss_rel_witt
ttso
(
mktsostate
(
tupdate t (
bis ++
flatten bsr) (
tso_buffers stso))
sm')
(
fun t' =>
if peq t'
t then (
bis ::
bsr)
else bp t')
tp (
update_partitioning t spt'
sp).
Proof.
Lemma ss_rel_preservation_alloc_tgt:
forall ttso stso bp tb tp smp p n t tm',
tso_pc_ss_rel_witt ttso stso bp tp smp ->
tso_buffers ttso t =
BufferedAlloc p n MObjStack ::
tb ->
length(
bp t) =
S(
length tb) ->
apply_buffer_item (
BufferedAlloc p n MObjStack) (
tso_mem ttso) =
Some tm' ->
tso_pc_ss_rel_witt
(
mktsostate (
tupdate t tb (
tso_buffers ttso))
tm')
stso
bp
(
update_partitioning t ((
p,
n) ::
tp t)
tp)
smp.
Proof.
Lemma ss_rel_preservation_src_nil:
forall ttso stso bsr bp tp smp t,
tso_pc_ss_rel_witt ttso stso bp tp smp ->
bp t =
nil ::
bsr ->
length bsr =
length (
tso_buffers ttso t) ->
tso_pc_ss_rel_witt
ttso
stso
(
fun t' =>
if peq t'
t then bsr else bp t')
tp smp.
Proof.
intros until 0;
intros []
BP BPL.
split;
try done.
-
intro t'.
destruct (
peq t'
t)
as [-> |
N]; [
by rewrite BPART,
BP |
by rewrite BPART].
-
intro t'.
destruct (
TREL t')
as [
PI BREL].
split.
done.
simpl in BREL.
destruct (
peq t'
t)
as [-> |
N].
simpl.
inv BREL;
try (
apply buffered_states_related_length_eq in BSR;
rewrite BSR,
BP in *;
by apply n_Sn in BPL);
by econstructor;
rewrite BP in *;
clarify;
inv PUB.
done.
Qed.
Lemma ss_rel_preservation_alloc_src_cons:
forall ttso stso bi bis bsr m'
bp tp spt smp t,
tso_pc_ss_rel_witt ttso stso bp tp smp ->
bp t = (
bi ::
bis) ::
bsr ->
apply_buffer_item bi stso.(
tso_mem) =
Some m' ->
part_update bi (
smp t) =
Some spt ->
length bsr =
length (
tso_buffers ttso t) ->
tso_pc_ss_rel_witt
ttso
(
mktsostate
(
tupdate t (
bis ++
flatten bsr)
stso.(
tso_buffers))
m')
(
fun t' =>
if peq t'
t then bis ::
bsr else bp t')
tp
(
update_partitioning t spt smp).
Proof.
intros until 0;
intros []
BP ABIs PU LB.
destruct (
TREL t)
as (
_ &
BTREL).
simpl in BTREL.
split;
simpl;
try done.
-
intros t'.
pose proof (
MB t')
as MBt.
unfold tupdate;
destruct (
peq t'
t)
as [-> |
N].
rewrite (
BPART t),
BP in MBt.
simpl in MBt.
intros bi'
IN'.
by apply MBt,
in_cons.
done.
-
eapply non_stack_mem_rel_preserved_by_stack_or_write;
try edone.
destruct BTREL.
apply buffered_states_related_length_eq in BSR.
rewrite BSR,
BP in LB.
by apply n_Sn in LB.
apply scratch_impl_stack_or_write,
SCR.
inv BP.
apply in_eq.
apply (
allocs_related_impl_stack_or_write _ _ _ AR).
inv BP.
apply in_eq.
-
eby erewrite mem_consistent_with_restr_apply_item.
-
eby eapply tso_fin_sup_tupdate.
-
by intro t';
unfold tupdate;
destruct peq;
clarify.
-
eapply unbuffer_preserves_scratch_allocs_fresh;
try edone.
by rewrite BPART,
BP.
-
eby eapply apply_buffer_item_preserves_mem_partitioning.
-
intro t'.
destruct (
TREL t')
as [
PI BREL].
destruct (
peq t'
t)
as [-> |
N].
split.
destruct BTREL.
apply buffered_states_related_length_eq in BSR.
rewrite BSR,
BP in LB.
by apply n_Sn in LB.
eapply update_part_scratch_preserves_partition_injectivity.
apply SCR.
inv BP.
apply in_eq. 2 :
apply PI.
by rewrite update_partitioning_s.
rewrite update_partitioning_s.
eapply allocs_related_item_preserves_partition_injectivity;
try edone.
inv BP.
apply in_eq.
rewrite update_partitioning_s.
inv BTREL.
apply buffered_states_related_length_eq in BSR.
rewrite BSR,
BP in LB.
by apply n_Sn in LB.
rewrite BP in *;
clarify.
unfold part_update_buffer in PUB;
simpl in PUB;
rewrite PU in PUB;
simpl in PUB.
eapply buffers_ss_rel_scratch.
intros bi'
IN'.
apply SCR,
in_cons,
IN'.
edone.
edone.
rewrite BP in *;
clarify.
unfold part_update_buffer in PUB;
simpl in PUB;
rewrite PU in PUB;
simpl in PUB.
eapply buffers_ss_rel_alloc.
intros bi'
IN'.
apply AR,
in_cons,
IN'.
edone.
edone.
by rewrite update_partitioning_o;
try split.
Qed.
Lemma ss_rel_preservation_other:
forall ttso stso bi bis bsr sm'
tm'
bp tp tb sp t,
tso_pc_ss_rel_witt ttso stso bp tp sp ->
buffer_item_irrelevant bi ->
bp t = (
bi ::
bis) ::
bsr ->
tso_buffers ttso t =
bi ::
tb ->
apply_buffer_item bi stso.(
tso_mem) =
Some sm' ->
apply_buffer_item bi ttso.(
tso_mem) =
Some tm' ->
tso_pc_ss_rel_witt
(
mktsostate (
tupdate t tb (
tso_buffers ttso))
tm')
(
mktsostate (
tupdate t (
bis ++
flatten bsr)
stso.(
tso_buffers))
sm')
(
fun t' =>
if peq t'
t then bis ::
bsr else bp t')
tp sp.
Proof.
Lemma ss_rel_sim:
forall ttso t stso bi b m',
tso_pc_ss_rel ttso stso ->
stso.(
tso_buffers)
t =
bi ::
b ->
apply_buffer_item bi stso.(
tso_mem) =
Some m' ->
exists ttso',
unbuffer_reachable ttso ttso' /\
tso_pc_ss_rel ttso' (
mktsostate (
tupdate t b stso.(
tso_buffers))
m').
Proof.
intros ttso t stso bi b m' [
bp [
tp [
sp TWREL]]]
SB SABI.
remember (
bp t)
as bpt.
revert bp Heqbpt ttso tp TWREL.
induction bpt as [|
bph bpt IH];
intros bp E ttso tp TWREL;
generalize TWREL;
intros X;
destruct X;
destruct (
TREL t)
as [
PI BREL];
simpl in *;
apply sym_eq in E.
inv BREL; [
inv BSR | | ];
try (
by specialize (
BPART t);
rewrite SB,
E in BPART).
specialize (
IH (
fun t' =>
if peq t'
t then bpt else bp t')).
simpl in IH.
destruct (
peq t t);
try done.
specialize (
IH (
refl_equal _)).
inv BREL.
inv BSR.
by rewrite E in *.
rewrite E in *.
clarify.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphr].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ttso))
tm')
(
update_partitioning t ((
p,
n) ::
tp t)
tp)).
apply modusponens in IH.
destruct IH as [
ttso' [
UR REL]].
exists ttso'.
split.
econstructor.
eby apply sym_eq.
edone.
edone.
done.
edone.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
eapply ss_rel_preservation_alloc_tgt;
try edone.
by rewrite E,
BSR0.
done.
simpl.
by rewrite tupdate_s.
exists (
mktsostate (
tupdate t tb (
tso_buffers ttso))
tm').
split.
econstructor.
eby apply sym_eq.
edone.
edone.
constructor.
rewrite (
BPART t),
E in SB.
inv SB.
unfold part_update_buffer in PUB;
simpl in PUB.
destruct (
part_update bi (
sp t))
as [
spt|]
_eqn :
PU;
try done.
eexists;
eexists;
eexists.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_alloc_src_cons _ _ _ _ _ _ _ _ _ _ t);
try edone.
eapply ss_rel_preservation_alloc_tgt;
try edone.
done.
by rewrite BSR0,
E.
simpl.
by rewrite tupdate_s.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct sb as [|
sbi sbir].
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ttso))
tm')
(
update_partitioning t tp0 tp)).
apply modusponens in IH.
destruct IH as [
ttsox [
URx TRWx]].
exists ttsox.
split.
econstructor;
try edone.
eby apply sym_eq.
edone.
done.
rewrite E in *.
clarify.
eapply (
ss_rel_preservation_free_nil _ _ _ _ _ _ _ _ _ _ t);
try edone.
eby apply sym_eq.
eby apply sym_eq.
by apply buffered_states_related_length_eq in BSR0.
exists ttso.
split.
constructor.
exists (
fun t' :
thread_id =>
if peq t'
t then sbir ::
sbr else bp t').
exists tp.
unfold part_update_buffer in PUB.
simpl in PUB.
destruct (
part_update sbi (
sp t))
as [
spt'|]
_eqn :
PU;
try done.
exists (
update_partitioning t spt'
sp).
rewrite BPART in SB.
replace (
bp t)
with ((
sbi ::
sbir) ::
sbr)
in SB.
simpl in SB.
inv SB.
eapply ss_rel_preservation_free_cons;
try edone.
eby apply sym_eq.
eby apply sym_eq.
by apply buffered_states_related_length_eq in BSR0.
rewrite BPART in SB.
replace (
bp t)
with ((
bi0 ::
sb) ::
sbr)
in SB.
simpl in SB.
inv SB.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
exists (
mktsostate (
tupdate t tb (
tso_buffers ttso))
tm').
split.
econstructor.
apply sym_eq.
edone.
edone.
reflexivity.
constructor.
eexists;
eexists;
eexists.
eapply (
ss_rel_preservation_other _ _ _ _ _ _ _ _ _ _ _ t);
try edone.
rewrite E in *.
clarify.
destruct bph as [|
bphi bphr].
inv PUB.
specialize (
IH ttso tp).
apply modusponens in IH.
destruct IH as [
ttso' [
UR REL]].
exists ttso'.
by split.
apply buffered_states_related_length_eq in BSR.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t);
try done.
exists ttso.
split.
constructor.
rewrite (
BPART t),
E in SB.
inv SB.
unfold part_update_buffer in PUB;
simpl in PUB.
destruct (
part_update bi (
sp t))
as [
spt|]
_eqn :
PU;
try done.
eexists;
eexists;
eexists.
apply buffered_states_related_length_eq in BSR.
eapply (
ss_rel_preservation_alloc_src_cons _ _ _ _ _ _ _ _ _ _ t);
try edone.
rewrite E in *.
clarify.
destruct bph as [|
bphi bphr].
inv PUB.
specialize (
IH ttso tp).
apply modusponens in IH.
destruct IH as [
ttso' [
UR REL]].
exists ttso'.
by split.
apply buffered_states_related_length_eq in BSR.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t);
try done.
exists ttso.
split.
constructor.
rewrite (
BPART t),
E in SB.
inv SB.
unfold part_update_buffer in PUB;
simpl in PUB.
destruct (
part_update bi (
sp t))
as [
spt|]
_eqn :
PU;
try done.
eexists;
eexists;
eexists.
apply buffered_states_related_length_eq in BSR.
eapply (
ss_rel_preservation_alloc_src_cons _ _ _ _ _ _ _ _ _ _ t);
try edone.
Qed.
Definition disjoint_item (
r :
arange) (
bi :
buffer_item) :=
match bi with
|
BufferedAlloc p'
n'
_ =>
ranges_disjoint (
p',
n')
r
|
_ =>
True
end.
Fixpoint disjoint_allocs (
b :
list buffer_item) :=
match b with
|
BufferedAlloc p n _ ::
br =>
disjoint_allocs br /\
forall bi,
In bi br ->
disjoint_item (
p,
n)
bi
|
nil =>
True
|
_ =>
False
end.
Ltac mach_scr_elim :=
match goal with
H :
machine_ptr ?
p,
H' :
scratch_ptr ?
p |-
_ =>
by destruct (
machine_not_scratch _ H H')
end.
Definition non_stack_kind (
k :
mobject_kind) :=
match k with
|
MObjStack =>
False
|
_ =>
True
end.
Definition non_stack_item (
bi :
buffer_item) :=
match bi with
|
BufferedAlloc pi ni ki =>
non_stack_kind ki
|
BufferedFree pi ki =>
non_stack_kind ki
|
_ =>
False
end.
Lemma irrelevant_src_buff_impl_tgt_success:
forall ts ss t bi sbr,
tso_pc_ss_rel ts ss ->
ss.(
tso_buffers)
t =
bi ::
sbr ->
non_stack_item bi ->
exists ts',
exists tbr,
tso_pc_ss_rel ts'
ss /\
ts'.(
tso_buffers)
t =
bi ::
tbr.
Proof.
intros ts ss t bi sbr TREL SB NS.
destruct TREL as [
bp [
tp [
sp TWREL]]].
remember (
bp t)
as bpt.
revert bp Heqbpt ts tp TWREL.
induction bpt as [|
bph bpt IH];
intros bp E ts tp TWREL;
apply sym_eq in E;
generalize TWREL;
destruct 1.
specialize (
BPART t).
rewrite E,
SB in BPART.
done.
specialize (
IH (
fun t' =>
if peq t'
t then bpt else bp t')).
simpl in IH.
destruct (
peq t t);
try done.
specialize (
IH (
refl_equal _)).
destruct (
TREL t)
as [
PIt BRELt].
inv BRELt.
inv BSR;
rewrite E in *;
clarify.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t ((
p,
n) ::
tp t)
tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
eapply ss_rel_preservation_alloc_tgt;
try edone.
by rewrite E,
BSR0.
done.
simpl.
by rewrite tupdate_s.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
AR _ (
in_eq _ _)).
unfold is_item_scratch_update in AR.
destruct AR;
destruct bphi as [ | ? ? [] | ? []];
try done;
destruct NS;
by mach_scr_elim.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t tp0 tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_free_nil _ _ _ _ _ _ _ _ _ _ t);
try edone;
eby apply sym_eq.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
FR _ (
in_eq _ _)).
unfold is_item_scratch_update in FR.
destruct FR;
destruct bphi as [ | ? ? [] | ? []];
try done;
destruct NS;
by mach_scr_elim.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
exists ts.
eexists.
split.
eexists;
eexists;
eexists;
edone.
eby apply sym_eq.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
SCR _ (
in_eq _ _)).
unfold is_item_scratch_update in SCR.
destruct bphi as [ | ? ? [] | ? []];
try done;
destruct NS;
by mach_scr_elim.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
AR _ (
in_eq _ _)).
unfold is_item_scratch_update in AR.
destruct AR;
destruct bphi as [ | ? ? [] | ? []];
try done;
destruct NS;
by mach_scr_elim.
Qed.
Lemma alloc_stack_src_buff_impl_tgt_partition:
forall ts ss t p n sbr,
tso_pc_ss_rel ts ss ->
ss.(
tso_buffers)
t =
BufferedAlloc p n MObjStack ::
sbr ->
machine_ptr p ->
exists ts',
exists r,
exists tpr,
exists bp,
exists tp,
exists sp,
tso_pc_ss_rel_witt ts'
ss bp tp sp /\
range_inside (
p,
n)
r /\
tp t =
r ::
tpr /\
range_not_in (
p,
n) (
sp t).
Proof.
intros ts ss t p n sbr TREL SB MP.
destruct TREL as [
bp [
tp [
sp TWREL]]].
remember (
bp t)
as bpt.
revert bp Heqbpt ts tp TWREL.
induction bpt as [|
bph bpt IH];
intros bp E ts tp TWREL;
apply sym_eq in E;
generalize TWREL;
destruct 1.
specialize (
BPART t).
rewrite E,
SB in BPART.
done.
specialize (
IH (
fun t' =>
if peq t'
t then bpt else bp t')).
simpl in IH.
destruct (
peq t t);
try done.
specialize (
IH (
refl_equal _)).
destruct (
TREL t)
as [
PIt BRELt].
inv BRELt.
inv BSR;
rewrite E in *;
clarify.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t ((
p0,
n0) ::
tp t)
tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
eapply ss_rel_preservation_alloc_tgt;
try edone.
by rewrite E,
BSR0.
done.
simpl.
by rewrite tupdate_s.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
exists (
mktsostate (
tupdate t tb ts.(
tso_buffers))
tm').
exists (
p0,
n0).
exists (
tp t).
exists bp.
exists (
update_partitioning t ((
p0,
n0) ::
tp t)
tp).
exists sp.
apply buffered_states_related_length_eq in BSR0.
split.
eapply ss_rel_preservation_alloc_tgt;
try edone;
by rewrite E,
BSR0.
split.
specialize (
AR _ (
in_eq _ _)).
simpl in AR.
by destruct AR as [
SCR |
RI]; [
mach_scr_elim | ].
split.
by rewrite update_partitioning_s.
unfold part_update_buffer in PUB;
simpl in PUB.
by destruct valid_alloc_range_dec;
try destruct range_in_dec.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t tp0 tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_free_nil _ _ _ _ _ _ _ _ _ _ t);
try edone;
eby apply sym_eq.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
FR _ (
in_eq _ _)).
unfold is_item_scratch_update in FR.
by destruct FR; [
mach_scr_elim | ].
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
by simpl in BIIR.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
SCR _ (
in_eq _ _)).
unfold is_item_scratch_update in SCR.
mach_scr_elim.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
AR _ (
in_eq _ _)).
unfold is_item_scratch_update in AR.
destruct AR.
mach_scr_elim.
eexists;
eexists;
eexists;
eexists;
eexists;
eexists.
split.
edone.
split.
edone.
split.
eby apply sym_eq.
unfold part_update_buffer in PUB;
simpl in PUB.
by destruct valid_alloc_range_dec;
try destruct range_in_dec.
Qed.
Lemma alloc_stack_src_buff_impl_part_update_succ:
forall ts ss bp tp sp t bi sbr,
tso_pc_ss_rel_witt ts ss bp tp sp ->
ss.(
tso_buffers)
t =
bi ::
sbr ->
part_update bi (
sp t) <>
None.
Proof.
intros ts ss bp tp sp t bi sbr TWREL SB.
remember (
bp t)
as bpt.
revert bp Heqbpt ts tp TWREL.
induction bpt as [|
bph bpt IH];
intros bp E ts tp TWREL;
apply sym_eq in E;
generalize TWREL;
destruct 1.
specialize (
BPART t).
rewrite E,
SB in BPART.
done.
specialize (
IH (
fun t' =>
if peq t'
t then bpt else bp t')).
simpl in IH.
destruct (
peq t t);
try done.
specialize (
IH (
refl_equal _)).
destruct (
TREL t)
as [
PIt BRELt].
inv BRELt.
inv BSR;
rewrite E in *;
clarify.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t ((
p,
n) ::
tp t)
tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
eapply ss_rel_preservation_alloc_tgt;
try edone.
by rewrite E,
BSR0.
done.
simpl.
by rewrite tupdate_s.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct (
part_update bphi (
sp t)).
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t tp0 tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_free_nil _ _ _ _ _ _ _ _ _ _ t);
try edone;
eby apply sym_eq.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
FR _ (
in_eq _ _)).
unfold is_item_scratch_update in FR.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct (
part_update bphi (
sp t)).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
by rewrite buffer_item_irrelevant_part_update.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct (
part_update bphi (
sp t)).
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct (
part_update bphi (
sp t)).
Qed.
Lemma tso_ss_rel_range_allocated:
forall ts ss p n k,
tso_pc_ss_rel ts ss ->
range_allocated (
p,
n)
k ss.(
tso_mem) ->
machine_ptr p ->
exists r',
range_inside (
p,
n)
r' /\
range_allocated r'
k ts.(
tso_mem).
Proof.
intros ts ss p n k [
bp [
tp [
sp []]]]
RA MP.
destruct k;
try (
by exists (
p,
n);
split;
[
apply range_inside_refl | ];
try apply (
NSMR (
p,
n)
MObjGlobal);
try apply (
NSMR (
p,
n)
MObjHeap)).
destruct (
proj2 (
proj2 (
proj2 MRWPs) (
p,
n))
RA)
as [
t INPs].
destruct (
proj1 (
TREL t)
_ _ MP INPs)
as [
r [
RIN INPt]].
exists r.
split.
done.
apply (
proj1 (
proj2 (
proj2 MRWPt)
r)).
eby eexists.
Qed.
Lemma tso_ss_rel_non_stack_alloc_contr:
forall ts ss r k pi ni ki b t,
tso_pc_ss_rel ts ss ->
range_allocated r k (
tso_mem ss) ->
ranges_overlap (
pi,
ni)
r ->
tso_buffers ss t =
BufferedAlloc pi ni ki ::
b ->
non_stack_kind ki ->
False.
Proof.
Lemma tso_pc_rel_valid_alloc_range_src_buff:
forall ts ss t p n k br,
tso_pc_ss_rel ts ss ->
ss.(
tso_buffers)
t =
BufferedAlloc p n k ::
br ->
valid_alloc_range (
p,
n).
Proof.
intros ts ss t p n k br [
bp [
tp [
sp TWREL]]]
SB.
remember (
bp t)
as bpt.
revert bp Heqbpt ts tp TWREL.
induction bpt as [|
bph bpt IH];
intros bp E ts tp TWREL;
apply sym_eq in E;
generalize TWREL;
destruct 1.
specialize (
BPART t).
rewrite E,
SB in BPART.
done.
specialize (
IH (
fun t' =>
if peq t'
t then bpt else bp t')).
simpl in IH.
destruct (
peq t t);
try done.
specialize (
IH (
refl_equal _)).
destruct (
TREL t)
as [
PIt BRELt].
inv BRELt.
inv BSR;
rewrite E in *;
clarify.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t ((
p0,
n0) ::
tp t)
tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
eapply ss_rel_preservation_alloc_tgt;
try edone.
by rewrite E,
BSR0.
done.
simpl.
by rewrite tupdate_s.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct k;
destruct valid_alloc_range_dec.
destruct (
unbuffer_unbuffer_safe TUS (
sym_eq H0))
as [
tm' [
ABIt US']].
simpl in ABIt,
US'.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH (
mktsostate
(
tupdate t tb (
tso_buffers ts))
tm')
(
update_partitioning t tp0 tp)).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR0.
eapply (
ss_rel_preservation_free_nil _ _ _ _ _ _ _ _ _ _ t);
try edone;
eby apply sym_eq.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB.
simpl in PUB.
by destruct k;
destruct valid_alloc_range_dec.
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
simpl in BIIR.
by destruct k;
destruct BIIR.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
unfold part_update_buffer in PUB;
simpl in PUB.
by destruct k;
destruct valid_alloc_range_dec;
try destruct range_in_dec.
rewrite E in *;
clarify.
destruct bph as [|
bphi bphs].
inv PUB.
specialize (
IH ts tp).
apply modusponens in IH.
done.
apply buffered_states_related_length_eq in BSR.
by eapply (
ss_rel_preservation_src_nil _ _ _ _ _ _ t).
specialize (
BPART t).
rewrite E,
SB in BPART.
simpl in BPART.
inv BPART.
specialize (
AR _ (
in_eq _ _)).
unfold is_item_scratch_update in AR.
unfold part_update_buffer in PUB;
simpl in PUB.
by destruct k;
destruct valid_alloc_range_dec;
try destruct range_in_dec.
Qed.
Lemma range_allocated_restr:
forall p n k m,
range_allocated (
p,
n)
k m ->
restricted_pointer p m.
Proof.
Lemma machine_overlap_machine:
forall p1 n1 p2 n2,
ranges_overlap (
p1,
n1) (
p2,
n2) ->
machine_ptr p1 ->
machine_ptr p2.
Proof.
by intros [
b1 o1]
n1 [
b2 o2]
n2 O;
destruct (
ranges_overlapD O)
as [->
_].
Qed.
Lemma alloc_unbuffer_safe:
forall t ss ts ss'
ab,
tso_pc_ss_rel ts ss ->
unbuffer_safe ss' ->
disjoint_allocs ab ->
ss.(
tso_buffers)
t =
ss'.(
tso_buffers)
t ++
ab ->
(
forall t',
t' <>
t ->
ss.(
tso_buffers)
t' =
ss'.(
tso_buffers)
t') ->
(
forall r k,
range_allocated r k ss'.(
tso_mem) ->
range_allocated r k ss.(
tso_mem)) ->
unbuffer_safe ss.
Proof.
Inductive alloc_steps :
Csharpminor.state ->
list arange ->
Csharpminor.state ->
Prop :=
|
alloc_steps_refl:
forall s,
alloc_steps s nil s
|
alloc_steps_step:
forall s s'
s''
p n b
(
STEP :
cs_step csm_globenv s (
TEmem (
MEalloc p n MObjStack))
s')
(
AS :
alloc_steps s'
b s''),
alloc_steps s ((
p,
n) ::
b)
s''.
Tactic Notation "
alloc_steps_cases"
tactic(
first)
tactic(
c) :=
first; [
c "
alloc_steps_refl" |
c "
alloc_steps_step"].
Definition base_offset :=
Int.repr 8.
Fixpoint ranges_of_vars (
vars:
list (
ident *
var_kind))
(
cenv:
compilenv)
(
scratch_block :
Z)
(
bp :
pointer)
:
option (
list arange) :=
match vars with
| (
vid,
Vscalar c) ::
r =>
match PMap.get vid cenv with
|
Var_local c' =>
match ranges_of_vars r cenv (
scratch_block + 1)
bp with
|
Some rb =>
Some ((
Ptr scratch_block base_offset,
Int.repr (
size_chunk c)) ::
rb)
|
None =>
None
end
|
Var_stack_scalar c'
offs =>
match ranges_of_vars r cenv scratch_block bp with
|
Some rb =>
Some ((
Ptr.add bp (
Int.repr offs),
Int.repr (
size_chunk c)) ::
rb)
|
None =>
None
end
|
_ =>
None
end
| (
vid,
Varray sz) ::
r =>
match PMap.get vid cenv with
|
Var_stack_array offs =>
match ranges_of_vars r cenv scratch_block bp with
|
Some rb =>
Some ((
Ptr.add bp (
Int.repr offs),
Int.repr (
Zmax 1
sz)) ::
rb)
|
None =>
None
end
|
_ =>
None
end
|
nil =>
Some nil
end.
Definition get_name (
v :
ident *
var_kind) :=
let (
n,
_) :=
v in n.
Definition get_vkind (
v :
ident *
var_kind) :=
let (
_,
k) :=
v in k.
Lemma assign_variables_not_in:
forall vr v ids ce s ce'
s',
~
In v (
map get_name vr) ->
assign_variables ids vr (
ce,
s) = (
ce',
s') ->
ce !!
v =
ce' !!
v.
Proof.
intro vr.
induction vr as [|
vh vt IH].
intros;
simpl in *;
clarify.
intros v ids ce s ce'
s'
NIN AV.
destruct vh as [
vid []];
simpl in AV;
(
assert (
NINv : ~
In v (
map get_name vt));
[
intro;
elim NIN;
simpl;
by right |]);
destruct (
Identset.mem vid ids);
specialize (
IH _ _ _ _ _ _ NINv AV) ;
rewrite PMap.gso in IH;
try done;
intro;
subst;
apply NIN;
left;
done.
Qed.
Lemma align_size_chunk_le:
forall n c,
n <=
align n (
size_chunk c).
Proof.
Lemma array_alignment_pos:
forall sz,
array_alignment sz > 0.
Proof.
intro.
unfold array_alignment.
repeat destruct zlt;
omega.
Qed.
Lemma assign_variables_mono:
forall ids vars ge n ce sz,
assign_variables ids vars (
ge,
n) = (
ce,
sz) ->
n <=
sz.
Proof.
Lemma assign_variables_in:
forall ids vars ge n ce sz,
NoDup (
map get_name vars) ->
assign_variables ids vars (
ge,
n) = (
ce,
sz) ->
forall v,
In v vars ->
match ce !! (
get_name v)
with
|
Var_stack_scalar c ofs =>
n <=
ofs /\
ofs +
size_chunk c <=
sz /\
get_vkind v =
Vscalar c /\
Identset.mem (
get_name v)
ids =
true
|
Var_local c =>
get_vkind v =
Vscalar c /\
Identset.mem (
get_name v)
ids =
false
|
Var_stack_array ofs =>
n <=
ofs /\
exists asz,
get_vkind v =
Varray asz /\
ofs +
Zmax 1
asz <=
sz
|
_ =>
False
end.
Proof.
Lemma align_size_le_divides:
forall s s'
(
LT :
s <=
s'),
(
align_size s |
align_size s').
Proof.
intros.
unfold align_size.
repeat destruct zlt;
try omegaContradiction;
by apply Zmod_divide.
Qed.
Lemma align_add:
forall s'
s n ofs
(
ALn : (
align_size s' |
n))
(
ALo : (
align_size s |
ofs))
(
Szlt:
s' <=
s),
(
align_size s' |
ofs +
n).
Proof.
Lemma align_size_chunk:
forall c,
(
align_size (
size_chunk c) |
size_chunk c).
Proof.
Lemma align_size_array:
forall sz,
(
align_size (
Zmax 1
sz) |
array_alignment sz).
Proof.
intro sz.
unfold align_size,
array_alignment.
assert (
Zmax 1
sz =
sz \/
sz < 1 /\
Zmax 1
sz = 1).
pose proof (
Zmax_spec 1
sz).
by destruct zlt;
vauto.
repeat destruct zlt;
try omegaContradiction;
try (
by apply Zmod_divide).
Qed.
Lemma ranges_of_vars_succ:
forall ids vars ge n sbp bp cenv fsize,
NoDup (
map get_name vars) ->
Ptr.block bp <
sbp ->
assign_variables ids vars (
ge,
n) = (
cenv,
fsize) ->
0 <=
n ->
fsize <=
Int.max_unsigned ->
valid_alloc_range (
bp,
Int.repr fsize) \/
fsize = 0 ->
exists rs,
ranges_of_vars vars cenv sbp bp =
Some rs /\
range_list_disjoint rs /\
(
forall r,
In r rs ->
valid_alloc_range r) /\
forall r,
In r rs ->
range_inside r (
bp,
Int.repr fsize) /\
(
Int.unsigned (
Ptr.offset bp) +
n <=
Int.unsigned (
Ptr.offset (
fst r))) \/
Ptr.block (
fst r) >=
sbp.
Proof.
intros ids vars.
induction vars as [|
v vr IH];
intros ge n sbp bp cenv fsize ND BIEQ AV NPOS MU VAR.
eby eexists.
inversion ND as [ |
vids vir NIN NDvr];
subst.
simpl in AV.
destruct v as [
vid [
c |
sz]].
destruct (
Identset.mem vid ids).
pose proof (
size_chunk_pos c)
as SCPOS.
pose proof (
align_size_chunk_le n c)
as ASCPOS.
assert (
NPOS': 0 <=
align n (
size_chunk c) +
size_chunk c).
omega.
specialize (
IH _ _ sbp bp _ _ NDvr BIEQ AV NPOS'
MU VAR).
destruct IH as [
rs' (
ROV &
RLD &
VARS &
RINOS)].
eexists.
split.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in *.
rewrite <-
E,
PMap.gss,
ROV.
reflexivity.
pose proof (
assign_variables_mono _ _ _ _ _ _ AV)
as ALFS.
unfold valid_alloc_range in VAR.
rewrite !
Int.unsigned_repr in VAR. 2 :
omega.
split.
split.
done.
intros [[
b'
o']
n']
IN'.
destruct bp as [
bpb bpo].
destruct (
RINOS _ IN')
as [[
RIN SEP] |
SCR].
right.
left.
simpl in SEP.
destruct RIN as [->
RIN].
eapply Zle_trans,
SEP.
rewrite !
Int.add_unsigned, !
size_chunk_repr;
repeat rewrite Int.unsigned_repr;
try omega.
unfold Int.max_unsigned.
omega.
left.
intro E.
rewrite E in *.
simpl in *.
omega.
split.
intros r IN.
destruct IN as [<- |
IN].
unfold Ptr.add.
destruct bp.
unfold valid_alloc_range.
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
repeat split;
try omega.
destruct VAR as [(
L &
SZ &
H &
ALG) |
E0]; [|
omegaContradiction].
eapply align_add.
-
eapply Zdivide_trans,
align_divides,
size_chunk_pos.
apply align_size_chunk.
-
apply ALG.
-
omega.
by apply VARS.
intros r IN.
simpl in IN.
destruct IN as [<- |
IN].
left.
destruct bp as [
bpb bpo].
split.
split.
done.
right;
split;
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
omega.
unfold Ptr.offset,
Ptr.add,
fst.
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
omega.
destruct (
RINOS _ IN)
as [[
RIN SEP] |
SCR].
left.
split.
done.
omega.
by right.
assert (
BIEQ':
Ptr.block bp <
sbp + 1).
omega.
specialize (
IH _ _ (
sbp + 1)
bp _ _ NDvr BIEQ'
AV NPOS MU VAR).
destruct IH as [
rs' (
ROV &
RLD &
VARS &
RINOS)].
eexists.
split.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in *.
rewrite <-
E,
PMap.gss,
ROV.
reflexivity.
split.
split.
done.
intros [[
b'
o']
n']
IN'.
destruct (
RINOS _ IN')
as [[
RIN SEP] |
SCR].
left.
intro E.
subst.
destruct bp.
destruct RIN as [->
_].
simpl in *.
omega.
left.
intro E.
subst.
simpl in *.
omega.
split.
intros r IN.
destruct IN as [<- |
IN].
by destruct c;
repeat split;
try compute;
try done;
apply Zmod_divide.
by apply VARS.
intros r IN.
simpl in IN.
destruct IN as [<- |
IN].
right.
simpl.
omega.
destruct (
RINOS _ IN)
as [[
RIN SEP] |
SCR].
left.
split.
done.
omega.
right.
omega.
pose proof (
Zle_max_l 1
sz)
as SCPOS.
pose proof (
array_alignment_pos sz)
as AAPOS.
pose proof (
align_le n _ AAPOS)
as ASCPOS.
assert (
NPOS': 0 <=
align n (
array_alignment sz) +
Zmax 1
sz).
omega.
specialize (
IH _ _ sbp bp _ _ NDvr BIEQ AV NPOS'
MU VAR).
destruct IH as [
rs' (
ROV &
RLD &
VARS &
RINOS)].
eexists.
split.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in *.
rewrite <-
E,
PMap.gss,
ROV.
reflexivity.
pose proof (
assign_variables_mono _ _ _ _ _ _ AV)
as ALFS.
unfold valid_alloc_range in VAR.
rewrite !
Int.unsigned_repr in VAR. 2 :
omega.
split.
split.
done.
intros [[
b'
o']
n']
IN'.
destruct bp as [
bpb bpo].
destruct (
RINOS _ IN')
as [[
RIN SEP] |
SCR].
right.
left.
simpl in SEP.
destruct RIN as [->
RIN].
eapply Zle_trans,
SEP.
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega.
unfold Int.max_unsigned.
omega.
left.
intro E.
rewrite E in *.
simpl in *.
omega.
split.
intros r IN.
destruct IN as [<- |
IN].
destruct bp;
unfold Ptr.add,
valid_alloc_range.
destruct VAR as [(
L &
SZ &
H &
ALG) |
E0]; [|
omegaContradiction].
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
repeat split;
try omega; [].
eapply align_add.
-
eapply Zdivide_trans. 2 :
apply align_divides.
apply align_size_array.
apply array_alignment_pos.
-
apply ALG.
-
omega.
by apply VARS.
intros r IN.
simpl in IN.
destruct IN as [<- |
IN].
left.
destruct bp as [
bpb bpo].
split.
split.
done.
right;
split;
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
omega.
unfold Ptr.offset,
Ptr.add,
fst.
rewrite !
Int.add_unsigned;
repeat rewrite Int.unsigned_repr;
try omega;
unfold Int.max_unsigned;
omega.
destruct (
RINOS _ IN)
as [[
RIN SEP] |
SCR].
left.
split.
done.
omega.
by right.
Qed.
Definition alloc_item_of_range (
r :
arange) :=
let (
p,
n) :=
r in BufferedAlloc p n MObjStack.
Definition alloc_items_of_ranges (
rs :
list arange) :=
List.map alloc_item_of_range rs.
Lemma apply_buffer_cons_decomp:
forall bi b m m',
apply_buffer (
bi ::
b)
m =
Some m' ->
exists m'',
apply_buffer_item bi m =
Some m'' /\
apply_buffer b m'' =
Some m'.
Proof.
intros bi b m m'
AB.
simpl in AB.
destruct (
apply_buffer_item bi m)
as [
m''|]
_eqn :
ABI;
try done.
exists m''.
by split.
Qed.
Definition cst_range_list (
p :
pointer) (
n :
Z) :=
if zeq n 0
then (
p,
Int.repr n) ::
nil
else nil.
Fixpoint build_csm_env (
vars :
list (
ident *
var_kind))
(
cenv :
compilenv)
(
sbp :
Z)
(
bp :
pointer)
(
acc :
env) :
env :=
match vars with
| (
vid,
vk) ::
vt =>
match cenv !!
vid with
|
Var_local c =>
build_csm_env vt cenv (
sbp + 1)
bp
(
acc !
vid <- (
Ptr sbp base_offset,
vk))
|
Var_stack_scalar c ofs =>
build_csm_env vt cenv sbp bp
(
acc !
vid <- (
Ptr.add bp (
Int.repr ofs),
vk))
|
Var_stack_array ofs =>
build_csm_env vt cenv sbp bp
(
acc !
vid <- (
Ptr.add bp (
Int.repr ofs),
vk))
|
_ =>
acc
end
|
nil =>
acc
end.
Definition renv :
Type :=
PTree.t arange.
Lemma elems_of_empty_nil:
forall A,
PTree.elements (
PTree.empty A) =
nil.
Proof.
Lemma permutation_1_eq:
forall A l (
e :
A),
Permutation l (
e ::
nil) ->
l = (
e ::
nil).
Proof.
intros A l e P.
remember (
e ::
nil)
as enil.
induction P;
subst;
try done.
clarify.
apply Permutation_sym,
Permutation_nil in P.
by rewrite P.
rewrite <-
IHP2 in IHP1 |- *;
try done.
by rewrite IHP1.
Qed.
Lemma nodup_map:
forall A B (
f :
A ->
B) (
l :
list A),
NoDup (
map f l) ->
NoDup l.
Proof.
intros A B f l.
induction l as [|
h t IH];
simpl;
intro ND;
constructor;
inversion ND as [ |
h'
t'
NIN NDvr];
subst.
intro IN;
apply NIN,
in_map,
IN.
apply IH,
NDvr.
Qed.
Lemma ptree_elems_1_eq:
forall A id (
x :
A),
PTree.elements (
PTree.empty A) !
id <-
x = (
id,
x) ::
nil.
Proof.
Lemma ptree_elems_insert:
forall A e v (
x :
A),
e !
v =
None ->
Permutation ((
v,
x) :: (
PTree.elements e))
(
PTree.elements (
e !
v <-
x)).
Proof.
Lemma ptree_insert_2_comm:
forall A x y (
a :
A)
b e,
x <>
y ->
e !
x <-
a !
y <-
b =
e !
y <-
b !
x <-
a.
Proof.
intros A x y a b e NE.
apply PTree.ext.
intro k.
destruct (
peq k x)
as [<- |
Nx];
destruct (
peq k y)
as [<- |
Ny];
by repeat (
try rewrite PTree.gss;
try rewrite PTree.gso).
Qed.
Lemma build_env_ranges_cons_perm:
forall v vr cenv sbp bp p vk e,
~
In v (
map get_name vr) ->
e !
v =
None ->
Permutation ((
p,
Int.repr (
sizeof(
vk))) ::
env_ranges (
build_csm_env vr cenv sbp bp e))
(
env_ranges (
build_csm_env vr cenv sbp bp (
e !
v <- (
p,
vk)))).
Proof.
Lemma env_ranges_permut_range_of_vars:
forall vars cenv sbp bp rs er,
NoDup (
map get_name vars) ->
ranges_of_vars vars cenv sbp bp =
Some rs ->
env_ranges (
build_csm_env vars cenv sbp bp empty_env) =
er ->
Permutation rs er.
Proof.
Lemma range_list_disjoint_app:
forall l1 l2,
range_list_disjoint (
l1 ++
l2) <->
range_list_disjoint l1 /\
range_list_disjoint l2 /\
range_lists_disjoint l1 l2.
Proof.
intros l1 l2.
induction l1 as [|
h t IH].
simpl.
repeat (
split;
try done).
by intros (
_ &
RLD &
_).
rewrite <-
app_comm_cons.
simpl.
split.
intros (
RLD &
RNI).
apply IH in RLD.
destruct RLD as (
RLDt &
RLDl2 &
RLSD).
split.
split.
done.
intros r IN.
apply RNI,
in_or_app.
by left.
split.
done.
intros r1 IN1 r2 IN2.
simpl in IN1.
destruct IN1 as [-> |
IN1].
apply RNI,
in_or_app.
by right.
by apply RLSD.
intros ((
RLDt &
RNI) &
RLDl2 &
RLSD).
split.
apply IH.
split.
done.
split.
done.
intros r1 IN1 r2 IN2.
apply RLSD.
by apply in_cons.
done.
intros r IN.
apply in_app_or in IN.
destruct IN as [
IN |
IN].
by apply RNI.
apply RLSD.
apply in_eq.
done.
Qed.
Lemma range_list_disjoint_perm:
forall l l',
Permutation l l' ->
range_list_disjoint l ->
range_list_disjoint l'.
Proof.
Definition mkcstenv (
p :
pointer) (
n :
Z)
(
e :
PTree.t Cstacked.env_item) :
Cstacked.env :=
mkcsenv (
if zeq n 0
then None else (
Some p))
e.
Lemma env_item_related_mem_alloc:
forall m sz bp ei1 ei2 p n k m',
env_item_related m sz bp ei1 ei2 ->
alloc_ptr (
p,
n)
k m =
Some m' ->
env_item_related m'
sz bp ei1 ei2.
Proof.
intros m sz bp ei1 ei2 p n k m'
EIR AP.
inv EIR;
econstructor;
try edone.
eby eapply load_some_alloc.
Qed.
Definition scratch_min_block := 1.
Lemma scratch_less_block:
forall b,
scratch_min_block <=
b ->
low_mem_restr b =
false.
Proof.
intros b.
unfold low_mem_restr.
destruct (
zeq b 0)
as [-> |
N];
try done.
unfold scratch_min_block.
intro;
omegaContradiction.
Qed.
Definition local_cons_with_ids (
te :
PTree.t Cstacked.env_item)
(
ids :
Identset.t) :
Prop :=
forall id,
match te !
id with
|
Some (
Env_local _ _) =>
Identset.mem id ids =
false
|
_ =>
True
end.
Lemma buffer_alloc_env_related:
forall env'
f opt ids vars cenv sbp bp rs vs k te te'
se se'
m m'
ge n fsize,
ranges_of_vars vars cenv sbp bp =
Some rs ->
apply_buffer (
alloc_items_of_ranges rs)
m =
Some m' ->
build_envmap vars cenv te =
Some te' ->
NoDup (
map get_name vars) ->
Ptr.block bp <
sbp ->
scratch_min_block <=
sbp ->
assign_variables ids vars (
ge,
n) = (
cenv,
fsize) ->
0 <=
n ->
fsize <=
Int.max_unsigned ->
valid_alloc_range (
bp,
Int.repr fsize) \/
fsize = 0 ->
build_csm_env vars cenv sbp bp se =
se' ->
env_items_related (
Int.repr fsize)
m
(
mkcstenv bp fsize te)
se ->
local_cons_with_ids te ids ->
alloc_steps (
SKalloc vs vars se (
Kcall opt (
Internal f)
env'
k))
rs
(
SKalloc vs nil se' (
Kcall opt (
Internal f)
env'
k)) /\
env_items_related (
Int.repr fsize)
m'
(
mkcstenv bp fsize te')
se' /\
local_cons_with_ids te'
ids.
Proof.
intros env'
f opt ids vars.
induction vars as [|
v vr IH];
intros cenv sbp bp rs vs k te te'
se se'
m m'
ge n fsize
ROV AB BEM ND UM SBPSCR AV NPOS FSIZEL VAR BE ER LCI.
simpl in ROV.
clarify.
simpl in AB,
BEM.
clarify.
split.
econstructor.
done.
inversion ND as [ |
vids vir NIN NDvr [
E1 E2]].
simpl in ROV.
simpl in AV.
destruct v as [
vid [
c |
sz]].
destruct (
Identset.mem vid ids)
as []
_eqn :
ISM.
pose proof (
size_chunk_pos c)
as SCPOS.
pose proof (
align_size_chunk_le n c)
as ASCPOS.
assert (
NPOS': 0 <=
align n (
size_chunk c) +
size_chunk c).
omega.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in E.
simpl in BEM,
BE.
rewrite <-
E,
PMap.gss in ROV,
BEM,
BE.
destruct (
ranges_of_vars vr cenv sbp bp)
as [|
rs']
_eqn :
Erov; [|
done].
injection ROV as Er;
rewrite <-
Er in *;
clear Er.
unfold alloc_items_of_ranges in AB.
simpl map in AB.
apply apply_buffer_cons_decomp in AB.
destruct AB as [
mi (
ABI &
AB)].
specialize (
IH _ _ _ _ vs k _ _ _ se'
_ _ _ _ _
Erov AB BEM NDvr UM SBPSCR AV NPOS'
FSIZEL VAR BE).
exploit IH.
intro id.
simpl.
destruct (
peq id vid)
as [-> |
N].
rewrite !
PTree.gss.
apply assign_variables_mono in AV.
destruct (
zeq fsize 0)
as [-> |
Nf0].
omegaContradiction.
eapply env_item_related_scalar.
omega.
rewrite Zmod_small.
done.
unfold Int.max_unsigned in FSIZEL.
omega.
rewrite !
PTree.gso;
try done.
pose proof (
ER id)
as ERid.
simpl in ERid.
destruct (
te !
id);
destruct (
se !
id);
try done.
eby eapply env_item_related_mem_alloc.
intro id.
destruct (
peq id vid)
as [-> |
N].
by rewrite PTree.gss.
rewrite PTree.gso.
apply (
LCI id).
done.
intros [
AS EIR].
split; [|
done].
eapply alloc_steps_step. 2 :
apply AS.
by eapply StepAllocLocal.
assert (
BIEQ':
Ptr.block bp <
sbp + 1).
omega.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in E.
simpl in BEM,
BE.
rewrite <-
E,
PMap.gss in ROV,
BEM,
BE.
destruct (
ranges_of_vars vr cenv (
sbp+1)
bp)
as [|
rs']
_eqn :
Erov; [|
done].
injection ROV as Er;
rewrite <-
Er in *;
clear Er.
unfold alloc_items_of_ranges in AB.
simpl map in AB.
apply apply_buffer_cons_decomp in AB.
destruct AB as [
mi (
ABI &
AB)].
assert (
SBPSCR' :
scratch_min_block <=
sbp + 1).
omega.
specialize (
IH _ (
sbp + 1)
bp _ vs k _ _ _ se'
_ _ _ _ _
Erov AB BEM NDvr BIEQ'
SBPSCR'
AV NPOS FSIZEL VAR BE).
exploit IH.
intro id.
simpl.
destruct (
peq id vid)
as [-> |
N].
rewrite !
PTree.gss.
eapply env_item_related_local.
eapply load_alloc_inside.
unfold apply_buffer_item in ABI.
apply ABI.
apply range_inside_refl.
unfold pointer_chunk_aligned,
base_offset,
align_chunk.
by destruct c;
compute;
apply Zmod_divide;
try compute.
by apply scratch_less_block.
done.
split.
by compute.
repeat (
split; [
by by destruct c;
simpl;
compute|]).
by destruct c;
compute;
apply Zmod_divide.
by destruct c.
rewrite !
PTree.gso;
try done.
pose proof (
ER id)
as ERid.
simpl in ERid.
destruct (
te !
id);
destruct (
se !
id);
try done.
eapply env_item_related_mem_alloc.
edone.
unfold apply_buffer_item in ABI.
apply ABI.
intro id.
destruct (
peq id vid)
as [-> |
N].
by rewrite PTree.gss.
rewrite PTree.gso.
apply (
LCI id).
done.
intros [
AS EIR].
split; [|
done].
eapply alloc_steps_step. 2 :
apply AS.
by econstructor.
pose proof (
array_alignment_pos sz)
as SCPOS.
pose proof (
align_le n (
array_alignment sz)
(
array_alignment_pos sz))
as ASCPOS.
pose proof (
Zle_max_l 1
sz).
assert (
NPOS': 0 <=
align n (
array_alignment sz) +
Zmax 1
sz).
omega.
pose proof (
assign_variables_not_in _ _ _ _ _ _ _ NIN AV)
as E.
simpl in E.
simpl in BEM,
BE.
rewrite <-
E,
PMap.gss in ROV,
BEM,
BE.
destruct (
ranges_of_vars vr cenv sbp bp)
as [|
rs']
_eqn :
Erov; [|
done].
injection ROV as Er;
rewrite <-
Er in *;
clear Er.
unfold alloc_items_of_ranges in AB.
simpl map in AB.
apply apply_buffer_cons_decomp in AB.
destruct AB as [
mi (
ABI &
AB)].
specialize (
IH _ _ _ _ vs k _ _ _ se'
_ _ _ _ _
Erov AB BEM NDvr UM SBPSCR AV NPOS'
FSIZEL VAR BE).
exploit IH.
intro id.
simpl.
destruct (
peq id vid)
as [-> |
N].
rewrite !
PTree.gss.
apply assign_variables_mono in AV.
destruct (
zeq fsize 0)
as [-> |
Nf0].
omegaContradiction.
eapply env_item_related_array.
omega.
rewrite Zmod_small.
done.
unfold Int.max_unsigned in FSIZEL.
omega.
rewrite !
PTree.gso;
try done.
pose proof (
ER id)
as ERid.
simpl in ERid.
destruct (
te !
id);
destruct (
se !
id);
try done.
eby eapply env_item_related_mem_alloc.
intro id.
destruct (
peq id vid)
as [-> |
N].
by rewrite PTree.gss.
rewrite PTree.gso.
apply (
LCI id).
done.
intros [
AS EIR].
split; [|
done].
eapply alloc_steps_step. 2 :
apply AS.
by eapply StepAllocLocal.
Qed.
Lemma update_buffer_allocs:
forall als sp,
(
forall r,
In r als ->
valid_alloc_range r) ->
range_list_disjoint als ->
range_lists_disjoint als sp ->
part_update_buffer (
alloc_items_of_ranges als)
sp =
Some (
rev als ++
sp).
Proof.
intros als.
induction als as [|
h t IH].
intros.
unfold part_update_buffer.
done.
intros sp VARS RLD RLSD.
specialize (
IH (
h ::
sp)).
exploit IH.
intros r IN.
by apply VARS,
in_cons.
by destruct RLD.
intros r1 IN1 r2 IN2.
simpl in IN2.
destruct IN2 as [<- |
IN2].
by apply ranges_disjoint_comm, (
proj2 RLD).
apply RLSD.
by apply in_cons.
done.
unfold part_update_buffer.
simpl.
intros PUB.
destruct (
part_update (
alloc_item_of_range h)
sp)
as [
spi|]
_eqn :
PU;
destruct h as [
p n];
simpl in PU;
destruct valid_alloc_range_dec as [|
NVAR];
try done;
try destruct range_in_dec as [[
r' [
IN OVER]] |];
try done.
inv PU.
rewrite app_ass.
done.
byContradiction.
eapply ranges_disjoint_dont_overlap,
OVER.
apply RLSD.
apply in_eq.
done.
elim NVAR.
apply VARS,
in_eq.
Qed.
Lemma buffers_related_part_update:
forall {
tb tp bp sp},
buffers_related tb tp bp sp ->
(
exists tp',
part_update_buffer tb tp =
Some tp') /\
(
exists sp',
part_update_buffer (
flatten bp)
sp =
Some sp').
Proof.
Lemma unbuffer_safe_partition_alloc:
forall tso tb tp t p n tp',
unbuffer_safe tso ->
mem_related_with_partitioning tso.(
tso_mem)
tp ->
(
tso_buffers tso t) =
tb ++
BufferedAlloc p n MObjStack ::
nil ->
part_update_buffer tb (
tp t) =
Some tp' ->
range_not_in (
p,
n)
tp'.
Proof.
Lemma unbuffer_safe_partition_alloc_pub:
forall tso tb tp t p n tp',
unbuffer_safe tso ->
mem_related_with_partitioning tso.(
tso_mem)
tp ->
(
tso_buffers tso t) =
tb ++
BufferedAlloc p n MObjStack ::
nil ->
part_update_buffer tb (
tp t) =
Some tp' ->
part_update_buffer (
tb ++
BufferedAlloc p n MObjStack ::
nil) (
tp t) =
Some ((
p,
n) ::
tp').
Proof.
Lemma states_related_suffix:
forall sb tb tp sp sm ts ss tp'
sp'
sm'
ts'
ss'
sb'
tb',
(
state_related tp sp sm ts ss ->
buffered_states_related tb tp ts'
sb sp sm ss') ->
buffered_states_related tb'
tp'
ts sb'
sp'
sm'
ss ->
apply_buffer sb'
sm' =
Some sm ->
part_update_buffer sb'
sp' =
Some sp ->
part_update_buffer tb'
tp' =
Some tp ->
buffered_states_related (
tb' ++
tb)
tp'
ts' (
sb' ++
sb)
sp'
sm'
ss'.
Proof.
intros sb tb tp sp sm ts ss tp'
sp'
sm'
ts'
ss'
sb'
tb'
SIMPL
BSR'
AB PUBs PUBt.
destruct BSR'
as [
smi [
spi [
tpi (
ABi &
PUBti &
PUBsi &
SR' &
SCO')]]].
rewrite PUBt in PUBti.
inv PUBti.
rewrite PUBs in PUBsi.
inv PUBsi.
rewrite AB in ABi.
inv ABi.
destruct (
SIMPL SR')
as [
sm [
sp [
tp (
AB' &
PUBt' &
PUBs' &
SR &
SCO)]]].
exists sm.
exists sp.
exists tp.
unfold part_update_buffer in *.
split.
by rewrite apply_buffer_app,
AB.
split.
by rewrite fold_left_opt_app,
PUBt.
split.
by rewrite fold_left_opt_app,
PUBs.
done.
Qed.
There is always an upper bound on all blocks appearing in memory and
buffers
Definition block_bound_buff (
bnd :
Z) (
b :
list buffer_item) :
Prop :=
forall blk ofs n,
In (
BufferedAlloc (
Ptr blk ofs)
n MObjStack)
b ->
blk <
bnd.
Definition block_bound_buffers (
bnd :
Z) (
tso :
tso_state) :
Prop :=
forall t,
block_bound_buff bnd (
tso_buffers tso t).
Lemma block_bound_buff_exists:
forall b,
exists bb,
block_bound_buff bb b.
Proof.
induction b as [|
h t IH].
by exists 0.
destruct IH as [
bb BB].
buffer_item_cases (
destruct h as [
p c v|
p n k|
p k])
Case.
Case "
BufferedWrite".
exists bb;
intros blk ofs n IN;
simpl in IN;
destruct IN as [
E |
IN]; [
done|
exact (
BB _ _ _ IN)].
Case "
BufferedAlloc".
destruct k;
try (
exists bb;
intros blk ofs n'
IN;
simpl in IN;
destruct IN as [
E |
IN]; [
done|
exact (
BB _ _ _ IN)]).
destruct p as [
b ofs].
destruct (
Zle_or_lt bb b).
exists (
b + 1).
intros blk'
ofs'
n'
IN;
simpl in IN.
destruct IN as [
E |
IN].
inv E.
omega.
specialize (
BB _ _ _ IN).
omega.
exists bb.
intros blk'
ofs'
n'
IN;
simpl in IN.
destruct IN as [
E |
IN].
by inv E.
exact (
BB _ _ _ IN).
Case "
BufferedFree".
exists bb;
intros blk ofs n IN;
simpl in IN;
destruct IN as [
E |
IN]; [
done|
exact (
BB _ _ _ IN)].
Qed.
Lemma block_bound_from_fin_sup:
forall tso,
tso_fin_sup tso ->
exists bb,
block_bound_buffers bb tso.
Proof.
intros tso [
l [
ND NEN]];
revert tso NEN.
induction l as [|
h l IH];
intros tso NEN.
exists 0.
intros t b ofs n.
by rewrite (
NEN t).
inversion ND as [|? ?
NI'
ND'];
subst.
specialize (
IH ND' (
mktsostate
(
tupdate h nil tso.(
tso_buffers))
tso.(
tso_mem)) ).
exploit IH.
intros t'
NIN;
simpl.
destruct (
peq t'
h)
as [-> |
N].
by rewrite tupdate_s.
rewrite tupdate_o; [|
done].
apply NEN.
intro IN.
simpl in IN.
destruct IN as [-> |
IN];
done.
intros [
bb BB].
unfold block_bound_buffers in BB.
simpl in BB.
destruct (
block_bound_buff_exists (
tso_buffers tso h))
as [
bbb BBB].
destruct (
Zle_or_lt bb bbb).
exists bbb.
intros t b ofs n IN.
specialize (
BB t).
destruct (
peq t h)
as [-> |
N].
apply (
BBB _ _ _ IN).
rewrite tupdate_o in BB; [|
done].
specialize (
BB _ _ _ IN).
omega.
exists bb.
intros t b ofs n IN.
specialize (
BB t).
destruct (
peq t h)
as [-> |
N].
specialize (
BBB _ _ _ IN).
omega.
rewrite tupdate_o in BB; [|
done].
apply (
BB _ _ _ IN).
Qed.
Definition is_mem_block_bound (
bnd :
Z) (
m :
mem) :
Prop :=
forall b ofs n k,
range_allocated ((
Ptr b ofs),
n)
k m ->
b <
bnd.
Lemma mem_bound_exists:
forall m,
exists bnd,
is_mem_block_bound bnd m.
Proof.
intros m.
destruct (
proj1 (
mvalid m))
as [
bnd B].
exists (
bnd + 1).
intros b ofs n k RA.
simpl in RA.
destruct (
Zle_or_lt (
bnd + 1)
b); [|
done].
exploit (
B b).
omega.
intro G;
rewrite G in RA.
simpl in RA.
done.
Qed.
Definition tso_memory_upper_bound (
bnd :
Z) (
tso :
tso_state) :
Prop :=
block_bound_buffers bnd tso /\
is_mem_block_bound bnd tso.(
tso_mem) /\
scratch_min_block <=
bnd.
Lemma block_bound_buffers_mono:
forall bnd bs bnd',
block_bound_buffers bnd bs ->
bnd <=
bnd' ->
block_bound_buffers bnd'
bs.
Proof.
intros bnd bs bnd' BB LE.
intros t blk ofs n IN.
pose proof (BB t blk ofs n IN). omega.
Qed.
Lemma mem_block_bound_mono:
forall bnd m bnd',
is_mem_block_bound bnd m ->
bnd <=
bnd' ->
is_mem_block_bound bnd'
m.
Proof.
intros bnd m bnd' MB LE b ofs n k RA.
pose proof (MB b ofs n k RA). omega.
Qed.
Lemma tso_memory_upper_bound_exists:
forall tso,
tso_fin_sup tso ->
exists bb,
tso_memory_upper_bound bb tso.
Proof.
Record is_buffer_ins (
t :
thread_id)
(
b :
list buffer_item)
(
tso tso' :
tso_state) :
Prop :=
mk_is_buffer_ins {
is_buffer_ins_s :
tso'.(
tso_buffers)
t =
tso.(
tso_buffers)
t ++
b;
is_buffer_ins_o :
forall t',
t' <>
t ->
tso'.(
tso_buffers)
t' =
tso.(
tso_buffers)
t';
is_buffer_ins_m :
tso'.(
tso_mem) =
tso.(
tso_mem)}.
Lemma buffer_scratch_ranges_app:
forall b1 b2,
buffer_scratch_ranges b1 ++
buffer_scratch_ranges b2 =
buffer_scratch_ranges (
b1 ++
b2).
Proof.
intros b1 b2.
induction b1 as [|
h b1 IH].
done.
destruct h as [
p c v|
p n []|
p []];
try done.
simpl.
destruct low_mem_restr.
done.
rewrite <-
app_comm_cons.
by rewrite <-
IH.
Qed.
Lemma buffer_scratch_ranges_in:
forall r rs,
In r (
buffer_scratch_ranges (
alloc_items_of_ranges rs)) ->
In r rs.
Proof.
intros r rs.
induction rs as [|[
p n]
rs IH].
done.
simpl.
unfold alloc_item_of_range.
destruct low_mem_restr.
intro.
right.
by apply IH.
simpl.
intros [<- |
IN].
by left.
right.
apply IH,
IN.
Qed.
Lemma range_list_disjoint_buffer_scratch_ranges:
forall rs,
range_list_disjoint rs ->
range_list_disjoint (
buffer_scratch_ranges (
alloc_items_of_ranges rs)).
Proof.
induction rs as [|
h rs IH].
done.
simpl.
intros [
RLD RNI].
specialize (
IH RLD).
destruct (
alloc_item_of_range h)
as [
p c v|
p n []|
p []]
_eqn :
E;
try done.
destruct low_mem_restr.
done.
unfold alloc_item_of_range in E.
destruct h.
inv E.
simpl.
split.
done.
intros r IN.
apply buffer_scratch_ranges_in in IN.
exact (
RNI r IN).
Qed.
Lemma block_bound_scratch_range_bound:
forall bnd b buff ofs n,
block_bound_buff bnd buff ->
In ((
Ptr b ofs),
n) (
buffer_scratch_ranges buff) ->
b <
bnd.
Proof.
intros bnd b buff ofs n.
induction buff as [|
h buff IH].
done.
unfold block_bound_buff in *.
simpl.
intros BBB IN.
apply modusponens in IH.
destruct h as [
p c v|
p n' []|
p k];
try by apply IH.
destruct low_mem_restr.
by apply IH.
simpl in IN.
destruct IN as [
E |
IN].
inv E;
eapply BBB;
eby left.
by apply IH.
intros blk'
ofs'
n'
IN'.
eapply BBB.
eby right.
Qed.
Lemma scratch_allocs_fresh_app:
forall tso sp t rs tso'
bnd,
mem_related_with_partitioning tso.(
tso_mem)
sp ->
scratch_allocs_fresh tso.(
tso_buffers)
sp ->
is_buffer_ins t (
alloc_items_of_ranges rs)
tso tso' ->
(
forall p n,
In (
p,
n)
rs ->
machine_ptr p \/
bnd <=
Ptr.block p) ->
range_list_disjoint rs ->
tso_memory_upper_bound bnd tso ->
scratch_allocs_fresh tso'.(
tso_buffers)
sp.
Proof.
Lemma in_buffer_scratch_ranges:
forall rs p1 n1
(
SC :
scratch_ptr p1)
(
IN :
In (
p1,
n1)
rs),
In (
p1,
n1) (
buffer_scratch_ranges (
alloc_items_of_ranges rs)).
Proof.
induction rs as [|
h rs IH].
done.
intros.
simpl in IN.
destruct IN as [-> |
IN].
simpl.
destruct (
low_mem_restr (
Ptr.block p1))
as []
_eqn :
E.
destruct p1;
simpl in *;
by rewrite SC in *.
apply in_eq.
simpl.
destruct (
alloc_item_of_range h)
as [|
n k [] |];
try eby eapply IH.
destruct low_mem_restr.
eby eapply IH.
simpl.
right.
eby eapply IH.
Qed.
Lemma new_alloc_disjoint:
forall p n tp rs sp
(
RNI :
range_not_in (
p,
n)
tp)
(
MP :
machine_ptr p)
(
INS :
forall (
p' :
pointer) (
n' :
int),
In (
p',
n')
rs ->
range_inside (
p',
n') (
p,
n) \/
scratch_ptr p')
(
RLD :
range_lists_disjoint
(
buffer_scratch_ranges (
alloc_items_of_ranges rs))
sp)
(
PI :
partition_injective tp sp),
range_lists_disjoint rs sp.
Proof.
Lemma parts_disjoint_to_buffers_related:
forall p n tp rs sp
(
RLD:
range_lists_disjoint rs sp)
(
RNI :
range_not_in (
p,
n)
tp)
(
VAR :
valid_alloc_range (
p,
n))
(
DISJ:
range_list_disjoint rs)
(
VARs :
forall r,
In r rs ->
valid_alloc_range r)
(
INS :
forall p'
n',
In (
p',
n')
rs ->
range_inside (
p',
n') (
p,
n) \/
scratch_ptr p'),
buffers_related (
BufferedAlloc p n MObjStack ::
nil)
tp
(
alloc_items_of_ranges rs ::
nil)
sp.
Proof.
intros.
econstructor;
try done. 3 :
econstructor.
intros bi IN.
unfold alloc_items_of_ranges in IN.
apply in_map_iff in IN.
destruct IN as [
r [<-
IN]].
destruct r;
destruct (
INS _ _ IN); [
by right |
by left].
by apply update_buffer_allocs.
Qed.
Lemma allocs_disjoint_to_buffers_related:
forall p n tp rs sp
(
RNI :
range_not_in (
p,
n)
tp)
(
VAR :
valid_alloc_range (
p,
n))
(
DISJ:
range_list_disjoint rs)
(
MP :
machine_ptr p)
(
VARs :
forall r,
In r rs ->
valid_alloc_range r)
(
INS :
forall p'
n',
In (
p',
n')
rs ->
range_inside (
p',
n') (
p,
n) \/
scratch_ptr p')
(
RLD :
range_lists_disjoint (
buffer_scratch_ranges (
alloc_items_of_ranges rs))
sp)
(
PI :
partition_injective tp sp),
buffers_related (
BufferedAlloc p n MObjStack ::
nil)
tp
(
alloc_items_of_ranges rs ::
nil)
sp.
Proof.
Lemma machine_buffer_alloc_items_of_ranges:
forall rs,
machine_buffer (
alloc_items_of_ranges rs).
Proof.
induction rs as [|h rs IH]. done.
intros bi IN.
simpl in IN. destruct IN as [<- | IN].
by destruct h.
by apply IH.
Qed.
Lemma fin_sup_buffer_ins:
forall t b tso tso',
tso_fin_sup tso ->
is_buffer_ins t b tso tso' ->
tso_fin_sup tso'.
Proof.
intros t b tso tso' [
l [
ND FS]]
IBI.
destruct (
In_dec peq t l)
as [
IN |
NIN].
exists l.
split.
done.
intros t'
NIN'.
destruct (
peq t'
t)
as [-> |
N].
done.
rewrite (
is_buffer_ins_o _ _ _ _ IBI); [
by apply FS |
done].
exists (
t ::
l).
split.
by constructor.
intros t'
NIN'.
destruct (
peq t'
t)
as [-> |
N].
elim NIN'.
by left.
rewrite (
is_buffer_ins_o _ _ _ _ IBI); [|
done].
destruct (
In_dec peq t'
l)
as [
IN2 |
NIN2].
elim NIN'.
by right.
by apply FS.
Qed.
Lemma disjoint_allocs_from_alloc_items_of_ranges:
forall rs
(
DISJ:
range_list_disjoint rs)
(
VARs :
forall r,
In r rs ->
valid_alloc_range r),
disjoint_allocs (
alloc_items_of_ranges rs).
Proof.
induction rs as [|[
p n]
rs IH].
done.
intros.
simpl in DISJ.
destruct DISJ as [
DISJ RNI].
split.
apply IH.
done.
intros r IN.
apply VARs,
in_cons,
IN.
intros bi IN.
unfold alloc_items_of_ranges in IN.
apply in_map_iff in IN.
destruct IN as [[
p'
n'] [<-
IN]].
simpl.
apply ranges_disjoint_comm,
RNI,
IN.
Qed.
Definition ranges_valid (
rl :
list arange) :=
forall r,
In r rl ->
valid_alloc_range r.
Lemma ranges_valid_part_update:
forall sp bi sp'
(
RV :
ranges_valid sp)
(
PU :
part_update bi sp =
Some sp'),
ranges_valid sp'.
Proof.
Lemma ranges_valid_part_update_buffer:
forall b sp sp'
(
RV :
ranges_valid sp)
(
PUB:
part_update_buffer b sp =
Some sp'),
ranges_valid sp'.
Proof.
induction b as [|
bi b IH].
intros.
by inv PUB.
intros.
unfold part_update_buffer in *.
simpl in PUB.
destruct (
part_update bi sp)
as [
spi|]
_eqn :
PU;
try done.
simpl in PUB.
eapply IH,
PUB.
eby eapply ranges_valid_part_update.
Qed.
Lemma partition_injective_buffers_related:
forall tb tp tp'
bp sp sp'
(
BR :
buffers_related tb tp bp sp)
(
RV :
ranges_valid sp)
(
PUBt :
part_update_buffer tb tp =
Some tp')
(
PUBs :
part_update_buffer (
flatten bp)
sp =
Some sp')
(
PI :
partition_injective tp sp),
partition_injective tp'
sp'.
Proof.
Lemma scratch_min_block_mptr:
forall tso p bnd,
machine_ptr p ->
tso_memory_upper_bound bnd tso ->
Ptr.block p <
bnd.
Proof.
intros tso p bnd MP (
_ &
_ &
SMB).
destruct p as [
b o].
unfold machine_ptr,
low_mem_restr,
scratch_min_block in *.
destruct (
zeq b 0)
as [-> |
N].
simpl.
omega.
done.
Qed.
Lemma allocs_disjoint_to_unbuffer_safe:
forall ttso tthr stso sthr bp sp tp t ttso'
stso'
p n rs bnd tp'
(
TC :
Comp.consistent tso_mm cst_sem (
ttso,
tthr))
(
USt :
unbuffer_safe ttso')
(
TREL:
tso_pc_related_witt (
ttso,
tthr) (
stso,
sthr)
bp tp sp)
(
PUt :
part_update_buffer (
tso_buffers ttso t ++
BufferedAlloc p n MObjStack ::
nil)
(
tp t) =
Some ((
p,
n) ::
tp'))
(
VAR :
valid_alloc_range (
p,
n))
(
DISJ:
range_list_disjoint rs)
(
MP :
machine_ptr p)
(
VARs:
forall r,
In r rs ->
valid_alloc_range r)
(
TSOBND:
tso_memory_upper_bound bnd stso)
(
INS :
forall p'
n',
In (
p',
n')
rs ->
range_inside (
p',
n') (
p,
n) \/
bnd <=
Ptr.block p')
(
BAt :
is_buffer_ins t (
BufferedAlloc p n MObjStack ::
nil)
ttso ttso')
(
BAs :
is_buffer_ins t (
alloc_items_of_ranges rs)
stso stso'),
unbuffer_safe stso'.
Proof.
Lemma memory_neutral_sim:
forall ttso tthr stso sthr ts ss ts'
ss'
t,
tso_pc_related (
ttso,
tthr) (
stso,
sthr) ->
tthr !
t =
Some ts ->
sthr !
t =
Some ss ->
(
forall tp sp sm,
state_related tp sp sm ts ss ->
state_related tp sp sm ts'
ss') ->
state_consistent_with_env ts' ->
tso_pc_related (
ttso,
tthr !
t <-
ts')
(
stso,
sthr !
t <-
ss').
Proof.
intros ttso tthr stso sthr ts ss ts'
ss'
t
[[
BCt USt] [
bp [
tp [
sp TSOREL]]]]
TS SS THRR SCE.
destruct TSOREL as (
MTB &
NSMR &
MCR &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL).
split.
eby eapply Comp.thread_update_preserves_consistency.
exists bp;
exists tp;
exists sp.
repeat (
split; [
done|]).
split.
eby eapply Comp.thread_update_preserves_consistency.
repeat (
split; [
done|]).
intro t'.
destruct (
TREL t')
as (
PI &
BR &
BOR).
repeat (
split; [
done|]).
simpl in *.
destruct (
peq t'
t)
as [-> |
N].
rewrite !
PTree.gss.
rewrite TS,
SS in BOR.
simpl in *.
destruct BOR as [
smt [
spt [
tpt (
AB &
PUBt &
PUBs &
SR &
SCO)]]].
exists smt.
exists spt.
exists tpt.
do 3 (
split; [
done|]).
split.
by apply THRR.
done.
by rewrite !
PTree.gso.
Qed.
Lemma alloc_steps_appD:
forall {
l1 l2 s s'}
(
AS :
alloc_steps s (
l1 ++
l2)
s'),
exists si,
alloc_steps s l1 si /\
alloc_steps si l2 s'.
Proof.
induction l1 as [|
h l1 IH];
simpl;
intros.
by eexists;
vauto.
inv AS.
destruct (
IH _ _ _ AS0)
as [
s'' [
AS1 AS2]].
eby eexists;
split; [
eapply alloc_steps_step|].
Qed.
Lemma alloc_steps_buffer:
forall ss thrs tso t rs ss'
(
AS :
alloc_steps ss rs ss')
(
STt :
thrs !
t =
Some ss)
(
USi :
unbuffer_safe (
buffer_insert_list t (
alloc_items_of_ranges rs)
tso)),
exists thrs',
taustar cshm_lts (
tso,
thrs)
(
buffer_insert_list t (
alloc_items_of_ranges rs)
tso,
thrs') /\
thrs' !
t =
Some ss' /\
(
forall t',
t' <>
t ->
thrs' !
t' =
thrs !
t').
Proof.
Lemma unbuffer_safe_buffer_insert_low_mp:
forall tso t p n k
(
M :
mrestr tso.(
tso_mem) =
low_mem_restr)
(
US :
unbuffer_safe (
buffer_insert tso t (
BufferedAlloc p n k))),
machine_ptr p /\
valid_alloc_range (
p,
n).
Proof.
Lemma is_buffer_ins_buffer_insert_list:
forall t b tso,
is_buffer_ins t b tso (
buffer_insert_list t b tso).
Proof.
Lemma is_buffer_ins_buffer_insert:
forall t bi tso,
is_buffer_ins t (
bi ::
nil)
tso (
buffer_insert tso t bi).
Proof.
Lemma empty_envs_items_rel:
forall fsize sm p,
env_items_related (
Int.repr fsize)
sm
(
mkcstenv p fsize (
PTree.empty env_item))
empty_env.
Proof.
Lemma empty_env_local_cons_with_ids:
forall ids,
local_cons_with_ids (
PTree.empty env_item)
ids.
Proof.
Lemma part_update_buffer_alloc_items_of_ranges:
forall {
rs sp sp'}
(
PUB :
part_update_buffer (
alloc_items_of_ranges rs)
sp =
Some sp'),
sp' =
rev rs ++
sp.
Proof.
unfold part_update_buffer.
induction rs as [|(
p,
n)
rs IH];
intros;
simpl in *.
by inv PUB.
destruct valid_alloc_range_dec; [|
done].
destruct range_in_dec.
done.
simpl in PUB.
rewrite (
IH _ _ PUB).
by rewrite app_ass.
Qed.
Lemma cons_to_app:
forall {
A} {
e:
A}
l,
e ::
l = (
e ::
nil) ++
l.
Proof.
done. Qed.
Lemma allocs_mem_agrees_on_scratch:
forall rs m m'
sp
(
AB :
apply_buffer (
alloc_items_of_ranges rs)
m =
Some m')
(
SPAL:
forall r,
In r sp ->
range_allocated r MObjStack m),
mem_agrees_on_scratch m m'
sp.
Proof.
Lemma allocs_mem_agrees_on_scratch_mrwp:
forall part part'
part''
m m'
m''
b rs t
(
MRWP:
mem_related_with_partitioning m part)
(
AB :
apply_buffer b m =
Some m')
(
PUB :
part_update_buffer b (
part t) =
Some part')
(
SUB :
forall r,
In r part'' ->
In r part')
(
AB' :
apply_buffer (
alloc_items_of_ranges rs)
m' =
Some m''),
mem_agrees_on_scratch m'
m''
part''.
Proof.
Lemma alloc_sim:
forall s s'
p n k (
st :
PTree.t Cstacked.state)
t tso csms
(
ST :
cst_step cst_globenv s (
TEmem (
MEalloc p n k))
s')
(
CS :
st !
t =
Some s)
(
USt :
unbuffer_safe (
buffer_insert tso t (
BufferedAlloc p n k)))
(
TSOPCREL :
tso_pc_related (
tso,
st)
csms),
can_reach_error csm_globenv csms \/
(
exists shms',
taustep cshm_lts csms Etau shms' /\
tso_pc_related (
buffer_insert tso t (
BufferedAlloc p n k),
st !
t <-
s')
shms').
Proof.
intros.
destruct csms as [
cstso csst].
generalize TSOPCREL;
intros [
TC [
bp [
tp [
sp TRELW]]]].
pose proof (
tso_pc_related_to_buff_states _ _ _ _ _ _ _ _ t TRELW)
as BOR.
pose proof TRELW as (
MTB &
NSMR & (
MCRt &
MCRs &
LR) &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL).
simpl in *.
rewrite CS in BOR.
destruct (
csst !
t)
as [
ss'|]
_eqn :
Ess';
simpl in BOR;
try done.
destruct BOR as [
sm' [
sp' [
tp' (
AB' &
PUBt &
PUBs &
SR &
SCO)]]].
assert (
SCO' :=
step_consistent_with_env ST SCO).
assert (
TC' :
Comp.consistent tso_mm cst_sem
(
buffer_insert tso t (
BufferedAlloc p n k),
st !
t <-
s')).
eapply Comp.step_preserves_consistency.
econstructor;
try edone;
eby econstructor.
done.
inv ST.
inv SR.
exploit (
unbuffer_safe_partition_alloc_pub _ (
tso_buffers tso t)
_ t p
(
Int.repr fsize)
tp'
USt MRPt).
by simpl;
rewrite tupdate_s.
done.
intro PUBtn.
assert (
RNIt:
range_not_in (
p, (
Int.repr fsize))
tp').
eapply unbuffer_safe_partition_alloc.
apply USt.
apply MRPt. 2 :
apply PUBt.
simpl.
rewrite tupdate_s.
done.
assert (
FINP :
exists p,
Genv.find_funct (
Cstacked.ge cst_globenv)
p =
Some (
Internal f)).
by inv KR.
assert (
KS :
exists csm_e,
exists csm_k0,
csm_k =
Kcall optid (
Internal f)
csm_e csm_k0).
eby inv KR;
eexists;
eexists.
destruct KS as [
csm_e [
csm_k0 KS]].
assert (
FS :=
TSO.tso_cons_impl_fin_sup _ _ SC).
destruct (
tso_memory_upper_bound_exists _ FS)
as [
bnd TSOUB].
unfold build_env in BE.
destruct FINP as [
fp FINP].
assert (
LIM :=
function_stacksize_limit _ _
(
PMap.init Var_global_array)
FINP).
destruct (
build_compilenv (
PMap.init Var_global_array)
f)
as [
cenv fsz]
_eqn :
Ebce.
destruct (
build_envmap (
fn_variables f)
cenv (
PTree.empty env_item))
as [
e|]
_eqn :
Ee; [|
done].
inv BE.
pose proof (
unbuffer_safe_buffer_insert_low_mp _ _ _ _ _ MCRt USt)
as [
MP VAR].
assert (
PBND :=
scratch_min_block_mptr _ _ _ MP TSOUB).
unfold build_compilenv in Ebce.
simpl in LIM.
destruct (
ranges_of_vars_succ _ _ _ 0
_ _ _ _ ND PBND Ebce
(
Zle_refl _)
LIM (
or_introl _ VAR))
as [
rs (
ROV &
RLD &
VARs &
INOSCR)].
assert(
USsi:
unbuffer_safe (
buffer_insert_list t (
alloc_items_of_ranges rs)
cstso)).
apply(
allocs_disjoint_to_unbuffer_safe _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
TC USt TRELW PUBtn VAR RLD MP VARs TSOUB).
intros p'
n'
IN'.
destruct (
INOSCR _ IN')
as [[
RI _] |
O].
by left.
right.
simpl in O.
omega.
apply is_buffer_ins_buffer_insert.
apply is_buffer_ins_buffer_insert_list.
assert (
ABs :=
no_unbuffer_errors _ t USsi).
rewrite buffer_insert_list_s,
buffer_insert_list_m,
apply_buffer_app,
AB'
in ABs.
simpl in ABs.
destruct (
apply_buffer (
alloc_items_of_ranges rs)
sm')
as [
sm''|]
_eqn:
ABs'';
[|
done].
destruct (
buffer_alloc_env_related csm_e f optid
_ _ _ _ _ _ vs csm_k0 _ _ empty_env
_ _ _ _ _ _ ROV ABs''
Ee ND PBND (
proj2 (
proj2 TSOUB))
Ebce (
Zle_refl _)
LIM (
or_introl _ VAR) (
refl_equal _) (
empty_envs_items_rel _ _ _)
(
empty_env_local_cons_with_ids _))
as (
ASTEPS &
ITSREL &
LC).
unfold mkcstenv in ITSREL.
destruct (
zeq fsize 0); [
done|].
destruct (
alloc_steps_buffer _ _ _ _ _ _ ASTEPS (
PTree.gss _ _ csst)
USsi)
as [
sthrs' (
TAUa &
NSa &
OSa)].
set (
ntso :=
buffer_insert_list t (
alloc_items_of_ranges rs)
cstso).
set (
nthr :=
sthrs' !
t <-
(
SKbind f vs (
map (@
fst _ _) (
fn_params f))
(
build_csm_env (
fn_variables f)
cenv bnd p empty_env)
(
Kcall optid (
Internal f)
csm_e csm_k0))).
assert(
WS :
taustep cshm_lts (
cstso,
csst)
Etau (
ntso,
nthr)).
eapply (@
steptau_taustar_taustep _ cshm_lts _ (
_,
_)).
simpl.
eapply Comp.step_tau;
try edone;
vauto; [].
eapply StepFunctionInternal;
try edone; [].
unfold fn_variables in ND.
unfold fst in ND.
rewrite !@
map_app,
map_map in ND.
apply ND.
eapply taustar_trans.
apply TAUa.
apply steptau_taustar.
simpl.
by eapply Comp.step_tau;
try edone;
vauto.
assert (
SAF' :
scratch_allocs_fresh (
tso_buffers ntso)
sp).
eapply scratch_allocs_fresh_app;
try edone.
apply is_buffer_ins_buffer_insert_list.
intros p'
n'
IN'.
destruct (
INOSCR (
p',
n')
IN')
as [[
RI _] |
BND].
left.
by destruct p';
destruct p;
destruct RI as [->
_].
right.
simpl in *.
omega.
assert (
RLDrssp :
range_lists_disjoint rs sp').
destruct (
TREL t)
as (
PIt' &
BRt' &
_).
eapply new_alloc_disjoint;
try edone.
intros p'
n'
IN'.
destruct (
INOSCR _ IN').
by left;
tauto.
destruct (
machine_or_scratch p')
as [
MP'|
SC'].
pose proof (
scratch_min_block_mptr _ _ _ MP'
TSOUB).
simpl in *.
omegaContradiction.
by right.
exploit (
scratch_allocs_fresh_apply_buffer _ _ _ ntso.(
tso_buffers)
(
tupdate t (
alloc_items_of_ranges rs)
ntso.(
tso_buffers))
_ PUBs);
unfold ntso.
by rewrite buffer_insert_list_s,
BPD,
tupdate_s.
intros t'
N.
by rewrite tupdate_o.
done.
intros (
_ &
_ &
RLDP).
specialize (
RLDP t t).
eby rewrite tupdate_s,
update_partitioning_s in RLDP.
eapply partition_injective_buffers_related;
try edone.
intros r IN.
assert (
range_allocated r MObjStack cstso.(
tso_mem)).
apply -> (
proj2 (
proj2 MRPs)).
eby eexists.
eby eapply allocated_range_valid.
eby rewrite <-
BPD.
assert (
BRt :
buffers_related
(
tso_buffers tso t ++
BufferedAlloc p (
Int.repr fsize)
MObjStack ::
nil)
(
tp t) (
bp t ++
alloc_items_of_ranges rs ::
nil)
(
sp t)).
destruct (
TREL t)
as (
PIt' &
BRt' &
_).
eapply buffers_related_suffix;
try edone.
eapply parts_disjoint_to_buffers_related;
try edone.
intros p'
n'
IN'.
destruct (
INOSCR _ IN').
by left;
tauto.
destruct (
machine_or_scratch p')
as [
MP'|
SC'].
pose proof (
scratch_min_block_mptr _ _ _ MP'
TSOUB).
simpl in *.
omegaContradiction.
by right.
eby rewrite <-
BPD.
assert (
NErsnil :
rs <>
nil).
destruct (
fn_variables f).
simpl in *.
inv Ebce.
done.
destruct p0 as [? []];
simpl in ROV;
destruct (
cenv !!
i);
try done;
destruct ranges_of_vars;
try done;
injection ROV;
by intros <-.
end_assert NErsnil.
right.
eexists (
_,
_).
split.
apply WS.
split.
done.
exists (
tupdate t (
bp t ++ (
alloc_items_of_ranges rs ::
nil))
bp).
exists tp.
exists sp.
unfold ntso,
nthr.
split;
simpl.
intro t'.
destruct (
peq t'
t)
as [-> |
N].
rewrite buffer_insert_list_s.
intros bi IN.
apply in_app_or in IN.
destruct IN.
eby eapply MTB.
eby eapply machine_buffer_alloc_items_of_ranges.
rewrite buffer_insert_list_o; [
apply MTB | ];
done.
split.
by rewrite buffer_insert_list_m.
split.
by rewrite buffer_insert_list_m.
split.
eapply Comp.taustep_preserves_consistency.
apply WS.
done.
split.
intro t'.
destruct (
peq t'
t)
as [-> |
N].
rewrite buffer_insert_list_s,
tupdate_s.
rewrite flatten_app.
simpl.
rewrite <-
app_nil_end,
BPD.
done.
by rewrite buffer_insert_list_o,
tupdate_o,
BPD.
split.
intros t'
bi IN.
destruct (
peq t'
t)
as [-> |
N].
rewrite tupdate_s in IN.
apply in_app_or in IN.
destruct IN as [
IN | [<- |
IM]].
eby eapply BNE.
by destruct rs.
done.
rewrite tupdate_o in IN.
eby eapply BNE.
done.
split.
done.
split.
done.
split.
by rewrite buffer_insert_list_m.
intros t'.
destruct (
TREL t')
as (
PI &
BR &
BSR).
split.
done.
split.
destruct (
peq t'
t)
as [-> |
N].
rewrite !@
tupdate_s.
done.
by rewrite !@
tupdate_o.
destruct (
peq t'
t)
as [-> |
N].
rewrite !@
tupdate_s, !@
PTree.gss.
simpl.
rewrite buffer_insert_list_m.
destruct (
buffers_related_part_update BRt)
as [
_ [
sps PUBs']].
unfold part_update_buffer in *.
rewrite flatten_app,
fold_left_opt_app, <-
BPD,
PUBs in PUBs'.
simpl in PUBs'.
rewrite <-
app_nil_end in PUBs'.
rewrite (
part_update_buffer_alloc_items_of_ranges PUBs')
in PUBs'.
eexists.
eexists.
eexists.
split.
rewrite flatten_app, <-
BPD,
apply_buffer_app,
AB'.
simpl.
rewrite <-
app_nil_end.
edone.
split.
edone.
split.
unfold part_update_buffer.
rewrite flatten_app,
fold_left_opt_app, <-
BPD,
PUBs.
simpl.
rewrite <-
app_nil_end.
edone.
rewrite cons_to_app.
split; [|
done].
eapply st_rel_bind.
eapply cont_related_load_inv.
edone.
eapply allocs_mem_agrees_on_scratch_mrwp;
try edone;
intros r IN;
apply in_or_app;
by right.
exists (
Int.repr fsize).
split.
repeat (
split; [
done|]).
destruct rs.
done.
simpl.
intro E.
eby eapply app_cons_not_nil,
sym_eq.
split.
apply range_list_disjoint_perm with (
l :=
rs).
apply Permutation_rev.
done.
split.
eapply Permutation_trans.
apply Permutation_sym,
Permutation_rev.
eapply env_ranges_permut_range_of_vars.
edone.
edone.
done.
done.
done.
intros r1 IN1 r2 IN2.
destruct IN2 as [<- | ?]; [|
done].
by apply ranges_disjoint_comm,
RNIt.
intros r1 IN1 r2 IN2.
apply In_rev in IN2.
apply ranges_disjoint_comm.
eby eapply RLDrssp.
rewrite !@
tupdate_o,
buffer_insert_list_m, !@
PTree.gso;
try done.
by rewrite OSa,
PTree.gso.
Qed.
End ALLOC_SIMS.