Commit b3159ec2 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'fix_and_cinc' into 'master'

Fix and conditional increment example

See merge request !19
parents fcd5c1de 31b7db5f
Pipeline #17179 failed with stage
in 15 minutes and 17 seconds
......@@ -91,6 +91,7 @@ theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v
theories/hocap/parfib.v
theories/logatom/cinc.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
......
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-05-31.0.5c07c3be") | (= "dev") }
"coq-iris" { (= "dev.2019-06-03.2.b368c861") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
From iris.algebra Require Import excl auth agree frac list cmra.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
(** Using prophecy variables with helping: implementing conditional counter from
"Logical Relations for Fine-Grained Concurrency" by Turon et al. (POPL 2013) *)
(** * Implementation of the functions. *)
(*
new_counter() :=
let c = ref (injL 0) in
let f = ref false in
ref (f, c)
*)
Definition new_counter : val :=
λ: <>,
let: "c" := ref (ref (InjL #0)) in
let: "f" := ref #true in
("f", "c").
(*
set_flag(ctr, b) :=
ctr.1 <- b
*)
Definition set_flag : val :=
λ: "ctr" "b",
Fst "ctr" <- "b".
(*
complete(c, f, x, n, p) :=
Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
*)
Definition complete : val :=
λ: "c" "f" "x" "n" "p",
Resolve (CAS "c" "x" (ref (InjL (if: !"f" then "n" + #1 else "n")))) "p" (ref #()) ;; #().
(*
get(c, f) :=
let x = !c in
match !x with
| injL n => n
| injR (n, p) => complete c f x n p; get(c, f)
*)
Definition get : val :=
rec: "get" "ctr" :=
let: "f" := Fst "ctr" in
let: "c" := Snd "ctr" in
let: "x" := !"c" in
match: !"x" with
InjL "n" => "n"
| InjR "args" =>
complete "c" "f" "x" (Fst "args") (Snd "args") ;;
"get" "ctr"
end.
(*
cinc(c, f) :=
let x = !c in
match !x with
| injL n =>
let p := new proph in
let y := ref (injR (n, p)) in
if CAS(c, x, y) then complete(c, f, y, n, p)
else cinc(c, f)
| injR (n, p) =>
complete(c, f, x, n, p);
cinc(c, f)
*)
Definition cinc : val :=
rec: "cinc" "ctr" :=
let: "f" := Fst "ctr" in
let: "c" := Snd "ctr" in
let: "x" := !"c" in
match: !"x" with
InjL "n" =>
let: "p" := NewProph in
let: "y" := ref (InjR ("n", "p")) in
if: CAS "c" "x" "y" then complete "c" "f" "y" "n" "p" ;; Skip
else "cinc" "ctr"
| InjR "args'" =>
complete "c" "f" "x" (Fst "args'") (Snd "args'") ;;
"cinc" "ctr"
end.
(** ** Proof setup *)
(** To represent histories of allocated locations, we need some helper lemmas
about suffixes on lists. *)
Section suffixes.
Lemma suffix_trans (h1 h2 h3 : list loc) :
h1 `suffix_of` h2
h2 `suffix_of` h3
h1 `suffix_of` h3.
Proof.
intros [? ->] [? ->]. rewrite app_assoc. by eexists.
Qed.
Lemma suffix_eq (h1 h2 : list loc) :
h1 `suffix_of` h2
h2 `suffix_of` h1
h1 = h2.
Proof.
intros [xs ->] [ys Heq]. rewrite <- app_nil_l in Heq at 1. rewrite app_assoc in Heq.
apply app_inv_tail, eq_sym in Heq. by apply app_eq_nil in Heq as [_ ->].
Qed.
Lemma suffix_in (h1 h2 : list loc) l :
h1 `suffix_of` h2
In l h1
In l h2.
Proof.
destruct h1 as [|y ys]; first done.
intros Hs Hin. destruct Hs as [l2' ->]. apply in_or_app. by right.
Qed.
Lemma suffix_in_head (h1 h2 : list loc) l :
h1 `suffix_of` h2
Some l = head h1
In l h2.
Proof.
destruct h1 as [|y ys]; first done.
intros Hs [=->]. eapply suffix_in; first done. apply in_eq.
Qed.
(** A helper lemma that will come up in the proof of [complete] *)
Lemma nodup_suffix_contradiction (l1 l2 l3 : loc) (H1 H2 H3 : list loc) :
Some l1 = hd_error H1
Some l2 = hd_error H2
Some l3 = hd_error H3
In l3 H1
H1 `suffix_of` H2
H2 `suffix_of` H3
l2 l3
NoDup H3
False.
Proof.
intros Heq Heq' Heq'' Hin Hs Hs' Hn Hd.
destruct Hs' as [xs ->]. destruct Hs as [ys ->]. destruct (in_split _ _ Hin) as (x & y & ->).
do 2 rewrite app_assoc in Hd. apply NoDup_remove_2 in Hd.
(* xs, ys, and x must be empty *)
destruct xs as [|x' xs]; last first.
{ simpl in *. inversion Heq''. subst.
contradict Hd. by left. }
destruct ys as [|y' ys]; last first.
{ simpl in *. inversion Heq''; subst.
contradict Hd. by left. }
destruct x as [|z' zs]; last first.
{ simpl in *. inversion Heq''; subst.
contradict Hd. by left. }
simpl in *. inversion Heq'; done.
Qed.
End suffixes.
(** Resource algebra for histories *)
Section histories.
Inductive hist :=
| histv (h : list loc) : hist
| histbot : hist.
Inductive hist_equiv : Equiv hist :=
| Hist_equiv h1 h2 : h1 = h2 h1 h2.
Existing Instance hist_equiv.
Instance hist_equiv_Equivalence : @Equivalence hist equiv.
Proof.
split.
- move => [|]; by constructor.
- move => [?|] []; inversion 1; subst; by constructor.
- move => [?|] [] [];
inversion 1; inversion 1; subst; by constructor.
Qed.
Canonical Structure histC : ofeT := discreteC hist.
Instance hist_valid : Valid hist :=
λ x, match x with histv _ => True | histbot => False end.
Instance hist_op : Op hist := λ h1 h2,
match h1, h2 with
| histv h1', histv h2' =>
if decide (h1' `suffix_of` h2')
then h2
else if decide (h2' `suffix_of` h1')
then h1
else histbot
| _, _ =>
histbot
end.
Arguments op _ _ !_ !_ /.
Instance hist_PCore : PCore hist := Some.
Global Instance hist_op_comm: Comm equiv hist_op.
Proof.
intros [h1|] [h2|]; auto. simpl.
case_decide as H1; [case_decide as H2|auto]; last auto.
constructor. destruct H1. subst. destruct H2.
rewrite <- app_nil_l in H at 1. rewrite app_assoc in H.
by apply app_inv_tail, eq_sym, app_eq_nil in H as [-> ->].
Qed.
Global Instance hist_op_idemp : IdemP eq hist_op.
Proof. intros [|]; [by simpl; rewrite decide_True|auto]. Qed.
Lemma hist_op_l h1 h2 (Le: h1 `suffix_of` h2) :
histv h1 histv h2 = histv h2.
Proof. simpl. case_decide; done. Qed.
Lemma hist_op_r h1 h2 (Le: h1 `suffix_of` h2) :
histv h2 histv h1 = histv h2.
Proof.
simpl. case_decide.
- f_equal. by apply suffix_eq.
- by case_decide.
Qed.
Global Instance hist_op_assoc: Assoc equiv (op: Op hist).
Proof.
intros [h1|] [h2|] [h3|]; eauto; simpl.
- repeat (case_decide; auto).
+ rewrite !hist_op_l; auto. etrans; eauto.
+ simpl. repeat case_decide; last done.
* destruct H as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
** contradict H1. by apply suffix_app_r.
** contradict H0. by apply suffix_app_r.
* contradict H1. by etrans.
+ rewrite hist_op_l; [by rewrite hist_op_r|auto].
+ rewrite !hist_op_r; auto. by etrans.
+ simpl. rewrite !decide_False; auto.
+ simpl. rewrite !decide_False; auto.
+ simpl. case_decide.
* exfalso. apply H. by etrans.
* case_decide; last done. exfalso.
destruct H4 as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
** contradict H0. by apply suffix_app_r.
** contradict H. by apply suffix_app_r.
- simpl. repeat case_decide; auto.
Qed.
Lemma hist_included h1 h2 :
histv h1 histv h2 h1 `suffix_of` h2.
Proof.
split.
- move => [[?|]]; simpl; last by inversion 1.
case_decide.
* inversion 1. naive_solver.
* case_decide; inversion 1; naive_solver.
- intros. exists (histv h2). by rewrite hist_op_l.
Qed.
Lemma hist_valid_op h1 h2 :
(histv h1 histv h2) h1 `suffix_of` h2 h2 `suffix_of` h1.
Proof. simpl. case_decide; first by left. case_decide; [by right|done]. Qed.
Lemma hist_core_self (X: hist) : core X = X.
Proof. done. Qed.
Instance hist_unit : Unit hist := histv nil.
Definition hist_ra_mixin : RAMixin hist.
Proof.
apply ra_total_mixin; eauto.
- intros [?|] [?|] [?|]; auto; inversion 1; naive_solver.
- by destruct 1; constructor.
- destruct 1. naive_solver.
- apply hist_op_assoc.
- apply hist_op_comm.
- intros ?. by rewrite hist_core_self idemp_L.
- intros [|] [|]; simpl; done.
Qed.
Canonical Structure histR := discreteR hist hist_ra_mixin.
Global Instance hist_cmra_discrete : CmraDiscrete histR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance hist_core (h: hist) : CoreId h.
Proof.
rewrite /CoreId. reflexivity.
Qed.
Definition hist_ucmra_mixin : UcmraMixin hist.
Proof.
split; [done| |auto]. intros [|]; [simpl|done]. done.
Qed.
Lemma hist_local_update h1 X h2 :
h1 `suffix_of` h2 (histv h1, X) ~l~> (histv h2, histv h2).
Proof.
intros Le. rewrite local_update_discrete.
move => [[h3|]|] /= ? Eq; split => //; last first; move : Eq.
- destruct X; by inversion 1.
- destruct X; rewrite /cmra_op /= => Eq;
repeat case_decide; auto; inversion Eq; subst; try naive_solver.
+ constructor. inversion H1. subst. f_equal. by apply suffix_eq.
+ constructor. inversion H2. subst. f_equal. apply suffix_eq; by etrans.
+ inversion H3; subst. by apply (suffix_trans _ _ _ H0) in Le.
Qed.
Canonical Structure histUR := UcmraT hist hist_ucmra_mixin.
End histories.
Definition histListUR := optionUR $ prodR fracR $ agreeR $ listC locC.
Definition historyUR := prodUR (authUR histListUR) (authUR histUR).
Definition flagUR := authR $ optionUR $ exclR boolC.
Definition numUR := authR $ optionUR $ exclR ZC.
Definition tokenUR := authR $ optionUR $ exclR valC.
Class cincG Σ := ConditionalIncrementG {
cinc_historyG :> inG Σ historyUR;
cinc_flagG :> inG Σ flagUR;
cinc_numG :> inG Σ numUR;
cinc_tokenG :> inG Σ tokenUR;
}.
Definition cincΣ : gFunctors :=
#[GFunctor historyUR; GFunctor flagUR; GFunctor numUR; GFunctor tokenUR].
Instance subG_cincΣ {Σ} : subG cincΣ Σ cincG Σ.
Proof. solve_inG. Qed.
Section conditional_counter.
Context {Σ} `{!heapG Σ, !cincG Σ}.
Context (N : namespace).
Local Definition stateN := N .@ "state".
Local Definition counterN := N .@ "counter".
Definition token : tokenUR :=
Excl' #().
Definition histList (H : list loc) (q : Qp) : histListUR :=
Some (q, to_agree H).
Definition half_history_frag (H : list loc) : historyUR :=
( (histList H (1/2)%Qp), (histv H)).
Definition full_history_frag (H : list loc) : historyUR :=
( (histList H 1%Qp), (histv H)).
Definition full_history_auth (H : list loc) : historyUR :=
( (histList H 1%Qp), (histv H)).
Definition hist_snapshot H : historyUR :=
( None, histv H).
Global Instance snapshot_persistent H γ_h : Persistent (own γ_h (hist_snapshot H)).
Proof.
apply own_core_persistent. rewrite /CoreId. done.
Qed.
(** Updating and synchronizing history RAs *)
Lemma sync_histories H1 H2 γ_h :
own γ_h (half_history_frag H1) - own γ_h (half_history_frag H2) - H1 = H2.
Proof.
iIntros "H1 H2". iCombine "H1" "H2" as "H". iPoseProof (own_valid with "H") as "H".
iDestruct "H" as %H. iPureIntro. destruct H as [[_ Hl1%agree_op_inv] _].
by apply to_agree_inj, leibniz_equiv in Hl1.
Qed.
Lemma add_half_histories (H : list loc) γ_h :
own γ_h (half_history_frag H) -
own γ_h (half_history_frag H) -
own γ_h (full_history_frag H).
Proof.
iIntros "H1 H2". iCombine "H1" "H2" as "H". done.
Qed.
Lemma update_history H H' l γ_h :
own γ_h (full_history_auth H) -
own γ_h (half_history_frag H) -
own γ_h (half_history_frag H') ==
own γ_h (full_history_auth (l :: H))
own γ_h (half_history_frag (l :: H))
own γ_h (half_history_frag (l :: H)).
Proof.
iIntros "H● H1◯ H2◯". iDestruct (sync_histories with "H1◯ H2◯") as %<-.
iDestruct (add_half_histories with "H1◯ H2◯") as "H◯".
iCombine "H● H◯" as "H". rewrite -own_op -own_op.
iApply (own_update with "H"). apply prod_update.
- apply auth_update, option_local_update. rewrite pair_op frac_op' agree_idemp.
rewrite Qp_div_2. apply exclusive_local_update. by constructor.
- apply auth_update. simpl. rewrite hist_op_l; last done.
by apply hist_local_update, suffix_cons_r.
Qed.
Lemma sync_snapshot H1 H2 H2' γ_h :
own γ_h (full_history_auth H1) - own γ_h ( H2', histv H2) - H2 `suffix_of` H1.
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H".
by iDestruct (own_valid with "H") as %[_ [Hs%hist_included _]%auth_both_valid].
Qed.
Lemma extract_snapshot H γ_h :
own γ_h (half_history_frag H) - own γ_h (hist_snapshot H).
Proof.
iIntros "H".
iAssert (own γ_h (half_history_frag H) own γ_h (hist_snapshot H))%I with "[H]" as "[_ H2]".
{ rewrite -own_op pair_op.
assert ( histList H (1 / 2) None = (histList H (1 / 2) None)) as Heq by apply auth_frag_op.
assert ( histv H histv H = (histv H histv H)) as Heq' by apply auth_frag_op.
rewrite Heq Heq' right_id. rewrite <- core_id_dup; first done. by rewrite /CoreId. }
rewrite intuitionistically_into_persistently.
by iApply persistent.
Qed.
Lemma sync_counter_values γ_n (n m : Z) :
own γ_n ( Excl' n) - own γ_n ( Excl' m) - n = m.
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". iDestruct (own_valid with "H") as "H".
by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
(** Updating and synchronizing the counter and flag RAs *)
Lemma sync_flag_values γ_n (b1 b2 : bool) :
own γ_n ( Excl' b1) - own γ_n ( Excl' b2) - b1 = b2.
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". iDestruct (own_valid with "H") as "H".
by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma update_counter_value γ_n (n1 n2 m : Z) :
own γ_n ( Excl' n1) - own γ_n ( Excl' n2) == own γ_n ( Excl' m) own γ_n ( Excl' m).
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". rewrite -own_op. iApply (own_update with "H").
by apply auth_update, option_local_update, exclusive_local_update.
Qed.
Lemma update_flag_value γ_n (b1 b2 b : bool) :
own γ_n ( Excl' b1) - own γ_n ( Excl' b2) == own γ_n ( Excl' b) own γ_n ( Excl' b).
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". rewrite -own_op. iApply (own_update with "H").
by apply auth_update, option_local_update, exclusive_local_update.
Qed.
Definition counter_content (γs : gname * gname * gname) (c : bool * Z) :=
(own γs.1.2 ( Excl' c.1) own γs.2 ( Excl' c.2))%I.
(** Definition of the invariant *)
Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
match vs with
| (#true , LitV (LitLoc l)) :: _ => Some l
| _ :: vs => val_to_some_loc vs
| _ => None
end.
Lemma val_to_some_loc_some vs l :
val_to_some_loc vs = Some l
v1 v2 vs', vs = (v1, v2) :: vs'
( (v1 = #true v2 = LitV (LitLoc l))
val_to_some_loc vs' = Some l).
Proof.
intros H. destruct vs as [|[v1 v2] vs']; first done.
exists v1, v2, vs'. split; first done.
destruct v1; try by right. destruct l0; try by right.
destruct b; try by right. destruct v2; try by right.
destruct l0; try by right. simpl in H. inversion H. by left.
Qed.
Inductive abstract_state : Set :=
| injl : Z abstract_state
| injr : Z proph_id abstract_state.
Definition own_token γ_t := (own γ_t token)%I.
Definition used_up l γ_h :=
( H, own γ_h (hist_snapshot H) In l H Some l head H)%I.
Definition not_done_state H l (γ_h : gname) :=
(own γ_h (half_history_frag H) Some l = head H)%I.
Definition pending_state P (n : Z) vs l_ghost (γ_h γ_n : gname) :=
(P match val_to_some_loc vs with None => True | Some l => l = l_ghost end own γ_n ( Excl' n))%I.
Definition accepted_state Q vs (l l_ghost : loc) (γ_h : gname) :=
(l_ghost {1/2} - match val_to_some_loc vs with None => True | Some l => l = l_ghost Q end)%I.
Definition done_state Q (l l_ghost : loc) (γ_t γ_h : gname) :=
((Q own_token γ_t) l_ghost - used_up l γ_h)%I.
Definition state_inv P Q (p : proph_id) n l l_ghost H γ_h γ_n γ_t : iProp Σ :=
( vs, proph p vs
((not_done_state H l γ_h
( pending_state P n vs l_ghost γ_h γ_n
accepted_state Q vs l l_ghost γ_h ))
done_state Q l l_ghost γ_t γ_h))%I.
Definition pau P Q γs :=
( P - AU << (b : bool) (n : Z), counter_content γs (b, n) >> @ ∖↑N,
<< counter_content γs (b, (if b then n + 1 else n)), COMM Q >>)%I.
Definition counter_inv γ_h γ_b γ_n f c :=
( (b : bool) (l : loc) (H : list loc) (q : Qp) (v : val),
f #b c #l l {q} v
own γ_h (full_history_auth H)
own γ_h (half_history_frag H)
([ list] l H, q, l {q} -)
Some l = head H NoDup H
own γ_b ( Excl' b)
(( (n : Z), v = InjLV #n own γ_h (half_history_frag H) own γ_n ( Excl' n))
( (n : Z) (p : proph_id), v = InjRV(#n,#p)
P Q l_ghost γ_t, inv stateN (state_inv P Q p n l l_ghost H γ_h γ_n γ_t)
pau P Q (γ_h, γ_b, γ_n))))%I.
Definition is_counter (γs : gname * gname * gname) (ctr : val) :=
( (γ_h γ_b γ_n : gname) (f c : loc),
⌜γs = (γ_h, γ_b, γ_n) ctr = (#f, #c)%V
inv counterN (counter_inv γ_h γ_b γ_n f c))%I.
Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
Global Instance counter_content_timeless γs ctr : Timeless (counter_content γs ctr) := _.
Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (injl 0).
(** A few more helper lemmas that will come up later *)
Lemma mapsto_valid_3 l v1 v2 q :
l v1 - l {q} v2 - False.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %Hv.
apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
Qed.
Instance in_dec (l : loc) H: Decision (In l H).
Proof.
induction H as [|a H IH].
- right. naive_solver.
- destruct (decide (l = a)).
+ left. naive_solver.
+ destruct IH; [ left | right]; naive_solver.
Qed.
Lemma nodup_fresh_loc l v H:
NoDup H l v - ([ list] l H, q, l {q} -) - NoDup (l :: H).
Proof.
intros Hd. iIntros "Hl Hls".
destruct (decide (In l H)) as [(x1 & x2 & ->)%in_split | Hn%NoDup_cons]; last done.
- destruct x1 as [|x1 x1s];
[ rewrite app_nil_l in Hd; rewrite app_nil_l; iDestruct "Hls" as "[Hl' _]" |
iDestruct "Hls" as "[_ [Hl' _]]" ];
iDestruct "Hl'" as (q v') "Hl'";