Using Model Checking to Debug Network Interface Firmware

Network interface rm ware is a piece of concurrent software that achieves high performance at the cost of software com- plexity. They contain subtle race conditions that make them dicult to debug using traditional debugging techniques. The problem is further compounded by the lack of debugging support on the devices. This is a serious problem because the device rm ware is trusted by the operating system. ESP is a language for programmable devices. It allows the use of model checkers to debug device rm ware. The use of model checkers allows the rm ware to be extensively tested. This paper describes the techniques used by the ESP com- piler to extract models that can be used by the model checker. Since model checking involves an exponential search, the model provided have to be fairly small to allow eectiv e model checking. Our earlier eorts yielded models that were too large to check for system-wide properties. The new version of the compiler uses abstraction to generate much smaller models. The paper also presents our experience with using the model checker to develop and debug the VMMC rm ware for the myrinet network interfaces. The new version of the compiler generated abstract models that was used to check for system-wide properties like absence of deadlocks. The model checker found several bugs in the rm ware using these models. Since the bugs were xed, we have not encountered any bugs while running the rm ware on the device.