Support typed atomic load and store

mit-pdos · Feb 12, 2025 · e98c778 · e98c778
1 parent ec2036b
commit e98c778
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 12 deletions.
diff --git a/new/golang/theory/mem.v b/new/golang/theory/mem.v
@@ -499,6 +499,47 @@ Section goose_lang.
       iIntros; iApply "HΦ"; iFrame; done.
   Qed.
 
+  Lemma wp_typed_Load (l : loc) (v : V) dq :
+    is_primitive_type t →
+    {{{ l ↦{dq} v }}}
+      ! #l
+    {{{ RET #v; l ↦{dq} v }}}.
+  Proof using Type*.
+    intros Hprim.
+    pose proof (to_val_has_go_type v) as Hty.
+    unseal.
+    generalize dependent (#v).
+    clear dependent V.
+    intros.
+    iIntros "Hl HΦ".
+    destruct t; try by exfalso.
+    all: inversion Hty; subst;
+      inversion Hty; subst;
+      simpl; rewrite to_val_unseal /= loc_add_0 !right_id;
+      iApply (wp_load with "[$Hl]"); iFrame.
+  Qed.
+
+  Lemma wp_typed_AtomicStore (l : loc) (v v' : V) :
+    is_primitive_type t →
+    {{{ l ↦ v }}}
+      AtomicStore #l #v'
+    {{{ RET #(); l ↦ v' }}}.
+  Proof using Type*.
+    intros Hprim.
+    pose proof (to_val_has_go_type v) as Hty_old.
+    pose proof (to_val_has_go_type v') as Hty.
+    unseal.
+    generalize dependent (#v). generalize dependent (#v').
+    clear dependent V.
+    intros.
+    iIntros "Hl HΦ".
+    destruct t; try by exfalso.
+    all: inversion Hty; subst;
+      inversion Hty_old; inversion Hty; subst;
+      simpl; rewrite to_val_unseal /= loc_add_0 !right_id;
+      iApply (wp_atomic_store with "[$Hl]"); iFrame.
+  Qed.
+
 End goose_lang.
 
 Notation "l ↦ dq v" := (typed_pointsto l dq v%V)

diff --git a/new/proof/sync/atomic.v b/new/proof/sync/atomic.v
@@ -20,11 +20,7 @@ Proof.
   iIntros (?) "#? HΦ".
   wp_func_call. wp_call.
   iMod "HΦ" as (?) "[Haddr HΦ]".
-  rewrite to_val_unseal.
-  iApply (wp_load with "[Haddr]").
-  { rewrite typed_pointsto_unseal /typed_pointsto_def to_val_unseal /= right_id loc_add_0 //. }
-  iNext. iIntros "H". iApply "HΦ".
-  rewrite typed_pointsto_unseal /typed_pointsto_def to_val_unseal /= right_id loc_add_0 //.
+  unshelve iApply (wp_typed_Load with "[$]"); try tc_solve; done.
 Qed.
 
 Lemma wp_StoreUint64 (addr : loc) (v : w64) :
@@ -36,11 +32,7 @@ Proof.
   iIntros (?) "#? HΦ".
   wp_func_call. wp_call.
   iMod "HΦ" as (?) "[Haddr HΦ]".
-  rewrite to_val_unseal.
-  iApply (wp_atomic_store with "[Haddr]").
-  { rewrite typed_pointsto_unseal /typed_pointsto_def to_val_unseal /= right_id loc_add_0 //. }
-  iNext. iIntros "H". iApply "HΦ".
-  rewrite typed_pointsto_unseal /typed_pointsto_def to_val_unseal /= right_id loc_add_0 //.
+  unshelve iApply (wp_typed_AtomicStore with "[$]"); try tc_solve; done.
 Qed.
 
 Lemma wp_AddUint64 (addr : loc) (v : w64) :
@@ -52,8 +44,7 @@ Proof.
 Admitted.
 
 Definition own_Uint64 (u : loc) dq (v : w64) : iProp Σ :=
-  u ↦{dq} atomic.Uint64.mk (default_val _) (default_val _) v
-.
+  u ↦{dq} atomic.Uint64.mk (default_val _) (default_val _) v.
 
 Lemma wp_Uint64__Load u dq :
   ∀ Φ,