Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2024)

<Previous Article In Volume
Next Article In Volume>

Formalizing Resource Ownership Semantics of Spinlocks with the Coq Proof Assistant

Authors
Sebastian Luis S. Ortiz1, *, Justin Gabriel R. Enriquez1, Henry N. Adorna1, Alfonso B. Labao1
1Department of Computer Science, College of Engineering, University of the Philippines - Diliman, Quezon City, NCR, Philippines
*Corresponding author. Email: ssortiz@up.edu.ph
Corresponding Author
Sebastian Luis S. Ortiz
Available Online 30 April 2025.
DOI
10.2991/978-94-6463-684-0_11How to use a DOI?
Keywords
Coq proof assistant; separation logic; resource ownership semantics; concurrency; multithreading; mutex; spinlock
Abstract

As the transistor count in modern central processing units (CPUs) reaches the physical limits of Moore’s Law, the parallelization of software-based compute has become the next step in maximizing the instruction-level and thread-level parallelism of modern multi-core architectures (e.g., advanced superscalar pipelined processors). With race conditions, memory corruption, and access violations afoot, systems level programmers need fast, efficient, and correct concurrency primitives upon which to build concurrent data structures. One such primitive is the lock. This paper explores how the Coq proof assistant can be used to formalize and prove the correctness of these primitives. The case study focuses on the simplest implementation of a mutual exclusion lock: the spinlock. It focuses on defining the core functions that define the spinlock arrangement, albeit with some strong assumptions regarding the acquirement of locks. It is shown that a model based on resource ownership semantics is simpler to fathom and prove than tree-based alternatives that model non-determinism as branched and interleaved thread execution.

Copyright
© 2025 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

<Previous Article In Volume
Next Article In Volume>
Volume Title
Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2024)
Series
Atlantis Highlights in Computer Sciences
Publication Date
30 April 2025
ISBN
978-94-6463-684-0
ISSN
2589-4900
DOI
10.2991/978-94-6463-684-0_11How to use a DOI?
Copyright
© 2025 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Cite this article

risenwbib
TY  - CONF
AU  - Sebastian Luis S. Ortiz
AU  - Justin Gabriel R. Enriquez
AU  - Henry N. Adorna
AU  - Alfonso B. Labao
PY  - 2025
DA  - 2025/04/30
TI  - Formalizing Resource Ownership Semantics of Spinlocks with the Coq Proof Assistant
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2024)
PB  - Atlantis Press
SP  - 167
EP  - 178
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6463-684-0_11
DO  - 10.2991/978-94-6463-684-0_11
ID  - Ortiz2025
ER  -