#pragma once

#define __CFA_NO_SCHED_STATS__

#include "limits.hfa"

// Intrusives lanes which are used by the relaxed ready queue
struct __attribute__((aligned(128))) __intrusive_lane_t {
	struct thread$ * prev;

	// spin lock protecting the queue
	volatile bool lock;

	__thread_desc_link anchor;

	#if !defined(__CFA_NO_STATISTICS__)
		unsigned cnt;
	#endif
};

// Get the head pointer (one before the first element) from the anchor
static inline thread$ * mock_head(const __intrusive_lane_t & this) {
	thread$ * rhead = (thread$ *)(
		(uintptr_t)( &this.anchor ) - __builtin_offsetof( thread$, link )
	);
	return rhead;
}

// Push a thread onto this lane
// returns true of lane was empty before push, false otherwise
static inline void push( __intrusive_lane_t & this, thread$ * node ) {
	/* paranoid */ verify( this.lock );
	/* paranoid */ verify( node->link.next == 0p );
	/* paranoid */ verify( node->link.ts   == MAX  );
	/* paranoid */ verify( this.prev->link.next == 0p );
	/* paranoid */ verify( this.prev->link.ts   == MAX  );
	if( this.anchor.next == 0p ) {
		/* paranoid */ verify( this.anchor.next == 0p );
		/* paranoid */ verify( this.anchor.ts   == MAX );
		/* paranoid */ verify( this.anchor.ts   != 0  );
		/* paranoid */ verify( this.prev == mock_head( this ) );
	} else {
		/* paranoid */ verify( this.anchor.next != 0p );
		/* paranoid */ verify( this.anchor.ts   != MAX );
		/* paranoid */ verify( this.anchor.ts   != 0  );
		/* paranoid */ verify( this.prev != mock_head( this ) );
	}

	// Get the relevant nodes locally
	this.prev->link.next = node;
	this.prev->link.ts   = rdtscl();
	this.prev = node;
	#if !defined(__CFA_NO_STATISTICS__)
		this.cnt++;
	#endif
}

// Pop a thread from this lane (must be non-empty)
// returns popped
// returns true of lane was empty before push, false otherwise
static inline [* thread$, unsigned long long] pop( __intrusive_lane_t & this ) {
	/* paranoid */ verify( this.lock );
	/* paranoid */ verify( this.anchor.next != 0p );
	/* paranoid */ verify( this.anchor.ts   != MAX );
	/* paranoid */ verify( this.anchor.ts   != 0  );

	// Get the relevant nodes locally
	thread$ * node = this.anchor.next;
	this.anchor.next = node->link.next;
	this.anchor.ts   = node->link.ts;
	bool is_empty = this.anchor.next == 0p;
	node->link.next = 0p;
	node->link.ts   = ULLONG_MAX;
	#if !defined(__CFA_NO_STATISTICS__)
		this.cnt--;
	#endif

	// Update head time stamp
	if(is_empty) this.prev = mock_head( this );

	/* paranoid */ verify( node->link.next == 0p );
	/* paranoid */ verify( node->link.ts   == MAX  );
	/* paranoid */ verify( node->link.ts   != 0  );
	/* paranoid */ verify( this.anchor.ts  != 0  );
	/* paranoid */ verify( (this.anchor.ts  == MAX) == is_empty );
	return [node, this.anchor.ts];
}

// Check whether or not list is empty
static inline bool is_empty(__intrusive_lane_t & this) {
	return this.anchor.next == 0p;
}

// Return the timestamp
static inline unsigned long long ts(__intrusive_lane_t & this) {
	// Cannot verify 'emptiness' here since it may not be locked
	/* paranoid */ verify(this.anchor.ts != 0);
	return this.anchor.ts;
}