Properly specify the interaction of library calls for mutexes

Jens Gustedt, INRIA and ICube, France

2025年10月07日

target

integration into IS ISO/IEC 9899:202y

document history

C document ID: C4242

document number	date	comment
n3672	202507	Original proposal
n3708	202510	better single out the different atomic operations
integrate feedback from the reflector

license

CC BY, see https://creativecommons.org/licenses/by/4.0

1 Motivation

This paper draws part of its motivation from n3655

‘’Make implicit undefined behaviour in mtx_destroy() explicit’’,

and could either replace the solutions proposed there or be constructed on top of it. When discussing that paper on the reflector it became quickly apparent, that not only the undefined behavior is currently poorly described, but that the description also lacks a proper integration into C11’s model of inter-thread time.

For example, the "General" section unspecifically indicate that lock and unlock "behave as atomic operation" and "in some particular order" without properly relating to the terminology that is developed for atomic objects. In particular a simple mapping of a lock operation as one single atomic operation is not sensible: because a thread that enters a lock operation can be blocked for an indeterminate amount of time, the entry into a call and the return from the call have to represent two separate events in the modification order of the mutex:

• The entry into a call already changes the behavior of the execution, even if the call did not yet return.
• Only if the return from a call to a lock operation acknowledges "success" the behavior might also change.

The only sensible way to provide this integration is to add mutexes to the set of atomic types, but much as atomic_flag that this type then has only atomic operations and an internal state that is not observable directly.

So, here we distinguish the following atomic modifications in the modification order of a mutex:

• an entry into a call to a lock operation (memory_order_relaxed),
• a successful return from a call to a lock operation (memory_order_acquire),
• an unsuccessful return from a call to a lock operation (memory_order_relaxed),
• an unlock operation (memory_order_release).

Additions by this paper here are:

• A proper integration of the mutex type into the atomicity, synchronization and timing terminologies that were introduced by C11.
• Bookkeeping of Annex J .2.

2 Wording

Replace the whole clause 7.30.4.1, General,

1 (削除) For purposes of determining the existence of a data race, lock and unlock operations behave as atomic operations. All lock and unlock operations on a particular mutex occur in some particular total order. (削除ここまで)

(削除) 2 NOTE This total order can be viewed as the modification order of the mutex. (削除ここまで)

by

(追記) 1 A mutex is an atomic object that implements specific operations corresponding to calls to the functions as described in this subclause. It has two states, locked and unlocked,^FTN0) that are only observable by the behavior of the operations associated with the type. The atomic operations are described by lock (mtx_lock, mtx_timedlock, mtx_trylock) and unlock (mtx_unlock) operations that operate on this state. The entry to a lock operation and the return from it are two distinct atomic modifications in the modification order of the mutex, lock-entry and lock-return. Unless the function return value is thrd_error, the calling thread is suspended between the lock-entry and the lock-return events performed during a mtx_lock or mtx_timedlock operation; after writing the lock-entry the calling thread is said to be blocked, the writing of lock-return is said to unblock the calling thread. (追記ここまで)

(追記) ^FTN0) If the mutex is recursive, a given mutex can be locked several times by the same thread. (追記ここまで)

(追記) 2 The lock-return of a successful lock operation and any unlock operation are synchronization operations with respect to the atomic mutex object; they have memory_order_acquire and memory_order_release semantics, respectively. A lock-entry and the lock-return from an operation that is unsuccessful have a memory order that is at least as strong as memory_order_relaxed. In addition to the atomic operations, there are the mtx_init and mtx_destroy operations as well as modifications of the object representation^FTN1) that also are modifications in the modification order of a mutex. (追記ここまで)

(追記) ^FTN1) These include for example a copy operation of a structure type that has a mtx_t member. (追記ここまで)

(追記) 3 A mutex that is not initialized by mtx_init, or whose last operation has been a mtx_destroy operation, or such that its object representation has been modified directly, has an indeterminate representation; performing any operation other than mtx_init on such a mutex has undefined behavior. (追記ここまで)

(追記) 4 As the consequence of a mtx_init operation the state of the mutex is unlocked, and, for any thread, the first subsequent modification in the modification order shall be a lock-entry or a mtx_destroy operation. (追記ここまで)

(追記) 5 Before a mtx_destroy operation the state of the mutex shall be unlocked, and, for any thread, the last preceding modification in the modification order shall not be the entry to a lock operation; similar requirements hold for a mutex that is not in an indeterminate state and to which a direct modification of the object representation is applied. (追記ここまで)

