Rely-guarantee reasoning about concurrent memory management in zephyr RTOs

12Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

Abstract

Formal verification of concurrent operating systems (OSs) is challenging, and in particular the verification of the dynamic memory management due to its complex data structures and allocation algorithm. Up to our knowledge, this paper presents the first formal specification and mechanized proof of a concurrent buddy memory allocation for a real-world OS. We develop a fine-grained formal specification of the buddy memory management in Zephyr RTOS. To ease validation of the specification and the source code, the provided specification closely follows the C code. Then, we use the rely-guarantee technique to conduct the compositional verification of functional correctness and invariant preservation. During the formal verification, we found three bugs in the C code of Zephyr.

Cite

CITATION STYLE

APA

Zhao, Y., & Sanán, D. (2019). Rely-guarantee reasoning about concurrent memory management in zephyr RTOs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11562 LNCS, pp. 515–533). Springer Verlag. https://doi.org/10.1007/978-3-030-25543-5_29

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free