43 dead_lock_detector::remove_object(
this);
48 bool is_locked()
const noexcept
50 return semaphore.load(std::memory_order::relaxed) != 0;
55 if constexpr (UseDeadLockDetector) {
56 hilet other = dead_lock_detector::lock(
this);
58 hi_axiom(other !=
this);
60 hi_axiom(other ==
nullptr);
63 hi_axiom(holds_invariant());
66 semaphore_value_type expected = 0;
67 if (!semaphore.compare_exchange_strong(expected, 1, std::memory_order::acquire)) {
68 [[unlikely]] lock_contended(expected);
71 hi_axiom(holds_invariant());
83 if constexpr (UseDeadLockDetector) {
84 hilet other = dead_lock_detector::lock(
this);
86 hi_axiom(other !=
this);
88 hi_axiom(other ==
nullptr);
91 hi_axiom(holds_invariant());
94 semaphore_value_type expected = 0;
95 if (!semaphore.compare_exchange_strong(expected, 1, std::memory_order::acquire)) {
96 hi_axiom(holds_invariant());
98 if constexpr (UseDeadLockDetector) {
100 hi_axiom(dead_lock_detector::unlock(
this));
103 [[unlikely]]
return false;
106 hi_axiom(holds_invariant());
110 void unlock() noexcept
112 if constexpr (UseDeadLockDetector) {
114 hi_axiom(dead_lock_detector::unlock(
this));
117 hi_axiom(holds_invariant());
119 if (semaphore.fetch_sub(1, std::memory_order::relaxed) != 1) {
120 [[unlikely]] semaphore.store(0, std::memory_order::release);
122 semaphore.notify_one();
127 hi_axiom(holds_invariant());
137 std::atomic_unsigned_lock_free semaphore = 0;
138 using semaphore_value_type =
typename decltype(semaphore)::value_type;
140 bool holds_invariant() const noexcept
142 return semaphore.load(std::memory_order::relaxed) <= 2;
145 hi_no_inline
void lock_contended(semaphore_value_type expected)
noexcept
147 hi_axiom(holds_invariant());
150 hilet should_wait = expected == 2;
154 if (should_wait || semaphore.compare_exchange_strong(expected, 2)) {
155 hi_axiom(holds_invariant());
159 hi_axiom(holds_invariant());
162 }
while (!semaphore.compare_exchange_strong(expected, 2));