thread-local invariants are now called non-atomic, and they handle their masks differently

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7fe0d2593e2751c35d7c3146e0e91ab2623a08a8
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 683b706631e7b85b76393dbbac9c01fe187a1613

theories/lifetime/tl_borrow.v

 From lrust.lifetime Require Export derived.
-From iris.base_logic.lib Require Export thread_local.
+From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 
-Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
+Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, &{κ,i}P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
+  (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
-  (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
+  (format "&na{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
 
-Section tl_bor.
-  Context `{invG Σ, lftG Σ, thread_localG Σ}
+Section na_bor.
+  Context `{invG Σ, lftG Σ, na_invG Σ}
           (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Global Instance tl_bor_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
-  Global Instance tl_bor_proper κ :
-    Proper ((⊣⊢) ==> (⊣⊢)) (tl_bor κ tid N).
+  Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
+  Global Instance na_bor_proper κ :
+    Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
   Proof.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma bor_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ,tid,N}P.
+  Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
   Proof.
     iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "[#? Hown]".
-    iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
+    iExists i. iFrame "#". iApply (na_inv_alloc tid E N with "[Hown]"). auto.
   Qed.
 
-  Lemma tl_bor_acc q κ E F :
-    ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
-    lft_ctx -∗ &tl{κ,tid,N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
-            ▷P ∗ tl_own tid (F ∖ ↑N) ∗
-            (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
+  Lemma na_bor_acc q κ E :
+    ↑lftN ⊆ E → ↑N ⊆ E →
+    lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid E ={E}=∗
+            ▷P ∗ na_own tid (E ∖ ↑N) ∗
+            (▷P -∗ na_own tid (E ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid E).
   Proof.
-    iIntros (???) "#LFT#HP Hκ Htlown".
+    iIntros (??) "#LFT#HP Hκ Hnaown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
+    iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
     iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
-    iIntros "{$HP $Htlown}!>HP Htlown".
+    iIntros "{$HP $Hnaown}!>HP Hnaown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_bor_shorten κ κ': κ ⊑ κ' -∗ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
+  Lemma na_bor_shorten κ κ': κ ⊑ κ' -∗ &na{κ',tid,N}P -∗ &na{κ,tid,N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
-End tl_bor.
+End na_bor.
 
-Typeclasses Opaque tl_bor.
+Typeclasses Opaque na_bor.

theories/typing/perm_incl.v

@@ -108,8 +108,8 @@ Section props.
     iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
-    iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]".
-    apply disjoint_union_l; solve_ndisj. done. iIntros "!>/=". eauto.
+    iMod (ty.(ty_share) _ lrustN with "LFT Hown Htok") as "[Hown $]"; [solve_ndisj|done|].
+    iIntros "!>/=". eauto.
   Qed.
 
   Lemma perm_split_own_prod2 ty1 ty2 (q1 q2 : Qp) ν :

theories/typing/type.v

 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Export thread_local.
+From iris.base_logic.lib Require Export na_invariants.
 From iris.program_logic Require Import hoare.
 From lrust.lang Require Export heap notation.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
@@ -8,11 +8,11 @@ From lrust.lifetime Require Import borrow frac_borrow reborrow.
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
   type_lftG :> lftG Σ;
-  type_thread_localG :> thread_localG Σ;
+  type_na_invG :> na_invG Σ;
   type_frac_borrowG Σ :> frac_borG Σ
 }.
 
-Definition mgmtE := ↑tlN ∪ ↑lftN.
+Definition mgmtE := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 
 (* [perm] is defined here instead of perm.v in order to define [cont] *)
@@ -48,8 +48,8 @@ Record type :=
     ty_shr_acc κ tid E F l q :
       ty_dup → mgmtE ∪ F ⊆ E →
       lft_ctx -∗ ty_shr κ tid F l -∗
-        q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
-           (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
+        q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
+           (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ na_own tid F)
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
@@ -314,7 +314,7 @@ Section types.
     iIntros "#LFT H[[Htok1 Htok2] Htl]". iDestruct "H" as (E1 E2) "(% & H1 & H2)".
     assert (F = E1 ∪ E2 ∪ F∖(E1 ∪ E2)) as ->.
     { rewrite -union_difference_L; set_solver. }
-    repeat setoid_rewrite tl_own_union; first last.
+    repeat setoid_rewrite na_own_union; first last.
     set_solver. set_solver. set_solver. set_solver.
     iDestruct "Htl" as "[[Htl1 Htl2] $]".
     iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]".
@@ -436,7 +436,7 @@ Section types.
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗
-          ∀ vl, ρ vl tid -∗ tl_own tid ⊤
+          ∀ vl, ρ vl tid -∗ na_own tid ⊤
                  -∗ WP f (map of_val vl) {{λ _, False}})%I;
        ty_shr κ tid N l := True%I |}.
   Next Obligation. done. Qed.
@@ -454,7 +454,7 @@ Section types.
   Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
     {| st_size := 1;
        st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ ∀ x vl,
-         {{ ρ x vl tid ∗ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
+         {{ ρ x vl tid ∗ na_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
     iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.

theories/typing/typing.v

@@ -12,14 +12,14 @@ Section typing.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
-    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e
-           {{ v, θ v tid ∗ tl_own tid ⊤ }}.
+    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e
+           {{ v, θ v tid ∗ na_own tid ⊤ }}.
 
   Definition typed_step_ty (ρ : perm) e ty :=
     typed_step ρ e (λ ν, ν ◁ ty)%P.
 
   Definition typed_program (ρ : perm) e :=
-    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e {{ _, False }}.
+    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e {{ _, False }}.
 
   Lemma typed_frame ρ e θ ξ:
     typed_step ρ e θ → typed_step (ρ ∗ ξ) e (λ ν, θ ν ∗ ξ)%P.
@@ -174,10 +174,10 @@ Section typing.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
-      lft_ctx -∗ ρ1 ν tid -∗ tl_own tid ⊤ -∗
+      lft_ctx -∗ ρ1 ν tid -∗ na_own tid ⊤ -∗
       (∀ (l:loc) vl q,
         (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗{q} vl ∗
-         |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
+         |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ na_own tid ⊤)))
        -∗ Φ #l)
       -∗ WP ν @ E {{ Φ }}.
 
@@ -241,7 +241,7 @@ Section typing.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     rewrite (union_difference_L (↑lrustN) ⊤); last done.
-    setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
+    setoid_rewrite ->na_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
     iMod (ty_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".