Add model and specs for atomic library

external/Goose/github_com/goose_lang/goose/internal/examples/semantics.v

@@ -119,6 +119,17 @@ Definition testAtomicLoadStore64: val :=
     "ok" <-[boolT] ((![boolT] "ok") && ("z" = #1));;
     ![boolT] "ok".
 
+Definition testAtomicPointers: val :=
+  rec: "testAtomicPointers" <> :=
+    let: "p" := ref (zero_val ptrT) in
+    let: "x" := ref (zero_val uint64T) in
+    atomic.Pointer__Store uint64T "p" "x";;
+    let: "y" := atomic.Pointer__Load uint64T "p" in
+    "y" <-[uint64T] #1;;
+    let: "ok" := ref_to boolT #true in
+    "ok" <-[boolT] ((![boolT] "ok") && ((![uint64T] "x") = #1));;
+    ![boolT] "ok".
+
 (* closures.go *)
 
 Notation AdderType := (uint64T -> uint64T)%ht (only parsing).

src/ShouldBuild.v

@@ -71,6 +71,9 @@ From Perennial.tutorial Require
 (* WIP slice library *)
 From Perennial.goose_lang.lib Require
      slice.pred_slice.
+(* sync/atomic library (not yet used) *)
+From Perennial.goose_lang.lib Require
+     atomic.atomic.
 
 (* WIP Z-based list library *)
 From Perennial.Helpers Require ListZ.

src/goose_lang/interpreter/generated_test.v

@@ -21,6 +21,7 @@ Example testAssignBitwise_ok : testAssignBitwise #() ~~> #true := t.
 
 (* atomic.go *)
 Example testAtomicLoadStore64_ok : testAtomicLoadStore64 #() ~~> #true := t.
+Example testAtomicPointers_ok : testAtomicPointers #() ~~> #true := t.
 
 (* closures.go *)
 Example testClosureBasic_ok : testClosureBasic #() ~~> #true := t.

src/goose_lang/lib/atomic/atomic.v

@@ -23,23 +23,39 @@ Context `{!heapGS Σ} (N : namespace).
 Proof.
   rewrite struct_pointsto_eq /struct_pointsto_def /=.
   rewrite loc_add_0 right_id.
-  iSplit.
-  - iIntros "[$ _]".
-  - iIntros "$".
-    iPureIntro. val_ty.
+  iSplit; [ iIntros "[$ _]" | iIntros "$" ].
+  iPureIntro. val_ty.
 Qed.
 
 #[local] Lemma uint32_pointsto (l: loc) (x: w32) :
   l ↦[uint32T] #x ⊣⊢ heap_pointsto l (DfracOwn 1) #x.
 Proof.
   rewrite struct_pointsto_eq /struct_pointsto_def /=.
   rewrite loc_add_0 right_id.
-  iSplit.
-  - iIntros "[$ _]".
-  - iIntros "$".
-    iPureIntro. val_ty.
+  iSplit; [ iIntros "[$ _]" | iIntros "$" ].
+  iPureIntro. val_ty.
 Qed.
 
+#[local] Lemma loc_pointsto (l: loc) (x: loc) q :
+  l ↦[ptrT]{q} #x ⊣⊢ heap_pointsto l q #x.
+Proof.
+  rewrite struct_pointsto_eq /struct_pointsto_def /=.
+  rewrite loc_add_0 right_id.
+  iSplit; [ iIntros "[$ _]" | iIntros "$" ].
+  iPureIntro. val_ty.
+Qed.
+
+#[global] Instance LoadUint64_Atomic (l:loc) : Atomic StronglyAtomic (atomic.LoadUint64 #l).
+Proof. apply _. Qed.
+#[global] Instance StoreUint64_Atomic (l:loc) (v: base_lit) : Atomic StronglyAtomic (atomic.StoreUint64 #l #v).
+Proof. apply _. Qed.
+#[global] Instance CompareAndSwap64_Atomic (l:loc) (v1 v2: base_lit) : Atomic StronglyAtomic (atomic.CompareAndSwapUint64 #l #v1 #v2).
+Proof. apply _. Qed.
+#[global] Instance Pointer__Load_Atomic t (l:loc) : Atomic StronglyAtomic (atomic.Pointer__Load t #l).
+Proof. apply _. Qed.
+#[global] Instance Pointer__Store_Atomic t (l:loc) (v: base_lit) : Atomic StronglyAtomic (atomic.Pointer__Store t #l #v).
+Proof. apply _. Qed.
+
 Lemma wp_LoadUint64 (l: loc) (x: w64) stk E :
   {{{ ▷l ↦[uint64T] #x }}}
     atomic.LoadUint64 #l @ stk; E
@@ -92,5 +108,32 @@ Proof.
   iApply "HΦ". iFrame.
 Qed.
 
+Lemma wp_Pointer__Load (l: loc) (l_v: loc) q stk E :
+  {{{ ▷l ↦[ptrT]{q} #l_v }}}
+    atomic.Pointer__Load ptrT #l @ stk; E
+  {{{ RET #l_v; l ↦[ptrT]{q} #l_v }}}.
+Proof.
+  iIntros (Φ) "Hl HΦ".
+  setoid_rewrite loc_pointsto.
+  rewrite /atomic.Pointer__Load.
+  wp_pures.
+  wp_apply (wp_load with "[$Hl]"). iIntros "Hl".
+  iApply "HΦ". iFrame.
+Qed.
+
+Lemma wp_Pointer__Store (l: loc) (l_v0 l_v': loc) stk E :
+  {{{ ▷l ↦[ptrT] #l_v0 }}}
+    atomic.Pointer__Store ptrT #l #l_v' @ stk; E
+  {{{ RET #(); l ↦[ptrT] #l_v' }}}.
+Proof.
+  iIntros (Φ) "Hl HΦ".
+  setoid_rewrite loc_pointsto.
+  rewrite /atomic.Pointer__Store.
+  wp_pures.
+  wp_apply (wp_atomic_store with "[$Hl]"). iIntros "Hl".
+  iApply "HΦ". iFrame.
+Qed.
+
+
 End proof.
 End goose_lang.

src/goose_lang/lib/atomic/impl.v

@@ -1,24 +1,25 @@
-From Perennial.goose_lang Require Import notation.
+From Perennial.goose_lang Require Import notation typing typed_mem.impl.
 
 (* this code is intended to be used qualified with the atomic module *)
 Module atomic.
 Section goose_lang.
-Context {ext:ffi_syntax}.
-
-Definition LoadUint64 : val :=
-  λ: "l", Load "l".
-
-Definition LoadUint32 : val := LoadUint64.
-
-Definition StoreUint64 : val :=
-  λ: "l" "x", AtomicStore "l" "x".
-
-Definition StoreUint32 : val := StoreUint64.
-
-Definition CompareAndSwapUint64 : val :=
-  λ: "l" "old" "new", CmpXchg "l" "old" "new".
-
-Definition CompareAndSwapUint32 : val := CompareAndSwapUint64.
+Context {ext:ffi_syntax} {ext_ty: ext_types ext}.
+
+(* these are not values so that they are Atomic *)
+
+Definition LoadUint64 : expr → expr := Load.
+Definition LoadUint32 : expr → expr := LoadUint64.
+Definition StoreUint64 : expr → expr → expr := AtomicStore.
+Definition StoreUint32 : expr → expr → expr := StoreUint64.
+Definition CompareAndSwapUint64 : expr → expr → expr → expr := CmpXchg.
+Definition CompareAndSwapUint32 : expr → expr → expr → expr := CompareAndSwapUint64.
+
+(* the type arguments to these functions are passed since that's the GooseLang
+calling convention. They are not needed in the model, since these operations
+only load pointers, and we don't need to know what the shape of the referenced
+data is to write the model. *)
+Definition Pointer__Load (_: ty) : expr → expr := Load.
+Definition Pointer__Store (_: ty) : expr → expr → expr := AtomicStore.
 
 End goose_lang.
 End atomic.