From de86652f87c99266eb49bd1f105f369e26c3316f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 29 Jun 2018 23:16:46 +0200 Subject: [PATCH] allow comparing more things in CAS See the comments in the code for why that makes sense --- theories/heap_lang/lang.v | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v index 55444e52f..4a98fbbe8 100644 --- a/theories/heap_lang/lang.v +++ b/theories/heap_lang/lang.v @@ -370,13 +370,16 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := (** Return whether it is possible to use CAS to compare vl (current value) with v1 (netest value). *) Definition vals_cas_compare_safe (vl v1 : val) : Prop := match vl, v1 with + (* We allow comparing literals with each other. *) | LitV _, LitV _ => True - (* We want to support CAS'ing [NONEV] to [SOMEV #l]. An implementation of - this is possible if literals have an invalid bit pattern that can be used to - represent NONE. *) + (* We assume that [NONEV] is represented as a NULL-pointer and [SOMEV x] as a + pointer to a location (never written to after allocation) storing [x]. Then + comparing [NONEV] with [NONEV] or [SOMEV x] is possible atomically by testing + for NULL. Comparing [SOMEV x] with [SOMEV y] is not possible though. *) | NONEV, NONEV => True - | NONEV, SOMEV (LitV _) => True - | SOMEV (LitV _), NONEV => True + | NONEV, SOMEV _ => True + | SOMEV _, NONEV => True + (* We don't allow comparing anything else. *) | _, _ => False end. (** Just a sanity check. *) -- GitLab