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.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.