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 appears 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 is to appear in ASPLOS 2018.
 12 *)
 13
 14"Linux-kernel memory consistency model"
 15
 16(*
 17 * File "lock.cat" handles locks and is experimental.
 18 * It can be replaced by include "cos.cat" for tests that do not use locks.
 19 *)
 20
 21include "lock.cat"
 22
 23(*******************)
 24(* Basic relations *)
 25(*******************)
 26
 27(* Fences *)
 28let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
 29let wmb = [W] ; fencerel(Wmb) ; [W]
 30let mb = ([M] ; fencerel(Mb) ; [M]) |
 31	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
 32	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
 33	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
 34let gp = po ; [Sync-rcu] ; po?
 35
 36let strong-fence = mb | gp
 37
 38(* Release Acquire *)
 39let acq-po = [Acquire] ; po ; [M]
 40let po-rel = [M] ; po ; [Release]
 41let rfi-rel-acq = [Release] ; rfi ; [Acquire]
 42
 43(**********************************)
 44(* Fundamental coherence ordering *)
 45(**********************************)
 46
 47(* Sequential Consistency Per Variable *)
 48let com = rf | co | fr
 49acyclic po-loc | com as coherence
 50
 51(* Atomic Read-Modify-Write *)
 52empty rmw & (fre ; coe) as atomic
 53
 54(**********************************)
 55(* Instruction execution ordering *)
 56(**********************************)
 57
 58(* Preserved Program Order *)
 59let dep = addr | data
 60let rwdep = (dep | ctrl) ; [W]
 61let overwrite = co | fr
 62let to-w = rwdep | (overwrite & int)
 63let to-r = addr | (dep ; rfi) | rfi-rel-acq
 64let fence = strong-fence | wmb | po-rel | rmb | acq-po
 65let ppo = to-r | to-w | fence
 66
 67(* Propagation: Ordering from release operations and strong fences. *)
 68let A-cumul(r) = rfe? ; r
 69let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
 70let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
 71
 72(*
 73 * Happens Before: Ordering from the passage of time.
 74 * No fences needed here for prop because relation confined to one process.
 75 *)
 76let hb = ppo | rfe | ((prop \ id) & int)
 77acyclic hb as happens-before
 78
 79(****************************************)
 80(* Write and fence propagation ordering *)
 81(****************************************)
 82
 83(* Propagation: Each non-rf link needs a strong fence. *)
 84let pb = prop ; strong-fence ; hb*
 85acyclic pb as propagation
 86
 87(*******)
 88(* RCU *)
 89(*******)
 90
 91(*
 92 * Effect of read-side critical section proceeds from the rcu_read_lock()
 93 * onward on the one hand and from the rcu_read_unlock() backwards on the
 94 * other hand.
 95 *)
 96let rscs = po ; crit^-1 ; po?
 97
 98(*
 99 * The synchronize_rcu() strong fence is special in that it can order not
100 * one but two non-rf relations, but only in conjunction with an RCU
101 * read-side critical section.
102 *)
103let link = hb* ; pb* ; prop
104
105(* Chains that affect the RCU grace-period guarantee *)
106let gp-link = gp ; link
107let rscs-link = rscs ; link
108
109(*
110 * A cycle containing at least as many grace periods as RCU read-side
111 * critical sections is forbidden.
112 *)
113let rec rcu-path =
114	gp-link |
115	(gp-link ; rscs-link) |
116	(rscs-link ; gp-link) |
117	(rcu-path ; rcu-path) |
118	(gp-link ; rcu-path ; rscs-link) |
119	(rscs-link ; rcu-path ; gp-link)
120
121irreflexive rcu-path as rcu