Set Implicit Arguments.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import PropositionalExtensionality.
Require Import List.
Require Import MyTactics.
Require Import MyClassicalChoice.
-------------------------------------------------------------------------
The type class STAR describes a monotonic separation algebra.
A resource could be an ordinary heap of references, which maps locations to
values; a heap of regions, which maps regions to sets of values; a heap of
monotonic references, which maps references to pairs of an ordering and a
value, and mandates monotonic updates; an integer, which represents a
number of time or space credits; etc. It is typically a Cartesian product
of several of these components.
A resource typically contains both duplicable information -- e.g. how many
references currently exist -- and linear information -- e.g. which
permission is held for each reference.
Class STAR (
resource :
Type) := {
Resources should support a commutative and associative separating
conjunction, represented as a three-place relation.
star:
resource ->
resource ->
resource ->
Prop;
star_commutative:
forall R1 R2 R,
star R1 R2 R ->
star R2 R1 R;
star_associative:
forall R1 R2 R3 R12 R123,
star R1 R2 R12 ->
star R12 R3 R123 ->
exists R23,
star R2 R3 R23 /\
star R1 R23 R123;
It is convenient (although perhaps somewhat artificial) to require star
to be deterministic, that is, to be a partial function. We formalize this
by stating that there should be a total function add that coincides with
star whenever star is defined.
Furthermore, it is convenient to require the function add to be
commutative and associative. This is not a consequence of the fact
that star is commutative and associative, because we require add
to be commutative and associative everywhere, including where star
is undefined. This might seem a strong requirement, but (perhaps by
luck) we are able to satisfy it.
Last, we require that, if R1 is split and if both pieces are compatible
with R2, then R1 itself is compatible with R2. This works even if
the split is not a valid one, that is, even if R1a and R1b are
actually not compatible.
The function add and its properties are not exploited in the type
soundness proof. They are used only in ResourcesReconfiguration, where
they simplify the construction of the resource reconfiguration tactic.
add:
resource ->
resource ->
resource;
star_deterministic:
forall R1 R2 R,
star R1 R2 R ->
R =
add R1 R2;
add_commutative:
forall R1 R2,
add R1 R2 =
add R2 R1;
add_associative:
forall R1 R2 R3,
add R1 (
add R2 R3) =
add (
add R1 R2)
R3;
compatible_split:
forall R1a R1b R2 R1a2 R1b2,
star R1a R2 R1a2 ->
star R1b R2 R1b2 ->
star (
add R1a R1b)
R2 (
add (
add R1a R1b)
R2);
Every resource R has a core neutral R. This core is obtained, intuitively
speaking, by keeping all duplicable information and discarding all linear
information.
neutral:
resource ->
resource;
The resource neutral R acts as a neutral element for R with respect to
star. That is, it is compatible with R, and adds nothing to it.
star_neutral:
forall R,
star R (
neutral R)
R;
Compatible resources have a common image through neutral. That is, if
star R1 R2 R holds, then R1, R2, and R have a common core.
compatible_implies_common_core:
forall R1 R2 R,
star R1 R2 R ->
neutral R1 =
neutral R;
There are several ways to define what it means for a resource R to be
duplicable. One is to state that two copies of R amount to one, that
is, star R R R holds. One other is to state that R is equal to its
core. The two definitions are equivalent. One implication is an axiom,
shown next, while the converse implication is derived below
(core_implies_duplicable). A third way would be to state that R is
duplicable if it is a core, that is, if there exists some resource R0
such that R = neutral R0. Again, this definition is equivalent to the
first one. One implication is the next axiom, while the converse
implication is derived below (duplicable_neutral).
Note that star R R R2 does not imply star R R R. A time credit, for
instance, is compatible with itself, yet it is not duplicable: two time
credits do not equal one.
duplicable_implies_core:
forall R,
star R R R ->
R =
neutral R;
If a duplicable resource is split, its parts are duplicable.
duplicable_split:
forall R1 R2 R,
star R1 R2 (
neutral R) ->
star R1 R1 R1;
The execution ordering rxo represents how the currently executing thread
is allowed to modify its own resource.
Note that, while it sounds reasonable for rxo to be transitive, and this
property does hold, it is actually not exploited anywhere.
rxo:
resource ->
resource ->
Prop;
rxo_reflexive:
forall R,
rxo R R;
rxo_transitive:
forall R1 R2 R3,
rxo R1 R2 ->
rxo R2 R3 ->
rxo R1 R3;
The information ordering represents how the currently executing thread is
allowed to modify some other (currently inactive) thread's resource.
That is, the information ordering describes the changes that can be
imposed to one thread by some other thread of execution.
rio:
resource ->
resource ->
Prop;
rio_reflexive:
forall R,
rio R R;
rio_transitive:
forall R1 R2 R3,
rio R1 R2 ->
rio R2 R3 ->
rio R1 R3;
The information ordering is compatible with separating conjunction in
the following sense: if we have a split and if the outside world requires
that the sum grow, then each summand is able to grow to reflect this.
Intuitively, the new duplicable information is simply sent down into
both sides of the split.
rio_star:
forall R1a R1b R1 R2,
star R1a R1b R1 ->
rio R1 R2 ->
exists R2a R2b,
star R2a R2b R2 /\
rio R1a R2a /\
rio R1b R2b;
The execution ordering is compatible with separating conjunction in
the following sense: if we have a split and if one summand decides
to grow according to rxo, then the other summand is able to grow
according to rio so that the sum grows with respect to rxo.
Intuitively, some new duplicable information is simply sent down into
the other summand, and the result still looks like an execution step
to the outside.
rxo_star:
forall R1a R1b R1 R2a,
star R1a R1b R1 ->
rxo R1a R2a ->
exists R2b R2,
star R2a R2b R2 /\
rio R1b R2b /\
rxo R1 R2;
rio_neutral:
forall R1 R2,
rio R1 R2 ->
rio (
neutral R1) (
neutral R2)
}.
Notation duplicable R :=
(
star R R R).
It makes sense to require that there exist at least one duplicable
resource, void, which intuitively describes the initial state of the
world, before the program begins to run. void is not used in the type
soundness proof, which is why we do not make it part of the type class
STAR. It is used only to type-check source programs: see for instance the
file WeakAffineRefWithAffineContent.v.
Class Void (
resource :
Type) (
S :
STAR resource) := {
The empty resource.
void:
resource;
The empty resource is duplicable.
duplicable_void:
duplicable void
}.
-------------------------------------------------------------------------
Tactics.
Obligation Tactic :=
try solve [
intuition (
subst;
eauto 6) ].
Ltac star_deterministic :=
match goal with
h:
star ?
R1 ?
R2 ?
R |-
_ =>
unpack (
star_deterministic _ _ _ h);
subst R
end.
Ltac star_comm a :=
match goal with h:
star ?
a1 ?
a2 a |-
_ =>
generalize (
star_commutative _ _ _ h);
clear h;
intro h end.
Ltac star_assoc_prelim a12 a23 :=
match goal with
|
h1:
star ?
a1 ?
a2 a12,
h2:
star a12 ?
a3 ?
a123 |-
_ =>
generalize (
star_associative _ _ _ _ _ h1 h2);
intros [
a23 [ ? ? ]]
end.
Lemma star_associative_reverse:
forall A (
IA :
STAR A)
R1 R2 R3 R23 R123,
star R2 R3 R23 ->
star R1 R23 R123 ->
exists R12,
star R1 R2 R12 /\
star R12 R3 R123.
Proof.
intros.
star_comm R123. star_comm R23.
star_assoc_prelim R23 R21. star_comm R21. star_comm R123.
eauto.
Qed.
Ltac star_assoc a12 a23 :=
match goal with
|
h1:
star ?
a1 ?
a2 a12,
h2:
star a12 ?
a3 ?
a123 |-
_ =>
generalize (
star_associative _ _ _ _ _ h1 h2);
intros [
a23 [ ? ? ]]
|
h1:
star ?
a1 ?
a2 a12,
h2:
star ?
a3 a12 ?
a123 |-
_ =>
generalize (
star_associative_reverse _ _ _ _ _ _ h1 h2);
intros [
a23 [ ? ? ]]
end.
Ltac star_associative :=
match goal with h1:
star ?
R1 ?
R2 ?
R12,
h2:
star ?
R12 ?
R3 ?
R123 |-
_ =>
unpack (
star_associative _ _ _ _ _ h1 h2)
end.
Ltac rio_star :=
match goal with
|
h1:
star ?
R1a ?
R1b ?
R1,
h2:
rio ?
R1 ?
R2 |-
_ =>
unpack (
rio_star _ _ _ _ h1 h2)
end.
-------------------------------------------------------------------------
The following properties are valid in all monotonic separation algebras.
Lemma core_implies_duplicable:
forall A (
IA :
STAR A) (
R :
A),
R =
neutral R ->
star R R R.
Proof.
If we have a1 * a2 = a and a * b = ab, where b is duplicable, then
we have (a1 * b) * (a2 * b) = ab.
Lemma send_down_both_ways:
forall A (
IA :
STAR A) (
a1 a2 a b ab :
A),
star a1 a2 a ->
star a b ab ->
duplicable b ->
exists a1b a2b,
star a1 b a1b /\
star a2 b a2b /\
star a1b a2b ab.
Proof.
intros.
star_assoc a a2b.
star_comm a2b.
star_assoc b ba2.
star_comm ba2.
star_assoc a2b a1b.
eauto.
Qed.
Implicit Arguments send_down_both_ways [
A IA a1 a2 a b ab ].
Lemma star_neutral_generalized:
forall A (
IA :
STAR A) (
R1 R2 :
A),
neutral R1 =
neutral R2 ->
star R1 (
neutral R2)
R1.
Proof.
Lemma duplicable_split_2:
forall A (
IA :
STAR A) (
R1 R2 R :
A),
star R1 R2 (
neutral R) ->
duplicable R2.
Proof.
Lemma duplicable_split_left:
forall A (
IA :
STAR A) (
R1 R2 R :
A),
star R1 R2 R ->
duplicable R ->
duplicable R1.
Proof.
Lemma duplicable_split_right:
forall A (
IA :
STAR A) (
R1 R2 R :
A),
star R1 R2 R ->
duplicable R ->
duplicable R2.
Proof.
Lemma neutral_idempotent:
forall A (
IA :
STAR A) (
R :
A),
neutral (
neutral R) =
neutral R.
Proof.
Lemma duplicable_neutral:
forall A (
IA :
STAR A) (
R :
A),
duplicable (
neutral R).
Proof.
Lemma star_neutral_map:
forall A (
IA :
STAR A) (
R1 R2 R :
A),
star R1 R2 R ->
star (
neutral R1) (
neutral R2) (
neutral R).
Proof.
Lemma star_neutral_bang:
forall A (
IA :
STAR A) (
R1 R2 R :
A),
star R1 R2 R ->
duplicable R2 ->
star (
neutral R1)
R2 (
neutral R).
Proof.
Hint Extern 1 =>
rewrite neutral_idempotent :
resources.
Hint Extern 1 (
star _ _ (
neutral _)) =>
eapply star_neutral_map :
resources.
Hint Resolve duplicable_neutral :
resources.
-------------------------------------------------------------------------
A type class for inhabited types.
Class Inhabited (
A:
Type) :
Type :=
{
inhabitant :
A }.
Instance inhabited_unit :
Inhabited unit := {
inhabitant :=
tt }.
-------------------------------------------------------------------------
The natural integers form a monotonic separation algebra, which can be used
(for instance) to represent time credits.
Program Instance nat_resource :
STAR nat := {
star n1 n2 n :=
n1 +
n2 =
n;
add n1 n2 :=
n1 +
n2;
neutral n := 0;
rxo n1 n2 :=
n1 >=
n2;
rio n1 n2 :=
n1 =
n2
}.
Program Instance nat_void :
Void nat_resource := {
void := 0
}.
Next Obligation.
reflexivity.
Qed.
-------------------------------------------------------------------------
Options over a type A form a monotonic separation algebra, where None
represents no permission and Some a represents a permission over an
object whose current description is a.
Splitting permissions is simple: permissions cannot be split, so one of the
two sides must have no permission.
Inductive option_star A :
option A ->
option A ->
option A ->
Prop :=
|
OptionStarLeft:
forall p,
option_star (@
None _)
p p
|
OptionStarRight:
forall p,
option_star p (@
None _)
p.
Hint Constructors option_star.
Properties of option_star.
Lemma option_star_duplicable_implies_core:
forall A (
p :
option A),
option_star p p p ->
p = (@
None _).
Proof.
inversion 1; auto.
Qed.
Lemma option_star_owned_left:
forall A (
p1 p2 p :
option A)
a,
option_star p1 p2 p ->
p1 =
Some a ->
p =
Some a.
Proof.
inversion 1; congruence.
Qed.
Lemma option_star_owned_right:
forall A (
p1 p2 p :
option A)
a,
option_star p1 p2 p ->
p2 =
Some a ->
p =
Some a.
Proof.
inversion 1; congruence.
Qed.
Lemma option_star_owned_exclusive:
forall A (
p1 p2 p :
option A)
a,
option_star p1 p2 p ->
p2 =
Some a ->
p1 = (@
None _).
Proof.
inversion 1; congruence.
Qed.
Lemma option_star_notowned_left:
forall A (
p1 p2 p :
option A),
option_star p1 p2 p ->
p = (@
None _) ->
p1 = (@
None _).
Proof.
inversion 1; congruence.
Qed.
Lemma option_star_notowned_right:
forall A (
p1 p2 p :
option A),
option_star p1 p2 p ->
p = (@
None _) ->
p2 = (@
None _).
Proof.
inversion 1; congruence.
Qed.
Hint Resolve option_star_duplicable_implies_core option_star_owned_left
option_star_owned_right option_star_owned_exclusive
option_star_notowned_left option_star_notowned_right :
option_star_inversion.
Definition option_add A (
IA :
Inhabited A) (
p1 p2 :
option A) :
option A :=
match p1,
p2 with
|
None,
p
|
p,
None =>
p
|
Some _,
Some _ =>
The definition of option_star does not allow this case to arise,
so, in principle, here we can return anything we like. However, we
must make sure that option_add is commutative and associative.
This turns out not to be so easy. Returning None satisfies
commutativity, but not associativity. So, we must return Some a
for some fixed element a. In order to choose such an element, we
require the type A to be inhabited.
Some inhabitant
end.
The ordering rxo over permissions reflects how a thread can decide to
alter the permissions that it possesses. It is permitted to abandon the
ownership of a resource, but not to spontaneously acquire it: hence the
following definition.
Definition option_rxo A (
p1 p2 :
option A) :=
p1 = (@
None _) ->
p2 = (@
None _).
Hint Unfold option_rxo.
The ordering rio over permissions is just equality: when a thread is
inactive, the permissions that it holds do not change.
Program Instance option_resource A (
IA :
Inhabited A) :
STAR (
option A) := {
star := @
option_star A;
add :=
option_add IA;
neutral p := @
None A;
rxo := @
option_rxo A;
rio p1 p2 :=
p1 =
p2
}.
Next Obligation.
inversion 2; constructor.
Qed.
Next Obligation.
inversion 2; inversion 1; subst; intuition eauto.
Qed.
Next Obligation.
inversion 1; subst; auto. destruct R; auto.
Qed.
Next Obligation.
destruct R1; destruct R2; auto.
Qed.
Next Obligation.
destruct R1; destruct R2; destruct R3; simpl; auto.
Qed.
Next Obligation.
introv h1 h2.
dependent destruction h1;
dependent destruction h2;
eauto;
repeat match goal with p:
option A |-
_ =>
destruct p end;
simpl;
eauto.
Qed.
Next Obligation.
inversion 2; auto.
Qed.
Next Obligation.
inversion 3; auto.
Qed.
Next Obligation.
unfold option_rxo; inversion 2; destruct R2a; intuition eauto. discriminate.
Qed.
Program Instance option_void :
forall A (
IA :
Inhabited A),
Void (
option_resource A IA) := {
void :=
None
}.
Next Obligation.
econstructor.
Qed.
-------------------------------------------------------------------------
Monotonic sets form a monotonic separation algebra.
A monotonic set is a product of a Boolean permission and a set of values
of type A, represented as a predicate over values of type A.
In order to re-use some code, the Boolean permission is encoded as an
option on unit. Some tt means that the permission is held; the owner of
the monotonic set is allowed to make it grow. None means that the
permission is not held.
Record mSet A :=
mkmSet {
owned:
option unit;
mset:
A ->
Prop
}.
Program Instance monotonic_set_resource A :
STAR (
mSet A) := {
The contents of the set must be identical on both sides: it is considered
duplicable, so even if one does not own the set, it is permitted to know
that a certain value is a member of the set.
star R1 R2 R :=
star (
owned R1) (
owned R2) (
owned R) /\
mset R1 =
mset R /\
mset R2 =
mset R;
In the definition of add, we use set intersection, because it is
commutative and associative.
add R1 R2 :=
mkmSet (
add (
owned R1) (
owned R2)) (
fun (
a :
A) =>
mset R1 a /\
mset R2 a);
neutral R :=
mkmSet (
neutral (
owned R)) (
mset R);
In both rxo and rio, the set can only grow with time. In rxo, the
set can grow strictly only if we are the owner, whereas, in rio, the
set can grow strictly only if we are not the owner. Both definitions
reflect the fact that only the owner of the set can make it grow.
rxo R1 R2 :=
rxo (
owned R1) (
owned R2) /\
(
forall a,
mset R1 a ->
mset R2 a) /\
(
owned R1 =
None ->
forall a,
mset R2 a ->
mset R1 a);
rio R1 R2 :=
rio (
owned R1) (
owned R2) /\
(
forall a,
mset R1 a ->
mset R2 a) /\
(
owned R1 =
Some tt ->
forall a,
mset R2 a ->
mset R1 a)
}.
Next Obligation.
Next Obligation.
intros.
unpack.
star_assoc (
owned R12)
ownedR23.
exists (
mkmSet ownedR23 (
mset R3)).
simpl.
intuition eauto;
congruence.
Qed.
Ltac prove_msets_equal :=
extensionality a;
eapply prop_ext;
intuition congruence.
Next Obligation.
destruct R.
intros.
unpack.
f_equal.
eapply star_deterministic;
eauto.
simpl in *.
prove_msets_equal.
Qed.
Next Obligation.
Next Obligation.
destruct R1;
destruct R2;
destruct R3.
f_equal.
eapply add_associative.
simpl.
prove_msets_equal.
Qed.
Next Obligation.
intros.
repeat match goal with R:
mSet A |-
_ =>
destruct R end;
simpl in *.
intuition subst.
repeat match goal with h:
option_star _ _ _ |-
_ =>
depelim h end;
repeat match goal with p:
option unit |-
_ =>
destruct p end;
simpl;
eauto.
prove_msets_equal.
prove_msets_equal.
Qed.
Next Obligation.
simpl. eauto.
Qed.
Next Obligation.
intros.
repeat match goal with R:
mSet A |-
_ =>
destruct R end;
simpl in *.
intuition eauto.
repeat match goal with h:
option_star _ _ _ |-
_ =>
depelim h end;
congruence.
Qed.
Next Obligation.
simpl. introv [ h [ ? ? ]]. destruct R; simpl. dependent destruction h; eauto.
Qed.
Next Obligation.
simpl.
introv [
h [ ? ? ]].
dependent destruction h;
repeat match goal with
|
h:
owned _ =
None |-
_ =>
try rewrite h in *;
clear h
|
h:
None =
owned _ |-
_ =>
try rewrite <-
h in *;
clear h
end;
intuition eauto.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
intuition eauto.
eapply rio_transitive;
eauto.
Permission is held in R1, so it must be held in R2 as well, since
R1 and R2 are related by rio, which is just equality here.
unfold rio in *;
simpl in *.
repeat match goal with
|
h:
owned _ =
Some _ |-
_ =>
try rewrite h in *;
clear h
|
h:
Some _ =
owned _ |-
_ =>
try rewrite <-
h in *;
clear h
end.
intuition eauto.
Qed.
Next Obligation.
intros.
unpack.
forwards [
owned2a [
owned2b [ ? [ ? ? ]]]]: (@
rio_star (
option unit)).
eassumption.
eassumption.
exists (
mkmSet owned2a (
mset R2)) (
mkmSet owned2b (
mset R2)).
simpl.
repeat match goal with h:
mset _ =
mset _ |-
_ =>
try rewrite h in *;
clear h end.
intuition eauto with option_star_inversion.
Qed.
Next Obligation.
intros.
unpack.
forwards [
owned2b [
owned2 [ ? [ ? ? ]]]]: (@
rxo_star (
option unit)).
eassumption.
eassumption.
exists (
mkmSet owned2b (
mset R2a)) (
mkmSet owned2 (
mset R2a)).
simpl.
repeat match goal with h:
mset _ =
mset _ |-
_ =>
try rewrite h in *;
clear h end.
intuition eauto with option_star_inversion.
Qed.
Next Obligation.
intros. unpack. simpl. intuition eauto. discriminate.
Qed.
Program Instance Void_mset A :
Void (
monotonic_set_resource A) := {
void :=
mkmSet None (
fun x =>
False)
}.
Next Obligation.
intros; simpl. intuition eauto.
Qed.
Definition empty_mset (
A :
Type) :
mSet A :=
mkmSet (
Some tt) (
fun x =>
False).
Definition singleton_mset A (
a :
A) :=
mkmSet (
Some tt) (
fun x =>
x =
a).
Definition extend_mset A (
R :
mSet A) (
a :
A) :=
mkmSet (
owned R) (
fun x =>
x =
a \/
mset R x).
Lemma star_extend_mset:
forall A (
R1 R2 R :
mSet A) (
a :
A),
star R1 R2 R ->
star (
extend_mset R1 a) (
extend_mset R2 a) (
extend_mset R a).
Proof.
unfold extend_mset, star. simpl. intuition eauto; extensionality b; congruence.
Qed.
Lemma rxo_extend_mset:
forall A (
R :
mSet A) (
a :
A),
owned R =
Some tt ->
rxo R (
extend_mset R a).
Proof.
intros. unfold rxo. simpl. intuition eauto. congruence.
Qed.
Lemma rio_extend_mset:
forall A (
R :
mSet A) (
a :
A),
owned R =
None ->
rio R (
extend_mset R a).
Proof.
intros. unfold rio. simpl. intuition eauto. congruence.
Qed.
-------------------------------------------------------------------------
The product of two monotonic separation algebras forms a monotonic
separation algebra.
Program Instance pair_resource A B (
IA :
STAR A) (
IB :
STAR B) :
STAR (
A *
B) := {
star R1 R2 R :=
let (
RA1,
RB1) :=
R1 in
let (
RA2,
RB2) :=
R2 in
let (
RA,
RB) :=
R in
star RA1 RA2 RA /\
star RB1 RB2 RB;
add R1 R2 :=
let (
RA1,
RB1) :=
R1 in
let (
RA2,
RB2) :=
R2 in
(
add RA1 RA2,
add RB1 RB2);
neutral R :=
let (
RA,
RB) :=
R in
(
neutral RA,
neutral RB);
rxo R1 R2 :=
let (
RA1,
RB1) :=
R1 in
let (
RA2,
RB2) :=
R2 in
rxo RA1 RA2 /\
rxo RB1 RB2;
rio R1 R2 :=
let (
RA1,
RB1) :=
R1 in
let (
RA2,
RB2) :=
R2 in
rio RA1 RA2 /\
rio RB1 RB2
}.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
RA RB ] [ ? ? ].
split;
eapply star_commutative;
eauto.
Qed.
Next Obligation.
intros ? ? ? ? [ RA1 RB1 ] [ RA2 RB2 ] [ RA3 RB3 ] [ RA12 RB12 ] [ RA123 RB123 ] [ ? ? ] [ ? ? ].
star_assoc RA12 RA23.
star_assoc RB12 RB23.
exists (RA23, RB23).
eauto.
Qed.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
RA RB ] [ ? ? ].
f_equal;
eapply star_deterministic;
eauto.
Qed.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ].
f_equal;
eapply add_commutative.
Qed.
Next Obligation.
intros.
repeat match goal with R: (
A *
B)%
type |-
_ =>
destruct R end.
f_equal;
eapply add_associative.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
RA RB ] [ ? ? ].
split;
eapply duplicable_split;
eauto.
Qed.
Next Obligation.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
RA3 RB3 ] [ ? ? ] [ ? ? ].
split;
eapply rxo_transitive;
eauto.
Qed.
Next Obligation.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
RA3 RB3 ] [ ? ? ] [ ? ? ].
split;
eapply rio_transitive;
eauto.
Qed.
Next Obligation.
intros ? ? ? ? [
RA1a RB1a ] [
RA1b RB1b ] [
RA1 RB1 ] [
RA2 RB2 ] [
hsa hsb ] [
hra hrb ].
forwards [
RA2a [
RA2b [ ? [ ? ? ]]]]: (@
rio_star A).
eexact hsa.
eexact hra.
forwards [
RB2a [
RB2b [ ? [ ? ? ]]]]: (@
rio_star B).
eexact hsb.
eexact hrb.
exists (
RA2a,
RB2a) (
RA2b,
RB2b).
tauto.
Qed.
Next Obligation.
intros ? ? ? ? [
RA1a RB1a ] [
RA1b RB1b ] [
RA1 RB1 ] [
RA2a RB2a ] [
hsa hsb ] [
hra hrb ].
forwards [
RA2b [
RA2 [ ? [ ? ? ]]]]: (@
rxo_star A).
eexact hsa.
eexact hra.
forwards [
RB2b [
RB2 [ ? [ ? ? ]]]]: (@
rxo_star B).
eexact hsb.
eexact hrb.
exists (
RA2b,
RB2b) (
RA2,
RB2).
tauto.
Qed.
Next Obligation.
intros ? ? ? ? [
RA1 RB1 ] [
RA2 RB2 ] [
hra hrb ].
split;
eapply rio_neutral;
eauto.
Qed.
Program Instance Void_pair_resource
A B (
IA :
STAR A) (
IB :
STAR B) (
VA :
Void IA) (
VB :
Void IB)
:
Void (
pair_resource A B IA IB) := {
void := (@
void A IA VA, @
void B IB VB)
}.
Next Obligation.
intros; simpl. destruct VA, VB. simpl. eauto.
Qed.
-------------------------------------------------------------------------
Allocation maps over a monotonic separation algebra form a monotonic
separation algebra.
An allocation map is a map of addresses to values, with support for dynamic
allocation of fresh addresses. Addresses are implemented as natural
integers. An allocation map is implemented as a pair of an allocation limit
and a function of addresses to values.
Record aMap A :=
mkaMap {
The allocation limit is the next available address.
alimit:
nat;
The allocation map per se maps addresses to values. For simplicity, we
make it a total function, but of course its value at and above the
allocation limit is irrelevant.
amap:
nat ->
A
}.
Ltac dam :=
repeat match goal with R:
aMap _ |-
_ =>
destruct R end.
Program Instance map_resource A (
IA :
STAR A) :
STAR (
aMap A) := {
The allocation limit must be the same on both sides of star. This is
required so that when one side decides to allocate a fresh address, the
new address really is globally fresh. Then, at each address r, the
value is split according to the relation star at type A.
star R1 R2 R :=
alimit R1 =
alimit R /\
alimit R2 =
alimit R /\
forall r,
star (
amap R1 r) (
amap R2 r) (
amap R r);
In the definition of add, we preserve the allocation limit if both
sides agree on the allocation limit, otherwise we produce a dummy
allocation limit. This definition satisfies commutativity and
associativity.
add R1 R2 :=
mkaMap (
if eq_nat_dec (
alimit R1) (
alimit R2)
then (
alimit R1)
else 0) (
fun r =>
add (
amap R1 r) (
amap R2 r));
neutral R :=
mkaMap (
alimit R) (
fun r =>
neutral (
amap R r));
The allocation limit can only grow with time; new addresses can be
allocated by this thread and by other threads. What happens at each
pre-existing adress r is dictated by the orderings rxo and rio
at type A.
rxo R1 R2 :=
alimit R1 <=
alimit R2 /\
forall r,
r <
alimit R1 ->
rxo (
amap R1 r) (
amap R2 r);
rio R1 R2 :=
alimit R1 <=
alimit R2 /\
forall r,
r <
alimit R1 ->
rio (
amap R1 r) (
amap R2 r)
}.
Next Obligation.
Next Obligation.
introv [ ? [?
h1 ]] [ ? [ ?
h2 ]].
Here, by exploiting the fact that star is deterministic, we are able to
name the existential witness, and avoid the need for some version of the
axiom of choice.
exists (
mkaMap (
alimit R1) (
fun a =>
add (
amap R2 a) (
amap R3 a))).
simpl.
split;
splits;
try congruence;
intro r.
specializes h1 r.
specializes h2 r.
star_assoc (
amap R12 r)
R23r.
replace (
add (
amap R2 r) (
amap R3 r))
with R23r;
eauto using star_deterministic.
specializes h1 r.
specializes h2 r.
star_assoc (
amap R12 r)
R23r.
replace (
add (
amap R2 r) (
amap R3 r))
with R23r;
eauto using star_deterministic.
Qed.
Next Obligation.
intros.
destruct R.
simpl in *.
intuition subst.
f_equal.
by_cases;
auto.
extensionality r.
eauto using star_deterministic.
Qed.
Next Obligation.
intros.
f_equal.
by_cases;
congruence.
extensionality r.
eapply add_commutative.
Qed.
Next Obligation.
intros.
f_equal.
by_cases;
simpl in *;
auto.
extensionality r.
eapply add_associative.
Qed.
Next Obligation.
Next Obligation.
intros.
dam.
simpl.
intuition eauto using star_neutral.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
intros.
unpack.
Intuitively, here is what we have to prove:
assert (
fact:
forall r,
exists R2ar R2br,
star R2ar R2br (
amap R2 r) /\
(
r <
alimit R1a ->
rio (
amap R1a r)
R2ar) /\
(
r <
alimit R1b ->
rio (
amap R1b r)
R2br)
).
intro.
destruct (
le_gt_dec (
alimit R1)
r).
Sub-case: above alimit R1.
We split the resources in R2 in an arbitrary way. (In practice,
these resources are likely to be absent, but we do not impose this
requirement in the definition of rio.
exists (
neutral (
amap R2 r)) (
amap R2 r).
repeat split;
try solve [
intro;
false;
omega ].
eauto using star_commutative,
star_neutral.
Sub-case: below alimit R1.
forwards [
R2ar [
R2br [ ? [ ? ? ]]]]: (@
rio_star A).
eauto.
eauto.
intuition eauto.
Now, since, for every r, there exist suitable R1ar and R2br,
this means that there exist functions from r to these witnesses.
Exhibit these maps and use them to build the desired resources.
generalize (
binary_choice _ fact).
intros [
map1 [
map2 properties ]].
exists (
mkaMap (
alimit R2)
map1).
exists (
mkaMap (
alimit R2)
map2).
repeat split;
simpl;
try solve [
omega |
intro r;
specializes properties r;
intuition eauto ].
Qed.
Next Obligation.
intros.
unpack.
Intuitively, here is what we have to prove:
assert (
fact:
forall r,
exists R2br R2r,
star (
amap R2a r)
R2br R2r /\
(
r <
alimit R1b ->
rio (
amap R1b r)
R2br) /\
(
r <
alimit R1 ->
rxo (
amap R1 r)
R2r)
).
intro.
destruct (
le_gt_dec (
alimit R1)
r).
Sub-case: above alimit R1.
R2b gets no new permissions -- its permission map is None
above reglimit R1. R2 inherits its permissions from R2a;
this reflects the new permissions that have been acquired during
this execution step.
exists (
neutral (
amap R2a r)) (
amap R2a r).
repeat split;
try solve [
intro;
false;
omega ].
eauto using star_neutral.
Sub-case: below alimit R1.
forwards [
R2br [
R2r [ ? [ ? ? ]]]]: (@
rxo_star A).
eauto.
eapply (
H1 r).
eauto.
intuition eauto.
Now, since, for every r, there exist suitable R2br and R2b,
this means that there exist functions from r to these witnesses.
Exhibit these maps and use them to build the desired resources.
generalize (
binary_choice _ fact).
intros [
map1 [
map2 properties ]].
exists (
mkaMap (
alimit R2a)
map1).
exists (
mkaMap (
alimit R2a)
map2).
repeat split;
simpl;
try solve [
omega |
intro r;
specializes properties r;
intuition eauto ].
Qed.
Next Obligation.
Program Instance void_map_resource A (
IA :
STAR A) (
VA :
Void IA) :
Void (
map_resource A IA) := {
void :=
mkaMap 0 (
fun _ =>
void)
}.
Next Obligation.
intros; destruct VA; simpl. intuition eauto.
Qed.
Lemma star_amap:
forall A (
IA :
STAR A) (
R1 R2 R :
aMap A) (
r :
nat),
star R1 R2 R ->
star (
amap R1 r) (
amap R2 r) (
amap R r).
Proof.
introv [ ? [ ? ? ]]. eauto.
Qed.
Definition allocate A (
R :
aMap A) (
a :
A) :=
mkaMap
(1 +
alimit R)
(
fun r =>
if le_gt_dec (
alimit R)
r then a else amap R r)
.
Lemma star_allocate:
forall A (
IA :
STAR A) (
R1 R2 R :
aMap A) (
a1 a2 a :
A),
star R1 R2 R ->
star a1 a2 a ->
star (
allocate R1 a1) (
allocate R2 a2) (
allocate R a).
Proof.
simpl; intuition eauto. by_cases; eauto.
Qed.
Lemma allocate_rxo:
forall A (
IA :
STAR A) (
R :
aMap A) (
a :
A),
rxo R (
allocate R a).
Proof.
intros.
unfold rxo,
allocate;
simpl.
split.
omega.
intros.
by_cases.
eauto using rxo_reflexive.
Qed.
Lemma allocate_rio:
forall A (
IA :
STAR A) (
R :
aMap A) (
a :
A),
rio R (
allocate R a).
Proof.
intros.
unfold rio,
allocate;
simpl.
split.
omega.
intros.
by_cases.
eauto using rio_reflexive.
Qed.
Definition update A (
R :
aMap A) (
r :
nat) (
a :
A) :=
mkaMap
(
alimit R)
(
fun r' =>
if eq_nat_dec r'
r then a else amap R r').
Lemma amap_update:
forall A (
R :
aMap A) (
r :
nat) (
a :
A),
amap (
update R r a)
r =
a.
Proof.
intros; simpl. by_cases; auto.
Qed.
Lemma star_update:
forall A (
IA :
STAR A) (
R1 R2 R :
aMap A) (
r :
nat) (
a1 a2 a :
A),
star R1 R2 R ->
star a1 a2 a ->
star (
update R1 r a1) (
update R2 r a2) (
update R r a).
Proof.
unfold update. simpl. intuition eauto; by_cases; subst; simpl; eauto.
Qed.
Lemma star_update_owned:
forall A (
IA :
STAR A) (
R1 R2 R :
aMap A) (
r :
nat) (
a :
A),
star R1 R2 R ->
amap R2 r =
neutral a ->
star (
update R1 r a)
R2 (
update R r a).
Proof.
unfold update.
simpl.
introv ?
eq.
intuition eauto;
by_cases;
subst;
simpl;
eauto.
rewrite eq.
eapply star_neutral.
Qed.
Lemma rxo_update:
forall A (
IA :
STAR A) (
R :
aMap A) (
r :
nat) (
a :
A),
rxo (
amap R r)
a ->
rxo R (
update R r a).
Proof.
intros.
unfold rxo.
simpl.
split.
omega.
intros.
by_cases.
subst.
eauto.
eauto using rxo_reflexive.
Qed.
Lemma rio_update:
forall A (
IA :
STAR A) (
R :
aMap A)
r (
a :
A),
rio (
amap R r)
a ->
rio R (
update R r a).
Proof.
intros.
unfold rio.
simpl.
intuition eauto.
by_cases;
simpl;
subst;
eauto using rio_reflexive.
Qed.
-------------------------------------------------------------------------
Lists of elements drawn from a monotonic separation algebra form a monotonic
separation algebra.
Inductive list_star (
A :
Type) (
star :
A ->
A ->
A ->
Prop) :
list A ->
list A ->
list A ->
Prop :=
|
ListStarNil:
list_star star nil nil nil
|
ListStarCons:
forall M1 M2 M m1 m2 m,
list_star star M1 M2 M ->
star m1 m2 m ->
list_star star (
m1 ::
M1) (
m2 ::
M2) (
m ::
M).
Hint Constructors list_star.
Fixpoint list_add (
A :
Type) (
add :
A ->
A ->
A) (
M1 M2 :
list A) :
list A :=
match M1,
M2 with
|
m1 ::
M1,
m2 ::
M2 =>
add m1 m2 ::
list_add add M1 M2
|
_,
_ =>
nil
end.
Inductive list_forall2 (
A :
Type) (
P :
A ->
A ->
Prop) :
list A ->
list A ->
Prop :=
|
ListForall2Nil:
list_forall2 P nil nil
|
ListForall2Cons:
forall M1 M2 m1 m2,
list_forall2 P M1 M2 ->
P m1 m2 ->
list_forall2 P (
m1 ::
M1) (
m2 ::
M2).
Hint Constructors list_forall2.
Program Instance list_resource A (
IA :
STAR A) :
STAR (
list A) := {
star :=
list_star star;
add :=
list_add add;
neutral :=
map neutral;
rxo :=
list_forall2 rxo;
rio :=
list_forall2 rio
}.
Next Obligation.
Next Obligation.
introv h. generalize R3 R123; clear R3 R123.
induction h; inversion 1; eauto; subst.
forwards: IHh. eassumption.
star_assoc m m23.
unpack. eauto.
Qed.
Next Obligation.
Next Obligation.
induction R1;
dependent destruction R2;
simpl;
auto.
f_equal.
eapply add_commutative.
auto.
Qed.
Next Obligation.
induction R1;
dependent destruction R2;
dependent destruction R3;
simpl;
auto.
f_equal.
eapply add_associative.
auto.
Qed.
Next Obligation.
introv h.
generalize R1b R1b2;
clear R1b R1b2.
induction h;
inversion 1;
simpl;
eauto using compatible_split.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
intros A IA.
for some reason, dependent destruction/induction do not work.
cut (
forall R1 R2 R,
list_star star R1 R2 R ->
R1 =
R ->
R2 =
R ->
R =
map neutral R);
eauto.
induction 1;
intros;
subst;
simpl;
eauto.
repeat match goal with h:
_ ::
_ =
_ ::
_ |-
_ =>
injection h;
clear h;
intros;
subst end.
f_equal;
eauto using duplicable_implies_core.
Qed.
Next Obligation.
intros A IA.
cut (
forall R1 R2 nR :
list A,
list_star star R1 R2 nR ->
forall R,
nR =
map neutral R ->
list_star star R1 R1 R1);
eauto.
induction 1;
intros;
destruct R;
simpl in *;
try discriminate;
eauto.
repeat match goal with h:
_ ::
_ =
_ ::
_ |-
_ =>
injection h;
clear h;
intros;
subst end.
eauto using duplicable_split.
Qed.
Next Obligation.
Next Obligation.
introv h.
generalize R3;
clear R3.
induction h;
inversion 1;
subst;
simpl;
eauto using rxo_transitive.
Qed.
Next Obligation.
Next Obligation.
introv h.
generalize R3;
clear R3.
induction h;
inversion 1;
subst;
simpl;
eauto using rio_transitive.
Qed.
Next Obligation.
introv h.
generalize R2;
clear R2.
induction h;
inversion 1;
subst;
simpl;
eauto.
forwards [
m1p [
m2p [ ? [ ? ? ]]]]: (@
rio_star A).
eassumption.
eassumption.
forwards [
M1p [
M2p [ ? [ ? ? ]]]]:
IHh.
eassumption.
exists (
m1p ::
M1p) (
m2p ::
M2p).
eauto 6.
Qed.
Next Obligation.
introv h.
generalize R2a;
clear R2a.
induction h;
inversion 1;
subst;
simpl;
eauto.
forwards [
m1p [
m2p [ ? [ ? ? ]]]]: (@
rxo_star A).
eassumption.
eassumption.
forwards [
M1p [
M2p [ ? [ ? ? ]]]]:
IHh.
eassumption.
exists (
m1p ::
M1p) (
m2p ::
M2p).
eauto 6.
Qed.
Next Obligation.
Program Instance void_list_resource A (
IA :
STAR A) :
Void (
list_resource A IA) := {
void :=
nil
}.
Next Obligation.
econstructor.
Qed.
List star preserves length.
Lemma star_length_eq:
forall A (
IA :
STAR A) (
M1 M2 M :
list A),
star M1 M2 M ->
length M2 =
length M.
Proof.
induction 1; simpl; intros; eauto.
Qed.
Lemma star_length_le:
forall A (
IA :
STAR A) (
M1 M2 M :
list A),
star M1 M2 M ->
forall k,
k <=
length M ->
k <=
length M2.
Proof.