diff options
Diffstat (limited to 'tools/memory-model/linux-kernel.cat')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index df97db03b6c2..cdf682859d4e 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -100,22 +100,22 @@ let rscs = po ; crit^-1 ; po? * one but two non-rf relations, but only in conjunction with an RCU * read-side critical section. *) -let link = hb* ; pb* ; prop +let rcu-link = hb* ; pb* ; prop (* Chains that affect the RCU grace-period guarantee *) -let gp-link = gp ; link -let rscs-link = rscs ; link +let gp-link = gp ; rcu-link +let rscs-link = rscs ; rcu-link (* * A cycle containing at least as many grace periods as RCU read-side * critical sections is forbidden. *) -let rec rcu-path = +let rec rb = gp-link | (gp-link ; rscs-link) | (rscs-link ; gp-link) | - (rcu-path ; rcu-path) | - (gp-link ; rcu-path ; rscs-link) | - (rscs-link ; rcu-path ; gp-link) + (rb ; rb) | + (gp-link ; rb ; rscs-link) | + (rscs-link ; rb ; gp-link) -irreflexive rcu-path as rcu +irreflexive rb as rcu |