SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification

This paper introduces SimplMM, a novel subsystem within the Certified Concurrent Abstraction Layers (CCAL) modular software verification framework, designed specifically for fine-grained concurrent software. SimplMM aims to provide a generic, practical, and realistic multicore machine model for verifying software within the CCAL framework. While formal multicore hardware semantics have seen extensive development, their integration with large-scale software verification has received limited attention. To address this gap, we propose a novel approach: a toolkit comprising a generic sequentially consistent multicore semantics, contextual refinement templates, and libraries. These components establish crucial connections between the machine model and verified program modules (layers) using CCAL. We demonstrate the practicality of our framework by successfully integrating it with existing large-scale proofs, specifically for CertiKOS running on top of the x86 hardware architecture. This research significantly advances the field of accurate and efficient concurrent software verification and development tools for multicore systems. Our provision of a practical and formal multicore machine model, seamlessly integrated within the CCAL framework, equips developers with a powerful toolkit for large-scale concurrent software verification. The effectiveness of our approach, validated through successful integration with existing large-scale proofs such as CertiKOS, establishes a robust foundation for the design and verification of concurrent software in multicore systems.