uu.seUppsala University Publications
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 read-copy update (RCU)
Max Planck Inst Software Syst MPI SWS, Kaiserslautern Saarbruke, Germany.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.ORCID iD: 0000-0001-9657-0179
2019 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 21, no 3, p. 287-306Article in journal (Refereed) Published
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 a 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 article presents an approach to systematically test the code of the main implementation of RCU used in the Linux kernel (Tree RCU) for concurrency errors, both under sequentially consistent 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. Additionally, we present the real cause behind some failures that have been observed in production systems in the past. More importantly, we were able to verify both the publish-subscribe and the grace-period guarantee, with the latter being the basic and most important guarantee that RCU offers, on several Linux kernel versions, for particular configurations. 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 hold that our effort constitutes a good first step toward making tools such as Nidhugg part of the standard testing infrastructure of the Linux kernel.

Place, publisher, year, edition, pages
SPRINGER HEIDELBERG , 2019. Vol. 21, no 3, p. 287-306
Keywords [en]
Software model checking, Linux kernel, Read-copy update, Nidhugg
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-384993DOI: 10.1007/s10009-019-00514-6ISI: 000468116300004OAI: oai:DiVA.org:uu-384993DiVA, id: diva2:1324003
Available from: 2019-06-13 Created: 2019-06-13 Last updated: 2019-06-13Bibliographically approved

Open Access in DiVA

fulltext(2347 kB)16 downloads
File information
File name FULLTEXT01.pdfFile size 2347 kBChecksum SHA-512
bc2355f2d8c9a34ebb2369ba42a728741c308b817e6585dfe183e0b1714b36cf375a6d38a494f2f40b0c55b7a486f8741faa119c8bdf31b02de6c304a90a5087
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Sagonas, Konstantinos

Search in DiVA

By author/editor
Sagonas, Konstantinos
By organisation
Computing Science
In the same journal
International Journal on Software Tools for Technology Transfer (STTT)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 16 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 206 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