uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU)
National Technical University of Athens, Greece.ORCID iD: 0000-0002-7905-9739
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.ORCID iD: 0000-0001-9657-0179
2017 (English)In: Proc. 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, New York: ACM Press, 2017, p. 172-181Conference paper, Published paper (Refereed)
Abstract [en]

Read-Copy-Update (RCU) is a synchronization mechanism used heavily in key components of the Linux kernel, such as the virtual filesystem (VFS), to achieve scalability by exploiting RCU's ability to allow concurrent reads and updates. RCU's design is non-trivial, requires significant effort to fully understand it, let alone become convinced that its implementation is faithful to its specification and provides its claimed properties. The fact that as time goes by Linux kernels are becoming increasingly more complex and are employed in machines with more and more cores and weak memory does not make the situation any easier.

This paper presents an approach to systematically test the code of the main flavor of RCU used in the Linux kernel (Tree RCU) for concurrency errors, both under sequential consistency and weak memory. Our modeling allows Nidhugg, a stateless model checking tool, to reproduce, within seconds, safety and liveness bugs that have been reported for RCU. More importantly, we were able to verify the Grace-Period guarantee, the basic guarantee that RCU offers, on several Linux kernel versions (non-preemptible builds). Our approach is effective, both in dealing with the increased complexity of recent Linux kernels and in terms of time that the process requires. We have good reasons to believe that our effort constitutes a big step towards making tools such as Nidhugg part of the standard testing infrastructure of the Linux kernel.

Place, publisher, year, edition, pages
New York: ACM Press, 2017. p. 172-181
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-333910DOI: 10.1145/3092282.3092287ISI: 000455699900022ISBN: 978-1-4503-5077-8 (print)OAI: oai:DiVA.org:uu-333910DiVA, id: diva2:1158231
Conference
SPIN 2017, July 13–14, Santa Barbara, CA
Projects
UPMARC
Funder
Swedish Research Council, 621-2017-04812Available from: 2017-07-13 Created: 2017-11-18 Last updated: 2019-02-26Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Sagonas, Konstantinos

Search in DiVA

By author/editor
Kokologiannakis, MichalisSagonas, Konstantinos
By organisation
Computing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 128 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf