memory-model/linux-kernel-hardware.cat at master · aparri/memory-model · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
// 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>
 *)

"Linux kernel hardware memory model"

(*
 * File "lock.cat" handles locks and is experimental.
 * It can be replaced by include "cos.cat" for tests that do not use locks.
 *)

include "lock.cat"

(*******************)
(* Basic relations *)
(*******************)

(* Fences *)
let rb-dep = [R] ; fencerel(Rb_dep) ; [R]
let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R]
let wmb = [W] ; fencerel(Wmb) ; [W]
let mb = ([M] ; fencerel(Mb) ; [M]) |
	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
let gp = po ; [Sync-rcu] ; po?

let strong-fence = mb | gp

(* Release Acquire *)
let acq-po = [Acquire] ; po ; [M]
let po-rel = [M] ; po ; [Release]
let rfi-rel-acq = [Release] ; rfi ; [Acquire]

(**********************************)
(* Fundamental coherence ordering *)
(**********************************)

(* Sequential Consistency Per Variable *)
let com = rf | co | fr
acyclic po-loc | com as coherence

(* Atomic Read-Modify-Write *)
empty rmw & (fre ; coe) as atomic

(**********************************)
(* Instruction execution ordering *)
(**********************************)

(* Preserved Program Order *)
let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let addrpo = addr ; po ; [W]
let overwrite = co | fr
let to-w = rwdep | addrpo | (overwrite & int)
let rdw = po-loc & (fre ; rfe)
let detour = po-loc & (coe ; rfe)
let rrdep = addr | (dep ; rfi) | rdw
let strong-rrdep = rrdep+ & rb-dep
let to-r = strong-rrdep | rfi-rel-acq
let fence = strong-fence | wmb | po-rel | rmb | acq-po
let ppo = (rrdep* ; (to-r | to-w | fence)) | rdw | detour

(* Happens Before *)
let A-cumul(r) = rfe? ; r
let cumul-fence = A-cumul(strong-fence | po-rel) | wmb

let rec prop = (overwrite & ext)? ; cumul-fence ; hb*
    and hb = ppo | rfe | ((hb* ; prop) & int)
acyclic hb as happens-before

(****************************************)
(* Write and fence propagation ordering *)
(****************************************)

(* Propagation *)
let prop2 = prop | ((overwrite & ext)? ; rfe?)
let pb = (prop2 ; strong-fence ; hb*) | ([W] ; prop ; [W])
acyclic pb as propagation

(*******)
(* RCU *)
(*******)

let rscs = po ; crit^-1 ; po?
let link = hb* ; pb* ; prop2

(* Chains that affect the RCU grace-period guarantee *)
let gp-link = gp ; link
let rscs-link = rscs ; link

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