Commit 7603e66d authored by Simon Friis Vindum's avatar Simon Friis Vindum

Add WIP Michael-Scott queue

parent c1dac1db
......@@ -62,6 +62,8 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
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/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel/heaplang/ltyping.v
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
From iris.algebra Require Import list.
From iris.program_logic Require Export lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
Import uPred.
(* The course-grained queue is implemented as a linked list guarded by a
lock.
*)
Definition TMaybe τ := (TSum TUnit τ).
Definition nil := Fold (InjL Unit).
Definition cons val tail := Fold (InjR (Pair val tail)).
Definition TListBody τ v := TMaybe (TProd τ.[ren (+1)] v).
Definition TList τ := TRec (TListBody τ (TVar 0)).
Definition CG_QueueType τ := Tref (TList τ).
Definition CG_dequeue_body head :=
Lam (* _ *)
(Case
(Unfold (Load head.[ren (+1)]))
(InjL Unit) (* The lock is empty, return none *)
(* InjL c *)
(Seq
(Store head.[ren (+2)] (Snd (Var 0 (* c *)))) (* Update the list pointer to the next element. *)
(InjR (Fst (Var 0))) (* Return the value in the previous head *)
)
).
Definition CG_dequeue head lock := with_lock (CG_dequeue_body head) lock.
Definition CG_dequeueV head lock := with_lockV (CG_dequeue_body head) lock.
Definition CG_enqueue_body head :=
Lam (* x *)
(Store
head.[ren (+1)]
(App
(Rec (* try(c) *)
(Case
(Var 1 (* c *)) (* Check the current element *)
(* c = nil. We've arrived at the end of the list *)
(cons (Var 3 (* x *)) nil)
(* c = cons ... The next element is a cons *)
(cons (Fst (Var 0)) (App (Var 1 (* try *)) (Unfold (Snd (Var 0 (* c *)))))
)
)
)
(Unfold (Load head.[ren (+1)]))
)
).
Definition CG_enqueue head lock := with_lock (CG_enqueue_body head) lock.
Definition CG_enqueueV head lock := with_lockV (CG_enqueue_body head) lock.
Definition CG_queue : expr :=
TLam (* _ *)
(LetIn
(* lock = *) newlock
(LetIn
(* head = *) (Alloc nil) (* Allocate nil *)
(Pair (CG_dequeue (Var 0) (Var 1)) (CG_enqueue (Var 0) (Var 1)))
)
).
Section CG_queue.
Context `{heapIG Σ, cfgSG Σ}.
Lemma CG_enqueue_type Γ τ :
typed (CG_QueueType τ :: LockType :: Γ) (CG_enqueue (Var 0) (Var 1)) (TArrow τ TUnit).
Proof.
apply with_lock_type.
2: { by constructor. }
econstructor.
econstructor.
- by econstructor.
- econstructor.
2: {
apply (TUnfold _ _ (TListBody τ (TVar 0))).
repeat econstructor; eauto.
}
+ repeat econstructor. asimpl. eauto.
Qed.
Lemma CG_dequeue_type Γ τ :
typed (CG_QueueType τ :: LockType :: Γ) (CG_dequeue (Var 0) (Var 1)) (TArrow TUnit (TMaybe τ)).
Proof.
apply with_lock_type.
2: { constructor. done. }
econstructor.
econstructor.
- apply (TUnfold _ _ (TListBody τ (TVar 0))). repeat econstructor.
- repeat econstructor; eauto.
- repeat econstructor; asimpl; eauto.
Qed.
Lemma CG_dequeue_to_val h l :
of_val (CG_dequeueV h l) = CG_dequeue h l.
Proof. trivial. Qed.
Lemma CG_enqueue_to_val h l :
of_val (CG_enqueueV h l) = CG_enqueue h l.
Proof. trivial. Qed.
Lemma CG_queue_type Γ :
typed Γ CG_queue
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
Proof.
econstructor.
econstructor.
- apply newlock_type.
- econstructor.
+ econstructor.
apply (TFold _ _ (TListBody (TVar 0) (TVar 0))).
repeat econstructor.
+ repeat econstructor.
* apply CG_dequeue_type.
* apply CG_enqueue_type.
Qed.
Lemma CG_dequeue_body_subst head f :
(CG_dequeue_body head).[f] = CG_dequeue_body head.[f].
Proof. rewrite /CG_dequeue_body. asimpl. reflexivity. Qed.
Hint Rewrite CG_dequeue_body_subst : autosubst.
Lemma CG_dequeue_subst (head lock : expr) f :
(CG_dequeue head lock).[f] = CG_dequeue head.[f] lock.[f].
Proof. rewrite /CG_dequeue. asimpl. reflexivity. Qed.
Hint Rewrite CG_dequeue_subst : autosubst.
Lemma CG_enqueue_body_subst head f :
(CG_enqueue_body head).[f] = CG_enqueue_body head.[f].
Proof. rewrite /CG_enqueue_body. asimpl. reflexivity. Qed.
Hint Rewrite CG_enqueue_body_subst : autosubst.
Lemma CG_enqueue_subst (head lock : expr) f :
(CG_enqueue head lock).[f] = CG_enqueue head.[f] lock.[f].
Proof. rewrite /CG_enqueue. asimpl. reflexivity. Qed.
Hint Rewrite CG_enqueue_subst : autosubst.
Definition program : expr :=
LetIn
(* lock = *) (App CG_queue Unit)
(Seq
(App (Snd (Var 0)) (#n 3))
(App (Fst (Var 0)) Unit)
).
(* Lemma CG_queue_test : WP program {{ v, ⌜v = #nv 3⌝ }}%I. *)
(* Proof. *)
(* rewrite /program. *)
(* iApply (wp_bind (fill [LetInCtx _])). *)
(* iApply wp_pure_step_later; auto. iNext. *)
(* Abort. *)
End CG_queue.
Hint Rewrite CG_dequeue_body_subst : autosubst.
Hint Rewrite CG_dequeue_subst : autosubst.
Hint Rewrite CG_enqueue_body_subst : autosubst.
Hint Rewrite CG_enqueue_subst : autosubst.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
From iris.algebra Require Import list.
From iris.program_logic Require Export lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
Import uPred.
Definition TMaybe τ := (TSum TUnit τ).
Definition none := InjL Unit.
Definition some v := InjR v.
(* Definition nil := InjL Unit. *)
(* Definition cons val tail := InjR (Pair val tail). *)
Definition TNodeBody τ v := TMaybe (TProd (TMaybe τ.[ren (+1)]) (Tref (Tref v))).
Definition TNode τ := TRec (TNodeBody τ (TVar 0)).
Definition MS_QueueType τ := Tref (Tref (TNode τ)).
Definition getValue (e : expr) : expr :=
(Case
e
(App (Rec (App (Var 0) Unit)) Unit)
(Var 0)
).
Definition MS_dequeue :=
(Rec (* try(_) *)
(LetIn
(* n = *) (Load (Var 2 (* head *)))
(LetIn
(* c = *) (getValue (Unfold (Load ((Var 0 (* n *))))))
(Case
(Unfold (Load (Load (Snd (Var 0 (* n *)))))) (* Get next node after sentinel *)
(* Snd n = InjL Unit => *)
none (* The queue is empty, return none *)
(* Snd n = InjR n' => *)
(If
(CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Snd (Var 1 (* n' *)))))
(* (CAS (Var 5 (* head *)) (Var 2 (* n *)) (Var 0 (* n' *))) *)
(some (getValue (Fst (Var 1 (* n *)))))
(App (Var 3 (* try *)) Unit)
)
)
)
)
).
Definition MS_enqueue :=
(Lam (* x. *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(App
(Rec (* try(c) *)
(LetIn
(* t = *) (Load (Var 1 (* c *)))
(Case
(Unfold (Load (Var 0 (* t' *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 3 (* c *)) (Var 1 (* t *)) (Var 4 (* n *)))
(* Insertion succeeded, we are done *)
Unit
(* Insertion failed, we try again*)
(App (Var 2 (* try *)) (Var 3 (* c *)))
)
(* c = InjR c' =>. We are not at the end yet, recurse on the tail *)
(App (Var 2 (* try *)) (Snd ((Var 0 (* c' *)))))
)
)
)
(* (Unfold (Load (Load (Var 2 (* head *))))) *)
(Snd (getValue (Unfold (Load (Load (Var 2 (* head *)))))))
)
)
).
Definition MS_queue : expr :=
TLam (* _ *)
(LetIn
(* head = *) (Alloc (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none))))))))
(Pair MS_dequeue MS_enqueue)
).
Section MS_queue.
Context `{heapIG Σ, cfgSG Σ}.
(* Check the types of the various functions. *)
Lemma getValue_type Γ τ e :
typed Γ e (TMaybe τ) typed Γ (getValue e) τ.
Proof.
intros ?. repeat econstructor. eassumption.
Qed.
Lemma MS_enqueue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
Proof.
econstructor.
econstructor.
- econstructor.
apply (TFold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. asimpl. done.
- econstructor.
2: {
econstructor.
apply getValue_type.
apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
econstructor.
econstructor.
+ repeat econstructor.
+ econstructor.
* apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat constructor.
* repeat econstructor; reflexivity.
* repeat econstructor.
Qed.
Lemma MS_dequeue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_dequeue (TArrow TUnit (TMaybe τ)).
Proof.
econstructor.
econstructor.
{ repeat econstructor. }
econstructor.
{ apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
- repeat econstructor.
- econstructor.
+ econstructor.
2: { econstructor. reflexivity. }
* econstructor.
* econstructor. reflexivity.
* repeat econstructor.
+ repeat econstructor. asimpl. done.
+ repeat econstructor.
Qed.
Lemma MS_queue_type Γ :
typed Γ MS_queue
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
Proof.
econstructor.
econstructor.
- econstructor.
econstructor.
apply (TFold _ _ (TNodeBody (TVar 0) (TVar 0))).
repeat econstructor.
- econstructor.
+ apply MS_dequeue_type.
+ apply MS_enqueue_type.
Qed.
Definition program : expr :=
LetIn
(* lock = *) (App MS_queue Unit)
(Seq
(App (Snd (Var 0)) (#n 3))
(App (Fst (Var 0)) Unit)
).
(* Lemma MS_queue_test : WP program {{ v, ⌜v = #nv 3⌝ }}%I. *)
(* Proof. *)
(* rewrite /program. *)
(* iApply (wp_bind (fill [LetInCtx _])). *)
(* iApply wp_pure_step_later; auto. iNext. *)
(* Admitted. *)
End MS_queue.
From Coq.Lists Require Import List.
From iris.algebra Require Import auth list.
From iris.program_logic Require Import adequacy ectxi_language.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
CG_queue MS_queue.
From iris.proofmode Require Import tactics.
Definition queueN : namespace := nroot .@ "stack".
Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Notation D := (prodO valO valO -n> iPropO Σ).
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
(* Definition nodeInv_pre : valO -n> (iPropO Σ) := λne nodeInv v, *)
(* (∃ ℓ m v ℓtail, *)
(* ⌜n = Loc ℓ⌝ ∗ ℓ ↦ᵢ (FoldV v) *)
(* ∗ (⌜v = noneV⌝ *)
(* ∨ (∃ n', ⌜v = someV (PairV v (Loc ℓtail))⌝ *)
(* ∗ ℓtail ↦ᵢ n' *)
(* ∗ ▷(nodeInv n')) *)
(* ))%I. *)
(* Global Instance nodeInv_pre_contractive Q : Contractive (nodeInv_pre Q). *)
(* Proof. solve_contractive. Qed. *)
(* Definition StackLink (Q : D) : D := fixpoint (StackLink_pre Q). *)
Definition isStackList ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => ↦ₛ FoldV noneV
| x :: xs' => True (* FIXME *)
end.
Fixpoint isNodeList ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => ↦ᵢ FoldV noneV
| x :: xs' =>
( tail next,
↦ᵢ FoldV (someV (PairV x (LocV tail)))
tail ↦ᵢ (LocV next)
isNodeList next xs')
end.
Definition sentinelInv sentinel xs v hdPt hd : iProp Σ :=
sentinel ↦ᵢ (FoldV (someV (PairV v (LocV hdPt))))
hdPt ↦ᵢ (LocV hd)
isNodeList hd xs.
(* Predicate expression that ℓ points to a queue with the values xs *)
Definition isMSQueue (τi : D) ( : loc) (xs : list val) : iProp Σ :=
(
sentinel,
(* ∃ ℓsentinel ℓfirst ℓhead, *)
(* ℓ points to the sentinel *)
↦ᵢ (LocV sentinel)
( v hdPt hd n, inv n (sentinelInv sentinel xs v hdPt hd))
(* The sentinel points to the first actual element *)
(* ∗ ℓsentinel ↦ᵢ{1/2} (FoldV (someV (PairV noneV (LocV ℓfirst)))) *)
(* ∗ ℓfirst ↦ᵢ (LocV ℓhead) *)
(* ∗ isNodeList ℓhead xsᵢ *)
)%I.
(* Definition isStackList (τi : D) (ℓ : loc) (xs : list val) (xs' : list val) : iProp Σ := *)
(* (⌜True⌝)%I. *)
Fixpoint xsLink (τi : D) (xs xs : list val) : iProp Σ :=
match (xs, xs) with
| (nil, nil) => True
| ((x :: xs'), (x :: xs')) => τi (x, x) xsLink τi xs' xs'
| _ => False
end.
Definition invariant τi hd sHd lock: iProp Σ :=
( hd ' xs xs,
hd = Loc hd isMSQueue τi hd xs
sHd = Loc ' isStackList ' xs
lock ↦ₛ (#v false)
xsLink τi xs xs
length xs = length xsₛ⌝
)%I.
Lemma MS_CG_counter_refinement :
[] MS_queue log CG_queue :
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
Proof.
iIntros (Δ vs ?) "#[Hspec HΓ]".
iDestruct (interp_env_empty with "HΓ") as "->". iClear "HΓ".
iIntros (j K) "Hj".
iApply wp_value.
iExists (TLamV _). iFrame "Hj". clear j K.
(* unfold interp. unfold interp_forall. *)
iAlways. iIntros (τi) "%". iIntros (j K) "Hj /=".
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
as (lock) "[Hj lockPts]"; eauto.
iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; eauto.
iApply wp_pure_step_later; auto. iNext.
(* Stepping through the specs allocation *)
iMod (step_alloc _ j (LetInCtx _ :: K) with "[$Hj]")
as (list) "[Hj listPts']"; eauto.
simpl.
iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; eauto.
(* Stepping through the initialization of the sentinel *)
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [AllocCtx])).
iApply (wp_bind (fill [AllocCtx])).
iApply (wp_bind (fill [PairRCtx (InjLV UnitV); InjRCtx; FoldCtx])).
iApply (wp_bind (fill [AllocCtx])).
iApply wp_alloc; first done.
iNext. iIntros (nil) "nilPts /=".
iApply wp_alloc; first done.
iNext. iIntros (tail) "tailPts /=".
iApply wp_value.
iApply wp_alloc; first done. iNext.
iIntros (sentinel) "sentinelPts /=".
iApply wp_alloc; first done. iNext.
iIntros (head) "headPts /=".
iApply wp_pure_step_later; auto. iNext.
iMod (inv_alloc (queueN.@"S") _ (sentinelInv sentinel [] noneV tail nil)
with "[sentinelPts tailPts nilPts]")
as "#sentinelI".
{ iNext. iFrame. }
iMod (inv_alloc queueN _ (invariant τi (Loc head) (Loc list) _)
with "[headPts lockPts listPts']")
as "#Hinv".
{ iNext. iExists _, _, [], [].
simpl.
iFrame.
iSplit. done.
iSplitL "headPts".
{ iExists _.
iFrame.
iExists _, _, _, _.
iAssumption.
}
iSplit; done.
}
iApply wp_value.
asimpl.
iExists (PairV (CG_dequeueV _ _) (CG_enqueueV _ _)).
simpl. rewrite CG_dequeue_to_val CG_enqueue_to_val.
iFrame.
iExists (_, _), (_, _).
iSplitL. { eauto. }
iSplit.
- (* dequeue *)
iIntros (vv) "!> [-> ->]".
clear j K.
iIntros (j K) "Hj". simpl.
rewrite with_lock_of_val.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (hd ' xs xs') "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
iDestruct "isMSQ" as (sentinel) "[hdPts #Hsentinel]".
iApply (wp_load with "hdPts").
iNext. iIntros "hdPts".
iMod ("Hclose" with "[hdPts lofal Hlink Hsq]").
{ iNext. iExists _, _, _, _.
iFrame.
iSplit; auto.
iSplitL "hdPts".
{ iExists _. iFrame. iAssumption. }
iSplit; auto.
}
simpl.
iModIntro.
iApply wp_pure_step_later; auto. iNext. asimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iDestruct "Hsentinel" as (v l1 l2 n) "Hsentinv".
iInv n as "[sentinelPts HRest]" "Hclose".
iApply (wp_load with "sentinelPts").
iNext. iIntros "sentinelPts".
iMod ("Hclose" with "[$]") as "_".
iModIntro. simpl.
iApply (wp_bind (fill [CaseCtx _ _])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
simpl.
iApply wp_pure_step_later; auto. iNext.
simpl.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])).
asimpl.
iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iInv n as "(sentinelPts & l2Pts & HRest)" "Hclose".
iApply (wp_load with "[$]").
iNext. iIntros "l2Pts".
iMod ("Hclose" with "[$]") as "_".
iModIntro.
simpl.
iInv n as "(sentinelPts & l2Pts & Hnode)" "Hclose".
destruct xs as [|x xs''].
+ (* xs is the empty list *)
assert (xs' = []) as ->. { destruct xs'. done. inversion H3. }