Commit 8bc221ff authored by Simon Friis Vindum's avatar Simon Friis Vindum

Add proof of alternative MS queue with a few holes

parent a00107f3
......@@ -63,6 +63,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/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/fact.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.
Definition TMaybe τ := (TSum TUnit τ).
Definition none := InjL Unit.
Definition some v := InjR v.
Definition TNodeBody τ v := TMaybe (TProd (TMaybe τ.[ren (+1)]) (Tref (Tref v))).
Definition TNode τ := TRec (TNodeBody τ (TVar 0)).
Definition MS_QueueType τ := Tref (Tref (TNode τ)).
(* Get the value of a some and spin it the argument is a none. *)
Definition getValue (e : expr) : expr :=
(Case e (App (Rec (App (Var 0) Unit)) Unit) (Var 0)).
(* Pseudo code for dequeue:
rec try() =>
let n = !head
c = getValue (unfold !n)
in case unfold !!(snd c) with
Nil => none
Cons x xs =>
if CAS head n !(snd c)
then some (getValue x)
else (try ())
*)
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 (* c *)))))) (* 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 (* c *)))))
(some (getValue (Fst (Var 0 (* n' *)))))
(App (Var 3 (* try *)) Unit)
)
)
)
)
).
(* Pseudo code for enqueue:
fun x =>
let n = alloc (fold (some (some x), (alloc (alloc (fold none))))))
in
(rec try(_) =>
let c = (snd (getValue (unfold !!tail)))
t = !c
in case (unfold !t) with
Left _ => if CAS c t n
then
tail <- n ;;
()
else try ()
Right c' =>
try (snd c')
)
()
*)
Definition MS_enqueue :=
(Lam (* x. *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(App
(Rec (* try(_) *)
(LetIn
(* c = *) (Snd (getValue (Unfold (Load (Load (Var 5 (* tail *)))))))
(LetIn
(* t = *) (Load (Var 0 (* c *)))
(Case
(Unfold (Load (Var 0 (* t *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 2 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
(* Insertion succeeded, we are done *)
(Seq
(* Update the tail pointer *)
(Store (Var 8 (* tail *)) (Var 5 (* n *)))
Unit)
(* Insertion failed, we try again*)
(App (Var 3 (* try *)) Unit)
)
(* c = InjR c' =>. We are not at the end yet, try again.*)
(App (Var 3 (* try *)) Unit)
)
)
)
)
Unit
)
)
).
Definition MS_queue : expr :=
TLam (* _ *)
(LetIn (* node = *) (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tail = *) (Alloc (Var 0 (* node *)))
(LetIn
(* head = *) (Alloc (Var 1 (* node *)))
(Pair MS_dequeue MS_enqueue)
))).
Section MS_queue_alt.
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_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
Proof.
econstructor. econstructor.
- econstructor.
apply (TFold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. asimpl. done.
- econstructor.
2: { econstructor. }
econstructor. econstructor.
+ econstructor.
apply getValue_type.
apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
+ asimpl.
econstructor.
* repeat constructor.
* econstructor.
-- apply (TUnfold _ _ (TNodeBody τ (TVar 0))). repeat constructor.
-- econstructor.
++ econstructor.
2: { by constructor. }
repeat econstructor.
repeat econstructor.
repeat econstructor.
++ repeat econstructor.
++ repeat econstructor.
-- 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.
apply (TFold _ _ (TNodeBody (TVar 0) (TVar 0))).
repeat econstructor.
- econstructor.
+ repeat econstructor.
+ econstructor.
* repeat econstructor.
* econstructor.
-- apply MS_dequeue_type.
-- apply MS_enqueue_type.
Qed.
End MS_queue_alt.
This diff is collapsed.
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