From 9cbc4c7f765e3e1da281cba0e6f5698eb2eb5de6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Jul 2019 17:03:09 +0200
Subject: [PATCH] few atomic snapshot comments
---
theories/logatom/snapshot/atomic_snapshot.v | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index d7364c69..0e461f31 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -9,7 +9,7 @@ From iris_examples.logatom.snapshot Require Import spec.
Set Default Proof Using "Type".
(** Specifying snapshots with histories
- Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
+ Inspired by atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
(*
@@ -25,6 +25,9 @@ Definition new_snapshot : val :=
let xp1 = !xp in
let v = (!xp1).2
let xp2 = ref (x, v + 1)
+ // This is where we need the nested references: the CAS compares the old
+ // inner reference with the new one, because it cannot atomically compared
+ // a pair of values.
if CAS xp xp1 xp2
then ()
else writeX (xp, yp) x
--
GitLab