Initial:

	flag = 1;
	x = 0;
	y = 0;

CPU0 (queue work):

	x = 1;
	do {
		if (atomic_cas(&flag, 0, 1)) {
			...
			break;
		}
		membar_release();
	} while (atomic_cas(&flag, 1, 1) != 1);

CPU1 (process queued work):

	if (atomic_swap(&flag, 0)) {
		membar_acquire();
		y = x;
	}

Allowed final states:

	y = 1, flag = 0         (queued work has been processed)
	y = 0, flag = 1         (still queued, not processed)

Forbidden final states:

	y = 0, flag = 0         (neither queued nor processed)

Not sure but probably OK final states:

	y = 1, flag = 1         (processed but also queued)