[thread.lock] - C++17 → C++20

Files changed (1) hide show

tmp/tmp7t_k09r1/{from.md → to.md} +136 -173

tmp/tmp7t_k09r1/{from.md → to.md} RENAMED Viewed

@@ -46,41 +46,37 @@ namespace std {
     lock_guard& operator=(const lock_guard&) = delete;
   private:
     mutex_type& pm;             // exposition only
   };
-  template<class Mutex> lock_guard(lock_guard<Mutex>) -> lock_guard<Mutex>;
 }
 ```
 An object of type `lock_guard` controls the ownership of a lockable
 object within a scope. A `lock_guard` object maintains ownership of a
-lockable object throughout the `lock_guard` object’s lifetime (
-[[basic.life]]). The behavior of a program is undefined if the lockable
 object referenced by `pm` does not exist for the entire lifetime of the
 `lock_guard` object. The supplied `Mutex` type shall meet the
-`BasicLockable` requirements ([[thread.req.lockable.basic]]).
 ``` cpp
 explicit lock_guard(mutex_type& m);
 ```
-*Requires:* If `mutex_type` is not a recursive mutex, the calling thread
-does not own the mutex `m`.
-*Effects:* As if by `m.lock()`.
-*Postconditions:* `&pm == &m`
 ``` cpp
 lock_guard(mutex_type& m, adopt_lock_t);
 ```
-*Requires:* The calling thread owns the mutex `m`.
-*Postconditions:* `&pm == &m`
 *Throws:* Nothing.
 ``` cpp
 ~lock_guard();
@@ -96,52 +92,49 @@ namespace std {
   class scoped_lock {
   public:
     using mutex_type = Mutex;   // If MutexTypes... consists of the single type Mutex
     explicit scoped_lock(MutexTypes&... m);
-    explicit scoped_lock(MutexTypes&... m, adopt_lock_t);
     ~scoped_lock();
     scoped_lock(const scoped_lock&) = delete;
     scoped_lock& operator=(const scoped_lock&) = delete;
   private:
     tuple<MutexTypes&...> pm;   // exposition only
   };
-  template<class... MutexTypes>
-    scoped_lock(scoped_lock<MutexTypes...>) -> scoped_lock<MutexTypes...>;
 }
 ```
 An object of type `scoped_lock` controls the ownership of lockable
 objects within a scope. A `scoped_lock` object maintains ownership of
-lockable objects throughout the `scoped_lock` object’s lifetime (
-[[basic.life]]). The behavior of a program is undefined if the lockable
 objects referenced by `pm` do not exist for the entire lifetime of the
 `scoped_lock` object. When `sizeof...(MutexTypes)` is `1`, the supplied
-`Mutex` type shall meet the `BasicLockable` requirements (
-[[thread.req.lockable.basic]]). Otherwise, each of the mutex types shall
-meet the `Lockable` requirements ([[thread.req.lockable.req]]).
 ``` cpp
 explicit scoped_lock(MutexTypes&... m);
 ```
-*Requires:* If a `MutexTypes` type is not a recursive mutex, the calling
-thread does not own the corresponding mutex element of `m`.
 *Effects:* Initializes `pm` with `tie(m...)`. Then if
 `sizeof...(MutexTypes)` is `0`, no effects. Otherwise if
 `sizeof...(MutexTypes)` is `1`, then `m.lock()`. Otherwise,
 `lock(m...)`.
 ``` cpp
-explicit scoped_lock(MutexTypes&... m, adopt_lock_t);
 ```
-*Requires:* The calling thread owns all the mutexes in `m`.
 *Effects:* Initializes `pm` with `tie(m...)`.
 *Throws:* Nothing.
@@ -202,12 +195,10 @@ namespace std {
   private:
     mutex_type* pm;             // exposition only
     bool owns;                  // exposition only
   };
-  template<class Mutex> unique_lock(unique_lock<Mutex>) -> unique_lock<Mutex>;
   template<class Mutex>
     void swap(unique_lock<Mutex>& x, unique_lock<Mutex>& y) noexcept;
 }
 ```
@@ -216,123 +207,113 @@ object within a scope. Ownership of the lockable object may be acquired
 at construction or after construction, and may be transferred, after
 acquisition, to another `unique_lock` object. Objects of type
 `unique_lock` are not copyable but are movable. The behavior of a
 program is undefined if the contained pointer `pm` is not null and the
 lockable object pointed to by `pm` does not exist for the entire
