summaryrefslogtreecommitdiffstats
path: root/tools/memory-model
diff options
context:
space:
mode:
authorAndrea Parri <andrea.parri@amarulasolutions.com>2018-05-14 19:33:54 -0400
committerIngo Molnar <mingo@kernel.org>2018-05-15 02:11:18 -0400
commit05604e7e3adbd78f074b7f86b14f50888bf66252 (patch)
tree5e366451ede247ce920c16a6a86e76004d01a889 /tools/memory-model
parentcee0321a404fe6b43d1f4364639c8ffe2f2b37d1 (diff)
tools/memory-model: Fix coding style in 'lock.cat'
This commit uses tabs for indentation and adds spaces around binary operator. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-16-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model')
-rw-r--r--tools/memory-model/lock.cat28
1 files changed, 14 insertions, 14 deletions
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index cd002a33ca8a..305ded17e741 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -84,16 +84,16 @@ let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
84 84
85(* rfe for LF events *) 85(* rfe for LF events *)
86let all-possible-rfe-lf = 86let all-possible-rfe-lf =
87 (* 87 (*
88 * Given an LF event r, compute the possible rfe edges for that event 88 * Given an LF event r, compute the possible rfe edges for that event
89 * (all those starting from LKW events in other threads), 89 * (all those starting from LKW events in other threads),
90 * and then convert that relation to a set of single-edge relations. 90 * and then convert that relation to a set of single-edge relations.
91 *) 91 *)
92 let possible-rfe-lf r = 92 let possible-rfe-lf r =
93 let pair-to-relation p = p ++ 0 93 let pair-to-relation p = p ++ 0
94 in map pair-to-relation ((LKW * {r}) & loc & ext) 94 in map pair-to-relation ((LKW * {r}) & loc & ext)
95 (* Do this for each LF event r that isn't in rfi-lf *) 95 (* Do this for each LF event r that isn't in rfi-lf *)
96 in map possible-rfe-lf (LF \ range(rfi-lf)) 96 in map possible-rfe-lf (LF \ range(rfi-lf))
97 97
98(* Generate all rf relations for LF events *) 98(* Generate all rf relations for LF events *)
99with rfe-lf from cross(all-possible-rfe-lf) 99with rfe-lf from cross(all-possible-rfe-lf)
@@ -110,10 +110,10 @@ let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
110 110
111(* rfe for RU events: an RU may read from an external UL or the initial write *) 111(* rfe for RU events: an RU may read from an external UL or the initial write *)
112let all-possible-rfe-ru = 112let all-possible-rfe-ru =
113 let possible-rfe-ru r = 113 let possible-rfe-ru r =
114 let pair-to-relation p = p ++ 0 114 let pair-to-relation p = p ++ 0
115 in map pair-to-relation (((UL|IW) * {r}) & loc & ext) 115 in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
116 in map possible-rfe-ru RU 116 in map possible-rfe-ru RU
117 117
118(* Generate all rf relations for RU events *) 118(* Generate all rf relations for RU events *)
119with rfe-ru from cross(all-possible-rfe-ru) 119with rfe-ru from cross(all-possible-rfe-ru)