Require Import Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Memeq.
Require Import TSOmachine.
Require Import TSOsimulation.
Require Import Simulations.
Require Import Events.
Require Import Globalenvs.
Require Import Libtactics.
Require Import MMperthreadsimdef.
Buffer relation
Irrelvant actions do not change partitions or values.
Definition buffer_item_irrelevant (
bi :
buffer_item) :=
match bi with
|
BufferedAlloc _ _ MObjHeap =>
True
|
BufferedFree _ MObjHeap =>
True
|
BufferedAlloc _ _ MObjGlobal =>
True
|
BufferedFree _ MObjGlobal =>
True
|
_ =>
False
end.
Applies a buffer item to a partition. For stack
allocations/deallocations this means adding/removing the
allocated/deallocated range to/from the partition.
Definition part_update (
bi :
buffer_item)
(
part :
list arange)
:
option (
list arange) :=
match bi with
|
BufferedAlloc p n MObjStack =>
if valid_alloc_range_dec (
p,
n)
then if range_in_dec (
p,
n)
part
then None
else Some ((
p,
n) ::
part)
else None
|
BufferedFree p MObjStack =>
match part with
| (
p',
n') ::
part' =>
if Ptr.eq_dec p p'
then Some part'
else None
|
_ =>
None
end
|
BufferedAlloc p n _ =>
Some part
|
BufferedFree p _ =>
Some part
|
BufferedWrite p c v =>
Some part
end.
Notation part_update_buffer := (
fold_left_opt part_update).
Definition non_stack k :=
match k with
|
MObjStack =>
False
|
_ =>
True
end.
Inductive buffers_related :
list buffer_item ->
list arange ->
list buffer_item ->
list arange ->
Prop :=
|
buffers_related_empty:
forall tp sp,
buffers_related nil tp nil sp
|
buffers_related_irrelevant:
forall tp sp bi sb tb
(
BIIR:
buffer_item_irrelevant bi)
(
BR:
buffers_related tb tp sb sp),
buffers_related (
bi ::
tb)
tp (
bi ::
sb)
sp
|
buffers_related_write:
forall tp sp p c v v'
sb tb
(
LD:
Val.lessdef v'
v)
(
BR:
buffers_related tb tp sb sp),
buffers_related (
BufferedWrite p c v ::
tb)
tp (
BufferedWrite p c v' ::
sb)
sp
|
buffers_related_local_write:
forall tp sp p c v sb tb
(
CI:
chunk_inside_range_list p c tp)
(
CNI:
range_not_in (
range_of_chunk p c)
sp)
(
ALG:
pointer_chunk_aligned p c)
(
BR:
buffers_related tb tp sb sp),
buffers_related (
BufferedWrite p c v ::
tb)
tp sb sp
|
buffers_related_salloc:
forall tp sp p n sb tb r
(
RNIN:
range_not_in (
p,
n)
sp)
(
RIr:
range_inside (
p,
n)
r)
(
INtp:
In r tp)
(
VAR:
valid_alloc_range (
p,
n))
(
BR:
buffers_related tb tp sb ((
p,
n) ::
sp)),
buffers_related tb tp (
BufferedAlloc p n MObjStack ::
sb)
sp
|
buffers_related_sfree:
forall tp sp p n sb tb
(
BR:
buffers_related tb tp sb sp),
buffers_related tb tp (
BufferedFree p MObjStack ::
sb) ((
p,
n) ::
sp)
|
buffers_related_talloc:
forall tp sp p n sb tb
(
RNIN:
range_not_in (
p,
n)
tp)
(
VAR:
valid_alloc_range (
p,
n))
(
BR:
buffers_related tb ((
p,
n) ::
tp)
sb sp),
buffers_related (
BufferedAlloc p n MObjStack ::
tb)
tp sb sp
|
buffers_related_tfree:
forall tp sp p n sb tb
(
RNIN:
range_not_in (
p,
n)
sp)
(
BR:
buffers_related tb tp sb sp),
buffers_related (
BufferedFree p MObjStack ::
tb) ((
p,
n) ::
tp)
sb sp.
Tactic Notation "
buffers_related_cases"
tactic(
first)
tactic(
c) :=
first; [
c "
buffers_related_empty" |
c "
buffers_related_irrelevant" |
c "
buffers_related_write" |
c "
buffers_related_local_write" |
c "
buffers_related_salloc" |
c "
buffers_related_sfree" |
c "
buffers_related_talloc" |
c "
buffers_related_tfree"].
Memories are related for non-stack object if the objects are
allocated at exactly the same places.
Definition non_stack_mem_related (
tm :
mem) (
sm :
mem) :
Prop :=
forall r k,
match k with
|
MObjStack =>
True
|
_ =>
range_allocated r k tm <->
range_allocated r k sm
end.
Memories are related for values if for any location, the value in the
Machabstr memory (if defined at all) is less defined than the value
at the same location in Machconcr memory.
Definition load_values_related (
tm :
mem) (
sm :
mem) :=
forall p c,
match load_ptr c tm p,
load_ptr c sm p with
|
Some tv,
Some sv =>
Val.lessdef sv tv
|
_,
None =>
True
|
_,
_ =>
False
end.
Partitioning among threads is a function that assigns a
list of owned regions to each thread id.
Definition partitioning :=
positive ->
list arange.
Partitioning is disjoint if the regions are pairwise disjoint.
Definition partitioning_disjoint (
part :
partitioning) :
Prop :=
forall x y,
x <>
y ->
range_lists_disjoint (
part x) (
part y).
Definition mem_related_with_partitioning
(
m :
mem)
(
part :
positive ->
list arange) :
Prop :=
partitioning_disjoint part /\
(
forall t,
range_list_disjoint (
part t)) /\
(
forall r, (
exists t,
In r (
part t)) <->
range_allocated r MObjStack m).
Lemma fold_left_opt_dest:
forall {
A B f} {
h:
A} {
t} {
v:
B} {
v'},
fold_left_opt f (
h ::
t)
v =
Some v' ->
exists v'',
f h v =
Some v'' /\
fold_left_opt f t v'' =
Some v'.
Proof.
intros A B f h t v v' FLO.
simpl in FLO.
destruct (f h v) as [v''|] _eqn : E; try done.
exists v''. by split.
Qed.
Lemma fold_left_opt_app_dest:
forall {
A B f} {
l1 :
list A} {
l2} {
v:
B} {
v'},
fold_left_opt f (
l1 ++
l2)
v =
Some v' ->
exists v'',
fold_left_opt f l1 v =
Some v'' /\
fold_left_opt f l2 v'' =
Some v'.
Proof.
intros A B f l1 l2 v v'
FLO.
rewrite fold_left_opt_app in FLO.
destruct (
fold_left_opt f l1 v)
as [
v''|]
_eqn :
E;
try done.
exists v''.
by split.
Qed.
Lemma biir_part_update:
forall bi p,
buffer_item_irrelevant bi ->
part_update bi p =
Some p.
Proof.
intros. by destruct bi as [|p' n []|p' []].
Qed.
Lemma buffers_related_suffix:
forall tb tp sb sp tb'
tp'
sb'
sp'
(
BR1:
buffers_related tb tp sb sp)
(
BR2:
buffers_related tb'
tp'
sb'
sp')
(
PUs:
part_update_buffer sb'
sp' =
Some sp)
(
PUt:
part_update_buffer tb'
tp' =
Some tp),
buffers_related (
tb' ++
tb)
tp' (
sb' ++
sb)
sp' .
Proof.
Definition range_list_allocated (
p :
list arange)
(
m :
mem) :
Prop :=
forall r :
arange,
In r p ->
range_allocated r MObjStack m.
Lemma mem_related_with_partitioning_ext:
forall m part part',
mem_related_with_partitioning m part ->
(
forall t,
part t =
part'
t) ->
mem_related_with_partitioning m part'.
Proof.
intros m part part' (
PD &
RLD &
MRWP)
E.
split.
intros t t'.
rewrite <- !
E.
apply PD.
split.
intro t;
rewrite <- !
E;
apply RLD.
intro r;
split.
intros [
t IN].
rewrite <-
E in IN.
apply (
proj1 (
MRWP r)).
eby eexists.
intro RA.
destruct (
proj2 (
MRWP r)
RA)
as [
t'
IN].
exists t'.
by rewrite <-
E.
Qed.
Lemma alloc_ptr_stack_preserves_mem_partitioning:
forall m m'
p n part t,
mem_related_with_partitioning m part ->
alloc_ptr (
p,
n)
MObjStack m =
Some m' ->
mem_related_with_partitioning m'
(
tupdate t ((
p,
n) :: (
part t))
part).
Proof.
Lemma alloc_ptr_non_stack_preserves_mem_partitioning:
forall m m'
p n k part,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
alloc_ptr (
p,
n)
k m =
Some m' ->
mem_related_with_partitioning m'
part.
Proof.
intros m m'
p n k part [
PD [
LD MR]]
NS AP.
split.
intros t1 t2 N r IN r'
IN'.
eby eapply (
PD _ _ N r IN r'
IN').
split.
apply LD.
intro r.
split.
intros [
t'
IN].
apply (
alloc_preserves_allocated AP);
apply (
proj1 (
MR _));
eexists;
eassumption.
intro RA.
destruct (
alloc_preserves_allocated_back AP _ _ RA)
as [[-> <-] |
RAo];
try done.
destruct (
proj2 (
MR _)
RAo);
vauto.
Qed.
Lemma alloc_ptr_non_stack_preserves_mem_partitioning_upd:
forall m m'
p n k part t,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
alloc_ptr (
p,
n)
k m =
Some m' ->
mem_related_with_partitioning m'
(
tupdate t (
part t)
part).
Proof.
Lemma store_ptr_preserves_mem_partitioning:
forall m m'
c p v part,
mem_related_with_partitioning m part ->
store_ptr c m p v =
Some m' ->
mem_related_with_partitioning m'
part.
Proof.
Lemma store_ptr_preserves_mem_partitioning2:
forall m m'
c p v part t,
mem_related_with_partitioning m part ->
store_ptr c m p v =
Some m' ->
mem_related_with_partitioning m'
(
tupdate t (
part t)
part).
Proof.
intros m m'
c p v part t [
PD [
LD MR]]
ST.
unfold tupdate.
split.
intros x y NE.
destruct (
peq x t)
as [-> |
Nx];
destruct (
peq y t)
as [-> |
Ny];
apply (
PD _ _ NE).
split.
intro t'.
destruct (
peq t'
t);
apply LD.
intro r.
split.
intros [
t'
IN].
apply (
proj1 (
store_preserves_allocated_ranges ST _ _)).
apply (
proj1 (
MR _)).
destruct (
peq t'
t);
eby eexists.
intro RA.
apply (
proj2 (
store_preserves_allocated_ranges ST _ _))
in RA.
destruct (
proj2 (
MR _)
RA)
as [
t'
IN].
exists t'.
by destruct (
peq t'
t)
as [-> |
_].
Qed.
Lemma ranges_disjoint_dont_overlap:
forall r r',
ranges_disjoint r r' ->
ranges_overlap r r' ->
False.
Proof.
intros r r' D O. apply O, D. Qed.
Lemma range_disjoint_remove:
forall p l,
range_list_disjoint l ->
range_list_disjoint (
range_remove p l).
Proof.
induction l as [|[
ph nh]
l IH].
done.
simpl.
intros [
DISJ RNI].
destruct (
Ptr.eq_dec ph p)
as [-> |
N].
auto.
simpl.
split.
by apply IH.
intros []
IN'.
eby eapply RNI,
in_range_remove.
Qed.
Lemma free_ptr_preserves_mem_partitioning:
forall m m'
p n rest k part t,
mem_related_with_partitioning m part ->
free_ptr p k m =
Some m' ->
part t = (
p,
n) ::
rest ->
mem_related_with_partitioning m'
(
tupdate t rest part).
Proof.
intros m m'
p n rest k part t [
PD [
LD MR]]
FP INP.
unfold tupdate.
pose proof (
free_cond_spec p k m)
as Fspec.
rewrite FP in Fspec.
destruct Fspec as [
n'
Fspec].
assert (
INpe:
exists t,
In (
p,
n) (
part t)).
exists t.
by rewrite INP;
left.
destruct (
alloc_ranges_same Fspec (
proj1 (
MR _)
INpe))
as [-> ->].
split.
intros t1 t2 N r IN r'
IN'.
destruct (
peq t1 t)
as [-> |
Nt1];
destruct (
peq t2 t)
as [-> |
Nt2];
try done;
try (
eapply PD; [
apply N |
apply IN |
apply IN']).
destruct r as [
rp rn].
eapply PD; [
apply N | |
apply IN'].
rewrite INP.
by right.
destruct r'.
eapply PD; [
apply N |
apply IN | ].
rewrite INP;
by right.
split.
intros t'.
destruct (
peq t'
t)
as [
_ |
N].
specialize (
LD t);
rewrite INP in LD;
simpl in LD;
tauto.
by apply LD.
intro r.
split.
intros [
t'
IN].
assert (
INpn :
In (
p,
n) (
part t)).
by rewrite INP;
left.
destruct (
peq t'
t)
as [<- |
N].
destruct r as [
pr nr].
assert (
IN2 :
In (
pr,
nr) (
part t')).
by rewrite INP;
right.
assert (
IN':
exists t,
In (
pr,
nr) (
part t)).
eexists;
eassumption.
apply (
proj1 (
MR _))
in IN'.
destruct (
free_preserves_allocated FP _ _ IN')
as [|[
E _]].
done.
simpl in E.
subst.
byContradiction.
specialize (
LD t');
rewrite INP in LD;
simpl in LD;
destruct LD as [
RLD RNI].
destruct (
alloc_ranges_same Fspec IN')
as [<-
_].
specialize (
RNI (
p,
n)
IN).
revert RNI.
apply ranges_overlap_refl.
eby eapply valid_alloc_range_non_empty,
allocated_range_valid.
assert (
IN':
exists t,
In r (
part t)).
eexists;
eassumption.
apply (
proj1 (
MR _))
in IN'.
destruct r as [
pr nr].
destruct (
free_preserves_allocated FP _ _ IN')
as [|[
E _]].
done.
simpl in E.
subst.
byContradiction.
eapply ranges_disjoint_dont_overlap.
apply (
PD _ _ N _ IN _ INpn).
eapply non_empty_same_ptr_overlap;
eapply valid_alloc_range_non_empty,
allocated_range_valid, (
proj1 (
MR _));
eexists;
eassumption.
intro RA.
pose proof (
free_preserves_allocated_back FP _ _ RA)
as RAo.
destruct (
proj2 (
MR _)
RAo)
as [
t'
IN'].
exists t'.
destruct (
peq t'
t)
as [-> |
N];
try done.
destruct r as [
pr nr].
rewrite INP in IN'.
simpl in IN'.
destruct IN'
as [
E |
IN'].
inv E.
destruct (
free_not_allocated FP _ _ RA).
done.
Qed.
Lemma free_ptr_non_stack_preserves_mem_partitioning:
forall m m'
p k part,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
free_ptr p k m =
Some m' ->
mem_related_with_partitioning m'
part.
Proof.
intros m m'
p k part [
PD [
LD MR]]
NS FP.
unfold tupdate.
split.
intros t1 t2 N r IN r'
IN'.
eby eapply (
PD _ _ N r IN r'
IN').
split.
by intros t';
apply LD.
intro r.
split.
intros [
t'
IN].
assert (
RA :
range_allocated r MObjStack m).
eby apply (
proj1 (
MR _));
eby eexists.
by destruct (
free_preserves_allocated FP _ _ RA)
as [
RA' | [<- <-]].
intro RA.
apply (
free_preserves_allocated_back FP)
in RA.
by destruct (
proj2 (
MR _)
RA)
as [
t'
IN'];
vauto.
Qed.
Lemma free_ptr_non_stack_preserves_mem_partitioning_upd:
forall m m'
p k part t,
mem_related_with_partitioning m part ->
match k with MObjStack =>
False |
_ =>
True end ->
free_ptr p k m =
Some m' ->
mem_related_with_partitioning m'
(
tupdate t (
part t)
part).
Proof.
Lemma apply_buffer_item_preserves_mem_partitioning:
forall m m'
bi part part'
t,
mem_related_with_partitioning m part ->
apply_buffer_item bi m =
Some m' ->
part_update bi (
part t) =
Some part' ->
mem_related_with_partitioning m' (
tupdate t part'
part).
Proof.
Lemma apply_buffer_preserves_mem_partitioning:
forall b m m'
part part'
t,
mem_related_with_partitioning m part ->
apply_buffer b m =
Some m' ->
part_update_buffer b (
part t) =
Some part' ->
mem_related_with_partitioning m' (
tupdate t part'
part).
Proof.
Lemma apply_buffer_consD:
forall {
bi b m m'}
(
AB :
apply_buffer (
bi ::
b)
m =
Some m'),
exists mi,
apply_buffer_item bi m =
Some mi /\
apply_buffer b mi =
Some m'.
Proof.
Lemma mem_agrees_on_local_preserved_by_irrelevant:
forall bi tm tm'
sp tp tmx tmx'
(
BIIR:
buffer_item_irrelevant bi)
(
ABI :
apply_buffer_item bi tm =
Some tmx)
(
ABI':
apply_buffer_item bi tm' =
Some tmx')
(
RLA :
range_list_allocated tp tm)
(
RLA':
range_list_allocated tp tm')
(
MA :
mem_agrees_on_local tm tm'
tp sp),
mem_agrees_on_local tmx tmx'
tp sp.
Proof.
intros.
(
buffer_item_cases (
destruct bi as [
p c v |
p n k |
p k])
Case);
intros r'
p'
CI;
specialize (
MA r'
p'
CI);
destruct (
chunk_inside_range_listD CI)
as [
rc (
INrc &
RIrc)].
Case "
BufferedWrite".
done.
Case "
BufferedAlloc".
assert(
ranges_disjoint (
range_of_chunk r'
p') (
p,
n)).
eapply ranges_disjoint_comm,
disjoint_inside_disjoint_r,
RIrc.
simpl in ABI;
apply (
alloc_allocatedD ABI (
RLA _ INrc)).
by destruct k;
try done;
simpl in ABI,
ABI';
rewrite (
load_alloc_other ABI), (
load_alloc_other ABI').
Case "
BufferedFree".
destruct(
free_someD ABI)
as [
n RA].
destruct(
free_someD ABI')
as [
n'
RA'].
simpl in ABI,
ABI'.
rewrite (
load_free_other ABI RA), (
load_free_other ABI'
RA');
try done.
-
destruct (
ranges_are_disjoint RA' (
RLA'
_ INrc))
as [[
_ E] |].
by subst.
by eapply ranges_disjoint_comm,
disjoint_inside_disjoint_r,
RIrc.
-
destruct (
ranges_are_disjoint RA (
RLA _ INrc))
as [[
_ E] |].
by subst.
by eapply ranges_disjoint_comm,
disjoint_inside_disjoint_r,
RIrc.
Qed.
Lemma mem_agrees_on_local_preserved_by_write:
forall p c v tm tm'
sp tp tmx tmx'
(
ABI :
apply_buffer_item (
BufferedWrite p c v)
tm =
Some tmx)
(
ABI':
apply_buffer_item (
BufferedWrite p c v)
tm' =
Some tmx')
(
MA :
mem_agrees_on_local tm tm'
tp sp),
mem_agrees_on_local tmx tmx'
tp sp.
Proof.
Lemma alloc_preserves_chunk_allocation:
forall {
r k m m'} (
A :
alloc_ptr r k m =
Some m'),
forall p c (
CA :
chunk_allocated_and_aligned p c m),
chunk_allocated_and_aligned p c m'.
Proof.
intros.
destruct CA as [[
r' [
k' [
RI RA]]]
PA].
split; [|
done].
exists r';
exists k';
split.
done.
eby eapply alloc_preserves_allocated.
Qed.
Lemma mem_agrees_on_local_preserved_by_talloc:
forall p n tm tm'
sp tp tmx tmx'
(
ABI :
apply_buffer_item (
BufferedAlloc p n MObjStack)
tm =
Some tmx)
(
ABI':
apply_buffer_item (
BufferedAlloc p n MObjStack)
tm' =
Some tmx')
(
MA :
mem_agrees_on_local tm tm'
tp sp),
mem_agrees_on_local tmx tmx' ((
p,
n)::
tp)
sp.
Proof.
Lemma mem_agrees_on_local_preserved_by_tfree:
forall p n tm tm'
sp tp tmx tmx'
(
RA :
range_allocated (
p,
n)
MObjStack tm)
(
RA' :
range_allocated (
p,
n)
MObjStack tm')
(
RNI :
range_not_in (
p,
n)
tp)
(
ABI :
apply_buffer_item (
BufferedFree p MObjStack)
tm =
Some tmx)
(
ABI':
apply_buffer_item (
BufferedFree p MObjStack)
tm' =
Some tmx')
(
MA :
mem_agrees_on_local tm tm' ((
p,
n)::
tp)
sp),
mem_agrees_on_local tmx tmx'
tp sp.
Proof.
Lemma mem_agrees_on_local_preserved_by_salloc:
forall p n tm tm'
sp tp
(
MA :
mem_agrees_on_local tm tm'
tp sp),
mem_agrees_on_local tm tm'
tp ((
p,
n)::
sp).
Proof.
intros.
intros p'
c'
CI.
specialize (
MA p'
c'
CI).
destruct (
load_ptr c'
tm p')
as []
_eqn :
Ltm;
destruct (
load_ptr c'
tm'
p')
as []
_eqn :
Ltm';
try done.
intro RNI;
apply MA.
intros r IN.
apply RNI.
by right.
Qed.
Fixpoint remove_frees_from_part (
sp :
list arange) (
b :
list buffer_item) :=
match b with
|
nil =>
sp
|
BufferedFree p MObjStack ::
b =>
range_remove p (
remove_frees_from_part sp b)
|
_ ::
b =>
remove_frees_from_part sp b
end.
Lemma in_rfree_part:
forall p n b sp,
In (
p,
n) (
remove_frees_from_part sp b) <->
In (
p,
n)
sp /\ ~
In (
BufferedFree p MObjStack)
b.
Proof.
induction b as [|
bi b];
intros;
simpl.
tauto.
destruct bi as [
p'
c'
v'|
p'
n'
k'|
p' []];
try (
specialize (
IHb sp);
destruct IHb as [
IHl IHr];
split;
[
intro;
split; [|
intros [|]];
try done;
tauto |
intros [
IN O];
apply IHr;
split; [|
intro IN';
elim O];
tauto]).
specialize (
IHb sp);
destruct IHb as [
IHl IHr].
split.
intro IN.
apply in_range_removeD in IN.
destruct IN as [
NE IN].
specialize (
IHl IN).
split.
tauto.
intros [
E|];
clarify;
tauto.
intros [
IN O].
apply in_range_removeI.
apply IHr.
tauto.
intro E;
subst;
tauto.
Qed.
Lemma mem_agrees_on_local_mono_sp:
forall tm tm'
tp sp sp'
(
SUB:
forall r,
In r sp ->
In r sp')
(
MA:
mem_agrees_on_local tm tm'
tp sp),
mem_agrees_on_local tm tm'
tp sp'.
Proof.
intros.
intros p c IN.
specialize (
MA p c IN).
destruct load_ptr;
destruct load_ptr;
try done; [].
intro RNI;
apply MA.
intros r'
IN'.
eapply RNI.
eauto.
Qed.
Lemma remove_frees_from_part_unbuffer:
forall r sp b bi
(
IN:
In r (
remove_frees_from_part sp (
bi ::
b))),
In r (
remove_frees_from_part sp b).
Proof.
intros.
destruct r as [
p n].
apply <-
in_rfree_part.
apply in_rfree_part in IN.
destruct IN as [
IN NIN].
split.
done.
intro IN';
elim NIN.
by right.
Qed.
Lemma mem_agrees_on_local_unbuffer:
forall tm tm'
tp sp bi b
(
MA:
mem_agrees_on_local tm tm'
tp (
remove_frees_from_part sp (
bi ::
b))),
mem_agrees_on_local tm tm'
tp (
remove_frees_from_part sp b).
Proof.
Lemma mem_agrees_on_local_preserved_by_sfree:
forall p n tm tm'
sp tp b
(
RNI :
range_not_in (
p,
n)
sp)
(
MA :
mem_agrees_on_local tm tm'
tp
(
remove_frees_from_part ((
p,
n)::
sp) (
BufferedFree p MObjStack::
b))),
mem_agrees_on_local tm tm'
tp (
remove_frees_from_part sp b).
Proof.
Lemma part_update_irrelevant:
forall {
bi} (
BIIR :
buffer_item_irrelevant bi)
part,
part_update bi part =
Some part.
Proof.
intros.
by destruct bi as [|p n []|p []].
Qed.
Lemma range_list_allocated_irrelevant:
forall bi tm tm'
tp
(
BIIR:
buffer_item_irrelevant bi)
(
ABI:
apply_buffer_item bi tm =
Some tm')
(
RLA:
range_list_allocated tp tm),
range_list_allocated tp tm'.
Proof.
Lemma range_list_allocated_part_alloc:
forall p n tm tm'
tp
(
A:
alloc_ptr (
p,
n)
MObjStack tm =
Some tm')
(
RLA:
range_list_allocated tp tm),
range_list_allocated ((
p,
n)::
tp)
tm'.
Proof.
Lemma range_list_allocated_part_free:
forall p n tm tm'
tp
(
F:
free_ptr p MObjStack tm =
Some tm')
(
RNI:
range_not_in (
p,
n)
tp)
(
RLA:
range_list_allocated ((
p,
n)::
tp)
tm),
range_list_allocated tp tm'.
Proof.
Lemma range_list_allocated_write:
forall p c v tm tm'
tp
(
ABI:
apply_buffer_item (
BufferedWrite p c v)
tm =
Some tm')
(
RLA:
range_list_allocated tp tm),
range_list_allocated tp tm'.
Proof.
Lemma irrelevant_agrees_on_local:
forall bi tm tm'
tp sp t
(
BIIR:
buffer_item_irrelevant bi)
(
ABI :
apply_buffer_item bi tm =
Some tm')
(
MRPt:
mem_related_with_partitioning tm tp),
mem_agrees_on_local tm tm' (
tp t)
sp.
Proof.
Lemma buffers_related_part_update_buffer:
forall sb sp tb tp
(
BR:
buffers_related tb tp sb sp),
exists sp',
part_update_buffer sb sp =
Some sp'.
Proof.
intros.
(
buffers_related_cases (
induction BR)
Case);
try done.
Case "
buffers_related_empty".
eby eexists.
Case "
buffers_related_irrelevant".
simpl.
by rewrite part_update_irrelevant.
Case "
buffers_related_salloc".
simpl.
destruct valid_alloc_range_dec; [|
done].
destruct range_in_dec as [[? [
IN O]]|];
eauto.
by specialize (
RNIN _ IN).
Case "
buffers_related_sfree".
simpl.
by destruct Ptr.eq_dec.
Qed.
Lemma range_remove_comm:
forall p p'
l,
range_remove p (
range_remove p'
l) =
range_remove p' (
range_remove p l).
Proof.
induction l as [|[
pr nr]
l IH].
done.
simpl.
by destruct (
Ptr.eq_dec pr p')
as [<-|
N];
destruct (
Ptr.eq_dec pr p)
as [<-|
N'];
simpl;
subst;
try done;
rewrite IH; (
repeat destruct Ptr.eq_dec).
Qed.
Lemma range_remove_comm_remove_frees:
forall p b sp,
range_remove p (
remove_frees_from_part sp b) =
remove_frees_from_part (
range_remove p sp)
b.
Proof.
induction b as [|
bi b IH].
done.
intros.
destruct bi as [| |
p' []];
simpl;
auto.
by rewrite <-
IH,
range_remove_comm.
Qed.
Lemma range_remove_not_in:
forall p n sp
(
RNE:
range_non_empty (
p,
n))
(
RNEsp:
forall r,
In r sp ->
range_non_empty r)
(
RNI:
range_not_in (
p,
n)
sp),
range_remove p sp =
sp.
Proof.
induction sp as [|[
p'
n']
sp IH].
done.
simpl.
destruct Ptr.eq_dec as [<- |
N];
intros.
specialize (
RNI _ (
in_eq _ _)).
by elim (
non_empty_same_ptr_overlap _ _ _ RNE (
RNEsp _ (
in_eq _ _))).
f_equal;
apply IH.
-
done.
-
intros r IN.
eby eapply RNEsp;
right.
-
intros r IN.
eby eapply RNI;
right.
Qed.
Lemma remove_disjoint:
forall {
p n sp m}
(
RLD:
range_list_disjoint ((
p,
n)::
sp))
(
RLA:
range_list_allocated ((
p,
n)::
sp)
m),
range_remove p sp =
sp.
Proof.
Lemma range_of_chunk_not_empty:
forall p c,
range_non_empty (
range_of_chunk p c).
Proof.
Lemma unbuffer_write_free:
forall p c v t t'
rest r sp'
stso sp
(
US:
unbuffer_safe stso)
(
RO:
ranges_overlap (
range_of_chunk p c)
r)
(
IN:
In r sp)
(
RLA:
range_list_allocated sp stso.(
tso_mem))
(
RLD:
range_list_disjoint sp)
(
PU:
part_update_buffer (
tso_buffers stso t)
sp =
Some sp')
(
NEt:
t <>
t')
(
Ebt:
tso_buffers stso t' =
BufferedWrite p c v ::
rest),
In r (
remove_frees_from_part sp (
tso_buffers stso t)).
Proof.
Lemma non_stack_mem_related_sym:
forall m m',
non_stack_mem_related m m' ->
non_stack_mem_related m'
m.
Proof.
intros m m'
NSR r k.
specialize (
NSR r k).
destruct k;
try done;
by apply iff_sym.
Qed.
Definition stack_or_write_item (
bi :
buffer_item) :
Prop :=
match bi with
|
BufferedAlloc _ _ MObjStack =>
True
|
BufferedFree _ MObjStack =>
True
|
BufferedWrite _ _ _ =>
True
|
_ =>
False
end.
Lemma non_stack_mem_rel_preserved_by_stack_or_write:
forall tm sm bi sm',
non_stack_mem_related tm sm ->
apply_buffer_item bi sm =
Some sm' ->
stack_or_write_item bi ->
non_stack_mem_related tm sm'.
Proof.
Lemma non_stack_mem_rel_preserved_by_stack_or_write_tgt:
forall tm sm bi tm',
non_stack_mem_related tm sm ->
apply_buffer_item bi tm =
Some tm' ->
stack_or_write_item bi ->
non_stack_mem_related tm'
sm.
Proof.
Lemma sim_alloc_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
p n k,
non_stack_mem_related tm sm ->
alloc_ptr (
p,
n)
k tm =
Some tm' ->
alloc_ptr (
p,
n)
k sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma sim_free_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
p k,
non_stack_mem_related tm sm ->
free_ptr p k tm =
Some tm' ->
free_ptr p k sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma sim_irrelevant_preserves_non_stack_mem_related:
forall tm sm tm'
sm'
bi,
non_stack_mem_related tm sm ->
buffer_item_irrelevant bi ->
apply_buffer_item bi tm =
Some tm' ->
apply_buffer_item bi sm =
Some sm' ->
non_stack_mem_related tm'
sm'.
Proof.
Lemma alloc_ptr_tgt_preserves_load_rel:
forall tm sm tm'
r k
(
LVR:
load_values_related tm sm)
(
A:
alloc_ptr r k tm =
Some tm')
(
NA:
forall r'
k',
range_allocated r'
k'
sm ->
ranges_disjoint r'
r),
load_values_related tm'
sm.
Proof.
Lemma alloc_ptr_src_preserves_load_rel:
forall tm sm sm'
r k r'
k'
(
LVR:
load_values_related tm sm)
(
A:
alloc_ptr r k sm =
Some sm')
(
RI:
range_inside r r')
(
RA:
range_allocated r'
k'
tm),
load_values_related tm sm'.
Proof.
Lemma free_ptr_tgt_preserves_load_rel:
forall tm sm tm'
p n k
(
LVR:
load_values_related tm sm)
(
F:
free_ptr p k tm =
Some tm')
(
RA:
range_allocated (
p,
n)
k tm)
(
NA:
forall r'
k',
range_allocated r'
k'
sm ->
ranges_disjoint r' (
p,
n)),
load_values_related tm'
sm.
Proof.
Lemma free_ptr_src_preserves_load_rel:
forall tm sm sm'
p k
(
LVR:
load_values_related tm sm)
(
F:
free_ptr p k sm =
Some sm'),
load_values_related tm sm'.
Proof.
Lemma local_write_preserves_load_rel:
forall tm sm c p v tm'
(
LVR:
load_values_related tm sm)
(
S:
store_ptr c tm p v =
Some tm')
(
CNI:
forall r k (
RA:
range_allocated r k sm),
ranges_disjoint (
range_of_chunk p c)
r),
load_values_related tm'
sm.
Proof.
Lemma write_preserves_load_rel:
forall tm sm c p v v'
tm'
sm'
(
LVR:
load_values_related tm sm)
(
LD:
Val.lessdef v'
v)
(
St:
store_ptr c tm p v =
Some tm')
(
Ss:
store_ptr c sm p v' =
Some sm'),
load_values_related tm'
sm'.
Proof.
Lemma irrelevant_preserves_load_rel:
forall tm sm tm'
sm'
bi
(
LVR:
load_values_related tm sm)
(
NSR:
non_stack_mem_related tm sm)
(
ABIt:
apply_buffer_item bi tm =
Some tm')
(
ABIs:
apply_buffer_item bi sm =
Some sm')
(
BIIR:
buffer_item_irrelevant bi),
load_values_related tm'
sm'.
Proof.
intros.
intros p'
c'.
specialize (
LVR p'
c').
(
buffer_item_cases (
destruct bi as [
p c v|
p n k|
p k])
Case);
simpl in ABIt,
ABIs,
BIIR.
Case "
BufferedWrite".
done.
Case "
BufferedAlloc".
destruct (
ranges_disjoint_dec (
range_of_chunk p'
c') (
p,
n))
as [
D|
O].
by rewrite (
load_alloc_other ABIt), (
load_alloc_other ABIs).
destruct (
range_inside_dec (
range_of_chunk p'
c') (
p,
n))
as [
RI|
NRI].
destruct (
load_ptr c'
sm'
p')
as [
sv'|]
_eqn :
SL'.
destruct (
load_chunk_allocated_someD SL').
by rewrite (
load_alloc_inside ABIt);
rewrite (
load_alloc_inside ABIs)
in SL';
vauto.
by destruct (
load_ptr c'
tm'
p').
by rewrite (
load_alloc_overlap ABIt), (
load_alloc_overlap ABIs).
Case "
BufferedFree".
assert (
RAn:
exists n,
range_allocated (
p,
n)
k tm /\
range_allocated (
p,
n)
k sm).
destruct (
free_someD ABIt)
as [
n RA].
eexists.
split.
edone.
specialize (
NSR (
p,
n)
k).
destruct k;
try done;
by apply NSR.
destruct RAn as [
n [
RAt RAs]].
destruct (
ranges_disjoint_dec (
range_of_chunk p'
c') (
p,
n))
as [
D|
O].
by rewrite (
load_free_other ABIt RAt D), (
load_free_other ABIs RAs D).
by rewrite (
load_free_overlap ABIt RAt O), (
load_free_overlap ABIs RAs O).
Qed.
Definition partition_injective (
tp :
list arange)
(
sp :
list arange) :
Prop :=
forall r (
IN :
In r sp),
exists r',
range_inside r r' /\
In r'
tp.
Lemma alloc_src_partition_injective:
forall r'
r tp sp
(
RIr:
range_inside r'
r)
(
INtp:
In r tp)
(
PI:
partition_injective tp sp),
partition_injective tp (
r'::
sp).
Proof.
intros.
intros ri IN. simpl in IN. destruct IN as [E | IN].
inv E. eexists. eby split.
eby eapply PI.
Qed.
Lemma alloc_tgt_partition_injective:
forall r tp sp
(
PI:
partition_injective tp sp),
partition_injective (
r::
tp)
sp.
Proof.
intros.
intros r' IN. destruct (PI r' IN) as [ri (RI' & IN')].
eexists. split. edone. by right.
Qed.
Lemma free_tgt_partition_injective:
forall r tp sp
(
RNIN:
range_not_in r sp)
(
MR:
forall r' (
IN:
In r'
sp),
range_non_empty r')
(
PI:
partition_injective (
r::
tp)
sp),
partition_injective tp sp.
Proof.
Lemma free_src_partition_injective:
forall r tp sp
(
PI:
partition_injective tp (
r::
sp)),
partition_injective tp sp.
Proof.
intros.
intros r'
IN.
apply (
PI r' (
in_cons _ _ _ IN)).
Qed.
Inductive tso_related_witt (
ts :
tso_state)
(
tp :
partitioning)
(
ss :
tso_state)
(
sp :
partitioning)
:
Prop :=
|
tso_related_witt_intro:
forall
(
NSMR:
non_stack_mem_related ts.(
tso_mem)
ss.(
tso_mem))
(
LR :
load_values_related ts.(
tso_mem)
ss.(
tso_mem))
(
MR :
mrestr ts.(
tso_mem) =
mrestr ss.(
tso_mem))
(
MRPt:
mem_related_with_partitioning ts.(
tso_mem)
tp)
(
MRPs:
mem_related_with_partitioning ss.(
tso_mem)
sp)
(
PI :
forall t,
partition_injective (
tp t) (
sp t))
(
BR :
forall t,
buffers_related (
ts.(
tso_buffers)
t) (
tp t)
(
ss.(
tso_buffers)
t) (
sp t)),
tso_related_witt ts tp ss sp.
Lemma unbuffer_safe_to_buffer_safe_for_mem:
forall stso t bis rb,
unbuffer_safe stso ->
stso.(
tso_buffers)
t =
bis ++
rb ->
buffer_safe_for_mem bis stso.(
tso_mem).
Proof.
intros stso t bis rb UBS.
revert bis rb.
simpl in UBS.
induction UBS as [
tso'
CABI UBS'
IH].
intros bis rb Eb.
destruct bis as [|
bi rbis].
eexists.
simpl.
reflexivity.
rewrite <-
app_comm_cons in Eb.
destruct (
CABI _ _ _ Eb)
as [
im'
ABIi].
specialize (
IH _ _ _ _ Eb ABIi rbis rb).
simpl in IH.
rewrite tupdate_s in IH.
destruct (
IH (
refl_equal _))
as [
m'
AB].
exists m'.
by simpl;
rewrite ABIi.
Qed.
Lemma irrelevant_preserves_mem_partitioning:
forall bi m m'
part
(
BIIR:
buffer_item_irrelevant bi)
(
MRWP:
mem_related_with_partitioning m part)
(
ABI:
apply_buffer_item bi m =
Some m'),
mem_related_with_partitioning m'
part.
Proof.
Preservation of tso_related_witt
Lemma irrelevant_preserves_tso_related_witt:
forall ts tp ss sp t btrest bsrest tm'
sm'
bi
(
REL:
tso_related_witt ts tp ss sp)
(
BIIR:
buffer_item_irrelevant bi)
(
ABIt:
apply_buffer_item bi ts.(
tso_mem) =
Some tm')
(
ABIs:
apply_buffer_item bi ss.(
tso_mem) =
Some sm')
(
Bt:
ts.(
tso_buffers)
t =
bi ::
btrest)
(
Bs:
ss.(
tso_buffers)
t =
bi ::
bsrest)
(
BRr:
buffers_related btrest (
tp t)
bsrest (
sp t)),
tso_related_witt
(
mktsostate (
tupdate t btrest ts.(
tso_buffers))
tm')
tp
(
mktsostate (
tupdate t bsrest ss.(
tso_buffers))
sm')
sp.
Proof.
Lemma write_preserves_tso_related_witt:
forall ts tp ss sp t btrest bsrest tm'
sm'
p c v v'
(
REL:
tso_related_witt ts tp ss sp)
(
ABIt:
apply_buffer_item (
BufferedWrite p c v)
ts.(
tso_mem) =
Some tm')
(
ABIs:
apply_buffer_item (
BufferedWrite p c v')
ss.(
tso_mem) =
Some sm')
(
LD:
Val.lessdef v'
v)
(
Bt:
ts.(
tso_buffers)
t =
BufferedWrite p c v ::
btrest)
(
Bs:
ss.(
tso_buffers)
t =
BufferedWrite p c v' ::
bsrest)
(
BRr:
buffers_related btrest (
tp t)
bsrest (
sp t)),
tso_related_witt
(
mktsostate (
tupdate t btrest ts.(
tso_buffers))
tm')
tp
(
mktsostate (
tupdate t bsrest ss.(
tso_buffers))
sm')
sp.
Proof.
Lemma mrwp_alloc_in:
forall {
m part r}
(
MRWP:
mem_related_with_partitioning m part)
(
RA:
range_allocated r MObjStack m),
exists t,
In r (
part t).
Proof.
intros.
destruct MRWP as (_ & _ & A).
by apply <- A.
Qed.
Lemma mrwp_in_alloc:
forall {
m part r t}
(
MRWP:
mem_related_with_partitioning m part)
(
IN:
In r (
part t)),
range_allocated r MObjStack m.
Proof.
intros.
destruct MRWP as (_ & _ & A).
apply -> A; vauto.
Qed.
Lemma local_write_preserves_tso_related_witt:
forall ts tp ss sp t btrest tm'
p c v
(
REL:
tso_related_witt ts tp ss sp)
(
ABIt:
apply_buffer_item (
BufferedWrite p c v)
ts.(
tso_mem) =
Some tm')
(
CI:
chunk_inside_range_list p c (
tp t))
(
CNI:
range_not_in (
range_of_chunk p c) (
sp t))
(
Bt:
ts.(
tso_buffers)
t =
BufferedWrite p c v ::
btrest)
(
BRr:
buffers_related btrest (
tp t) (
tso_buffers ss t) (
sp t)),
tso_related_witt
(
mktsostate (
tupdate t btrest ts.(
tso_buffers))
tm')
tp
ss sp.
Proof.
Lemma salloc_preserves_tso_related_witt:
forall ts tp ss sp t bsrest sm'
p n r
(
REL:
tso_related_witt ts tp ss sp)
(
ABIs:
apply_buffer_item (
BufferedAlloc p n MObjStack)
ss.(
tso_mem) =
Some sm')
(
Bs:
ss.(
tso_buffers)
t =
BufferedAlloc p n MObjStack ::
bsrest)
(
RNIN:
range_not_in (
p,
n) (
sp t))
(
RIr:
range_inside (
p,
n)
r)
(
INtp:
In r (
tp t))
(
VAR:
valid_alloc_range (
p,
n))
(
BRr:
buffers_related (
tso_buffers ts t) (
tp t)
bsrest ((
p,
n)::(
sp t))),
tso_related_witt
ts tp
(
mktsostate (
tupdate t bsrest ss.(
tso_buffers))
sm')
(
tupdate t ((
p,
n)::(
sp t))
sp).
Proof.
Lemma sfree_preserves_tso_related_witt:
forall ts tp ss sp t bsrest sptrest sm'
p n
(
REL:
tso_related_witt ts tp ss sp)
(
ABIs:
apply_buffer_item (
BufferedFree p MObjStack)
ss.(
tso_mem) =
Some sm')
(
Bs:
ss.(
tso_buffers)
t =
BufferedFree p MObjStack ::
bsrest)
(
Bspt:
sp t = (
p,
n)::
sptrest)
(
BRr:
buffers_related (
tso_buffers ts t) (
tp t)
bsrest sptrest),
tso_related_witt
ts tp
(
mktsostate (
tupdate t bsrest ss.(
tso_buffers))
sm')
(
tupdate t sptrest sp).
Proof.
Lemma talloc_preserves_tso_related_witt:
forall ts tp ss sp t btrest tm'
p n
(
REL:
tso_related_witt ts tp ss sp)
(
ABIt:
apply_buffer_item (
BufferedAlloc p n MObjStack)
ts.(
tso_mem) =
Some tm')
(
Bt:
ts.(
tso_buffers)
t =
BufferedAlloc p n MObjStack ::
btrest)
(
RNIN:
range_not_in (
p,
n) (
tp t))
(
VAR:
valid_alloc_range (
p,
n))
(
BRr:
buffers_related btrest ((
p,
n)::(
tp t))
(
tso_buffers ss t) (
sp t)),
tso_related_witt
(
mktsostate (
tupdate t btrest ts.(
tso_buffers))
tm')
(
tupdate t ((
p,
n)::(
tp t))
tp)
ss sp.
Proof.
Lemma tfree_preserves_tso_related_witt:
forall ts tp ss sp t btrest btptrest tm'
p n
(
REL:
tso_related_witt ts tp ss sp)
(
ABIt:
apply_buffer_item (
BufferedFree p MObjStack)
ts.(
tso_mem) =
Some tm')
(
Bt:
ts.(
tso_buffers)
t =
BufferedFree p MObjStack ::
btrest)
(
Etpt:
tp t = (
p,
n)::
btptrest)
(
RNIN:
range_not_in (
p,
n) (
sp t))
(
BRr:
buffers_related btrest btptrest
(
tso_buffers ss t) (
sp t)),
tso_related_witt
(
mktsostate (
tupdate t btrest ts.(
tso_buffers))
tm')
(
tupdate t btptrest tp)
ss sp.
Proof.
Inductive tso_related_witt_sf (
ts :
tso_state)
(
tp :
partitioning)
(
ss :
tso_state)
(
sp :
partitioning)
:
Prop :=
|
tso_related_witt_sf_intro:
forall
(
US:
unbuffer_safe ts)
(
FS:
tso_fin_sup ss)
(
TREL:
tso_related_witt ts tp ss sp),
tso_related_witt_sf ts tp ss sp.
Definition tso_related_sf ts ss :=
exists tp,
exists sp,
tso_related_witt_sf ts tp ss sp.
Lemma sf_rel_sim:
forall ts t ss bi b m'
(
TREL:
tso_related_sf ts ss)
(
Bt:
ss.(
tso_buffers)
t =
bi ::
b)
(
ABIs:
apply_buffer_item bi ss.(
tso_mem) =
Some m'),
exists ts',
tso_related_sf ts' (
mktsostate (
tupdate t b ss.(
tso_buffers))
m').
Proof.
Lemma alloc_stack_src_buff_impl_part_update_succ:
forall ts tp ss sp t bi sbr
(
REL:
tso_related_witt_sf ts tp ss sp)
(
Bs:
ss.(
tso_buffers)
t =
bi ::
sbr),
part_update bi (
sp t) <>
None.
Proof.
Lemma tso_pc_rel_valid_alloc_range_src_buff:
forall {
ts tp ss sp t p n k sbr}
(
REL:
tso_related_witt_sf ts tp ss sp)
(
Bs:
ss.(
tso_buffers)
t =
BufferedAlloc p n k ::
sbr),
valid_alloc_range (
p,
n) /\
restricted_pointer p (
tso_mem ss).
Proof.
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
(
REL:
tso_related_sf ts ss)
(
Bt:
ss.(
tso_buffers)
t =
bi ::
sbr)
(
NSI:
non_stack_item bi),
exists ts',
exists tbr,
tso_related_sf ts'
ss /\
ts'.(
tso_buffers)
t =
bi ::
tbr.
Proof.
Lemma tso_rel_sf_range_allocated:
forall ts ss p n k,
tso_related_sf ts ss ->
range_allocated (
p,
n)
k ss.(
tso_mem) ->
exists r',
range_inside (
p,
n)
r' /\
range_allocated r'
k ts.(
tso_mem).
Proof.
intros ts ss p n k [
tp [
sp TWREL]]
RA.
inv TWREL.
inv TREL.
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 (
mrwp_alloc_in MRPs RA)
as [
t INPs].
destruct (
PI _ _ INPs)
as [
r [
RIN INPt]].
exists r.
split.
done.
apply (
mrwp_in_alloc MRPt INPt).
Qed.
Lemma tso_rel_sf_non_stack_alloc_contr:
forall ts ss r k pi ni ki b t,
tso_related_sf 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 alloc_stack_src_buff_impl_tgt_partition:
forall ts ss t p n sbr
(
REL:
tso_related_sf ts ss)
(
Bt:
ss.(
tso_buffers)
t =
BufferedAlloc p n MObjStack ::
sbr),
exists ts',
exists r,
exists tp,
exists sp,
tso_related_witt_sf ts'
tp ss sp /\
range_inside (
p,
n)
r /\
In r (
tp t) /\
range_not_in (
p,
n) (
sp t).
Proof.
Lemma pointer_in_range_list_in:
forall p l,
pointer_in_range_list p l =
true ->
exists n,
In (
p,
n)
l.
Proof.
intros p.
induction l as [|[
p'
n']
l IH].
done.
simpl;
destruct (
Ptr.eq_dec p p')
as [-> |
N].
intro.
eexists.
left;
reflexivity.
intro H.
destruct (
IH H).
eexists;
right;
eassumption.
Qed.
Lemma alloc_unbuffer_safe:
forall p n k t ss ts ss'
ab
(
REL:
tso_related_sf ts ss)
(
USs:
unbuffer_safe ss')
(
Eab:
ab =
nil \/
ab =
BufferedAlloc p n k ::
nil)
(
Ebs:
ss.(
tso_buffers)
t =
ss'.(
tso_buffers)
t ++
ab)
(
Ebo:
forall t',
t' <>
t ->
ss.(
tso_buffers)
t' =
ss'.(
tso_buffers)
t')
(
RAS:
forall r k (
RA:
range_allocated r k ss'.(
tso_mem)),
range_allocated r k ss.(
tso_mem)),
unbuffer_safe ss.
Proof.
Unbuffer safety for free/write fail simulation.
Inductive tso_related_fw (
ts :
tso_state)
(
ss :
tso_state)
:
Prop :=
|
tso_related_witt_fw_intro:
forall tp sp
(
USs:
unbuffer_safe ss)
(
REL:
tso_related_witt ts tp ss sp),
tso_related_fw ts ss.
Definition write_or_free (
bi :
buffer_item) :=
match bi with
|
BufferedFree _ _ =>
True
|
BufferedWrite _ _ _ =>
True
|
_ =>
False
end.
Definition writes_or_frees (
b :
list buffer_item) :=
forall bi (
IN:
In bi b),
write_or_free bi.
Lemma tso_pc_related_unsafe_store_sim:
forall ts ss t bi tbr
(
TREL:
tso_related_fw ts ss)
(
TB:
ts.(
tso_buffers)
t =
bi ::
tbr)
(
WF:
write_or_free bi),
apply_buffer_item bi ts.(
tso_mem) <>
None.
Proof.
Lemma tso_related_fw_sim:
forall {
bi ts tm'
tbr ss t}
(
ABIt:
apply_buffer_item bi ts.(
tso_mem) =
Some tm')
(
Bt:
ts.(
tso_buffers)
t =
bi ::
tbr)
(
TREL:
tso_related_fw ts ss),
exists ss',
tso_related_fw (
mktsostate (
tupdate t tbr ts.(
tso_buffers))
tm')
ss'.
Proof.
Lemma unbuffer_safety_rev_write_free_gen:
forall t ts ts'
ss fw
(
FS:
tso_fin_sup ts)
(
TREL:
tso_related_fw ts ss)
(
US:
unbuffer_safe ts')
(
DAL:
writes_or_frees fw)
(
SBT:
ts.(
tso_buffers)
t =
ts'.(
tso_buffers)
t ++
fw)
(
SBO:
forall t',
t' <>
t ->
ts.(
tso_buffers)
t' =
ts'.(
tso_buffers)
t')
(
MR:
mrestr ts.(
tso_mem) =
mrestr ts'.(
tso_mem))
(
RAS:
forall r k (
RA:
range_allocated r k ts.(
tso_mem)),
range_allocated r k ts'.(
tso_mem)),
unbuffer_safe ts.
Proof.