"Linux kernel strong memory model"

(*
 * Copyright (C) 2016 Alan Stern <stern@rowland.harvard.edu>,
 *		      Andrea Parri <parri.andrea@gmail.com>
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, you can access it online at
 * http://www.gnu.org/licenses/gpl-2.0.html.
 *)

include "cos-opt.cat"
include "lock.cat"

let com = rf | co | fr
let coherence-order = po-loc | com
acyclic coherence-order as coherence

empty rmw & (fre;coe) as atomic


let rf = rf | next-crit
let rfe = rf & ext

let exec-order-fence = rmb | acq-po | lk-po
let propagation-fence = strong-fence | wmb | po-relass | po-ul
let ordering-fence = propagation-fence | exec-order-fence

(* Determine the release sequences *)
let rel-seq = [ReleaseAssign] ; coi? ; (rf ; rmw)*
let po-rel-seq = po ; rel-seq

(* On Alpha, rd-dep-fence makes addr, dep-rfi, and rdw strong *)
let dep = addr | data
let dep-rfi = dep ; rfi
let rd-addr-dep-rfi = (addr | dep-rfi)+ & rd-dep-fence
let rdw = po-loc & (fre ; rfe)
let rd-rdw = rdw & rd-dep-fence
let po-loc-ww = po-loc & (W*W)
let detour = (po-loc & (coe ; rfe)) \ (po-loc-ww ; po-loc)
let addrpo = addr ; po

(* The set of writes that are bounded by the end of the thread
   or by a fence before the next write to the same address *)
let BOUNDED-W = W \ domain(po-loc-ww \ ordering-fence)
(* The set of "non-obscurable" writes on ARM *)
let NOW = domain(rfe) | range(rmw) | ReleaseAssign |
		BOUNDED-W | domain(detour)
(* The set of "obscurable" writes *)
let OW = W \ NOW
(* The set of reads which might be forwarded from obscurable writes *)
let OR = range(rfi & (OW*R))

let nco = co & (NOW*W)
let ncoe = nco & ext

let strong-ppo = rd-addr-dep-rfi | ordering-fence |
		((dep | ctrl | addrpo) & (R*W))
let Alpha-strong-ppo = strong-ppo | rd-rdw | detour |
		(po-loc & ((M\OW\OR)*W))
let ARM-strong-ppo = strong-ppo | addr | dep-rfi
let ppo = Alpha-strong-ppo | ARM-strong-ppo | rdw

let rfe-ppo = strong-ppo | (ARM-strong-ppo ; ppo* ; Alpha-strong-ppo)
let po-relass-acq-hb = (po ; (rfe & (ReleaseAssign*Acquire)) ; rfe-ppo) |
               (po-ul ; next-crit ; lk-po)

(* Release paired with Acquire is both A- and B-cumulative *)
let AB-cum-hb = strong-fence | po-relass-acq-hb
let A-cum-hb = AB-cum-hb | po-relass | po-rel-seq
let B-cum-hb = AB-cum-hb | wmb

let hb0 = (ppo* ; Alpha-strong-ppo) | (rfe ; rfe-ppo)
let propbase0 = propagation-fence | (rfe? ; A-cum-hb)

let rec B-cum-propbase = (B-cum-hb ; hb* ) |
		(rfe? ; AB-cum-hb ; hb* )
    and propbase = propbase0 | B-cum-propbase
    and short-obs = ((ncoe|fre) ; propbase+ ; rfe) & int
    and obs = short-obs |
		((hb* ; (ncoe|fre) ; propbase* ; B-cum-propbase ; rfe) & int)
    and hb = hb0 | (obs ; rfe-ppo)

acyclic hb as happens-before
irreflexive (short-obs ; Alpha-strong-ppo) as observation


let strong-prop = fre? ; propbase* ; rfe? ; strong-fence ; hb* ; obs?
let prop = (propbase & (W*W)) | strong-prop
let cpord = nco | prop

acyclic cpord as propagation


(* Propagation between strong fences *)
let rcu-order = hb* ; obs? ; cpord* ; fre? ; propbase* ; rfe?

(* Chains that can prevent the RCU grace-period guarantee *)
let gp-link = sync ; rcu-order
let cs-link = po? ; crit^-1 ; po? ; rcu-order
let rcu-path0 = gp-link |
	(gp-link ; cs-link) |
	(cs-link ; gp-link)
let rec rcu-path = rcu-path0 |
	(rcu-path ; rcu-path) |
	(gp-link ; rcu-path ; cs-link) |
	(cs-link ; rcu-path ; gp-link)

irreflexive rcu-path as rcu