Documentation / litmus-tests / locking / DCL-fixed.litmus


Based on kernel version 6.9. Page generated on 2024-05-14 10:02 EST.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
C DCL-fixed

(*
 * Result: Never
 *
 * This litmus test demonstrates that double-checked locking can be
 * reliable given proper use of smp_load_acquire() and smp_store_release()
 * in addition to the locking.
 *)

{
	int flag;
	int data;
}

P0(int *flag, int *data, spinlock_t *lck)
{
	int r0;
	int r1;
	int r2;

	r0 = smp_load_acquire(flag);
	if (r0 == 0) {
		spin_lock(lck);
		r1 = READ_ONCE(*flag);
		if (r1 == 0) {
			WRITE_ONCE(*data, 1);
			smp_store_release(flag, 1);
		}
		spin_unlock(lck);
	}
	r2 = READ_ONCE(*data);
}

P1(int *flag, int *data, spinlock_t *lck)
{
	int r0;
	int r1;
	int r2;

	r0 = smp_load_acquire(flag);
	if (r0 == 0) {
		spin_lock(lck);
		r1 = READ_ONCE(*flag);
		if (r1 == 0) {
			WRITE_ONCE(*data, 1);
			smp_store_release(flag, 1);
		}
		spin_unlock(lck);
	}
	r2 = READ_ONCE(*data);
}

locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)