Commit caf53b92 authored by Armaël Guéneau's avatar Armaël Guéneau

Merge branch 'linear-credits' into 'master'

Modify the logic to add a notion of "affine" resources, i.e. resources
that can be garbage collected. Previously, all resources were implicitly
affine and could be garbage collected.

This new distinction is relevant for time credits: a negative number of
time credits does not entails False anymore, but only a positive number
of credits can be garbage collected. This adds a side-condition to the 
garbage collecting rule in presence of credits, but simplifies the rule
to split a number of credits: [$(n+m) = $n * $m] now always hold, while
it previously required to prove [0 <= n] and [0 <= m] as side
conditions.
parents 95663185 b82651fb
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Require Export CFLibCredits.
Ltac xpay_core tt ::= xpay_nat_core tt.
Notation "'\$' x" := (\$_nat x)
(at level 40, format "\$ x") : heap_scope.
......@@ -505,6 +505,7 @@ Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2)
Ltac xgc_remove_hprop H :=
eapply (@local_gc_pre_on H);
[ try xlocal
| try affine
| hsimpl
| xtag_pre_post ].
......@@ -557,6 +558,7 @@ Ltac xgc_post_if_not_evar_then cont :=
Lemma local_gc_pre_all : forall B Q (F:~~B) H,
is_local F ->
affine H ->
F \[] Q ->
F H Q.
Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
......@@ -1067,7 +1069,7 @@ Qed.
Ltac xlet_core cont0 cont1 cont2 :=
apply local_erase;
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
match goal with |- cf_let ?F1 (fun x => _) ?H ?Q =>
cont0 tt;
split; [ | cont1 x; cont2 tt ];
xtag_pre_post
......@@ -1618,7 +1620,7 @@ Lemma xret_lemma : forall B (v:B) H (Q:B->hprop),
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. eapply (@local_gc_pre_on (\GC)).
auto. hchanges W. apply~ local_erase. hsimpl.
auto. affine. hchanges W. apply~ local_erase. hsimpl.
Qed.
(* Lemma used by [xret] and [xret_no_gc]
......@@ -3832,15 +3834,11 @@ Tactic Notation "xname_post" ident(X) :=
used before a credit split operation, e.g. to replace
[$n] with [$a \* $b], when [n = a + b].
LATER: add demos for this tactic.
LATER: add demos for this tactic.
*)
Ltac xcredit goal :=
match goal with
| |- context[\$_nat goal] =>
idtac (* no need to rewrite *)
| |- context[\$_nat ?n] =>
math_rewrite (n = goal :> nat)
| |- context[\$ goal] =>
idtac (* no need to rewrite *)
| |- context[\$ ?n] =>
......@@ -3853,10 +3851,10 @@ Ltac xcredit goal :=
(** [xpay] applys to a goal of the form [(Pay_ ;; F1) H Q].
It is used to eliminate the call to Pay, by spending one credit.
[xpay (n + m)] where [n] and [m] are numbers such that:
where [n] denotes the remainder, and [m] denotes the
payment that need to be performed (e.g. 1).
payment that need to be performed (e.g. 1).
WARNING: the interface of the latter might change.
LATER: add demos for this tactic. *)
......@@ -3867,15 +3865,11 @@ Ltac xpay_start tt :=
Ltac xpay_core tt :=
xpay_start tt; [ unfold pay_one; hsimpl | ].
Ltac xpay_nat_core tt :=
xpay_start tt; [ rewrite pay_one_nat; hsimpl | ].
Tactic Notation "xpay" := xpay_core tt.
Ltac xpay_on_impl goal :=
xcredit goal;
first [ rewrite credits_int_split_eq
| rewrite credits_nat_split_eq ];
first [ rewrite credits_split_eq ];
xpay.
Tactic Notation "xpay" constr(goal) :=
......@@ -3886,8 +3880,8 @@ Tactic Notation "xpay" constr(goal) :=
(* ** [xpay_skip] *)
(** [xpay_skip] is used to skip the paying of one credit;
use it for development purposes only.
use it for development purposes only.
LATER: add demos for this tactic. *)
Ltac xpay_fake tt :=
......@@ -3903,22 +3897,31 @@ Tactic Notation "xpay_skip" := xpay_fake tt.
(*--------------------------------------------------------*)
(* ** [xgc_credit] *)
(* [xgc_credit_core HP] applies to a term [HP] that is an inequality
between two credit expressions, e.g. [m <= n].
(* [xgc_credit_core HP] applies to a term [HP] that is an inequality
between two credit expressions, e.g. [m <= n].
This inequality is used to change [\$n] to [\$m] in the
precondition of the goal.
LATER: add demos for this tactic. *)
*)
Ltac xgc_credit_core HP :=
let H := fresh in
let E := fresh in
destruct (credits_nat_le_rest HP) as (H&E);
xchange E; [ chsimpl | xgc H; clear H E ].
destruct (credits_le_rest HP) as (H&HA&E);
xchange E; [ xgc H; clear H HA E; hclean ].
Tactic Notation "xgc_credit" constr(HP) :=
xgc_credit_core HP.
Lemma demo_xgc_credit_core : forall m n B (F : ~~B) Q,
m <= n ->
is_local F ->
F (\$m) Q ->
F (\$n) Q.
Proof.
introv H L HH.
xgc_credit H.
assumption.
Qed.
(*--------------------------------------------------------*)
(* ** [xskip_credits] *)
......@@ -3927,8 +3930,8 @@ Tactic Notation "xgc_credit" constr(HP) :=
in the goal, by replacing [\$ x] with the empty heap predicate \[].
Implementing using [skip_credits] then [hsimpl].
Should only be used for development purpose.
Should only be used for development purpose.
LATER: add demos for this tactic. *)
Ltac xskip_credits_base :=
......
......@@ -32,6 +32,13 @@ Parameter Array : forall A, list A -> loc -> hprop.
the ownership of single cells, each of which being
described using heap_is_single. *)
Parameter affine_Array : forall A t (L: list A), affine (t ~> Array L).
(* TODO: prove this *)
Hint Resolve affine_Array : affine.
(* Expose that [array A] (defined in Array_ml) is defined as [loc]. *)
Hint Transparent array : affine.
(* -------------------------------------------------------------------------- *)
(* The length of an array is at most [Sys.max_array_length]. This could be
......
......@@ -25,8 +25,8 @@ Hint Extern 1 (RegisterSpec not) => Provide not_spec.
- [==] at type [loc] implements comparison of locations
- [==] in general, if it returns true, then implies logical equality.
The first specification is used by default.
Use [xapp_spec infix_eq_eq_gen_spec] for the latter.
The first specification is used by default.
Use [xapp_spec infix_eq_eq_gen_spec] for the latter.
*)
Parameter infix_eq_eq_loc_spec : curried 2%nat infix_eq_eq__ /\
......@@ -142,9 +142,9 @@ Hint Extern 1 (RegisterSpec infix_star__) => Provide infix_star_spec.
Hint Extern 1 (RegisterSpec infix_slash__) => Provide infix_slash_spec.
Hint Extern 1 (RegisterSpec Pervasives_ml.mod) => Provide mod_spec.
Notation "x `/` y" := (Z.quot x y)
Notation "x `/` y" := (Z.quot x y)
(at level 69, right associativity) : charac.
Notation "x `mod` y" := (Z.rem x y)
Notation "x `mod` y" := (Z.rem x y)
(at level 69, no associativity) : charac.
(* TODO: check levels for these notations *)
......@@ -240,7 +240,7 @@ Hint Extern 1 (RegisterSpec asr) => Provide asr_spec.
(************************************************************)
(** References *)
Definition Ref {A} (v:A) (r:loc) :=
Definition Ref {A} (v:A) (r:loc) :=
r ~> `{ contents' := v }.
Axiom Ref_Heapdata : forall A,
......@@ -251,23 +251,31 @@ Existing Instance Ref_Heapdata.
(*
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
xunfold @Ref.
xunfold @Ref.
lets: star_is_single_same_loc.
hchange (@star_is_single_same_loc x). hsimpl.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
*)
Notation "r '~~>' v" := (hdata (Ref v) r)
(at level 32, no associativity) : heap_scope.
Lemma affine_Ref : forall A r (v: A), affine (r ~~> v).
Proof. intros. unfold Ref, hdata. affine. Qed.
Hint Resolve affine_Ref : affine.
(* Expose that [ref_ A] (defined in Pervasives_ml) is defined as [loc] *)
Hint Transparent ref_ : affine.
Lemma ref_spec : forall A (v:A),
app ref [v]
PRE \[]
app ref [v]
PRE \[]
POST (fun r => r ~~> v).
Proof using. xcf_go~. Qed.
Lemma infix_emark_spec : forall A (v:A) r,
app infix_emark__ [r]
app infix_emark__ [r]
INV (r ~~> v)
POST \[= v].
Proof using. xunfold @Ref. xcf_go~. Qed.
......@@ -289,8 +297,8 @@ Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;)
format "'App'' r `:= x") : charac.
Lemma incr_spec : forall (n:int) r,
app incr [r]
PRE (r ~~> n)
app incr [r]
PRE (r ~~> n)
POST (# r ~~> (n+1)).
Proof using. xcf_go~. Qed.
......@@ -309,7 +317,7 @@ Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.
(** Group of References *)
Axiom ref_spec_group : forall A (M:map loc A) (v:A),
app Pervasives_ml.ref [v]
app Pervasives_ml.ref [v]
PRE (Group Ref M)
POST (fun (r:loc) => Group Ref (M[r:=v]) \* \[r \notindom M]).
(* TODO: proof *)
......@@ -325,10 +333,10 @@ Qed.
Lemma infix_colon_eq_spec_group : forall `{Inhab A} (M:map loc A) (v:A) r,
r \indom M ->
app Pervasives_ml.infix_colon_eq__ [r v]
app Pervasives_ml.infix_colon_eq__ [r v]
PRE (Group Ref M)
POST (# Group Ref (M[r:=v])).
Proof using.
Proof using.
intros. rewrite~ (Group_rem r M). xapp. intros tt.
hchanges~ (Group_add' r M).
Qed.
......@@ -338,14 +346,14 @@ Qed.
(** Pairs *)
Lemma fst_spec : forall A B (x:A) (y:B),
app fst [(x,y)]
PRE \[]
app fst [(x,y)]
PRE \[]
POST \[= x].
Proof using. xcf_go~. Qed.
Lemma snd_spec : forall A B (x:A) (y:B),
app snd [(x,y)]
PRE \[]
app snd [(x,y)]
PRE \[]
POST \[= y].
Proof using. xcf_go~. Qed.
......@@ -356,9 +364,9 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec.
(************************************************************)
(** Unit *)
Lemma ignore_spec :
app ignore [tt]
PRE \[]
Lemma ignore_spec :
app ignore [tt]
PRE \[]
POST \[= tt].
Proof using. xcf_go~. Qed.
......@@ -392,7 +400,7 @@ Instance Ref_Heapdata : forall a A (T:htype A a),
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
unfold Ref. hdata_simpl. hextract as x1 x2.
hchange (@star_is_single_same_loc x). hsimpl.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
Open Local Scope heap_scope_advanced.
......@@ -402,7 +410,7 @@ Notation "'~~>' v" := (~> Ref (@Id _) v)
(*
Notation "l '~~>' v" := (r ~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope.
(at level 32, no associativity) : heap_scope.
*)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) r)
(at level 32, no associativity) : heap_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment