Lock Management

Source code annotations are an efficient way to refine the assertions you make about the locks in your code. There are three types of assertions: protection, order, and side effects.

Protection assertions state what is protected by a given lock. For example, the following source code annotations can be used to assert how data is protected.

MUTEX_PROTECTS_DATA

RWLOCK_PROTECTS_DATA

SCHEME_PROTECTS_DATA

DATA_READABLE_WITHOUT_LOCK

RWLOCK_COVERS_LOCK

A variation of the assert subcommand is used to assert that a given lock protects some piece of data or a function. Another variation, assert ... covers, asserts that a given lock protects another lock; this is used for hierarchical locking schemes.

Order assertions specify the order in which the given locks must be acquired. The source code annotation LOCK_ORDER or the assert order subcommand can be used to specify lock ordering.

Side effect assertions state that a function has the side effect of releasing or acquiring a given lock. Use the following source code annotations:

MUTEX_ACQUIRED_AS_SIDE_EFFECT

READ_LOCK_ACQUIRED_AS_SIDE_EFFECT

WRITE_LOCK_ACQUIRED_AS_SIDE_EFFECT

LOCK_RELEASED_AS_SIDE_EFFECT

LOCK_UPGRADED_AS_SIDE_EFFECT

LOCK_DOWNGRADED_AS_SIDE_EFFECT

NO_COMPETING_THREADS_AS_SIDE_EFFECT

COMPETING_THREADS_AS_SIDE_EFFECT

You can also use the assert side effect subcommand to specify side effects. In some cases you may want to make side effect assertions about an external function and the lock is not visible from the loaded module (for example, it is static to the module of the external function). In such a case, you can "create" a lock by using a form of the declare subcommand.