linux/tools/memory-model/linux-kernel.bell
<<
>>
Prefs
   1// SPDX-License-Identifier: GPL-2.0+
   2(*
   3 * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
   4 * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
   5 * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
   6 *                    Andrea Parri <parri.andrea@gmail.com>
   7 *
   8 * An earlier version of this file appeared in the companion webpage for
   9 * "Frightening small children and disconcerting grown-ups: Concurrency
  10 * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
  11 * which appeared in ASPLOS 2018.
  12 *)
  13
  14"Linux-kernel memory consistency model"
  15
  16enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
  17                'release (*smp_store_release*) ||
  18                'acquire (*smp_load_acquire*) ||
  19                'noreturn (* R of non-return RMW *)
  20instructions R[{'once,'acquire,'noreturn}]
  21instructions W[{'once,'release}]
  22instructions RMW[{'once,'acquire,'release}]
  23
  24enum Barriers = 'wmb (*smp_wmb*) ||
  25                'rmb (*smp_rmb*) ||
  26                'mb (*smp_mb*) ||
  27                'barrier (*barrier*) ||
  28                'rcu-lock (*rcu_read_lock*)  ||
  29                'rcu-unlock (*rcu_read_unlock*) ||
  30                'sync-rcu (*synchronize_rcu*) ||
  31                'before-atomic (*smp_mb__before_atomic*) ||
  32                'after-atomic (*smp_mb__after_atomic*) ||
  33                'after-spinlock (*smp_mb__after_spinlock*) ||
  34                'after-unlock-lock (*smp_mb__after_unlock_lock*)
  35instructions F[Barriers]
  36
  37(* SRCU *)
  38enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
  39instructions SRCU[SRCU]
  40(* All srcu events *)
  41let Srcu = Srcu-lock | Srcu-unlock | Sync-srcu
  42
  43(* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
  44let rcu-rscs = let rec
  45            unmatched-locks = Rcu-lock \ domain(matched)
  46        and unmatched-unlocks = Rcu-unlock \ range(matched)
  47        and unmatched = unmatched-locks | unmatched-unlocks
  48        and unmatched-po = [unmatched] ; po ; [unmatched]
  49        and unmatched-locks-to-unlocks =
  50                [unmatched-locks] ; po ; [unmatched-unlocks]
  51        and matched = matched | (unmatched-locks-to-unlocks \
  52                (unmatched-po ; unmatched-po))
  53        in matched
  54
  55(* Validate nesting *)
  56flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking
  57flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking
  58
  59(* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
  60let srcu-rscs = let rec
  61            unmatched-locks = Srcu-lock \ domain(matched)
  62        and unmatched-unlocks = Srcu-unlock \ range(matched)
  63        and unmatched = unmatched-locks | unmatched-unlocks
  64        and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc
  65        and unmatched-locks-to-unlocks =
  66                ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc
  67        and matched = matched | (unmatched-locks-to-unlocks \
  68                (unmatched-po ; unmatched-po))
  69        in matched
  70
  71(* Validate nesting *)
  72flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking
  73flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
  74
  75(* Check for use of synchronize_srcu() inside an RCU critical section *)
  76flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
  77
  78(* Validate SRCU dynamic match *)
  79flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
  80
  81(* Compute marked and plain memory accesses *)
  82let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
  83                LKR | LKW | UL | LF | RL | RU
  84let Plain = M \ Marked
  85