diff options
Diffstat (limited to 'tools/memory-model/linux-kernel.cat')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 41 |
1 files changed, 24 insertions, 17 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index df97db03b6c2..59b5cbe6b624 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -5,10 +5,10 @@ * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>, * Andrea Parri <parri.andrea@gmail.com> * - * An earlier version of this file appears in the companion webpage for + * An earlier version of this file appeared in the companion webpage for * "Frightening small children and disconcerting grown-ups: Concurrency * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, - * which is to appear in ASPLOS 2018. + * which appeared in ASPLOS 2018. *) "Linux-kernel memory consistency model" @@ -100,22 +100,29 @@ 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 +(* + * Any sequence containing at least as many grace periods as RCU read-side + * critical sections (joined by rcu-link) acts as a generalized strong fence. + *) +let rec rcu-fence = gp | + (gp ; rcu-link ; rscs) | + (rscs ; rcu-link ; gp) | + (gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) | + (rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) | + (rcu-fence ; rcu-link ; rcu-fence) + +(* rb orders instructions just as pb does *) +let rb = prop ; rcu-fence ; hb* ; pb* + +irreflexive rb as rcu (* - * A cycle containing at least as many grace periods as RCU read-side - * critical sections is forbidden. + * The happens-before, propagation, and rcu constraints are all + * expressions of temporal ordering. They could be replaced by + * a single constraint on an "executes-before" relation, xb: + * + * let xb = hb | pb | rb + * acyclic xb as executes-before *) -let rec rcu-path = - 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) - -irreflexive rcu-path as rcu |