Initial memory:

	flag = 1;
	x = 0;

	resched = 0;            CPU0 private
	y = 0;                  CPU1 private

CPU0 (queue work):

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

CPU1 (process queued work):

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

Allowed final states:

	resched = 0, y = 1      (queued work has been processed)
	resched = 1, y = 0      (not processed but will be rescheduled)

Forbidden final states:

	resched = 0, y = 0      (not processed but won't be rescheduled)

Not sure but probably OK final states:

	resched = 1, y = 1      (processed and will also be rescheduled)