Analyzing singularity channel contracts

13 years 11 months ago

Download www.cs.ucsb.edu

This paper presents techniques for analyzing channel contract speciﬁcations in Microsoft Research’s Singularity operating system. A channel contract is a state machine that speciﬁes the allowable interactions between a server and a client through an asynchronous communication channel. We show that, contrary to what is claimed in the Singularity documentation, processes that faithfully follow a channel contract can deadlock. We present a realizability analysis that can be used to identify channel contracts with problems. Our realizability analysis also leads to an efﬁcient veriﬁcation approach where properties about the interaction behavior can be veriﬁed without modeling the contents of communication channels. We analyzed more than 90 channel contracts from the Singularity code distribution and documentation. Only two contracts failed our realizability condition and these two contracts allow deadlocks. Our experimental results demonstrate that realizability analysis and ve...

Zachary Stengel, Tevfik Bultan

Real-time Traffic