Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915548984508416 |
|---|---|
| author | Chalmers, Kevin Pedersen, Jan Bækgaard |
| author_facet | Chalmers, Kevin Pedersen, Jan Bækgaard |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_10818 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes Chalmers, Kevin Pedersen, Jan Bækgaard Distributed, Parallel, and Cluster Computing 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. |
| title | Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes |
| topic | Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2510.10818 |