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 FREEWRITE_SIM.
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 globenv_machine:
forall id p,
Genv.find_symbol (
Cstacked.ge cst_globenv)
id =
Some p ->
machine_ptr p.
Hypothesis globenv_same:
Genv.genv_match (
fun a b =>
a =
b) (
Cstacked.ge cst_globenv) (
ge csm_globenv) /\
Cstacked.gvare cst_globenv =
gvare csm_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 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).
Notation unbuffer_item_preserves_tso_pc_unsafe :=
(
unbuffer_item_preserves_tso_pc_unsafe cst_globenv).
Notation tso_pc_related_to_buff_states :=
(
tso_pc_related_to_buff_states cst_globenv).
Definition writes_or_frees (
b :
list buffer_item) :=
forall bi,
In bi b ->
match bi with
|
BufferedFree _ _ =>
True
|
BufferedWrite _ _ _ =>
True
|
_ =>
False
end.
Lemma tso_pc_related_unsafe_store_sim:
forall ts tthr ss sthr t p c v tbr,
tso_pc_unsafe_related (
ts,
tthr) (
ss,
sthr) ->
ts.(
tso_buffers)
t =
BufferedWrite p c v ::
tbr ->
store_ptr c ts.(
tso_mem)
p v <>
None.
Proof.
intros ts tthr ss sthr t p c v tbr TREL TB WR.
destruct TREL as [
bp [
tp [
sp (
MTB &
NSMR & (
MCRt &
MCRs &
LR) &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL)]]].
destruct (
TREL t)
as (
_ &
BRELt &
_).
simpl in *.
remember (
tso_buffers ts t)
as tbt.
remember (
tp t)
as tpt.
remember (
bp t)
as bpt.
remember (
sp t)
as spt.
destruct BRELt;
try done.
inv TB.
pose proof (
BPD t)
as BPt.
rewrite <-
Heqbpt in BPt.
simpl in BPt.
destruct (
unbuffer_unbuffer_safe (
proj2 SC)
BPt)
as [
sm' [
ABI _]].
unfold apply_buffer_item,
fst in ABI.
pose proof (
store_chunk_allocated_spec c (
tso_mem ss)
p v)
as SS.
rewrite ABI in SS.
destruct SS as [[
r' [
k' [
RI RA]]]
PCAL].
pose proof (
store_chunk_allocated_spec c (
tso_mem ts)
p v)
as STS.
rewrite WR in STS.
elim STS;
clear STS;
split; [|
done].
destruct k'
as []
_eqn :
Ek';
try by specialize (
NSMR r'
k');
rewrite Ek'
in NSMR;
apply NSMR in RA;
exists r';
eexists;
split;
edone.
destruct BIIR as [
MP _].
destruct r'
as [
p'
n'].
assert (
MP':
machine_ptr p').
destruct p;
destruct p';
destruct RI as [->
_];
by simpl in *.
apply (
proj2 (
proj2 MRPs))
in RA.
destruct RA as [
t'
IN].
destruct (
proj1 (
TREL t')
_ _ MP'
IN)
as [
rt [
RIt INt]].
exists rt.
exists MObjStack.
split.
eby eapply range_inside_trans.
apply (
proj2 (
proj2 MRPt)
rt).
eby eexists.
Qed.
Lemma tso_pc_related_unsafe_free_sim:
forall ts tthr ss sthr t p k tbr,
tso_pc_unsafe_related (
ts,
tthr) (
ss,
sthr) ->
ts.(
tso_buffers)
t =
BufferedFree p k ::
tbr ->
free_ptr p k ts.(
tso_mem) <>
None.
Proof.
intros ts tthr ss sthr t p k tbr TREL TB FR.
destruct TREL as [
bp [
tp [
sp (
MTB &
NSMR & (
MCRt &
MCRs &
LR) &
SC &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL)]]].
destruct (
TREL t)
as (
_ &
BRELt &
_).
simpl in *.
remember (
tso_buffers ts t)
as tbt.
remember (
tp t)
as tpt.
remember (
bp t)
as bpt.
remember (
sp t)
as spt.
destruct BRELt;
try done.
inv TB.
assert (
RA:
range_allocated (
p,
n)
MObjStack (
tso_mem ts)).
apply (
proj2 (
proj2 MRPt) (
p,
n)).
exists t.
rewrite <-
Heqtpt.
apply in_eq.
pose proof (
free_cond_spec p MObjStack (
tso_mem ts))
as FS.
rewrite FR in FS.
eby eapply FS.
inv TB.
pose proof (
BPD t)
as BPt.
rewrite <-
Heqbpt in BPt.
simpl in BPt.
destruct (
unbuffer_unbuffer_safe (
proj2 SC)
BPt)
as [
sm' [
ABI _]].
unfold apply_buffer_item,
fst in ABI.
pose proof (
free_cond_spec p k (
tso_mem ss))
as FS.
rewrite ABI in FS.
destruct FS as [
n RA].
assert (
RAt:
range_allocated (
p,
n)
k (
tso_mem ts)).
by destruct k as []
_eqn :
Ek;
simpl in BIIR;
try done;
specialize (
NSMR (
p,
n)
k);
rewrite Ek in NSMR;
apply NSMR in RA.
pose proof (
free_cond_spec p k (
tso_mem ts))
as FS.
rewrite FR in FS.
eby eapply FS.
Qed.
Lemma unbuffer_safety_rev_write_free_gen:
forall t ts tthr ts'
ss sthr fw,
tso_fin_sup ts ->
tso_pc_unsafe_related (
ts,
tthr) (
ss,
sthr) ->
mrestr ts'.(
tso_mem) =
low_mem_restr ->
unbuffer_safe ts' ->
writes_or_frees fw ->
ts.(
tso_buffers)
t =
ts'.(
tso_buffers)
t ++
fw ->
(
forall t',
t' <>
t ->
ts.(
tso_buffers)
t' =
ts'.(
tso_buffers)
t') ->
(
forall r k,
range_allocated r k ts.(
tso_mem) ->
range_allocated r k ts'.(
tso_mem)) ->
unbuffer_safe ts.
Proof.
Inductive free_steps :
Csharpminor.state ->
list pointer ->
Csharpminor.state ->
Prop :=
|
free_steps_refl:
forall s,
free_steps s nil s
|
free_steps_step:
forall s s'
s''
p ps
(
STEP :
cs_step csm_globenv s (
TEmem (
MEfree p MObjStack))
s')
(
FS :
free_steps s'
ps s''),
free_steps s (
p ::
ps)
s''.
Tactic Notation "
free_steps_cases"
tactic(
first)
tactic(
c) :=
first; [
c "
free_steps_refl" |
c "
free_steps_step"].
Definition free_item_of_ptr (
p :
pointer) :=
BufferedFree p MObjStack.
Lemma kfree_free_steps:
forall ps v k e,
free_steps (
SKstmt Sskip e (
Kfree ps v k))
ps
(
SKstmt Sskip e (
Kfree nil v k)).
Proof.
by induction ps as [|p ps IH]; intros; econstructor;
[econstructor | apply IH].
Qed.
Lemma taustar_ne_taustep:
forall {
lbls lts}
s s'
(
TAU :
taustar lts s s')
(
NE :
s <>
s'),
taustep lts s (
tau lbls)
s'.
Proof.
Lemma free_steps_appD:
forall {
l1 l2 s s'}
(
FS :
free_steps s (
l1 ++
l2)
s'),
exists si,
free_steps s l1 si /\
free_steps si l2 s'.
Proof.
induction l1 as [|
h l1 IH];
intros.
simpl in FS.
exists s.
split.
constructor.
done.
rewrite <-
app_comm_cons in FS.
inv FS.
destruct (
IH _ _ _ FS0)
as [
s'' [
FS1 FS2]].
eexists.
split.
eby eapply free_steps_step.
edone.
Qed.
Lemma free_steps_success:
forall s ps s'
thrs t tso tso'
(
FS :
free_steps s ps s')
(
CS :
thrs !
t =
Some s)
(
Etso' :
tso' =
buffer_insert_list t (
map free_item_of_ptr ps)
tso)
(
US :
unbuffer_safe tso'),
exists thrs',
taustar cshm_lts (
tso,
thrs) (
tso',
thrs') /\
thrs' !
t =
Some s' /\
forall t',
t' <>
t ->
thrs' !
t' =
thrs !
t'.
Proof.
Lemma fin_sup_buffer_insert_list:
forall t b tso,
tso_fin_sup tso ->
tso_fin_sup (
buffer_insert_list t b tso).
Proof.
Lemma free_steps_fail:
forall s ps s'
thrs t tso tso'
(
TC :
Comp.consistent tso_mm cs_sem (
tso,
thrs))
(
FS :
free_steps s ps s')
(
CS :
thrs !
t =
Some s)
(
Etso' :
tso' =
buffer_insert_list t (
map free_item_of_ptr ps)
tso)
(
NUS' : ~
unbuffer_safe tso'),
can_reach_error csm_globenv (
tso,
thrs).
Proof.
Lemma range_remove_app:
forall p l1 l1'
l2,
In p (
map (@
fst _ _)
l1) ->
range_remove p l1 =
l1' ->
range_remove p (
l1 ++
l2) =
l1' ++
l2.
Proof.
intro p.
induction l1 as [|[
p'
n']
l1 IH];
intros l1'
l2 IN RR.
done.
simpl in *.
destruct (
Ptr.eq_dec p'
p)
as [-> |
N].
by subst.
erewrite IH.
rewrite <-
RR;
reflexivity.
by destruct IN.
done.
Qed.
Lemma in_range_remove_decomp:
forall p sp,
In p (
map (@
fst _ _)
sp) ->
exists l1,
exists l2,
exists n,
sp =
l1 ++ (
p,
n) ::
l2 /\
range_remove p sp =
l1 ++
l2.
Proof.
intros p sp.
induction sp as [|[
p'
n']
sp IH];
intro IN.
done.
simpl in IN.
destruct (
Ptr.eq_dec p'
p)
as [-> |
N].
exists nil.
exists sp.
exists n'.
simpl.
by destruct Ptr.eq_dec.
destruct IN as [-> |
IN].
done.
destruct (
IH IN)
as [
l1 [
l2 [
n [
Esp Err]]]].
exists ((
p',
n') ::
l1).
exists l2.
exists n.
simpl.
destruct Ptr.eq_dec.
done.
rewrite Err,
Esp.
done.
Qed.
Lemma pointer_in_range_list_false:
forall l p n'
(
PIRL:
pointer_in_range_list p l =
false),
~
In (
p,
n')
l.
Proof.
induction l as [|[
hp hn]
l IH];
intros;
intro IN.
done.
simpl in IN;
destruct IN as [
E |
IN]; [
inv E|];
simpl in PIRL;
destruct Ptr.eq_dec;
try done;
eby eapply IH.
Qed.
Lemma part_update_buffer_free:
forall {
ps sp}
sp'
(
PERM:
Permutation (
map (@
fst _ _)
sp)
ps),
part_update_buffer (
map free_item_of_ptr ps) (
sp ++
sp') =
Some sp'.
Proof.
Lemma machine_buffer_free_items_of_ptrs:
forall ps,
machine_buffer (
map free_item_of_ptr ps).
Proof.
induction ps as [|h rs IH]. done.
intros bi IN.
simpl in IN. destruct IN as [<- | IN].
by destruct h.
by apply IH.
Qed.
Lemma buffer_scratch_ranges_app_free:
forall b ps,
buffer_scratch_ranges b =
buffer_scratch_ranges (
b ++
map free_item_of_ptr ps).
Proof.
intros.
induction b.
simpl. by induction ps.
simpl. by rewrite <- IHb.
Qed.
Lemma scratch_allocs_fresh_free:
forall tso sp ps t
(
SAF :
scratch_allocs_fresh tso.(
tso_buffers)
sp),
scratch_allocs_fresh
(
tso_buffers (
buffer_insert_list t (
map free_item_of_ptr ps)
tso))
sp.
Proof.
Lemma update_part_buffer_valid_alloc_range:
forall tso t sp sp'
r
(
US :
unbuffer_safe tso)
(
PUB :
part_update_buffer (
tso_buffers tso t) (
sp t) =
Some sp')
(
MRWP :
mem_related_with_partitioning tso.(
tso_mem)
sp)
(
IN :
In r sp'),
valid_alloc_range r.
Proof.
Lemma update_part_buffer_mrestr:
forall tso t sp sp'
p n
(
US :
unbuffer_safe tso)
(
PUB :
part_update_buffer (
tso_buffers tso t) (
sp t) =
Some sp')
(
MRWP :
mem_related_with_partitioning tso.(
tso_mem)
sp)
(
IN :
In (
p,
n)
sp'),
mrestr tso.(
tso_mem) (
Ptr.block p).
Proof.
Lemma env_ranges_exists:
forall r e,
In r (
env_ranges e) ->
exists id,
exists ei,
e !
id =
Some ei /\
csm_env_item_range ei =
r.
Proof.
intros r e IN.
unfold env_ranges in IN.
apply in_map_iff in IN.
simpl in IN.
destruct IN as [[
id ei] [
CEIR INelems]].
eexists;
eexists;
split.
eby apply PTree.elements_complete.
done.
Qed.
Lemma related_env_partitions_injective:
forall csal cmal vals cse cme,
env_related csal cmal vals cse cme ->
partition_injective csal cmal.
Proof.
Lemma partition_injective_app:
forall sp1 sp2 tp1 tp2,
partition_injective sp1 tp1 ->
partition_injective sp2 tp2 ->
partition_injective (
sp1 ++
sp2) (
tp1 ++
tp2).
Proof.
intros sp1 sp2 tp1 tp2 PI1 PI2 p n MPTR IN.
destruct (
in_app_or _ _ _ IN)
as [
IN1 |
IN2].
destruct (
PI1 _ _ MPTR IN1)
as [
r' [
RI INt]].
exists r'.
split.
done.
by apply in_or_app;
left.
destruct (
PI2 _ _ MPTR IN2)
as [
r' [
RI INt]].
exists r'.
split.
done.
by apply in_or_app;
right.
Qed.
Lemma related_cont_partitions_injective:
forall tal sal smem tk sk,
cont_related tal sal smem tk sk ->
partition_injective tal sal.
Proof.
Lemma frees_mem_agrees_on_scratch:
forall lp m m'
sp
(
AB :
apply_buffer (
map free_item_of_ptr lp)
m =
Some m')
(
SPAL:
forall r,
In r sp ->
range_allocated r MObjStack m'),
mem_agrees_on_scratch m m'
sp.
Proof.
Lemma free_sim_aux:
forall s s'
p k (
st :
PTree.t Cstacked.state)
t tso cstso
(
csst :
PTree.t Csharpminor.state)
csm_e lp v csm_k
(
ST :
cst_step cst_globenv s (
TEmem (
MEfree p k))
s')
(
CS :
st !
t =
Some s)
(
Ess' :
csst !
t =
Some (
SKstmt Sskip csm_e (
Kfree lp v csm_k)))
(
USi :
unbuffer_safe (
buffer_insert_list t (
map free_item_of_ptr lp)
cstso))
(
TSOPCREL :
tso_pc_related (
tso,
st) (
cstso,
csst)),
can_reach_error csm_globenv (
cstso,
csst) \/
(
exists shms' :
St cshm_lts,
taustep cshm_lts (
cstso,
csst)
Etau shms' /\
tso_pc_unsafe_related (
buffer_insert tso t (
BufferedFree p k),
st !
t <-
s')
shms').
Proof.
intros.
pose proof TSOPCREL as [
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 &
MCM) &
TCs &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL).
simpl in *.
pose proof TCs as [
BCs USs].
rewrite CS in BOR.
rewrite Ess'
in BOR.
destruct BOR as [
sm' [
sp' [
tp' (
AB' &
PUBt &
PUBs &
SR &
SCO)]]].
assert (
SCO' :=
step_consistent_with_env ST SCO).
inv ST.
inv SR.
destruct cst_obs'
as [|[
px n] []];
destruct OP as [
CSB CMB];
try done; [].
inv CSB.
assert (
FS :=
kfree_free_steps lp v csm_k csm_e).
right.
destruct (
free_steps_success _ _ _ _ _ _ _ FS Ess' (
refl_equal _)
USi)
as [
thrs' (
TAU' &
CS' &
OS')].
eexists (
_,
_).
assert(
NElpnil :
lp <>
nil).
destruct lp.
pose proof (
Permutation_nil (
Permutation_sym P)).
by destruct csm_obs'.
done.
end_assert NElpnil.
assert(
WS :
taustep cshm_lts
(
cstso,
csst)
Etau
(
buffer_insert_list t (
map free_item_of_ptr lp)
cstso,
thrs')).
eapply (
taustar_ne_taustep _ _ TAU').
by intro X;
injection X;
simpl in *;
intros E1 _;
rewrite E1,
CS'
in Ess';
inv Ess'.
end_assert WS.
assert (
PUBf :=
part_update_buffer_free csm_obs P).
assert (
BRt :
buffers_related
(
tso_buffers tso t ++
BufferedFree p MObjStack ::
nil)
(
tp t) (
bp t ++ (
map free_item_of_ptr lp ::
nil))
(
sp t)).
destruct (
TREL t)
as (
PIt' &
BRt' &
_).
eapply buffers_related_suffix;
try edone.
2 :
eby rewrite <-
BPD.
econstructor;
try eby vauto.
intros bi IN.
apply in_map_iff in IN.
destruct IN as [
p' [
Ebi IN]].
apply (
Permutation_in _ (
Permutation_sym P))
in IN.
apply in_map_iff in IN.
destruct IN as [[
pr nr] [
Ep'
INr]].
simpl in Ep';
subst.
specialize (
PI p'
nr).
destruct p';
unfold machine_ptr in PI.
simpl.
destruct (
low_mem_restr z).
destruct (
PI (
refl_equal _)
INr)
as [
r' [
RI INr']].
destruct INr'
as [<- | ]; [|
done].
right.
destruct p.
unfold range_inside in RI.
exploit update_part_buffer_valid_alloc_range.
apply USs.
edone.
edone.
apply in_or_app.
eby left.
unfold valid_alloc_range.
omega.
by left.
intros [
pr pn]
IN.
pose proof (
related_cont_partitions_injective _ _ _ _ _ KR)
as PIC.
specialize (
PIC pr pn).
destruct (
machine_or_scratch pr)
as [
Mpr |
Spr].
destruct (
PIC Mpr IN)
as [
r' [
RIr'
INr']].
eapply disjoint_inside_disjoint. 2 :
apply RIr'.
eapply CSRLD; [
done |
by apply in_eq].
eapply ranges_disjoint_comm,
machine_scratch_disjoint.
replace (
machine_ptr p)
with (
low_mem_restr (
Ptr.block p) =
true);
[|
by destruct p].
rewrite <-
MCRt.
eby destruct TC;
eapply update_part_buffer_mrestr;
try apply in_eq.
done.
split.
eassumption.
exists (
tupdate t (
bp t ++ (
map free_item_of_ptr lp ::
nil))
bp).
exists tp.
exists sp.
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_free_items_of_ptrs.
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.
intro Enil.
by destruct lp.
done.
rewrite tupdate_o in IN.
eby eapply BNE.
done.
split.
by apply scratch_allocs_fresh_free.
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.
simpl in *.
destruct (
peq t'
t)
as [-> |
N].
rewrite !@
tupdate_s, !@
PTree.gss,
CS'.
simpl.
rewrite buffer_insert_list_m.
pose proof (
no_unbuffer_errors _ t USi)
as AB.
rewrite buffer_insert_list_s,
buffer_insert_list_m in AB.
destruct (
apply_buffer (
tso_buffers cstso t ++
map free_item_of_ptr lp)
(
tso_mem cstso))
as [
sm''|]
_eqn :
AB''; [|
done].
eexists sm''.
eexists csm_obs.
exists cst_obs.
unfold part_update_buffer in *.
rewrite !
flatten_app, <- !
BPD, !
fold_left_opt_app,
PUBs,
PUBt.
simpl.
split.
by rewrite <-
app_nil_end.
split.
by destruct (
Ptr.eq_dec p p)
as [
_|?].
split.
by simpl;
rewrite <-
app_nil_end.
split; [|
done].
eapply st_rel_return;
try edone.
eapply cont_related_load_inv;
try edone; [].
eapply frees_mem_agrees_on_scratch.
eby rewrite apply_buffer_app,
AB'
in AB''.
exploit (
apply_buffer_preserves_mem_partitioning _ _ _ _
csm_obs t MRPs AB'').
unfold part_update_buffer;
rewrite fold_left_opt_app.
by rewrite PUBs.
intros (
_ &
_ &
MR)
r IN.
eapply MR.
exists t.
by rewrite update_partitioning_s.
eby rewrite !@
tupdate_o, !@
PTree.gso,
OS',
buffer_insert_list_m.
Qed.
Lemma free_sim:
forall s s'
p k (
st :
PTree.t Cstacked.state)
t tso csms
(
ST :
cst_step cst_globenv s (
TEmem (
MEfree p k))
s')
(
CS :
st !
t =
Some s)
(
US :
unbuffer_safe (
buffer_insert tso t (
BufferedFree p k)))
(
TSOPCREL :
tso_pc_related (
tso,
st)
csms),
can_reach_error csm_globenv csms \/
(
exists shms' :
St cshm_lts,
taustep cshm_lts csms Etau shms' /\
tso_pc_related (
buffer_insert tso t (
BufferedFree p k),
st !
t <-
s')
shms').
Proof.
Lemma free_fail_sim:
forall s p k s'
tso t tso' (
st :
PTree.t Cstacked.state)
sms
(
ST :
cst_step cst_globenv s (
TEmem (
MEfree p k))
s')
(
TS :
tso_step tso (
MMfreefail t p k)
tso')
(
CS :
st !
t =
Some s)
(
TSOPCREL :
tso_pc_related (
tso,
st)
sms),
can_reach_error csm_globenv sms.
Proof.
Lemma eval_var_ref_related:
forall tp sp sm cst_e csm_e id p c
(
ER :
env_related tp sp sm cst_e csm_e)
(
EVR :
Cstacked.eval_var_ref cst_globenv cst_e id p c),
eval_var_ref csm_globenv csm_e id p c.
Proof.
Lemma store_machine_agrees_on_scratch:
forall c m p v m'
sp
(
SP :
store_ptr c m p v =
Some m')
(
MP :
machine_ptr p),
mem_agrees_on_scratch m m'
sp.
Proof.
Definition prefix_buffer_machine (
tp :
list arange)
(
tb :
list buffer_item) :
Prop :=
forall tbpfx tbsfx tp',
tbpfx ++
tbsfx =
tb ->
part_update_buffer tbpfx tp =
Some tp' ->
forall p n,
In (
p,
n)
tp' ->
machine_ptr p.
Lemma unbuffer_safe_prefix_buffer_machine:
forall t ttso tp,
unbuffer_safe ttso ->
mem_related_with_partitioning ttso.(
tso_mem)
tp ->
mrestr ttso.(
tso_mem) =
low_mem_restr ->
prefix_buffer_machine (
tp t) (
tso_buffers ttso t).
Proof.
Lemma machine_ptr_add:
forall p n,
machine_ptr p ->
machine_ptr (
p +
n).
Proof.
by intros [b o] n. Qed.
Lemma eval_var_ref_machine:
forall tp sp sm te se p c id,
env_related tp sp sm te se ->
(
forall p n,
In (
p,
n)
tp ->
machine_ptr p) ->
Cstacked.eval_var_ref cst_globenv te id p c ->
machine_ptr p.
Proof.
intros tp sp sm te se p c id ER MTP EVR.
destruct ER as [
n (
TPD &
_ &
_ &
EIR)].
specialize (
EIR id).
inv EVR;
rewrite EG in EIR;
destruct (
se !
id)
as [
sei|]
_eqn :
Esei;
try done.
inv EIR.
rewrite EB in TPD.
destruct TPD as (
_ &
TPD &
_).
apply machine_ptr_add.
eapply MTP.
rewrite TPD.
eby left.
eby eapply globenv_machine.
Qed.
Lemma call_cont_related:
forall {
tp sp sm stk smk},
cont_related tp sp sm stk smk ->
cont_related tp sp sm (
Cstacked.call_cont stk) (
call_cont smk).
Proof.
intros tp sp sm stk smk KR.
eby induction KR; try edone; econstructor.
Qed.
Lemma machine_val_cast:
forall v c,
machine_val v ->
machine_val (
cast_value_to_chunk c v).
Proof.
by intros [] [].
Qed.
Lemma write_thread_sim:
forall {
ts p c v ts'
tp sp sm ss}
(
TPMP :
forall p n,
In (
p,
n)
tp ->
machine_ptr p)
(
ST :
cst_step cst_globenv ts (
TEmem (
MEwrite p c v))
ts')
(
SR :
state_related tp sp sm ts ss),
machine_ptr p /\
machine_val v /\
exists ss',
cs_step csm_globenv ss (
TEmem (
MEwrite p c v))
ss' /\
(
forall sm',
store_ptr c sm p v =
Some sm' ->
state_related tp sp sm'
ts'
ss').
Proof.
Lemma buffer_scratch_ranges_app_write:
forall b p c v,
buffer_scratch_ranges b =
buffer_scratch_ranges (
b ++
BufferedWrite p c v ::
nil).
Proof.
intros.
induction b. done.
simpl. by rewrite IHb.
Qed.
Lemma scratch_allocs_fresh_write:
forall tso sp t p c v
(
SAF :
scratch_allocs_fresh (
tso_buffers tso)
sp),
scratch_allocs_fresh
(
tupdate t (
tso_buffers tso t ++
BufferedWrite p c v ::
nil)
(
tso_buffers tso))
sp.
Proof.
Lemma write_sim_aux:
forall s s'
p c v (
st :
PTree.t Cstacked.state)
t tso cstso csst
(
ST :
cst_step cst_globenv s (
TEmem (
MEwrite p c v))
s')
(
CS :
st !
t =
Some s)
(
US :
unbuffer_safe (
buffer_insert cstso t (
BufferedWrite p c v)))
(
TSOPCREL :
tso_pc_related (
tso,
st) (
cstso,
csst)),
(
exists shms' :
St cshm_lts,
taustep cshm_lts (
cstso,
csst)
Etau shms' /\
tso_pc_unsafe_related (
buffer_insert tso t (
BufferedWrite p c v),
st !
t <-
s')
shms').
Proof.
intros.
pose proof TSOPCREL as [
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 &
MCM) &
TCs &
BPD &
BNE &
SAF &
MRPt &
MRPs &
TREL).
simpl in *.
pose proof TCs as [
BCs USs].
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 (
TPMP :
forall p n,
In (
p,
n)
tp' ->
machine_ptr p).
pose proof (
unbuffer_safe_prefix_buffer_machine t _ _
(
proj2 TC)
MRPt MCRt)
as PBM.
by eapply (
PBM _ nil); [
rewrite app_nil_end |
apply PUBt].
end_assert TPMP.
assert (
SCO' :=
step_consistent_with_env ST SCO).
destruct (
write_thread_sim TPMP ST SR)
as (
MP &
MV & [
nss (
NST &
CSR)]).
assert(
WS :
taustep cshm_lts
(
cstso,
csst)
Etau
(
buffer_insert cstso t (
BufferedWrite p c v),
csst !
t <-
nss)).
apply step_taustep.
simpl.
eby eapply Comp.step_ord;
try edone;
econstructor.
end_assert WS.
assert (
BRt :
buffers_related
(
tso_buffers tso t ++
BufferedWrite p c v ::
nil)
(
tp t) (
bp t ++ ((
BufferedWrite p c v ::
nil) ::
nil))
(
sp t)).
destruct (
TREL t)
as (
PIt' &
BRt' &
_).
eapply buffers_related_suffix;
try edone.
2 :
eby rewrite <-
BPD.
eby econstructor;
vauto.
eexists (
_,
_).
split.
eassumption.
exists (
tupdate t (
bp t ++ ((
BufferedWrite p c v ::
nil) ::
nil))
bp).
exists tp.
exists sp.
split;
simpl.
intro t'.
destruct (
peq t'
t)
as [-> |
N].
rewrite tupdate_s.
intros bi IN.
apply in_app_or in IN.
eby destruct IN as [
IN | [<- | ?]];
try edone;
eapply MTB.
by rewrite tupdate_o; [
apply MTB | ].
split.
done.
split.
done.
split.
eapply Comp.taustep_preserves_consistency.
apply WS.
done.
split.
intro t'.
destruct (
peq t'
t)
as [-> |
N].
by rewrite !@
tupdate_s,
flatten_app;
simpl;
rewrite <-
BPD.
by rewrite !@
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.
done.
done.
rewrite tupdate_o in IN.
eby eapply BNE.
done.
split.
by apply scratch_allocs_fresh_write.
split.
done.
split.
done.
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.
pose proof (
no_unbuffer_errors _ t US)
as AB.
simpl in AB.
rewrite tupdate_s in AB.
destruct (
apply_buffer (
tso_buffers cstso t ++
BufferedWrite p c v ::
nil)
(
tso_mem cstso))
as [
sm''|]
_eqn :
AB''; [|
done].
eexists sm''.
eexists sp'.
exists tp'.
unfold part_update_buffer in *.
rewrite !
flatten_app, <- !
BPD, !
fold_left_opt_app,
PUBs,
PUBt.
simpl.
destruct (
low_mem_restr (
Ptr.block p))
as []
_eqn :
LMR;
[|
by destruct p;
simpl in *;
rewrite LMR in MP].
split.
done.
split.
done.
split.
done.
split; [|
done].
apply CSR.
rewrite apply_buffer_app,
AB'
in AB''.
simpl in AB''.
by destruct (
store_ptr c sm'
p v)
as [
smx|];
clarify.
eby rewrite !@
tupdate_o, !@
PTree.gso.
Qed.
Lemma write_step_fails:
forall s p c v s'
thrs t tso tso'
(
TC :
Comp.consistent tso_mm cs_sem (
tso,
thrs))
(
FS :
cs_step csm_globenv s (
TEmem (
MEwrite p c v))
s')
(
CS :
thrs !
t =
Some s)
(
Etso' :
tso' =
buffer_insert tso t (
BufferedWrite p c v))
(
NUS' : ~
unbuffer_safe tso'),
can_reach_error csm_globenv (
tso,
thrs).
Proof.
Lemma write_sim:
forall s s'
p c v (
st :
PTree.t Cstacked.state)
t tso csms
(
ST :
cst_step cst_globenv s (
TEmem (
MEwrite p c v))
s')
(
CS :
st !
t =
Some s)
(
US :
unbuffer_safe (
buffer_insert tso t (
BufferedWrite p c v)))
(
TSOPCREL :
tso_pc_related (
tso,
st)
csms),
can_reach_error csm_globenv csms \/
(
exists shms' :
St cshm_lts,
taustep cshm_lts csms Etau shms' /\
tso_pc_related (
buffer_insert tso t (
BufferedWrite p c v),
st !
t <-
s')
shms').
Proof.
Lemma write_fail_sim:
forall s p c v s'
tso t tso' (
st :
PTree.t Cstacked.state)
sms
(
ST :
cst_step cst_globenv s (
TEmem (
MEwrite p c v))
s')
(
TS :
tso_step tso (
MMreadfail t p c)
tso')
(
CS :
st !
t =
Some s)
(
TSOPCREL :
tso_pc_related (
tso,
st)
sms),
can_reach_error csm_globenv sms.
Proof.
End FREEWRITE_SIM.