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
|
"AArch64, follow documentation"
include "cos.cat"
(* Uniproc *)
acyclic po-loc | rf | fr | co as uniproc
(* Utilities *)
let dd = addr | data
let rdw = po-loc & (fre;rfe)
let detour = po-loc & (coe ; rfe)
let addrpo = addr;po
let com = fr | co | rf
empty rmw & (fre;coe) as atomic
include "aarch64fences.cat"
let ci0 = ctrlisb | detour
let ii0 = dd | rfi | rdw
let cc0 = dd | ctrl | addrpo
let ic0 = 0
include "ppo.cat"
let acq = (A * M) & po
let rel = (M * L) & po
let ppo = ppo | acq
let strongf = dmb.sy & (M * M)
| dsb.sy & (M * M)
| dmb.st & (W * W)
| dsb.st & (W * W)
| dmb.ld & (R * M)
| dsb.ld & (R * M)
let weakf = rel
let fence = strongf | weakf
let hb = (R * M) & fence | rfe | ppo
acyclic hb as thin_air
(* Now we take "observed" as defined in the doc *)
let hbstar = hb*
let comstar = (fr|rf|co)*
(* prop is (almost) as before, basically fence effect *)
(* coe? added, given the definition of observed writes:
A write is said to be observed by an observer..
- when a subsequent read by the
same observer return the values written by the observed write, or
written by a write [to that location by any observer] that is sequenced
in the Coherence order of the location after the observed write.
-> rfe
- A subsequent write of the location by the same observer is sequenced
in the Coherence order of the location after the observed write
-> coe
*)
(* Observation of external accesses *)
let observe-write = rfe|coe
let observe-read = fre
let observe-access = observe-write|observe-read
let prop_base = observe-access?;fence;hbstar
let prop = prop_base & (W * W)
| (comstar; prop_base*; strongf; hbstar)
(* Observer: a thread that performs two observations,
the second one is relatively new we assume:
fre|coe ---> the target write is observed after the source event *)
let observer =
observe-write; ppo; (fre|coe)
| observe-access; fence ; (fre|coe)
| observe-access;(L * A) & po;fre
irreflexive prop+;observer as observation
(* As before *)
let prop_al = (L * A) & (rf | po)
| (A * L) & fr
let xx = (W * W) & (X * X) & po
acyclic co | prop | xx | prop_al;hbstar as propagation
|
