diff --git a/storage/innobase/include/ib0mutex.h b/storage/innobase/include/ib0mutex.h index 2e77e191dab..b81dd6d7289 100644 --- a/storage/innobase/include/ib0mutex.h +++ b/storage/innobase/include/ib0mutex.h @@ -538,9 +538,8 @@ struct TTASEventMutex { /** Release the mutex. */ void exit() UNIV_NOTHROW { m_lock_word.store(false); - std::atomic_thread_fence(std::memory_order_acquire); - if (m_waiters.load(std::memory_order_acquire)) { + if (m_waiters.load()) { signal(); } } @@ -672,20 +671,11 @@ struct TTASEventMutex { m_policy.add(n_spins, n_waits); } - /** @return the value of the m_waiters flag */ - lock_word_t waiters() UNIV_NOTHROW { - return (m_waiters.load(std::memory_order_relaxed)); - } - /** Note that there are threads waiting on the mutex */ - void set_waiters() UNIV_NOTHROW { - m_waiters.store(true, std::memory_order_release); - } + void set_waiters() UNIV_NOTHROW { m_waiters.store(true); } /** Note that there are no threads waiting on the mutex */ - void clear_waiters() UNIV_NOTHROW { - m_waiters.store(false, std::memory_order_release); - } + void clear_waiters() UNIV_NOTHROW { m_waiters.store(false); } /** Wakeup any waiting thread(s). */ void signal() UNIV_NOTHROW; diff --git a/storage/innobase/include/ut0mutex.ic b/storage/innobase/include/ut0mutex.ic index 6b3ec99c617..ef8179747f2 100644 --- a/storage/innobase/include/ut0mutex.ic +++ b/storage/innobase/include/ut0mutex.ic @@ -49,6 +49,111 @@ bool TTASEventMutex::wait(const char *filename, uint32_t line, sync_cell_t *cell; sync_array_t *sync_arr; + /* We shall prove that in C++14 as defined by the draft N4140 following holds: + + Theorem 1. If thread X decides to call os_event_wait(), and each thread which + calls enter() eventually calls exit(), then X will eventually be woken up. + + Proof: By contradiction. + We assume the contrary, that thread X got to endless sleep, so the following + operations are in `sequenced-before` relation in X: + X1 epoc_counter=os_event_reset() + X2 m_waiters.store(true) + X3 unsuccessful m_lock_word.compare_exchange_strong(false,true) + X4 os_event_wait(epoc_counter) + + ----- + Lemma 1. All os_event_set()s `happen-before` X1. + Proof of Lemma 1: By contradiction. + The three functions os_event_reset(), os_event_set() and os_event_wait() use + internally the same mutex, so there must be a single objective order in which + calls to them `synchronize-with` each other, and thus for each two such calls + exactly one has to `happens-before` the other. + + If there is at least one call to os_event_set() which `happens-after` X1, then + we can show that X will not sleep indefinitely, as either: + a) os_event_set() `happens-before` X4, in which case it increments the + epoch counter, and os_event_wait() will notice epoch counter doesn't match + the one from X1 and will not even start the sleep, + b) X4 `happens-before` the os_event_set() in which case by the specification + of os_event_set() it will wake up thread X. + Contradiction with assumption that thread X goes to endless sleep ends the + proof of Lemma 1. + ----- + + X4 is only executed if X3 seen m_lock_word==true, and this `true` must be a + result of most recent store in modification-order of m_lock_word because: + "29.3.11 Atomic read-modify-write operations shall always read the last value + (in the modification order) written before the write associated with the + read-modify-write operation." + + We only write `true` to m_lock_word using compare_exchange_strong in enter(), + so let Y be the last thread which performed this operation before X3 in + `modification-order` of m_lock_word. + We've assumed Y must eventually call exit(), which involves: + Y1 m_lock_word.store(false) + Y2 if (m_waiters.load()) { + Y3 m_waiters.store(false) + Y4 os_event_set() } + + The standard says: + "29.3.3. There shall be a single total order S on all memory_order_seq_cst + operations, consistent with the “happens before” order and modification orders + for all affected locations (...)" + + We will now show, that X2 is before Y2 in S. + + As Y's enter() is `sequenced-before` Y1, and the enter() executed the last + write before X3 in the `modification-order` of m_lock_word, it follows, that + Y1 must be after X3 in the `modification-order` of m_lock_word. + + So, X3 is before Y1 in S, to be consistent with `modification-order` of + m_lock_word. + + Y1 is `sequenced-before` Y2, thus Y1 `happens-before` Y2, thus Y1 is before + Y2 in S. + X2 is `sequenced-before` X3, thus X2 `happens-before` X3, thus X2 is before + X3 in S. + Combining all these, we get that X2 is before Y2 in S. + + Now, we will show that Y2 can not read `true` nor `false` as both lead to + contradiction. + + If Y2 loads `true`, then Y will proceed to call os_event_set() during Y4. + By Lemma 1 Y4 `happens-before` X1. But, Y2 is `sequenced-before` Y4, + and X1 is `sequenced-before` X2, which together would give that Y2 + `happens-before` X2 which contradicts the rule that S is consistent with + `happens-before`, and we've already established that X2 is before Y2 in S. + + So, it must be that Y2 loads `false`. There is only one place in code which + writes `false` to this variable: during exit(). Of course thread Y can not + read in Y2 its own future store from Y3, so it must be some other thread Z, + which was executing: + Z3 m_waiters.store(false) + Z4 os_event_set() + By Lemma 1 Z4 `happens-before` X1, and since Z3 is `sequenced-before` Z4, and + X1 is `sequenced-before` X2, we get Z3 `happens-before` X2. + Thus, we get, that in S the order is: Z3, X2, Y2. + + We will now use following rule from the standard for Y2=B, X2=A, M=m_waiters: + "29.3.3. (...)such that each memory_order_seq_cst operation B + that loads a value from an atomic object M observes one of the following + values: + (3.1) the result of the last modification A of M that precedes B in S, if it + exists, or + (3.2) if A exists, the result of some modification of M that is not + memory_order_seq_cst and that does not happen before A, or + (3.3) if A does not exist, the result of some modification of M that is not + memory_order_seq_cst." + Note that (3.2) and (3.3) are both impossible, as all operations on m_waiters + are memory_order_seq_cst. + Thus, Y2 must read he result of the last modification of m_waiters that + precedes Y2 in S. This can not be Z3, because it is not the last modification + before Y2, as we know X2 must appear somewhere between Z3 and Y2 in S. + + So, Y2 can not load `false` neither. Contradiction ends the proof. + */ + sync_arr = sync_array_get_and_reserve_cell( this, (m_policy.get_id() == LATCH_ID_BUF_BLOCK_MUTEX || @@ -98,7 +203,7 @@ void TTASEventMutex::signal() UNIV_NOTHROW { clear_waiters(); /* The memory order of resetting the waiters field and - signaling the object is important. See LEMMA 1 above. */ + signaling the object is important. See Theorem 1 above. */ os_event_set(m_event); sync_array_object_signalled();