Skip to content
Snippets Groups Projects
Commit c79971e7 authored by Joshua Yanovski's avatar Joshua Yanovski
Browse files

Skiplist WIP

parent 236de776
No related branches found
No related tags found
No related merge requests found
......@@ -27,8 +27,13 @@ theories/lang/lib/new_delete.v
theories/lang/lib/spawn.v
theories/lang/lib/lock.v
theories/lang/lib/arc.v
theories/lang/lib/btree/base.v
theories/lang/lib/btree/history.v
theories/lang/lib/btree/atomic.v
theories/lang/lib/btree/btree.v
theories/lang/lib/btree/skiplist_code.v
theories/lang/lib/btree/skiplist_inv.v
theories/lang/lib/btree/skiplist.v
theories/lang/lib/tests.v
theories/typing/base.v
theories/typing/type.v
......
(* Logically atomic triple *)
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
From iris.proofmode Require Import tactics.
From stdpp Require Import hlist.
Import uPred.
Definition mono {M X} (F : (X uPred M) (X uPred M)) := P Q, ( (x : X), P x Q x) ( (x : X), F P x F Q x).
Definition Fix {M X} (F : (X uPred M) (X uPred M)) : X uPred M :=
(λ x, P (_ : x, P x F P x), P x)%I.
Lemma Fix_implies_F_Fix {M X} F :
@mono M X F
x, Fix F x F (Fix F) x.
Proof.
iIntros (Hmono x) "HFix".
iDestruct "HFix" as (P Hincl) "HP".
pose proof (Hmono P (Fix F)).
rewrite -(impl_elim_r (F P x) (F (Fix F) x)).
iSplit. by iApply Hincl.
rewrite -H. iIntros "{HP}". auto.
iIntros (x') "HP".
iExists P, Hincl. eauto.
Qed.
Lemma F_Fix_implies_Fix {M X} F :
@mono M X F
x, F (Fix F) x Fix F x.
Proof.
iIntros (H x) "HF".
iExists (F (Fix F)).
rewrite -exist_intro; first done.
apply H.
intros x'.
by rewrite Fix_implies_F_Fix.
Qed.
Corollary Fix_unfold {M X} F :
@mono M X F
x, Fix F x F (Fix F) x.
Proof.
iIntros.
iSplit.
- rewrite -Fix_implies_F_Fix //; auto.
- rewrite F_Fix_implies_Fix //; auto.
Qed.
Lemma Fix_coind {M X} (F : (X uPred M) (X uPred M)) :
(P : X uPred M), ( x, P x F P x)
( x, P x Fix F x).
Proof.
iIntros.
by iExists P, H.
Qed.
Fixpoint incl {M Tl} : relation (himpl Tl (uPred M)) :=
match Tl with
| tnil => λ P Q, P -∗ Q
| tcons T' Tl => λ P Q, (x: T'), incl (P x) (Q x)
end.
Definition mono' {M Tl} F := P Q, @incl M Tl P Q @incl M Tl (F P) (F Q).
Definition Fix' {M Tl} (F : himpl Tl (uPred M) himpl Tl (uPred M)) :=
huncurry (Fix (λ P, hcurry (F (huncurry P)))).
Lemma incl_curry_impl {M Tl} P Q :
@incl M Tl P Q ( x, hcurry P x hcurry Q x).
Proof.
split.
- intros. induction x; simpl in *.
+ rewrite /incl in H. apply H.
+ by apply IHx.
- induction Tl; simpl in *; intros.
+ apply (H hnil).
+ apply IHTl. intros x'. apply (H (hcons _ _)).
Qed.
Lemma incl_uncurry_impl {M Tl} P Q :
@incl M Tl (huncurry P) (huncurry Q) ( x, P x Q x).
Proof.
split.
- intros. induction x; simpl in *.
+ rewrite /incl in H. apply H.
+ apply (IHx (λ l, P (hcons a l)) (λ l, Q (hcons a l))).
apply (H a).
- induction Tl; simpl in *; intros.
+ apply (H hnil).
+ apply IHTl. intros x'. apply (H (hcons _ _)).
Qed.
Lemma mono'_curry_mono {M Tl} F :
@mono' M Tl F mono (λ P, hcurry (F (huncurry P))).
Proof.
rewrite /mono /mono' /=.
intros.
setoid_rewrite incl_curry_impl in H.
apply H.
intros.
by rewrite ->! hcurry_uncurry.
Qed.
Lemma Fix'_implies_F_Fix' {M Tl} F :
@mono' M Tl F
incl (Fix' F) (F (Fix' F)).
Proof.
intros.
apply mono'_curry_mono in H.
rewrite incl_curry_impl.
intros.
eapply Fix_implies_F_Fix in H.
setoid_rewrite <- hcurry_uncurry at 1 in H.
apply H.
Qed.
Lemma F_Fix'_implies_Fix' {M Tl} F :
@mono' M Tl F
incl (F (Fix' F)) (Fix' F).
Proof.
intros.
apply mono'_curry_mono in H.
rewrite incl_curry_impl.
intros.
eapply F_Fix_implies_Fix in H.
setoid_rewrite <- hcurry_uncurry at 2 in H.
apply H.
Qed.
Fixpoint hequiv {M Tl} {struct Tl} : Equiv (himpl Tl (uPred M)) :=
match Tl with
| tnil => λ P Q, @equiv (uPred M) _ P Q
| tcons T' Tl => λ P Q, (x: T'), P x Q x
end.
Existing Instance hequiv.
Lemma double_hincl_hequiv {M Tl} P Q:
@incl M Tl P Q incl Q P P Q.
Proof.
intros.
induction Tl.
- apply equiv_spec.
auto.
- intros x.
by apply IHTl.
Qed.
Corollary Fix'_unfold {M Tl} F :
@mono' M Tl F
Fix' F F (Fix' F).
Proof.
intros.
apply double_hincl_hequiv.
{ by apply Fix'_implies_F_Fix'. }
by apply F_Fix'_implies_Fix'.
Qed.
Lemma Fix'_coind {M Tl} (F : himpl Tl (uPred M) himpl Tl (uPred M)) :
mono' F
(P : himpl Tl (uPred M)), incl P (F P)
incl P (Fix' F).
Proof.
intros.
rewrite incl_curry_impl.
intros.
rewrite /Fix'.
rewrite -> hcurry_uncurry.
apply Fix_coind.
intros x'.
eapply incl_curry_impl in H0.
rewrite -> H0.
apply incl_curry_impl.
simpl in *.
apply H.
apply incl_curry_impl.
intros.
by setoid_rewrite hcurry_uncurry.
Qed.
Section atomic.
Context `{irisG Λ Σ} {A: Type}
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val Λ iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
.
Definition atomic_shift'_pre (Φ : val Λ iProp Σ) (F : iProp Σ) : iProp Σ :=
(|={Eo,Ei}=> x : A,
α x ((α x ={Ei,Eo}=∗ F) y, β x y ={Ei,Eo}=∗ Φ y))%I.
Lemma atomic_shift'_pre_mono' (Φ : val Λ iProp Σ) :
mono' (Tl := tnil) (atomic_shift'_pre Φ).
Proof.
unfold mono'.
simpl.
intros.
rewrite /atomic_shift'_pre.
by setoid_rewrite <- H.
Qed.
Definition atomic_shift (Φ : val Λ iProp Σ) :=
Fix' (Tl := tnil) (atomic_shift'_pre Φ).
Lemma atomic_shift_unfold (Φ : val Λ iProp Σ) :
atomic_shift Φ
(|={Eo,Ei}=> x : A,
α x ((α x ={Ei,Eo}=∗ atomic_shift Φ) y, β x y ={Ei,Eo}=∗ Φ y))%I.
Proof.
rewrite {1}/atomic_shift.
by rewrite (Fix'_unfold _ (atomic_shift'_pre_mono' Φ)).
Qed.
Lemma atomic_shift_unfold_coind (Φ : val Λ iProp Σ) (P : himpl tnil (uPred (iResUR Σ))) :
incl P (atomic_shift'_pre Φ P) incl P (atomic_shift Φ).
Proof.
intros H.
rewrite /atomic_shift.
by apply (Fix'_coind (Tl := tnil) _ (atomic_shift'_pre_mono' Φ)).
Qed.
(* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
(* logically atomic wp: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_wp
(e: expr _) : iProp Σ :=
( Φ, atomic_shift Φ -∗ WP e @ Eo {{ Φ }})%I.
End atomic.
Arguments atomic_shift_unfold_coind {_ _ _ _ _ _ _ _ _} _ _.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Import invariants fractional cancelable_invariants auth own namespaces.
From iris.proofmode Require Import tactics notation.
From lrust.lang Require Import lang proofmode lifting notation tactics.
From lrust.lang.lib Require Import new_delete.
From iris.algebra Require Import gset gmap list auth excl frac agree.
From stdpp Require Import list hlist (*listset*) sorting.
From lrust.lang.lib.btree Require Import atomic btree history.
Set Default Proof Using "Type".
Import uPred.
Section skiplist.
Context (null: loc).
Definition cas_next :=
(λ: [ "x"; "cmp"; "val"],
CAS ("x" + #2) "cmp" "val"
)%V.
Definition cas_value :=
(λ: [ "x"; "cmp"; "val"],
CAS ("x" + #1) "cmp" "val"
)%V.
Definition cas_head :=
(λ: [ "x"; "cmp"; "val"],
CAS ("x" + #0) "cmp" "val"
)%V.
Definition cas_right :=
(λ: [ "x"; "cmp"; "val"],
CAS ("x" + #2) "cmp" "val"
)%V.
Definition make_node :=
(λ: [ "k"; "v"; "n" ],
let: "x" := new [ #(3)%nat ] in
"x" + #0 <- "k";;
"x" + #1 <- "v";;
"x" + #2 <- "n";;
"x"
)%V.
Definition make_index :=
(λ: [ "p"; "d"; "n" ],
let: "x" := new [ #(3)%nat ] in
"x" + #0 <- "p";;
"x" + #1 <- "d";;
"x" + #2 <- "n";;
"x"
)%V.
Definition make_head :=
(λ: [ "l"; "p"; "d"; "n" ],
let: "x" := new [ #(3)%nat ] in
"x" + #0 <- "p";;
"x" + #1 <- "d";;
"x" + #2 <- "n";;
"x" + #3 <- "l";;
"x"
)%V.
Definition make_marker :=
(λ: [ "n" ],
let: "x" := new [ #(3)%nat ] in
"x" + #0 <- #1;;
"x" + #1 <- "x";;
"x" + #2 <- "n";;
"x"
)%V.
Definition append_marker :=
(λ: [ "x"; "next" ],
cas_next [ "x"; "next"; make_marker [ "next" ] ]
)%V.
Definition link :=
(λ: [ "x"; "cmp"; "val" ],
"val" + #2 <-ˢᶜ "cmp";;
if: !ˢᶜ ((!ˢᶜ ("x" + #0)) + #1) = #null then #false
else cas_right [ "x"; "cmp"; "val" ]
)%V.
Definition unlink :=
(λ: [ "x"; "cmp" ],
if: !ˢᶜ ((!ˢᶜ ("x" + #0)) + #1) = #null
then cas_right [ "x"; "cmp"; !ˢᶜ ("cmp" + #1) ]
else #false
)%V.
Definition is_marker' :=
(λ: ["x"],
!ˢᶜ ("x" + #1) = "x"
)%V.
Definition compare :=
(rec: "compare" [ "x";"y"] :=
if: "x" "y" then
if: "x" = "y" then #0
else #-1
else #1
)%V.
Definition help_delete :=
(rec: "help_delete" [ "b";"n";"f" ] :=
if: "f" = !ˢᶜ ("n" + #2) then
if: "n" = !ˢᶜ ("b" + #2) then
(if: "f" = #null then cas_next [ "n"; "f"; make_marker [ "f" ] ]
else if: is_marker' [ "f" ] then cas_next [ "b"; "n"; !ˢᶜ ("f" + #2) ]
else cas_next [ "n"; "f"; make_marker [ "f" ]]);; #()
else #()
else #()
)%V.
Definition try_reduce_level :=
(rec: "try_reduce_level" [ "x" ] :=
let: "h" := !ˢᶜ ("x" + #0) in
if: #4 !ˢᶜ ("h" + #3) then
let: "d" := !ˢᶜ ("h" + #1) in
if: "d" = #null then #()
else
let: "e" := !ˢᶜ ("d" + #1) in
if: "e" = #null then #()
else if: !ˢᶜ ("e" + #2) = #null then #()
else if: !ˢᶜ ("d" + #2) = #null then #()
else if: !ˢᶜ ("h" + #2) = #null then #()
else
if: cas_head [ "x"; "h"; "d" ] then
if: !ˢᶜ ("h" + #2) = #null then #()
else (cas_head [ "x"; "d"; "h" ];; #())
else #()
else #()
)%V.
Definition find_predecessor_3 :=
(λ: [ "x"; "k"; "inner";
"find_predecessor"; "q"; "r";
"find_predecessor_2"; "continue" ],
if: "inner" then
if: "continue" then
let: "d" := !ˢᶜ ("q" + #1) in
if: "d" = #null then
!ˢᶜ ("q" + #0)
else
"find_predecessor_2" [ "x"; "k"; "inner"; "find_predecessor"; "d"; !ˢᶜ ("d" + #2) ]
else "find_predecessor_2" [ "x"; "k"; "inner"; "find_predecessor"; "q"; "r" ]
else "find_predecessor_2" [ "x"; "k"; "inner"; "find_predecessor"; "q"; "r" ]
)%V.
Definition find_predecessor_2 :=
(rec: "find_predecessor_2" [ "x"; "k"; "inner"; "find_predecessor"; "q"; "r" ] :=
if: "inner" then
let: "continue" := #true in
(if: "r" = #null then find_predecessor_3 [ "x"; "k"; "inner"; "find_predecessor"; "q"; "r"; "find_predecessor_2"; "continue" ]
else
let: "n" := !ˢᶜ ("r" + #0) in
let: "tk" := !ˢᶜ ("n" + #0) in
let: "tv" := !ˢᶜ ("n" + #1) in
if: "tv" = #null then
if: unlink [ "q"; "r" ] then
find_predecessor_3 [ "x"; "k"; "inner"; "find_predecessor"; "q"; !ˢᶜ ("q" + #2); "find_predecessor_2"; #false ]
else
find_predecessor_3 [ "x"; "k"; #false; "find_predecessor"; "q"; "r"; "find_predecessor_2"; "continue" ]
else if: #1 compare [ "k"; "tk" ] then
find_predecessor_3 [ "x"; "k"; "inner"; "find_predecessor"; "r"; !ˢᶜ ("q" + #2); "find_predecessor_2"; #false ]
else find_predecessor_3 [ "x"; "k"; "inner"; "find_predecessor"; "q"; "r"; "find_predecessor_2"; "continue" ]
)
else "find_predecessor" [ "x"; "k" ]
)%V.
Definition find_predecessor :=
(rec: "find_predecessor" [ "x"; "k" ] :=
let: "q" := !ˢᶜ ("x" + #0) in
(find_predecessor_2 [ "x"; "k"; #true;
"find_predecessor";
"q"; !ˢᶜ ("q" + #2) ])
)%V.
Definition find_node :=
(λ: [ "x"; "k" ],
(rec: "find_node" [] :=
let: "b" := find_predecessor [ "x"; "k" ] in
(rec: "find_node_1" [ "b"; "n" ] :=
if: "n" = #null then
#null
else
let: "f" := !ˢᶜ ("n" + #2) in
if: "n" = !ˢᶜ ("b" + #2) then
let: "v" := !ˢᶜ ("n" + #1) in
if: "v" = #null then (* n is deleted *)
help_delete [ "b"; "n"; "f" ];;
"find_node" []
else if: "v" = "n" then (* b is deleted *)
"find_node" []
else if: !ˢᶜ ("b" + #1) = #null then (* b is deleted *)
"find_node" []
else
let: "c" := compare [ "k"; !ˢᶜ ("n" + #0) ] in
if: "c" = #0 then
Var "n"
else if: "c" #-1 then
#null
else
"find_node_1" [ "n"; "f" ]
else
"find_node" [] (* inconsistent read *)
) [ "b"; !ˢᶜ ("b" + #2) ]
) []
)%V.
Definition build_index_chain_1 :=
(λ: [ "z"; "level" ],
(rec: "build_index_chain_1" [ "i"; "idx" ] :=
if: "i" "level"
then "build_index_chain_1" [ "i" + #1; make_index [ "z"; "idx"; #null ] ]
else Var "idx") [ #1; #null ]
)%V.
Definition build_index_chain_2 :=
(λ: [ "z"; "level"; "idxs" ],
(rec: "build_index_chain_2" [ "i"; "idx" ] :=
if: "i" "level" then
"idxs" + "i" <- "idx" ;;
"build_index_chain_2" [ "i" + #1; make_index [ "z"; "idx"; #null ] ]
else Var "idx") [ #1; #null ]
)%V.
Definition build_index_chain_3 :=
(λ: [ "h"; "oldlevel"; "level"; "idxs" ],
let: "oldbase" := !ˢᶜ ("h" + #0) in
(rec: "build_index_chain_3" [ "j"; "newh" ] :=
if: "j" "level" then
"build_index_chain_3" [ "j" + #1;
make_head [ "oldbase"; "newh"; !("idxs" + "j"); "j" ] ]
else Var "newh") [ "oldlevel" + #1; "h" ]
)%V.
Definition build_index_chain_4 :=
(λ: [ "x"; "h"; "idx"; "level"; "idxs" ],
(rec: "build_index_chain_4" [] :=
"h" <- !ˢᶜ ("x" + #0);;
let: "old_level" := !ˢᶜ ("h" + #3) in
if: "level" "old_level" then
Var "idx"
else
let: "newh" := build_index_chain_3
[ "h"; "old_level"; "level"; "idxs" ] in
if: cas_head [ "x"; "h"; "newh" ] then
"h" <- "newh";;
"level" <- "old_level";;
!("idxs" + "level")
else
"build_index_chain_4" []) []
)%V.
Definition build_index_chain :=
(λ: [ "x"; "z"; "level"; "next"; "k" ],
let: "h" := !ˢᶜ ("x" + #0) in
let: "idx" :=
let: "max" := !ˢᶜ ("h" + #3) in
if: "level" "max"
then build_index_chain_1 [ "z"; "level" ]
else
("level" <- "max" + #1;;
let: "idxs" := new [ "level" + #1%nat ] in
let: "idx" := build_index_chain_2 [ "z"; "level"; "idxs" ] in
build_index_chain_4 [ "x"; "h"; "idx"; "level"; "idxs" ])
in "next" [ "x"; "h"; "level"; "idx"; "k" ]
)%V.
Definition insert_index_chain :=
(λ: [ "x"; "h"; "level"; "idx"; "k" ],
(rec: "insert_index_chain" [ "insertion_level"; "outer" ] :=
if: "outer" then
(rec: "insert_index_chain_1" [ "j"; "q"; "r"; "t"; "inner" ] :=
if: "inner" then
let: "continue" := #true in
if: "q" = #null then
"inner" <- #false;;
"outer" <- #false
else if: "r" = #null then #()
else
let: "n" := !ˢᶜ ("r" + #0) in
let: "tv" := !ˢᶜ ("n" + #1) in
if: "tv" = #null then
if: unlink [ "q"; "r" ] then
"inner" <- #false
else
"r" <- !ˢᶜ ("q" + #2);;
"continue" <- #false
else
let: "tk" := !ˢᶜ ("n" + #0) in
if: #1 compare [ "k"; "tk" ] then
"q" <- "r";;
"r" <- !ˢᶜ ("r" + #2);;
"continue" <- #false
else #();;
if: "inner" then
if: "continue" then
if: "j" = "insertion_level" then
let: "lk" := link [ "q"; "r"; "t" ] in
let: "tn" := !ˢᶜ ("t" + #0) in
let: "tnv" := !ˢᶜ ("tn" + #1) in
if: "lk" then
if: "tnv" = #null then
find_node [ "x"; "k" ];;
"inner" <- #false;;
"outer" <- #false
else if: "insertion_level" = #1 then
"inner" <- #false;;
"outer" <- #false
else
"insertion_level" <- "insertion_level" - #1
else
"inner" <- #false
else
#();;
if: "inner" then
if: "continue" then
"j" <- "j" - #1;;
if: "insertion_level" "j" then
if: "j" + #1 "level" then
"t" <- !ˢᶜ ("t" + #1)
else #()
else #();;
"q" <- !ˢᶜ ("q" + #1);;
"r" <- !ˢᶜ ("q" + #2)
else #()
else #()
else #()
else #();;
"insert_index_chain_1" [ "j"; "q"; "r"; "t"; "inner" ]
else #()
) [ !ˢᶜ ("h" + #3); "h"; !ˢᶜ ("h" + #2); "idx"; #true ];;
"insert_index_chain" [ "insertion_level"; "outer" ]
else #()
) [ "level"; #true ]
)%V.
Definition do_get :=
(rec: "do_get" [ "x"; "k" ] :=
let: "n" := find_node [ "x"; "k"] in
if: "n" = #null then
#null
else
let: "v" := !ˢᶜ ("n" + #1) in
if: "v" = #null then
"do_get" [ "x"; "k" ]
else
Var "v"
)%V.
Definition make_map_impl :=
#true%V.
Definition get_impl :=
do_get%V.
Definition put_impl :=
((rec: "put" [ "x";"k";"v" ] := !ˢᶜ "x"))%V.
Definition remove_impl :=
#true%V.
End skiplist.
\ No newline at end of file
This diff is collapsed.
......@@ -148,6 +148,8 @@ Definition atomic (e: expr) : bool :=
bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
| BinOp op e1 e2 =>
bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| _ => false
end.
Lemma atomic_correct e : atomic e language.atomic (to_expr e).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment