diff --git a/iris_heap_lang/lib/peterson.v b/iris_heap_lang/lib/peterson.v index f8e7ea58b636b91979796288523e2b99130b0103..9e8cc6b2db3a46ef930b66e745fcdb2785f5d9d4 100644 --- a/iris_heap_lang/lib/peterson.v +++ b/iris_heap_lang/lib/peterson.v @@ -1,37 +1,44 @@ From iris.algebra Require Import excl auth. From iris.base_logic Require Import invariants. -From cosmo.program_logic Require Export proofmode. +From iris.heap_lang Require Export notation proofmode. Set Default Proof Using "Type". Open Scope Z. - - (* * Implementation. *) - - Definition make : val := λ: <>, - let: "turn" := ref_at #0 in - let: "flag0" := ref_at #false in - let: "flag1" := ref_at #false in + let: "turn" := ref #0 in + let: "flag0" := ref #false in + let: "flag1" := ref #false in (("turn", #0, "flag0", "flag1"), ("turn", #1, "flag1", "flag0")). +Definition wait : val := + rec: "go" "other_flag" "turn" "tid" := + if: (! "other_flag") && (! "turn" = (#1 - "tid")) + then "go" "other_flag" "turn" "tid" else #(). + Definition acquire: val := λ: "lk", - let: ("turn", "tid", "my_flag", "other_flag") := "lk" in - "my_flag" <-at #true ;; - "turn" <-at (#1 - "tid") ;; - while: (!at "other_flag") && (!at "turn" = (#1 - "tid")) do - #() - enddo. + let: "turn" := Fst $ Fst $ Fst $ "lk" in + let: "tid" := Snd $ Fst $ Fst $ "lk" in + let: "my_flag" := Snd $ Fst $ "lk" in + let: "other_flag" := Snd $ "lk" in + (* let: ("turn", "tid", "my_flag", "other_flag") := "lk" in *) + "my_flag" <- #true ;; + "turn" <- (#1 - "tid") ;; + wait "other_flag" "turn" "tid". Definition release : val := λ: "lk", - let: ("turn", "tid", "my_flag", "other_flag") := "lk" in - "my_flag" <-at #false. + let: "turn" := Fst $ Fst $ Fst $ "lk" in + let: "tid" := Snd $ Fst $ Fst $ "lk" in + let: "my_flag" := Snd $ Fst $ "lk" in + let: "other_flag" := Snd $ "lk" in + (* let: ("turn", "tid", "my_flag", "other_flag") := "lk" in *) + "my_flag" <- #false. @@ -45,11 +52,10 @@ Inductive peterson_state : Type := Outside | Entered | Waiting | InCriticalSecti Instance peterson_state_inhabited : Inhabited peterson_state := populate Outside. Instance peterson_state_eq_dec : EqDecision peterson_state. Proof. intros [][] ; first [ by right | by left ]. Qed. -Canonical Structure peterson_stateO : ofeT := leibnizO peterson_state. +Canonical Structure peterson_stateO : ofe := leibnizO peterson_state. Class PetersonG Σ := { peterson_state_inG :> inG Σ (authUR (optionUR (exclR peterson_stateO))) ; - peterson_view_inG :> inG Σ (authUR (optionUR (exclR viewO))) ; }. (* @@ -61,11 +67,10 @@ Class PetersonG Σ := { Record peterson_gnames := Peterson_gnames { peterson_state_gname : gname ; - peterson_view_gname : gname ; }. Section proof. - Context `{!cosmoG Σ, !PetersonG Σ} (N : namespace). + Context `{!heapGS Σ, !PetersonG Σ} (N : namespace). (* ICFP20: “peterson_inv” is the assertion “PetersonInv” from the paper in @@ -73,52 +78,48 @@ Section proof. *) Definition peterson_inv_threadlocal - (flag : location) (γ : peterson_gnames) (f : bool) (s : peterson_state) (V : view) + (flag : loc) (γ : peterson_gnames) (f : bool) (s : peterson_state) : iProp Σ := - ( flag ↦at( #f, V ) + ( flag ↦ #f ∗ own γ.(peterson_state_gname) (● (Excl' s)) - ∗ own γ.(peterson_view_gname) (● (Excl' V)) ∗ ⌜(s = Outside) ∨ (f = true)⌝ )%I. Definition peterson_inv - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (R : vProp Σ) + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : iProp Σ := - (∃ (t : Z) (f0 f1 : bool) (s0 s1 : peterson_state) (V0 V1 Vt : view), + (∃ (t : Z) (f0 f1 : bool) (s0 s1 : peterson_state), ⌜0 ≤ tid ≤ 1⌝ ∗ ⌜0 ≤ t ≤ 1⌝ - ∗ turn ↦at( #t, Vt ) - ∗ peterson_inv_threadlocal flag0 γ0 f0 s0 V0 - ∗ peterson_inv_threadlocal flag1 γ1 f1 s1 V1 + ∗ turn ↦ #t + ∗ peterson_inv_threadlocal flag0 γ0 f0 s0 + ∗ peterson_inv_threadlocal flag1 γ1 f1 s1 ∗ ⌜if decide (t = tid) then - s0 = Waiting → s1 = Waiting ∧ Vt = V1 + s0 = Waiting → s1 = Waiting else - s1 = Waiting → s0 = Waiting ∧ Vt = V0 + s1 = Waiting → s0 = Waiting ⌝ - ∗ (⌜s0 ≠ InCriticalSection ∧ s1 ≠ InCriticalSection⌝ -∗ R (V0 ⊔ V1)) + ∗ (⌜s0 ≠ InCriticalSection ∧ s1 ≠ InCriticalSection⌝ -∗ R) )%I. (* ICFP20: “is_peterson” corresponds to the assertion “canLock” of the paper. *) - Definition is_peterson (lk : val) (γ0 : peterson_gnames) (R : vProp Σ) : vProp Σ := - (∃ (tid : Z) (turn flag0 flag1 : location) (γ1 : peterson_gnames) (V0 : view), + Definition is_peterson (lk : val) (γ0 : peterson_gnames) (R : iProp Σ) : iProp Σ := + (∃ (tid : Z) (turn flag0 flag1 : loc) (γ1 : peterson_gnames), ⌜lk = (#turn, #tid, #flag0, #flag1)%V⌝ - ∗ ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ ⎡ own γ0.(peterson_state_gname) (◯ (Excl' Outside)) ⎤ - ∗ ⎡ own γ0.(peterson_view_gname) (◯ (Excl' V0)) ⎤ - ∗ monPred_in V0 + ∗ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own γ0.(peterson_state_gname) (◯ (Excl' Outside)) )%I. (* ICFP20: “locked” corresponds to the assertion “locked” of the paper. *) - Definition locked (lk : val) (γ0 : peterson_gnames) (R : vProp Σ) : vProp Σ := - (∃ (tid : Z) (turn flag0 flag1 : location) (γ1 : peterson_gnames) (V0 : view), + Definition locked (lk : val) (γ0 : peterson_gnames) (R : iProp Σ) : iProp Σ := + (∃ (tid : Z) (turn flag0 flag1 : loc) (γ1 : peterson_gnames), ⌜lk = (#turn, #tid, #flag0, #flag1)%V⌝ - ∗ ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ ⎡ own γ0.(peterson_state_gname) (◯ (Excl' InCriticalSection)) ⎤ - ∗ ⎡ own γ0.(peterson_view_gname) (◯ (Excl' V0)) ⎤ + ∗ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own γ0.(peterson_state_gname) (◯ (Excl' InCriticalSection)) )%I. @@ -134,59 +135,55 @@ Section proof. Proof. lia. Qed. Lemma peterson_inv_swap - (tid tid' : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (R : vProp Σ) : + (tid tid' : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : tid' = 1 - tid → peterson_inv tid turn flag0 flag1 γ0 γ1 R -∗ peterson_inv tid' turn flag1 flag0 γ1 γ0 R. Proof. iIntros (->) "I". iDestruct "I" as - (t f0 f1 s0 s1 V0 V1 Vt Btid%int_is_bool Bt%int_is_bool) "(?&?&?&Ht&HR)". + (t f0 f1 s0 s1 Btid%int_is_bool Bt%int_is_bool) "(?&?&?&Ht&HR)". iDestruct "Ht" as %Ht. - rewrite Logic.and_comm (comm join) /peterson_inv. - repeat (iExists _). iFrame. iPureIntro. + rewrite Logic.and_comm. + iExists t, f1, f0, s1, s0. iFrame. + iPureIntro. case Bt ; case Btid ; intros -> -> ; by case_match. Qed. Lemma peterson_inv_swap_equiv - (tid tid' : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (R : vProp Σ) : + (tid tid' : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : tid' = 1 - tid → peterson_inv tid turn flag0 flag1 γ0 γ1 R ⊣⊢ peterson_inv tid' turn flag1 flag0 γ1 γ0 R. Proof. intros ?. iSplit ; iApply peterson_inv_swap ; by lia. Qed. - Lemma make_spec (R : vProp Σ) : + Lemma make_spec (R : iProp Σ) : {{{ R }}} make #() {{{ lk0 lk1 γ0 γ1 , RET (lk0, lk1) ; ⌜lk0 ≠ lk1⌝ ∗ is_peterson lk0 γ0 R ∗ is_peterson lk1 γ1 R }}}. Proof. iIntros (Φ) "HR Post". - (* unpack R *) - iDestruct (monPred_in_intro with "HR") as (V) "[ #? ? ]". (* allocate locations *) wp_lam. - wp_ref turn at V. - wp_ref flag0 at V. - wp_ref flag1 at V. + wp_alloc turn. + wp_alloc flag0. + wp_alloc flag1. (* create ghost variables *) iMod (own_alloc (● (Excl' Outside) ⋅ ◯ (Excl' Outside))) as (γ0s) "[Hγ0s● Hγ0s◯]". { by apply auth_both_valid_discrete. } iMod (own_alloc (● (Excl' Outside) ⋅ ◯ (Excl' Outside))) as (γ1s) "[Hγ1s● Hγ1s◯]". { by apply auth_both_valid_discrete. } - iMod (own_alloc (● (Excl' V) ⋅ ◯ (Excl' V))) as (γ0V) "[Hγ0V● Hγ0V◯]". - { by apply auth_both_valid_discrete. } - iMod (own_alloc (● (Excl' V) ⋅ ◯ (Excl' V))) as (γ1V) "[Hγ1V● Hγ1V◯]". - { by apply auth_both_valid_discrete. } - set γ0 := Peterson_gnames γ0s γ0V. - set γ1 := Peterson_gnames γ1s γ1V. + set γ0 := Peterson_gnames γ0s. + set γ1 := Peterson_gnames γ1s. (* create invariant *) iMod (inv_alloc _ _ (peterson_inv 0 turn flag0 flag1 γ0 γ1 R) - with "[- Hγ0s◯ Hγ1s◯ Hγ0V◯ Hγ1V◯ Post]") as "#I". + with "[- Hγ0s◯ Hγ1s◯ Post]") as "#I". { rewrite /peterson_inv /peterson_inv_threadlocal. repeat (iExists _). iFrame. iPureIntro. repeat split ; by auto. } wp_pures. iApply "Post". (* create the two representation predicates *) + iModIntro. iSplit ; first done. - iSplitL "Hγ0s◯ Hγ0V◯" ; + iSplitL "Hγ0s◯" ; last (rewrite peterson_inv_swap_equiv ; last done) ; repeat (iExists _) ; by iFrame "# ∗". Qed. @@ -210,76 +207,65 @@ Section proof. | iDestruct tmp_name as pat2 ]. Lemma write_my_flag_false - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (V0 V0' : view) (R : vProp Σ) : + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : {{{ - ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ monPred_in V0' - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ - ∗ ⎡ R V0' ⎤ + inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) + ∗ R }}} - #flag0 <-at #false + #flag0 <- #false {{{ RET #() ; - ⎡ own (peterson_state_gname γ0) (◯ Excl' Outside) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0') ⎤ + own (peterson_state_gname γ0) (◯ Excl' Outside) }}}. Proof. - iIntros (Φ) "(#? & #? & Hs0◯ & HV0◯ & HR) Post". + iIntros (Φ) "(#? & Hs0◯ & HR) Post". (* open invariant *) - iInv N as - (t f0 f1 ? s1 ? V1 Vt) - "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & HV0● & _) & Hthread1 & >Ht & _)" ; + iInv N as (t f0 f1 s0 s1) + "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & _) & Hthread1 & >Ht & _)"; iDestruct "Btid" as %Btid ; iDestruct "Bt" as %Bt ; iDestruct "Ht" as %Ht. (* unify the thread’s and invariant’s knowledge of the ghost state *) auth_unify "Hs0●" "Hs0◯". - auth_unify "HV0●" "HV0◯". (* update the ghost state *) auth_update "Hs0●" "Hs0◯" Outside. - auth_update "HV0●" "HV0◯" V0'. (* perform atomic operation *) - wp_write at V0'. + wp_store. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ Post". + iModIntro. iSplitR "Hs0◯ Post". { repeat (iExists _). iFrame. iPureIntro. repeat (split ; auto). - case_match ; [ done | by intros [? _]%Ht ]. + case_match ; [ done | by intros ?%Ht]. } (* conclude *) iApply "Post". by iFrame. Qed. Lemma write_my_flag_true - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (V0 : view) (R : vProp Σ) : + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : {{{ - ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ monPred_in V0 - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' Outside) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own (peterson_state_gname γ0) (◯ Excl' Outside) }}} - #flag0 <-at #true + #flag0 <- #true {{{ RET #() ; - ⎡ own (peterson_state_gname γ0) (◯ Excl' Entered) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + own (peterson_state_gname γ0) (◯ Excl' Entered) }}}. Proof. - iIntros (Φ) "(#? & #? & Hs0◯ & HV0◯) Post". + iIntros (Φ) "(#? & Hs0◯) Post". (* open invariant *) - iInv N as - (t f0 f1 ? s1 ? V1 Vt) - "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & HV0● & _) & Hthread1 & >Ht & HR)" ; + iInv N as (t f0 f1 s0 s1) + "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & _) & Hthread1 & >Ht & HR)"; iDestruct "Btid" as %Btid ; iDestruct "Bt" as %Bt ; iDestruct "Ht" as %Ht. (* unify the thread’s and invariant’s knowledge of the ghost state *) auth_unify "Hs0●" "Hs0◯". - auth_unify "HV0●" "HV0◯". (* update the ghost state *) auth_update "Hs0●" "Hs0◯" Entered. (* perform atomic operation *) - wp_write at V0. + wp_store. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ Post". + iModIntro. iSplitR "Hs0◯ Post". { repeat (iExists _). iFrame. repeat (iSplit ; auto). - - iPureIntro. case_match ; [ done | by intros [? _]%Ht ]. + - iPureIntro. case_match ; [ done | by intros ?%Ht ]. - iIntros ([_ ?]). by iApply "HR". } (* conclude *) @@ -287,36 +273,32 @@ Section proof. Qed. Lemma write_turn - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (V0 : view) (R : vProp Σ) : + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : {{{ - ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ monPred_in V0 - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' Entered) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own (peterson_state_gname γ0) (◯ Excl' Entered) }}} - #turn <-at #(1-tid) + #turn <- #(1-tid) {{{ RET #() ; - ⎡ own (peterson_state_gname γ0) (◯ Excl' Waiting) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + own (peterson_state_gname γ0) (◯ Excl' Waiting) }}}. Proof. - iIntros (Φ) "(#? & #? & Hs0◯ & HV0◯) Post". + iIntros (Φ) "(#? & Hs0◯) Post". (* open invariant *) iInv N as - (t f0 f1 ? s1 ? V1 Vt) - "(>Btid & _ & Hturn & >(Hflag0 & Hs0● & HV0● & Himpl0) & Hthread1 & _ & HR)" ; + (t f0 f1 s0 s1) + "(>Btid & _ & Hturn & >(Hflag0 & Hs0● & Himpl0) & Hthread1 & _ & HR)"; iDestruct "Btid" as %Btid ; iDestruct "Himpl0" as %Himpl0. (* unify the thread’s and invariant’s knowledge of the ghost state *) auth_unify "Hs0●" "Hs0◯". - auth_unify "HV0●" "HV0◯". (* deduce that f0 = true *) destruct Himpl0 as [? | ->] ; first congruence. (* update the ghost state *) auth_update "Hs0●" "Hs0◯" Waiting. (* perform atomic operation *) - wp_write at V0. + wp_store. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ Post". + iModIntro. iSplitR "Hs0◯ Post". { repeat (iExists _). iFrame. repeat iSplit ; auto with lia. - iPureIntro. case_match ; [ lia | done ]. @@ -327,34 +309,30 @@ Section proof. Qed. Lemma read_other_flag - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (V0 : view) (R : vProp Σ) : + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : {{{ - ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' Waiting) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own (peterson_state_gname γ0) (◯ Excl' Waiting) }}} - !at #flag1 + ! #flag1 {{{ (f1 : bool), RET #f1 ; - ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ - ∗ (if f1 then - ⎡ own (peterson_state_gname γ0) (◯ Excl' Waiting) ⎤ + (if f1 then + own (peterson_state_gname γ0) (◯ Excl' Waiting) else - ⎡ own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) ⎤ - ∗ ∃ (V1 : view), monPred_in V1 ∗ ⎡ R (V0 ⊔ V1) ⎤ + own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) ∗ R ) }}}. Proof. - iIntros (Φ) "(#? & Hs0◯ & HV0◯) Post". + iIntros (Φ) "(#? & Hs0◯) Post". (* open invariant *) iInv N as - (t f0 f1 s0 s1 V0' V1 Vt) - "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & HV0● & #Himpl0) - & >(Hflag1 & Hs1● & HV1● & #Himpl1) & >Ht & HR)" ; + (t f0 f1 s0 s1) + "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & #Himpl0) + & >(Hflag1 & Hs1● & #Himpl1) & >Ht & HR)"; iDestruct "Btid" as %Btid ; iDestruct "Bt" as %Bt ; iDestruct "Ht" as %Ht ; iDestruct "Himpl0" as %Himpl0 ; iDestruct "Himpl1" as %Himpl1. (* unify the thread’s and invariant’s knowledge of the ghost state *) auth_unify "Hs0●" "Hs0◯". - auth_unify "HV0●" "HV0◯". (* deduce that f0 = true *) destruct Himpl0 as [? | ->] ; first congruence. (* case analysis on other_flag *) @@ -362,9 +340,9 @@ Section proof. (* if other_flag = true: do nothing *) { (* perform atomic operation *) - wp_read as "_". + wp_load. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ Post". + iModIntro. iSplitR "Hs0◯ Post". { repeat (iExists _). iFrame. repeat iSplit ; by auto with lia. } (* conclude *) iApply "Post". by iFrame. @@ -376,52 +354,49 @@ Section proof. (* update the ghost state *) auth_update "Hs0●" "Hs0◯" InCriticalSection. (* perform atomic operation *) - wp_read. + wp_load. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ HR Post". + iModIntro. iSplitR "Hs0◯ HR Post". { repeat (iExists _). iFrame. repeat iSplit ; auto with lia. - by case_match. - by iIntros ([? _]). } (* conclude *) - iApply "Post". iFrame. (* get R: *) iExists V1. iFrame "#". by iApply "HR". + iApply "Post". iFrame. (* get R: *) by iApply "HR". } Qed. Lemma read_turn - (tid : Z) (turn flag0 flag1 : location) (γ0 γ1 : peterson_gnames) (V0 : view) (R : vProp Σ) : + (tid : Z) (turn flag0 flag1 : loc) (γ0 γ1 : peterson_gnames) (R : iProp Σ) : {{{ - ⎡ inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) ⎤ - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' Waiting) ⎤ - ∗ ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ + inv N (peterson_inv tid turn flag0 flag1 γ0 γ1 R) + ∗ own (peterson_state_gname γ0) (◯ Excl' Waiting) }}} - !at #turn + ! #turn {{{ (t : Z), RET #t ; - ⎡ own (peterson_view_gname γ0) (◯ Excl' V0) ⎤ - ∗ ( + ( ( ⌜t = 1-tid⌝ - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' Waiting) ⎤ + ∗ own (peterson_state_gname γ0) (◯ Excl' Waiting) ) ∨ ( ⌜t = tid⌝ - ∗ ⎡ own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) ⎤ - ∗ ∃ (V1 : view), monPred_in V1 ∗ ⎡ R (V0 ⊔ V1) ⎤ + ∗ own (peterson_state_gname γ0) (◯ Excl' InCriticalSection) + ∗ R ) ) }}}. Proof. - iIntros (Φ) "(#? & Hs0◯ & HV0◯) Post". + iIntros (Φ) "(#? & Hs0◯) Post". (* open invariant *) iInv N as - (t f0 f1 ? s1 ? V1 Vt) - "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & HV0● & Himpl0) & Hthread1 & >Ht & HR)" ; + (t f0 f1 ? s1) + "(>Btid & >Bt & Hturn & >(Hflag0 & Hs0● & Himpl0) & Hthread1 & >Ht & HR)" ; iDestruct "Btid" as %Btid%int_is_bool ; iDestruct "Bt" as %Bt%int_is_bool ; iDestruct "Ht" as %Ht ; iDestruct "Himpl0" as %Himpl0. (* unify the thread’s and invariant’s knowledge of the ghost state *) auth_unify "Hs0●" "Hs0◯". - auth_unify "HV0●" "HV0◯". (* deduce that f0 = true *) destruct Himpl0 as [? | ->] ; first congruence. (* case analysis on turn *) @@ -429,94 +404,88 @@ Section proof. (* if turn = 1-tid: do nothing *) { (* perform atomic operation *) - wp_read as "_". + wp_load. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ Post". + iModIntro. iSplitR "Hs0◯ Post". { repeat (iExists _). iFrame. repeat iSplit ; by auto with lia. } (* conclude *) - iApply "Post". iFrame "HV0◯". iLeft. by iFrame. + iApply "Post". iLeft. by iFrame. } (* if turn = tid: get resource R and enter critical section *) { (* deduce that s1 = Waiting and Vt = V1 *) destruct (decide _) as [_|?] ; last done. - destruct Ht as [-> ->] ; first done. + specialize (Ht eq_refl). (* update the ghost state *) auth_update "Hs0●" "Hs0◯" InCriticalSection. (* perform atomic operation *) - wp_read. + wp_load. (* close invariant *) - iModIntro. iSplitR "Hs0◯ HV0◯ HR Post". + iModIntro. iSplitR "Hs0◯ HR Post". { repeat (iExists _). iFrame. repeat iSplit ; auto with lia. - by case_match. - by iIntros ([? _]). } (* conclude *) - iApply "Post". iFrame "HV0◯". iRight. iSplit ; first done. - iFrame "Hs0◯". (* get R: *) iExists V1. iFrame "#". by iApply "HR". + iApply "Post". iRight. iSplit ; first done. + iFrame "Hs0◯". (* get R: *) by iApply "HR"; simplify_eq. } Qed. - Lemma release_spec (lk : val) (γ0 : peterson_gnames) (R : vProp Σ) : + Lemma release_spec (lk : val) (γ0 : peterson_gnames) (R : iProp Σ) : {{{ locked lk γ0 R ∗ R }}} release lk {{{ RET #() ; is_peterson lk γ0 R }}}. Proof. iIntros (Φ) "[Hlocked HR] Post". - iDestruct "Hlocked" as (??????) "(-> & #? & Hs0◯ & HV0◯)". + iDestruct "Hlocked" as (?????) "(-> & #HI & Hs0◯)". wp_lam. wp_pures. - (* unpack R *) - iDestruct (monPred_in_intro with "HR") as (V0') "[#? HR]". (* (1) write false to my_flag *) - wp_apply (write_my_flag_false with "[$]") ; iIntros "(Hs0◯ & HV0◯)". + wp_apply (write_my_flag_false with "[$Hs0◯ $HI $HR]"); iIntros "Hs0◯". (* conclude *) iApply "Post". repeat (iExists _). by iFrame "# ∗". Qed. - Lemma acquire_spec (lk : val) (γ0 : peterson_gnames) (R : vProp Σ) : + Lemma acquire_spec (lk : val) (γ0 : peterson_gnames) (R : iProp Σ) : {{{ is_peterson lk γ0 R }}} acquire lk {{{ RET #() ; locked lk γ0 R ∗ R }}}. Proof. iIntros (Φ) "Hlk Post". - iDestruct "Hlk" as (γ1 turn flag0 flag1 tid V0) "(-> & #? & Hs0◯ & HV0◯ & #?)". + iDestruct "Hlk" as (γ1 turn flag0 flag1 tid) "(-> & #HI & Hs0◯)". wp_lam. wp_pures. (* (1) write true to my_flag *) - wp_apply (write_my_flag_true with "[$]") ; iIntros "[Hs0◯ HV0◯]". + wp_apply (write_my_flag_true with "[$HI $Hs0◯]"); iIntros "Hs0◯". wp_pures. (* (2) write to turn *) - wp_apply (write_turn with "[$]") ; iIntros "[Hs0◯ HV0◯]". - wp_seq. wp_closure. + wp_apply (write_turn with "[$HI $Hs0◯]"); iIntros "Hs0◯". + wp_seq. (* start the waiting loop *) iLöb as "IH_loop". - wp_pures. + wp_rec. wp_pures. (* (3) read from other_flag *) - wp_apply (read_other_flag with "[$]") ; iIntros ([]) "(HV0◯ & Hread)" ; + wp_apply (read_other_flag with "[$]") ; iIntros ([]) "Hread"; [ iRename "Hread" into "Hs0◯" | iDestruct "Hread" as "(Hs0◯ & HR)" ]. (* case of (3): if other_flag = true: continue the loop *) { wp_pures. (* (4) read from turn *) - wp_apply (read_turn with "[$]") ; iIntros (t) "(HV0◯ & [(-> & Hs0◯) | (-> & Hs0◯ & HR)])". + wp_apply (read_turn with "[$]") ; iIntros (t) "[(-> & Hs0◯) | (-> & Hs0◯ & HR)]". (* case of (4): if turn = 1-tid: loop again *) { - wp_op. rewrite bool_decide_eq_true_2 ; last done. wp_if. wp_seq. - by iApply ("IH_loop" with "[$] [$] [$]"). + wp_op. rewrite bool_decide_eq_true_2 ; last done. wp_if. + by iApply ("IH_loop" with "[$] [$]"). } (* case of (4): if turn = tid: get resource R and enter critical section *) { iClear "IH_loop". - wp_op. rewrite bool_decide_eq_false_2 ; last lia. wp_if. + wp_op. rewrite bool_decide_eq_false_2 ; last by inversion 1; lia. wp_if. iApply "Post". iSplitR "HR". (* forge the “locked” token *) - { repeat (iExists _). iFrame. by iSplit. } + { repeat (iExists _). by iFrame "#∗". } (* pack R *) - { - iDestruct "HR" as (V1) "[#? ?]". - iApply monPred_in_elim ; last done. - solve_monPred_in. - } + { done. } } } (* case of (3): if other_flag = false: get resource R and enter critical section *) @@ -524,13 +493,9 @@ Section proof. iClear "IH_loop". wp_pures. iApply "Post". iSplitR "HR". (* forge the “locked” token *) - { repeat (iExists _). iFrame. by iSplit. } + { repeat (iExists _). by iFrame "#∗". } (* pack R *) - { - iDestruct "HR" as (V1) "[#? ?]". - iApply monPred_in_elim ; last done. - solve_monPred_in. - } + { done. } } Qed. @@ -545,7 +510,7 @@ Section proof. Theorem combined_spec P : {{{ P }}} make #() - {{{ lk0 lk1 (unlocked locked : val → vProp Σ), RET (lk0, lk1) ; + {{{ lk0 lk1 (unlocked locked : val → iProp Σ), RET (lk0, lk1) ; unlocked lk0 ∗ unlocked lk1 ∗ ∀ lk, {{{ unlocked lk }}} acquire lk {{{ RET #() ; locked lk ∗ P }}} @@ -562,14 +527,14 @@ Section proof. else if decide (v = lk1) then is_peterson lk1 γ1 P else False%I - : vProp Σ). + : iProp Σ). pose (locked' := λ (v : val), if decide (v = lk0) then locked lk0 γ0 P else if decide (v = lk1) then locked lk1 γ1 P else False%I - : vProp Σ). + : iProp Σ). assert (unlocked' lk0 = is_peterson lk0 γ0 P) as Eunlocked0. { rewrite /unlocked'. by case_match. } assert (unlocked' lk1 = is_peterson lk1 γ1 P) as Eunlocked1.