Properly specify the interaction of library calls for mutexes

Jens Gustedt, INRIA and ICube, France

2025-07-28

target

integration into IS ISO/IEC 9899:202y

document history

document number date comment
n3672 202507 Original proposal

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 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:

Additions by this paper here are:

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 as described in this clause. It has two states, locked and unlocked,FTN0) that are only observable by the behavior of the function calls associated to the type. The atomic operations are described as lock and unlock operations that operate on this state. The entry to a call to a lock operation and the return from such a call are two distinct modifications in the modification order of the mutex. The return from a successful call to a lock operation is an acquire operation (it acquires the mutex), an unlock operation on a is a release operation (it releases the mutex).
FTN0) If the mutex is recursive, a given mutex may be be locked several times by the same thread.
2 The entry to the call and the return from an unsuccessful call to a lock operation 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 function calls as well as modifications of the object representationFTN1) 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 a call to mtx_init, or whose last operation has been a call to mtx_destroy, or such that its object representation has been modified, has an indeterminate representation; performing any operation other than a call to mtx_init on such a mutex has undefined behavior.
4 After a call to mtx_init the state of the mutex is unlocked, and, for any thread, the first subsequent atomic operation performed in the modification order shall be the entry to a call to a lock operation.
5 Before a call to mtx_destroy the state of the mutex shall be unlocked, and, for any thread, the last preceding atomic operation performed in the modification order shall not be the entry to a call to a lock operation; similar requirements hold for a mutex that is not in an indeterminate state and to which a modification of the object representation is applied.
6 NOTE That means that if a thread is blocked on a mutex or holds a lock on it 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 the mutex pointed to by mtx.

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 after a call to mtx_init is not the entry to a call to a lock operation (7.30.4.1).

Acknowledgment

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