From bfd93cbad7d453f22be63f7c17f69dd842d29a5f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 29 Oct 2017 14:13:34 +0100
Subject: [PATCH] comment a little more on CAS being atomic, but not strongly
 atomic

---
 theories/lang/lang.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index b83234e0..a04889cb 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -317,6 +317,9 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
    state being stuck like we could in a language where failing and succeeding
    CAS are mutually exclusive.
 
+   This means that CAS is atomic (it always reducs to an irreducible
+   expression), but not strongly atomic (it does not always reduce to a value).
+
    If there is a concurrent non-atomic write, the CAS itself is stuck: All it's
    reductions are blocked.  *)
 | CasStuckS l n e1 lit1 e2 lit2 litl σ :
-- 
GitLab