Analyzing singularity channel contracts

This paper presents techniques for analyzing channel contract spec- ifications in Microsoft Research's Singularity operating s ystem. A channel contract is a state machine that specifies the allowa ble in- teractions between a server and a client through an asynchro nous communication channel. We show that, contrary to what is claimed in the Singularity documentation, processes that faithful ly follow a channel contract can deadlock. We present a realizability a naly- sis that can be used to identify channel contracts with probl ems. Our realizability analysis also leads to an efficient verific ation ap- proach where properties about the interaction behavior can be ver- ified without modeling the contents of communication channe ls. We analyzed more than 90 channel contracts from the Singular- ity code distribution and documentation. Only two contracts failed our realizability condition and these two contracts allow d eadlocks. Our experimental results demonstrate that realizability a nalysis and verification of channel contracts can be done efficiently usi ng our approach.