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, 15 Nov 2018 14:56:30 -0800
From:   "Paul E. McKenney" <paulmck@linux.ibm.com>
To:     linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        mingo@kernel.org
Cc:     stern@rowland.harvard.edu, parri.andrea@gmail.com,
        will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com,
        npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
        luc.maranget@inria.fr, akiyks@gmail.com
Subject: Q&A from "Concurrency with tools/memory-model"
Reply-To: paulmck@linux.ibm.com
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
User-Agent: Mutt/1.5.21 (2010-09-15)
Message-Id: <20181115225630.GA30917@linux.ibm.com>
Sender: linux-kernel-owner@vger.kernel.org
Precedence: bulk

Hello!

Good turnout and some good questions here in Vancouver BC, please see
below for rough notes.  ;-)

							Thanx, Paul

------------------------------------------------------------------------

"Concurrency with tools/memory-model"

Andrea Parri presenting.

Rough notes of Q&A.

o	Want atomic bit operation.

o	But smp_read_barrier_depends() not there, so how to note pairing?
	A:  Note the dependency as the other end of the pairing.

o	Speculation barriers, as in Spectre and Meltdown?  A: This would
	require adding timing, not in the immediate future.

o	What ordering does system calls provide?  A: None that we know of.
	Boqun: Userspace needs to explicitly provide the needed ordering
	when interacting with the kernel.  Some architectures do provide
	full barriers, but not to be counted on.

o	Why herd7?  A: Based on other formalizations -- note that herd7
	had a number of hardware models.  Paul: Plus the founder of the
	LKMM project is a co-author of herd, which might have had some
	effect.

o	Why not also model interrupts and NMIs?  Promela and spin have
	been used for this.  A: Cannot currently model them.  You can
	emulated them with additional threads and locks, if you wish.
	Vincent Nimal and Lihao Liang have done some academic work on
	these topics.