-remaining lifetime ([[basic.life]]) of the `unique_lock` object. The
-supplied `Mutex` type shall meet the `BasicLockable` requirements (
-[[thread.req.lockable.basic]]).
-[*Note 1*: `unique_lock<Mutex>` meets the `BasicLockable` requirements.
-If `Mutex` meets the `Lockable` requirements (
-[[thread.req.lockable.req]]), `unique_lock<Mutex>` also meets the
-`Lockable` requirements; if `Mutex` meets the `TimedLockable`
-requirements ([[thread.req.lockable.timed]]), `unique_lock<Mutex>` also
-meets the `TimedLockable` requirements. — *end note*]
-##### `unique_lock` constructors, destructor, and assignment <a id="thread.lock.unique.cons">[[thread.lock.unique.cons]]</a>
 ``` cpp
 unique_lock() noexcept;
 ```
-*Effects:* Constructs an object of type `unique_lock`.
-*Postconditions:* `pm == 0` and `owns == false`.
 ``` cpp
 explicit unique_lock(mutex_type& m);
 ```
-*Requires:* If `mutex_type` is not a recursive mutex the calling thread
-does not own the mutex.
-*Effects:* Constructs an object of type `unique_lock` and calls
-`m.lock()`.
-*Postconditions:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 unique_lock(mutex_type& m, defer_lock_t) noexcept;
 ```
-*Effects:* Constructs an object of type `unique_lock`.
-*Postconditions:* `pm == addressof(m)` and `owns == false`.
 ``` cpp
 unique_lock(mutex_type& m, try_to_lock_t);
 ```
-*Requires:* The supplied `Mutex` type shall meet the `Lockable`
-requirements ([[thread.req.lockable.req]]). If `mutex_type` is not a
 recursive mutex the calling thread does not own the mutex.
-*Effects:* Constructs an object of type `unique_lock` and calls
-`m.try_lock()`.
-*Postconditions:* `pm == addressof(m)` and `owns == res`, where `res` is
-the value returned by the call to `m.try_lock()`.
 ``` cpp
 unique_lock(mutex_type& m, adopt_lock_t);
 ```
-*Requires:* The calling thread owns the mutex.
-*Effects:* Constructs an object of type `unique_lock`.
-*Postconditions:* `pm == addressof(m)` and `owns == true`.
 *Throws:* Nothing.
 ``` cpp
 template<class Clock, class Duration>
   unique_lock(mutex_type& m, const chrono::time_point<Clock, Duration>& abs_time);
 ```
-*Requires:* If `mutex_type` is not a recursive mutex the calling thread
-does not own the mutex. The supplied `Mutex` type shall meet the
-`TimedLockable` requirements ([[thread.req.lockable.timed]]).
-*Effects:* Constructs an object of type `unique_lock` and calls
-`m.try_lock_until(abs_time)`.
-*Postconditions:* `pm == addressof(m)` and `owns == res`, where `res` is
-the value returned by the call to `m.try_lock_until(abs_time)`.
 ``` cpp
 template<class Rep, class Period>
   unique_lock(mutex_type& m, const chrono::duration<Rep, Period>& rel_time);
 ```
-*Requires:* If `mutex_type` is not a recursive mutex the calling thread
-does not own the mutex. The supplied `Mutex` type shall meet the
-`TimedLockable` requirements ([[thread.req.lockable.timed]]).
-*Effects:* Constructs an object of type `unique_lock` and calls
-`m.try_lock_for(rel_time)`.
-*Postconditions:* `pm == addressof(m)` and `owns == res`, where `res` is
-the value returned by the call to `m.try_lock_for(rel_time)`.
 ``` cpp
 unique_lock(unique_lock&& u) noexcept;
 ```
-*Postconditions:* `pm == u_p.pm` and `owns == u_p.owns` (where `u_p` is
-the state of `u` just prior to this construction), `u.pm == 0` and
 `u.owns == false`.
 ``` cpp
 unique_lock& operator=(unique_lock&& u);
 ```
 *Effects:* If `owns` calls `pm->unlock()`.
-*Postconditions:* `pm == u_p.pm` and `owns == u_p.owns` (where `u_p` is
-the state of `u` just prior to this construction), `u.pm == 0` and
 `u.owns == false`.
 [*Note 1*: With a recursive mutex it is possible for both `*this` and
 `u` to own the same mutex before the assignment. In this case, `*this`
 will own the mutex after the assignment and `u` will not. — *end note*]
@@ -343,44 +324,44 @@ will own the mutex after the assignment and `u` will not. — *end note*]
 ~unique_lock();
 ```
 *Effects:* If `owns` calls `pm->unlock()`.
-##### `unique_lock` locking <a id="thread.lock.unique.locking">[[thread.lock.unique.locking]]</a>
 ``` cpp
 void lock();
 ```
 *Effects:* As if by `pm->lock()`.
-*Postconditions:* `owns == true`.
 *Throws:* Any exception thrown by `pm->lock()`. `system_error` when an
