No description
  • C 98.2%
  • Assembly 1%
  • Makefile 0.3%
  • Shell 0.2%
  • Python 0.1%
Find a file
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Andrea Parri 5b735eb1ce tools/memory-model: Model smp_mb__after_unlock_lock()
The kernel documents smp_mb__after_unlock_lock() the following way:

  "Place this after a lock-acquisition primitive to guarantee that
   an UNLOCK+LOCK pair acts as a full barrier.  This guarantee applies
   if the UNLOCK and LOCK are executed by the same CPU or if the
   UNLOCK and LOCK operate on the same lock variable."

Formalize in LKMM the above guarantee by defining (new) mb-links according
to the law:

  ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
	fencerel(After-unlock-lock) ; [M])

where the component ([UL] ; co ; [LKW]) identifies "UNLOCK+LOCK pairs on
the same lock variable" and the component ([UL] ; po ; [LKW]) identifies
"UNLOCK+LOCK pairs executed by the same CPU".

In particular, the LKMM forbids the following two behaviors (the second
litmus test below is based on:

  Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html

c.f., Section "Tree RCU Grace Period Memory Ordering Building Blocks"):

C after-unlock-lock-same-cpu

(*
 * Result: Never
 *)

{}

P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
{
	int r0;

	spin_lock(s);
	WRITE_ONCE(*x, 1);
	spin_unlock(s);
	spin_lock(t);
	smp_mb__after_unlock_lock();
	r0 = READ_ONCE(*y);
	spin_unlock(t);
}

P1(int *x, int *y)
{
	int r0;

	WRITE_ONCE(*y, 1);
	smp_mb();
	r0 = READ_ONCE(*x);
}

exists (0:r0=0 /\ 1:r0=0)

C after-unlock-lock-same-lock-variable

(*
 * Result: Never
 *)

{}

P0(spinlock_t *s, int *x, int *y)
{
	int r0;

	spin_lock(s);
	WRITE_ONCE(*x, 1);
	r0 = READ_ONCE(*y);
	spin_unlock(s);
}

P1(spinlock_t *s, int *y, int *z)
{
	int r0;

	spin_lock(s);
	smp_mb__after_unlock_lock();
	WRITE_ONCE(*y, 1);
	r0 = READ_ONCE(*z);
	spin_unlock(s);
}

P2(int *z, int *x)
{
	int r0;

	WRITE_ONCE(*z, 1);
	smp_mb();
	r0 = READ_ONCE(*x);
}

exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0)

Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Will Deacon <will.deacon@arm.com>
Cc: linux-arch@vger.kernel.org
Cc: parri.andrea@gmail.com
Link: http://lkml.kernel.org/r/20181203230451.28921-1-paulmck@linux.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
2019-01-21 11:06:55 +01:00
arch openrisc: remove unneeded code in arch/openrisc/Makefile 2019-01-17 23:42:59 +09:00
block block: fix kerneldoc comment for blk_attempt_plug_merge() 2019-01-09 15:29:08 -07:00
certs kbuild: remove redundant target cleaning on failure 2019-01-06 09:46:51 +09:00
crypto Kconfig updates for v4.21 2018-12-29 13:03:29 -08:00
Documentation Devicetree fixes for v5.0: 2019-01-18 06:15:28 +12:00
drivers First 5.0 rc pull request 2019-01-18 17:17:20 +12:00
firmware kbuild: change filechk to surround the given command with { } 2019-01-06 09:46:51 +09:00
fs AFS fixes 2019-01-18 06:27:24 +12:00
include First 5.0 rc pull request 2019-01-18 17:17:20 +12:00
init kbuild: Disable LD_DEAD_CODE_DATA_ELIMINATION with ftrace & GCC <= 4.7 2019-01-14 10:37:09 +09:00
ipc
kernel Merge branch 'stable/for-linus-5.0' of git://git.kernel.org/pub/scm/linux/kernel/git/konrad/swiotlb 2019-01-18 06:22:08 +12:00
lib sbitmap: Protect swap_lock from hardirq 2019-01-15 16:29:57 +12:00
LICENSES
mm mm/mmu_notifier: mm/rmap.c: Fix a mmu_notifier range bug in try_to_unmap_one 2019-01-10 02:58:21 -08:00
net Merge git://git.kernel.org/pub/scm/linux/kernel/git/davem/net 2019-01-16 05:13:36 +12:00
samples Merge git://git.kernel.org/pub/scm/linux/kernel/git/davem/net 2019-01-16 05:13:36 +12:00
scripts kbuild: remove unused baseprereq 2019-01-14 12:19:40 +09:00
security Merge branch 'fixes-v5.0-rc2' of git://git.kernel.org/pub/scm/linux/kernel/git/jmorris/linux-security 2019-01-17 16:54:58 +12:00
sound remove dma_zalloc_coherent 2019-01-12 10:52:40 -08:00
tools tools/memory-model: Model smp_mb__after_unlock_lock() 2019-01-21 11:06:55 +01:00
usr
virt KVM: validate userspace input in kvm_clear_dirty_log_protect() 2019-01-11 18:38:07 +01:00
.clang-format
.cocciconfig
.get_maintainer.ignore
.gitattributes
.gitignore
.mailmap A few early MIPS fixes for 4.21: 2019-01-05 12:48:25 -08:00
COPYING
CREDITS Add CREDITS entry for Shaohua Li 2019-01-04 14:27:09 -07:00
Kbuild kbuild: use assignment instead of define ... endef for filechk_* rules 2019-01-06 10:22:35 +09:00
Kconfig
MAINTAINERS Staging driver fixes for 5.0-rc2 2019-01-14 05:49:35 +12:00
Makefile kbuild: mark prepare0 as PHONY to fix external module build 2019-01-17 23:42:59 +09:00
README

Linux kernel
============

There are several guides for kernel developers and users. These guides can
be rendered in a number of formats, like HTML and PDF. Please read
Documentation/admin-guide/README.rst first.

In order to build the documentation, use ``make htmldocs`` or
``make pdfdocs``.  The formatted documentation can also be read online at:

    https://www.kernel.org/doc/html/latest/

There are various text files in the Documentation/ subdirectory,
several of them using the Restructured Text markup notation.

Please read the Documentation/process/changes.rst file, as it contains the
requirements for building and running the kernel, and information about
the problems which may result by upgrading your kernel.