Prof. Tevfik Bultan and M.S. student Zachary Stengel identified a flaw in a novel operating system developed by Microsoft Research called Singularity. Although Singularity operating system has been developed with the goal of improving dependability, due to this flaw, Singularity processes were vulnerable to deadlocks. In a paper published in the 2009 International Symposium on Software Testing and Analysis (ISSTA 2009), the leading research conference in software testing and analysis, Prof. Bultan and Mr. Stengel discuss this flaw, its effects and how it can be fixed.
In order to improve the dependability of software systems, Singularity operating system uses process isolation. Singularity processes are not allowed to share memory to avoid situations where a buggy process crashes the whole system. Instead, all inter-process communication occurs via message passing over bidirectional conduits, called channels. Singularity processes are required to specify a channel contract that identifies the sequences of messages that can be sent through a given channel. In return, the Singularity system is supposed to guarantee that processes that follow the same contract can interact with each other without any problems such as deadlocks. In their paper, Prof. Bultan and Mr. Stengel show that this is not the case, and, in fact, Singularity processes can deadlock even when they faithfully implement a contract. Moreover, Prof. Bultan and Mr. Stengel present a condition for channel contracts, if checked, guarantees deadlock free communication among processes. The paper can be found at: http://www.cs.ucsb.edu/~vlab/publications.html