Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67;
Date:   Thu, 25 Apr 2019 14:26:11 +0200
From:   Peter Zijlstra <peterz@infradead.org>
To:     huangpei@loongson.cn
Cc:     Paul Burton <paul.burton@mips.com>,
        "stern@rowland.harvard.edu" <stern@rowland.harvard.edu>,
        "akiyks@gmail.com" <akiyks@gmail.com>,
        "andrea.parri@amarulasolutions.com" 
        <andrea.parri@amarulasolutions.com>,
        "boqun.feng@gmail.com" <boqun.feng@gmail.com>,
        "dlustig@nvidia.com" <dlustig@nvidia.com>,
        "dhowells@redhat.com" <dhowells@redhat.com>,
        "j.alglave@ucl.ac.uk" <j.alglave@ucl.ac.uk>,
        "luc.maranget@inria.fr" <luc.maranget@inria.fr>,
        "npiggin@gmail.com" <npiggin@gmail.com>,
        "paulmck@linux.ibm.com" <paulmck@linux.ibm.com>,
        "will.deacon@arm.com" <will.deacon@arm.com>,
        "linux-kernel@vger.kernel.org" <linux-kernel@vger.kernel.org>,
        "torvalds@linux-foundation.org" <torvalds@linux-foundation.org>,
        Huacai Chen <chenhc@lemote.com>
Subject: Re: Re: Re: [RFC][PATCH 2/5] mips/atomic: Fix loongson_llsc_mb()
 wreckage
Message-ID: <20190425122611.GT4038@hirez.programming.kicks-ass.net>
References: <20190424123656.484227701@infradead.org>
 <20190424124421.636767843@infradead.org>
 <20190424211759.52xraajqwudc2fza@pburton-laptop>
 <2b2b07cc.bf42.16a52dc4e4d.Coremail.huangpei@loongson.cn>
 <20190425073348.GV11158@hirez.programming.kicks-ass.net>
 <5b13fd3b.c031.16a54452744.Coremail.huangpei@loongson.cn>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <5b13fd3b.c031.16a54452744.Coremail.huangpei@loongson.cn>
User-Agent: Mutt/1.10.1 (2018-07-13)
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

On Thu, Apr 25, 2019 at 07:32:59PM +0800, huangpei@loongson.cn wrote:

> > > If it is not LL/SC but other memory access from B on V, A's ll/sc can
> > > follow the atomic semantics even if A violate the coherence protocol
> > > in the same situation.
> > 
> > *shudder*...
> > 
> >   C atomic-set
> > 
> >   {
> > 	  atomic_set(v, 1);
> >   }

This is the initial state.

> 
> > 
> >   P1(atomic_t *v)
> >   {
> > 	  atomic_add_unless(v, 1, 0);
> >   }
> > 
> >   P2(atomic_t *v)
> >   {
> > 	  atomic_set(v, 0);
> >   }
> > 
> >   exists
> >   (v=2)
> > 
> > So that one will still work? (that is, v=2 is forbidden)
> 
> you mean C，P1, P2 on 3 different CPU? I do not know much about LKMM, can explain the test case more explicit?

The 'C' is the language identifier, the 'atomic-set' is the litmus name.

The unnamed block give the initial conditions.

Pn blocks give code sequences for CPU n

The 'exists' clause is evaluated after all Pn blocks are done.

There's others in this thread that can point you to many papers and
resources on these litmus test thingies.

So basically the initial value of @v is set to 1.

Then CPU-1 does atomic_add_unless(v, 1, 0)
     CPU-2 does atomic_set(v, 0)

If CPU1 goes first, it will see 1, which is not 0 and thus add 1 to 1
and obtains 2. Then CPU2 goes and writes 0, so the exist clause sees
v==0 and doesn't observe 2.

The other way around, CPU-2 goes first, writes a 0, then CPU-1 goes and
observes the 0, finds it matches 0 and doesn't add.  Again, the exist
clause will find 0 doesn't match 2.

This all goes unstuck if interleaved like:


	CPU-1			CPU-2

				xor	t0, t0
1:	ll	t0, v
	bez	t0, 2f
				sw	t0, v
	add	t0, t1
	sc	t0, v
	beqz t0, 1b

(sorry if I got the MIPS asm wrong; it's not something I normally write)

And the store-word from CPU-2 doesn't make the SC from CPU-1 fail.