/*
 * seqlock_aba.c — DF-4197 model harness.
 *
 * Reproduces, deterministically and under stress, the seqcount protocol
 * violation in DragonFly's Linux-compat seqlock shim
 * (sys/dev/drm/include/linux/seqlock.h) as consumed by drm_vblank.c:
 *
 *   store_vblank()            drm_vblank.c:92-106
 *   drm_vblank_count_and_time drm_vblank.c:772-791  (do { read_seqbegin;
 *                                read fields } while (read_seqretry))
 *
 * The shim (verbatim semantics, cpu fences replaced by gcc atomics):
 *   write_seqlock   : spin_lock; sl->sequence++;  fence;
 *   write_sequnlock : sl->sequence--;  spin_unlock; fence;   <-- DECREMENT
 *   read_seqbegin   : return READ_ONCE(sl->sequence);        <-- no wait-even
 *   read_seqretry   : fence; return sl->sequence != start;
 *
 * Because the sequence count RETURNS TO ITS ORIGINAL VALUE after a write
 * (0 -> 1 -> 0) instead of advancing monotonically (Linux: 0 -> 1 -> 2), a
 * reader that starts before a writer and re-checks after that writer
 * completes sees sequence == start and ACCEPTS a torn {count,time} pair.
 *
 * Modes:
 *   ./seqlock_aba demo     deterministic single-thread interleave
 *   ./seqlock_aba stress   2 threads, 4M writer cycles, count torn pairs
 *   ./seqlock_aba demo_fixed / stress_fixed   same with corrected (Linux)
 *                         semantics for comparison
 */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <pthread.h>
#include <stdbool.h>

/* ---- verbatim shim semantics (sys/dev/drm/include/linux/seqlock.h) ---- */
typedef struct {
	unsigned sequence;
	pthread_mutex_t lock;	/* stands in for struct spinlock */
} seqlock_t;

static void seqlock_init(seqlock_t *sl)
{
	sl->sequence = 0;
	pthread_mutex_init(&sl->lock, NULL);
}

static bool g_fixed_semantics = false;	/* fixed = Linux monotonic seqcount */

static void write_seqlock(seqlock_t *sl)
{
	pthread_mutex_lock(&sl->lock);
	sl->sequence++;
	__asm__ __volatile__("sfence" ::: "memory");
}

static void write_sequnlock(seqlock_t *sl)
{
	if (g_fixed_semantics)
		sl->sequence++;	/* Linux: advance past the writer */
	else
		sl->sequence--;	/* DF shim: return to original value */
	__asm__ __volatile__("sfence" ::: "memory");
	pthread_mutex_unlock(&sl->lock);
}

static unsigned read_seqbegin(const seqlock_t *sl)
{
	/* DF shim: plain load, does NOT wait for even.
	 * fixed: wait until even, like Linux read_seqcount_begin. */
	if (g_fixed_semantics) {
		unsigned s;
		do {
			s = __atomic_load_n(&sl->sequence, __ATOMIC_ACQUIRE);
		} while (s & 1);
		return s;
	}
	return __atomic_load_n(&sl->sequence, __ATOMIC_ACQUIRE);
}

static int read_seqretry(const seqlock_t *sl, unsigned start)
{
	__asm__ __volatile__("lfence" ::: "memory");
	return __atomic_load_n(&sl->sequence, __ATOMIC_ACQUIRE) != start;
}

/* ---- the drm_vblank.c pattern ---- */
struct drm_vblank_crtc_like {
	seqlock_t seqlock;
	unsigned long long count;	/* u64 count */
	long long time;			/* ktime_t time */
};

static void store_vblank(struct drm_vblank_crtc_like *vblank,
			 unsigned int vblank_count_inc, long long t_vblank)
{
	/* drm_vblank.c:102-105 */
	write_seqlock(&vblank->seqlock);
	vblank->time = t_vblank;
	vblank->count += vblank_count_inc;
	write_sequnlock(&vblank->seqlock);
}

