ARK-OS/arkos/kernel/tools/memory-model/Documentation/herd-representation.txt

#
# Legend:
#	R,	a Load event
#	W,	a Store event
#	F,	a Fence event
#	LKR,	a Lock-Read event
#	LKW,	a Lock-Write event
#	UL,	an Unlock event
#	LF,	a Lock-Fail event
#	RL,	a Read-Locked event
#	RU,	a Read-Unlocked event
#	R*,	a Load event included in RMW
#	W*,	a Store event included in RMW
#	SRCU,	a Sleepable-Read-Copy-Update event
#
#	po,	a Program-Order link
#	rmw,	a Read-Modify-Write link - every rmw link is a po link
#
# By convention, a blank line in a cell means "same as the preceding line".
#
# Note that the syntactic representation does not always match the sets and
# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
# link, and W[ACQUIRE] are not included in the Acquire set.
#
# Disclaimer.  The table includes representations of "add" and "and" operations;
# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
# "andnot" operations are omitted.
#
    ------------------------------------------------------------------------------
    |                        C macro | Events                                    |
    ------------------------------------------------------------------------------
    |                    Non-RMW ops |                                           |
    ------------------------------------------------------------------------------
    |                      READ_ONCE | R[ONCE]                                   |
    |                    atomic_read |                                           |
    |                     WRITE_ONCE | W[ONCE]                                   |
    |                     atomic_set |                                           |
    |               smp_load_acquire | R[ACQUIRE]                                |
    |            atomic_read_acquire |                                           |
    |              smp_store_release | W[RELEASE]                                |
    |             atomic_set_release |                                           |
    |                   smp_store_mb | W[ONCE] ->po F[MB]                        |
    |                         smp_mb | F[MB]                                     |
    |                        smp_rmb | F[rmb]                                    |
    |                        smp_wmb | F[wmb]                                    |
    |          smp_mb__before_atomic | F[before-atomic]                          |
    |           smp_mb__after_atomic | F[after-atomic]                           |
    |                    spin_unlock | UL                                        |
    |                 spin_is_locked | On success: RL                            |
    |                                | On failure: RU                            |
    |         smp_mb__after_spinlock | F[after-spinlock]                         |
    |      smp_mb__after_unlock_lock | F[after-unlock-lock]                      |
    |                  rcu_read_lock | F[rcu-lock]                               |
    |                rcu_read_unlock | F[rcu-unlock]                             |
    |                synchronize_rcu | F[sync-rcu]                               |
    |                rcu_dereference | R[ONCE]                                   |
    |             rcu_assign_pointer | W[RELEASE]                                |
    |                 srcu_read_lock | R[srcu-lock]                              |
    |                 srcu_down_read |                                           |
    |               srcu_read_unlock | W[srcu-unlock]                            |
    |                   srcu_up_read |                                           |
    |               synchronize_srcu | SRCU[sync-srcu]                           |
    | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock]                 |
    ------------------------------------------------------------------------------
    |       RMW ops w/o return value |                                           |
    ------------------------------------------------------------------------------
    |                     atomic_add | R*[NORETURN] ->rmw W*[NORETURN]           |
    |                     atomic_and |                                           |
    |                      spin_lock | LKR ->po LKW                              |
    ------------------------------------------------------------------------------
    |        RMW ops w/ return value |                                           |
    ------------------------------------------------------------------------------
    |              atomic_add_return | R*[MB] ->rmw W*[MB]                       |
    |               atomic_fetch_add |                                           |
    |               atomic_fetch_and |                                           |
    |                    atomic_xchg |                                           |
    |                           xchg |                                           |
    |            atomic_add_negative |                                           |
    |      atomic_add_return_relaxed | R*[ONCE] ->rmw W*[ONCE]                   |
    |       atomic_fetch_add_relaxed |                                           |
    |       atomic_fetch_and_relaxed |                                           |
    |            atomic_xchg_relaxed |                                           |
    |                   xchg_relaxed |                                           |
    |    atomic_add_negative_relaxed |                                           |
    |      atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE]             |
    |       atomic_fetch_add_acquire |                                           |
    |       atomic_fetch_and_acquire |                                           |
    |            atomic_xchg_acquire |                                           |
    |                   xchg_acquire |                                           |
    |    atomic_add_negative_acquire |                                           |
    |      atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE]             |
    |       atomic_fetch_add_release |                                           |
    |       atomic_fetch_and_release |                                           |
    |            atomic_xchg_release |                                           |
    |                   xchg_release |                                           |
    |    atomic_add_negative_release |                                           |
    ------------------------------------------------------------------------------
    |            Conditional RMW ops |                                           |
    ------------------------------------------------------------------------------
    |                 atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB]           |
    |                                | On failure: R*[MB]                        |
    |                        cmpxchg |                                           |
    |              atomic_add_unless |                                           |
    |         atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE]       |
    |                                | On failure: R*[ONCE]                      |
    |         atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[ACQUIRE] |
    |                                | On failure: R*[ACQUIRE]                   |
    |         atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RELEASE] |
    |                                | On failure: R*[RELEASE]                   |
    |                   spin_trylock | On success: LKR ->po LKW                  |
    |                                | On failure: LF                            |
    ------------------------------------------------------------------------------