30 Jun, 2020

8 commits

  • herdtools 7.56 has enhanced herd7's C parser so that the "(void)expr"
    construct in Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus is
    accepted.

    This is independent of LKMM's cat model, so mention the required
    version in the header of the litmus test and its entry in README.

    CC: Boqun Feng
    Reported-by: Andrea Parri
    Acked-by: Andrea Parri
    Signed-off-by: Akira Yokosawa
    Signed-off-by: Paul E. McKenney

    Akira Yokosawa
     
  • This commit cites a pertinent RCU-related litmus test.

    Co-developed-by: Joel Fernandes (Google)
    Co-developed-by: Akira Yokosawa
    [Alan: grammar nit]
    [ paulmck: Update commit log and title per Akira feedback. ]
    Suggested-by: Alan Stern
    Signed-off-by: Joel Fernandes (Google)
    Signed-off-by: Akira Yokosawa
    Signed-off-by: Paul E. McKenney

    Joel Fernandes (Google)
     
  • Where Documentation/litmus-tests/README lists RCU litmus tests,
    Documentation/litmus-tests/atomic/README lists atomic litmus tests.
    For symmetry, merge the latter into former, with some context
    adjustment in the introduction.

    Acked-by: Andrea Parri
    Acked-by: Joel Fernandes (Google)
    Acked-by: Boqun Feng
    Signed-off-by: Akira Yokosawa
    Signed-off-by: Paul E. McKenney

    Akira Yokosawa
     
  • We already use a litmus test in atomic_t.txt to describe atomic RMW +
    smp_mb__after_atomic() is stronger than acquire (both the read and the
    write parts are ordered). So make it a litmus test in atomic-tests
    directory, so that people can access the litmus easily.

    Additionally, change the processor numbers "P1, P2" to "P0, P1" in
    atomic_t.txt for the consistency with the processor numbers in the
    litmus test, which herd can handle.

    Acked-by: Alan Stern
    Acked-by: Andrea Parri
    Signed-off-by: Boqun Feng
    Reviewed-by: Joel Fernandes (Google)
    Signed-off-by: Paul E. McKenney

    Boqun Feng
     
  • We already use a litmus test in atomic_t.txt to describe the behavior of
    an atomic_set() with the an atomic RMW, so add it into atomic-tests
    directory to make it easily accessible for anyone who cares about the
    semantics of our atomic APIs.

    Besides currently the litmus test "atomic-set" in atomic_t.txt has a few
    things to be improved:

    1) The CPU/Processor numbers "P1,P2" are not only inconsistent with
    the rest of the document, which uses "CPU0" and "CPU1", but also
    unacceptable by the herd tool, which requires processors start
    at "P0".

    2) The initialization block uses a "atomic_set()", which is OK, but
    it's better to use ATOMIC_INIT() to make clear this is an
    initialization.

    3) The return value of atomic_add_unless() is discarded
    inexplicitly, which is OK for C language, but it will be helpful
    to the herd tool if we use a void cast to make the discard
    explicit.

    4) The name and the paragraph describing the test need to be more
    accurate and aligned with our wording in LKMM.

    Therefore fix these in both atomic_t.txt and the new added litmus test.

    Acked-by: Andrea Parri
    Acked-by: Alan Stern
    Signed-off-by: Boqun Feng
    Reviewed-by: Joel Fernandes (Google)
    Signed-off-by: Paul E. McKenney

    Boqun Feng
     
  • Although we have atomic_t.txt and its friends to describe the semantics
    of atomic APIs and lib/atomic64_test.c for build testing and testing in
    UP mode, the tests for our atomic APIs in real SMP mode are still
    missing. Since now we have the LKMM tool in kernel and litmus tests can
    be used to generate kernel modules for testing purpose with "klitmus" (a
    tool from the LKMM toolset), it makes sense to put a few typical litmus
    tests into kernel so that

    1) they are the examples to describe the conceptual mode of the
    semantics of atomic APIs, and

    2) they can be used to generate kernel test modules for anyone
    who is interested to test the atomic APIs implementation (in
    most cases, is the one who implements the APIs for a new arch)

    Therefore, introduce the atomic directory for this purpose. The
    directory is maintained by the LKMM group to make sure the litmus tests
    are always aligned with our memory model.

    Acked-by: Alan Stern
    Acked-by: Andrea Parri
    Reviewed-by: Joel Fernandes (Google)
    Signed-off-by: Boqun Feng
    Signed-off-by: Paul E. McKenney

    Boqun Feng
     
  • This adds an example for the important RCU grace period guarantee, which
    shows an RCU reader can never span a grace period.

    Acked-by: Andrea Parri
    Signed-off-by: Joel Fernandes (Google)
    Signed-off-by: Paul E. McKenney

    Joel Fernandes (Google)
     
  • This adds an example for the important RCU grace period guarantee, which
    shows an RCU reader can never span a grace period.

    Acked-by: Andrea Parri
    Signed-off-by: Joel Fernandes (Google)
    Signed-off-by: Paul E. McKenney

    Joel Fernandes (Google)