-exception is required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 bool try_lock();
 ```
-*Requires:* The supplied `Mutex` shall meet the `Lockable`
-requirements ([[thread.req.lockable.req]]).
 *Effects:* As if by `pm->try_lock()`.
 *Returns:* The value returned by the call to `try_lock()`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `try_lock()`.
 *Throws:* Any exception thrown by `pm->try_lock()`. `system_error` when
-an exception is required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -388,22 +369,22 @@ an exception is required ([[thread.req.exception]]).
 ``` cpp
 template<class Clock, class Duration>
   bool try_lock_until(const chrono::time_point<Clock, Duration>& abs_time);
 ```
-*Requires:* The supplied `Mutex` type shall meet the `TimedLockable`
-requirements ([[thread.req.lockable.timed]]).
 *Effects:* As if by `pm->try_lock_until(abs_time)`.
 *Returns:* The value returned by the call to `try_lock_until(abs_time)`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `try_lock_until(abs_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_until()`. `system_error`
-when an exception is required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -411,22 +392,22 @@ when an exception is required ([[thread.req.exception]]).
 ``` cpp
 template<class Rep, class Period>
   bool try_lock_for(const chrono::duration<Rep, Period>& rel_time);
 ```
-*Requires:* The supplied `Mutex` type shall meet the `TimedLockable`
-requirements ([[thread.req.lockable.timed]]).
 *Effects:* As if by `pm->try_lock_for(rel_time)`.
-*Returns:* The value returned by the call to `try_lock_until(rel_time)`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `try_lock_for(rel_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_for()`. `system_error`
-when an exception is required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -435,20 +416,20 @@ when an exception is required ([[thread.req.exception]]).
 void unlock();
 ```
 *Effects:* As if by `pm->unlock()`.
-*Postconditions:* `owns == false`.
 *Throws:* `system_error` when an exception is
-required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if on entry `owns` is `false`.
-##### `unique_lock` modifiers <a id="thread.lock.unique.mod">[[thread.lock.unique.mod]]</a>
 ``` cpp
 void swap(unique_lock& u) noexcept;
 ```
@@ -458,20 +439,20 @@ void swap(unique_lock& u) noexcept;
 mutex_type* release() noexcept;
 ```
 *Returns:* The previous value of `pm`.
-*Postconditions:* `pm == 0` and `owns == false`.
 ``` cpp
 template<class Mutex>
   void swap(unique_lock<Mutex>& x, unique_lock<Mutex>& y) noexcept;
 ```
 *Effects:* As if by `x.swap(y)`.
-##### `unique_lock` observers <a id="thread.lock.unique.obs">[[thread.lock.unique.obs]]</a>
 ``` cpp
 bool owns_lock() const noexcept;
 ```
@@ -503,15 +484,13 @@ namespace std {
     explicit shared_lock(mutex_type& m);        // blocking
     shared_lock(mutex_type& m, defer_lock_t) noexcept;
     shared_lock(mutex_type& m, try_to_lock_t);
     shared_lock(mutex_type& m, adopt_lock_t);
     template<class Clock, class Duration>
-      shared_lock(mutex_type& m,
-                  const chrono::time_point<Clock, Duration>& abs_time);
     template<class Rep, class Period>
-      shared_lock(mutex_type& m,
-                const chrono::duration<Rep, Period>& rel_time);
     ~shared_lock();
     shared_lock(const shared_lock&) = delete;
     shared_lock& operator=(const shared_lock&) = delete;
@@ -539,12 +518,10 @@ namespace std {
   private:
     mutex_type* pm;                             // exposition only
     bool owns;                                  // exposition only
   };
-  template<class Mutex> shared_lock(shared_lock<Mutex>) -> shared_lock<Mutex>;
   template<class Mutex>
     void swap(shared_lock<Mutex>& x, shared_lock<Mutex>& y) noexcept;
 }
 ```
@@ -553,99 +530,89 @@ lockable object within a scope. Shared ownership of the lockable object
 may be acquired at construction or after construction, and may be
 transferred, after acquisition, to another `shared_lock` object. Objects
 of type `shared_lock` are not copyable but are movable. The behavior of
 a program is undefined if the contained pointer `pm` is not null and the
 lockable object pointed to by `pm` does not exist for the entire
-remaining lifetime ([[basic.life]]) of the `shared_lock` object. The
-supplied `Mutex` type shall meet the shared mutex requirements (
-[[thread.sharedtimedmutex.requirements]]).
-[*Note 1*: `shared_lock<Mutex>` meets the `TimedLockable`
-requirements ([[thread.req.lockable.timed]]). — *end note*]
-##### `shared_lock` constructors, destructor, and assignment <a id="thread.lock.shared.cons">[[thread.lock.shared.cons]]</a>
 ``` cpp
 shared_lock() noexcept;
 ```
-*Effects:* Constructs an object of type `shared_lock`.
-*Postconditions:* `pm == nullptr` and `owns == false`.
 ``` cpp
 explicit shared_lock(mutex_type& m);
 ```
-*Requires:* The calling thread does not own the mutex for any ownership
-mode.
-*Effects:* Constructs an object of type `shared_lock` and calls
-`m.lock_shared()`.
-*Postconditions:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 shared_lock(mutex_type& m, defer_lock_t) noexcept;
 ```
-*Effects:* Constructs an object of type `shared_lock`.
-*Postconditions:* `pm == addressof(m)` and `owns == false`.
 ``` cpp
 shared_lock(mutex_type& m, try_to_lock_t);
 ```
-*Requires:* The calling thread does not own the mutex for any ownership
-mode.
-*Effects:* Constructs an object of type `shared_lock` and calls
-`m.try_lock_shared()`.
-*Postconditions:* `pm == addressof(m)` and `owns == res` where `res` is
-the value returned by the call to `m.try_lock_shared()`.
 ``` cpp
 shared_lock(mutex_type& m, adopt_lock_t);
 ```
-*Requires:* The calling thread has shared ownership of the mutex.
-*Effects:* Constructs an object of type `shared_lock`.
-*Postconditions:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 template<class Clock, class Duration>
   shared_lock(mutex_type& m,
               const chrono::time_point<Clock, Duration>& abs_time);
 ```
-*Requires:* The calling thread does not own the mutex for any ownership
-mode.
-*Effects:* Constructs an object of type `shared_lock` and calls
-`m.try_lock_shared_until(abs_time)`.
-*Postconditions:* `pm == addressof(m)` and `owns == res` where `res` is
-the value returned by the call to `m.try_lock_shared_until(abs_time)`.
 ``` cpp
 template<class Rep, class Period>
   shared_lock(mutex_type& m,
               const chrono::duration<Rep, Period>& rel_time);
 ```
-*Requires:* The calling thread does not own the mutex for any ownership
-mode.
-*Effects:* Constructs an object of type `shared_lock` and calls
-`m.try_lock_shared_for(rel_time)`.
-*Postconditions:* `pm == addressof(m)` and `owns == res` where `res` is
-the value returned by the call to `m.try_lock_shared_for(rel_time)`.
 ``` cpp
 ~shared_lock();
 ```
@@ -653,36 +620,36 @@ the value returned by the call to `m.try_lock_shared_for(rel_time)`.
 ``` cpp
 shared_lock(shared_lock&& sl) noexcept;
 ```
-*Postconditions:* `pm == sl_p.pm` and `owns == sl_p.owns` (where `sl_p`
-is the state of `sl` just prior to this construction),
-`sl.pm == nullptr` and `sl.owns == false`.
 ``` cpp
 shared_lock& operator=(shared_lock&& sl) noexcept;
 ```
 *Effects:* If `owns` calls `pm->unlock_shared()`.
-*Postconditions:* `pm == sl_p.pm` and `owns == sl_p.owns` (where `sl_p`
-is the state of `sl` just prior to this assignment), `sl.pm == nullptr`
-and `sl.owns == false`.
-##### `shared_lock` locking <a id="thread.lock.shared.locking">[[thread.lock.shared.locking]]</a>
 ``` cpp
 void lock();
 ```
 *Effects:* As if by `pm->lock_shared()`.
-*Postconditions:* `owns == true`.
 *Throws:* Any exception thrown by `pm->lock_shared()`. `system_error`
-when an exception is required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -693,39 +660,36 @@ bool try_lock();
 *Effects:* As if by `pm->try_lock_shared()`.
 *Returns:* The value returned by the call to `pm->try_lock_shared()`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `pm->try_lock_shared()`.
 *Throws:* Any exception thrown by `pm->try_lock_shared()`.
-`system_error` when an exception is
-required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 template<class Clock, class Duration>
-  bool
-  try_lock_until(const chrono::time_point<Clock, Duration>& abs_time);
 ```
 *Effects:* As if by `pm->try_lock_shared_until(abs_time)`.
 *Returns:* The value returned by the call to
 `pm->try_lock_shared_until(abs_time)`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `pm->try_lock_shared_until(abs_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_shared_until(abs_time)`.
-`system_error` when an exception is
-required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -738,16 +702,15 @@ template <class Rep, class Period>
 *Effects:* As if by `pm->try_lock_shared_for(rel_time)`.
 *Returns:* The value returned by the call to
 `pm->try_lock_shared_for(rel_time)`.
-*Postconditions:* `owns == res`, where `res` is the value returned by
-the call to `pm->try_lock_shared_for(rel_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_shared_for(rel_time)`.
-`system_error` when an exception is
-required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
@@ -756,20 +719,20 @@ required ([[thread.req.exception]]).
 void unlock();
 ```
 *Effects:* As if by `pm->unlock_shared()`.
-*Postconditions:* `owns == false`.
 *Throws:* `system_error` when an exception is
-required ([[thread.req.exception]]).
 *Error conditions:*
 - `operation_not_permitted` — if on entry `owns` is `false`.
-##### `shared_lock` modifiers <a id="thread.lock.shared.mod">[[thread.lock.shared.mod]]</a>
 ``` cpp
 void swap(shared_lock& sl) noexcept;
 ```
@@ -779,20 +742,20 @@ void swap(shared_lock& sl) noexcept;
 mutex_type* release() noexcept;
 ```
 *Returns:* The previous value of `pm`.
-*Postconditions:* `pm == nullptr` and `owns == false`.
 ``` cpp
 template<class Mutex>
   void swap(shared_lock<Mutex>& x, shared_lock<Mutex>& y) noexcept;
 ```
 *Effects:* As if by `x.swap(y)`.
-##### `shared_lock` observers <a id="thread.lock.shared.obs">[[thread.lock.shared.obs]]</a>
 ``` cpp
 bool owns_lock() const noexcept;
 ```

     lock_guard& operator=(const lock_guard&) = delete;
   private:
     mutex_type& pm;             // exposition only
   };
 }
 ```
 An object of type `lock_guard` controls the ownership of a lockable
 object within a scope. A `lock_guard` object maintains ownership of a
+lockable object throughout the `lock_guard` object’s lifetime
+[[basic.life]]. The behavior of a program is undefined if the lockable
 object referenced by `pm` does not exist for the entire lifetime of the
 `lock_guard` object. The supplied `Mutex` type shall meet the
+*Cpp17BasicLockable* requirements [[thread.req.lockable.basic]].
 ``` cpp
 explicit lock_guard(mutex_type& m);
 ```
+*Preconditions:* If `mutex_type` is not a recursive mutex, the calling
+thread does not own the mutex `m`.
+*Effects:* Initializes `pm` with `m`. Calls `m.lock()`.
 ``` cpp
 lock_guard(mutex_type& m, adopt_lock_t);
 ```
+*Preconditions:* The calling thread owns the mutex `m`.
+*Effects:* Initializes `pm` with `m`.
 *Throws:* Nothing.
 ``` cpp
 ~lock_guard();
   class scoped_lock {
   public:
     using mutex_type = Mutex;   // If MutexTypes... consists of the single type Mutex
     explicit scoped_lock(MutexTypes&... m);
+    explicit scoped_lock(adopt_lock_t, MutexTypes&... m);
     ~scoped_lock();
     scoped_lock(const scoped_lock&) = delete;
     scoped_lock& operator=(const scoped_lock&) = delete;
   private:
     tuple<MutexTypes&...> pm;   // exposition only
   };
 }
 ```
 An object of type `scoped_lock` controls the ownership of lockable
 objects within a scope. A `scoped_lock` object maintains ownership of
+lockable objects throughout the `scoped_lock` object’s lifetime
+[[basic.life]]. The behavior of a program is undefined if the lockable
 objects referenced by `pm` do not exist for the entire lifetime of the
 `scoped_lock` object. When `sizeof...(MutexTypes)` is `1`, the supplied
+`Mutex` type shall meet the *Cpp17BasicLockable* requirements
+[[thread.req.lockable.basic]]. Otherwise, each of the mutex types shall
+meet the *Cpp17Lockable* requirements [[thread.req.lockable.req]].
 ``` cpp
 explicit scoped_lock(MutexTypes&... m);
 ```
+*Preconditions:* If a `MutexTypes` type is not a recursive mutex, the
+calling thread does not own the corresponding mutex element of `m`.
 *Effects:* Initializes `pm` with `tie(m...)`. Then if
 `sizeof...(MutexTypes)` is `0`, no effects. Otherwise if
 `sizeof...(MutexTypes)` is `1`, then `m.lock()`. Otherwise,
 `lock(m...)`.
 ``` cpp
+explicit scoped_lock(adopt_lock_t, MutexTypes&... m);
 ```
+*Preconditions:* The calling thread owns all the mutexes in `m`.
 *Effects:* Initializes `pm` with `tie(m...)`.
 *Throws:* Nothing.
   private:
     mutex_type* pm;             // exposition only
     bool owns;                  // exposition only
   };
   template<class Mutex>
     void swap(unique_lock<Mutex>& x, unique_lock<Mutex>& y) noexcept;
 }
 ```
 at construction or after construction, and may be transferred, after
 acquisition, to another `unique_lock` object. Objects of type
 `unique_lock` are not copyable but are movable. The behavior of a
 program is undefined if the contained pointer `pm` is not null and the
 lockable object pointed to by `pm` does not exist for the entire
+remaining lifetime [[basic.life]] of the `unique_lock` object. The
+supplied `Mutex` type shall meet the *Cpp17BasicLockable* requirements
+[[thread.req.lockable.basic]].
+[*Note 1*: `unique_lock<Mutex>` meets the *Cpp17BasicLockable*
+requirements. If `Mutex` meets the *Cpp17Lockable* requirements
+[[thread.req.lockable.req]], `unique_lock<Mutex>` also meets the
+*Cpp17Lockable* requirements; if `Mutex` meets the *Cpp17TimedLockable*
+requirements [[thread.req.lockable.timed]], `unique_lock<Mutex>` also
+meets the *Cpp17TimedLockable* requirements. — *end note*]
+##### Constructors, destructor, and assignment <a id="thread.lock.unique.cons">[[thread.lock.unique.cons]]</a>
 ``` cpp
 unique_lock() noexcept;
 ```
+*Ensures:* `pm == 0` and `owns == false`.
 ``` cpp
 explicit unique_lock(mutex_type& m);
 ```
+*Preconditions:* If `mutex_type` is not a recursive mutex the calling
+thread does not own the mutex.
+*Effects:* Calls `m.lock()`.
+*Ensures:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 unique_lock(mutex_type& m, defer_lock_t) noexcept;
 ```
+*Ensures:* `pm == addressof(m)` and `owns == false`.
 ``` cpp
 unique_lock(mutex_type& m, try_to_lock_t);
 ```
+*Preconditions:* The supplied `Mutex` type meets the *Cpp17Lockable*
+requirements [[thread.req.lockable.req]]. If `mutex_type` is not a
 recursive mutex the calling thread does not own the mutex.
+*Effects:* Calls `m.try_lock()`.
+*Ensures:* `pm == addressof(m)` and `owns == res`, where `res` is the
+value returned by the call to `m.try_lock()`.
 ``` cpp
 unique_lock(mutex_type& m, adopt_lock_t);
 ```
+*Preconditions:* The calling thread owns the mutex.
+*Ensures:* `pm == addressof(m)` and `owns == true`.
 *Throws:* Nothing.
 ``` cpp
 template<class Clock, class Duration>
   unique_lock(mutex_type& m, const chrono::time_point<Clock, Duration>& abs_time);
 ```
+*Preconditions:* If `mutex_type` is not a recursive mutex the calling
+thread does not own the mutex. The supplied `Mutex` type meets the
+*Cpp17TimedLockable* requirements [[thread.req.lockable.timed]].
+*Effects:* Calls `m.try_lock_until(abs_time)`.
+*Ensures:* `pm == addressof(m)` and `owns == res`, where `res` is the
+value returned by the call to `m.try_lock_until(abs_time)`.
 ``` cpp
 template<class Rep, class Period>
   unique_lock(mutex_type& m, const chrono::duration<Rep, Period>& rel_time);
 ```
+*Preconditions:* If `mutex_type` is not a recursive mutex the calling
+thread does not own the mutex. The supplied `Mutex` type meets the
+*Cpp17TimedLockable* requirements [[thread.req.lockable.timed]].
+*Effects:* Calls `m.try_lock_for(rel_time)`.
+*Ensures:* `pm == addressof(m)` and `owns == res`, where `res` is the
+value returned by the call to `m.try_lock_for(rel_time)`.
 ``` cpp
 unique_lock(unique_lock&& u) noexcept;
 ```
+*Ensures:* `pm == u_p.pm` and `owns == u_p.owns` (where `u_p` is the
+state of `u` just prior to this construction), `u.pm == 0` and
 `u.owns == false`.
 ``` cpp
 unique_lock& operator=(unique_lock&& u);
 ```
 *Effects:* If `owns` calls `pm->unlock()`.
+*Ensures:* `pm == u_p.pm` and `owns == u_p.owns` (where `u_p` is the
+state of `u` just prior to this construction), `u.pm == 0` and
 `u.owns == false`.
 [*Note 1*: With a recursive mutex it is possible for both `*this` and
 `u` to own the same mutex before the assignment. In this case, `*this`
 will own the mutex after the assignment and `u` will not. — *end note*]
 ~unique_lock();
 ```
 *Effects:* If `owns` calls `pm->unlock()`.
+##### Locking <a id="thread.lock.unique.locking">[[thread.lock.unique.locking]]</a>
 ``` cpp
 void lock();
 ```
 *Effects:* As if by `pm->lock()`.
+*Ensures:* `owns == true`.
 *Throws:* Any exception thrown by `pm->lock()`. `system_error` when an
+exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 bool try_lock();
 ```
+*Preconditions:* The supplied `Mutex` meets the *Cpp17Lockable*
+requirements [[thread.req.lockable.req]].
 *Effects:* As if by `pm->try_lock()`.
 *Returns:* The value returned by the call to `try_lock()`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `try_lock()`.
 *Throws:* Any exception thrown by `pm->try_lock()`. `system_error` when
+an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 template<class Clock, class Duration>
   bool try_lock_until(const chrono::time_point<Clock, Duration>& abs_time);
 ```
+*Preconditions:* The supplied `Mutex` type meets the
+*Cpp17TimedLockable* requirements [[thread.req.lockable.timed]].
 *Effects:* As if by `pm->try_lock_until(abs_time)`.
 *Returns:* The value returned by the call to `try_lock_until(abs_time)`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `try_lock_until(abs_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_until()`. `system_error`
+when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 template<class Rep, class Period>
   bool try_lock_for(const chrono::duration<Rep, Period>& rel_time);
 ```
+*Preconditions:* The supplied `Mutex` type meets the
+*Cpp17TimedLockable* requirements [[thread.req.lockable.timed]].
 *Effects:* As if by `pm->try_lock_for(rel_time)`.
+*Returns:* The value returned by the call to `try_lock_for(rel_time)`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `try_lock_for(rel_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_for()`. `system_error`
+when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 void unlock();
 ```
 *Effects:* As if by `pm->unlock()`.
+*Ensures:* `owns == false`.
 *Throws:* `system_error` when an exception is
+required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if on entry `owns` is `false`.
+##### Modifiers <a id="thread.lock.unique.mod">[[thread.lock.unique.mod]]</a>
 ``` cpp
 void swap(unique_lock& u) noexcept;
 ```
 mutex_type* release() noexcept;
 ```
 *Returns:* The previous value of `pm`.
+*Ensures:* `pm == 0` and `owns == false`.
 ``` cpp
 template<class Mutex>
   void swap(unique_lock<Mutex>& x, unique_lock<Mutex>& y) noexcept;
 ```
 *Effects:* As if by `x.swap(y)`.
+##### Observers <a id="thread.lock.unique.obs">[[thread.lock.unique.obs]]</a>
 ``` cpp
 bool owns_lock() const noexcept;
 ```
     explicit shared_lock(mutex_type& m);        // blocking
     shared_lock(mutex_type& m, defer_lock_t) noexcept;
     shared_lock(mutex_type& m, try_to_lock_t);
     shared_lock(mutex_type& m, adopt_lock_t);
     template<class Clock, class Duration>
+      shared_lock(mutex_type& m, const chrono::time_point<Clock, Duration>& abs_time);
     template<class Rep, class Period>
+      shared_lock(mutex_type& m, const chrono::duration<Rep, Period>& rel_time);
     ~shared_lock();
     shared_lock(const shared_lock&) = delete;
     shared_lock& operator=(const shared_lock&) = delete;
   private:
     mutex_type* pm;                             // exposition only
     bool owns;                                  // exposition only
   };
   template<class Mutex>
     void swap(shared_lock<Mutex>& x, shared_lock<Mutex>& y) noexcept;
 }
 ```
 may be acquired at construction or after construction, and may be
 transferred, after acquisition, to another `shared_lock` object. Objects
 of type `shared_lock` are not copyable but are movable. The behavior of
 a program is undefined if the contained pointer `pm` is not null and the
 lockable object pointed to by `pm` does not exist for the entire
+remaining lifetime [[basic.life]] of the `shared_lock` object. The
+supplied `Mutex` type shall meet the shared mutex requirements
+[[thread.sharedtimedmutex.requirements]].
+[*Note 1*: `shared_lock<Mutex>` meets the *Cpp17TimedLockable*
+requirements [[thread.req.lockable.timed]]. — *end note*]
+##### Constructors, destructor, and assignment <a id="thread.lock.shared.cons">[[thread.lock.shared.cons]]</a>
 ``` cpp
 shared_lock() noexcept;
 ```
+*Ensures:* `pm == nullptr` and `owns == false`.
 ``` cpp
 explicit shared_lock(mutex_type& m);
 ```
+*Preconditions:* The calling thread does not own the mutex for any
+ownership mode.
+*Effects:* Calls `m.lock_shared()`.
+*Ensures:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 shared_lock(mutex_type& m, defer_lock_t) noexcept;
 ```
+*Ensures:* `pm == addressof(m)` and `owns == false`.
 ``` cpp
 shared_lock(mutex_type& m, try_to_lock_t);
 ```
+*Preconditions:* The calling thread does not own the mutex for any
+ownership mode.
+*Effects:* Calls `m.try_lock_shared()`.
+*Ensures:* `pm == addressof(m)` and `owns == res` where `res` is the
+value returned by the call to `m.try_lock_shared()`.
 ``` cpp
 shared_lock(mutex_type& m, adopt_lock_t);
 ```
+*Preconditions:* The calling thread has shared ownership of the mutex.
+*Ensures:* `pm == addressof(m)` and `owns == true`.
 ``` cpp
 template<class Clock, class Duration>
   shared_lock(mutex_type& m,
               const chrono::time_point<Clock, Duration>& abs_time);
 ```
+*Preconditions:* The calling thread does not own the mutex for any
+ownership mode.
+*Effects:* Calls `m.try_lock_shared_until(abs_time)`.
+*Ensures:* `pm == addressof(m)` and `owns == res` where `res` is the
+value returned by the call to `m.try_lock_shared_until(abs_time)`.
 ``` cpp
 template<class Rep, class Period>
   shared_lock(mutex_type& m,
               const chrono::duration<Rep, Period>& rel_time);
 ```
+*Preconditions:* The calling thread does not own the mutex for any
+ownership mode.
+*Effects:* Calls `m.try_lock_shared_for(rel_time)`.
+*Ensures:* `pm == addressof(m)` and `owns == res` where `res` is the
+value returned by the call to `m.try_lock_shared_for(rel_time)`.
 ``` cpp
 ~shared_lock();
 ```
 ``` cpp
 shared_lock(shared_lock&& sl) noexcept;
 ```
+*Ensures:* `pm == sl_p.pm` and `owns == sl_p.owns` (where `sl_p` is the
+state of `sl` just prior to this construction), `sl.pm == nullptr` and
+`sl.owns == false`.
 ``` cpp
 shared_lock& operator=(shared_lock&& sl) noexcept;
 ```
 *Effects:* If `owns` calls `pm->unlock_shared()`.
+*Ensures:* `pm == sl_p.pm` and `owns == sl_p.owns` (where `sl_p` is the
+state of `sl` just prior to this assignment), `sl.pm == nullptr` and
+`sl.owns == false`.
+##### Locking <a id="thread.lock.shared.locking">[[thread.lock.shared.locking]]</a>
 ``` cpp
 void lock();
 ```
 *Effects:* As if by `pm->lock_shared()`.
+*Ensures:* `owns == true`.
 *Throws:* Any exception thrown by `pm->lock_shared()`. `system_error`
+when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 *Effects:* As if by `pm->try_lock_shared()`.
 *Returns:* The value returned by the call to `pm->try_lock_shared()`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `pm->try_lock_shared()`.
 *Throws:* Any exception thrown by `pm->try_lock_shared()`.
+`system_error` when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 ``` cpp
 template<class Clock, class Duration>
+  bool try_lock_until(const chrono::time_point<Clock, Duration>& abs_time);
 ```
 *Effects:* As if by `pm->try_lock_shared_until(abs_time)`.
 *Returns:* The value returned by the call to
 `pm->try_lock_shared_until(abs_time)`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `pm->try_lock_shared_until(abs_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_shared_until(abs_time)`.
+`system_error` when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 *Effects:* As if by `pm->try_lock_shared_for(rel_time)`.
 *Returns:* The value returned by the call to
 `pm->try_lock_shared_for(rel_time)`.
+*Ensures:* `owns == res`, where `res` is the value returned by the call
+to `pm->try_lock_shared_for(rel_time)`.
 *Throws:* Any exception thrown by `pm->try_lock_shared_for(rel_time)`.
+`system_error` when an exception is required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if `pm` is `nullptr`.
 - `resource_deadlock_would_occur` — if on entry `owns` is `true`.
 void unlock();
 ```
 *Effects:* As if by `pm->unlock_shared()`.
+*Ensures:* `owns == false`.
 *Throws:* `system_error` when an exception is
+required [[thread.req.exception]].
 *Error conditions:*
 - `operation_not_permitted` — if on entry `owns` is `false`.
+##### Modifiers <a id="thread.lock.shared.mod">[[thread.lock.shared.mod]]</a>
 ``` cpp
 void swap(shared_lock& sl) noexcept;
 ```
 mutex_type* release() noexcept;
 ```
 *Returns:* The previous value of `pm`.
+*Ensures:* `pm == nullptr` and `owns == false`.
 ``` cpp
 template<class Mutex>
   void swap(shared_lock<Mutex>& x, shared_lock<Mutex>& y) noexcept;
 ```
 *Effects:* As if by `x.swap(y)`.
+##### Observers <a id="thread.lock.shared.obs">[[thread.lock.shared.obs]]</a>
 ``` cpp
 bool owns_lock() const noexcept;
 ```

Diff to HTML by rtfpessoa