diff --git a/_CoqProject b/_CoqProject
index dc79c329b959f2b82a2f6d24ed24584928450c7c..799b53c4984cc7098ab25115582e8f828994754c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,6 +37,7 @@ theories/bi/fixpoint.v
 theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/lib/fractional.v
+theories/bi/lib/atomic.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
@@ -72,6 +73,7 @@ theories/program_logic/ectx_lifting.v
 theories/program_logic/ownp.v
 theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
+theories/program_logic/atomic.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
new file mode 100644
index 0000000000000000000000000000000000000000..4ae20945f679f725bdaed5d70efafa78d4ae8411
--- /dev/null
+++ b/theories/bi/lib/atomic.v
@@ -0,0 +1,14 @@
+From iris.bi Require Export bi updates.
+From stdpp Require Import coPset.
+From iris.proofmode Require Import classes class_instances.
+Set Default Proof Using "Type".
+
+Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
+  (α: A → PROP) (* atomic pre-condition *)
+  (β: A → B → PROP) (* atomic post-condition *)
+  (Ei Eo: coPset) (* inside/outside masks *)
+  (Q: A → B → PROP) (* post-condition *)
+  : PROP :=
+    (∃ (F P:PROP), F ∗ ▷ P ∗ □ (▷ P ={Eo, Ei}=∗ ∃ x, α x ∗
+          ((α x ={Ei, Eo}=∗ ▷ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ F -∗ Q x y)))
+    )%I.
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
new file mode 100644
index 0000000000000000000000000000000000000000..2ee18897893e96da311372d3665d76403ac87ddf
--- /dev/null
+++ b/theories/program_logic/atomic.v
@@ -0,0 +1,14 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics classes.
+From iris.bi.lib Require Import atomic.
+Set Default Proof Using "Type".
+
+Definition atomic_wp `{irisG Λ Σ} {A B : Type}
+  (e: expr Λ) (* expression *)
+  (α: A → iProp Σ) (* atomic pre-condition *)
+  (β: A → B → iProp Σ) (* atomic post-condition *)
+  (Ei Eo: coPset) (* inside/outside masks *)
+  (f: A → B → val Λ) (* Turn the return data into the return value *)
+  : iProp Σ :=
+    (∀ Φ, atomic_shift α β Ei Eo (λ x y, Φ (f x y)) -∗
+          WP e {{ Φ }})%I.