# Boundary-Aware Concurrent Queue: A Fast and Scalable Concurrent FIFO Queue on GPU Environments
## 3 BACQ Proposal
### Ensure Fairness and Linearizability with Tickets  
We must establish a linearizable fair queue ordering mechanism for our concurrent environment. A queue has _add (enqueue)_ and _remove (dequeue)_ methods that operate in a FIFO fashion. Items must be enqueued before they can be dequeued, and items must be dequeued in the order they were enqueued. To prove linearizability, we must identify the linearization point and show the history is a FIFO order at those linearization points. The linearization points are the publication points, which are Listing 2 Line 49 for enqueue and Listing 3 Line 43 for dequeue. Consider a history of events, \(\mathrm{H}=\{E_{1},E_{2},D_{1},E_{3},D_{2},D_{3},D_{empty},E_{4},D_{4}\}\). In this notation, \(D_{i}\) dequeues the node enqueued by \(E_{i}\). \(D_{empty}\) returns a queue empty exception and does not affect indexing. Every successful event \((E_{i},D_{i})\) will obtain a slot index from the queue. This history of events is sequential if the following relationships hold:  
\[E_{i}<E_{j}\ \wedge D_{i}<D_{j}\ \wedge E_{i}<D_{i}\ \wedge E_{i}<D_{j}\ \ \ \forall_{i}<j \tag{1}\]  
Proof. : For any request, Listing 2 Line 21 establishes the enqueue priority and similarly and Listing 3 Line 21 establishes the dequeue priority. This priority never changes. Our atomic tail counter ensures \(\forall i<j,E_{i}<E_{j}\). Our atomic head counter ensures \(\forall i<j,D_{i}<D_{j}\). Since a node must be enqueued before it can be dequeued, we have \(E_{i}<D_{i}\). Thus, for \(\forall i<j\), we have \(E_{i}<D_{i}\wedge E_{i}<D_{j}\). On GPUs, it is common to encounter multiple requests targeting the same index position simultaneously. We introduce a unique ticketing system for concurrent requests targeting the same index position to address this. Each request, whether an enqueue (\(E_{i}\)) or dequeue (\(D_{i}\)), awaits publication until it matches the desired ticket number. The desired ticket for \(E_{i}\) and \(D_{i}\) will be calculated as:  
Desired \(Ticket_{E_{i}}\ =\ 2\ *\ [tail/N]\)  
Desired \(Ticket_{D_{i}}\ =\ 2\ *\ [head/N]+1\)  
Here, N represents the buffer size of the queue, and tail and head are counters indicating the tail and head positions of the queue, respectively. When a request reaches the same index position after N operations, the desired ticket is updated as follows:  
Desired \(Ticket_{E_{i+N}}\ =\ 2\ *\ [tail+N)/N]\ =\ 2\ *\ [tail/N]\ +\ 2\)  
Desired \(Ticket_{D_{i+N}}\ =\ 2\ *\ [head+N)/N]\ +\ 1\ =\ 2\ *\ [tail/N]\ +\ 3\)  
This ticketing system ensures that the ticket value continuously increases for each request, thereby maintaining a FIFO ordering at the time of publication. We employ fetch-and-add operations on the head and tail counters, which, in conjunction with a per-element ticketing system, ensures fair ordering. We handle boundary conditions before the FAA operation on the head and tail counters to guarantee the operations' fairness. Moreover, this approach does not confine head and tail counters within the buffer size bounds; rather, it emulates an infinite-length array. So, whenever a thread establishes its FIFO order, there is no risk that the thread will experience interference from failed CAS attempts in other threads. In our experiment, we measured the elapsed time for both enqueue-only and dequeue-only scenarios to understand any differences in their execution times. Figure 14 illustrates  
Figure 13: Fair publication order for an enqueue request. that regardless of the number of requests, both the enqueue and dequeue methods exhibit similar performance characteristics. This observation suggests that once the order is established, neither operation significantly outpaces the other. Three cases remain to ensure linearizability: enqueuing to a full queue, dequeuing from an empty queue, and dequeuing while an enqueue into an empty queue is in progress. Queue Empty: This exception occurs whenever head overtaken tail reads (Listing 3 Line 3).