diff options
| -rw-r--r-- | tools/memory-model/lock.cat | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index df74de2148f6..7217cd4941a4 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -32,6 +32,17 @@ include "cross.cat" * LKW, LF, RL, and RU have no ordering properties. *) +(* Backward compatibility *) +let RL = try RL with emptyset +let RU = try RU with emptyset + +(* Treat RL as a kind of LF: a read with no ordering properties *) +let LF = LF | RL + +(* There should be no ordinary R or W accesses to spinlocks *) +let ALL-LOCKS = LKR | LKW | UL | LF | RU +flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses + (* Link Lock-Reads to their RMW-partner Lock-Writes *) let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) let rmw = rmw | lk-rmw @@ -49,20 +60,9 @@ flag ~empty LKW \ range(lk-rmw) as unpaired-LKW (* This will be allowed if we implement spin_is_locked() *) flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR -(* There should be no ordinary R or W accesses to spinlocks *) -let ALL-LOCKS = LKR | LKW | UL | LF -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses - (* The final value of a spinlock should not be tested *) flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final -(* Backward compatibility *) -let RL = try RL with emptyset -let RU = try RU with emptyset - -(* Treat RL as a kind of LF: a read with no ordering properties *) -let LF = LF | RL - (* * Put lock operations in their appropriate classes, but leave UL out of W * until after the co relation has been generated. |