Potential to modify ordering for data in half_lock model

[wang384670111]

I developed a static analysis tool to detect issues related to memory ordering, thread performance, and security. During my examination of several crates, I encountered alarms triggered by the following code：

  {
    "AtomicCorrelationViolation": {
      "bug_kind": "AtimicCorrelationViolation",
      "possibility": "Possibly",
      "diagnosis": {
        "atomic": "/Users/wangcheng/.cargo/registry/src/index.crates.io-6f17d22bba15001f/signal-hook-registry-1.4.1/src/half_lock.rs:150:30: 150:52"
      },
      "explanation": "Using an atomic operation with a stronger memory ordering than necessary can lead to unnecessary performance overhead. Using Acquire is sufficient to ensure the correctness of the program"
    }
  },
  {
    "AtomicCorrelationViolation": {
      "bug_kind": "AtimicCorrelationViolation",
      "possibility": "Possibly",
      "diagnosis": {
        "atomic": "/Users/wangcheng/.cargo/registry/src/index.crates.io-6f17d22bba15001f/signal-hook-registry-1.4.1/src/half_lock.rs:205:30: 205:52"
      },
      "explanation": "Using an atomic operation with a stronger memory ordering than necessary can lead to unnecessary performance overhead. Using Acquire is sufficient to ensure the correctness of the program"
    }
  },
  {
    "AtomicCorrelationViolation": {
      "bug_kind": "AtimicCorrelationViolation",
      "possibility": "Possibly",
      "diagnosis": {
        "atomic": "/Users/wangcheng/.cargo/registry/src/index.crates.io-6f17d22bba15001f/signal-hook-registry-1.4.1/src/half_lock.rs:228:48: 228:70"
      },
      "explanation": "Using an atomic operation with a stronger memory ordering than necessary can lead to unnecessary performance overhead. Using Acquire is sufficient to ensure the correctness of the program"
    }
  },
  {
    "AtomicCorrelationViolation": {
      "bug_kind": "AtimicCorrelationViolation",
      "possibility": "Possibly",
      "diagnosis": {
        "atomic": "/Users/wangcheng/.cargo/registry/src/index.crates.io-6f17d22bba15001f/signal-hook-registry-1.4.1/src/half_lock.rs:81:34: 81:61"
      },
      "explanation": "Using an atomic operation with a stronger memory ordering than necessary can lead to unnecessary performance overhead. Using AcqRel is sufficient to ensure the correctness of the program."
    }
  }

After reviewing the code, I believe the detector's results are accurate. https://github.com/vorner/signal-hook/blob/7dfed903c065962164699c0c015c36f838135fa6/signal-hook-registry/src/half_lock.rs#L150-L154 Acquire at 150 is ok because data is dereferenced at 154. We should use Acquire to observe other modifications made to this location. Therefore, I believe that the load operation for the head should use Acquire. Similar usage appears in the code below: https://github.com/vorner/signal-hook/blob/7dfed903c065962164699c0c015c36f838135fa6/signal-hook-registry/src/half_lock.rs#L205-L209 Additionally, using Acquire at 228 is sufficient, as this line converts the pointer into a smart pointer. Since smart pointers automatically implement dereferencing, seeing the contents inside the local at 229 during drop is necessary. Therefore, using Acquire ensures the correctness of the program. https://github.com/vorner/signal-hook/blob/7dfed903c065962164699c0c015c36f838135fa6/signal-hook-registry/src/half_lock.rs#L226-L230 Finally, the swap at 81 should use AcqRel. We need to ensure a Release fence for the successful initialization at line 77. Additionally, the drop at 86 requires visibility into the content pointed by the pointer, necessitating an Acquire fence. Therefore, using AcqRel for swap ensures the program's correctness https://github.com/vorner/signal-hook/blob/7dfed903c065962164699c0c015c36f838135fa6/signal-hook-registry/src/half_lock.rs#L77-L86

(happy to make a PR if this looks reasonable)

[vorner]

Hello

I'd agree that the used SeqCsq used everywhere is probably stronger than necessary. But if you read the big comment at the top of the file, it explains why I believe being conservative is better here (better safe than sorry) ‒ signals are rare in practice and already so expensive things that the difference that ordering makes is negligible.

Also, the reasoning you give above is more reasoning why at least this ordering is needed, not why it is enough (though I feel like it should be enough, as mentioned).

So, if you want to go ahead and change these, I'd ask you to:

• Explain why you think the stuff mentioned in the comment isn't true.
• Provide some kind of proof (semi-formal) why the used orderings are (always) enough.