Modular Verification of Concurrent Thread Management

Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

Thread management is an essential functionality in OS kernels. However, verification of thread management remains a challenge, due to two conflicting requirements: on the one hand, a thread manager—operating below the thread abstraction layer–should hide its implementation details and be verified independently from the threads being managed; on the other hand, the thread management code in many real-world systems is concurrent, which might be executed by the threads being managed, so it seems inappropriate to abstract threads away in the verification of thread managers. Previous approaches on kernel verification view thread managers as sequential code, thus cannot be applied to thread management in realistic kernels. In this paper, we propose a novel two-layer framework to verify concurrent thread management. We choose a lower abstraction level than the previous approaches, where we abstract away the context switch routine only, and allow the rest of the thread management code to run concurrently in the upper level. We also treat thread management data as abstract resources so that threads in the environment can be specified in assertions and be reasoned about in a proof system similar to concurrent separation logic.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication10th Asian Symposium, APLAS 2012, Proceedings
EditorsRanjit Jhala, Atsushi Igarashi
PublisherSpringer
Pages315-331
Number of pages17
Volume7705
ISBN (Electronic)9783642351822
ISBN (Print)9783642351815
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event10th Asian Symposium on Programming Languages and Systems - Kyoto International Community House, Kyoto, Japan
Duration: 11 Dec 201213 Dec 2012
Conference number: 10
http://aplas12.kuis.kyoto-u.ac.jp/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume7705
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th Asian Symposium on Programming Languages and Systems
Abbreviated titleAPLAS 2012
CountryJapan
CityKyoto
Period11/12/1213/12/12
Internet address

Fingerprint Dive into the research topics of 'Modular Verification of Concurrent Thread Management'. Together they form a unique fingerprint.

  • Cite this

    Guo, Y., Feng, X., Shao, Z., & Shi, P. (2012). Modular Verification of Concurrent Thread Management. In R. Jhala, & A. Igarashi (Eds.), Programming Languages and Systems: 10th Asian Symposium, APLAS 2012, Proceedings (Vol. 7705, pp. 315-331). (Lecture Notes in Computer Science; Vol. 7705). Springer. https://doi.org/10.1007/978-3-642-35182-2_23