From 52d636bc162dd6d2c6b7b4e097a2b0a449e5c63b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Apr 2025 10:18:52 +0200
Subject: [PATCH] rdcss: comment
---
theories/logatom/rdcss/rdcss.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index f95a0c43..6c757cda 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -80,7 +80,8 @@ Definition complete : val :=
let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("data") in
- (* Create a thread identifier using NewProph. *)
+ (* Create a thread identifier using NewProph.
+ We don't actually need a prophecy ID here, just some unique identifier. *)
let: "tid_ghost" := NewProph in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost";;
--
GitLab