• Marco Elver's avatar
    tools/memory-model: Fix "conflict" definition · c1b14609
    Marco Elver authored
    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.pdfSigned-off-by: default avatarMarco Elver <elver@google.com>
    Co-developed-by: default avatarAlan Stern <stern@rowland.harvard.edu>
    Signed-off-by: default avatarAlan Stern <stern@rowland.harvard.edu>
    Acked-by: default avatarAndrea Parri <parri.andrea@gmail.com>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
    c1b14609
explanation.txt 96.2 KB