diff options
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell new file mode 100644 index 000000000000..57112505f5e0 --- /dev/null +++ b/tools/memory-model/linux-kernel.bell @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: GPL-2.0+ +(* + * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>, + * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria + * 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 + * "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. + *) + +"Linux kernel memory model" + +enum Accesses = 'once (*READ_ONCE,WRITE_ONCE,ACCESS_ONCE*) || + 'release (*smp_store_release*) || + 'acquire (*smp_load_acquire*) || + 'noreturn (* R of non-return RMW *) +instructions R[{'once,'acquire,'noreturn}] +instructions W[{'once,'release}] +instructions RMW[{'once,'acquire,'release}] + +enum Barriers = 'wmb (*smp_wmb*) || + 'rmb (*smp_rmb*) || + 'mb (*smp_mb*) || + 'rb_dep (*smp_read_barrier_depends*) || + 'rcu-lock (*rcu_read_lock*) || + 'rcu-unlock (*rcu_read_unlock*) || + 'sync-rcu (*synchronize_rcu*) || + 'before_atomic (*smp_mb__before_atomic*) || + 'after_atomic (*smp_mb__after_atomic*) || + 'after_spinlock (*smp_mb__after_spinlock*) +instructions F[Barriers] + +(* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) +let matched = let rec + unmatched-locks = Rcu-lock \ domain(matched) + and unmatched-unlocks = Rcu-unlock \ range(matched) + and unmatched = unmatched-locks | unmatched-unlocks + and unmatched-po = [unmatched] ; po ; [unmatched] + and unmatched-locks-to-unlocks = + [unmatched-locks] ; po ; [unmatched-unlocks] + and matched = matched | (unmatched-locks-to-unlocks \ + (unmatched-po ; unmatched-po)) + in matched + +(* Validate nesting *) +flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking +flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking + +(* Outermost level of nesting only *) +let crit = matched \ (po^-1 ; matched ; po^-1) |