/*
 * Deterministic ABA replay on the Michael-Scott queue of msq.h.
 * One OS thread plays T1, T2 and T3 in a fixed interleaving: T1 runs
 * D2..D12 of a dequeue, the others run whole operations, then T1 runs D13.
 *
 *   gcc -std=c11 -O2 aba_demo.c -o aba_counted
 *   gcc -std=c11 -O2 -DMSQ_NO_COUNT aba_demo.c -o aba_nocount
 */
#include "msq.h"
#include <stdio.h>

static const char *name(uint32_t i)
{
    static const char *n[] = {"S", "n1", "n2", "B", "A"};
    return i < 5 ? n[i] : "nil";
}

static bool in_free_list(msq *q, uint32_t i)
{
    for (uint32_t k = IDX(atomic_load(&q->free_top)); k != MSQ_NIL;
         k = (uint32_t)atomic_load(&q->nodes[k].free_next))
        if (k == i)
            return true;
    return false;
}

static void show(msq *q, const char *when)
{
    uint64_t h = atomic_load(&q->head), t = atomic_load(&q->tail);
    printf("  %-28s Head=%s(cnt %u)%s  Tail=%s(cnt %u)%s\n", when,
           name(IDX(h)), CNT(h), in_free_list(q, IDX(h)) ? " [free!]" : "",
           name(IDX(t)), CNT(t), in_free_list(q, IDX(t)) ? " [free!]" : "");
}

int main(void)
{
    msq q;
    uint64_t v;
    msq_init(&q, 4); /* dummy is node 0 (S); free list pops 4, 3, 2, 1 */
    msq_enqueue(&q, 'a'); /* node 4 = A */
    msq_enqueue(&q, 'b'); /* node 3 = B */
    show(&q, "initial S->A(a)->B(b):");

    /* T1: D2..D12, then preempted just before the CAS at D13 */
    uint64_t head = atomic_load(&q.head);
    uint64_t next = atomic_load(&q.nodes[IDX(head)].next);
    uint64_t t1v = atomic_load(&q.nodes[IDX(next)].value);
    printf("T1 reads head=%s(cnt %u) next=%s value=%c, then stalls\n",
           name(IDX(head)), CNT(head), name(IDX(next)), (int)t1v);

    msq_dequeue(&q, &v); printf("T2 dequeue -> %c (frees S)\n", (int)v);
    msq_dequeue(&q, &v); printf("T2 dequeue -> %c (frees A)\n", (int)v);
    msq_enqueue(&q, 'c'); printf("T3 enqueue c (reuses node A)\n");
    msq_enqueue(&q, 'd'); printf("T3 enqueue d (reuses node S)\n");
    msq_dequeue(&q, &v); printf("T2 dequeue -> %c (frees B)\n", (int)v);
    msq_dequeue(&q, &v); printf("T2 dequeue -> %c (frees A)\n", (int)v);
    show(&q, "before T1 resumes:");

    /* T1 resumes at D13 */
    uint64_t expect = head;
    bool ok = atomic_compare_exchange_strong(
        &q.head, &expect, PACK(IDX(next), BUMP(CNT(head))));
    if (ok) {
        pool_put(&q, IDX(head)); /* D19 */
        printf("T1 CAS(Head, S, A) SUCCEEDS -> returns %c again\n", (int)t1v);
    } else {
        printf("T1 CAS(Head, S, A) fails: Head is S(cnt %u), not S(cnt %u)\n",
               CNT(expect), CNT(head));
        printf("T1 retries: dequeue -> %s\n",
               msq_dequeue(&q, &v) ? "value" : "EMPTY");
    }
    show(&q, "after T1:");
    msq_destroy(&q);
    return 0;
}