{"ID":2856912,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.10818","arxiv_id":"2510.10818","title":"Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes","abstract":"We present the first spin-free, kernel-lock-free mutex that cooperates with user-mode schedulers and is formally proven FIFO-fair and linearizable using CSP/FDR. Our fairness oracle and stability-based proof method are reusable across coroutine runtime designs. We designed the claim/release protocol for a process-oriented language -- ProcessJ -- to manage the race for claiming shared inter-process communication channels. Internally, we use a lock-free queue to park waiting processes for gaining access to a shared object, such as exclusive access to a shared channel to read from or write to. The queue ensures control and fairness for processes wishing to access a shared resource, as the protocol handles claim requests in the order they are inserted into the queue. We produce CSP models of our protocol and a mutex specification, demonstrating with FDR that our protocol behaves as a locking mutex.","short_abstract":"We present the first spin-free, kernel-lock-free mutex that cooperates with user-mode schedulers and is formally proven FIFO-fair and linearizable using CSP/FDR. Our fairness oracle and stability-based proof method are reusable across coroutine runtime designs. We designed the claim/release protocol for a process-orien...","url_abs":"https://arxiv.org/abs/2510.10818","url_pdf":"https://arxiv.org/pdf/2510.10818v1","authors":"[\"Kevin Chalmers\",\"Jan Bækgaard Pedersen\"]","published":"2025-10-12T21:58:52Z","proceeding":"cs.DC","tasks":"[\"cs.DC\"]","methods":"[]","has_code":false}