linux-kernel - Re: Plain accesses and data races in the Linux Kernel Memory Model

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Message-ID: <20190122154745.GA13659@andrea>
Date:   Tue, 22 Jan 2019 16:47:45 +0100
From:   Andrea Parri <andrea.parri@...rulasolutions.com>
To:     Alan Stern <stern@...land.harvard.edu>
Cc:     LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>,
        Boqun Feng <boqun.feng@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Nicholas Piggin <npiggin@...il.com>,
        "Paul E. McKenney" <paulmck@...ux.ibm.com>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        Dmitry Vyukov <dvyukov@...gle.com>,
        linux-kernel@...r.kernel.org
Subject: Re: Plain accesses and data races in the Linux Kernel Memory Model

> @@ -131,7 +159,7 @@ let rec rcu-fence = rcu-gp | srcu-gp |
>  	(rcu-fence ; rcu-link ; rcu-fence)
>  
>  (* rb orders instructions just as pb does *)
> -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
> +let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [marked]

Testing has revealed some subtle semantics changes for some RCU tests
_without_ unmarked memory accesses; an example is reported at the end
of this email.  I suspect that the improvements you mentioned in this
thread can restore the original semantics but I'm reporting this here
for further reference.

With the above definition of 'rb', we're losing links which originate
or target RCU fences, so that this definition is in fact a relaxation
w.r.t. the current semantics (even when limiting to marked accesses).
The test below, for example, is currently forbidden by the LKMM, but
it becomes allowed with this patch.

FWIW, I checked that including the RCU fences in 'marked' can restore
the original semantics of these tests; I'm still not sure whether this
change can make sense though....

Thoughts?

Oh, one last (and unrelated) nit before I forget: IIUC, we used to
upper-case set names, so I'd also suggest s/marked/Marked, s/plain/Plain
and similarly for the other sets to be introduced.

  Andrea

C sync-rcu-is-not-idempotent

{ }

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

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

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

	rcu_read_lock();
	WRITE_ONCE(*y, 1);
	r0 = READ_ONCE(*z);
	rcu_read_unlock();
}

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

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

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

>  
>  irreflexive rb as rcu
>