Theoretical origin of acquire semantics only for reads?

Question

What theoretical concept lies behind the strong restriction of acquire semantics - to reads, and release semantics - to writes? (With papers titles and authors, if possible.)

Is it related to provision of correctness of more complex approaches than lock-based synchronization (as lock-free, wait-free algorithms)?

How the correctness of protected data access is guaranteed by this concept with a lock-based approach?

Rationale for the astonishment (it was preface but I've later moved it to bottom):

Letʼs consider an inter-processor synchronization using a pure spinlock (avoid queues and task switching). While a spinlock is held, the data protected by it can be read or written. All these operations shall be finished (reads - values moved to the processor, writes - values exposed to other processors visibility) before releasing the spinlock. Release could be as simple as a single write to spinlockʼs location. So, the ordering is to, in a layman words, to commit all reads and writes in program order before the write that releases the spinlock - this is called "release semantics" tied to the spinlock release.

... read protected data...
... write protected data...
<-- The barrier between previous reads/writes and spinlock store
do_unlock: write-release (spinlock address) -- release for the barrier
... unrelated activity...

This is OK, no problems here.

(I use "processor" here universally for "core", "hart", "PE" (ARM term) as well - as a single entity with independent instruction stream.)

Then, letʼs move to spinlock acquiring. The change of a shared state which prevents other processors to use the data protected by a spinlock is writing a value to the spinlock location which shows the spinlock is held (it could be simply 1, or processorʼs id... any except "free" denotation). The important fact this is write, not just read, despite read inevitably participates here to detect when an acquire attempt can be issued. Only after this write is exposed to other processors the acquired one can start with read and write of protected data.

This definitely suggests a barrier (StoreLoad+StoreStore) shall be applied between the succeeded write to spinlock and the protected data use:

... unrelated activity...
do_lock: for(;;) {
    if (locked) { continue; }
    if (compare-and-store succeeds) { break; }
} // acquire!
<-- Here the barrier between spinlock store and following reads/writes
... read protected data...
... write protected data...

A barrier of this style - between operation and following instructions in the program order - is called "acquire semantics". But in all sources I see it is tyable only to reads, not writes. If additional measures are not applied to install a barrier between the spinlock store and the protected data access, processor reordering may violate the safety.

Different processor ISAs currently address this issue in a different manner:

For x86 family, "Reads or writes cannot be reordered with I/O instructions, locked instructions, or serializing instructions" - so a locked instruction like CMPXCHG provides even stronger guarantees.

For RISC-V, the following is declared in the base specification:

The LR/SC sequence can be given acquire semantics by setting the aq bit on the LR instruction. The LR/SC sequence can be given release semantics by setting the rl bit on the SC instruction. Setting the aq bit on the LR instruction, and setting both the aq and the rl bit on the SC instruction makes the LR/SC sequence sequentially consistent, meaning that it cannot be reordered with earlier or later memory operations from the same hart.

so setting aq on LR is enough to make respective SC having acquire semantics as well, so, all instructions following in program order shall be committed after committing of SC (store gets visible to others).

ARMv8.1 suggests using instructions like CASA where acquire semantics is spreaded to both CAS sub-actions - read and write. (ARM DDI 0487F.c says "CASA and CASAL load from memory with acquire semantics." without a word of propagation of acquire semantics to store counterpart, but, in practice, I couldnʼt disprove this propagation.)

But ARMv8.0 doesnʼt have CASA and entails use of LR/SC sequence (called "load exclusive" / "store exclusive" in ARM). If to lock using cycle of LDAXR+STLXR, ordering is insufficient. The answer here shows an example of real code which fails on AArch64 using LR/SC. In a sequence like:

1:      ldaxrb  w2, [x0] // LL+acquire
         // stlxrb can be replaced with stxrb
         // (no SC, plain store)
         // with the same outcome
        stlxrb  w3, w1, [x0] // SC+release
        cbnz    w3, 1b
//-     ldarb   w3, [x0] // load+acquire

Without the (commented here) ldarb, reordering happens and the test program crashes. This ldarb seems a true minimum of ordering; extended versions with dmb, dsb work as well (dmb ld does but dmb st doesnʼt; dsb ld already does). Iʼve confirmed the author conclusion using another AArch64 processor model.

In ARMv8.0, this looks as the design gap, fixed later on. But my question now is where the concept "acquire - for reads" originates in.

P.S.: I have asked nearly the same but at purely practical aspect here. The following discussion exposed the issue is real, and provided more evidences, but with no theoretical reference.

UPDATE(2024-03-19): The earliest mention Iʼve found is in the article: "Memory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors" by: Kourosh Gharachorloo, Daniel Lenoski, James Laudon, Phillip Gibbons, Anoop Gupta, and John Hennessy, 1990. It is apparently first to define "Release consistency" and respective terms for acquire and release semantics. This article declares, as well, that "Although the store access is necessary to ensure mutual exclusion, it does not function as either an acquire or a release." This looks too hasty from the current POV. To be continued.