(追記) 6 NOTE That means that if a thread is suspended to acquire the lock of a mutex and another thread concurrently calls mtx_destroy on that same mutex, the behavior is undefined. Similarly, if a thread holds a lock on a mutex and the same or another thread concurrently calls mtx_destroy on that same mutex, the behavior is undefined. (追記ここまで)

...

7.30.4.2 The mtx_destroy function

...

Transform the second sentence into a note.

2 The mtx_destroy function releases any resources used by the mutex pointed to by mtx.

(追記) 3 NOTE In an execution that respects the requirements (7.30.4.1) for the modification order, the mutex is initialized prior to a call to mtx_destroy and (追記ここまで) no threads (削除) can be (削除ここまで) (追記) are (追記ここまで) blocked waiting (削除) for (削除ここまで) (追記) to acquire the lock of (追記ここまで) the mutex pointed to by mtx.

...

7.30.4.3 The mtx_init function

...

3 If the mtx_init function succeeds, it sets the mutex pointed to by mtx to a (削除) value (削除ここまで) (追記) valid representation (追記ここまで) that uniquely identifies the newly created mutex (追記) and that corresponds to the unlocked state (追記ここまで).

Returns

4 The mtx_init function returns thrd_success on success, or thrd_error (削除) if the request could not be honored (削除ここまで) (追記) otherwise.

7.30.4.4 The mtx_lock function

...

Returns

3 The mtx_lock function returns thrd_success on success (追記ここまで) (追記) if the mutex has been successfully locked by the calling thread (追記ここまで), or thrd_error (削除) if the request could not be honored (削除ここまで) (追記) otherwise (追記ここまで).

...

7.30.4.5 The mtx_timedlock function

...

Returns

3 The mtx_timedlock function returns thrd_success (削除) on success (削除ここまで) (追記) if the mutex has been successfully locked by the calling thread (追記ここまで), or (追記) otherwise (追記ここまで) thrd_timedout if the time specified was reached (削除) without acquiring the requested resource (削除ここまで), or thrd_error (削除) if the request could not be honored (削除ここまで) (追記) otherwise (追記ここまで).

...

7.30.4.6 The mtx_trylock function

...

Returns

3 The mtx_trylock function returns thrd_success (削除) on success (削除ここまで) (追記) if the mutex has been successfully locked by the calling thread (追記ここまで), or (追記) otherwise (追記ここまで) thrd_busy if (削除) the resource requested is already in use (削除ここまで) (追記) the mutex is in a valid state but could not be locked (追記ここまで), or thrd_error (削除) if the request could not be honored (削除ここまで) (追記) otherwise (追記ここまで).

Split the last sentence off and make it a note.

(追記) 4 NOTE (追記ここまで) mtx_trylock can spuriously fail to lock (削除) an unused resource (削除ここまで) (追記) an unlocked but otherwise valid mutex (追記ここまで), in which case it returns thrd_busy.

...

7.30.4.7 The mtx_unlock function

...

Returns

4 The mtx_unlock function returns thrd_success on success, or thrd_error (削除) if the request could not be honored (削除ここまで) (追記) otherwise.

...

Annex J .2 Undefined behavior

(181c) An operation other than a call to mtx_init is performed on a mutex that has an indeterminate representation (7.30.4.1). (追記ここまで)

(追記) (181d) For any thread the last operation on a mutex M has been the entry to a lock operation when another thread issues a call to mtx_destroy with M, or modifies the object representation of M directly (7.30.4.1). (追記ここまで)

(追記) (181e) For any thread the last operation on a mutex M has been the return from a successful lock operation when the same or any other thread issues a call to mtx_destroy with M, or modifies the object representation of M directly (7.30.4.1). (追記ここまで)

(追記) (181f) For any thread the first atomic operation on the mutex passed to a call to mtx_init is not the entry to a call to a lock operation (7.30.4.1). (追記ここまで)

3 Note to the editors

The changes here add mtx_t to the notion of atomic types. If n3706 is accepted into C2Y (there should be an online vote for inclusion before the end of 2025) the list of atomic types that are exempted from the generic atomic operations (7.17.7.2) should be amended with mtx_t.

... that operate on all atomic types other than atomic_flag (追記) and mtx_t (追記ここまで)

Acknowledgment

Thanks to Dave Banham, Hans Boehm and Joseph Myers for discussions and suggestions for improvements.