linux-kernel - Re: [PATCH v3] tools/memory-model/Documentation: Fix "conflict" definition

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-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <Pine.LNX.4.44L0.2003021256130.1555-100000@iolanthe.rowland.org>
Date:   Mon, 2 Mar 2020 12:56:59 -0500 (EST)
From:   Alan Stern <stern@...land.harvard.edu>
To:     Marco Elver <elver@...gle.com>
cc:     linux-kernel@...r.kernel.org, <kasan-dev@...glegroups.com>,
        <parri.andrea@...il.com>, <will@...nel.org>,
        <peterz@...radead.org>, <boqun.feng@...il.com>,
        <npiggin@...il.com>, <dhowells@...hat.com>, <j.alglave@....ac.uk>,
        <luc.maranget@...ia.fr>, <paulmck@...nel.org>, <akiyks@...il.com>,
        <dlustig@...dia.com>, <joel@...lfernandes.org>,
        <linux-arch@...r.kernel.org>
Subject: Re: [PATCH v3] tools/memory-model/Documentation: Fix "conflict"
 definition

On Mon, 2 Mar 2020, Marco Elver wrote:

> The definition of "conflict" should not include the type of access nor
> whether the accesses are concurrent or not, which this patch addresses.
> The definition of "data race" remains unchanged.
> 
> The definition of "conflict" as we know it and is cited by various
> papers on memory consistency models appeared in [1]: "Two accesses to
> the same variable conflict if at least one is a write; two operations
> conflict if they execute conflicting accesses."
> 
> The LKMM as well as the C11 memory model are adaptations of
> data-race-free, which are based on the work in [2]. Necessarily, we need
> both conflicting data operations (plain) and synchronization operations
> (marked). For example, C11's definition is based on [3], which defines a
> "data race" as: "Two memory operations conflict if they access the same
> memory location, and at least one of them is a store, atomic store, or
> atomic read-modify-write operation. In a sequentially consistent
> execution, two memory operations from different threads form a type 1
> data race if they conflict, at least one of them is a data operation,
> and they are adjacent in <T (i.e., they may be executed concurrently)."
> 
> [1] D. Shasha, M. Snir, "Efficient and Correct Execution of Parallel
>     Programs that Share Memory", 1988.
> 	URL: http://snir.cs.illinois.edu/listed/J21.pdf
> 
> [2] S. Adve, "Designing Memory Consistency Models for Shared-Memory
>     Multiprocessors", 1993.
> 	URL: http://sadve.cs.illinois.edu/Publications/thesis.pdf
> 
> [3] H.-J. Boehm, S. Adve, "Foundations of the C++ Concurrency Memory
>     Model", 2008.
> 	URL: https://www.hpl.hp.com/techreports/2008/HPL-2008-56.pdf
> 
> Signed-off-by: Marco Elver <elver@...gle.com>
> Co-developed-by: Alan Stern <stern@...land.harvard.edu>
> Signed-off-by: Alan Stern <stern@...land.harvard.edu>
> ---
> v3:
> * Apply Alan's suggestion.
> * s/two race candidates/race candidates/

Looks good!

Alan