client.v 3.78 KB
 Robbert Krebbers committed Feb 24, 2016 1 ``````From barrier Require Import proof. `````` Ralf Jung committed Feb 22, 2016 2 ``````From program_logic Require Import auth sts saved_prop hoare ownership. `````` Ralf Jung committed Feb 22, 2016 3 4 ``````Import uPred. `````` Ralf Jung committed Feb 29, 2016 5 6 7 8 ``````Definition worker (n : Z) := (λ: "b" "y", wait "b" ;; (!"y") 'n)%L. Definition client := (let: "y" := ref '0 in let: "b" := newbarrier '() in Fork (Skip ;; Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;; "y" <- (λ: "z", "z" + '42) ;; signal "b")%L. `````` Ralf Jung committed Feb 22, 2016 9 10 `````` Section client. `````` Robbert Krebbers committed Feb 24, 2016 11 `````` Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace). `````` Ralf Jung committed Feb 22, 2016 12 13 `````` Local Notation iProp := (iPropG heap_lang Σ). `````` Ralf Jung committed Feb 29, 2016 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 `````` Definition y_inv q y : iProp := (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, (* TODO: '() conflicts with '(n + 42)... *) || f 'n {{ λ v, v = LitV (n + 42)%Z }})%I. Lemma y_inv_split q y : y_inv q y ⊑ (y_inv (q/2) y ★ y_inv (q/2) y). Proof. rewrite /y_inv. apply exist_elim=>f. rewrite -!(exist_intro f). rewrite heap_mapsto_op_split. ecancel [y ↦{_} _; y ↦{_} _]%I. by rewrite [X in X ⊑ _]always_sep_dup. Qed. Lemma worker_safe q (n : Z) (b y : loc) : (heap_ctx heapN ★ recv heapN N b (y_inv q y)) ⊑ || worker n (Loc b) (Loc y) {{ λ _, True }}. Proof. rewrite /worker. wp_lam. wp_let. ewp apply wait_spec. rewrite comm. apply sep_mono_r. apply wand_intro_l. rewrite sep_exist_r. apply exist_elim=>f. wp_seq. (* TODO these aprenthesis are rather surprising. *) (ewp apply: (wp_load heapN _ _ q f)); eauto with I. strip_later. (* hu, shouldn't it do that? *) rewrite -assoc. apply sep_mono_r. apply wand_intro_l. rewrite always_elim (forall_elim n) sep_elim_r sep_elim_l. apply wp_mono=>?. eauto with I. Qed. `````` Ralf Jung committed Feb 22, 2016 41 42 43 44 `````` Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊑ || client {{ λ _, True }}. Proof. intros ?. rewrite /client. `````` Ralf Jung committed Feb 29, 2016 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 `````` (ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y. apply wand_intro_l. wp_let. ewp eapply (newbarrier_spec heapN N (y_inv 1 y)); last done. rewrite comm. rewrite {1}[heap_ctx _]always_sep_dup -!assoc. apply sep_mono_r. apply forall_intro=>b. apply wand_intro_l. wp_let. ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm. rewrite [(|| _ {{ _ }} ★ _)%I]comm -!assoc assoc. apply sep_mono;last first. { (* The original thread, the sender. *) wp_seq. (ewp eapply wp_store); eauto with I. strip_later. rewrite assoc [(_ ★ y ↦ _)%I]comm. apply sep_mono_r, wand_intro_l. wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm. apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + '42)%L). apply sep_intro_True_r; first done. apply: always_intro. apply forall_intro=>n. wp_let. wp_op. by apply const_intro. } (* The two spawned threads, the waiters. *) ewp eapply recv_split. rewrite comm. apply sep_mono. { apply recv_mono. rewrite y_inv_split. done. } apply wand_intro_r. wp_seq. ewp eapply wp_fork. rewrite [heap_ctx _]always_sep_dup !assoc [(_ ★ recv _ _ _ _)%I]comm. rewrite -!assoc assoc. apply sep_mono. - wp_seq. by rewrite -worker_safe comm. - by rewrite -worker_safe. `````` Ralf Jung committed Feb 22, 2016 68 69 `````` Qed. End client. `````` Ralf Jung committed Feb 22, 2016 70 71 `````` Section ClosedProofs. `````` Ralf Jung committed Feb 23, 2016 72 `````` Definition Σ : iFunctorG := #[ heapGF ; barrierGF ]. `````` Ralf Jung committed Feb 22, 2016 73 74 75 76 `````` Notation iProp := (iPropG heap_lang Σ). Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}. Proof. `````` Ralf Jung committed Feb 23, 2016 77 `````` apply ht_alt. rewrite (heap_alloc ⊤ (nroot .@ "Barrier")); last first. `````` Ralf Jung committed Feb 22, 2016 78 `````` { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *) `````` Robbert Krebbers committed Feb 22, 2016 79 `````` by move=>? _. } `````` Ralf Jung committed Feb 22, 2016 80 `````` apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. `````` Robbert Krebbers committed Feb 24, 2016 81 `````` rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //. `````` Ralf Jung committed Feb 22, 2016 82 `````` (* This, too, should be automated. *) `````` Robbert Krebbers committed Feb 22, 2016 83 `````` by apply ndot_ne_disjoint. `````` Ralf Jung committed Feb 22, 2016 84 85 86 87 `````` Qed. Print Assumptions client_safe_closed. End ClosedProofs.``````