Verification of Resource Sharing Protocol Implementations – A Case Study in RTEMS
To avoid race conditions and ensure data integrity, resource sharing protocols have been widely studied in real-time systems for decades. However, the corresponding realization is often based on assumed abstractions and necessary adaptions in each real-time operating system. The theoretically proven properties of such a protocol may not be delivered properly, leading to serious mismatches. This talk will go through our experience in verifying official implementation of the immediate ceiling priority protocol (ICPP) and the multiprocessor resource sharing protocol (MrsP) in RTEMS, resulting in the discovery of long-stayed mismatches.