static unsigned long long drm_vblank_count_and_time(
		struct drm_vblank_crtc_like *vblank, long long *vblanktime)
{
	/* drm_vblank.c:784-788 */
	unsigned long long vblank_count;
	unsigned int seq;

	do {
		seq = read_seqbegin(&vblank->seqlock);
		vblank_count = vblank->count;
		*vblanktime = vblank->time;
	} while (read_seqretry(&vblank->seqlock, seq));

	return vblank_count;
}

/* ---------------- deterministic demo ---------------- */
static int demo(void)
{
	struct drm_vblank_crtc_like v;
	long long t;
	unsigned seq_probe;

	seqlock_init(&v.seqlock);
	v.count = 100;
	v.time = 100000;

	printf("[demo] semantics=%s\n", g_fixed_semantics ? "FIXED(Linux)" : "DF-shim");
	fflush(stdout);

	/* reader starts (drm_vblank.c:785) */
	seq_probe = read_seqbegin(&v.seqlock);
	unsigned long long count_read_first = v.count;	/* :786 — reads OLD */
	printf("[demo] read_seqbegin -> %u; reader loaded count=%llu (preempted here...)\n",
	       seq_probe, count_read_first);
	fflush(stdout);

	/* writer preempts the reader between :786 and :787 — exactly the
	 * scenario the seqcount protocol exists to detect */
	store_vblank(&v, 1, 200000);
	printf("[demo] writer ran a FULL cycle: count=101 time=200000, sequence=%u\n",
	       v.seqlock.sequence);
	fflush(stdout);

	/* reader resumes: loads time (NEW) and re-checks */
	long long time_read = v.time;			/* :787 — reads NEW */
	int retry = read_seqretry(&v.seqlock, seq_probe);	/* :788 */

	printf("[demo] reader resumed: loaded time=%lld, read_seqretry=%d\n",
	       time_read, retry);
	if (!retry && count_read_first == 100 && time_read == 200000) {
		printf("[demo] RESULT: TORN PAIR ACCEPTED {count=100(old), time=200000(new)} — "
		       "reader believes it is consistent\n");
		return 1;	/* bug demonstrated */
	}
	printf("[demo] RESULT: retry=%d — torn pair REJECTED, reader retries\n", retry);
	return 0;
}

/* ---------------- stress ---------------- */
static struct drm_vblank_crtc_like sv;
static volatile int writer_done;
static unsigned long long torn_accepted, consistent, retried_snapshots;

static void *writer_fn(void *arg)
{
	(void)arg;
	for (int i = 0; i < 4 * 1000 * 1000; i++)
		store_vblank(&sv, 1, (long long)(i + 1) * 1000);
	writer_done = 1;
	return NULL;
}

static void *reader_fn(void *arg)
{
	(void)arg;
	long long t;
	while (!writer_done) {
		unsigned long long c = drm_vblank_count_and_time(&sv, &t);
		/* invariant of a consistent snapshot: time == count * 1000
		 * (writer stores count=n then time=n*1000 in the same
		 * write_seqlock section) */
		if (t != (long long)c * 1000)
			torn_accepted++;
		else
			consistent++;
	}
	return NULL;
}

int main(int argc, char **argv)
{
	const char *mode = argc > 1 ? argv[1] : "demo";
	g_fixed_semantics = strstr(mode, "fixed") != NULL;

	if (strcmp(mode, "demo") == 0 || strcmp(mode, "demo_fixed") == 0)
		return demo();

	/* stress */
	pthread_t w, r;
	seqlock_init(&sv.seqlock);
	sv.count = 0;
	sv.time = 0;
	pthread_create(&w, NULL, writer_fn, NULL);
	pthread_create(&r, NULL, reader_fn, NULL);
	pthread_join(w, NULL);
	pthread_join(r, NULL);
	printf("[stress] semantics=%s consistent=%llu torn_accepted=%llu\n",
	       g_fixed_semantics ? "FIXED(Linux)" : "DF-shim",
	       consistent, torn_accepted);
	return torn_accepted > 0 ? 1 : 0;
}