Commit 5f900155 authored by Amin Timany's avatar Amin Timany

Add symbol table example

parent 65cd332b
......@@ -80,6 +80,7 @@ theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel/F_mu_ref_conc/examples/symbol_table/symbol_nat.v
theories/logrel_heaplang/ltyping.v
theories/logrel_heaplang/ltyping_safety.v
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import auth list.
From iris.program_logic Require Import adequacy.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_unary.
Definition symbol_typ :=
TArrow
TUnit
(TExist (TProd (TArrow TUnit (TVar 0)) (TArrow (TVar 0) (TBool)))).
Definition symbol_nat : expr :=
Lam (LetIn (Alloc (#n 0))
(Pack
(Pair
(Lam (FAA (Var 1) (#n 1)))
(Lam (If
(BinOp Lt (Var 0) (Load (Var 1)))
(# true)
(App Unit Unit))
))
)
).
Section symbol_nat_sem_typ.
Context `{heapIG Σ, inG Σ (authUR mnatUR)}.
Definition Max_token γ m : iProp Σ := own γ ( (m : mnat)).
Definition Token γ m := own γ ( (S m : mnat)).
Lemma Token_init : (|==> γ, Max_token γ 0)%I.
Proof.
iApply own_alloc.
by apply auth_auth_valid.
Qed.
Lemma Token_alloc γ k : Max_token γ k == Max_token γ (k + 1) Token γ k.
Proof.
iIntros "Hk".
rewrite /Max_token /Token Nat.add_1_r; simpl.
iMod (own_update _ _ ( (S k : mnat) (S k : mnat)) with "Hk")
as "[$ $]"; last done.
apply auth_update_alloc.
by apply mnat_local_update; eauto.
Qed.
Lemma Token_lt γ k k' : Max_token γ k - Token γ k' - k' < k.
Proof.
iIntros "Hmt Htk".
rewrite /Max_token /Token; simpl.
by iDestruct (own_valid_2 with "Hmt Htk") as
%[?%mnat_included _]%auth_both_valid.
Qed.
Lemma symbol_nat_sem_typ : [] symbol_nat : symbol_typ.
Proof.
iIntros (? ? ?) "HΔ".
rewrite /symbol_nat /symbol_typ /interp_expr /=.
iDestruct (interp_env_length with "HΔ") as %?; destruct vs; last done.
asimpl.
iApply wp_value.
iAlways.
iIntros (? ?); simplify_eq; simpl.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply wp_alloc; first done.
iNext. iIntros (l) "Hl".
iApply wp_pure_step_later; auto. iNext. asimpl.
iMod Token_init as (γ) "Hmt".
iMod (inv_alloc (nroot .@ "tk") _ ( t, l ↦ᵢ (#nv t) Max_token γ t)
with "[Hl Hmt]") as "#Hinv".
{ unfold Max_token. by iNext; iExists _; iFrame. }
iApply wp_value.
iAlways.
iExists (λne v, m, v = #nv m Token γ m)%I.
iSplit.
{ iPureIntro; apply _. }
iExists _; iSplit; first done.
iExists _, _; iSplit; first done.
iSplit.
- iAlways.
iIntros (? ?); simplify_eq; simpl.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply wp_atomic.
iInv (nroot.@"tk") as (t) "[Hl Hmt]" "Hcl".
iModIntro.
iApply (wp_FAA with "Hl").
iNext. iIntros "Hl".
iMod (Token_alloc with "Hmt") as "[Hmt Htk]".
iMod ("Hcl" with "[Hl Hmt]") as "_".
{ iNext; iExists _; iFrame. }
eauto.
- iAlways.
iIntros (w). iDestruct 1 as (m ?) "Htk"; simplify_eq.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [IfCtx _ _])).
iApply (wp_bind (fill [BinOpRCtx _ (#nv _)])).
iApply wp_atomic.
iInv (nroot.@"tk") as (t) "[Hl Hmt]" "Hcl".
iModIntro.
iApply (wp_load with "Hl").
iNext. iIntros "Hl".
iDestruct (Token_lt with "Hmt Htk") as %?.
iMod ("Hcl" with "[Hl Hmt]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
simpl.
iApply wp_pure_step_later; auto. iNext.
simpl. destruct lt_dec; last done. simpl.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value; eauto.
Qed.
End symbol_nat_sem_typ.
......@@ -338,7 +338,7 @@ Section fundamental.
iDestruct "Hv" as (τi Hτi (v1, v2) Hvv) "#Hvv"; simplify_eq /=.
iApply wp_pure_step_later; auto. iNext.
iApply fupd_wp.
iMod (step_Pack with "[Hj]") as "Hj"; eauto.
iMod (step_pack with "[Hj]") as "Hj"; eauto.
asimpl.
iModIntro.
iApply wp_wand_r; iSplitL.
......@@ -378,7 +378,7 @@ Section fundamental.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=.
iApply fupd_wp.
iMod (step_Fold _ j K (of_val w') w' with "[-]") as "Hz"; eauto.
iMod (step_fold _ j K (of_val w') w' with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto.
iModIntro. iApply wp_value. iNext; iExists _; iFrame "Hz".
by rewrite -interp_subst.
......@@ -501,6 +501,32 @@ Section fundamental.
iExists (#v false); eauto.
Qed.
Lemma bin_log_related_FAA Γ e1 e2 e1' e2'
(IHHtyped1 : Γ e1 log e1' : Tref TNat)
(IHHtyped2 : Γ e2 log e2' : TNat) :
Γ FAA e1 e2 log FAA e1' e2' : TNat.
Proof.
iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (FAALCtx _) v v' "[Hv #Hiv]"
('`IHHtyped1 _ _ j ((FAALCtx _) :: K)).
iDestruct "Hiv" as ([l l'] ?) "Hll"; simplify_eq.
smart_wp_bind (FAARCtx _) u u' "[Hu #Hiu]"
('`IHHtyped2 _ _ j ((FAARCtx _) :: K)).
iDestruct "Hiu" as (m) "[% %]"; simplify_eq.
iApply wp_atomic; eauto.
iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #>Hv]]" "Hclose".
iDestruct "Hv" as (?) "[% %]"; simplify_eq/=.
iModIntro.
iApply (wp_FAA with "Hv1"); auto using to_of_val.
iNext. iIntros "Hw2".
iMod (step_faa with "[$Hu Hv2]") as "[Hu Hv2]"; eauto;
first solve_ndisj.
iMod ("Hclose" with "[Hw2 Hv2]").
{ iNext; iExists (#nv _, #nv _); simpl; iFrame. by eauto. }
iModIntro.
iExists (#nv _); iFrame; eauto.
Qed.
Theorem binary_fundamental Γ e τ :
Γ e : τ Γ e log e : τ.
Proof.
......@@ -537,5 +563,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_FAA; eauto.
Qed.
End fundamental.
......@@ -172,5 +172,18 @@ Section typed_interp.
+ iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
- (* FAA *)
smart_wp_bind (FAALCtx _) v1 "#Hv1" IHtyped1; cbn.
smart_wp_bind (FAARCtx _) v2 "#Hv2" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv1" as (l) "[% Hv1]".
iDestruct "Hv2" as (k) "%"; simplify_eq/=.
iApply wp_atomic.
iInv (logN .@ l) as (w) "[Hw1 #>Hw2]" "Hclose".
iDestruct "Hw2" as (m) "%"; simplify_eq/=.
iApply (wp_FAA with "Hw1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hw1".
iMod ("Hclose" with "[Hw1]"); last by eauto.
iNext; iExists _; iFrame. by eauto.
Qed.
End typed_interp.
......@@ -52,8 +52,9 @@ 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)
(* Fetch and add for fine-grained concurrency *)
| FAA (e1 : expr) (e2 : expr).
Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
......@@ -159,7 +160,9 @@ 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)
| FAALCtx (e2 : expr)
| FAARCtx (v1 : val).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
......@@ -189,6 +192,8 @@ 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
| FAALCtx e2 => FAA e e2
| FAARCtx v1 => FAA (of_val v1) e
end.
Definition state : Type := gmap loc val.
......@@ -264,7 +269,11 @@ 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]>σ) []
| FAAS l m e2 k σ :
to_val e2 = Some (NatV k)
σ !! l = Some (NatV m)
head_step (FAA (Loc l) e2) σ [] (#n m) (<[l:=NatV (m + k)]>σ) [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -348,6 +357,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)
| FAA e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| _ => False
end.
Local Hint Resolve language.val_irreducible.
......
......@@ -113,6 +113,19 @@ Section lang_rules.
iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Lemma wp_FAA E l m e2 k :
IntoVal e2 (#nv k)
{{{ l ↦ᵢ (#nv m) }}} FAA (Loc l) e2 @ E
{{{ RET (#nv m); l ↦ᵢ #nv (m + k) }}}.
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.
......
......@@ -353,6 +353,31 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
Lemma step_faa E j K l m e2 k:
to_val e2 = Some (#nv k) nclose specN E
spec_ctx j fill K (FAA (Loc l) e2) l ↦ₛ (#nv m)
={E}= j fill K (#n m) l ↦ₛ #nv (m + k).
Proof.
iIntros (??) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (ρ) "Hinv".
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_both_valid.
iDestruct (own_valid_2 with "Hown Hl")
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
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 m)))). }
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 (m + k)))); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (#n m)]> tp), (<[l:=#nv (m + k)]>σ).
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)
......@@ -382,12 +407,12 @@ Section cfg.
spec_ctx j fill K (TApp (TLam e)) ={E}= j fill K e.
Proof. by intros ?; apply: do_step_pure. Qed.
Lemma step_Fold E j K e v :
Lemma step_fold E j K e v :
to_val e = Some v nclose specN E
spec_ctx j fill K (Unfold (Fold e)) ={E}= j fill K e.
Proof. by intros ?; apply: do_step_pure. Qed.
Lemma step_Pack E j K e1 v e2 :
Lemma step_pack E j K e1 v e2 :
to_val e1 = Some v nclose specN E
spec_ctx j fill K (UnpackIn (Pack e1) e2) ={E}= j fill K e2.[e1/].
Proof. by intros ?; apply: do_step_pure. Qed.
......
......@@ -77,6 +77,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| TCAS e1 e2 e3 τ :
EqType τ Γ e1 : Tref τ Γ e2 : τ Γ e3 : τ
Γ CAS e1 e2 e3 : TBool
| TFAA e1 e2 : Γ e1 : Tref TNat Γ e2 : TNat Γ FAA e1 e2 : 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