[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <Y9WeOTmGCCfjMUtG@andrea>
Date: Sat, 28 Jan 2023 23:14:17 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
paulmck@...nel.org, will@...nel.org, peterz@...radead.org,
boqun.feng@...il.com, npiggin@...il.com, dhowells@...hat.com,
j.alglave@....ac.uk, luc.maranget@...ia.fr, akiyks@...il.com,
dlustig@...dia.com, joel@...lfernandes.org, urezki@...il.com,
quic_neeraju@...cinc.com, frederic@...nel.org,
linux-kernel@...r.kernel.org
Subject: Re: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po
> Evidently the plain-coherence check rules out x=1 at the
> end, because when I relax that check, x=1 becomes a possible result.
> Furthermore, the graphical output confirms that this execution has a
> ww-incoh edge from Wx=2 to Wx=1. But there is no ww-vis edge from Wx=1
> to Wx=2! How can this be possible? It seems like a bug in herd7.
By default, herd7 performs some edges removal when generating the
graphical outputs. The option -showraw can be useful to increase
the "verbosity", for example,
[with "exists (x=2)", output in /tmp/T.dot]
$ herd7 -conf linux-kernel.cfg T.litmus -show prop -o /tmp -skipchecks plain-coherence -doshow ww-vis -showraw ww-vis
> Furthermore, the execution with x=2 at the end doesn't have either a
> ww-vis or a ww-nonrace edge betwen Wx=1 and Wx=2. So why isn't there a
> ww-race edge?
And similarly
[with "exists (x=2)"]
$ herd7 -conf linux-kernel.cfg T.litmus -show prop -o /tmp -doshow ww-vis,ww-nonrace -showraw ww-vis,ww-nonrace
Andrea
Powered by blists - more mailing lists