dtact 0.2.6

use dtact::dta_scheduler::{Mailbox, TaskChunk, Warehouse};
use dtact::memory_management::{ContextPool, FiberContext, FiberStatus, SafetyLevel};
use loom::sync::Arc;
use loom::sync::atomic::Ordering;
use loom::thread;

// ---------------------------------------------------------------------------
// Helper: a preemption-bounded loom::model builder.
//
// Loom's default mode exhaustively enumerates *every* interleaving, including
// all spurious CAS failures in a `compare_exchange_weak` retry loop.  For
// algorithms that retry until success (ContextPool free-list, Warehouse MPMC)
// this causes exponential branch counts.
//
// `preemption_bound(N)` restricts exploration to executions where each thread
// is preempted at most N times.  This still finds all single-preemption races
// (the most common in practice) while keeping runtime bounded.
//
// References: tokio / crossbeam use the same pattern.
fn bounded_model<F: Fn() + Sync + Send + 'static>(f: F) {
    let mut builder = loom::model::Builder::new();
    builder.preemption_bound = Some(2);
    builder.max_branches = 10_000;
    builder.check(f);
}

// ---------------------------------------------------------------------------
// Test 1: Production FiberContext state-machine transitions
//
// Verifies that the Running → Suspending → Yielded path and the concurrent
// waker's Notified write race correctly under all interleavings.  Uses the
// actual production `FiberContext::state` atomic rather than a mock.
// ---------------------------------------------------------------------------
#[cfg_attr(miri, ignore)]
#[test]
fn test_production_fiber_state_transitions() {
    loom::model(|| {
        let ctx = Arc::new(FiberContext::new());

        // Dispatch loop picks it up.
        ctx.state
            .store(FiberStatus::Running as u32, Ordering::Release);

        let ctx_clone = ctx.clone();

        // Waker thread: simulates `wake_by_ref_impl` swapping to Notified.
        let waker = thread::spawn(move || {
            let prev = ctx_clone
                .state
                .swap(FiberStatus::Notified as u32, Ordering::AcqRel);
            if prev == FiberStatus::Yielded as u32 {
                // Would enqueue the fiber — simulated here.
            }
        });

        // Fiber thread: simulates `wait_pinned`'s Running→Suspending CAS.
        let waiter = thread::spawn(move || {
            let cur_state = ctx.state.load(Ordering::Acquire);
            if cur_state != FiberStatus::Running as u32 {
                ctx.state
                    .store(FiberStatus::Running as u32, Ordering::Release);
            }

            // CAS: only suspend if no waker has fired.
            if ctx
                .state
                .compare_exchange(
                    FiberStatus::Running as u32,
                    FiberStatus::Suspending as u32,
                    Ordering::Release,
                    Ordering::Acquire,
                )
                .is_ok()
            {
                // Fiber suspended correctly.
            }
        });

        waker.join().unwrap();
        waiter.join().unwrap();
    });
}

// ---------------------------------------------------------------------------
// Test 2: ContextPool lock-free free-list (alloc + free)
//
// Verifies that concurrent alloc_context / free_context never lose or
// double-free a slot, exercising the ABA-protected 64-bit CAS on `free_head`.
// ---------------------------------------------------------------------------
#[cfg_attr(miri, ignore)]
#[test]
fn test_production_context_pool_alloc_free() {
    bounded_model(|| {
        let pool = Arc::new(ContextPool::new(2, 8192, SafetyLevel::Safety0, 0).expect("pool init"));

        let p1 = pool.clone();
        let t1 = thread::spawn(move || {
            if let Some(idx) = p1.alloc_context() {
                p1.free_context(idx);
            }
        });

        let p2 = pool.clone();
        let t2 = thread::spawn(move || {
            if let Some(idx) = p2.alloc_context() {
                p2.free_context(idx);
            }
        });

        t1.join().unwrap();
        t2.join().unwrap();
    });
}

// ---------------------------------------------------------------------------
// Test 3: Mailbox SPSC push/pop
//
// The Mailbox is a single-producer/single-consumer ring.  We verify that
// a concurrent push and pop either both succeed or correctly observe empty/full.
// No retry loop — loom can exhaustively enumerate the two-thread schedule.
// ---------------------------------------------------------------------------
#[cfg_attr(miri, ignore)]
#[test]
fn test_production_mailbox_spsc() {
    loom::model(|| {
        let mailbox = Arc::new(Mailbox::new());

        let m1 = mailbox.clone();
        let producer = thread::spawn(move || {
            let chunk = TaskChunk::default();
            let _ = m1.push(chunk);
        });

        let m2 = mailbox.clone();
        let consumer = thread::spawn(move || {
            let _ = m2.pop();
        });

        producer.join().unwrap();
        consumer.join().unwrap();
    });
}

// ---------------------------------------------------------------------------
// Test 4: Warehouse MPMC push/pop
//
// The Warehouse uses a Vyukov-style bounded MPMC ring with CAS retry loops
// and staggered backoff.  `preemption_bound(2)` keeps branch counts
// manageable while still finding the most common data races (single and
// double preemptions).
// ---------------------------------------------------------------------------
#[cfg_attr(miri, ignore)]
#[test]
fn test_production_warehouse_mpmc() {
    bounded_model(|| {
        let warehouse = Arc::new(Warehouse::new());

        let w1 = warehouse.clone();
        let producer = thread::spawn(move || {
            let chunk = TaskChunk::default();
            let _ = w1.push(chunk);
        });

        let w2 = warehouse.clone();
        let consumer = thread::spawn(move || {
            let _ = w2.pop();
        });

        producer.join().unwrap();
        consumer.join().unwrap();
    });
}

// ---------------------------------------------------------------------------
// Test 5: Warehouse 2-producer / 1-consumer contention
//
// Exercises the thundering-herd scenario where two producers race on the
// same `tail` slot, verifying that exactly the right number of backlog
// increments occur.
// ---------------------------------------------------------------------------
#[cfg_attr(miri, ignore)]
#[test]
fn test_production_warehouse_two_producers() {
    bounded_model(|| {
        let warehouse = Arc::new(Warehouse::new());

        let w1 = warehouse.clone();
        let p1 = thread::spawn(move || {
            let _ = w1.push(TaskChunk::default());
        });

        let w2 = warehouse.clone();
        let p2 = thread::spawn(move || {
            let _ = w2.push(TaskChunk::default());
        });

        let w3 = warehouse.clone();
        let c1 = thread::spawn(move || {
            let _ = w3.pop();
        });

        p1.join().unwrap();
        p2.join().unwrap();
        c1.join().unwrap();
    });
}