Commit de2c8673 by David Swasey

Add fetch and increment.

parent 32230c36
......@@ -409,6 +409,25 @@ Section fundamental.
iExists (#v false); eauto.
Qed.
Lemma bin_log_related_FAI Γ e e'
(IHHtyped : Γ e log e' : (Tref TNat)) :
Γ FAI e log FAI e' : TNat.
Proof.
iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind FAICtx v v' "[Hv #Hiv]"
('`IHHtyped _ _ _ j (FAICtx :: K)).
iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
iApply wp_atomic; eauto.
iInv (logN .@ (l,l')) as ([w w']) "[Hw1 >[Hw2 #Hw]]" "Hclose"; simpl.
iDestruct "Hw" as (n) "[%%]"; subst. iModIntro.
iApply (wp_fai with "Hw1"). iNext. iIntros "Hw1".
iMod (step_fai with "[Hv Hw2]") as "[Hv Hw2]";
[solve_ndisj|by iFrame|].
iMod ("Hclose" with "[Hw1 Hw2]").
{ iNext. iExists (_,_); iFrame; auto. }
iModIntro. iExists _; iFrame; auto.
Qed.
Theorem binary_fundamental Γ e τ :
Γ ⊢ₜ e : τ Γ e log e : τ.
Proof.
......@@ -438,5 +457,6 @@ Section fundamental.
- eapply bin_log_related_load; eauto.
- eapply bin_log_related_store; eauto.
- eapply bin_log_related_CAS; eauto.
- eapply bin_log_related_FAI; eauto.
Qed.
End fundamental.
......@@ -141,5 +141,14 @@ Section typed_interp.
+ iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
- (* FAI *)
smart_wp_bind FAICtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iApply wp_atomic.
iInv (logN .@ l) as (w) "[Hw1 >Hw2]" "Hclose".
iDestruct "Hw2" as (n) "%"; subst.
iApply (wp_fai with "Hw1"). iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1]"); eauto.
iExists (#nv S n); eauto.
Qed.
End typed_interp.
......@@ -46,7 +46,8 @@ Module F_mu_ref_conc.
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
(* Compare and swap used for fine-grained concurrency *)
| CAS (e0 : expr) (e1 : expr) (e2 : expr).
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAI (e : expr).
Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
......@@ -142,7 +143,8 @@ Module F_mu_ref_conc.
| StoreRCtx (v1 : val)
| CasLCtx (e1 : expr) (e2 : expr)
| CasMCtx (v0 : val) (e2 : expr)
| CasRCtx (v0 : val) (v1 : val).
| CasRCtx (v0 : val) (v1 : val)
| FAICtx.
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
......@@ -168,6 +170,7 @@ Module F_mu_ref_conc.
| CasLCtx e1 e2 => CAS e e1 e2
| CasMCtx v0 e2 => CAS (of_val v0) e e2
| CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
| FAICtx => FAI e
end.
Definition state : Type := gmap loc val.
......@@ -227,7 +230,10 @@ Module F_mu_ref_conc.
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
head_step (CAS (Loc l) e1 e2) σ (# true) (<[l:=v2]>σ) [].
head_step (CAS (Loc l) e1 e2) σ (# true) (<[l:=v2]>σ) []
| FaiS l n σ :
σ !! l = Some (#nv n)
head_step (FAI (Loc l)) σ (#n n) (<[l:=#nv S n]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -311,6 +317,7 @@ Definition is_atomic (e : expr) : Prop :=
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| CAS e1 e2 e3 => is_Some (to_val e1) is_Some (to_val e2)
is_Some (to_val e3)
| FAI e => is_Some (to_val e)
| _ => False
end.
Local Hint Resolve language.val_irreducible.
......
......@@ -112,6 +112,18 @@ Section lang_rules.
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_fai E l n :
{{{ l ↦ᵢ #nv n }}} FAI (Loc l) @ E
{{{ RET (#nv n); l ↦ᵢ #nv S n }}}.
Proof.
iIntros (Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_fork E e Φ :
(|={E}=> Φ UnitV) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof.
......
......@@ -270,6 +270,31 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_fai E ρ j K l n:
nclose specN E
spec_ctx ρ j fill K (FAI (Loc l)) l ↦ₛ (#nv n)
={E}= j fill K (of_val (#nv n)) l ↦ₛ (#nv S n).
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
iDestruct (own_valid_2 with "Hown Hl")
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#n n)))). }
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree (#nv S n))); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (#n n)]> tp), (<[l:=#nv S n]>σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_rec E ρ j K e1 e2 v :
to_val e2 = Some v nclose specN E
spec_ctx ρ j fill K (App (Rec e1) e2)
......
......@@ -65,6 +65,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| TCAS e1 e2 e3 τ :
EqType τ Γ ⊢ₜ e1 : Tref τ Γ ⊢ₜ e2 : τ Γ ⊢ₜ e3 : τ
Γ ⊢ₜ CAS e1 e2 e3 : TBool
| TFAI e : Γ ⊢ₜ e : Tref TNat Γ ⊢ₜ FAI e : TNat
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Lemma typed_subst_invariant Γ e τ s1 s2 :
......
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