Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2407.20559 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916339281559552 |
|---|---|
| author | Colvin, Robert J. Hayes, Ian J. Heiner, Scott Höfner, Peter Meinicke, Larissa Su, Roger C. |
| author_facet | Colvin, Robert J. Hayes, Ian J. Heiner, Scott Höfner, Peter Meinicke, Larissa Su, Roger C. |
| contents | Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the code as written, the effects of which are typically summarised as a "weak memory model" - a term which includes further complicating factors that may be introduced by compiler optimisations. In many cases, the nondeterminism inherent in weak memory models can be expressed as micro-parallelism, i.e., parallelism within threads and not just between them. Fortunately Jones' rely/guarantee reasoning provides a compositional method for shared-variable concurrency, whether that be in terms of communication between top-level threads or micro-parallelism within threads. In this paper we provide an in-depth verification of the lock algorithm used in the seL4 microkernel, using rely/guarantee to handle both interthread communication as well as micro-parallelism introduced by weak memory models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_20559 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures Colvin, Robert J. Hayes, Ian J. Heiner, Scott Höfner, Peter Meinicke, Larissa Su, Roger C. Logic in Computer Science Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the code as written, the effects of which are typically summarised as a "weak memory model" - a term which includes further complicating factors that may be introduced by compiler optimisations. In many cases, the nondeterminism inherent in weak memory models can be expressed as micro-parallelism, i.e., parallelism within threads and not just between them. Fortunately Jones' rely/guarantee reasoning provides a compositional method for shared-variable concurrency, whether that be in terms of communication between top-level threads or micro-parallelism within threads. In this paper we provide an in-depth verification of the lock algorithm used in the seL4 microkernel, using rely/guarantee to handle both interthread communication as well as micro-parallelism introduced by weak memory models. |
| title | Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.20559 |