Orange Pi5 kernel

^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   1) // SPDX-License-Identifier: GPL-2.0+
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   2) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   3)  * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   4)  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   5)  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   6)  *                    Andrea Parri <parri.andrea@gmail.com>
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   7)  *
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   8)  * An earlier version of this file appeared in the companion webpage for
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300   9)  * "Frightening small children and disconcerting grown-ups: Concurrency
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  10)  * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  11)  * which appeared in ASPLOS 2018.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  12)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  13) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  14) "Linux-kernel memory consistency model"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  15) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  16) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  17)  * File "lock.cat" handles locks and is experimental.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  18)  * It can be replaced by include "cos.cat" for tests that do not use locks.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  19)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  20) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  21) include "lock.cat"
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  22) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  23) (*******************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  24) (* Basic relations *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  25) (*******************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  26) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  27) (* Release Acquire *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  28) let acq-po = [Acquire] ; po ; [M]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  29) let po-rel = [M] ; po ; [Release]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  30) let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  31) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  32) (* Fences *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  33) let R4rmb = R \ Noreturn	(* Reads for which rmb works *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  34) let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  35) let wmb = [W] ; fencerel(Wmb) ; [W]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  36) let mb = ([M] ; fencerel(Mb) ; [M]) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  37) 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  38) 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  39) 	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  40) 	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  41) 		fencerel(After-unlock-lock) ; [M])
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  42) let gp = po ; [Sync-rcu | Sync-srcu] ; po?
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  43) let strong-fence = mb | gp
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  44) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  45) let nonrw-fence = strong-fence | po-rel | acq-po
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  46) let fence = nonrw-fence | wmb | rmb
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  47) let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  48) 		Before-atomic | After-atomic | Acquire | Release |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  49) 		Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  50) 	(po ; [Release]) | ([Acquire] ; po)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  51) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  52) (**********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  53) (* Fundamental coherence ordering *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  54) (**********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  55) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  56) (* Sequential Consistency Per Variable *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  57) let com = rf | co | fr
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  58) acyclic po-loc | com as coherence
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  59) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  60) (* Atomic Read-Modify-Write *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  61) empty rmw & (fre ; coe) as atomic
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  62) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  63) (**********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  64) (* Instruction execution ordering *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  65) (**********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  66) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  67) (* Preserved Program Order *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  68) let dep = addr | data
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  69) let rwdep = (dep | ctrl) ; [W]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  70) let overwrite = co | fr
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  71) let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  72) let to-r = addr | (dep ; [Marked] ; rfi)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  73) let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  74) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  75) (* Propagation: Ordering from release operations and strong fences. *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  76) let A-cumul(r) = (rfe ; [Marked])? ; r
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  77) let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  78) 	po-unlock-rf-lock-po) ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  79) let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  80) 	[Marked] ; rfe? ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  81) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  82) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  83)  * Happens Before: Ordering from the passage of time.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  84)  * No fences needed here for prop because relation confined to one process.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  85)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  86) let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  87) acyclic hb as happens-before
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  88) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  89) (****************************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  90) (* Write and fence propagation ordering *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  91) (****************************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  92) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  93) (* Propagation: Each non-rf link needs a strong fence. *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  94) let pb = prop ; strong-fence ; hb* ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  95) acyclic pb as propagation
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  96) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  97) (*******)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  98) (* RCU *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300  99) (*******)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 100) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 101) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 102)  * Effects of read-side critical sections proceed from the rcu_read_unlock()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 103)  * or srcu_read_unlock() backwards on the one hand, and from the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 104)  * rcu_read_lock() or srcu_read_lock() forwards on the other hand.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 105)  *
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 106)  * In the definition of rcu-fence below, the po term at the left-hand side
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 107)  * of each disjunct and the po? term at the right-hand end have been factored
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 108)  * out.  They have been moved into the definitions of rcu-link and rb.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 109)  * This was necessary in order to apply the "& loc" tests correctly.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 110)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 111) let rcu-gp = [Sync-rcu]		(* Compare with gp *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 112) let srcu-gp = [Sync-srcu]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 113) let rcu-rscsi = rcu-rscs^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 114) let srcu-rscsi = srcu-rscs^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 115) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 116) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 117)  * The synchronize_rcu() strong fence is special in that it can order not
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 118)  * one but two non-rf relations, but only in conjunction with an RCU
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 119)  * read-side critical section.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 120)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 121) let rcu-link = po? ; hb* ; pb* ; prop ; po
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 122) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 123) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 124)  * Any sequence containing at least as many grace periods as RCU read-side
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 125)  * critical sections (joined by rcu-link) induces order like a generalized
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 126)  * inter-CPU strong fence.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 127)  * Likewise for SRCU grace periods and read-side critical sections, provided
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 128)  * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 129)  * struct srcu_struct location.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 130)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 131) let rec rcu-order = rcu-gp | srcu-gp |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 132) 	(rcu-gp ; rcu-link ; rcu-rscsi) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 133) 	((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 134) 	(rcu-rscsi ; rcu-link ; rcu-gp) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 135) 	((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 136) 	(rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 137) 	((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 138) 	(rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 139) 	((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 140) 	(rcu-order ; rcu-link ; rcu-order)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 141) let rcu-fence = po ; rcu-order ; po?
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 142) let fence = fence | rcu-fence
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 143) let strong-fence = strong-fence | rcu-fence
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 144) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 145) (* rb orders instructions just as pb does *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 146) let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 147) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 148) irreflexive rb as rcu
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 149) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 150) (*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 151)  * The happens-before, propagation, and rcu constraints are all
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 152)  * expressions of temporal ordering.  They could be replaced by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 153)  * a single constraint on an "executes-before" relation, xb:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 154)  *
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 155)  * let xb = hb | pb | rb
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 156)  * acyclic xb as executes-before
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 157)  *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 158) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 159) (*********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 160) (* Plain accesses and data races *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 161) (*********************************)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 162) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 163) (* Warn about plain writes and marked accesses in the same region *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 164) let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 165) 	([Marked] ; (po-loc \ barrier) ; [Plain & W])
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 166) flag ~empty mixed-accesses as mixed-accesses
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 167) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 168) (* Executes-before and visibility *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 169) let xbstar = (hb | pb | rb)*
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 170) let vis = cumul-fence* ; rfe? ; [Marked] ;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 171) 	((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 172) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 173) (* Boundaries for lifetimes of plain accesses *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 174) let w-pre-bounded = [Marked] ; (addr | fence)?
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 175) let r-pre-bounded = [Marked] ; (addr | nonrw-fence |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 176) 	([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))?
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 177) let w-post-bounded = fence? ; [Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 178) let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 179) 	[Marked]
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 180) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 181) (* Visibility and executes-before for plain accesses *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 182) let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 183) 	(w-post-bounded ; vis ; w-pre-bounded)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 184) let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 185) 	(w-post-bounded ; vis ; r-pre-bounded)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 186) let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 187) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 188) (* Potential races *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 189) let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain))
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 190) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 191) (* Coherence requirements for plain accesses *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 192) let wr-incoh = pre-race & rf & rw-xbstar^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 193) let rw-incoh = pre-race & fr & wr-vis^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 194) let ww-incoh = pre-race & co & ww-vis^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 195) empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 196) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 197) (* Actual races *)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 198) let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 199) let ww-race = (pre-race & co) \ ww-nonrace
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 200) let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 201) let rw-race = (pre-race & fr) \ rw-xbstar
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 202) 
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 203) flag ~empty (ww-race | wr-race | rw-race) as data-race