Commit 3f48de33 authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

prove SPMC message passing

parent c4c9bf84
......@@ -161,6 +161,7 @@ theories/examples/queue/proof_abs_graph_graph.v
theories/examples/queue/proof_hw_graph.v
theories/examples/queue/proof_per_elem_graph.v
theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_mp2_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_ms_closed.v
theories/examples/queue/proof_ms_gps.v
......
From iris.algebra Require Import auth numbers.
From iris.proofmode Require Import tactics.
From gpfsl.lang Require Import notation.
From gpfsl.lang Require Import notation.
From gpfsl.logic Require Import logatom invariants proofmode.
From gpfsl.logic Require Import new_delete repeat_loop.
From gpfsl.gps Require Import surface_iSP protocols escrows.
From gpfsl.examples.queue Require Import spec_graph.
From gpfsl.examples Require Import set_helper.
Require Import iris.prelude.options.
Local Open Scope Z_scope.
Local Notation graph := (graph qevent).
Implicit Types (G : graph).
Section spmc_mp.
Context `{!noprolG Σ,
!gpsG Σ boolProtocol,
!inG Σ (graphR qevent),
!inG Σ (authR natUR)}.
Context (mpN qN : namespace)
(DISJ1: mpN ## histN) (DISJ2: qN ## histN) (DISJ3: mpN ## qN).
Definition mpinvN := mpN .@ "inv".
Definition flagN := mpN .@ "flag".
Hypothesis Q : weak_queue_spec Σ.
Local Existing Instances QueueInv_Objective QueueLocal_Persistent.
Local Notation iProp := (iProp Σ).
Local Notation vProp := (vProp Σ).
Definition spmc_mp : expr :=
let: "q" := Q.(new_queue) [] in
let: "flag" := new [ #1] in
"flag" <- #0 ;;
Fork (Q.(enqueue) ["q"; #1] ;;
Q.(enqueue) ["q"; #2] ;;
"flag" <-ʳᵉˡ #1 ) ;;
Fork (Q.(dequeue) ["q"]);;
(repeat: !ᵃᶜ "flag") ;;
Q.(dequeue) ["q"].
(** Invariant on the queue state: A successful dequeue consumes a token [◯ 1]
and there are only 2 such tokens. *)
Definition MPInv γg γm q : vProp := G,
Q.(QueueInv) γg q G
own γm ( 2%nat)
own γm ( (size G.(com)))
.
(** The flag location transfers the knowledge about the enqueue events. *)
Definition FlagProtocol γg q s (v : val) : vProp :=
match s with
| false => v = #0
| true => v = #1 G M e1 e2 eV1 eV2 v1 v2,
Q.(QueueLocal) qN γg q G M
e1 e2
G.(Es) !! e1 = Some eV1 G.(Es) !! e2 = Some eV2
eV1.(ge_event) = Enq v1 eV2.(ge_event) = Enq v2
e1 M e2 M
end.
Definition FlagInterp γg q : interpO Σ boolProtocol :=
λ _ _ _ _, FlagProtocol γg q.
Global Instance FlagProtocol_persistent γg q s v :
Persistent (FlagProtocol γg q s v).
Proof. rewrite /Persistent. destruct s; by iIntros "#FP". Qed.
Global Instance FlagInterp_persistent γg q s l γl t b v V :
Persistent (FlagInterp γg q s l γl t b v V).
Proof. destruct b; apply _. Qed.
Lemma spmc_mp_spec tid :
{{{ True }}} spmc_mp @ tid; {{{ v, RET #v; 0 < v }}}.
Proof using All.
iIntros (Φ) "_ Post".
rewrite /spmc_mp.
wp_apply (new_queue_spec _ qN with "[//]").
iIntros (γg q) "[#QL QI]".
iMod (own_alloc (( 2%nat 0%nat) ( 1%nat 1%nat))) as (γm) "[●m [◯m1 ◯m2]]".
{ rewrite -assoc -!auth_frag_op !nat_op /=. by apply auth_both_valid. }
wp_let.
wp_apply wp_new; [done..|].
iIntros (f) "(_ & f↦ & _)". rewrite own_loc_na_vec_singleton.
wp_let. wp_write.
(* setup the invariant and the protocol *)
iMod (GPS_iSP_Init flagN (FlagInterp γg q) (FlagInterp γg q false) f false with "f↦ [//]")
as (γf ?) "FPW".
iDestruct (GPS_iSP_SWWriter_Reader with "FPW") as "#FPR".
iMod (inv_alloc mpinvN _ (MPInv γg γm q) with "[QI ●m]") as "#I".
{ iNext. iExists . iFrame "QI". iDestruct "●m" as "[$ $]". }
(* enqueuing thread *)
wp_apply (wp_fork with "[FPW]"); [done|..].
{ iIntros "!>" (?).
(* enqueue 1 *)
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]".
awp_apply (enqueue_spec with "⊒V QL"); [solve_ndisj|done|].
iInv mpinvN as (G1) "(QI & >●m & >◯m)".
iAaccIntro with "QI".
{ iFrame. iIntros "QI !> !>". iExists _. iFrame. }
iIntros (V1 G1' enqId1 enq1 Venq1 M1') "(QI & #⊒V1 & #QL1 & %F) !>".
set (eV1 := mkGraphEvent enq1 Venq1 M1') in *.
rewrite /is_enqueue in F.
destruct F as (SubG11' &_&_&_& -> & ? & EsG1' &_& ComG1' & InM1' &_).
have HeV1 : G1'.(Es) !! enqId1 = Some eV1.
{ subst enqId1. rewrite EsG1'. apply lookup_app_1_eq. }
iDestruct (view_at_elim with "⊒V1 QL1") as "{QL QL1} QL1".
iSplitR "FPW".
{ iNext. iExists G1'. rewrite -ComG1'. iFrame. }
iIntros "_". wp_seq.
(* enqueue 2 *)
awp_apply (enqueue_spec with "⊒V QL1"); [solve_ndisj|done|].
iInv mpinvN as (G2) "(QI & >●m & >◯m)".
rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]".
iDestruct (graph_master_consistent with "Gm") as %EGC.
iPoseProof (QueueLocal_graph_snap with "QL1") as "Gs".
iDestruct (graph_master_snap_included with "Gm Gs") as %SubG1'2.
iSpecialize ("QI" with "[$Gm]").
iAaccIntro with "QI".
{ iFrame. iIntros "QI !> !>". iExists _. iFrame. }
iIntros (V2 G2' enqId2 enq2 Venq2 M2') "(QI & #⊒V2 & #QL2 & %F) !>".
set (eV2 := mkGraphEvent enq2 Venq2 M2') in *.
rewrite /is_enqueue in F.
destruct F as (SubG22' & SubM1'2' &_&_& -> & ? & EsG2' &_& ComG2' & InM2' &_).
have HeV2 : G2'.(Es) !! enqId2 = Some eV2.
{ subst enqId2. rewrite EsG2'. apply lookup_app_1_eq. }
iDestruct (view_at_elim with "⊒V2 QL2") as "{QL2} QL2".
iSplitR "FPW".
{ iNext. iExists G2'. rewrite -ComG2'. iFrame. }
iIntros "_". wp_seq.
(* set the flag *)
iApply (GPS_iSP_SWWrite flagN (FlagInterp γg q) (FlagInterp γg q false)
True%I _ AcqRel _ _ true _ #1 with "[$FPW]");
[solve_ndisj|done|done|by right|done|..].
{ simpl. iSplitL; [|done].
iIntros "!> * % !>". iSplitR; [done|].
iExists G2', M2', enqId1, enqId2, eV1, eV2, _, _. iFrame "QL2".
iPureIntro. split_and!; [| |done|done|done| |done].
- subst enqId1 enqId2.
have ? : (length (Es G1) < length (Es G1')).
{ rewrite EsG1' app_length /=. lia. }
suff ? : (length (Es G1') length (Es G2))%nat by lia.
apply prefix_length. by destruct SubG1'2.
- eapply prefix_lookup; [done|].
destruct SubG1'2, SubG22'. by trans G2.(Es).
- set_solver +InM1' SubM1'2'. }
by iIntros "!> * _". }
iIntros "_". wp_seq.
(* dequeuing thread *)
wp_apply (wp_fork with "[◯m1]"); [done|..].
{ iIntros "!>" (?).
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]".
awp_apply (dequeue_spec with "⊒V QL"); [solve_ndisj|].
iInv mpinvN as (G) "(QI & >●m & >◯m)".
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
iAaccIntro with "QI".
{ iFrame. iIntros "QI !> !>". iExists _. iFrame. }
iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F) !>".
iSplitL; last by iIntros. iNext. iExists G'.
set (dV := mkGraphEvent deq Vdeq M') in *.
destruct F as (SubG' & SubM' & HVin & HVcomm & [CASE|CASE]).
- destruct CASE as (_&_&_&_&_& ComG' &_). rewrite ComG'. iFrame.
- destruct CASE as (_&_&_&_& NoSo & _ & _ & ComG' & _).
iFrame. iCombine "◯m ◯m1" as "◯m".
rewrite ComG' size_union.
+ rewrite size_singleton (comm plus). iFrame.
+ apply disjoint_singleton_l. rewrite -(bsq_cons_so_com _ QC).
by apply NoSo. }
iIntros "_". wp_seq.
(* main thread *)
iClear "QL".
(* wait for the flag to be set *)
wp_bind (repeat: _)%E.
iLöb as "IH".
iApply wp_repeat; [done|].
iApply (GPS_iSP_Read flagN (FlagInterp γg q) (FlagInterp γg q false) (FlagInterp γg q false f γf)
with "[$FPR]"); [solve_ndisj|done|done|by right|..].
{ iIntros "!>" (????) "!>". iSplit; last iSplit; by iIntros "#$". }
iIntros "!>" (? s' v'). simpl.
iDestruct 1 as "[% [FPR' FI]]". destruct s'; simpl; last first.
{ (* keep looping *)
iDestruct "FI" as %->.
iExists 0. iSplit; [done|]. simpl.
by iApply ("IH" with "Post ◯m2"). }
(* done looping *)
iClear "IH FPR FPR'".
iDestruct "FI" as "[-> QL]".
iExists 1. iSplit; [done|]. simpl. iIntros "!> !>". wp_seq.
iDestruct "QL" as (G0 M0 ??????) "(#QL & %NEe12 & %HeV1 & %HeV2 & %Henq1 & %Henq2 & %HM1 & %HM2)".
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]".
iApply (wp_step_fupd _ _ _ _ ( _, _ - _)%I with "[$Post]"); [auto..|].
awp_apply (dequeue_spec with "⊒V QL"); [solve_ndisj|].
iInv mpinvN as (G) "(QI & >●m & >◯m)".
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]".
iDestruct (graph_master_consistent with "Gm") as %EGC.
iPoseProof (QueueLocal_graph_snap with "QL") as "Gs".
iDestruct (graph_master_snap_included with "Gm Gs") as %SubG0G.
iSpecialize ("QI" with "[$Gm]").
apply (prefix_lookup _ G.(Es)) in HeV1; [|by destruct SubG0G].
apply (prefix_lookup _ G.(Es)) in HeV2; [|by destruct SubG0G].
iCombine "◯m ◯m2" as "◯m".
iDestruct (own_valid_2 with "●m ◯m") as %[LT%nat_included _]%auth_both_valid_discrete.
have {}LT : (size (com G) 1)%nat by lia.
iAaccIntro with "QI".
{ iDestruct "◯m" as "[◯m $]". iFrame. iIntros "QI !> !>". iExists _. iFrame. }
iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F)".
set (dV := mkGraphEvent deq Vdeq M') in *.
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
destruct F as (SubG' & SubM' & HVin & HVcomm & [CASE|CASE]).
- (* empty pop *) exfalso.
destruct CASE as (-> & -> & ? & EsG' & _ & ComG' & ?).
have HdV : G'.(Es) !! deqId = Some dV.
{ subst deqId. rewrite EsG'. apply lookup_app_1_eq. }
(* WLOG, let e1 be an unmatched enqueue *)
wlog: e1 e2 eV1 eV2 v1 v2 NEe12 HeV1 HeV2 Henq1 Henq2 HM1 HM2 / unmatched_enq_2 G e1.
{ case (decide (unmatched_enq_2 G e1)) => [?|MATCH] X; first by eapply (X e1 e2).
eapply (X e2 e1); [done..|]. clear X.
unfold unmatched_enq_2 in MATCH |- *.
split.
{ exists v2.
apply (f_equal (fmap ge_event)) in HeV2.
move: HeV2. rewrite /= Henq2 //. }
intros d2 In2 So2. apply MATCH.
split.
{ exists v1.
apply (f_equal (fmap ge_event)) in HeV1.
move: HeV1. rewrite /= Henq1 //. }
intros d1 In1 So1.
rewrite -(bsq_cons_so_com _ QC) in LT.
have INCL : {[(e1,d1); (e2,d2)]} G.(so) by set_solver +So1 So2.
move: INCL => /(subseteq_size _ _).
rewrite size_union; [|set_solver +NEe12].
rewrite !size_singleton. lia. }
intros [_ UNMATCHED].
(* Empty dequeue couldn't have seen an unmatched enqueue. Contradiction. *)
refine (_ (bsq_cons_non_empty _ QC' _ _ HdV ltac:(done) e1 _ eV1 _ ltac:(done) _)); cycle 1.
{ rewrite EsG'. eapply prefix_lookup; [done|by eexists]. }
{ set_solver +SubM' HM1. }
intros (d' & Com_ed' & _). rewrite ComG' -(bsq_cons_so_com _ QC) in Com_ed'.
apply (UNMATCHED d'); [|done].
specialize (egcons_so _ EGC _ _ Com_ed') as (_ & dV' & _ & HdV' & _).
apply lookup_lt_Some in HdV'.
rewrite /to_set. apply elem_of_set_seq. lia.
- (* successful dequeue *)
rewrite /is_enqueue /is_dequeue in CASE.
destruct CASE as (?&_&_&_& NoSo & _ & _ & ComG' & _).
iIntros "!>". iSplitL.
{ iNext. iExists _. iFrame.
rewrite ComG' size_union.
- rewrite size_singleton (comm plus). iFrame.
- apply disjoint_singleton_l. rewrite -(bsq_cons_so_com _ QC).
by apply NoSo. }
iIntros "_ Post". by iApply "Post".
Qed.
End spmc_mp.
......@@ -9,18 +9,6 @@ Require Import iris.prelude.options.
Local Notation event_list := (event_list qevent).
Definition unmatched_enq_2 G eid : Prop :=
( v : Z, ge_event <$> (G.(Es) !! eid) = Some (Enq v))
set_Forall (λ id', (eid, id') G.(so)) (to_set G.(Es)).
Instance umatched_enq_dec G eid : Decision (unmatched_enq_2 G eid).
Proof.
apply and_dec; last apply _.
case (G.(Es) !! eid) as [[e V]|].
- destruct e; [left | right | right]; eauto; intros []; discriminate.
- right. intros []; discriminate.
Qed.
Section RSL.
Context {Σ : gFunctors} `{noprolG Σ, inG Σ (graphR qevent)}.
......
From stdpp Require Import namespaces.
From gpfsl.logic Require Import logatom.
From gpfsl.examples Require Export set_helper.
From gpfsl.examples.graph Require Export spec.
From gpfsl.examples.queue Require Export event.
......@@ -17,6 +18,18 @@ Definition unmatched_enq G eid : Prop :=
( v : Z, ge_event <$> (G.(Es) !! eid) = Some (Enq v))
( id, (eid, id) G.(so)).
Definition unmatched_enq_2 G eid : Prop :=
( v : Z, ge_event <$> (G.(Es) !! eid) = Some (Enq v))
set_Forall (λ id', (eid, id') G.(so)) (to_set G.(Es)).
Instance umatched_enq_dec G eid : Decision (unmatched_enq_2 G eid).
Proof.
apply and_dec; last apply _.
case (G.(Es) !! eid) as [[e V]|].
- destruct e; [left | right | right]; eauto; intros []; discriminate.
- right. intros []; discriminate.
Qed.
(** Queue predicates *)
Definition QueueLocalT Σ : Type :=
namespace gname loc graph logView vProp Σ.
......
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